Theory Simple_Network_Language_Export_Code

section ‹Assembling the Model Checker and Generating Code›

text ‹
We assemble the model checker:

▪ A parser is added to parse JSON files
▪ The resulting JSON data is validated and converted to the simple networks language
▪ The verified model checker is run on this input, and the output is printed
▪ The verified part includes a ``renaming'' step to normalize identifiers in the input

Then the code is exported:

▪ We add some logging utilities (via code printings)
▪ Code generation is setup
▪ We export this to SML via reflection
▪ And test it on a few small examples
›

theory Simple_Network_Language_Export_Code
  imports
    Munta_Model_Checker.JSON_Parsing
    Munta_Model_Checker.Simple_Network_Language_Renaming
    Munta_Model_Checker.Simple_Network_Language_Deadlock_Checking
    Shortest_SCC_Paths
    Munta_Base.Error_List_Monad
begin

datatype result =
  Renaming_Failed | Preconds_Unsat | Sat | Unsat

abbreviation "renum_automaton ≡ Simple_Network_Rename_Defs.renum_automaton"

locale Simple_Network_Rename_Formula_String_Defs =
  Simple_Network_Rename_Defs_int where automata = automata for automata ::
    "(nat list × nat list ×
     (String.literal act, nat, String.literal, int, String.literal, int) transition list
      × (nat × (String.literal, int) cconstraint) list) list"
begin

definition check_renaming where "check_renaming urge Φ L⇩0 s⇩0 ≡ combine [
    assert (∀i<n_ps. ∀x∈loc_set. ∀y∈loc_set. renum_states i x = renum_states i y ⟶ x = y)
      STR ''Location renamings are injective'',
    assert (inj_on renum_clocks (insert urge clk_set'))
      STR ''Clock renaming is injective'',
    assert (inj_on renum_vars var_set)
      STR ''Variable renaming is injective'',
    assert (inj_on renum_acts act_set)
      STR ''Action renaming is injective'',
    assert (fst ` set bounds' = var_set)
      STR ''Bound set is exactly the variable set'',
    assert (⋃ ((λg. fst ` set g) ` set (map (snd o snd o snd) automata)) ⊆ loc_set)
      STR ''Invariant locations are contained in the location set'',
    assert (⋃ ((set o fst) ` set automata) ⊆ loc_set)
      STR ''Broadcast locations are containted in the location set'',
    assert ((⋃x∈set automata. set (fst (snd x))) ⊆ loc_set)
      STR ''Urgent locations are containted in the location set'',
    assert (urge ∉ clk_set')
      STR ''Urge not in clock set'',
    assert (L⇩0 ∈ states)
      STR ''Initial location is in the state set'',
    assert (fst ` set s⇩0 = var_set)
      STR ''Initial state has the correct domain'',
    assert (distinct (map fst s⇩0))
      STR ''Initial state is unambiguous'',
    assert (set2_formula Φ ⊆ loc_set)
      STR ''Formula locations are contained in the location set'',
    assert (locs_of_formula Φ ⊆ {0..<n_ps})
      STR ''Formula automata are contained in the automata set'',
    assert (vars_of_formula Φ ⊆ var_set)
      STR ''Variables of the formula are contained in the variable set''
  ]
"

end (* Simple_Network_Rename_Formula_String_Defs *)

locale Simple_Network_Rename_Formula_String =
  Simple_Network_Rename_Formula_String_Defs +
  fixes urge :: String.literal
  fixes Φ :: "(nat, nat, String.literal, int) formula"
    and s⇩0 :: "(String.literal × int) list"
    and L⇩0 :: "nat list"
  assumes renum_states_inj:
    "∀i<n_ps. ∀x∈loc_set. ∀y∈loc_set. renum_states i x = renum_states i y ⟶ x = y"
  and renum_clocks_inj: "inj_on renum_clocks (insert urge clk_set')"
  and renum_vars_inj:   "inj_on renum_vars var_set"
  and renum_acts_inj:   "inj_on renum_acts act_set"
  and bounds'_var_set:  "fst ` set bounds' = var_set"
  and loc_set_invs: "⋃ ((λg. fst ` set g) ` set (map (snd o snd o snd) automata)) ⊆ loc_set"
  and loc_set_broadcast: "⋃ ((set o fst) ` set automata) ⊆ loc_set"
  and loc_set_urgent: "⋃ ((set o (fst o snd)) ` set automata) ⊆ loc_set"
  and urge_not_in_clk_set: "urge ∉ clk_set'"
  assumes L⇩0_states: "L⇩0 ∈ states"
      and s⇩0_dom: "fst ` set s⇩0 = var_set" and s⇩0_distinct: "distinct (map fst s⇩0)"
  assumes formula_dom:
    "set2_formula Φ ⊆ loc_set"
    "locs_of_formula Φ ⊆ {0..<n_ps}"
    "vars_of_formula Φ ⊆ var_set"
begin

interpretation Simple_Network_Rename_Formula
  by (standard;
      rule renum_states_inj renum_clocks_inj renum_vars_inj bounds'_var_set renum_acts_inj
        loc_set_invs loc_set_broadcast loc_set_urgent urge_not_in_clk_set
        infinite_literal infinite_UNIV_nat L⇩0_states s⇩0_dom s⇩0_distinct formula_dom
     )+ ― ‹slow: 40s›

lemmas Simple_Network_Rename_intro = Simple_Network_Rename_Formula_axioms

end

lemma is_result_assert_iff:
  "is_result (assert b m) ⟷ b"
  unfolding assert_def by auto

lemma is_result_combine_Cons_iff:
  "is_result (combine (x # xs)) ⟷ is_result x ∧ is_result (combine xs)"
  by (cases x; cases "combine xs") auto

lemma is_result_combine_iff:
  "is_result (a <|> b) ⟷ is_result a ∧ is_result b"
  by (cases a; cases b) (auto simp: combine2_def)

context Simple_Network_Rename_Formula_String_Defs
begin

lemma check_renaming:
  "Simple_Network_Rename_Formula_String
    broadcast bounds'
    renum_acts renum_vars renum_clocks renum_states
    automata urge Φ s⇩0 L⇩0 ⟷
  is_result (check_renaming urge Φ L⇩0 s⇩0)
  "
  unfolding check_renaming_def Simple_Network_Rename_Formula_String_def
  by (simp add: is_result_combine_Cons_iff is_result_assert_iff del: combine.simps(2))

end

context Simple_Network_Impl_nat_defs
begin

definition check_precond1 where
"check_precond1 =
  combine [
    assert (m > 0)
      (STR ''At least one clock''),
    assert (0 < length automata)
      (STR ''At least one automaton''),
    assert (∀i<n_ps. let (_, _, trans, _) = (automata ! i) in ∀ (l, _, _, _, _, _, l') ∈ set trans.
      l < num_states i ∧ l' < num_states i)
      (STR ''Number of states is correct (transitions)''),
    assert (∀i < n_ps. let (_, _, _, inv) = (automata ! i) in ∀ (x, _) ∈ set inv. x < num_states i)
      (STR ''Number of states is correct (invariants)''),
    assert (∀(_, _, trans, _) ∈ set automata. ∀(_, _, _, _, f, _, _) ∈ set trans.
      ∀(x, upd) ∈ set f. x < n_vs ∧ (∀i ∈ vars_of_exp upd. i < n_vs))
      (STR ''Variable set bounded (updates)''),
    assert (∀(_, _, trans, _) ∈ set automata. ∀(_, b, _, _, _, _, _) ∈ set trans.
      ∀i ∈ vars_of_bexp b. i < n_vs)
      (STR ''Variable set bounded (guards)''),
    assert (∀ i < n_vs. fst (bounds' ! i) = i)
      (STR ''Bounds first index''),
    assert (∀a ∈ set broadcast. a < num_actions)
      (STR ''Broadcast actions bounded''),
    assert (∀(_, _, trans, _) ∈ set automata. ∀(_, _, _, a, _, _, _) ∈ set trans.
        pred_act (λa. a < num_actions) a)
      (STR ''Actions bounded (transitions)''),
    assert (∀(_, _, trans, _) ∈ set automata. ∀(_, _, g, _, _, r, _) ∈ set trans.
      (∀c ∈ set r. 0 < c ∧ c ≤ m) ∧
      (∀ (c, x) ∈ collect_clock_pairs g. 0 < c ∧ c ≤ m ∧ x ∈ ℕ))
      (STR ''Clock set bounded (transitions)''),
    assert (∀(_, _, _, inv) ∈ set automata. ∀(l, g) ∈ set inv.
      (∀ (c, x) ∈ collect_clock_pairs g. 0 < c ∧ c ≤ m ∧ x ∈ ℕ))
      (STR ''Clock set bounded (invariants)''),
    assert (∀(_, _, trans, _) ∈ set automata. ∀(_, _, g, a, _, _, _) ∈ set trans.
      case a of In a ⇒ a ∈ set broadcast ⟶ g = [] | _ ⇒ True)
      (STR ''Broadcast receivers are unguarded''),
    assert (∀(_, U, _, _)∈set automata. U = [])
      STR ''Urgency was removed''
  ]
"

lemma check_precond1:
  "is_result check_precond1
  ⟷ Simple_Network_Impl_nat_urge broadcast bounds' automata m num_states num_actions"
  unfolding check_precond1_def Simple_Network_Impl_nat_def Simple_Network_Impl_nat_urge_def
    Simple_Network_Impl_nat_urge_axioms_def
  by (simp add: is_result_combine_Cons_iff is_result_assert_iff del: combine.simps(2))

context
  fixes k :: "nat list list list"
    and L⇩0 :: "nat list"
    and s⇩0 :: "(nat × int) list"
    and formula :: "(nat, nat, nat, int) formula"
begin

definition check_precond2 where
  "check_precond2 ≡
  combine [
    assert (∀i < n_ps. ∀(l, g) ∈ set ((snd o snd o snd) (automata ! i)).
      ∀(x, m) ∈ collect_clock_pairs g. m ≤ int (k ! i ! l ! x))
      (STR ''Ceiling invariants''),
    assert (∀i < n_ps. ∀(l, _, g, _) ∈ set ((fst o snd o snd) (automata ! i)).
      (∀(x, m) ∈ collect_clock_pairs g. m ≤ int (k ! i ! l ! x)))
      (STR ''Ceiling transitions''),
    assert (∀i < n_ps. ∀ (l, b, g, a, upd, r, l') ∈ set ((fst o snd o snd) (automata ! i)).
       ∀c ∈ {0..<m+1} - set r. k ! i ! l' ! c ≤ k ! i ! l ! c)
      (STR ''Ceiling resets''),
    assert (length k = n_ps)
      (STR ''Ceiling length''),
    assert (∀ i < n_ps. length (k ! i) = num_states i)
      (STR ''Ceiling length automata)''),
    assert (∀ xs ∈ set k. ∀ xxs ∈ set xs. length xxs = m + 1)
      (STR ''Ceiling length clocks''),
    assert (∀i < n_ps. ∀l < num_states i. k ! i ! l ! 0 = 0)
      (STR ''Ceiling zero clock''),
    assert (∀(_, _, _, inv) ∈ set automata. distinct (map fst inv))
      (STR ''Unambiguous invariants''),
    assert (bounded bounds (map_of s⇩0))
      (STR ''Initial state bounded''),
    assert (length L⇩0 = n_ps)
      (STR ''Length of initial state''),
    assert (∀i < n_ps. L⇩0 ! i ∈ fst ` set ((fst o snd o snd) (automata ! i)))
      (STR ''Initial state has outgoing transitions''),
    assert (vars_of_formula formula ⊆ {0..<n_vs})
      (STR ''Variable set of formula'')
]"

lemma check_precond2:
  "is_result check_precond2 ⟷
  Simple_Network_Impl_nat_ceiling_start_state_axioms broadcast bounds' automata m num_states
      k L⇩0 s⇩0 formula"
  unfolding check_precond2_def Simple_Network_Impl_nat_ceiling_start_state_axioms_def
  by (simp add: is_result_combine_Cons_iff is_result_assert_iff del: combine.simps(2))

end

definition
  "check_precond k L⇩0 s⇩0 formula ≡ check_precond1 <|> check_precond2 k L⇩0 s⇩0 formula"

lemma check_precond:
  "Simple_Network_Impl_nat_ceiling_start_state broadcast bounds' automata m num_states
      num_actions k L⇩0 s⇩0 formula ⟷ is_result (check_precond k L⇩0 s⇩0 formula)"
  unfolding check_precond_def is_result_combine_iff check_precond1 check_precond2
    Simple_Network_Impl_nat_ceiling_start_state_def
  ..

end

derive "show" acconstraint act sexp formula

fun shows_exp and shows_bexp where
  "shows_exp (const c) = show c" |
  "shows_exp (var v) = show v" |
  "shows_exp (if_then_else b e1 e2) =
    shows_bexp b @ '' ? '' @ shows_exp e1 @ '' : '' @ shows_exp e2" |
  "shows_exp (binop _ e1 e2) = ''binop '' @ shows_exp e1 @ '' '' @ shows_exp e2" |
  "shows_exp (unop _ e) = ''unop '' @ shows_exp e" |
  "shows_bexp (bexp.lt a b) = shows_exp a @ '' < '' @ shows_exp b" |
  "shows_bexp (bexp.le a b) = shows_exp a @ '' <= '' @ shows_exp b" |
  "shows_bexp (bexp.eq a b) = shows_exp a @ '' = '' @ shows_exp b" |
  "shows_bexp (bexp.ge a b) = shows_exp a @ '' >= '' @ shows_exp b" |
  "shows_bexp (bexp.gt a b) = shows_exp a @ '' > '' @ shows_exp b" |
  "shows_bexp bexp.true = ''true''" |
  "shows_bexp (bexp.not b) = ''! '' @ shows_bexp b" |
  "shows_bexp (bexp.and a b) = shows_bexp a @ '' && '' @ shows_bexp b" |
  "shows_bexp (bexp.or a b) = shows_bexp a @ '' || '' @ shows_bexp b" |
  "shows_bexp (bexp.imply a b) = shows_bexp a @ '' -> '' @ shows_bexp b"

instantiation bexp :: ("show", "show") "show"
begin

definition "shows_prec p (e :: (_, _) bexp) rest = shows_bexp e @ rest" for p

definition "shows_list (es) s =
  map shows_bexp es |> intersperse '', '' |> (λxs. ''['' @ concat xs @ '']'' @ s)"
instance
  by standard (simp_all add: shows_prec_bexp_def shows_list_bexp_def show_law_simps)

end

instantiation exp :: ("show", "show") "show"
begin

definition "shows_prec p (e :: (_, _) exp) rest = shows_exp e @ rest" for p

definition "shows_list (es) s =
  map shows_exp es |> intersperse '', '' |> (λxs. ''['' @ concat xs @ '']'' @ s)"
instance
  by standard (simp_all add: shows_prec_exp_def shows_list_exp_def show_law_simps)

end


definition
  "pad m s = replicate m CHR '' '' @ s"

definition "shows_rat r ≡ case r of fract.Rat s f b ⇒
  (if s then '''' else ''-'') @ show f @ (if b ≠ 0 then ''.'' @ show b else '''')"

fun shows_json :: "nat ⇒ JSON ⇒ string" where
  "shows_json n (Nat m) = show m |> pad n"
| "shows_json n (Rat r) = shows_rat r |> pad n"
| "shows_json n (JSON.Int r) = show r |> pad n"
| "shows_json n (Boolean b) = (if b then ''true'' else ''false'') |> pad n"
| "shows_json n Null = ''null'' |> pad n"
| "shows_json n (String s) = pad n (''\"'' @ s @ ''\"'')"
| "shows_json n (JSON.Array xs) = (
  if xs = Nil then
    pad n ''[]''
  else
    pad n ''[⏎''
    @ concat (map (shows_json (n + 2)) xs |> intersperse '',⏎'')
    @ ''⏎''
    @ pad n '']''
  )"
| "shows_json n (JSON.Object xs) = (
  if xs = Nil then
    pad n ''{}''
  else
    pad n ''{⏎''
    @ concat (
      map (λ(k, v). pad (n + 2) (''\"'' @ k @ ''\"'') @ '':⏎'' @ shows_json (n + 4) v) xs
      |> intersperse '',⏎''
    )
    @ ''⏎''
    @ pad n ''}''
  )"

instantiation JSON :: "show"
begin

definition "shows_prec p (x :: JSON) rest = shows_json 0 x @ rest" for p

definition "shows_list jsons s =
  map (shows_json 0) jsons |> intersperse '', '' |> (λxs. ''['' @ concat xs @ '']'' @ s)"
instance
  by standard (simp_all add: shows_prec_JSON_def shows_list_JSON_def show_law_simps)

end


definition rename_network where
  "rename_network broadcast bounds' automata renum_acts renum_vars renum_clocks renum_states ≡
  let
    automata = map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states) automata;
    broadcast = map renum_acts broadcast;
    bounds' = map (λ(a,b,c). (renum_vars a, b, c)) bounds'
  in
    (broadcast, automata, bounds')
"

definition
  "show_clock inv_renum_clocks = show o inv_renum_clocks"

definition
  "show_locs inv_renum_states = show o map_index inv_renum_states"

definition
  "show_vars inv_renum_vars = show o map_index (λi v. show (inv_renum_vars i) @ ''='' @ show v)"

definition
  "show_state inv_renum_states inv_renum_vars ≡ λ(L, vs).
  let L = show_locs inv_renum_states L; vs = show_vars inv_renum_vars vs in
  ''<'' @ L @ ''>, <'' @ vs @ ''>''"

definition do_rename_mc where
  "do_rename_mc f dc broadcast bounds' automata k urge L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks
≡
let
   _ = println (STR ''Checking renaming'');
   formula = (if dc then formula.EX (not sexp.true) else formula);
   renaming_valid = Simple_Network_Rename_Formula_String_Defs.check_renaming
      broadcast bounds' renum_acts renum_vars renum_clocks renum_states automata urge formula L⇩0 s⇩0;
   _ = println (STR ''Renaming network'');
   (broadcast, automata, bounds') = rename_network
      broadcast bounds' (map (conv_urge urge) automata)
      renum_acts renum_vars renum_clocks renum_states;
   _ = trace_level 4 (λ_. return (STR ''Automata after renaming''));
   _ = map (λa. show a |> String.implode |> (λs. trace_level 4 (λ_. return s))) automata;
   _ = println (STR ''Renaming formula'');
   formula =
    (if dc then formula.EX (not sexp.true) else map_formula renum_states renum_vars id formula);
    _ = println (STR ''Renaming state'');
   L⇩0 = map_index renum_states L⇩0;
   s⇩0 = map (λ(x, v). (renum_vars x, v)) s⇩0;
   show_clock = show o inv_renum_clocks;
   show_state = show_state inv_renum_states inv_renum_vars
in
  if is_result renaming_valid then do {
    let _ = println (STR ''Checking preconditions'');
    let r = Simple_Network_Impl_nat_defs.check_precond
      broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
    let _ = (case r of Result _ ⇒ ()
      | Error es ⇒
        let
          _ = println STR '''';
          _ = println STR ''The following pre-conditions were not satisified:''
        in
          let _ = map println es in println STR '''');
    let _ = println (STR ''Running precond_mc'');
    let r = f show_clock show_state
        broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
    Some r
  }
  else do {
    let _ = println (STR ''The following conditions on the renaming were not satisfied:'');
    let _ = the_errors renaming_valid |> map println;
    None}
"

definition rename_mc where
  "rename_mc dc broadcast bounds' automata k urge L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks
≡
do {
  let r = do_rename_mc (if dc then precond_dc else precond_mc)
    dc broadcast bounds' automata k urge L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks;
  case r of Some r ⇒ do {
    r ← r;
    case r of
      None ⇒ return Preconds_Unsat
    | Some False ⇒ return Unsat
    | Some True ⇒ return Sat
  }
  | None ⇒ return Renaming_Failed
}
"

(*
definition rename_mc where
  "rename_mc dc broadcast bounds' automata k L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks
≡
let
   _ = println (STR ''Checking renaming'');
  formula = (if dc then formula.EX (not sexp.true) else formula);
   renaming_valid = Simple_Network_Rename_Formula_String_Defs.check_renaming
      broadcast bounds' renum_vars renum_clocks renum_states automata formula L⇩0 s⇩0;
   _ = println (STR ''Renaming network'');
   (broadcast, automata, bounds') = rename_network
      broadcast bounds' automata renum_acts renum_vars renum_clocks renum_states;
   _ = println (STR ''Automata after renaming'');
   _ = map (λa. show a |> String.implode |> println) automata;
   _ = println (STR ''Renaming formula'');
   formula =
    (if dc then formula.EX (not sexp.true) else map_formula renum_states renum_vars id formula);
    _ = println (STR ''Renaming state'');
   L⇩0 = map_index renum_states L⇩0;
   s⇩0 = map (λ(x, v). (renum_vars x, v)) s⇩0;
   show_clock = show o inv_renum_clocks;
   show_state = show_state inv_renum_states inv_renum_vars
in
  if is_result renaming_valid then do {
    let _ = println (STR ''Checking preconditions'');
    let r = Simple_Network_Impl_nat_defs.check_precond
      broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula;
    let _ = (case r of Result _ ⇒ [()]
      | Error es ⇒ let _ = println (STR ''The following pre-conditions were not satisified'') in
          map println es);
    let _ = println (STR ''Running precond_mc'');
    r ← (if dc
      then precond_dc show_clock show_state
        broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
      else precond_mc show_clock show_state
        broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula);
    case r of
      None ⇒ return Preconds_Unsat
    | Some False ⇒ return Unsat
    | Some True ⇒ return Sat
  } 
  else do {
    let _ = println (STR ''The following conditions on the renaming were not satisfied:'');
    let _ = the_errors renaming_valid |> map println;
    return Renaming_Failed}
"
*)

theorem model_check_rename:
  "<emp> rename_mc False broadcast bounds automata k urge L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks
    <λ Sat ⇒ ↑(
        (¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0) ⟶
          N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula
        ))
     | Unsat ⇒ ↑(
        (¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_ . 0) ⟶
          ¬ N broadcast automata bounds,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula
        ))
     | Renaming_Failed ⇒ ↑(¬ Simple_Network_Rename_Formula
        broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata formula)
     | Preconds_Unsat ⇒ ↑(¬ Simple_Network_Impl_nat_ceiling_start_state
        (map renum_acts broadcast)
        (map (λ(a,p). (renum_vars a, p)) bounds)
        (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
          (map (conv_urge urge) automata))
        m num_states num_actions k
        (map_index renum_states L⇩0) (map (λ(x, v). (renum_vars x, v)) s⇩0)
        (map_formula renum_states renum_vars id formula))
    >⇩t"
proof -
  have *: "
    Simple_Network_Rename_Formula_String
        broadcast bounds renum_acts renum_vars renum_clocks renum_states automata urge formula s⇩0 L⇩0
  = Simple_Network_Rename_Formula
        broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata formula
  "
    unfolding
      Simple_Network_Rename_Formula_String_def Simple_Network_Rename_Formula_def
      Simple_Network_Rename_Start_def Simple_Network_Rename_Start_axioms_def
      Simple_Network_Rename_def Simple_Network_Rename_Formula_axioms_def
    using infinite_literal by auto
  define A where "A ≡ N broadcast automata bounds"
  define check where "check ≡ A,(L⇩0, map_of s⇩0, λ_ . 0) ⊨ formula"
  define A' where "A' ≡ N
    (map renum_acts broadcast)
    (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
      (map (conv_urge urge) automata))
    (map (λ(a,p). (renum_vars a, p)) bounds)"
  define check' where "check' ≡
    A',(map_index renum_states L⇩0, map_of (map (λ(x, v). (renum_vars x, v)) s⇩0), λ_ . 0) ⊨
    map_formula renum_states renum_vars id formula"
  define preconds_sat where "preconds_sat ≡
    Simple_Network_Impl_nat_ceiling_start_state
      (map renum_acts broadcast)
      (map (λ(a,p). (renum_vars a, p)) bounds)
      (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
        (map (conv_urge urge) automata))
      m num_states num_actions k
      (map_index renum_states L⇩0) (map (λ(x, v). (renum_vars x, v)) s⇩0)
      (map_formula renum_states renum_vars id formula)"
  define renaming_valid where "renaming_valid ≡
    Simple_Network_Rename_Formula
      broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata formula
  "
  have [simp]: "check ⟷ check'" 
    if renaming_valid
    using that unfolding check_def check'_def A_def A'_def renaming_valid_def
    by (rule Simple_Network_Rename_Formula.models_iff'[symmetric])
  have test[symmetric, simp]:
    "Simple_Network_Language_Model_Checking.has_deadlock A (L⇩0, map_of s⇩0, λ_. 0)
  ⟷Simple_Network_Language_Model_Checking.has_deadlock A'
     (map_index renum_states L⇩0, map_of (map (λ(x, y). (renum_vars x, y)) s⇩0), λ_. 0)
  " if renaming_valid
    using that unfolding check_def check'_def A_def A'_def renaming_valid_def
    unfolding Simple_Network_Rename_Formula_def
    by (elim conjE) (rule Simple_Network_Rename_Start.has_deadlock_iff'[symmetric])
  note [sep_heap_rules] =
    model_check[
    of _ _
    "map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
    "map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
      (map (conv_urge urge) automata)"
    m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0"
    "map_formula renum_states renum_vars id formula",
    folded A'_def preconds_sat_def renaming_valid_def, folded check'_def, simplified
    ]
  show ?thesis
    unfolding rename_mc_def do_rename_mc_def rename_network_def
    unfolding if_False
    unfolding Simple_Network_Rename_Formula_String_Defs.check_renaming[symmetric] * Let_def
    unfolding
      A_def[symmetric] check_def[symmetric]
      preconds_sat_def[symmetric] renaming_valid_def[symmetric]
    by (sep_auto simp: model_checker.refine[symmetric] split: bool.splits)
qed

theorem deadlock_check_rename:
  "<emp> rename_mc True broadcast bounds automata k urge L⇩0 s⇩0 formula
    m num_states num_actions renum_acts renum_vars renum_clocks renum_states
    inv_renum_states inv_renum_vars inv_renum_clocks
    <λ Sat   ⇒ ↑(  has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_.  0))
     | Unsat ⇒ ↑(¬ has_deadlock (N broadcast automata bounds) (L⇩0, map_of s⇩0, λ_. 0))
     | Renaming_Failed ⇒ ↑(¬ Simple_Network_Rename_Formula
        broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata
        (formula.EX (not sexp.true)))
     | Preconds_Unsat ⇒ ↑(¬ Simple_Network_Impl_nat_ceiling_start_state
        (map renum_acts broadcast)
        (map (λ(a,p). (renum_vars a, p)) bounds)
        (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
          (map (conv_urge urge) automata))
        m num_states num_actions k
        (map_index renum_states L⇩0) (map (λ(x, v). (renum_vars x, v)) s⇩0)
        (formula.EX (not sexp.true)))
    >⇩t"
proof -
  have *: "
    Simple_Network_Rename_Formula_String
        broadcast bounds renum_acts renum_vars renum_clocks renum_states automata urge
        (formula.EX (not sexp.true)) s⇩0 L⇩0
  = Simple_Network_Rename_Formula
        broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata
        (formula.EX (not sexp.true))
  "
    unfolding
      Simple_Network_Rename_Formula_String_def Simple_Network_Rename_Formula_def
      Simple_Network_Rename_Start_def Simple_Network_Rename_Start_axioms_def
      Simple_Network_Rename_def Simple_Network_Rename_Formula_axioms_def
    using infinite_literal by auto
  define A where "A ≡ N broadcast automata bounds"
  define A' where "A' ≡ N
    (map renum_acts broadcast)
    (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
      (map (conv_urge urge) automata))
    (map (λ(a,p). (renum_vars a, p)) bounds)"
  define preconds_sat where "preconds_sat ≡
    Simple_Network_Impl_nat_ceiling_start_state
      (map renum_acts broadcast)
      (map (λ(a,p). (renum_vars a, p)) bounds)
      (map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
        (map (conv_urge urge) automata))
      m num_states num_actions k
      (map_index renum_states L⇩0) (map (λ(x, v). (renum_vars x, v)) s⇩0)
      (formula.EX (not sexp.true))"
  define renaming_valid where "renaming_valid ≡
    Simple_Network_Rename_Formula
      broadcast bounds renum_acts renum_vars renum_clocks renum_states urge s⇩0 L⇩0 automata
      (formula.EX (not sexp.true))"
 have test[symmetric, simp]:
    "Simple_Network_Language_Model_Checking.has_deadlock A (L⇩0, map_of s⇩0, λ_. 0)
  ⟷Simple_Network_Language_Model_Checking.has_deadlock A'
     (map_index renum_states L⇩0, map_of (map (λ(x, y). (renum_vars x, y)) s⇩0), λ_. 0)
  " if renaming_valid
    using that unfolding check_def A_def A'_def renaming_valid_def Simple_Network_Rename_Formula_def
    by (elim conjE) (rule Simple_Network_Rename_Start.has_deadlock_iff'[symmetric])
  note [sep_heap_rules] =
    deadlock_check[
    of _ _
    "map renum_acts broadcast" "map (λ(a,p). (renum_vars a, p)) bounds"
    "map_index (renum_automaton renum_acts renum_vars renum_clocks renum_states)
      (map (conv_urge urge) automata)"
    m num_states num_actions k "map_index renum_states L⇩0" "map (λ(x, v). (renum_vars x, v)) s⇩0",
    folded preconds_sat_def A'_def renaming_valid_def,
    simplified
    ]
  show ?thesis
    unfolding rename_mc_def do_rename_mc_def  rename_network_def
    unfolding if_True
    unfolding Simple_Network_Rename_Formula_String_Defs.check_renaming[symmetric] * Let_def
    unfolding A_def[symmetric] preconds_sat_def[symmetric] renaming_valid_def[symmetric]
    by (sep_auto simp: deadlock_checker.refine[symmetric] split: bool.splits)
qed


paragraph ‹Code Setup for the Model Checker›

lemmas [code] =
  reachability_checker_def
  Alw_ev_checker_def
  leadsto_checker_def
  model_checker_def[unfolded PR_CONST_def]

lemmas [code] =
  Prod_TA_Defs.n_ps_def
  Simple_Network_Impl_Defs.n_vs_def
  automaton_of_def
  Simple_Network_Impl_nat_defs.pairs_by_action_impl_def
  Simple_Network_Impl_nat_defs.all_actions_from_vec_def
  Simple_Network_Impl_nat_defs.all_actions_by_state_def
  Simple_Network_Impl_nat_defs.compute_upds_impl_def
  Simple_Network_Impl_nat_defs.actions_by_state_def
  Simple_Network_Impl_nat_defs.check_boundedi_def
  Simple_Network_Impl_nat_defs.get_committed_def
  Simple_Network_Impl_nat_defs.make_combs_def
  Simple_Network_Impl_nat_defs.trans_map_def
  Simple_Network_Impl_nat_defs.actions_by_state'_def
  Simple_Network_Impl_nat_defs.bounds_map_def
  Simple_Network_Impl_nat_defs.bin_actions_def
  mk_updsi_def

lemma (in Simple_Network_Impl_nat_defs) bounded_s⇩0_iff:
  "bounded bounds (map_of s⇩0) ⟷ bounded (map_of bounds') (map_of s⇩0)"
  unfolding bounds_def snd_conv ..

lemma int_Nat_range_iff:
  "(n :: int) ∈ ℕ ⟷ n ≥ 0" for n
  using zero_le_imp_eq_int unfolding Nats_def by auto

lemmas [code] =
  Simple_Network_Impl_nat_ceiling_start_state_def
  Simple_Network_Impl_nat_ceiling_start_state_axioms_def[
    unfolded Simple_Network_Impl_nat_defs.bounded_s⇩0_iff]
  Simple_Network_Impl_nat_def[unfolded int_Nat_range_iff]
  Simple_Network_Impl_nat_urge_def
  Simple_Network_Impl_nat_urge_axioms_def

lemmas [code_unfold] = bounded_def dom_map_of_conv_image_fst

export_code Simple_Network_Impl_nat_ceiling_start_state_axioms

export_code precond_mc in SML module_name Test

export_code precond_dc checking SML


paragraph ‹Code Setup for Renaming›

lemmas [code] =
  Simple_Network_Rename_Formula_String_def
  Simple_Network_Impl.clk_set'_def
  Simple_Network_Impl.clkp_set'_def

lemmas [code] =
  Simple_Network_Rename_Defs.renum_automaton_def
  Simple_Network_Rename_Defs.renum_cconstraint_def
  Simple_Network_Rename_Defs.map_cconstraint_def
  Simple_Network_Rename_Defs.renum_reset_def
  Simple_Network_Rename_Defs.renum_upd_def
  Simple_Network_Rename_Defs.renum_act_def
  Simple_Network_Rename_Defs.renum_exp_def
  Simple_Network_Rename_Defs.renum_bexp_def
  Simple_Network_Rename_Formula_String_Defs.check_renaming_def
  Simple_Network_Impl_nat_defs.check_precond_def
  Simple_Network_Impl_nat_defs.check_precond1_def[unfolded int_Nat_range_iff]
  Simple_Network_Impl_nat_defs.check_precond2_def[
    unfolded Simple_Network_Impl_nat_defs.bounded_s⇩0_iff]

lemma (in Prod_TA_Defs) states_mem_iff:
  "L ∈ states ⟷ length L = n_ps ∧ (∀ i. i < n_ps ⟶
    (∃ (l, b, g, a, r, u, l') ∈ fst (snd (snd (fst (snd A) ! i))). L ! i = l ∨ L ! i = l'))"
  unfolding states_def trans_def N_def by (auto split: prod.split)

lemmas [code_unfold] =
  Prod_TA_Defs.states_mem_iff
  Simple_Network_Impl.act_set_compute
  Simple_Network_Impl_Defs.var_set_compute
  Simple_Network_Impl_Defs.loc_set_compute
  setcompr_eq_image
  Simple_Network_Impl.length_automata_eq_n_ps[symmetric]

export_code rename_mc in SML module_name Test



paragraph ‹Calculating the Clock Ceiling›

context Simple_Network_Impl_nat_defs
begin

definition "clkp_inv i l ≡
  ⋃g ∈ set (filter (λ(a, b). a = l) (snd (snd (snd (automata ! i))))). collect_clock_pairs (snd g)"

definition "clkp_set'' i l ≡
    clkp_inv i l ∪ (⋃ (l', b, g, _) ∈ set (fst (snd (snd (automata ! i)))).
      if l' = l then collect_clock_pairs g else {})"

definition
  "collect_resets i l = (⋃ (l', b, g, a, f, r, _) ∈ set (fst (snd (snd (automata ! i)))).
    if l' = l then set r else {})"

context
  fixes q c :: nat
begin

  definition "n ≡ num_states q"

  definition "V ≡ λ v. v ≤ n"

  definition "
    bound_g l ≡
      Max ({0} ∪ ⋃ ((λ (x, d). if x = c then {d} else {}) ` clkp_set'' q l))
    "

  definition "
    bound_inv l ≡
      Max ({0} ∪ ⋃ ((λ (x, d). if x = c then {d} else {}) ` clkp_inv q l))
  "

  definition "
    bound l ≡ max (bound_g l) (bound_inv l)
  "

definition "
  resets l ≡
    fold
    (λ (l1, b, g, a, f, r, l') xs. if l1 ≠ l ∨ l' ∈ set xs ∨ c ∈ set r then xs else (l' # xs))
    (fst (snd (snd (automata ! q))))
    []
"

text ‹
  Edges in the direction nodes to single sink.
›
definition "
  E' l ≡ resets l
"

text ‹
  Turning around the edges to obtain a single source shortest paths problem.
›
definition "
  E l ≡ if l = n then [0..<n] else filter (λ l'. l ∈ set (E' l')) [0..<n]
"

text ‹
  Weights already turned around.
›
definition "
  W l l' ≡ if l = n then - bound l' else 0
"

definition G where "
  G ≡ ⦇ gi_V = V, gi_E = E, gi_V0 = [n], … = W ⦈
"

definition "
  local_ceiling_single ≡
  let
    w = calc_shortest_scc_paths G n
  in
    map (λ x. case x of None ⇒ 0 | Some x ⇒ nat(-x)) w
"

end

definition "
  local_ceiling ≡
    rev $
    fold
      (λ q xs.
        (λ x. rev x # xs) $
        fold
          (λ l xs.
            (λ x. (0 # rev x) # xs) $
            fold
              (λ c xs. local_ceiling_single q c ! l # xs)
              [1..<Suc m]
              []
          )
          [0..<n q]
          []
      )
      [0..<n_ps]
      []
"

end


lemmas [code] =
  Simple_Network_Impl_nat_defs.local_ceiling_def
  Simple_Network_Impl_nat_defs.local_ceiling_single_def
  Simple_Network_Impl_nat_defs.n_def
  Simple_Network_Impl_nat_defs.G_def
  Simple_Network_Impl_nat_defs.W_def
  Simple_Network_Impl_nat_defs.V_def
  Simple_Network_Impl_nat_defs.E'_def
  Simple_Network_Impl_nat_defs.E_def
  Simple_Network_Impl_nat_defs.resets_def
  Simple_Network_Impl_nat_defs.bound_def
  Simple_Network_Impl_nat_defs.bound_inv_def
  Simple_Network_Impl_nat_defs.bound_g_def
  Simple_Network_Impl_nat_defs.collect_resets_def
  Simple_Network_Impl_nat_defs.clkp_set''_def
  Simple_Network_Impl_nat_defs.clkp_inv_def

export_code Simple_Network_Impl_nat_defs.local_ceiling checking SML_imp



paragraph ‹Calculating the Renaming›

definition "mem_assoc x = list_ex (λ(y, _). x = y)"

definition "mk_renaming str xs ≡
do {
  mapping ← fold_error
    (λx m.
      if mem_assoc x m then Error [STR ''Duplicate name: '' + str x] else (x,length m) # m |> Result
    ) xs [];
  Result (let
    m = map_of mapping;
    f = (λx.
      case m x of
        None ⇒ let _ = println (STR ''Key error: '' + str x) in undefined
      | Some v ⇒ v);
    m = map_of (map prod.swap mapping);
    f_inv = (λx.
      case m x of
        None ⇒ let _ = println (STR ''Key error: '' + String.implode (show x)) in undefined
      | Some v ⇒ v)
  in (f, f_inv)
  )
}"

definition
  "extend_domain m d n ≡
    let
      (i, xs) = fold
        (λx (i, xs). if x ∈ set d then (i + 1, (x, i + 1) # xs) else (i, xs)) d (n, []);
      m' = map_of xs
    in
      (λx. if x ∈ set d then the (m' x) else m x)"

(* Unused *)
lemma is_result_make_err:
  "is_result (make_err m e) ⟷ False"
  by (cases e) auto

(* Unused *)
lemma is_result_assert_msg_iff:
  "is_result (assert_msg b m r) ⟷ is_result r ∧ b"
  unfolding assert_msg_def by (simp add: is_result_make_err)

context Simple_Network_Impl
begin

definition action_set where
  "action_set ≡
    (⋃(_, _, trans, _) ∈ set automata. ⋃(_, _, _, a, _, _, _) ∈ set trans. set_act a)
    ∪ set broadcast"

definition loc_set' where
  "loc_set' p = (⋃(l, _, _, _, _, _, l')∈set (fst (snd (snd (automata ! p)))). {l, l'})" for p

end


definition
  "concat_str = String.implode o concat o map String.explode"


paragraph ‹Unsafe Glue Code›
definition list_of_set' :: "'a set ⇒ 'a list" where
  "list_of_set' xs = undefined"

definition list_of_set :: "'a set ⇒ 'a list" where
  "list_of_set xs = list_of_set' xs |> remdups"

code_printing
  constant list_of_set' ⇀ (SML) "(fn Set xs => xs) _"
       and              (OCaml) "(fun x -> match x with Set xs -> xs) _"



definition
  "mk_renaming' xs ≡ mk_renaming (String.implode o show) xs"

definition "make_renaming ≡ λ broadcast automata bounds.
  let
    action_set = Simple_Network_Impl.action_set automata broadcast |> list_of_set;
    clk_set = Simple_Network_Impl.clk_set' automata |> list_of_set;
    clk_set = clk_set @ [STR ''_urge''];
    loc_set' = (λi. Simple_Network_Impl.loc_set' automata i |> list_of_set);
    loc_set = Prod_TA_Defs.loc_set
      (set broadcast, map automaton_of automata, map_of bounds);
    loc_set_diff = (λi. loc_set - Simple_Network_Impl.loc_set' automata i |> list_of_set);
    loc_set = list_of_set loc_set;
    var_set = Prod_TA_Defs.var_set
      (set broadcast, map automaton_of automata, map_of bounds) |> list_of_set;
    n_ps = length automata;
    num_actions = length action_set;
    m = length (remdups clk_set);
    num_states_list = map (λi. loc_set' i |> remdups |> length) [0..<n_ps];
    num_states = (λi. num_states_list ! i);
    mk_renaming = mk_renaming (λx. x)
  in do {
    ((renum_acts, _), (renum_clocks, inv_renum_clocks), (renum_vars, inv_renum_vars)) ←
      mk_renaming action_set <|> mk_renaming clk_set <|> mk_renaming var_set;
    let renum_clocks = Suc o renum_clocks;
    let inv_renum_clocks = (λc. if c = 0 then STR ''0'' else inv_renum_clocks (c - 1));
    renum_states_list' ← combine_map (λi. mk_renaming' (loc_set' i)) [0..<n_ps];
    let renum_states_list = map fst renum_states_list';
    let renum_states_list = map_index
      (λi m. extend_domain m (loc_set_diff i) (length (loc_set' i))) renum_states_list;
    let renum_states = (λi. renum_states_list ! i);
    let inv_renum_states = (λi. map snd renum_states_list' ! i);
    assert (fst ` set bounds ⊆ set var_set)
      STR ''State variables are declared but do not appear in model'';
    Result (m, num_states, num_actions, renum_acts, renum_vars, renum_clocks, renum_states,
      inv_renum_states, inv_renum_vars, inv_renum_clocks)
  }"

definition "preproc_mc ≡ λdc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula.
  let _ = println (STR ''Make renaming'') in
  case make_renaming broadcast automata bounds of
    Error e ⇒ return (Error e)
  | Result (m, num_states, num_actions, renum_acts, renum_vars, renum_clocks, renum_states,
      inv_renum_states, inv_renum_vars, inv_renum_clocks) ⇒ do {
    let _ = println (STR ''Renaming'');
    let (broadcast', automata', bounds') = rename_network
      broadcast bounds automata renum_acts renum_vars renum_clocks renum_states;
    let _ = println (STR ''Calculating ceiling'');
    let k = Simple_Network_Impl_nat_defs.local_ceiling broadcast' bounds' automata' m num_states;
    let _ = println (STR ''Running model checker'');
    let inv_renum_states = (λi. ids_to_names i o inv_renum_states i);
    r ← rename_mc dc broadcast bounds automata k STR ''_urge'' L⇩0 s⇩0 formula
      m num_states num_actions renum_acts renum_vars renum_clocks renum_states
      inv_renum_states inv_renum_vars inv_renum_clocks;
    return (Result r)
  }
"

definition
  "err s = Error [s]"

definition
"do_preproc_mc ≡ λdc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula. do {
  r ← preproc_mc dc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula;
  return (case r of
    Error es ⇒
      intersperse (STR ''⏎'') es
      |> concat_str
      |> (λe. STR ''Error during preprocessing:⏎'' + e)
      |> err
  | Result Renaming_Failed ⇒ STR ''Renaming failed'' |> err
  | Result Preconds_Unsat ⇒ STR ''Input invalid'' |> err
  | Result Unsat ⇒
      (if dc then STR ''Model has no deadlock!'' else STR ''Property is not satisfied!'') |> Result
  | Result Sat ⇒
      (if dc then STR ''Model has a deadlock!''  else STR ''Property is satisfied!'') |> Result
  )
}"

lemmas [code] =
  Simple_Network_Impl.action_set_def
  Simple_Network_Impl.loc_set'_def

export_code do_preproc_mc in SML module_name Main

definition parse where
  "parse parser s ≡ case parse_all lx_ws parser s of
    Inl e ⇒ Error [e () ''Parser: '' |> String.implode]
  | Inr r ⇒ Result r"

definition get_nat :: "string ⇒ JSON ⇒ nat Error_List_Monad.result" where
  "get_nat s json ≡ case json of
    Object as ⇒ Error []
  | _ ⇒ Error [STR ''JSON Get: expected object'']
" for json

definition of_object :: "JSON ⇒ (string ⇀ JSON) Error_List_Monad.result" where
  "of_object json ≡ case json of
    Object as ⇒ map_of as |> Result
  | _ ⇒ Error [STR ''json_to_map: expected object'']
" for json

definition get where
  "get m x ≡ case m x of
    None ⇒ Error [STR ''(Get) key not found: '' + String.implode (show x)]
  | Some a ⇒ Result a"

definition
  "get_default def m x ≡ case m x of None ⇒ def | Some a ⇒ a"

definition default where
  "default def x ≡ case x of Result s ⇒ s | Error e ⇒ def"

definition of_array where
  "of_array json ≡ case json of
    JSON.Array s ⇒ Result s
  | _ ⇒ Error [STR ''of_array: expected sequence'']
" for json

definition of_string where
  "of_string json ≡ case json of
    JSON.String s ⇒ Result (String.implode s)
  | _ ⇒ Error [STR ''of_array: expected sequence'']
" for json

definition of_nat where
  "of_nat json ≡ case json of
    JSON.Nat n ⇒ Result n
  | _ ⇒ Error [STR ''of_nat: expected natural number'']
" for json

definition of_int where
  "of_int json ≡ case json of
    JSON.Int n ⇒ Result n
  | _ ⇒ Error [STR ''of_int: expected integral number'']
" for json

definition [consuming]:
  "lx_underscore = exactly ''_'' with (λ_. CHR ''_'')"

definition [consuming]:
  "lx_hyphen = exactly ''-'' with (λ_. CHR ''-'')"

definition [consuming]:
  "ta_var_ident ≡
    (lx_alphanum ∥ lx_underscore)
    -- Parser_Combinator.repeat (lx_alphanum ∥ lx_underscore ∥ lx_hyphen)
    with uncurry (#)
  "

definition [consuming]:
  "parse_bound ≡ ta_var_ident --
    exactly ''['' *-- lx_int -- exactly '':'' *-- lx_int --* exactly '']''"

definition "parse_bounds ≡ parse_list' (lx_ws *-- parse_bound with (λ(s,p). (String.implode s, p)))"

lemma
  "parse parse_bounds (STR ''id[-1:2], id[-1:0]'')
 = Result [(STR ''id'', -1, 2), (STR ''id'', -1, 0)]"
  by eval

lemma "parse parse_bounds (STR '''') = Result []"
  by eval

definition [consuming]:
  "scan_var = ta_var_ident"

abbreviation seq_ignore_left_ws (infixr "**--" 60)
  where "p **-- q ≡ token p *-- q" for p q

abbreviation seq_ignore_right_ws (infixr "--**" 60)
  where "p --** q ≡ token p --* q" for p q

abbreviation seq_ws (infixr "---" 60)
  where "seq_ws p q ≡ token p -- q" for p q

definition scan_acconstraint where [unfolded Let_def, consuming]:
  "scan_acconstraint ≡
    let scan =
      (λs c. scan_var --- exactly s **-- token lx_int with (λ(x, y). c (String.implode x) y)) in
  (
    scan ''<''  lt ∥
    scan ''<='' le ∥
    scan ''=='' eq ∥
    scan ''=''  eq ∥
    scan ''>='' ge ∥
    scan ''>''  gt
  )
"

definition [consuming]:
  "scan_parens lparen rparen inner ≡ exactly lparen **-- inner --** token (exactly rparen)"

definition [consuming]: "scan_loc ≡
  (scan_var --- (exactly ''.'' *-- scan_var))
  with (λ (p, s). loc (String.implode p) (String.implode s))"

definition [consuming]: "scan_bexp_elem ≡ scan_acconstraint ∥ scan_loc"

abbreviation "scan_parens' ≡ scan_parens ''('' '')''"

definition [consuming]: "scan_infix_pair a b s ≡ a --- exactly s **-- token b"

lemma [fundef_cong]:
  assumes "⋀l2. ll_fuel l2 ≤ ll_fuel l' ⟹ A l2 = A' l2"
  assumes "⋀l2. ll_fuel l2 + (if length s > 0 then 1 else 0) ≤ ll_fuel l' ⟹ B l2 = B' l2"
  assumes "s = s'" "l=l'"
  shows "scan_infix_pair A B s l = scan_infix_pair A' B' s' l'"
  using assms unfolding scan_infix_pair_def gen_token_def
  by (cases s; intro Parser_Combinator.bind_cong repeat_cong assms) auto

lemma [fundef_cong]:
  assumes "⋀l2. ll_fuel l2 < ll_fuel l ⟹ A l2 = A' l2" "l = l'"
  shows "scan_parens' A l = scan_parens' A' l'"
  using assms unfolding scan_parens_def gen_token_def
  by (intro Parser_Combinator.bind_cong repeat_cong assms) auto

lemma token_cong[fundef_cong]:
  assumes "⋀l2. ll_fuel l2 ≤ ll_fuel l ⟹ A l2 = A' l2" "l = l'"
  shows "token A l = token A' l'"
  using assms unfolding scan_parens_def gen_token_def
  by (intro Parser_Combinator.bind_cong repeat_cong assms) auto

lemma is_cparser_scan_parens'[parser_rules]:
  "is_cparser (scan_parens' a)"
  unfolding scan_parens_def by simp

fun aexp and mexp and scan_exp and scan_7 and scan_6 and scan_0 where ― ‹slow: 90s›
  "aexp ::=
  token lx_int with exp.const ∥ token scan_var with exp.var o String.implode ∥
  scan_parens' (scan_exp --- exactly ''?'' **-- scan_7 --- exactly '':'' **-- scan_exp)
  with (λ (e1, b, e2). exp.if_then_else b e1 e2) ∥
  tk_lparen **-- scan_exp --** tk_rparen"
| "mexp ::= chainL1 aexp (multiplicative_op with (λf a b. exp.binop f a b))"
| "scan_exp ::= chainL1 mexp (additive_op with (λf a b. exp.binop f a b))"
| "scan_7 ::=
    scan_infix_pair scan_6 scan_7 ''->'' with uncurry bexp.imply ∥
    scan_infix_pair scan_6 scan_7 ''||'' with uncurry bexp.or ∥
    scan_6" |
  "scan_6 ::=
    scan_infix_pair scan_0 scan_6 ''&&'' with uncurry bexp.and ∥
    scan_0" |
  "scan_0 ::=
    (exactly ''~'' ∥ exactly ''!'') **-- scan_parens' scan_7 with bexp.not ∥
    token (exactly ''true'') with (λ_. bexp.true) ∥
    scan_infix_pair aexp aexp ''<='' with uncurry bexp.le ∥
    scan_infix_pair aexp aexp ''<''  with uncurry bexp.lt ∥
    scan_infix_pair aexp aexp ''=='' with uncurry bexp.eq ∥
    scan_infix_pair aexp aexp ''>''  with uncurry bexp.gt ∥
    scan_infix_pair aexp aexp ''>='' with uncurry bexp.ge ∥
    scan_parens' scan_7"

context
  fixes elem :: "(char, 'bexp) parser"
    and Imply Or And :: "'bexp ⇒ 'bexp ⇒ 'bexp"
    and Not :: "'bexp ⇒ 'bexp"
begin

fun scan_7' and scan_6' and scan_0' where
  "scan_7' ::=
    scan_infix_pair scan_6' scan_7' ''->'' with uncurry Imply ∥
    scan_infix_pair scan_6' scan_7' ''||'' with uncurry Or ∥
    scan_6'" |
  "scan_6' ::=
    scan_infix_pair scan_0' scan_6' ''&&'' with uncurry And ∥
    scan_0'" |
  "scan_0' ::=
    (exactly ''~'' ∥ exactly ''!'') **-- scan_parens' scan_7' with Not ∥
    elem ∥
    scan_parens' scan_7'"

context
  assumes [parser_rules]: "is_cparser elem"
begin

lemma [parser_rules]:
  "is_cparser scan_0'"
  by (simp add: scan_0'.simps[abs_def])

lemma [parser_rules]:
  "is_cparser scan_6'"
  by (subst scan_6'.simps[abs_def]) simp

end
end

abbreviation "scan_bexp ≡ scan_7' scan_bexp_elem sexp.imply sexp.or sexp.and sexp.not"

lemma [parser_rules]:
  "is_cparser scan_bexp"
  by (subst scan_7'.simps[abs_def]) simp

lemma "parse scan_bexp (STR ''a < 3 && b>=2 || ~ (c <= 4)'')
= Result (sexp.or (and (lt STR ''a'' 3) (ge STR ''b'' 2)) (not (sexp.le STR ''c'' 4)))"
  by eval

definition [consuming]: "scan_prefix p head = exactly head **-- p" for p

definition [consuming]: "scan_formula ≡
  scan_prefix scan_bexp ''E<>'' with formula.EX ∥
  scan_prefix scan_bexp ''E[]'' with EG ∥
  scan_prefix scan_bexp ''A<>'' with AX ∥
  scan_prefix scan_bexp ''A[]'' with AG ∥
  scan_infix_pair scan_bexp scan_bexp ''-->'' with uncurry Leadsto"

(* unused *)
lemma is_cparser_token[parser_rules]:
  "is_cparser (token a)" if "is_cparser a"
  using that unfolding gen_token_def by simp

definition [consuming]: "scan_action ≡
  (scan_var --* token (exactly ''?'')) with In o String.implode ∥
  (scan_var --* token (exactly ''!'')) with Out o String.implode ∥
  scan_var with Sil o String.implode"

abbreviation orelse (infix "orelse" 58) where
  "a orelse b ≡ default b a"

definition
  "parse_action s ≡ parse scan_action s orelse Sil (STR '''')"

fun chop_sexp where
  "chop_sexp clocks (and a b) (cs, es) =
    chop_sexp clocks a (cs, es) |> chop_sexp clocks b" |
  "chop_sexp clocks (eq a b) (cs, es) =
    (if a ∈ set clocks then (eq a b # cs, es) else (cs, eq a b # es))" |
  "chop_sexp clocks (le a b) (cs, es) =
    (if a ∈ set clocks then (le a b # cs, es) else (cs, le a b # es))" |
  "chop_sexp clocks (lt a b) (cs, es) =
    (if a ∈ set clocks then (lt a b # cs, es) else (cs, lt a b # es))" |
  "chop_sexp clocks (ge a b) (cs, es) =
    (if a ∈ set clocks then (ge a b # cs, es) else (cs, ge a b # es))" |
  "chop_sexp clocks (gt a b) (cs, es) =
    (if a ∈ set clocks then (gt a b # cs, es) else (cs, gt a b # es))" |
  "chop_sexp clocks a (cs, es) = (cs, a # es)"

fun sexp_to_acconstraint :: "(String.literal, String.literal, String.literal, int) sexp ⇒ _" where
  "sexp_to_acconstraint (lt a (b :: int)) = acconstraint.LT a b" |
  "sexp_to_acconstraint (le a b) = acconstraint.LE a b" |
  "sexp_to_acconstraint (eq a b) = acconstraint.EQ a b" |
  "sexp_to_acconstraint (ge a b) = acconstraint.GE a b" |
  "sexp_to_acconstraint (gt a b) = acconstraint.GT a b"

no_notation top_assn ("true")

fun sexp_to_bexp :: "(String.literal, String.literal, String.literal, int) sexp ⇒ _" where
  "sexp_to_bexp (lt a (b :: int)) = bexp.lt (exp.var a) (exp.const b) |> Result" |
  "sexp_to_bexp (le a b) = bexp.le (exp.var a) (exp.const b) |> Result" |
  "sexp_to_bexp (eq a b) = bexp.eq (exp.var a) (exp.const b) |> Result" |
  "sexp_to_bexp (ge a b) = bexp.ge (exp.var a) (exp.const b) |> Result" |
  "sexp_to_bexp (gt a b) = bexp.gt (exp.var a) (exp.const b) |> Result" |
  "sexp_to_bexp (and a b) =
    do {a ← sexp_to_bexp a; b ← sexp_to_bexp b; bexp.and a b |> Result}" |
  "sexp_to_bexp (sexp.or a b) =
    do {a ← sexp_to_bexp a; b ← sexp_to_bexp b; bexp.or a b |> Result}" |
  "sexp_to_bexp (imply a b) =
    do {a ← sexp_to_bexp a; b ← sexp_to_bexp b; bexp.imply a b |> Result}" |
  "sexp_to_bexp x        = Error [STR ''Illegal construct in binary operation'']"

(*
definition [consuming]: "scan_bexp_elem' ≡
  token (exactly ''true'') with (λ_. bexp.true) ∥
  scan_acconstraint with (λb. case sexp_to_bexp b of Result b ⇒ b)"

abbreviation "scan_bexp' ≡ scan_7 scan_bexp_elem' bexp.imply bexp.or bexp.and bexp.not"

lemma [parser_rules]:
  "is_cparser scan_bexp'"
  by (subst scan_7.simps[abs_def]) simp

lemma token_cong[fundef_cong]:
  assumes "⋀l2. ll_fuel l2 ≤ ll_fuel l ⟹ A l2 = A' l2" "l = l'"
  shows "token A l = token A' l'"
  using assms unfolding scan_parens_def gen_token_def
  by (intro Parser_Combinator.bind_cong repeat_cong assms) auto
*)

(*
abbreviation additive_op where "additive_op ≡ 
  tk_plus ⪢ Parser_Combinator.return (+)
∥ tk_minus ⪢ Parser_Combinator.return (-)"

  abbreviation "multiplicative_op ≡ 
    tk_times ⪢ return ( * )
  ∥ tk_div ⪢ return (div)"  
  abbreviation "power_op ≡ 
    tk_power ⪢ return (λa b. a^nat b)" ― ‹Note: Negative powers are treated as ‹x⇧0››
*)

definition [consuming]:
  "scan_update ≡
   scan_var --- (exactly ''='' ∥ exactly '':='') **-- scan_exp
   with (λ(s, x). (String.implode s, x))"

abbreviation "scan_updates ≡ parse_list scan_update"

value "parse scan_updates (STR '' y2  := 0'')"
(* = Result [(STR ''y2'', exp.const (0 :: int))] *)

value "parse scan_updates (STR ''y2 := 0, x2 := 0'')"
(* = Result [(STR ''y2'', exp.const 0), (STR ''x2'', exp.const 0)]" *)
value "parse scan_exp (STR ''( 1 ? L == 0 : 0 )'')"
(*  = Result (if_then_else (bexp.eq STR ''L'' 0) (exp.const 1) (exp.const 0)) *)

definition compile_invariant where
  "compile_invariant clocks vars inv ≡
    let
      (cs, es) = chop_sexp clocks inv ([], []);
      g = map sexp_to_acconstraint cs
    in
      if es = []
      then Result (g, bexp.true)
      else do {
        let e = fold (and) (tl es) (hd es);
        b ← sexp_to_bexp e;
        assert (set_bexp b ⊆ set vars) (String.implode (''Unknown variable in bexp: '' @ show b));
        Result (g, b)
      }" for inv

definition compile_invariant' where
  "compile_invariant' clocks vars inv ≡
  if inv = STR '''' then
    Result ([], bexp.true)
  else do {
    inv ← parse scan_bexp inv |> err_msg (STR ''Failed to parse guard in '' + inv);
    compile_invariant clocks vars inv
  }
" for inv

definition convert_node where
  "convert_node clocks vars n ≡ do {
    n ←  of_object n;
    ID ← get n ''id'' ⤜ of_nat;
    name ← get n ''name'' ⤜ of_string;
    inv ← get n ''invariant'' ⤜ of_string;
    (inv, inv_vars) ←
      compile_invariant' clocks vars inv |> err_msg (STR ''Failed to parse invariant!'');
    assert (case inv_vars of bexp.true ⇒ True | _ ⇒ False)
      (STR ''State invariants on nodes are not supported'');
    Result ((name, ID), inv)
  }"

definition convert_edge where
  "convert_edge clocks vars e ≡ do {
    e ← of_object e;
    source ← get e ''source'' ⤜ of_nat;
    target ← get e ''target'' ⤜ of_nat;
    guard  ← get e ''guard''  ⤜ of_string;
    label  ← get e ''label''  ⤜ of_string;
    update ← get e ''update'' ⤜ of_string;
    label  ← if label = STR '''' then STR '''' |> Sil |> Result else
      parse scan_action label |> err_msg (STR ''Failed to parse label in '' + label);
    (g, check)  ← compile_invariant' clocks vars guard |> err_msg (STR ''Failed to parse guard!'');
    upd ← if update = STR '''' then Result [] else
      parse scan_updates update |> err_msg (STR ''Failed to parse update in '' + update);
    let resets = filter (λx. fst x ∈ set clocks) upd;
    assert
      (list_all (λ(_, d). case d of exp.const x ⇒ x = 0 | _ ⇒ undefined) resets)
      (STR ''Clock resets to values different from zero are not supported'');
    let resets = map fst resets;
    let upds = filter (λx. fst x ∉ set clocks) upd;
    assert
      (list_all (λ(x, _). x ∈ set vars) upds)
      (STR ''Unknown variable in update: '' + update);
    Result (source, check, g, label, upds, resets, target)
  }"

definition convert_automaton where
  "convert_automaton clocks vars a ≡ do {
    nodes ← get a ''nodes'' ⤜ of_array;
    edges ← get a ''edges'' ⤜ of_array;
    nodes ← combine_map (convert_node clocks vars) nodes;
    let invs = map (λ ((_, n), g). (n, g)) nodes;
    let names_to_ids = map fst nodes;
    assert (map fst names_to_ids |> filter (λs. s ≠ STR '''') |> distinct)
      (STR ''Node names are ambiguous'' + (show (map fst names_to_ids) |> String.implode));
    assert (map snd names_to_ids |> distinct) (STR ''Duplicate node id'');
    let ids_to_names = map_of (map prod.swap names_to_ids);
    let names_to_ids = map_of names_to_ids;
    let committed = default [] (get a ''committed'' ⤜ of_array);
    committed ← combine_map of_nat committed;
    let urgent = default [] (get a ''urgent'' ⤜ of_array);
    urgent ← combine_map of_nat urgent;
    edges ← combine_map (convert_edge clocks vars) edges;
    Result (names_to_ids, ids_to_names, (committed, urgent, edges, invs))
  }"

fun rename_locs_sexp where
  "rename_locs_sexp f (not a) =
    do {a ← rename_locs_sexp f a; not a |> Result}" |
  "rename_locs_sexp f (imply a b) =
    do {a ← rename_locs_sexp f a; b ← rename_locs_sexp f b; imply a b |> Result}" |
  "rename_locs_sexp f (sexp.or a b) =
    do {a ← rename_locs_sexp f a; b ← rename_locs_sexp f b; sexp.or a b |> Result}" |
  "rename_locs_sexp f (and a b) =
    do {a ← rename_locs_sexp f a; b ← rename_locs_sexp f b; and a b |> Result}" |
  "rename_locs_sexp f (loc n x) = do {x ← f n x; loc n x |> Result}" |
  "rename_locs_sexp f (eq a b) = Result (eq a b)" |
  "rename_locs_sexp f (lt a b) = Result (lt a b)" |
  "rename_locs_sexp f (le a b) = Result (le a b)" |
  "rename_locs_sexp f (ge a b) = Result (ge a b)" |
  "rename_locs_sexp f (gt a b) = Result (gt a b)"

fun rename_locs_formula where
  "rename_locs_formula f (formula.EX φ) = rename_locs_sexp f φ ⤜ Result o formula.EX" |
  "rename_locs_formula f (EG φ) = rename_locs_sexp f φ ⤜ Result o EG" |
  "rename_locs_formula f (AX φ) = rename_locs_sexp f φ ⤜ Result o AX" |
  "rename_locs_formula f (AG φ) = rename_locs_sexp f φ ⤜ Result o AG" |
  "rename_locs_formula f (Leadsto φ ψ) =
    do {φ ← rename_locs_sexp f φ; ψ ← rename_locs_sexp f ψ; Leadsto φ ψ |> Result}"

definition convert :: "JSON ⇒
  ((nat ⇒ nat ⇒ String.literal) × (String.literal ⇒ nat) × String.literal list ×
    (nat list × nat list ×
     (String.literal act, nat, String.literal, int, String.literal, int) transition list
      × (nat × (String.literal, int) cconstraint) list) list ×
   (String.literal × int × int) list ×
   (nat, nat, String.literal, int) formula × nat list × (String.literal × int) list
  ) Error_List_Monad.result" where
  "convert json ≡ do {
    all ← of_object json;
    automata ← get all ''automata'';
    automata ← of_array automata;
    let broadcast = default [] (do {x ← get all ''broadcast''; of_array x});
    broadcast ← combine_map of_string broadcast;
    let _ = trace_level 3
      (λ_. return (STR ''Broadcast channels '' + String.implode (show broadcast)));
    let bounds = default (STR '''') (do {
      x ← get all ''vars''; of_string x}
    );
    bounds ← parse parse_bounds bounds |> err_msg (STR ''Failed to parse bounds'');
    clocks ← get all ''clocks'';
    clocks ← of_string clocks;
    clocks ← parse (parse_list (lx_ws *-- ta_var_ident with String.implode)) clocks
       |> err_msg (STR ''Failed to parse clocks'');
    formula ← get all ''formula'';
    formula ← of_string formula;
    formula ← parse scan_formula formula |> err_msg (STR ''Failed to parse formula'');
    automata ← combine_map of_object automata;
    process_names ← combine_map (λa. get a ''name'' ⤜ of_string) automata;
    assert (distinct process_names) (STR ''Process names are ambiguous'');
    assert (locs_of_formula formula ⊆ set process_names) (STR ''Unknown process name in formula'');
    let process_names_to_index = List_Index.index process_names;
    init_locs ← combine_map
      (λa. do {x ← get a ''initial''; x ← of_nat x; x |> Result})
      automata;
    let formula = formula.map_formula process_names_to_index id id id formula;
    let vars = map fst bounds;
    let init_vars = map (λx. (x, 0::int)) vars;
    names_automata ← combine_map (convert_automaton clocks vars) automata;
    let automata = map (snd o snd) names_automata;
    let names    = map fst names_automata;
    let ids_to_names = map (fst o snd) names_automata;
    let ids_to_names =
      (λp i. case (ids_to_names ! p) i of Some n ⇒ n | None ⇒ String.implode (show i));
    formula ← rename_locs_formula (λi. get (names ! i)) formula;
    Result
    (ids_to_names, process_names_to_index,
     broadcast, automata, bounds, formula, init_locs, init_vars)
}" for json



paragraph ‹Unsafe Glue Code for Printing›

code_printing
  constant print ⇀ (SML) "writeln _"
       and        (OCaml) "print'_string _"
code_printing
  constant println ⇀ (SML) "writeln _"
       and          (OCaml) "print'_string _"

definition parse_convert_run_print where
  "parse_convert_run_print dc s ≡
   case parse json s ⤜ convert of
     Error es ⇒ do {let _ = map println es; return ()}
   | Result (ids_to_names, _, broadcast, automata, bounds, formula, L⇩0, s⇩0) ⇒ do {
      r ← do_preproc_mc dc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula;
      case r of
        Error es ⇒ do {let _ = map println es; return ()}
      | Result s ⇒ do {let _ = println s; return ()}
  }"

definition parse_convert_run where
  "parse_convert_run dc s ≡
   case
      parse json s ⤜ (λr.
      let
      s' = show r |> String.implode;
      _  = trace_level 2 (λ_. return s')
      in parse json s' ⤜ (λr'.
      assert (r = r') STR ''Parse-print-parse loop failed!'' ⤜ (λ_. convert r)))
   of
     Error es ⇒ return (Error es)
   | Result (ids_to_names, _, broadcast, automata, bounds, formula, L⇩0, s⇩0) ⇒
      do_preproc_mc dc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula
"

definition convert_run where
  "convert_run dc json_data ≡
   case (
      let
      s' = show json_data |> String.implode;
      _  = trace_level 2 (λ_. return s')
      in parse json s' ⤜ (λr'.
      assert (json_data = r') STR ''Parse-print-parse loop failed!'' ⤜ (λ_. convert json_data)))
   of
     Error es ⇒ return (Error es)
   | Result (ids_to_names, _, broadcast, automata, bounds, formula, L⇩0, s⇩0) ⇒
      do_preproc_mc dc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula
"

text ‹Eliminate Gabow statistics›
code_printing
  code_module Gabow_Skeleton_Statistics ⇀ (SML) ‹›
code_printing
  code_module AStatistics ⇀ (SML) ‹›

text ‹Delete ``junk''›
code_printing code_module Bits_Integer ⇀ (SML) ‹›

code_printing
  constant stat_newnode ⇀ (SML) "(fn x => ()) _"
| constant stat_start   ⇀ (SML) "(fn x => ()) _"
| constant stat_stop    ⇀ (SML) "(fn x => ()) _"


(* Fix to IArray theory *)
code_printing
  constant IArray.sub' ⇀ (SML) "(Vector.sub o (fn (a, b) => (a, IntInf.toInt b)))"

code_printing code_module "Logging" ⇀ (SML)
‹
structure Logging : sig
  val set_level : int -> unit
  val trace : int -> (unit -> string) -> unit
  val get_trace: unit -> (int * string) list
end = struct
  val level = Unsynchronized.ref 0;
  val messages : (int * string) list ref = Unsynchronized.ref [];
  fun set_level i = level := i;
  fun get_trace () = !messages;
  fun trace i f =
    if i > !level
    then ()
    else
      let
        val s = f ();
        val _ = messages := (i, s) :: !messages;
      in () end;
end
›
and (Eval) ‹›
code_reserved (Eval) Logging
code_reserved (SML) Logging


code_printing constant trace_level ⇀ (SML)
  "Logging.trace (IntInf.toInt (integer'_of'_int _)) (_ ())"
and (Eval)
  "(fn '_ => fn s => writeln (s ())) _ (_ ())"

text ‹To disable state tracing:›
⌦‹code_printing
  constant "Show_State_Defs.tracei" ⇀
      (SML)   "(fn n => fn show_state => fn show_clock => fn typ => fn x => ()) _ _ _"
  and (OCaml) "(fun n show_state show_clock ty x -> -> ()) _ _ _"›

paragraph ‹SML Code Export›
text_raw ‹\label{export-munta}›

text ‹Now we export the actual executable code for \munta. First for SML:›

export_code parse_convert_run Result Error
  in SML module_name Model_Checker
  file_prefix "Simple_Model_Checker"

paragraph ‹OCaml Code Export›
text_raw ‹\label{export-ocaml}›

text ‹This is how to do it for OCaml:›

declare [[code abort:
  Diff_Array.new_array'
  Diff_Array.array_length'
  Diff_Array.array_get'
  Diff_Array.array_set'
  Diff_Array.array_grow'
  Diff_Array.array_shrink'
]] ― ‹TODO: there is no setup of diff arrays for OCaml›

export_code
  convert_run Result Error String.explode int_of_integer nat_of_integer
  JSON.Object JSON.Array JSON.String JSON.Int JSON.Nat JSON.Rat JSON.Boolean JSON.Null fract.Rat
  in OCaml module_name Model_Checker
  file_prefix "Simple_Model_Checker"

paragraph ‹Running Munta›
text_raw ‹\label{run-munta}›

text ‹
Adding a bit of wrapper code, so that we can directly run \textsc{Munta} from within Isabelle:
›
definition parse_convert_run_test where
  "parse_convert_run_test dc s ≡ do {
    x ← parse_convert_run dc s;
    case x of
      Error es ⇒ do {let _ = map println es; return (STR ''Fail'')}
    | Result r ⇒ return r
  }"

ML ‹
  fun assert comp exp =
    if comp = exp then () else error ("Assertion failed! expected: " ^ exp ^ " but got: " ^ comp)
  fun test dc file =
  let
    val dir = Path.append @{master_dir} @{path "../benchmarks/"}
    val file = Path.explode file |> Path.append dir
    val s = File.read file
  in
    @{code parse_convert_run_test} dc s end
›

text ‹Now we can run \munta\ on a few examples:›

ML_val ‹assert (test false "HDDI_02.muntax" ()) "Property is not satisfied!"›
ML_val ‹assert (test true "HDDI_02.muntax" ()) "Model has no deadlock!"›

ML_val ‹assert (test false "simple.muntax" ()) "Property is satisfied!"›
ML_val ‹assert (test true "simple.muntax" ()) "Model has no deadlock!"›

ML_val ‹assert (test false "light_switch.muntax" ()) "Property is satisfied!"›
ML_val ‹assert (test true "light_switch.muntax" ()) "Model has no deadlock!"›

ML_val ‹assert (test false "PM_test.muntax" ()) "Property is not satisfied!"›
ML_val ‹assert (test true "PM_test.muntax" ()) "Model has a deadlock!"›

ML_val ‹assert (test false "bridge.muntax" ()) "Property is satisfied!"›
ML_val ‹assert (test true "bridge.muntax" ()) "Model has no deadlock!"›

ML_val ‹assert (test false "fischer.muntax" ()) "Property is satisfied!"›
ML_val ‹assert (test true "fischer.muntax" ()) "Model has no deadlock!"›

ML_val ‹assert (test false "PM_all_4.muntax" ()) "Property is not satisfied!"›
ML_val ‹assert (test true "PM_all_4.muntax" ()) "Model has no deadlock!"›

end