Theory Monitor
theory Monitor
imports
Formula
Optimized_Join
"MFOTL_Monitor.Abstract_Monitor"
"HOL-Library.While_Combinator"
"HOL-Library.Mapping"
"Deriving.Derive"
"Generic_Join.Generic_Join_Correctness"
begin
section ‹Generic monitoring algorithm›
text ‹The algorithm defined here abstracts over the implementation of the temporal operators.›
subsection ‹Monitorable formulas›
definition "mmonitorable φ ⟷ safe_formula φ ∧ Formula.future_bounded φ"
definition "mmonitorable_regex b g r ⟷ safe_regex b g r ∧ Regex.pred_regex Formula.future_bounded r"
definition is_simple_eq :: "Formula.trm ⇒ Formula.trm ⇒ bool" where
"is_simple_eq t1 t2 = (Formula.is_Const t1 ∧ (Formula.is_Const t2 ∨ Formula.is_Var t2) ∨
Formula.is_Var t1 ∧ Formula.is_Const t2)"