Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/MFOTL_Monitor/ Datei vom 31.4.2026 mit Größe 2 kB

Quelle Examples.thy

Sprache: Isabelle

(*<*)
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
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

Wurzel

Suchen

NIST Cobol Testsuite

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.