Theory Examples

(*<*)
theory Examples
  imports Monitor_Code
begin
(*>*)

section ‹Examples›

abbreviation "TT ≡ MFOTL.Eq (MFOTL.Const ''_'') (MFOTL.Const ''_'')"
abbreviation "Eventually I ψ ≡ MFOTL.Until TT I ψ"

definition "φ⇩e⇩x = MFOTL.And_Not (MFOTL.Pred ''A'' [MFOTL.Var 0])
  (Eventually (interval 1 2) (MFOTL.Exists (MFOTL.Pred ''B'' [MFOTL.Var 1, MFOTL.Var 0])))"

lemma "mmonitorable φ⇩e⇩x" by eval

text ‹Offline monitoring:›

lift_definition π⇩e⇩x :: "string MFOTL.prefix" is
  "[ ({(''A'', [''d'']), (''A'', [''e''])}, 1)
   , ({(''B'', [''d'', ''f''])}, 2)
   , ({(''B'', [''e'', ''f''])}, 5)
  ]"
  by simp

lemma "monitor φ⇩e⇩x π⇩e⇩x = {(0, [Some ''e''])}" by eval

text ‹Online monitoring:›

definition "m1 = mstep ({(''A'', [''d'']), (''A'', [''e''])}, 1) (minit φ⇩e⇩x)"
definition "m2 = mstep ({(''B'', [''d'', ''f''])}, 2) (snd m1)"
definition "m3 = mstep ({(''B'', [''e'', ''f''])}, 5) (snd m2)"

lemma "fst m1 = {}" by eval
lemma "fst m2 = {}" by eval
lemma "fst m3 = {(0, [Some ''e''])}" by eval


text ‹Operation of the monitor:›

lemma "minit φ⇩e⇩x = ⦇
  mstate_i = 0,
  mstate_m =
    MAnd (MPred ''A'' [MFOTL.Var 0]) False
     (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
       ([], []) [] [])
     ([], []),
  mstate_n = 1⦈"
  by eval

lemma "mstate_m (snd m1) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
    ([], []) [] [(1, {[None]}, {})])
  ([{[Some ''d''], [Some ''e'']}], [])"
  by eval

lemma "mstate_m (snd m2) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
   ([], []) [] [(1, {[None]}, {[Some ''d'']}), (2, {[None]}, {})])
  ([{[Some ''d''], [Some ''e'']}, {}], [])"
  by eval

lemma "mstate_m (snd m3) = MAnd (MPred ''A'' [MFOTL.Var 0]) False
  (MUntil True (MRel {[None]}) (interval 1 2) (MExists (MPred ''B'' [MFOTL.Var 1, MFOTL.Var 0]))
    ([], []) [] [(5, {[None]}, {})])
  ([{}], [])"
  by eval

(*<*)
end
(*>*)