(*<*)
theory Examples
imports Monitor Checker_Code
begin
(*>*)

section ‹Examples›

definition monitor :: "(('n :: linorder × 'd :: {default, linorder} list) set × nat) list → ('n, 'd) formula → ('n, 'd) expl list" where
  "monitor π φ = map (λi. eval (trace_of_list π) (λp q. size p ≤ size q) (sorted_list_of_set (fv φ)) i φ) [0 ..< length π]"
definition check :: "(('n :: linorder × 'd :: {default, linorder} list) set × nat) list → ('n, 'd) formula → bool" where
  "check π φ = list_all (check_all (trace_of_list π) φ) (monitor π φ)"

subsection ‹Infinite Domain›

definition prefix :: "((string × string list) set × nat) list" where 
  "prefix =
     [({(''mgr_S'', [''Mallory'', ''Alice'']),
        (''mgr_S'', [''Merlin'', ''Bob'']),
        (''mgr_S'', [''Merlin'', ''Charlie''])}, 1307532861::nat),
      ({(''approve'', [''Mallory'', ''152''])}, 1307532861),
      ({(''approve'', [''Merlin'', ''163'']),
        (''publish'', [''Alice'', ''160'']),
        (''mgr_F'', [''Merlin'', ''Charlie''])}, 1307955600),
      ({(''approve'', [''Merlin'', ''187'']),
        (''publish'', [''Bob'', ''163'']),
        (''publish'', [''Alice'', ''163'']),
        (''publish'', [''Charlie'', ''163'']),
        (''publish'', [''Charlie'', ''152''])}, 1308477599)]"

definition phi :: "(string, string) Formula.formula" where
  "phi = Formula.Imp (Formula.Pred ''publish'' [Formula.Var ''a'', Formula.Var ''f''])
    (Formula.Once (init 604800) (Formula.Exists ''m'' (Formula.Since
      (Formula.Neg (Formula.Pred ''mgr_F'' [Formula.Var ''m'', Formula.Var ''a''])) all
      (Formula.And (Formula.Pred ''mgr_S'' [Formula.Var ''m'', Formula.Var ''a''])
                 (Formula.Pred ''approve'' [Formula.Var ''m'', Formula.Var ''f''])))))"

value "monitor prefix phi"
lemma "check prefix phi"
  by eval

subsection ‹Finite Domain›

datatype Domain = Mallory | Merlin | Martin | Alice | Bob | Charlie | David | Default | R42 | R152 | R160 | R163 | R187

definition ord :: "Domain → nat" where
  "ord d = (case d of
     Mallory → 0
   | Merlin → 1
   | Martin → 2
   | Alice → 3
   | Bob → 4
   | Charlie → 5
   | David → 6
   | Default → 7
   | R42 → 8
   | R152 → 9
   | R160 → 10
   | R163 → 11
   | R187 → 12)"

instantiation Domain :: default begin
definition "default_Domain = Default"
instance ..
end
instantiation Domain :: universe begin
definition "universe_Domain = Some [Mallory, Merlin, Martin, Alice, Bob, Charlie, David, Default, R42, R152, R160, R163, R187]"
instance by standard (auto simp: universe_Domain_def intro: Domain.exhaust)
end
instantiation Domain :: linorder begin
definition "less_eq_Domain d d' = (ord d ≤ ord d')"
definition "less_Domain d d' = (ord d < ord d')"
instance by standard (auto simp: less_eq_Domain_def less_Domain_def ord_def split: Domain.splits)
end

definition fprefix :: "((string × Domain list) set × nat) list" where 
  "fprefix =
     [({(''mgr_S'', [Mallory, Alice]),
        (''mgr_S'', [Merlin, Bob]),
        (''mgr_S'', [Merlin, Charlie])}, 1307532861::nat),
      ({(''approve'', [Mallory, R152])}, 1307532861),
      ({(''approve'', [Merlin, R163]),
        (''publish'', [Alice, R160]),
        (''mgr_F'', [Merlin, Charlie])}, 1307955600),
      ({(''approve'', [Merlin, R187]),
        (''publish'', [Bob, R163]),
        (''publish'', [Alice, R163]),
        (''publish'', [Charlie, R163]),
        (''publish'', [Charlie, R152])}, 1308477599)]"

definition fphi :: "(string, Domain) Formula.formula" where
  "fphi = Formula.Imp (Formula.Pred ''publish'' [Formula.Var ''a'', Formula.Var ''f''])
    (Formula.Once (init 604800) (Formula.Exists ''m'' (Formula.Since
      (Formula.Neg (Formula.Pred ''mgr_F'' [Formula.Var ''m'', Formula.Var ''a''])) all
      (Formula.And (Formula.Pred ''mgr_S'' [Formula.Var ''m'', Formula.Var ''a''])
                 (Formula.Pred ''approve'' [Formula.Var ''m'', Formula.Var ''f''])))))"

value "monitor fprefix fphi"
lemma "check fprefix fphi"
  by eval

(*<*)
end
(*>*)