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

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.