Theory Simple_Network_Language_Certificate_Code
section ‹Assembling the Checker and Generating Code›
text ‹\label{export-muntac}
We provide some optimized code equations.
Then we assemble the certificate checker:
▪ A parser is added to parse JSON files
▪ The resulting JSON data is validated and converted to the simple networks language
▪ The (binary) certificate is read
▪ There is an additional ``renaming'' that maps identifiers between the input and the certificate
▪ The certficiate, the renaming, and the model are passed to the checker
▪ and the output is printed
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_Certificate_Code
imports
Simple_Network_Language_Certificate
Simple_Network_Language_Certificate_Checking
begin
paragraph ‹Optimized code equations›
lemmas [code_unfold] = imp_for_imp_for'
definition dbm_subset'_impl'_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array ⇒ bool Heap"
where [symmetric, int_folds]:
"dbm_subset'_impl'_int = dbm_subset'_impl'"
lemma less_eq_dbm_le_int[int_folds]:
"(≤) = dbm_le_int"
unfolding dbm_le_dbm_le_int less_eq ..
schematic_goal dbm_subset'_impl'_int_code[code]:
"dbm_subset'_impl'_int ≡ λm a b.
do {
imp_for 0 ((m + 1) * (m + 1)) Heap_Monad.return
(λi _. do {
x ← Array.nth a i; y ← Array.nth b i; Heap_Monad.return (dbm_le_int x y)
})
True
}
"
unfolding dbm_subset'_impl'_int_def[symmetric] dbm_subset'_impl'_def int_folds .
definition dbm_subset_impl_int
:: "nat ⇒ int DBMEntry Heap.array ⇒ int DBMEntry Heap.array ⇒ bool Heap"
where [symmetric, int_folds]:
"dbm_subset_impl_int = dbm_subset_impl"
schematic_goal dbm_subset_impl_int_code[code]:
"dbm_subset_impl_int ≡ ?i"
unfolding dbm_subset_impl_int_def[symmetric] dbm_subset_impl_def
unfolding int_folds
.
lemmas [code_unfold] = int_folds
export_code state_space in SML module_name Test
hide_const Parser_Combinator.return
hide_const Error_Monad.return
definition
"show_lit = String.implode o show"
definition "rename_state_space ≡ λdc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula.
let _ = println (STR ''Make renaming'') in
do {
(m, num_states, num_actions, renum_acts, renum_vars, renum_clocks, renum_states,
inv_renum_states, inv_renum_vars, inv_renum_clocks)
← make_renaming broadcast automata bounds;
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);
let f = (λshow_clock
show_state broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula.
state_space broadcast bounds' automata m num_states num_actions k L⇩0 s⇩0 formula
show_clock show_state ()
);
let r = do_rename_mc f 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;
let show_clock = show o inv_renum_clocks;
let show_state = (show_state :: _ ⇒ _ ⇒ _ × int list ⇒ _) inv_renum_states inv_renum_vars;
let renamings =
(m, num_states, num_actions, renum_acts, renum_vars, renum_clocks, renum_states,
inv_renum_states, inv_renum_vars, inv_renum_clocks
);
Result (r, show_clock, show_state, renamings, k)
}"
definition
"check_subsumed n xs (i :: int) M ≡
do {
(_, b) ← imp_nfoldli xs (λ(_, b). return (¬ b)) (λM' (j, b).
if i = j then return (j + 1, b) else do {
b ← dbm_subset'_impl n M M';
if b then return (j, True) else return (j + 1, False)
}
) (0, False);
return b
}
"
definition
"imp_filter_index P xs = do {
(_, xs) ← imp_nfoldli xs (λ_. return True) (λx (i :: nat, xs).
do {
b ← P i x;
return (i + 1, if b then (x # xs) else xs)
}
) (0, []);
return (rev xs)
}"
definition
"filter_dbm_list n xs =
imp_filter_index (λi M. do {b ← check_subsumed n xs i M; return (¬ b)}) xs"
partial_function (heap) imp_map :: "('a ⇒ 'b Heap) ⇒ 'a list ⇒ 'b list Heap" where
"imp_map f xs =
(if xs = [] then return [] else do {y ← f (hd xs); ys ← imp_map f (tl xs); return (y # ys)})"
lemma imp_map_simps[code, simp]:
"imp_map f [] = return []"
"imp_map f (x # xs) = do {y ← f x; ys ← imp_map f xs; return (y # ys)}"
by (simp add: imp_map.simps)+
definition trace_state where
"trace_state n show_clock show_state ≡
λ (l, M). do {
let st = show_state l;
m ← show_dbm_impl n show_clock show M;
let s = ''('' @ st @ '', ['' @ m @ ''])'';
let s = String.implode s;
let _ = println s;
return ()
}
" for show_clock show_state
definition
"show_str = String.implode o show"
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 {
let r = rename_state_space dc ids_to_names (broadcast, automata, bounds) L⇩0 s⇩0 formula;
case r of
Error es ⇒ do {let _ = map println es; return ()}
| Result (r, show_clk, show_st, renamings, k) ⇒
case r of None ⇒ return () | Some r ⇒
do {
r ← r;
let _ = STR ''Number of discrete states: '' + (length r |> show_str) |> println;
let _ =
STR ''Size of passed list: '' + show_str (sum_list (map (length o snd) r)) |> println;
let n = Simple_Network_Impl.clk_set' automata |> list_of_set |> length;
r ← imp_map (λ (a, b). do {
b ← imp_map (return o snd) b; b ← filter_dbm_list n b; return (a, b)
}) r;
let _ = STR ''Number of discrete states: '' + show_str (length r) |> println;
let _ = STR ''Size of passed list after removing subsumed states: ''
+ show_str (sum_list (map (length o snd) r)) |> println;
let show_dbm = (λM. do {
s ← show_dbm_impl_all n show_clk show M;
return (''<'' @ s @ ''>'')
});
_ ← imp_map (λ (s, xs).
do {
let s = show_st s;
xs ← imp_map show_dbm xs;
let _ = s @ '': '' @ show xs |> String.implode |> println;
return ()
}
) r;
return ()
}
}"
ML ‹
structure Timing : sig
val start_timer: unit -> unit
val save_time: string -> unit
val get_timings: unit -> (string * Time.time) list
end = struct
val t = Unsynchronized.ref Time.zeroTime;
val timings = Unsynchronized.ref [];
fun start_timer () = (t := Time.now ());
fun get_elapsed () = Time.- (Time.now (), !t);
fun save_time s = (timings := ((s, get_elapsed ()) :: !timings));
fun get_timings () = !timings;
end
›
ML ‹
fun print_timings () =
let
val tab = Timing.get_timings ();
fun print_time (s, t) = writeln(s ^ ": " ^ Time.toString t);
in map print_time tab end;
›
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 -> ()) _ _ _"