Agnishom

• Results from [ThatiR05]
  • Algorithm is referred to as resolving the past and deriving the future
    • involves transforming the formula
  • Metric Temporal Logic with both Past and Future
  • Upperbounds
    • MTL + Past + Future
      • Space: $O(m 2^m)$
      • Time: $O(m^3 2^{3m})$ for processing each event
• $m$ is size of formula + sum of numercal constants

Agnishom

Require Export Setoid.
Require Export Relation_Definitions.

Section ASet.

Declare Scope aset_scope.
Delimit Scope aset_scope with aset. (* so that we can write term%aset *)

Open Scope aset_scope.

Agnishom

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith. 

Import ListNotations.

Require Import Coq.Init.Nat.
Require Import Lia.

Agnishom

// g++ -o boostregex-test boostregex-test.cpp -lboost_regex

#include <fstream>
#include <vector>
#include <string>
#include <iostream>
#include <sstream>
#include <iomanip>
#include <chrono>
#include <boost/regex.hpp> 

Agnishom

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.

Import ListNotations.

Require Import Coq.Init.Nat.
Require Import Lia.

Agnishom

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.

Import ListNotations.

Require Import Coq.Init.Nat.

Require Import Recdef.
Require Import FunInd.
Require Import Coq.Program.Wf.

Agnishom

Require Import Coq.Lists.List.

Declare Scope regex_scope.
Open Scope regex_scope.

Section Regex.

Variable (A : Type).

Inductive Regex : Type :=

Agnishom

(* 
  
  Some lemmas that can be used in conjunction with those in Coq.Lists.List
  
  See https://coq.inria.fr/library/Coq.Lists.List.html
 
 *)

 Require Import Lia.
 Require Import Coq.Lists.List.

Agnishom

#include <iostream>
#include <string>
#include <pcre.h>
#include <chrono>

using namespace std;

int main() {
    string pattern;
    string input;

Agnishom

use std::collections::VecDeque;
use std::cell::RefCell;
use std::rc::Rc;
use std::cell::Ref;

pub mod vllsimple;
use vllsimple::*;

struct part_man{
    // pools