Initial import from AFP.

This commit is contained in:
Achim D. Brucker 2020-12-19 09:35:49 +00:00
commit bc6cffa54d
22 changed files with 5109 additions and 0 deletions

View File

@ -0,0 +1,447 @@
section\<open>Code Generation\<close>
text\<open>This theory is used to generate an executable Scala implementation of the inference tool which
can be used to infer real EFSMs from real traces. Certain functions are replaced with native
implementations. These can be found at \url{https://github.com/jmafoster1/efsm-inference/blob/master/inference-tool/src/main/scala/inference/Dirties.scala}.\<close>
theory Code_Generation
imports
"HOL-Library.Code_Target_Numeral"
Inference
SelectionStrategies
"heuristics/Store_Reuse_Subsumption"
"heuristics/Increment_Reset"
"heuristics/Same_Register"
"heuristics/Distinguishing_Guards"
"heuristics/PTA_Generalisation"
"heuristics/Weak_Subsumption"
"heuristics/Least_Upper_Bound"
EFSM_Dot
"code-targets/Code_Target_FSet"
"code-targets/Code_Target_Set"
"code-targets/Code_Target_List"
efsm2sal
begin
declare One_nat_def [simp del]
(*
Let's use the native operators for booleans and pairs
*)
code_printing
constant HOL.conj \<rightharpoonup> (Scala) "_ && _" |
constant HOL.disj \<rightharpoonup> (Scala) "_ || _" |
constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Scala) infix 4 "==" |
constant "fst" \<rightharpoonup> (Scala) "_.'_1" |
constant "snd" \<rightharpoonup> (Scala) "_.'_2"|
constant "(1::nat)" \<rightharpoonup> (Scala) "Nat.Nata((1))"
(*
This gives us a speedup as we don't need to check that a register is undefined in the initial
state if there is no way to get back there. This is true by definition.
*)
definition "initially_undefined_context_check_full = initially_undefined_context_check"
(* This gives us a speedup because we can check this before we have to call out to z3 *)
fun mutex :: "'a gexp \<Rightarrow> 'a gexp \<Rightarrow> bool" where
"mutex (Eq (V v) (L l)) (Eq (V v') (L l')) = (if v = v' then l \<noteq> l' else False)" |
"mutex (gexp.In v l) (Eq (V v') (L l')) = (v = v' \<and> l' \<notin> set l)" |
"mutex (Eq (V v') (L l')) (gexp.In v l) = (v = v' \<and> l' \<notin> set l)" |
"mutex (gexp.In v l) (gexp.In v' l') = (v = v' \<and> set l \<inter> set l' = {})" |
"mutex _ _ = False"
lemma mutex_not_gval:
"mutex x y \<Longrightarrow> gval (gAnd y x) s \<noteq> true"
unfolding gAnd_def
apply (induct x y rule: mutex.induct)
apply simp_all
apply (case_tac "s v")
apply (case_tac "s v'")
apply simp
apply simp
apply (case_tac "s v")
apply (case_tac "s v'")
apply simp
apply simp
apply (metis maybe_negate_true maybe_or_false trilean.distinct(1) value_eq.simps(3))
apply (case_tac "s v")
apply (case_tac "s v'")
apply simp
apply simp
apply simp
apply (case_tac "s v")
apply (case_tac "s v'")
apply simp
apply simp
apply simp
apply (case_tac "s v")
apply (case_tac "s v'")
by auto
(* (\<exists>(i, s1) \<in> set (get_ins (Guard t1)).
\<exists>(i', s2) \<in> set (get_ins (Guard t2)).
i = i' \<and>
\<not> (set s2) \<subseteq> (set s1) \<and>
restricted_once (I i) (Guard t2)) *)
definition choice_cases :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
"choice_cases t1 t2 = (
if \<exists>(x, y) \<in> set (List.product (Guards t1) (Guards t2)). mutex x y then
False
else if Guards t1 = Guards t2 then
satisfiable (fold gAnd (rev (Guards t1)) (gexp.Bc True))
else
satisfiable ((fold gAnd (rev (Guards t1@Guards t2)) (gexp.Bc True)))
)"
lemma existing_mutex_not_true:
"\<exists>x\<in>set G. \<exists>y\<in>set G. mutex x y \<Longrightarrow> \<not> apply_guards G s"
apply clarify
apply (simp add: apply_guards_rearrange)
apply (case_tac "y \<in> set (x#G)")
defer
apply simp
apply (simp only: apply_guards_rearrange)
apply simp
apply (simp only: apply_guards_double_cons)
using mutex_not_gval
by auto
lemma [code]: "choice t t' = choice_cases t t'"
apply (simp only: choice_alt choice_cases_def)
apply (case_tac "\<exists>x\<in>set (map (\<lambda>(x, y). mutex x y) (List.product (Guards t) (Guards t'))). x")
apply (simp add: choice_alt_def)
apply (metis existing_mutex_not_true Un_iff set_append)
apply (case_tac "Guards t = Guards t'")
apply (simp add: choice_alt_def apply_guards_append)
apply (simp add: fold_apply_guards rev_apply_guards satisfiable_def)
apply (simp add: choice_alt_def satisfiable_def)
by (metis foldr_append foldr_apply_guards foldr_conv_fold)
fun guardMatch_code :: "vname gexp list \<Rightarrow> vname gexp list \<Rightarrow> bool" where
"guardMatch_code [(gexp.Eq (V (vname.I i)) (L (Num n)))] [(gexp.Eq (V (vname.I i')) (L (Num n')))] = (i = 0 \<and> i' = 0)" |
"guardMatch_code _ _ = False"
lemma [code]: "guardMatch t1 t2 = guardMatch_code (Guards t1) (Guards t2)"
apply (simp add: guardMatch_def)
using guardMatch_code.elims(2) by fastforce
fun outputMatch_code :: "output_function list \<Rightarrow> output_function list \<Rightarrow> bool" where
"outputMatch_code [L (Num n)] [L (Num n')] = True" |
"outputMatch_code _ _ = False"
lemma [code]: "outputMatch t1 t2 = outputMatch_code (Outputs t1) (Outputs t2)"
by (metis outputMatch_code.elims(2) outputMatch_code.simps(1) outputMatch_def)
fun always_different_outputs :: "vname aexp list \<Rightarrow> vname aexp list \<Rightarrow> bool" where
"always_different_outputs [] [] = False" |
"always_different_outputs [] (a#_) = True" |
"always_different_outputs (a#_) [] = True" |
"always_different_outputs ((L v)#t) ((L v')#t') = (if v = v' then always_different_outputs t t' else True)" |
"always_different_outputs (h#t) (h'#t') = always_different_outputs t t'"
lemma always_different_outputs_outputs_never_equal:
"always_different_outputs O1 O2 \<Longrightarrow>
apply_outputs O1 s \<noteq> apply_outputs O2 s"
apply(induct O1 O2 rule: always_different_outputs.induct)
by (simp_all add: apply_outputs_def)
fun tests_input_equality :: "nat \<Rightarrow> vname gexp \<Rightarrow> bool" where
"tests_input_equality i (gexp.Eq (V (vname.I i')) (L _)) = (i = i')" |
"tests_input_equality _ _ = False"
fun no_illegal_updates_code :: "update_function list \<Rightarrow> nat \<Rightarrow> bool" where
"no_illegal_updates_code [] _ = True" |
"no_illegal_updates_code ((r', u)#t) r = (r \<noteq> r' \<and> no_illegal_updates_code t r)"
lemma no_illegal_updates_code_aux:
"(\<forall>u\<in>set u. fst u \<noteq> r) = no_illegal_updates_code u r"
proof(induct u)
case Nil
then show ?case
by simp
next
case (Cons a u)
then show ?case
apply (cases a)
apply (case_tac aa)
by auto
qed
lemma no_illegal_updates_code [code]:
"no_illegal_updates t r = no_illegal_updates_code (Updates t) r"
by (simp add: no_illegal_updates_def no_illegal_updates_code_aux)
fun input_updates_register_aux :: "update_function list \<Rightarrow> nat option" where
"input_updates_register_aux ((n, V (vname.I n'))#_) = Some n'" |
"input_updates_register_aux (h#t) = input_updates_register_aux t" |
"input_updates_register_aux [] = None"
definition input_updates_register :: "transition_matrix \<Rightarrow> (nat \<times> String.literal)" where
"input_updates_register e = (
case fthe_elem (ffilter (\<lambda>(_, t). input_updates_register_aux (Updates t) \<noteq> None) e) of
(_, t) \<Rightarrow> (case
input_updates_register_aux (Updates t) of
Some n \<Rightarrow> (n, Label t)
)
)"
definition "dirty_directly_subsumes e1 e2 s1 s2 t1 t2 = (if t1 = t2 then True else directly_subsumes e1 e2 s1 s2 t1 t2)"
definition "always_different_outputs_direct_subsumption m1 m2 s s' t2 = ((\<exists>p c1 c. obtains s c1 m1 0 <> p \<and> obtains s' c m2 0 <> p \<and> (\<exists>i. can_take_transition t2 i c)))"
lemma always_different_outputs_direct_subsumption:
"always_different_outputs (Outputs t1) (Outputs t2) \<Longrightarrow>
always_different_outputs_direct_subsumption m1 m2 s s' t2 \<Longrightarrow>
\<not> directly_subsumes m1 m2 s s' t1 t2"
apply (simp add: directly_subsumes_def always_different_outputs_direct_subsumption_def)
apply (erule exE)
apply (erule conjE)
apply (erule exE)+
apply (rule_tac x=c1 in exI)
apply (rule_tac x=c in exI)
by (metis always_different_outputs_outputs_never_equal bad_outputs)
definition negate :: "'a gexp list \<Rightarrow> 'a gexp" where
"negate g = gNot (fold gAnd g (Bc True))"
lemma gval_negate_cons:
"gval (negate (a # G)) s = gval (gNot a) s \<or>? gval (negate G) s"
apply (simp only: negate_def gval_gNot gval_fold_equiv_gval_foldr)
by (simp only: foldr.simps comp_def gval_gAnd de_morgans_2)
lemma negate_true_guard:
"(gval (negate G) s = true) = (gval (fold gAnd G (Bc True)) s = false)"
by (metis (no_types, lifting) gval_gNot maybe_double_negation maybe_not.simps(1) negate_def)
lemma gval_negate_not_invalid:
"(gval (negate gs) (join_ir i ra) \<noteq> invalid) = (gval (fold gAnd gs (Bc True)) (join_ir i ra) \<noteq> invalid)"
by (metis gval_gNot maybe_not_invalid negate_def)
definition "dirty_always_different_outputs_direct_subsumption = always_different_outputs_direct_subsumption"
lemma [code]: "always_different_outputs_direct_subsumption m1 m2 s s' t = (
if Guards t = [] then
recognises_and_visits_both m1 m2 s s'
else
dirty_always_different_outputs_direct_subsumption m1 m2 s s' t
)"
apply (simp add: always_different_outputs_direct_subsumption_def)
apply (simp add: recognises_and_visits_both_def)
apply safe
apply (rule_tac x=p in exI)
apply auto[1]
using can_take_transition_empty_guard apply blast
apply (metis always_different_outputs_direct_subsumption_def dirty_always_different_outputs_direct_subsumption_def)
by (simp add: always_different_outputs_direct_subsumption_def dirty_always_different_outputs_direct_subsumption_def)
definition guard_subset_subsumption :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
"guard_subset_subsumption t1 t2 = (Label t1 = Label t2 \<and> Arity t1 = Arity t2 \<and> set (Guards t1) \<subseteq> set (Guards t2) \<and> Outputs t1 = Outputs t2 \<and> Updates t1 = Updates t2)"
lemma guard_subset_subsumption:
"guard_subset_subsumption t1 t2 \<Longrightarrow> directly_subsumes a b s s' t1 t2"
apply (rule subsumes_in_all_contexts_directly_subsumes)
apply (simp add: subsumes_def guard_subset_subsumption_def)
by (metis can_take_def can_take_transition_def can_take_subset)
definition "guard_subset_eq_outputs_updates t1 t2 = (Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
Outputs t1 = Outputs t2 \<and>
Updates t1 = Updates t2 \<and>
set (Guards t2) \<subseteq> set (Guards t1))"
definition "guard_superset_eq_outputs_updates t1 t2 = (Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
Outputs t1 = Outputs t2 \<and>
Updates t1 = Updates t2 \<and>
set (Guards t2) \<supset> set (Guards t1))"
definition is_generalisation_of :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"is_generalisation_of t' t i r = (
t' = remove_guard_add_update t i r \<and>
i < Arity t \<and>
r \<notin> set (map fst (Updates t)) \<and>
(length (filter (tests_input_equality i) (Guards t)) \<ge> 1)
)"
lemma tests_input_equality:
"(\<exists>v. gexp.Eq (V (vname.I xb)) (L v) \<in> set G) = (1 \<le> length (filter (tests_input_equality xb) G))"
proof(induct G)
case Nil
then show ?case by simp
next
case (Cons a G)
then show ?case
apply (cases a)
apply simp
apply simp
apply (case_tac x21)
apply simp
apply simp
apply (case_tac "x2 = vname.I xb")
apply simp
defer
defer
apply simp+
apply (case_tac x22)
apply auto[1]
apply simp+
apply (case_tac x22)
using tests_input_equality.elims(2) by auto
qed
lemma [code]:
"Store_Reuse.is_generalisation_of x xa xb xc = is_generalisation_of x xa xb xc"
apply (simp add: Store_Reuse.is_generalisation_of_def is_generalisation_of_def)
using tests_input_equality by blast
definition iEFSM2dot :: "iEFSM \<Rightarrow> nat \<Rightarrow> unit" where
"iEFSM2dot _ _ = ()"
definition logStates :: "iEFSM \<Rightarrow> nat \<Rightarrow> unit" where
"logStates _ _ = ()"
(* This is the infer function but with logging *)
(*
function infer_with_log :: "nat \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"infer_with_log stepNo k e r m check np = (
let scores = if k = 1 then score_1 e r else (k_score k e r) in
case inference_step e scores m check np of
None \<Rightarrow> e |
Some new \<Rightarrow> let
temp = iEFSM2dot new stepNo;
temp2 = logStates (size (S new)) (size (S e)) in
if (S new) |\<subset>| (S e) then
infer_with_log (stepNo + 1) k new r m check np
else e
)"
*)
(*
function infer_with_log :: "(cfstate \<times> cfstate) set \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where *)
function infer_with_log :: "(cfstate \<times> cfstate) set \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"infer_with_log failedMerges k e r m check np = (
let scores = if k = 1 then score_1 e r else (k_score k e r) in
case inference_step failedMerges e (ffilter (\<lambda>s. (S1 s, S2 s) \<notin> failedMerges \<and> (S2 s, S1 s) \<notin> failedMerges) scores) m check np of
(None, _) \<Rightarrow> e |
(Some new, failedMerges) \<Rightarrow> if (Inference.S new) |\<subset>| (Inference.S e) then
let temp2 = logStates new (size (Inference.S e)) in
infer_with_log failedMerges k new r m check np else e
)"
by auto
termination
apply (relation "measures [\<lambda>(_, _, e, _). size (Inference.S e)]")
apply simp
by (metis (no_types, lifting) case_prod_conv measures_less size_fsubset)
lemma infer_empty: "infer f k {||} r m check np = {||}"
by (simp add: score_1_def S_def fprod_empty k_score_def)
(*
lemma [code]: "infer f k e r m check np = infer_with_log f k e r m check np"
sorry
*)
(* declare make_pta_fold [code] *)
declare GExp.satisfiable_def [code del]
declare initially_undefined_context_check_full_def [code del]
declare generalise_output_context_check_def [code del]
declare dirty_always_different_outputs_direct_subsumption_def [code del]
declare diff_outputs_ctx_def [code del]
declare random_member_def [code del]
declare dirty_directly_subsumes_def [code del]
declare recognises_and_visits_both_def [code del]
declare initially_undefined_context_check_def [code del]
declare can_still_take_ctx_def [code del]
code_printing
constant infer \<rightharpoonup> (Scala) "Code'_Generation.infer'_with'_log" |
constant recognises_and_visits_both \<rightharpoonup> (Scala) "Dirties.recognisesAndGetsUsToBoth" |
constant iEFSM2dot \<rightharpoonup> (Scala) "PrettyPrinter.iEFSM2dot(_, _)" |
constant logStates \<rightharpoonup> (Scala) "Log.logStates(_, _)" |
constant "dirty_directly_subsumes" \<rightharpoonup> (Scala) "Dirties.scalaDirectlySubsumes" |
constant "GExp.satisfiable" \<rightharpoonup> (Scala) "Dirties.satisfiable" |
constant "initially_undefined_context_check_full" \<rightharpoonup> (Scala) "Dirties.initiallyUndefinedContextCheck" |
constant "generalise_output_context_check" \<rightharpoonup> (Scala) "Dirties.generaliseOutputContextCheck" |
constant "dirty_always_different_outputs_direct_subsumption" \<rightharpoonup> (Scala) "Dirties.alwaysDifferentOutputsDirectSubsumption" |
constant "diff_outputs_ctx" \<rightharpoonup> (Scala) "Dirties.diffOutputsCtx" |
constant "can_still_take" \<rightharpoonup> (Scala) "Dirties.canStillTake" |
constant "random_member" \<rightharpoonup> (Scala) "Dirties.randomMember"
code_printing
constant "show_nat" \<rightharpoonup> (Scala) "Code'_Numeral.integer'_of'_nat((_)).toString()"
| constant "show_int" \<rightharpoonup> (Scala) "Code'_Numeral.integer'_of'_int((_)).toString()"
| constant "join" \<rightharpoonup> (Scala) "_.mkString((_))"
(*
Mapping finfuns to Scala native Maps
*)
code_printing
type_constructor finfun \<rightharpoonup> (Scala) "Map[_, _]"
| constant "finfun_const" \<rightharpoonup> (Scala) "scala.collection.immutable.Map().withDefaultValue((_))"
| constant "finfun_update" \<rightharpoonup> (Scala) "_ + (_ -> _)"
| constant "finfun_apply" \<rightharpoonup> (Scala) "_((_))"
| constant "finfun_to_list" \<rightharpoonup> (Scala) "_.keySet.toList"
declare finfun_to_list_const_code [code del]
declare finfun_to_list_update_code [code del]
definition mismatched_updates :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
"mismatched_updates t1 t2 = (\<exists>r \<in> set (map fst (Updates t1)). r \<notin> set (map fst (Updates t2)))"
lemma [code]:
"directly_subsumes e1 e2 s1 s2 t1 t2 = (if t1 = t2 then True else dirty_directly_subsumes e1 e2 s1 s2 t1 t2)"
by (simp add: directly_subsumes_reflexive dirty_directly_subsumes_def)
export_code
(* Essentials *)
try_heuristics_check
learn
infer_with_log
nondeterministic
make_pta
AExp.enumerate_vars
(* Logical connectives *)
gAnd
gOr
gNot
Lt
Le
Ge
Ne
(* Scoring functions *)
naive_score
naive_score_eq_bonus
exactly_equal
naive_score_outputs
naive_score_comprehensive
naive_score_comprehensive_eq_high
leaves
(* Heuristics *)
same_register
insert_increment_2
heuristic_1
heuristic_2
distinguish
weak_subsumption
lob
(* Nondeterminism metrics *)
nondeterministic_pairs
nondeterministic_pairs_labar
nondeterministic_pairs_labar_dest
(* Utilities *)
min
max
drop_pta_guards
test_log
iefsm2dot
efsm2dot
guards2sal
guards2sal_num
fold_In
max_int
enumerate_vars
derestrict
in Scala
(* file "../../inference-tool/src/main/scala/inference/Inference.scala" *)
end

View File

@ -0,0 +1,148 @@
chapter\<open>Output\<close>
text\<open>This chapter provides two different output formats for EFSMs.\<close>
section\<open>Graphical Output\<close>
text\<open>It is often more intuitive and aesthetically pleasing to view EFSMs graphically. DOT is a graph
layout engine which converts textual representations of graphs to more useful formats, such as SVG
or PNG representations. This theory defines functions to convert arbitrary EFSMs to DOT for easier
viewing. Here, transitions use the syntactic sugar presented in \cite{foster2018} such that they
take the form $\textit{label}:\textit{arity}[g_1, \ldots, g_g]/f_1, \ldots, f_f[u_1, \ldots, u_u]$.\<close>
theory EFSM_Dot
imports Inference
begin
fun string_of_digit :: "nat \<Rightarrow> String.literal" where
"string_of_digit n = (
if n = 0 then (STR ''0'')
else if n = 1 then (STR ''1'')
else if n = 2 then (STR ''2'')
else if n = 3 then (STR ''3'')
else if n = 4 then (STR ''4'')
else if n = 5 then (STR ''5'')
else if n = 6 then (STR ''6'')
else if n = 7 then (STR ''7'')
else if n = 8 then (STR ''8'')
else (STR ''9''))"
abbreviation newline :: String.literal where
"newline \<equiv> STR ''\010''"
abbreviation quote :: String.literal where
"quote \<equiv> STR ''\"''"
definition shows_string :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal"
where
"shows_string = (+)"
fun showsp_nat :: "String.literal \<Rightarrow> nat \<Rightarrow> String.literal \<Rightarrow> String.literal"
where
"showsp_nat p n =
(if n < 10 then shows_string (string_of_digit n)
else showsp_nat p (n div 10) o shows_string (string_of_digit (n mod 10)))"
declare showsp_nat.simps [simp del]
definition showsp_int :: "String.literal \<Rightarrow> int \<Rightarrow> String.literal \<Rightarrow> String.literal"
where
"showsp_int p i =
(if i < 0 then shows_string STR ''-'' o showsp_nat p (nat (- i)) else showsp_nat p (nat i))"
definition "show_int n \<equiv> showsp_int ((STR '''')) n ((STR ''''))"
definition "show_nat n \<equiv> showsp_nat ((STR '''')) n ((STR ''''))"
definition replace_backslash :: "String.literal \<Rightarrow> String.literal" where
"replace_backslash s = String.implode (fold (@) (map (\<lambda>x. if x = CHR 0x5c then [CHR 0x5c,CHR 0x5c] else [x]) (String.explode s)) '''')"
code_printing
constant replace_backslash \<rightharpoonup> (Scala) "_.replace(\"\\\\\", \"\\\\\\\\\")"
fun value2dot :: "value \<Rightarrow> String.literal" where
"value2dot (value.Str s) = quote + replace_backslash s + quote" |
"value2dot (Num n) = show_int n"
fun vname2dot :: "vname \<Rightarrow> String.literal" where
"vname2dot (vname.I n) = STR ''i<sub>''+(show_nat (n))+STR ''</sub>''" |
"vname2dot (R n) = STR ''r<sub>''+(show_nat n)+STR ''</sub>''"
fun aexp2dot :: "vname aexp \<Rightarrow> String.literal" where
"aexp2dot (L v) = value2dot v" |
"aexp2dot (V v) = vname2dot v" |
"aexp2dot (Plus a1 a2) = (aexp2dot a1)+STR '' + ''+(aexp2dot a2)" |
"aexp2dot (Minus a1 a2) = (aexp2dot a1)+STR '' - ''+(aexp2dot a2)" |
"aexp2dot (Times a1 a2) = (aexp2dot a1)+STR '' &times; ''+(aexp2dot a2)"
fun join :: "String.literal list \<Rightarrow> String.literal \<Rightarrow> String.literal" where
"join [] _ = (STR '''')" |
"join [a] _ = a" |
"join (h#t) s = h+s+(join t s)"
definition show_nats :: "nat list \<Rightarrow> String.literal" where
"show_nats l = join (map show_nat l) STR '', ''"
fun gexp2dot :: "vname gexp \<Rightarrow> String.literal" where
"gexp2dot (GExp.Bc True) = (STR ''True'')" |
"gexp2dot (GExp.Bc False) = (STR ''False'')" |
"gexp2dot (GExp.Eq a1 a2) = (aexp2dot a1)+STR '' = ''+(aexp2dot a2)" |
"gexp2dot (GExp.Gt a1 a2) = (aexp2dot a1)+STR '' &gt; ''+(aexp2dot a2)" |
"gexp2dot (GExp.In v l) = (vname2dot v)+STR ''&isin;{''+(join (map value2dot l) STR '', '')+STR ''}''" |
"gexp2dot (Nor g1 g2) = STR ''!(''+(gexp2dot g1)+STR ''&or;''+(gexp2dot g2)+STR '')''"
primrec guards2dot_aux :: "vname gexp list \<Rightarrow> String.literal list" where
"guards2dot_aux [] = []" |
"guards2dot_aux (h#t) = (gexp2dot h)#(guards2dot_aux t)"
lemma gexp2dot_aux_code [code]: "guards2dot_aux l = map gexp2dot l"
by (induct l, simp_all)
primrec updates2dot_aux :: "update_function list \<Rightarrow> String.literal list" where
"updates2dot_aux [] = []" |
"updates2dot_aux (h#t) = ((vname2dot (R (fst h)))+STR '' := ''+(aexp2dot (snd h)))#(updates2dot_aux t)"
lemma updates2dot_aux_code [code]:
"updates2dot_aux l = map (\<lambda>(r, u). (vname2dot (R r))+STR '' := ''+(aexp2dot u)) l"
by (induct l, auto)
primrec outputs2dot :: "output_function list \<Rightarrow> nat \<Rightarrow> String.literal list" where
"outputs2dot [] _ = []" |
"outputs2dot (h#t) n = ((STR ''o<sub>''+(show_nat n))+STR ''</sub> := ''+(aexp2dot h))#(outputs2dot t (n+1))"
fun updates2dot :: "update_function list \<Rightarrow> String.literal" where
"updates2dot [] = (STR '''')" |
"updates2dot a = STR ''&#91;''+(join (updates2dot_aux a) STR '', '')+STR ''&#93;''"
fun guards2dot :: "vname gexp list \<Rightarrow> String.literal" where
"guards2dot [] = (STR '''')" |
"guards2dot a = STR ''&#91;''+(join (guards2dot_aux a) STR '', '')+STR ''&#93;''"
definition latter2dot :: "transition \<Rightarrow> String.literal" where
"latter2dot t = (let l = (join (outputs2dot (Outputs t) 1) STR '', '')+(updates2dot (Updates t)) in (if l = (STR '''') then (STR '''') else STR ''/''+l))"
definition transition2dot :: "transition \<Rightarrow> String.literal" where
"transition2dot t = (Label t)+STR '':''+(show_nat (Arity t))+(guards2dot (Guards t))+(latter2dot t)"
definition efsm2dot :: "transition_matrix \<Rightarrow> String.literal" where
"efsm2dot e = STR ''digraph EFSM{''+newline+
STR '' graph [rankdir=''+quote+(STR ''LR'')+quote+STR '', fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+
STR '' node [color=''+quote+(STR ''black'')+quote+STR '', fillcolor=''+quote+(STR ''white'')+quote+STR '', shape=''+quote+(STR ''circle'')+quote+STR '', style=''+quote+(STR ''filled'')+quote+STR '', fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+
STR '' edge [fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+newline+
STR '' s0[fillcolor=''+quote+STR ''gray''+quote+STR '', label=<s<sub>0</sub>>];''+newline+
(join (map (\<lambda>s. STR '' s''+show_nat s+STR ''[label=<s<sub>'' +show_nat s+ STR ''</sub>>];'') (sorted_list_of_fset (EFSM.S e - {|0|}))) (newline))+newline+newline+
(join ((map (\<lambda>((from, to), t). STR '' s''+(show_nat from)+STR ''->s''+(show_nat to)+STR ''[label=<<i>''+(transition2dot t)+STR ''</i>>];'') (sorted_list_of_fset e))) newline)+newline+
STR ''}''"
definition iefsm2dot :: "iEFSM \<Rightarrow> String.literal" where
"iefsm2dot e = STR ''digraph EFSM{''+newline+
STR '' graph [rankdir=''+quote+(STR ''LR'')+quote+STR '', fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+
STR '' node [color=''+quote+(STR ''black'')+quote+STR '', fillcolor=''+quote+(STR ''white'')+quote+STR '', shape=''+quote+(STR ''circle'')+quote+STR '', style=''+quote+(STR ''filled'')+quote+STR '', fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+
STR '' edge [fontname=''+quote+STR ''Latin Modern Math''+quote+STR ''];''+newline+newline+
STR '' s0[fillcolor=''+quote+STR ''gray''+quote+STR '', label=<s<sub>0</sub>>];''+newline+
(join (map (\<lambda>s. STR '' s''+show_nat s+STR ''[label=<s<sub>'' +show_nat s+ STR ''</sub>>];'') (sorted_list_of_fset (S e - {|0|}))) (newline))+newline+newline+
(join ((map (\<lambda>(uid, (from, to), t). STR '' s''+(show_nat from)+STR ''->s''+(show_nat to)+STR ''[label=<<i> [''+show_nats (sort uid)+STR '']''+(transition2dot t)+STR ''</i>>];'') (sorted_list_of_fset e))) newline)+newline+
STR ''}''"
abbreviation newline_str :: string where
"newline_str \<equiv> ''\010''"
abbreviation quote_str :: string where
"quote_str \<equiv> ''0x22''"
end

View File

@ -0,0 +1,588 @@
chapter\<open>EFSM Inference\<close>
text\<open>This chapter presents the definitions necessary for EFSM inference by state-merging.\<close>
section\<open>Inference by State-Merging\<close>
text\<open>This theory sets out the key definitions for the inference of EFSMs from system traces.\<close>
theory Inference
imports
Subsumption
"Extended_Finite_State_Machines.Transition_Lexorder"
"HOL-Library.Product_Lexorder"
begin
declare One_nat_def [simp del]
subsection\<open>Transition Identifiers\<close>
text\<open>We first need to define the \texttt{iEFSM} data type which assigns each transition a unique identity.
This is necessary because transitions may not occur uniquely in an EFSM. Assigning transitions a unique
identifier enables us to look up the origin and destination states of transitions without having to
pass them around in the inference functions.\<close>
type_synonym tid = nat
type_synonym tids = "tid list"
type_synonym iEFSM = "(tids \<times> (cfstate \<times> cfstate) \<times> transition) fset"
definition origin :: "tids \<Rightarrow> iEFSM \<Rightarrow> nat" where
"origin uid t = fst (fst (snd (fthe_elem (ffilter (\<lambda>x. set uid \<subseteq> set (fst x)) t))))"
definition dest :: "tids \<Rightarrow> iEFSM \<Rightarrow> nat" where
"dest uid t = snd (fst (snd (fthe_elem (ffilter (\<lambda>x. set uid \<subseteq> set (fst x)) t))))"
definition get_by_id :: "iEFSM \<Rightarrow> tid \<Rightarrow> transition" where
"get_by_id e uid = (snd \<circ> snd) (fthe_elem (ffilter (\<lambda>(tids, _). uid \<in> set tids) e))"
definition get_by_ids :: "iEFSM \<Rightarrow> tids \<Rightarrow> transition" where
"get_by_ids e uid = (snd \<circ> snd) (fthe_elem (ffilter (\<lambda>(tids, _). set uid \<subseteq> set tids) e))"
definition uids :: "iEFSM \<Rightarrow> nat fset" where
"uids e = ffUnion (fimage (fset_of_list \<circ> fst) e)"
definition max_uid :: "iEFSM \<Rightarrow> nat option" where
"max_uid e = (let uids = uids e in if uids = {||} then None else Some (fMax uids))"
definition tm :: "iEFSM \<Rightarrow> transition_matrix" where
"tm e = fimage snd e"
definition all_regs :: "iEFSM \<Rightarrow> nat set" where
"all_regs e = EFSM.all_regs (tm e)"
definition max_reg :: "iEFSM \<Rightarrow> nat option" where
"max_reg e = EFSM.max_reg (tm e)"
definition "max_reg_total e = (case max_reg e of None \<Rightarrow> 0 | Some r \<Rightarrow> r)"
definition max_output :: "iEFSM \<Rightarrow> nat" where
"max_output e = EFSM.max_output (tm e)"
definition max_int :: "iEFSM \<Rightarrow> int" where
"max_int e = EFSM.max_int (tm e)"
definition S :: "iEFSM \<Rightarrow> nat fset" where
"S m = (fimage (\<lambda>(uid, (s, s'), t). s) m) |\<union>| fimage (\<lambda>(uid, (s, s'), t). s') m"
lemma S_alt: "S t = EFSM.S (tm t)"
apply (simp add: S_def EFSM.S_def tm_def)
by force
lemma to_in_S:
"(\<exists>to from uid. (uid, (from, to), t) |\<in>| xb \<longrightarrow> to |\<in>| S xb)"
apply (simp add: S_def)
by blast
lemma from_in_S:
"(\<exists>to from uid. (uid, (from, to), t) |\<in>| xb \<longrightarrow> from |\<in>| S xb)"
apply (simp add: S_def)
by blast
subsection\<open>Building the PTA\<close>
text\<open>The first step in EFSM inference is to construct a PTA from the observed traces in the same way
as for classical FSM inference. Beginning with the empty EFSM, we iteratively attempt to walk each
observed trace in the model. When we reach a point where there is no available transition, one is
added. For classical FSMs, this is simply an atomic label. EFSMs deal with data, so we need to add
guards which test for the observed input values and outputs which produce the observed values.\<close>
primrec make_guard :: "value list \<Rightarrow> nat \<Rightarrow> vname gexp list" where
"make_guard [] _ = []" |
"make_guard (h#t) n = (gexp.Eq (V (vname.I n)) (L h))#(make_guard t (n+1))"
primrec make_outputs :: "value list \<Rightarrow> output_function list" where
"make_outputs [] = []" |
"make_outputs (h#t) = (L h)#(make_outputs t)"
definition max_uid_total :: "iEFSM \<Rightarrow> nat" where
"max_uid_total e = (case max_uid e of None \<Rightarrow> 0 | Some u \<Rightarrow> u)"
definition add_transition :: "iEFSM \<Rightarrow> cfstate \<Rightarrow> label \<Rightarrow> value list \<Rightarrow> value list \<Rightarrow> iEFSM" where
"add_transition e s label inputs outputs = finsert ([max_uid_total e + 1], (s, (maxS (tm e))+1), \<lparr>Label=label, Arity=length inputs, Guards=(make_guard inputs 0), Outputs=(make_outputs outputs), Updates=[]\<rparr>) e"
fun make_branch :: "iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> iEFSM" where
"make_branch e _ _ [] = e" |
"make_branch e s r ((label, inputs, outputs)#t) =
(case (step (tm e) s r label inputs) of
Some (transition, s', outputs', updated) \<Rightarrow>
if outputs' = (map Some outputs) then
make_branch e s' updated t
else
make_branch (add_transition e s label inputs outputs) ((maxS (tm e))+1) r t |
None \<Rightarrow>
make_branch (add_transition e s label inputs outputs) ((maxS (tm e))+1) r t
)"
primrec make_pta_aux :: "log \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"make_pta_aux [] e = e" |
"make_pta_aux (h#t) e = make_pta_aux t (make_branch e 0 <> h)"
definition "make_pta log = make_pta_aux log {||}"
lemma make_pta_aux_fold [code]:
"make_pta_aux l e = fold (\<lambda>h e. make_branch e 0 <> h) l e"
by(induct l arbitrary: e, auto)
subsection\<open>Integrating Heuristics\<close>
text\<open>A key contribution of the inference technique presented in \cite{foster2019} is the ability to
introduce \emph{internal variables} to the model to generalise behaviours and allow transitions to
be merged. This is done by providing the inference technique with a set of \emph{heuristics}. The
aim here is not to create a ``one size fits all'' magic oracle, rather to recognise particular
\emph{data usage patterns} which can be abstracted.\<close>
type_synonym update_modifier = "tids \<Rightarrow> tids \<Rightarrow> cfstate \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> iEFSM option"
definition null_modifier :: update_modifier where
"null_modifier f _ _ _ _ _ _ = None"
definition replace_transition :: "iEFSM \<Rightarrow> tids \<Rightarrow> transition \<Rightarrow> iEFSM" where
"replace_transition e uid new = (fimage (\<lambda>(uids, (from, to), t). if set uid \<subseteq> set uids then (uids, (from, to), new) else (uids, (from, to), t)) e)"
definition replace_all :: "iEFSM \<Rightarrow> tids list \<Rightarrow> transition \<Rightarrow> iEFSM" where
"replace_all e ids new = fold (\<lambda>id acc. replace_transition acc id new) ids e"
definition replace_transitions :: "iEFSM \<Rightarrow> (tids \<times> transition) list \<Rightarrow> iEFSM" where
"replace_transitions e ts = fold (\<lambda>(uid, new) acc. replace_transition acc uid new) ts e"
primrec try_heuristics_check :: "(transition_matrix \<Rightarrow> bool) \<Rightarrow> update_modifier list \<Rightarrow> update_modifier" where
"try_heuristics_check _ [] = null_modifier" |
"try_heuristics_check check (h#t) = (\<lambda>a b c d e f ch.
case h a b c d e f ch of
Some e' \<Rightarrow> Some e' |
None \<Rightarrow> (try_heuristics_check check t) a b c d e f ch
)"
subsection\<open>Scoring State Merges\<close>
text\<open>To tackle the state merging challenge, we need some means of determining which states are
compatible for merging. Because states are merged pairwise, we additionally require a way of
ordering the state merges. The potential merges are then sorted highest to lowest according to this
score such that we can merge states in order of their merge score.
We want to sort first by score (highest to lowest) and then by state pairs (lowest to highest) so we
endup merging the states with the highest scores first and then break ties by those state pairs
which are closest to the origin.\<close>
record score =
Score :: nat
S1 :: cfstate
S2 :: cfstate
instantiation score_ext :: (linorder) linorder begin
definition less_score_ext :: "'a::linorder score_ext \<Rightarrow> 'a score_ext \<Rightarrow> bool" where
"less_score_ext t1 t2 = ((Score t2, S1 t1, S2 t1, more t1) < (Score t1, S1 t2, S2 t2, more t2) )"
definition less_eq_score_ext :: "'a::linorder score_ext \<Rightarrow> 'a::linorder score_ext \<Rightarrow> bool" where
"less_eq_score_ext s1 s2 = (s1 < s2 \<or> s1 = s2)"
instance
apply standard prefer 5
unfolding less_score_ext_def less_eq_score_ext_def
using score.equality apply fastforce
by auto
end
type_synonym scoreboard = "score fset"
type_synonym strategy = "tids \<Rightarrow> tids \<Rightarrow> iEFSM \<Rightarrow> nat"
definition outgoing_transitions :: "cfstate \<Rightarrow> iEFSM \<Rightarrow> (cfstate \<times> transition \<times> tids) fset" where
"outgoing_transitions s e = fimage (\<lambda>(uid, (from, to), t'). (to, t', uid)) ((ffilter (\<lambda>(uid, (origin, dest), t). origin = s)) e)"
primrec paths_of_length :: "nat \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> tids list fset" where
"paths_of_length 0 _ _ = {|[]|}" |
"paths_of_length (Suc m) e s = (
let
outgoing = outgoing_transitions s e;
paths = ffUnion (fimage (\<lambda>(d, t, id). fimage (\<lambda>p. id#p) (paths_of_length m e d)) outgoing)
in
ffilter (\<lambda>l. length l = Suc m) paths
)"
lemma paths_of_length_1: "paths_of_length 1 e s = fimage (\<lambda>(d, t, id). [id]) (outgoing_transitions s e)"
apply (simp add: One_nat_def)
apply (simp add: outgoing_transitions_def comp_def One_nat_def[symmetric])
apply (rule fBall_ffilter2)
defer
apply (simp add: ffilter_def ffUnion_def fBall_def Abs_fset_inverse)
apply auto[1]
apply (simp add: ffilter_def ffUnion_def fBall_def Abs_fset_inverse fset_both_sides)
by force
fun step_score :: "(tids \<times> tids) list \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> nat" where
"step_score [] _ _ = 0" |
"step_score ((id1, id2)#t) e s = (
let score = s id1 id2 e in
if score = 0 then
0
else
score + (step_score t e s)
)"
lemma step_score_foldr [code]:
"step_score xs e s = foldr (\<lambda>(id1, id2) acc. let score = s id1 id2 e in
if score = 0 then
0
else
score + acc) xs 0"
proof(induct xs)
case Nil
then show ?case
by simp
next
case (Cons a xs)
then show ?case
apply (cases a, clarify)
by (simp add: Let_def)
qed
definition score_from_list :: "tids list fset \<Rightarrow> tids list fset \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> nat" where
"score_from_list P1 P2 e s = (
let
pairs = fimage (\<lambda>(l1, l2). zip l1 l2) (P1 |\<times>| P2);
scored_pairs = fimage (\<lambda>l. step_score l e s) pairs
in
fSum scored_pairs
)"
definition k_score :: "nat \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> scoreboard" where
"k_score k e strat = (
let
states = S e;
pairs_to_score = (ffilter (\<lambda>(x, y). x < y) (states |\<times>| states));
paths = fimage (\<lambda>(s1, s2). (s1, s2, paths_of_length k e s1, paths_of_length k e s2)) pairs_to_score;
scores = fimage (\<lambda>(s1, s2, p1, p2). \<lparr>Score = score_from_list p1 p2 e strat, S1 = s1, S2 = s2\<rparr>) paths
in
ffilter (\<lambda>x. Score x > 0) scores
)"
definition score_state_pair :: "strategy \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> cfstate \<Rightarrow> nat" where
"score_state_pair strat e s1 s2 = (
let
T1 = outgoing_transitions s1 e;
T2 = outgoing_transitions s2 e
in
fSum (fimage (\<lambda>((_, _, t1), (_, _, t2)). strat t1 t2 e) (T1 |\<times>| T2))
)"
definition score_1 :: "iEFSM \<Rightarrow> strategy \<Rightarrow> scoreboard" where
"score_1 e strat = (
let
states = S e;
pairs_to_score = (ffilter (\<lambda>(x, y). x < y) (states |\<times>| states));
scores = fimage (\<lambda>(s1, s2). \<lparr>Score = score_state_pair strat e s1 s2, S1 = s1, S2 = s2\<rparr>) pairs_to_score
in
ffilter (\<lambda>x. Score x > 0) scores
)"
lemma score_1: "score_1 e s = k_score 1 e s"
proof-
have fprod_fimage:
"\<And>a b. ((\<lambda>(_, _, id). [id]) |`| a |\<times>| (\<lambda>(_, _, id). [id]) |`| b) =
fimage (\<lambda>((_, _, id1), (_, _, id2)). ([id1], [id2])) (a |\<times>| b)"
apply (simp add: fimage_def fprod_def Abs_fset_inverse fset_both_sides)
by force
show ?thesis
apply (simp add: score_1_def k_score_def Let_def comp_def)
apply (rule arg_cong[of _ _ "ffilter (\<lambda>x. 0 < Score x)"])
apply (rule fun_cong[of _ _ "(Inference.S e |\<times>| Inference.S e)"])
apply (rule ext)
subgoal for x
apply (rule fun_cong[of _ _ "ffilter (\<lambda>a. case a of (a, b) \<Rightarrow> a < b) x"])
apply (rule arg_cong[of _ _ fimage])
apply (rule ext)
subgoal for x
apply (case_tac x)
apply simp
apply (simp add: paths_of_length_1)
apply (simp add: score_state_pair_def Let_def score_from_list_def comp_def)
subgoal for a b
apply (rule arg_cong[of _ _ fSum])
apply (simp add: fprod_fimage)
apply (rule fun_cong[of _ _ "(outgoing_transitions a e |\<times>| outgoing_transitions b e)"])
apply (rule arg_cong[of _ _ fimage])
apply (rule ext)
apply clarify
by (simp add: Let_def)
done
done
done
qed
fun bool2nat :: "bool \<Rightarrow> nat" where
"bool2nat True = 1" |
"bool2nat False = 0"
definition score_transitions :: "transition \<Rightarrow> transition \<Rightarrow> nat" where
"score_transitions t1 t2 = (
if Label t1 = Label t2 \<and> Arity t1 = Arity t2 \<and> length (Outputs t1) = length (Outputs t2) then
1 + bool2nat (t1 = t2) + card ((set (Guards t2)) \<inter> (set (Guards t2))) + card ((set (Updates t2)) \<inter> (set (Updates t2))) + card ((set (Outputs t2)) \<inter> (set (Outputs t2)))
else
0
)"
subsection\<open>Merging States\<close>
definition merge_states_aux :: "nat \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"merge_states_aux s1 s2 e = fimage (\<lambda>(uid, (origin, dest), t). (uid, (if origin = s1 then s2 else origin , if dest = s1 then s2 else dest), t)) e"
definition merge_states :: "nat \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"merge_states x y t = (if x > y then merge_states_aux x y t else merge_states_aux y x t)"
lemma merge_states_symmetry: "merge_states x y t = merge_states y x t"
by (simp add: merge_states_def)
lemma merge_state_self: "merge_states s s t = t"
apply (simp add: merge_states_def merge_states_aux_def)
by force
lemma merge_states_self_simp [code]:
"merge_states x y t = (if x = y then t else if x > y then merge_states_aux x y t else merge_states_aux y x t)"
apply (simp add: merge_states_def merge_states_aux_def)
by force
subsection\<open>Resolving Nondeterminism\<close>
text\<open>Because EFSM transitions are not simply atomic actions, duplicated behaviours cannot be
resolved into a single transition by simply merging destination states, as it can in classical FSM
inference. It is now possible for attempts to resolve the nondeterminism introduced by merging
states to fail, meaning that two states which initially seemed compatible cannot actually be merged.
This is not the case in classical FSM inference.\<close>
type_synonym nondeterministic_pair = "(cfstate \<times> (cfstate \<times> cfstate) \<times> ((transition \<times> tids) \<times> (transition \<times> tids)))"
definition state_nondeterminism :: "nat \<Rightarrow> (cfstate \<times> transition \<times> tids) fset \<Rightarrow> nondeterministic_pair fset" where
"state_nondeterminism og nt = (if size nt < 2 then {||} else ffUnion (fimage (\<lambda>x. let (dest, t) = x in fimage (\<lambda>y. let (dest', t') = y in (og, (dest, dest'), (t, t'))) (nt - {|x|})) nt))"
lemma state_nondeterminism_empty [simp]: "state_nondeterminism a {||} = {||}"
by (simp add: state_nondeterminism_def ffilter_def Set.filter_def)
lemma state_nondeterminism_singledestn [simp]: "state_nondeterminism a {|x|} = {||}"
by (simp add: state_nondeterminism_def ffilter_def Set.filter_def)
(* For each state, get its outgoing transitions and see if there's any nondeterminism there *)
definition nondeterministic_pairs :: "iEFSM \<Rightarrow> nondeterministic_pair fset" where
"nondeterministic_pairs t = ffilter (\<lambda>(_, _, (t, _), (t', _)). Label t = Label t' \<and> Arity t = Arity t' \<and> choice t t') (ffUnion (fimage (\<lambda>s. state_nondeterminism s (outgoing_transitions s t)) (S t)))"
definition nondeterministic_pairs_labar_dest :: "iEFSM \<Rightarrow> nondeterministic_pair fset" where
"nondeterministic_pairs_labar_dest t = ffilter
(\<lambda>(_, (d, d'), (t, _), (t', _)).
Label t = Label t' \<and> Arity t = Arity t' \<and> (choice t t' \<or> (Outputs t = Outputs t' \<and> d = d')))
(ffUnion (fimage (\<lambda>s. state_nondeterminism s (outgoing_transitions s t)) (S t)))"
definition nondeterministic_pairs_labar :: "iEFSM \<Rightarrow> nondeterministic_pair fset" where
"nondeterministic_pairs_labar t = ffilter
(\<lambda>(_, (d, d'), (t, _), (t', _)).
Label t = Label t' \<and> Arity t = Arity t' \<and> (choice t t' \<or> Outputs t = Outputs t'))
(ffUnion (fimage (\<lambda>s. state_nondeterminism s (outgoing_transitions s t)) (S t)))"
definition deterministic :: "iEFSM \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> bool" where
"deterministic t np = (np t = {||})"
definition nondeterministic :: "iEFSM \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> bool" where
"nondeterministic t np = (\<not> deterministic t np)"
definition insert_transition :: "tids \<Rightarrow> cfstate \<Rightarrow> cfstate \<Rightarrow> transition \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"insert_transition uid from to t e = (
if \<nexists>(uid, (from', to'), t') |\<in>| e. from = from' \<and> to = to' \<and> t = t' then
finsert (uid, (from, to), t) e
else
fimage (\<lambda>(uid', (from', to'), t').
if from = from' \<and> to = to' \<and> t = t' then
(List.union uid' uid, (from', to'), t')
else
(uid', (from', to'), t')
) e
)"
definition make_distinct :: "iEFSM \<Rightarrow> iEFSM" where
"make_distinct e = ffold_ord (\<lambda>(uid, (from, to), t) acc. insert_transition uid from to t acc) e {||}"
\<comment> \<open>When we replace one transition with another, we need to merge their uids to keep track of which\<close>
\<comment> \<open>transition accounts for which action in the original traces \<close>
definition merge_transitions_aux :: "iEFSM \<Rightarrow> tids \<Rightarrow> tids \<Rightarrow> iEFSM" where
"merge_transitions_aux e oldID newID = (let
(uids1, (origin, dest), old) = fthe_elem (ffilter (\<lambda>(uids, _). oldID = uids) e);
(uids2, (origin, dest), new) = fthe_elem (ffilter (\<lambda>(uids, _). newID = uids) e) in
make_distinct (finsert (List.union uids1 uids2, (origin, dest), new) (e - {|(uids1, (origin, dest), old), (uids2, (origin, dest), new)|}))
)"
(* merge_transitions - Try dest merge transitions t1 and t2 dest help resolve nondeterminism in
newEFSM. If either subsumes the other directly then the subsumed transition
can simply be replaced with the subsuming one, else we try dest apply the
modifier function dest resolve nondeterminism that way. *)
(* @param oldEFSM - the EFSM before merging the states which caused the nondeterminism *)
(* @param preDestMerge - the EFSM after merging the states which caused the nondeterminism *)
(* @param newEFSM - the current EFSM with nondeterminism *)
(* @param t1 - a transition dest be merged with t2 *)
(* @param u1 - the unique identifier of t1 *)
(* @param t2 - a transition dest be merged with t1 *)
(* @param u2 - the unique identifier of t2 *)
(* @param modifier - an update modifier function which tries dest generalise transitions *)
definition merge_transitions :: "(cfstate \<times> cfstate) set \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> transition \<Rightarrow> tids \<Rightarrow> transition \<Rightarrow> tids \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> iEFSM option" where
"merge_transitions failedMerges oldEFSM preDestMerge destMerge t1 u1 t2 u2 modifier check = (
if \<forall>id \<in> set u1. directly_subsumes (tm oldEFSM) (tm destMerge) (origin [id] oldEFSM) (origin u1 destMerge) t2 t1 then
\<comment> \<open>Replace t1 with t2\<close>
Some (merge_transitions_aux destMerge u1 u2)
else if \<forall>id \<in> set u2. directly_subsumes (tm oldEFSM) (tm destMerge) (origin [id] oldEFSM) (origin u2 destMerge) t1 t2 then
\<comment> \<open>Replace t2 with t1\<close>
Some (merge_transitions_aux destMerge u2 u1)
else
case modifier u1 u2 (origin u1 destMerge) destMerge preDestMerge oldEFSM check of
None \<Rightarrow> None |
Some e \<Rightarrow> Some (make_distinct e)
)"
definition outgoing_transitions_from :: "iEFSM \<Rightarrow> cfstate \<Rightarrow> transition fset" where
"outgoing_transitions_from e s = fimage (\<lambda>(_, _, t). t) (ffilter (\<lambda>(_, (orig, _), _). orig = s) e)"
definition order_nondeterministic_pairs :: "nondeterministic_pair fset \<Rightarrow> nondeterministic_pair list" where
"order_nondeterministic_pairs s = map snd (sorted_list_of_fset (fimage (\<lambda>s. let (_, _, (t1, _), (t2, _)) = s in (score_transitions t1 t2, s)) s))"
(* resolve_nondeterminism - tries dest resolve nondeterminism in a given iEFSM *)
(* @param ((from, (dest1, dest2), ((t1, u1), (t2, u2)))#ss) - a list of nondeterministic pairs where
from - nat - the state from which t1 and t2 eminate
dest1 - nat - the destination state of t1
dest2 - nat - the destination state of t2
t1 - transition - a transition dest be merged with t2
t2 - transition - a transition dest be merged with t1
u1 - nat - the unique identifier of t1
u2 - nat - the unique identifier of t2
ss - list - the rest of the list *)
(* @param oldEFSM - the EFSM before merging the states which caused the nondeterminism *)
(* @param newEFSM - the current EFSM with nondeterminism *)
(* @param m - an update modifier function which tries dest generalise transitions *)
(* @param check - a function which takes an EFSM and returns a bool dest ensure that certain
properties hold in the new iEFSM *)
function resolve_nondeterminism :: "(cfstate \<times> cfstate) set \<Rightarrow> nondeterministic_pair list \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> (iEFSM option \<times> (cfstate \<times> cfstate) set)" where
"resolve_nondeterminism failedMerges [] _ newEFSM _ check np = (
if deterministic newEFSM np \<and> check (tm newEFSM) then Some newEFSM else None, failedMerges
)" |
"resolve_nondeterminism failedMerges ((from, (dest1, dest2), ((t1, u1), (t2, u2)))#ss) oldEFSM newEFSM m check np = (
if (dest1, dest2) \<in> failedMerges \<or> (dest2, dest1) \<in> failedMerges then
(None, failedMerges)
else
let destMerge = merge_states dest1 dest2 newEFSM in
case merge_transitions failedMerges oldEFSM newEFSM destMerge t1 u1 t2 u2 m check of
None \<Rightarrow> resolve_nondeterminism (insert (dest1, dest2) failedMerges) ss oldEFSM newEFSM m check np |
Some new \<Rightarrow> (
let newScores = order_nondeterministic_pairs (np new) in
if (size new, size (S new), size (newScores)) < (size newEFSM, size (S newEFSM), size ss) then
case resolve_nondeterminism failedMerges newScores oldEFSM new m check np of
(Some new', failedMerges) \<Rightarrow> (Some new', failedMerges) |
(None, failedMerges) \<Rightarrow> resolve_nondeterminism (insert (dest1, dest2) failedMerges) ss oldEFSM newEFSM m check np
else
(None, failedMerges)
)
)"
apply (clarify, metis neq_Nil_conv prod_cases3 surj_pair)
by auto
termination
by (relation "measures [\<lambda>(_, _, _, newEFSM, _). size newEFSM,
\<lambda>(_, _, _, newEFSM, _). size (S newEFSM),
\<lambda>(_, ss, _, _, _). size ss]", auto)
subsection\<open>EFSM Inference\<close>
(* Merge - tries dest merge two states in a given iEFSM and resolve the resulting nondeterminism *)
(* @param e - an iEFSM *)
(* @param s1 - a state dest be merged with s2 *)
(* @param s2 - a state dest be merged with s1 *)
(* @param m - an update modifier function which tries dest generalise transitions *)
(* @param check - a function which takes an EFSM and returns a bool dest ensure that certain
properties hold in the new iEFSM *)
definition merge :: "(cfstate \<times> cfstate) set \<Rightarrow> iEFSM \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> (iEFSM option \<times> (cfstate \<times> cfstate) set)" where
"merge failedMerges e s1 s2 m check np = (
if s1 = s2 \<or> (s1, s2) \<in> failedMerges \<or> (s2, s1) \<in> failedMerges then
(None, failedMerges)
else
let e' = make_distinct (merge_states s1 s2 e) in
resolve_nondeterminism failedMerges (order_nondeterministic_pairs (np e')) e e' m check np
)"
(* inference_step - attempt dest carry out a single step of the inference process by merging the *)
(* @param e - an iEFSM dest be generalised *)
(* @param ((s, s1, s2)#t) - a list of triples of the form (score, state, state) dest be merged *)
(* @param m - an update modifier function which tries dest generalise transitions *)
(* @param check - a function which takes an EFSM and returns a bool dest ensure that certain
properties hold in the new iEFSM *)
function inference_step :: "(cfstate \<times> cfstate) set \<Rightarrow> iEFSM \<Rightarrow> score fset \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> (iEFSM option \<times> (cfstate \<times> cfstate) set)" where
"inference_step failedMerges e s m check np = (
if s = {||} then (None, failedMerges) else
let
h = fMin s;
t = s - {|h|}
in
case merge failedMerges e (S1 h) (S2 h) m check np of
(Some new, failedMerges) \<Rightarrow> (Some new, failedMerges) |
(None, failedMerges) \<Rightarrow> inference_step (insert ((S1 h), (S2 h)) failedMerges) e t m check np
)"
by auto
termination
apply (relation "measures [\<lambda>(_, _, s, _, _, _). size s]")
apply simp
by (simp add: card_minus_fMin)
(* Takes an iEFSM and iterates inference_step until no further states can be successfully merged *)
(* @param e - an iEFSM dest be generalised *)
(* @param r - a strategy dest identify and prioritise pairs of states dest merge *)
(* @param m - an update modifier function which tries dest generalise transitions *)
(* @param check - a function which takes an EFSM and returns a bool dest ensure that certain
properties hold in the new iEFSM *)
function infer :: "(cfstate \<times> cfstate) set \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> strategy \<Rightarrow> update_modifier \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"infer failedMerges k e r m check np = (
let scores = if k = 1 then score_1 e r else (k_score k e r) in
case inference_step failedMerges e (ffilter (\<lambda>s. (S1 s, S2 s) \<notin> failedMerges \<and> (S2 s, S1 s) \<notin> failedMerges) scores) m check np of
(None, _) \<Rightarrow> e |
(Some new, failedMerges) \<Rightarrow> if (S new) |\<subset>| (S e) then infer failedMerges k new r m check np else e
)"
by auto
termination
apply (relation "measures [\<lambda>(_, _, e, _). size (S e)]")
apply simp
by (metis (no_types, lifting) case_prod_conv measures_less size_fsubset)
fun get_ints :: "trace \<Rightarrow> int list" where
"get_ints [] = []" |
"get_ints ((_, inputs, outputs)#t) = (map (\<lambda>x. case x of Num n \<Rightarrow> n) (filter is_Num (inputs@outputs)))"
definition learn :: "nat \<Rightarrow> iEFSM \<Rightarrow> log \<Rightarrow> strategy \<Rightarrow> update_modifier \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"learn n pta l r m np = (
let check = accepts_log (set l) in
(infer {} n pta r m check np)
)"
subsection\<open>Evaluating Inferred Models\<close>
text\<open>We need a function to test the EFSMs we infer. The \texttt{test\_trace} function executes a
trace in the model and outputs a more comprehensive trace such that the expected outputs and actual
outputs can be compared. If a point is reached where the model does not recognise an action, the
remainder of the trace forms the second element of the output pair such that we know the exact point
at which the model stopped processing.\<close>
definition i_possible_steps :: "iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> label \<Rightarrow> inputs \<Rightarrow> (tids \<times> cfstate \<times> transition) fset" where
"i_possible_steps e s r l i = fimage (\<lambda>(uid, (origin, dest), t). (uid, dest, t))
(ffilter (\<lambda>(uid, (origin, dest::nat), t::transition).
origin = s
\<and> (Label t) = l
\<and> (length i) = (Arity t)
\<and> apply_guards (Guards t) (join_ir i r)
)
e)"
fun test_trace :: "trace \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> ((label \<times> inputs \<times> cfstate \<times> cfstate \<times> registers \<times> tids \<times> value list \<times> outputs) list \<times> trace)" where
"test_trace [] _ _ _ = ([], [])" |
"test_trace ((l, i, expected)#es) e s r = (
let
ps = i_possible_steps e s r l i
in
if fis_singleton ps then
let
(id, s', t) = fthe_elem ps;
r' = evaluate_updates t i r;
actual = evaluate_outputs t i r;
(est, fail) = (test_trace es e s' r')
in
((l, i, s, s', r, id, expected, actual)#est, fail)
else
([], (l, i, expected)#es)
)"
text\<open>The \texttt{test\_log} function executes the \texttt{test\_trace} function on a collection of
traces known as the \emph{test set.}\<close>
definition test_log :: "log \<Rightarrow> iEFSM \<Rightarrow> ((label \<times> inputs \<times> cfstate \<times> cfstate \<times> registers \<times> tids \<times> value list \<times> outputs) list \<times> trace) list" where
"test_log l e = map (\<lambda>t. test_trace t e 0 <>) l"
end

View File

@ -0,0 +1,36 @@
chapter AFP
session Extended_Finite_State_Machine_Inference (AFP) = Extended_Finite_State_Machines +
options [timeout = 600]
directories
"heuristics"
"code-targets"
"examples"
theories
"Subsumption"
"examples/Drinks_Subsumption"
"Inference"
"SelectionStrategies"
"heuristics/Store_Reuse"
"heuristics/Store_Reuse_Subsumption"
"heuristics/Increment_Reset"
"heuristics/Same_Register"
"heuristics/Least_Upper_Bound"
"heuristics/Distinguishing_Guards"
"heuristics/Weak_Subsumption"
"heuristics/PTA_Generalisation"
"EFSM_Dot"
"efsm2sal"
"code-targets/Code_Target_List"
"code-targets/Code_Target_Set"
"code-targets/Code_Target_FSet"
"Code_Generation"
document_files
"root.tex"
"root.bib"

View File

@ -0,0 +1,110 @@
section\<open>Selection Strategies\<close>
text\<open>The strategy used to idenfity and prioritise states to be merged plays a big part in how the
final model turns out. This theory file presents a number of different selection strategies.\<close>
theory SelectionStrategies
imports Inference
begin
(* One point if they're equal *)
text\<open>The simplest strategy is to assign one point for each shared pair of transitions.\<close>
definition exactly_equal :: strategy where
"exactly_equal t1ID t2ID e = bool2nat ((get_by_ids e t1ID) = (get_by_ids e t2ID))"
text\<open>Another simple strategy is to look at the labels and arities of outgoing transitions of each
state. Pairs of states are ranked by how many transitions with the same label and arity they have in
common.\<close>
definition naive_score :: strategy where
"naive_score t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
bool2nat (Label t1 = Label t2 \<and> Arity t1 = Arity t2 \<and> length (Outputs t1) = length (Outputs t2))
)"
text\<open>Building off the above strategy, it makes sense to give transitions an extra ``bonus point'' if
they are exactly equal.\<close>
definition naive_score_eq_bonus :: strategy where
"naive_score_eq_bonus t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
score_transitions t1 t2
)"
(* One point each for equal label, arity, and outputs *)
text\<open>Another strategy is to assign bonus points for each shared output.\<close>
definition naive_score_outputs :: strategy where
"naive_score_outputs t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
bool2nat (Label t1 = Label t2) + bool2nat (Arity t1 = Arity t2) + bool2nat (Outputs t1 = Outputs t2)
)"
(* Functions with same label, and input and output arities contribute one point for each guard *)
(* and output they share. *)
text\<open>Along similar lines, we can assign additional bonus points for shared guards.\<close>
definition naive_score_comprehensive :: strategy where
"naive_score_comprehensive t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
if Label t1 = Label t2 \<and> Arity t1 = Arity t2 then
if length (Outputs t1) = length (Outputs t2) then
card (set (Guards t1) \<inter> set (Guards t2)) + length (filter (\<lambda>(p1, p2). p1 = p2) (zip (Outputs t1) (Outputs t2)))
else 0
else 0
)"
(* Functions with same label, and input and output arities contribute one point for each guard *)
(* and output they share. Transitions which are exactly equal get a very high score. *)
text\<open>This strategy is similar to the one above except that transitions which are exactly equal get
100 bonus points. \<close>
definition naive_score_comprehensive_eq_high :: strategy where
"naive_score_comprehensive_eq_high t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
if t1 = t2 then
100
else
if Label t1 = Label t2 \<and> Arity t1 = Arity t2 then
if length (Outputs t1) = length (Outputs t2) then
card (set (Guards t1) \<inter> set (Guards t2)) + length (filter (\<lambda>(p1, p2). p1 = p2) (zip (Outputs t1) (Outputs t2)))
else 0
else 0
)"
(* One point if one subsumes the other *)
text\<open>We can incorporate the subsumption relation into the scoring of merges such that a pair of
states receives one point for each pair of transitions where one directly subsumes the other.\<close>
definition naive_score_subsumption :: "strategy" where
"naive_score_subsumption t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID;
s = origin t1ID e
in
bool2nat (directly_subsumes (tm e) (tm e) s s t1 t2) + bool2nat (directly_subsumes (tm e) (tm e) s s t2 t1)
)"
(* Orders by the origin state so we merge leaves first *)
text\<open>An alternative strategy is to simply score merges based on the states' proximity to the origin.\<close>
definition leaves :: strategy where
"leaves t1ID t2ID e = (
let
t1 = get_by_ids e t1ID;
t2 = get_by_ids e t2ID
in
if (Label t1 = Label t2 \<and> Arity t1 = Arity t2 \<and> length (Outputs t1) = length (Outputs t2)) then
origin t1ID e + origin t2ID e
else
0)"
end

View File

@ -0,0 +1,204 @@
section \<open>Contexts and Subsumption\<close>
text\<open>This theory uses contexts to extend the idea of transition subsumption from \cite{lorenzoli2008} to
EFSM transitions with register update functions. The \emph{subsumption in context} relation is the
main contribution of \cite{foster2018}.\<close>
theory Subsumption
imports
"Extended_Finite_State_Machines.EFSM"
begin
definition posterior_separate :: "nat \<Rightarrow> vname gexp list \<Rightarrow> update_function list \<Rightarrow> inputs \<Rightarrow> registers \<Rightarrow> registers option" where
"posterior_separate a g u i r = (if can_take a g i r then Some (apply_updates u (join_ir i r) r) else None)"
definition posterior :: "transition \<Rightarrow> inputs \<Rightarrow> registers \<Rightarrow> registers option" where
"posterior t i r = posterior_separate (Arity t) (Guards t) (Updates t) i r"
definition subsumes :: "transition \<Rightarrow> registers \<Rightarrow> transition \<Rightarrow> bool" where
"subsumes t2 r t1 = (Label t1 = Label t2 \<and> Arity t1 = Arity t2 \<and>
(\<forall>i. can_take_transition t1 i r \<longrightarrow> can_take_transition t2 i r) \<and>
(\<forall>i. can_take_transition t1 i r \<longrightarrow>
evaluate_outputs t1 i r = evaluate_outputs t2 i r) \<and>
(\<forall>p1 p2 i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 \<longrightarrow>
posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1 \<longrightarrow>
(\<forall>P r'. (p1 $ r' = None) \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r'))))
)"
lemma no_functionality_subsumed:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
\<nexists>i. can_take_transition t1 i c \<Longrightarrow>
subsumes t2 c t1"
by (simp add: subsumes_def posterior_separate_def can_take_transition_def)
lemma subsumes_updates:
"subsumes t2 r t1 \<Longrightarrow>
can_take_transition t1 i r \<Longrightarrow>
evaluate_updates t1 i r $ a = Some x \<Longrightarrow>
evaluate_updates t2 i r $ a = Some x"
apply (simp add: subsumes_def posterior_separate_def can_take_transition_def[symmetric])
apply clarsimp
apply (erule_tac x=i in allE)+
apply (erule_tac x="evaluate_updates t1 i r" in allE)
apply (erule_tac x="evaluate_updates t2 i r" in allE)
apply (erule_tac x=i in allE)
apply simp
apply (simp add: all_comm[of "\<lambda>P r'.
P (evaluate_updates t2 i r $ r') \<longrightarrow> evaluate_updates t1 i r $ r' = None \<or> P (evaluate_updates t1 i r $ r')"])
apply (erule_tac x=a in allE)
by auto
lemma subsumption:
"(Label t1 = Label t2 \<and> Arity t1 = Arity t2) \<Longrightarrow>
(\<forall>i. can_take_transition t1 i r \<longrightarrow> can_take_transition t2 i r) \<Longrightarrow>
(\<forall>i. can_take_transition t1 i r \<longrightarrow>
evaluate_outputs t1 i r = evaluate_outputs t2 i r) \<Longrightarrow>
(\<forall>p1 p2 i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 \<longrightarrow>
posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1 \<longrightarrow>
(\<forall>P r'. (p1 $ r' = None) \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))) \<Longrightarrow>
subsumes t2 r t1"
by (simp add: subsumes_def)
lemma bad_guards:
"\<exists>i. can_take_transition t1 i r \<and> \<not> can_take_transition t2 i r \<Longrightarrow>
\<not> subsumes t2 r t1"
by (simp add: subsumes_def)
lemma inconsistent_updates:
"\<exists>p2 p1. (\<exists>i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 \<and>
posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1) \<and>
(\<exists>r' P. P (p2 $ r') \<and> (\<exists>y. p1 $ r' = Some y) \<and> \<not> P (p1 $ r')) \<Longrightarrow>
\<not> subsumes t2 r t1"
by (metis (no_types, hide_lams) option.simps(3) subsumes_def)
lemma bad_outputs:
"\<exists>i. can_take_transition t1 i r \<and> evaluate_outputs t1 i r \<noteq> evaluate_outputs t2 i r \<Longrightarrow>
\<not> subsumes t2 r t1"
by (simp add: subsumes_def)
lemma no_choice_no_subsumption: "Label t = Label t' \<Longrightarrow>
Arity t = Arity t' \<Longrightarrow>
\<not> choice t t' \<Longrightarrow>
\<exists>i. can_take_transition t' i c \<Longrightarrow>
\<not> subsumes t c t'"
by (meson bad_guards can_take_def can_take_transition_def choice_def)
lemma subsumption_def_alt: "subsumes t1 c t2 = (Label t2 = Label t1 \<and>
Arity t2 = Arity t1 \<and>
(\<forall>i. can_take_transition t2 i c \<longrightarrow> can_take_transition t1 i c) \<and>
(\<forall>i. can_take_transition t2 i c \<longrightarrow> evaluate_outputs t2 i c = evaluate_outputs t1 i c) \<and>
(\<forall>i. can_take_transition t2 i c \<longrightarrow>
(\<forall>r' P.
P (evaluate_updates t1 i c $ r') \<longrightarrow>
evaluate_updates t2 i c $ r' = None \<or> P (evaluate_updates t2 i c $ r'))))"
apply (simp add: subsumes_def posterior_separate_def can_take_transition_def[symmetric])
by blast
lemma subsumes_update_equality:
"subsumes t1 c t2 \<Longrightarrow> (\<forall>i. can_take_transition t2 i c \<longrightarrow>
(\<forall>r'.
((evaluate_updates t1 i c $ r') = (evaluate_updates t2 i c $ r')) \<or>
evaluate_updates t2 i c $ r' = None))"
apply (simp add: subsumption_def_alt)
apply clarify
subgoal for i r' y
apply (erule_tac x=i in allE)+
apply simp
apply (erule_tac x=r' in allE)
by auto
done
text_raw\<open>\snip{subsumptionReflexive}{1}{2}{%\<close>
lemma subsumes_reflexive: "subsumes t c t"
text_raw\<open>$\langle\isa{proof}\rangle$}%endsnip\<close>
by (simp add: subsumes_def)
text_raw\<open>\snip{subsumptionTransitive}{1}{2}{%\<close>
lemma subsumes_transitive:
assumes p1: "subsumes t1 c t2"
and p2: "subsumes t2 c t3"
shows "subsumes t1 c t3"
text_raw\<open>}%endsnip\<close>
using p1 p2
apply (simp add: subsumes_def)
by (metis subsumes_update_equality p1 p2 can_take_transition_def option.distinct(1) option.sel posterior_separate_def)
lemma subsumes_possible_steps_replace:
"(s2', t2') |\<in>| possible_steps e2 s2 r2 l i \<Longrightarrow>
subsumes t2 r2 t1 \<Longrightarrow>
((s2, s2'), t2') = ((ss2, ss2'), t1) \<Longrightarrow>
(s2', t2) |\<in>| possible_steps (replace e2 ((ss2, ss2'), t1) ((ss2, ss2'), t2)) s2 r2 l i"
proof(induct e2)
case empty
then show ?case
by (simp add: no_outgoing_transitions)
next
case (insert x e2)
then show ?case
apply (simp add: fmember_possible_steps subsumes_def)
apply standard
apply (simp add: replace_def)
apply auto[1]
by (simp add: can_take)
qed
subsection\<open>Direct Subsumption\<close>
text\<open>When merging EFSM transitions, one must \emph{account for} the behaviour of the other. The
\emph{subsumption in context} relation formalises the intuition that, in certain contexts, a
transition $t_2$ reproduces the behaviour of, and updates the data state in a manner consistent
with, another transition $t_1$, meaning that $t_2$ can be used in place of $t_1$ with no observable
difference in behaviour.
The subsumption in context relation requires us to supply a context in which to test subsumption,
but there is a problem when we try to apply this to inference: Which context should we use? The
\emph{direct subsumption} relation works at EFSM level to determine when and whether one transition
is able to account for the behaviour of another such that we can use one in place of another without
adversely effecting observable behaviour.\<close>
text_raw\<open>\snip{directlySubsumes}{1}{2}{%\<close>
definition directly_subsumes :: "transition_matrix \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> cfstate \<Rightarrow> transition \<Rightarrow> transition \<Rightarrow> bool" where
"directly_subsumes e1 e2 s1 s2 t1 t2 \<equiv> (\<forall>c1 c2 t. (obtains s1 c1 e1 0 <> t \<and> obtains s2 c2 e2 0 <> t) \<longrightarrow> subsumes t1 c2 t2)"
text_raw\<open>}%endsnip\<close>
text_raw\<open>\snip{subsumesAllContexts}{1}{2}{%\<close>
lemma subsumes_in_all_contexts_directly_subsumes:
"(\<And>c. subsumes t2 c t1) \<Longrightarrow> directly_subsumes e1 e2 s s' t2 t1"
text_raw\<open>}%endsnip\<close>
by (simp add: directly_subsumes_def)
text_raw\<open>\snip{directSubsumption}{1}{2}{%\<close>
lemma direct_subsumption:
"(\<And>t c1 c2. obtains s1 c1 e1 0 <> t \<Longrightarrow> obtains s2 c2 e2 0 <> t \<Longrightarrow> f c2) \<Longrightarrow>
(\<And>c. f c \<Longrightarrow> subsumes t1 c t2) \<Longrightarrow>
directly_subsumes e1 e2 s1 s2 t1 t2"
text_raw\<open>}%endsnip\<close>
apply (simp add: directly_subsumes_def)
by auto
text_raw\<open>\snip{obtainableNoSubsumption}{1}{2}{%\<close>
lemma visits_and_not_subsumes:
"(\<exists>c1 c2 t. obtains s1 c1 e1 0 <> t \<and> obtains s2 c2 e2 0 <> t \<and> \<not> subsumes t1 c2 t2) \<Longrightarrow>
\<not> directly_subsumes e1 e2 s1 s2 t1 t2"
text_raw\<open>}%endsnip\<close>
apply (simp add: directly_subsumes_def)
by auto
text_raw\<open>\snip{directSubsumptionReflexive}{1}{2}{%\<close>
lemma directly_subsumes_reflexive: "directly_subsumes e1 e2 s1 s2 t t"
text_raw\<open>}%endsnip\<close>
apply (simp add: directly_subsumes_def)
by (simp add: subsumes_reflexive)
text_raw\<open>\snip{directSubsumptionTransitive}{1}{2}{%\<close>
lemma directly_subsumes_transitive:
assumes p1: "directly_subsumes e1 e2 s1 s2 t1 t2"
and p2: "directly_subsumes e1 e2 s1 s2 t2 t3"
shows "directly_subsumes e1 e2 s1 s2 t1 t3"
text_raw\<open>}%endsnip\<close>
using p1 p2
apply (simp add: directly_subsumes_def)
using subsumes_transitive by blast
end

View File

@ -0,0 +1,164 @@
section\<open>Finite Sets\<close>
text\<open>Here we define the operations on the \texttt{fset} datatype in terms of lists rather than sets.
This allows the Scala implementation to skip a case match each time, which makes for cleaner and
slightly faster code.\<close>
theory Code_Target_FSet
imports "Extended_Finite_State_Machines.FSet_Utils"
begin
code_datatype fset_of_list
declare FSet.fset_of_list.rep_eq [code]
lemma fprod_code [code]:
"fprod (fset_of_list xs) (fset_of_list ys) = fset_of_list (remdups [(x, y). x \<leftarrow> xs, y \<leftarrow> ys])"
apply (simp add: fprod_def fset_of_list_def fset_both_sides Abs_fset_inverse)
by auto
lemma fminus_fset_filter [code]:
"fset_of_list A - xs = fset_of_list (remdups (filter (\<lambda>x. x |\<notin>| xs) A))"
by auto
lemma sup_fset_fold [code]:
"(fset_of_list f1) |\<union>| (fset_of_list f2) = fset_of_list (remdups (f1@f2))"
by simp
lemma bot_fset [code]: "{||} = fset_of_list []"
by simp
lemma finsert [code]:
"finsert a (fset_of_list as) = fset_of_list (List.insert a as)"
by (simp add: List.insert_def finsert_absorb fset_of_list_elem)
lemma ffilter_filter [code]:
"ffilter f (fset_of_list as) = fset_of_list (List.filter f (remdups as))"
by simp
lemma fimage_map [code]:
"fimage f (fset_of_list as) = fset_of_list (List.map f (remdups as))"
by simp
lemma ffUnion_fold [code]:
"ffUnion (fset_of_list as) = fold (|\<union>|) as {||}"
by (simp add: fold_union_ffUnion)
lemma fmember [code]: "a |\<in>| (fset_of_list as) = List.member as a"
by (simp add: fset_of_list_elem member_def)
lemma fthe_elem [code]: "fthe_elem (fset_of_list [x]) = x"
by simp
lemma size [code]: "size (fset_of_list as) = length (remdups as)"
proof(induct as)
case Nil
then show ?case
by simp
next
case (Cons a as)
then show ?case
by (simp add: fset_of_list.rep_eq insert_absorb)
qed
lemma fMax_fold [code]: "fMax (fset_of_list (a#as)) = fold max as a"
by (metis Max.set_eq_fold fMax.F.rep_eq fset_of_list.rep_eq)
lemma fMin_fold [code]: "fMin (fset_of_list (h#t)) = fold min t h"
apply (simp add: fset_of_list_def)
by (metis Min.set_eq_fold fMin_Min fset_of_list.abs_eq list.simps(15))
lemma fremove_code [code]:
"fremove a (fset_of_list A) = fset_of_list (filter (\<lambda>x. x \<noteq> a) A)"
apply (simp add: fremove_def minus_fset_def ffilter_def fset_both_sides Abs_fset_inverse fset_of_list.rep_eq)
by auto
lemma fsubseteq [code]:
"(fset_of_list l) |\<subseteq>| A = List.list_all (\<lambda>x. x |\<in>| A) l"
by (induct l, auto)
lemma fsum_fold [code]: "fSum (fset_of_list l) = fold (+) (remdups l) 0"
proof(induct l)
case Nil
then show ?case
by (simp add: fsum.F.rep_eq fSum_def)
next
case (Cons a l)
then show ?case
apply simp
apply standard
apply (simp add: finsert_absorb fset_of_list_elem)
by (simp add: add.commute fold_plus_sum_list_rev fset_of_list.rep_eq fsum.F.rep_eq fSum_def)
qed
lemma code_fset_eq [code]:
"HOL.equal X (fset_of_list Y) \<longleftrightarrow> size X = length (remdups Y) \<and> (\<forall>x |\<in>| X. List.member Y x)"
apply (simp only: HOL.equal_class.equal_eq fset_eq_alt)
apply (simp only: size)
using fmember by fastforce
lemma code_fsubset [code]:
"s |\<subset>| s' = (s |\<subseteq>| s' \<and> size s < size s')"
apply standard
apply (simp only: size_fsubset)
by auto
lemma code_fset [code]: "fset (fset_of_list l) = fold insert l {}"
using fset_of_list.rep_eq union_set_fold by fastforce
lemma code_fBall [code]: "fBall (fset_of_list l) f = list_all f l"
by (simp add: Ball_set fBall.rep_eq fset_of_list.rep_eq)
lemma code_fBex [code]: "fBex (fset_of_list l) f = list_ex f l"
by (meson Bex_set fBexE fset_of_list_elem rev_fBexI)
definition "nativeSort = sort"
code_printing constant nativeSort \<rightharpoonup> (Scala) "_.sortWith((Orderings.less))"
lemma [code]: "sorted_list_of_fset (fset_of_list l) = nativeSort (remdups l)"
by (simp add: nativeSort_def sorted_list_of_fset_sort)
lemma [code]: "sorted_list_of_set (set l) = nativeSort (remdups l)"
by (simp add: nativeSort_def sorted_list_of_set_sort_remdups)
lemma [code]: "fMin (fset_of_list (h#t)) = hd (nativeSort (h#t))"
by (metis fMin_Min hd_sort_Min list.distinct(1) nativeSort_def)
lemma sorted_Max_Cons:
"l \<noteq> [] \<Longrightarrow>
sorted (a#l) \<Longrightarrow>
Max (set (a#l)) = Max (set l)"
using eq_iff by fastforce
lemma sorted_Max:
"l \<noteq> [] \<Longrightarrow>
sorted l \<Longrightarrow>
Max (set l) = hd (rev l)"
proof(induct l)
case Nil
then show ?case by simp
next
case (Cons a l)
then show ?case
by (metis sorted_Max_Cons Max_singleton hd_rev last.simps list.set(1) list.simps(15) sorted.simps(2))
qed
lemma [code]: "fMax (fset_of_list (h#t)) = last (nativeSort (h#t))"
by (metis Max.set_eq_fold fMax_fold hd_rev list.simps(3) nativeSort_def set_empty2 set_sort sorted_Max sorted_sort)
definition "list_max l = fold max l"
code_printing constant list_max \<rightharpoonup> (Scala) "_.par.fold((_))(Orderings.max)"
lemma [code]: "fMax (fset_of_list (h#t)) = list_max t h"
by (metis fMax_fold list_max_def)
definition "list_min l = fold min l"
code_printing constant list_min \<rightharpoonup> (Scala) "_.par.fold((_))(Orderings.min)"
lemma [code]: "fMin (fset_of_list (h#t)) = list_min t h"
by (metis fMin_fold list_min_def)
lemma fis_singleton_code [code]: "fis_singleton s = (size s = 1)"
apply (simp add: fis_singleton_def is_singleton_def)
by (simp add: card_Suc_eq)
end

View File

@ -0,0 +1,127 @@
chapter\<open>Code Generation\<close>
text\<open>This chapter details the code generator setup to produce executable Scala code for our
inference technique.\<close>
section\<open>Lists\<close>
text\<open>Here we define some equivalent definitions which make for a faster implementation. We also
make use of the \texttt{code\_printing} statement such that native Scala implementations of common
list operations are used instead of redefining them. This allows us to use the \texttt{par}
construct such that the parallel implementations are used, which makes for an even faster
implementation.\<close>
theory Code_Target_List
imports Main
begin
declare List.insert_def [code del]
declare member_rec [code del]
lemma [code]: "List.insert x xs = (if List.member xs x then xs else x#xs)"
by (simp add: in_set_member)
declare enumerate_eq_zip [code]
declare foldr_conv_foldl [code]
declare map_filter_map_filter [code_unfold del]
(* Use the native implementations of list functions *)
definition "flatmap l f = List.maps f l"
lemma [code]: "List.maps f l = flatmap l f"
by (simp add: flatmap_def)
definition "map_code l f = List.map f l"
lemma [code]:"List.map f l = map_code l f"
by (simp add: map_code_def)
lemma [code]: "removeAll a l = filter (\<lambda>x. x \<noteq> a) l"
by (induct l arbitrary: a) simp_all
definition "filter_code l f = List.filter f l"
lemma [code]: "List.filter l f = filter_code f l"
by (simp add: filter_code_def)
definition all :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
"all l f = list_all f l"
lemma [code]: "list_all f l = all l f"
by (simp add: all_def)
definition ex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
"ex l f = list_ex f l"
lemma [code]: "list_ex f l = ex l f"
by (simp add: ex_def)
declare foldl_conv_fold[symmetric]
lemma fold_conv_foldl [code]: "fold f xs s = foldl (\<lambda>x s. f s x) s xs"
by (simp add: foldl_conv_fold)
lemma code_list_eq [code]:
"HOL.equal xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
apply (simp add: HOL.equal_class.equal_eq)
by (simp add: Ball_set list_eq_iff_zip_eq)
definition take_map :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"take_map n l = (if length l \<le> n then l else map (\<lambda>i. l ! i) [0..<n])"
lemma nth_take_map: "i < n \<Longrightarrow> take_map n xs ! i = xs ! i"
by (simp add: take_map_def)
lemma [code]: "take n l = take_map n l"
by (simp add: list_eq_iff_nth_eq min_def take_map_def)
fun upt_tailrec :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
"upt_tailrec i 0 l = l" |
"upt_tailrec i (Suc j) l = (if i \<le> j then upt_tailrec i j ([j]@l) else l)"
lemma upt_arbitrary_l: "(upt i j)@l = upt_tailrec i j l"
by (induct i j l rule: upt_tailrec.induct, auto)
lemma [code]: "upt i j = upt_tailrec i j []"
by (metis upt_arbitrary_l append_Nil2)
function max_sort :: "('a::linorder) list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"max_sort [] l = l" |
"max_sort (h#t) l = (let u = (h#t); m = Max (set u) in max_sort (removeAll m u) (m#l))"
using splice.cases apply blast
by auto
termination
apply (relation "measures [\<lambda>(l1, l2). length l1]")
apply simp
by (metis Max_eq_iff List.finite_set case_prod_conv length_removeAll_less list.distinct(1) measures_less set_empty)
lemma remdups_fold [code]:
"remdups l = foldr (\<lambda>i l. if i \<in> set l then l else i#l) l []"
proof(induct l)
case Nil
then show ?case
by simp
next
case (Cons a l)
then show ?case
apply (simp)
apply standard
apply (metis set_remdups)
using set_remdups by fastforce
qed
code_printing
constant Cons \<rightharpoonup> (Scala) "_::_"
| constant rev \<rightharpoonup> (Scala) "_.par.reverse.toList"
| constant List.member \<rightharpoonup> (Scala) "_.contains((_))"
| constant "List.remdups" \<rightharpoonup> (Scala) "_.par.distinct.toList"
| constant "List.length" \<rightharpoonup> (Scala) "Nat.Nata(_.par.length)"
| constant "zip" \<rightharpoonup> (Scala) "_.par.zip((_)).toList"
| constant "flatmap" \<rightharpoonup> (Scala) "_.par.flatMap((_)).toList"
| constant "List.null" \<rightharpoonup> (Scala) "_.isEmpty"
| constant "map_code" \<rightharpoonup> (Scala) "_.par.map((_)).toList"
| constant "filter_code" \<rightharpoonup> (Scala) "_.par.filter((_)).toList"
| constant "all" \<rightharpoonup> (Scala) "_.par.forall((_))"
| constant "ex" \<rightharpoonup> (Scala) "_.par.exists((_))"
| constant "nth" \<rightharpoonup> (Scala) "_(Code'_Numeral.integer'_of'_nat((_)).toInt)"
| constant "foldl" \<rightharpoonup> (Scala) "Dirties.foldl"
| constant "hd" \<rightharpoonup> (Scala) "_.head"
end

View File

@ -0,0 +1,44 @@
section\<open>Sets\<close>
text\<open>While the default code generator setup for sets works fine, it does not make for particularly
readable code. The reason for this is that the default setup needs to work with potentially infinite
sets. All of the sets we need to use here are finite so we present an alternative setup for the
basic set operations which generates much cleaner code.\<close>
theory Code_Target_Set
imports "HOL-Library.Cardinality"
begin
code_datatype set
declare List.union_coset_filter [code del]
declare insert_code [code del]
declare remove_code [code del]
declare card_coset_error [code del]
declare coset_subseteq_set_code [code del]
declare eq_set_code(1) [code del]
declare eq_set_code(2) [code del]
declare eq_set_code(4) [code del]
declare List.subset_code [code del]
declare inter_coset_fold [code del]
declare Cardinality.subset'_code [code del]
declare subset_eq [code]
(* Get rid of that one unnamed lemma *)
lemma [code del]:
"x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
by (simp add: member_def)
lemma sup_set_append[code]: "(set x) \<union> (set y) = set (x @ y)"
by simp
declare product_concat_map [code]
lemma [code]: "insert x (set s) = (if x \<in> set s then set s else set (x#s))"
apply (simp)
by auto
lemma [code]:
"Cardinality.subset' (set l1) (set l2) = ((list_all (\<lambda>x. List.member l2 x)) l1)"
by (meson in_set_member list.pred_set subset'_code(2))
end

View File

@ -0,0 +1,70 @@
@article{bochvar1981,
author = {Bochvar, D. A.},
doi = {10.1080/01445348108837023},
issn = {14645149},
journal = {History and Philosophy of Logic},
month = {jan},
number = {1-2},
pages = {87--112},
title = {{On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus}},
url = {http://www.tandfonline.com/doi/abs/10.1080/01445348108837023},
volume = {2},
year = {1981}
}
@InCollection{foster2018,
address = {Heidelberg},
author = {Michael Foster and Ramsay G. Taylor and Achim D. Brucker
and John Derrick},
booktitle = {ICFEM},
doi = {10.1007/978-3-030-02450-5},
editor = {Jin Song Dong and Jing Sun},
isbn = {978-3-030-02449-9},
keywords = {model inference, state machine models, EFSM},
language = {USenglish},
location = {Gold Coast, Australia},
number = {11232},
pages = {373--387},
pdf = {https://www.brucker.ch/bibliography/download/2018/foster.ea-efsm-2018.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Formalising Extended Finite State Machine Transition
Merging},
url = {https://www.brucker.ch/bibliography/abstract/foster.ea-efsm-2018},
year = {2018}
}
@InCollection{foster2019,
address = {Heidelberg},
author = {Michael Foster and Achim D. Brucker and Ramsay G. Taylor
and Siobh{\'a}n North and John Derrick},
booktitle = {Software Engineering and Formal Methods (SEFM)},
doi = {10.1007/978-3-030-30446-1_14},
editor = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n},
isbn = {3-540-25109-X},
keywords = {EFSM Inference, Model Inference, Reverse Engineering},
language = {USenglish},
location = {Oslo},
number = {11724},
pages = {257--272},
pdf = {https://www.brucker.ch/bibliography/download/2019/foster.ea-incorporating-2019.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Incorporating Data into EFSM Inference},
url = {https://www.brucker.ch/bibliography/abstract/foster.ea-incorporating-2019},
year = {2019}
}
@inproceedings{lorenzoli2008,
address = {New York, New York, USA},
author = {Lorenzoli, Davide and Mariani, Leonardo and Pezz{\`{e}}, Mauro},
booktitle = {Proceedings of the 13th international conference on Software engineering - ICSE '08},
doi = {10.1145/1368088.1368157},
isbn = {9781605580791},
keywords = {dynamic analysis,gk-tail,model synthesis},
pages = {501},
publisher = {ACM Press},
title = {{Automatic generation of software behavioral models}},
url = {http://portal.acm.org/citation.cfm?doid=1368088.1368157},
year = {2008}
}

View File

@ -0,0 +1,108 @@
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt}
\usepackage[USenglish]{babel}
\usepackage[numbers, sort&compress]{natbib}
\usepackage{isabelle,isabellesym}
\usepackage{booktabs}
\usepackage{paralist}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage{rotating}
\pagestyle{headings}
\isabellestyle{default}
\setcounter{tocdepth}{1}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\thy}{\isabellecontext}
\renewcommand{\isamarkupsection}[1]{%
\begingroup%
\def\isacharunderscore{\textunderscore}%
\section{#1 (\thy)}%
\def\isacharunderscore{-}%
\expandafter\label{sec:\isabellecontext}%
\endgroup%
}
\newcommand{\orcidID}[1]{} % temp. hack
\newcommand{\repeatisanl}[1]
{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
\title{Inference of Extended Finite State Machines}%
\author{%
\begin{minipage}{.8\textwidth}
\centering
Michael~Foster\footnotemark[1]\orcidID{0000-0001-8233-9873}%
\qquad\qquad%
Achim~D.~Brucker\footnotemark[2]\orcidID{0000-0002-6355-1200}%
\\%
Ramsay~G.~Taylor\footnotemark[1]\orcidID{0000-0002-4036-7590}%
\qquad\qquad%
John~Derrick\footnotemark[1]\orcidID{0000-0002-6631-8914}%
\end{minipage}
}
\publishers{%
\footnotemark[1]~Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }%
\texttt{\{%
\href{mailto:jmafoster1@sheffield.ac.uk}{jmafoster1},%
\href{mailto:r.g.taylor@sheffield.ac.uk}{r.g.taylor},%
\href{mailto:j.derrick@sheffield.ac.uk}{j.derrick}%
\}@sheffield.ac.uk}\\[2em]%
\footnotemark[2]~%
Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }%
\href{mailto:a.brucker@exeter.ac.uk}{\texttt{a.brucker@exeter.ac.uk}}%
}
\begin{document}
\maketitle
\begin{abstract}
In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the \emph{subsumption in context} relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the \emph{direct subsumption} relation, which lifts the \emph{subsumption in context} relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and the that subsumption and direct subsumption are preorder relations.
We also provide a number of different \emph{heuristics} which can be used to abstract away concrete values into \emph{registers} so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined.
\begin{quote}
\bigskip
\noindent{\textbf{Keywords:} EFSMs, Model inference, Reverse engineering }
\end{quote}
\end{abstract}
\tableofcontents
\cleardoublepage
\chapter{Introduction}\label{chap:intro}
This AFP entry provides a formal implementation of a state-merging technique to infer EFSMs from black-box traces and is an accompaniment to work published in \cite{foster2018} and \cite{foster2019}. The inference technique builds off classical FSM inference techniques which work by first building a Prefix Tree Acceptor from traces of the underlying system, and then iteratively merging states which share behaviour to form a smaller model.
Most notably, we formalise the definitions of \emph{subsumption in context} and \emph{direct subsumption.} When merging EFSM transitions, one must \emph{account for} the behaviour of the other. The \emph{subsumption in context} relation from \cite{foster2018} formalises the intuition that, in certain contexts, a transition $t_2$ reproduces the behaviour of, and updates the data state in a manner consistent with, another transition $t_1$, meaning that $t_2$ can be used in place of $t_1$ with no observable difference in behaviour. This relation requires us to supply a context in which to test subsumption, but there is a problem when we try to apply this to inference: Which context should we use? The \emph{directly subsumes} relation presented in \cite{foster2019} incorporates subsumption into a relation which can be used to determine if it is safe to merge a pair of transitions in an EFSM. It is this which allows us to take the subsumption relation from \cite{foster2018} and use it in the inference process.
The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle. Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}).
\begin{sidewaysfigure}
\centering
\resizebox{\textheight}{!}{\includegraphics[height=\textheight]{session_graph}}
\caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}}
\end{sidewaysfigure}
\nocite{foster.ea:efsm:2018}
\clearpage
\input{session}
{\small
\bibliographystyle{abbrvnat}
\bibliography{root}
}
\end{document}
\endinput
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

View File

@ -0,0 +1,74 @@
section\<open>Output to SAL\<close>
text\<open>SAL is a framework for combining different tools for abstraction, program analysis, theorem
proving, and model checking. It is able to verify and refute properties of EFSMs phrased in LTL. In
\cite{foster2019}, it is proposed that a model checker be used to assist in checking the conditions
necessary for one transition to subsume another. In order to effect this, it is necessary to convert
the EFSM into a format that SAL can recognise. This theory file sets out the various definitions
needed to do this such that SAL can be used to check subsumption conditions when running the EFSM
inference tool generated by the code generator.\<close>
theory efsm2sal
imports "EFSM_Dot"
begin
definition replace :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" where
"replace s old new = s"
code_printing constant replace \<rightharpoonup> (Scala) "_.replaceAll(_, _)"
definition escape :: "String.literal \<Rightarrow> (String.literal \<times> String.literal) list \<Rightarrow> String.literal" where
"escape s replacements = fold (\<lambda>(old, new) s'. replace s' old new) replacements s"
definition "replacements = [
(STR ''/'', STR ''_SOL__''),
(STR 0x5C+STR 0x5C, STR ''_BSOL__''),
(STR '' '', STR ''_SPACE__''),
(STR 0x5C+STR ''('', STR ''_LPAR__''),
(STR 0x5C+STR '')'', STR ''_RPAR__''),
(STR 0x5C+STR ''.'', STR ''_PERIOD__''),
(STR ''@'', STR ''_COMMAT__'')
]"
fun aexp2sal :: "vname aexp \<Rightarrow> String.literal" where
"aexp2sal (L (Num n)) = STR ''Some(Num(''+ show_int n + STR ''))''"|
"aexp2sal (L (value.Str n)) = STR ''Some(Str(String__''+ (if n = STR '''' then STR ''_EMPTY__'' else escape n replacements) + STR ''))''" |
"aexp2sal (V (I i)) = STR ''Some(i('' + show_nat (i) + STR ''))''" |
"aexp2sal (V (R r)) = STR ''r__'' + show_nat r" |
"aexp2sal (Plus a1 a2) = STR ''value_plus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"aexp2sal (Minus a1 a2) = STR ''value_minus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"aexp2sal (Times a1 a2) = STR ''value_times(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''"
fun gexp2sal :: "vname gexp \<Rightarrow> String.literal" where
"gexp2sal (Bc True) = STR ''True''" |
"gexp2sal (Bc False) = STR ''False''" |
"gexp2sal (Eq a1 a2) = STR ''value_eq('' + aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"gexp2sal (Gt a1 a2) = STR ''value_gt('' + aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"gexp2sal (In v l) = join (map (\<lambda>l'. STR ''gval(value_eq('' + aexp2sal (V v) + STR '', '' + aexp2sal (L l') + STR ''))'') l) STR '' OR ''" |
"gexp2sal (Nor g1 g2) = STR ''NOT (gval('' + gexp2sal g1 + STR '') OR gval( '' + gexp2sal g2 + STR ''))''"
fun guards2sal :: "vname gexp list \<Rightarrow> String.literal" where
"guards2sal [] = STR ''TRUE''" |
"guards2sal G = join (map gexp2sal G) STR '' AND ''"
fun aexp2sal_num :: "vname aexp \<Rightarrow> nat \<Rightarrow> String.literal" where
"aexp2sal_num (L (Num n)) _ = STR ''Some(Num(''+ show_int n + STR ''))''"|
"aexp2sal_num (L (value.Str n)) _ = STR ''Some(Str(String__''+ (if n = STR '''' then STR ''_EMPTY__'' else escape n replacements) + STR ''))''" |
"aexp2sal_num (V (vname.I i)) _ = STR ''Some(i('' + show_nat i + STR ''))''" |
"aexp2sal_num (V (vname.R i)) m = STR ''r__'' + show_nat i + STR ''.'' + show_nat m" |
"aexp2sal_num (Plus a1 a2) _ = STR ''value_plus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"aexp2sal_num (Minus a1 a2) _ = STR ''value_minus(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''" |
"aexp2sal_num (Times a1 a2) _ = STR ''value_times(''+aexp2sal a1 + STR '', '' + aexp2sal a2 + STR '')''"
fun gexp2sal_num :: "vname gexp \<Rightarrow> nat \<Rightarrow> String.literal" where
"gexp2sal_num (Bc True) _ = STR ''True''" |
"gexp2sal_num (Bc False) _ = STR ''False''" |
"gexp2sal_num (Eq a1 a2) m = STR ''gval(value_eq('' + aexp2sal_num a1 m + STR '', '' + aexp2sal_num a2 m + STR ''))''" |
"gexp2sal_num (Gt a1 a2) m = STR ''gval(value_gt('' + aexp2sal_num a1 m + STR '', '' + aexp2sal_num a2 m + STR ''))''" |
"gexp2sal_num (In v l) m = join (map (\<lambda>l'. STR ''gval(value_eq('' + aexp2sal_num (V v) m + STR '', '' + aexp2sal_num (L l') m + STR ''))'') l) STR '' OR ''" |
"gexp2sal_num (Nor g1 g2) m = STR ''NOT ('' + gexp2sal_num g1 m + STR '' OR '' + gexp2sal_num g2 m + STR '')''"
fun guards2sal_num :: "vname gexp list \<Rightarrow> nat \<Rightarrow> String.literal" where
"guards2sal_num [] _ = STR ''TRUE''" |
"guards2sal_num G m = join (map (\<lambda>g. gexp2sal_num g m) G) STR '' AND ''"
end

View File

@ -0,0 +1,154 @@
subsection{*Example*}
text{*This theory shows how contexts can be used to prove transition subsumption.*}
theory Drinks_Subsumption
imports "Extended_Finite_State_Machine_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2"
begin
lemma stop_at_3: "\<not>obtains 1 c drinks2 3 r t"
proof(induct t arbitrary: r)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
by (simp add: drinks2_def)
qed
lemma no_1_2: "\<not>obtains 1 c drinks2 2 r t"
proof(induct t arbitrary: r)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
apply (simp add: drinks2_def)
apply clarsimp
apply (simp add: drinks2_def[symmetric])
apply (erule disjE)
apply simp
apply (erule disjE)
apply simp
by (simp add: stop_at_3)
qed
lemma no_change_1_1: "obtains 1 c drinks2 1 r t \<Longrightarrow> c = r"
proof(induct t)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
apply (simp add: drinks2_def)
apply clarsimp
apply (simp add: drinks2_def[symmetric])
apply (erule disjE)
apply (simp add: vend_nothing_def apply_updates_def)
by (simp add: no_1_2)
qed
lemma obtains_1: "obtains 1 c drinks2 0 <> t \<Longrightarrow> c $ 2 = Some (Num 0)"
proof(induct t)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
apply (simp add: drinks2_def)
apply clarsimp
apply (simp add: drinks2_def[symmetric])
apply (simp add: select_def can_take apply_updates_def)
using no_change_1_1 by fastforce
qed
lemma obtains_1_1_2:
"obtains 1 c1 drinks2 1 r t \<Longrightarrow>
obtains 1 c2 drinks 1 r t \<Longrightarrow>
c1 = r \<and> c2 = r"
proof(induct t arbitrary: r)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
apply (simp add: drinks2_def drinks_def)
apply clarsimp
apply (simp add: drinks2_def[symmetric] drinks_def[symmetric])
apply safe
using Cons.prems(1) no_change_1_1 apply blast
apply (simp add: coin_def vend_nothing_def)
using Cons.prems(1) no_change_1_1 apply blast
apply (simp add: vend_fail_def vend_nothing_def apply_updates_def)
using Cons.prems(1) no_change_1_1 apply blast
apply (metis drinks_rejects_future numeral_eq_one_iff obtains.cases obtains_recognises semiring_norm(85))
using no_1_2 apply blast
using no_1_2 apply blast
using Cons.prems(1) no_change_1_1 apply blast
using no_1_2 apply blast
using no_1_2 apply blast
using no_1_2 by blast
qed
lemma obtains_1_c2:
"obtains 1 c1 drinks2 0 <> t \<Longrightarrow> obtains 1 c2 drinks 0 <> t \<Longrightarrow> c2 $ 2 = Some (Num 0)"
proof(induct t)
case Nil
then show ?case
by (simp add: obtains_base)
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply (simp add: obtains_step)
apply clarify
apply (simp add: in_possible_steps[symmetric])
apply (simp add: drinks2_def drinks_def)
apply clarsimp
apply (simp add: drinks2_def[symmetric] drinks_def[symmetric])
apply (simp add: select_def can_take apply_updates_def)
using obtains_1_1_2 by fastforce
qed
lemma directly_subsumes: "directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing"
apply (rule direct_subsumption[of _ _ _ _ "\<lambda>c2. c2 $ 2 = Some (Num 0)"])
apply (simp add: obtains_1_c2)
apply (rule subsumption)
apply (simp add: vend_fail_def vend_nothing_def)
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)
apply (simp add: vend_fail_def vend_nothing_def)
by (simp add: posterior_separate_def vend_fail_def vend_nothing_def)
lemma directly_subsumes_flip: "directly_subsumes drinks2 drinks 1 1 vend_nothing vend_fail"
apply (rule direct_subsumption[of _ _ _ _ "\<lambda>c2. c2 $ 2 = Some (Num 0)"])
apply (simp add: obtains_1_c2)
apply (rule subsumption)
apply (simp add: vend_fail_def vend_nothing_def)
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)
by (simp add: posterior_separate_def vend_fail_def vend_nothing_def)
end

View File

@ -0,0 +1,117 @@
section\<open>Distinguishing Guards\<close>
text\<open>If we cannot resolve the nondeterminism which arises from merging states by merging
transitions, we might then conclude that those states should not be merged. Alternatively, we could
consider the possibility of \emph{value-dependent} behaviour. This theory presents a heuristic which
tries to find a guard which distinguishes between a pair of transitions.\<close>
theory Distinguishing_Guards
imports "../Inference"
begin
hide_const uids
definition put_updates :: "tids \<Rightarrow> update_function list \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"put_updates uids updates iefsm = fimage (\<lambda>(uid, fromTo, tran).
case uid of [u] \<Rightarrow>
if u \<in> set uids then
(uid, fromTo, \<lparr>Label = Label tran, Arity = Arity tran, Guards = Guards tran, Outputs = Outputs tran, Updates = (Updates tran)@updates\<rparr>)
else
(uid, fromTo, tran)
) iefsm"
definition transfer_updates :: "iEFSM \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"transfer_updates e pta = fold (\<lambda>(tids, (from, to), tran) acc. put_updates tids (Updates tran) acc) (sorted_list_of_fset e) pta"
fun trace_collect_training_sets :: "trace \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> tids \<Rightarrow> tids \<Rightarrow> (inputs \<times> registers) list \<Rightarrow> (inputs \<times> registers) list \<Rightarrow> ((inputs \<times> registers) list \<times> (inputs \<times> registers) list)" where
"trace_collect_training_sets [] uPTA s registers T1 T2 G1 G2 = (G1, G2)" |
"trace_collect_training_sets ((label, inputs, outputs)#t) uPTA s registers T1 T2 G1 G2 = (
let
(uids, s', tran) = fthe_elem (ffilter (\<lambda>(uids, s', tran). evaluate_outputs tran inputs registers = map Some outputs) (i_possible_steps uPTA s registers label inputs));
updated = (evaluate_updates tran inputs registers)
in
if hd uids \<in> set T1 then
trace_collect_training_sets t uPTA s' updated T1 T2 ((inputs, registers)#G1) G2
else if hd uids \<in> set T2 then
trace_collect_training_sets t uPTA s' updated T1 T2 G1 ((inputs, registers)#G2)
else
trace_collect_training_sets t uPTA s' updated T1 T2 G1 G2
)"
primrec collect_training_sets :: "log \<Rightarrow> iEFSM \<Rightarrow> tids \<Rightarrow> tids \<Rightarrow> (inputs \<times> registers) list \<Rightarrow> (inputs \<times> registers) list \<Rightarrow> ((inputs \<times> registers) list \<times> (inputs \<times> registers) list)" where
"collect_training_sets [] uPTA T1 T2 G1 G2 = (G1, G2)" |
"collect_training_sets (h#t) uPTA T1 T2 G1 G2 = (
let (G1a, G2a) = trace_collect_training_sets h uPTA 0 <> T1 T2 [] [] in
collect_training_sets t uPTA T1 T2 (List.union G1 G1a) (List.union G2 G2a)
)"
definition find_distinguishing_guards :: "(inputs \<times> registers) list \<Rightarrow> (inputs \<times> registers) list \<Rightarrow> (vname gexp \<times> vname gexp) option" where
"find_distinguishing_guards G1 G2 = (
let gs = {(g1, g2).
(\<forall>(i, r) \<in> set G1. gval g1 (join_ir i r) = true) \<and>
(\<forall>(i, r) \<in> set G2. gval g2 (join_ir i r) = true) \<and>
(\<forall>i r. \<not> (gval g1 (join_ir i r) = true \<and> gval g2 (join_ir i r) = true))
} in
if gs = {} then None else Some (Eps (\<lambda>g. g \<in> gs))
)"
declare find_distinguishing_guards_def [code del]
code_printing constant find_distinguishing_guards \<rightharpoonup> (Scala) "Dirties.findDistinguishingGuards"
definition add_guard :: "transition \<Rightarrow> vname gexp \<Rightarrow> transition" where
"add_guard t g = t\<lparr>Guards := List.insert g (Guards t)\<rparr>"
definition distinguish :: "log \<Rightarrow> update_modifier" where
"distinguish log t1ID t2ID s destMerge preDestMerge old check = (
let
t1 = get_by_ids destMerge t1ID;
t2 = get_by_ids destMerge t2ID;
uPTA = transfer_updates destMerge (make_pta log);
(G1, G2) = collect_training_sets log uPTA t1ID t2ID [] []
in
case find_distinguishing_guards G1 G2 of
None \<Rightarrow> None |
Some (g1, g2) \<Rightarrow> (
let rep = replace_transitions preDestMerge [(t1ID, add_guard t1 g1), (t2ID, add_guard t2 g2)] in
if check (tm rep) then Some rep else None
)
)"
definition can_still_take_ctx :: "transition_matrix \<Rightarrow> transition_matrix \<Rightarrow> cfstate \<Rightarrow> cfstate \<Rightarrow> transition \<Rightarrow> transition \<Rightarrow> bool" where
"can_still_take_ctx e1 e2 s1 s2 t1 t2 = (
\<forall>t. recognises e1 t \<and> visits s1 e1 0 <> t \<and> recognises e2 t \<and> visits s2 e2 0 <> t \<longrightarrow>
(\<forall>a. obtains s2 a e2 0 <> t \<and> (\<forall>i. can_take_transition t2 i a \<longrightarrow> can_take_transition t1 i a))
)"
lemma distinguishing_guard_subsumption:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = Updates t2 \<Longrightarrow>
can_still_take_ctx e1 e2 s1 s2 t1 t2 \<Longrightarrow>
recognises e1 p \<Longrightarrow>
visits s1 e1 0 <> p \<Longrightarrow>
obtains s2 c e2 0 <> p \<Longrightarrow>
subsumes t1 c t2"
apply (simp add: subsumes_def can_still_take_ctx_def)
apply (erule_tac x=p in allE)
apply simp
by (simp add: obtains_recognises obtains_visits)
definition "recognises_and_visits_both a b s s' = (
\<exists>p c1 c2. obtains s c1 a 0 <> p \<and> obtains s' c2 b 0 <> p)"
definition "can_still_take e1 e2 s1 s2 t1 t2 = (
Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
Outputs t1 = Outputs t2 \<and>
Updates t1 = Updates t2 \<and>
can_still_take_ctx e1 e2 s1 s2 t1 t2 \<and>
recognises_and_visits_both e1 e2 s1 s2)"
lemma can_still_take_direct_subsumption:
"can_still_take e1 e2 s1 s2 t1 t2 \<Longrightarrow>
directly_subsumes e1 e2 s1 s2 t1 t2"
apply (simp add: directly_subsumes_def can_still_take_def)
apply standard
by (meson distinguishing_guard_subsumption obtains_visits obtains_recognises recognises_and_visits_both_def)
end

View File

@ -0,0 +1,56 @@
theory Group_By
imports Main
begin
fun group_by :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
"group_by f [] = []" |
"group_by f (h#t) = (
let
group = (takeWhile (f h) t);
dropped = drop (length group) t
in
(h#group)#(group_by f dropped)
)"
lemma "(group_by f xs = []) = (xs = [])"
by (induct xs, auto simp add: Let_def)
lemma not_empty_group_by_drop: "\<forall>x \<in> set (group_by f (drop l xs)). x \<noteq> []"
by (induct xs arbitrary: l, auto simp add: drop_Cons' Let_def)
lemma no_empty_groups: "\<forall>x\<in>set (group_by f xs). x \<noteq> []"
by (metis not_empty_group_by_drop empty_iff empty_set group_by.elims list.distinct(1) set_ConsD)
lemma "(drop (length (takeWhile f l)) l) = dropWhile f l"
by (simp add: dropWhile_eq_drop)
lemma takeWhile_dropWhile: "takeWhile f l @ dropWhile f l = l' \<Longrightarrow> l' = l"
by simp
lemma append_pref: "l' = l'' \<Longrightarrow> (l@l' = l@l'')"
by simp
lemma dropWhile_drop: "\<exists>x. dropWhile f l = drop x l"
using dropWhile_eq_drop by blast
lemma group_by_drop_foldr: "drop x l = foldr (@) (group_by f (drop x l)) []"
proof (induct l arbitrary: x)
case (Cons a l)
then show ?case
apply (simp add: drop_Cons' Let_def)
by (metis append_take_drop_id takeWhile_eq_take)
qed auto
lemma group_by_inverse: "foldr (@) (group_by f l) [] = l"
proof(induct l)
case (Cons a l)
then show ?case
apply (simp add: Let_def dropWhile_eq_drop[symmetric])
apply (rule takeWhile_dropWhile[of "f a"])
apply (rule append_pref)
apply (insert dropWhile_drop[of "f a" l])
apply (erule exE)
by (simp add: group_by_drop_foldr)
qed auto
end

View File

@ -0,0 +1,85 @@
section\<open>Increment and Reset\<close>
text\<open>The ``increment and reset'' heuristic proposed in \cite{foster2019} is a naive way of
introducing an incrementing register into a model. This this theory implements that heuristic.\<close>
theory Increment_Reset
imports "../Inference"
begin
definition initialiseReg :: "transition \<Rightarrow> nat \<Rightarrow> transition" where
"initialiseReg t newReg = \<lparr>Label = Label t, Arity = Arity t, Guards = Guards t, Outputs = Outputs t, Updates = ((newReg, L (Num 0))#Updates t)\<rparr>"
definition "guardMatch t1 t2 = (\<exists>n n'. Guards t1 = [gexp.Eq (V (vname.I 0)) (L (Num n))] \<and> Guards t2 = [gexp.Eq (V (vname.I 0)) (L (Num n'))])"
definition "outputMatch t1 t2 = (\<exists>m m'. Outputs t1 = [L (Num m)] \<and> Outputs t2 = [L (Num m')])"
lemma guard_match_commute: "guardMatch t1 t2 = guardMatch t2 t1"
apply (simp add: guardMatch_def)
by auto
lemma guard_match_length:
"length (Guards t1) \<noteq> 1 \<or> length (Guards t2) \<noteq> 1 \<Longrightarrow> \<not> guardMatch t1 t2"
apply (simp add: guardMatch_def)
by auto
fun insert_increment :: update_modifier where
"insert_increment t1ID t2ID s new _ old check = (let
t1 = get_by_ids new t1ID;
t2 = get_by_ids new t2ID in
if guardMatch t1 t2 \<and> outputMatch t1 t2 then let
r = case max_reg new of None \<Rightarrow> 1 | Some r \<Rightarrow> r+ 1;
newReg = R r;
newT1 = \<lparr>Label = Label t1, Arity = Arity t1, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t1)\<rparr>;
newT2 = \<lparr>Label = Label t2, Arity = Arity t2, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t2)\<rparr>;
to_initialise = ffilter (\<lambda>(uid, (from, to), t). (to = dest t1ID new \<or> to = dest t2ID new) \<and> t \<noteq> t1 \<and> t \<noteq> t2) new;
initialisedTrans = fimage (\<lambda>(uid, (from, to), t). (uid, initialiseReg t r)) to_initialise;
initialised = replace_transitions new (sorted_list_of_fset initialisedTrans);
rep = replace_transitions new [(t1ID, newT1), (t2ID, newT2)]
in
if check (tm rep) then Some rep else None
else
None
)"
definition struct_replace_all :: "iEFSM \<Rightarrow> transition \<Rightarrow> transition \<Rightarrow> iEFSM" where
"struct_replace_all e old new = (let
to_replace = ffilter (\<lambda>(uid, (from, dest), t). same_structure t old) e;
replacements = fimage (\<lambda>(uid, (from, to), t). (uid, new)) to_replace
in
replace_transitions e (sorted_list_of_fset replacements))"
lemma output_match_symmetry: "(outputMatch t1 t2) = (outputMatch t2 t1)"
apply (simp add: outputMatch_def)
by auto
lemma guard_match_symmetry: "(guardMatch t1 t2) = (guardMatch t2 t1)"
apply (simp add: guardMatch_def)
by auto
fun insert_increment_2 :: update_modifier where
"insert_increment_2 t1ID t2ID s new _ old check = (let
t1 = get_by_ids new t1ID;
t2 = get_by_ids new t2ID in
if guardMatch t1 t2 \<and> outputMatch t1 t2 then let
r = case max_reg new of None \<Rightarrow> 1 | Some r \<Rightarrow> r + 1;
newReg = R r;
newT1 = \<lparr>Label = Label t1, Arity = Arity t1, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t1)\<rparr>;
newT2 = \<lparr>Label = Label t2, Arity = Arity t2, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t2)\<rparr>;
to_initialise = ffilter (\<lambda>(uid, (from, to), t). (to = dest t1ID new \<or> to = dest t2ID new) \<and> t \<noteq> t1 \<and> t \<noteq> t2) new;
initialisedTrans = fimage (\<lambda>(uid, (from, to), t). (uid, initialiseReg t r)) to_initialise;
initialised = replace_transitions new (sorted_list_of_fset initialisedTrans);
rep = struct_replace_all (struct_replace_all initialised t2 newT2) t1 newT1
in
if check (tm rep) then Some rep else None
else
None
)"
fun guardMatch_alt_2 :: "vname gexp list \<Rightarrow> bool" where
"guardMatch_alt_2 [(gexp.Eq (V (vname.I i)) (L (Num n)))] = (i = 1)" |
"guardMatch_alt_2 _ = False"
fun outputMatch_alt_2 :: "vname aexp list \<Rightarrow> bool" where
"outputMatch_alt_2 [(L (Num n))] = True" |
"outputMatch_alt_2 _ = False"
end

View File

@ -0,0 +1,955 @@
section\<open>Least Upper Bound\<close>
text\<open>The simplest way to merge a pair of transitions with identical outputs and updates is to
simply take the least upper bound of their \emph{guards}. This theory presents several variants on
this theme.\<close>
theory Least_Upper_Bound
imports "../Inference"
begin
fun literal_args :: "'a gexp \<Rightarrow> bool" where
"literal_args (Bc v) = False" |
"literal_args (Eq (V _) (L _)) = True" |
"literal_args (In _ _) = True" |
"literal_args (Eq _ _) = False" |
"literal_args (Gt va v) = False" |
"literal_args (Nor v va) = (literal_args v \<and> literal_args va)"
lemma literal_args_eq:
"literal_args (Eq a b) \<Longrightarrow> \<exists>v l. a = (V v) \<and> b = (L l)"
apply (cases a)
apply simp
apply (cases b)
by auto
definition "all_literal_args t = (\<forall>g \<in> set (Guards t). literal_args g)"
fun merge_in_eq :: "vname \<Rightarrow> value \<Rightarrow> vname gexp list \<Rightarrow> vname gexp list" where
"merge_in_eq v l [] = [Eq (V v) (L l)]" |
"merge_in_eq v l ((Eq (V v') (L l'))#t) = (if v = v' \<and> l \<noteq> l' then (In v [l, l'])#t else (Eq (V v') (L l'))#(merge_in_eq v l t))" |
"merge_in_eq v l ((In v' l')#t) = (if v = v' then (In v (remdups (l#l')))#t else (In v' l')#(merge_in_eq v l t))" |
"merge_in_eq v l (h#t) = h#(merge_in_eq v l t)"
fun merge_in_in :: "vname \<Rightarrow> value list \<Rightarrow> vname gexp list \<Rightarrow> vname gexp list" where
"merge_in_in v l [] = [In v l]" |
"merge_in_in v l ((Eq (V v') (L l'))#t) = (if v = v' then (In v (List.insert l' l))#t else (Eq (V v') (L l'))#(merge_in_in v l t))" |
"merge_in_in v l ((In v' l')#t) = (if v = v' then (In v (List.union l l'))#t else (In v' l')#(merge_in_in v l t))" |
"merge_in_in v l (h#t) = h#(merge_in_in v l t)"
fun merge_guards :: "vname gexp list \<Rightarrow> vname gexp list \<Rightarrow> vname gexp list" where
"merge_guards [] g2 = g2" |
"merge_guards ((Eq (V v) (L l))#t) g2 = merge_guards t (merge_in_eq v l g2)" |
"merge_guards ((In v l)#t) g2 = merge_guards t (merge_in_in v l g2)" |
"merge_guards (h#t) g2 = h#(merge_guards t g2)"
text\<open>The ``least upper bound'' (lob) heuristic simply disjoins the guards of two transitions with
identical outputs and updates.\<close>
definition lob_aux :: "transition \<Rightarrow> transition \<Rightarrow> transition option" where
"lob_aux t1 t2 = (if Outputs t1 = Outputs t2 \<and> Updates t1 = Updates t2 \<and> all_literal_args t1 \<and> all_literal_args t2 then
Some \<lparr>Label = Label t1, Arity = Arity t1, Guards = remdups (merge_guards (Guards t1) (Guards t2)), Outputs = Outputs t1, Updates = Updates t1\<rparr>
else None)"
fun lob :: update_modifier where
"lob t1ID t2ID s new _ old _ = (let
t1 = (get_by_ids new t1ID);
t2 = (get_by_ids new t2ID) in
case lob_aux t1 t2 of
None \<Rightarrow> None |
Some lob_t \<Rightarrow>
Some (replace_transitions new [(t1ID, lob_t), (t2ID, lob_t)])
)"
lemma lob_aux_some: "Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = Updates t2 \<Longrightarrow>
all_literal_args t1 \<Longrightarrow>
all_literal_args t2 \<Longrightarrow>
Label t = Label t1 \<Longrightarrow>
Arity t = Arity t1 \<Longrightarrow>
Guards t = remdups (merge_guards (Guards t1) (Guards t2)) \<Longrightarrow>
Outputs t = Outputs t1 \<Longrightarrow>
Updates t = Updates t1 \<Longrightarrow>
lob_aux t1 t2 = Some t"
by (simp add: lob_aux_def)
fun has_corresponding :: "vname gexp \<Rightarrow> vname gexp list \<Rightarrow> bool" where
"has_corresponding g [] = False" |
"has_corresponding (Eq (V v) (L l)) ((Eq (V v') (L l'))#t) = (if v = v' \<and> l = l' then True else has_corresponding (Eq (V v) (L l)) t)" |
"has_corresponding (In v' l') ((Eq (V v) (L l))#t) = (if v = v' \<and> l \<in> set l' then True else has_corresponding (In v' l') t)" |
"has_corresponding (In v l) ((In v' l')#t) = (if v = v' \<and> set l' \<subseteq> set l then True else has_corresponding (In v l) t)" |
"has_corresponding g (h#t) = has_corresponding g t"
lemma no_corresponding_bc: "\<not>has_corresponding (Bc x1) G1"
apply (induct G1)
by auto
lemma no_corresponding_gt: "\<not>has_corresponding (Gt x1 y1) G1"
apply (induct G1)
by auto
lemma no_corresponding_nor: "\<not>has_corresponding (Nor x1 y1) G1"
apply (induct G1)
by auto
lemma has_corresponding_eq: "has_corresponding (Eq x21 x22) G1 \<Longrightarrow> (Eq x21 x22) \<in> set G1"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (cases a)
apply simp
subgoal for x21a x22a
apply (case_tac "x21a")
apply simp
apply (case_tac "x22a")
apply clarify
apply simp
apply (case_tac "x21")
apply simp
apply (case_tac "x22")
apply (metis has_corresponding.simps(2))
by auto
by auto
qed auto
lemma has_corresponding_In: "has_corresponding (In v l) G1 \<Longrightarrow> (\<exists>l'. (In v l') \<in> set G1 \<and> set l' \<subseteq> set l) \<or> (\<exists>l' \<in> set l. (Eq (V v) (L l')) \<in> set G1)"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (cases a)
apply simp
defer
apply simp
apply simp
defer
apply simp
apply simp
subgoal for x21 x22 apply (case_tac x21)
apply simp
apply (case_tac x22)
apply fastforce
apply simp+
done
by metis
qed auto
lemma gval_each_one: "g \<in> set G \<Longrightarrow> apply_guards G s \<Longrightarrow> gval g s = true"
using apply_guards_cons apply_guards_rearrange by blast
lemma has_corresponding_apply_guards:
"\<forall>g\<in>set G2. has_corresponding g G1 \<Longrightarrow>
apply_guards G1 s \<Longrightarrow>
apply_guards G2 s"
proof(induct G2)
case (Cons a G2)
then show ?case
apply (cases a)
apply (simp add: no_corresponding_bc)
apply simp
apply (metis (full_types) has_corresponding_eq append_Cons append_self_conv2 apply_guards_append apply_guards_rearrange)
apply (simp add: no_corresponding_gt)
apply simp
subgoal for v l
apply (insert has_corresponding_In[of v l G1])
apply simp
apply (erule disjE)
apply clarsimp
subgoal for l'
apply (insert apply_guards_rearrange[of "In v l'" G1 s])
apply simp
apply (simp only: apply_guards_cons[of "In v l" G2])
apply (simp only: apply_guards_cons[of "In v l'" G1])
apply simp
apply (cases "s v")
apply simp
by force
apply clarsimp
subgoal for l'
apply (insert apply_guards_rearrange[of "Eq (V v) (L l')" G1 s])
apply simp
apply (simp only: apply_guards_cons[of "In v l" G2])
apply (simp only: apply_guards_cons[of "Eq (V v) (L l')" G1])
apply (cases "s v")
apply simp
apply simp
using trilean.distinct(1) by presburger
done
by (simp add: no_corresponding_nor)
qed auto
lemma correspondence_subsumption:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = Updates t2 \<Longrightarrow>
\<forall>g \<in> set (Guards t2). has_corresponding g (Guards t1) \<Longrightarrow>
subsumes t2 c t1"
by (simp add: can_take_def can_take_transition_def has_corresponding_apply_guards subsumption)
definition "is_lob t1 t2 = (
Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
Outputs t1 = Outputs t2 \<and>
Updates t1 = Updates t2 \<and>
(\<forall>g \<in> set (Guards t2). has_corresponding g (Guards t1)))"
lemma is_lob_direct_subsumption:
"is_lob t1 t2 \<Longrightarrow> directly_subsumes e1 e2 s s' t2 t1"
apply (rule subsumes_in_all_contexts_directly_subsumes)
by (simp add: is_lob_def correspondence_subsumption)
fun has_distinguishing :: "vname gexp \<Rightarrow> vname gexp list \<Rightarrow> bool" where
"has_distinguishing g [] = False" |
"has_distinguishing (Eq (V v) (L l)) ((Eq (V v') (L l'))#t) = (if v = v' \<and> l \<noteq> l' then True else has_distinguishing (Eq (V v) (L l)) t)" |
"has_distinguishing (In (I v') l') ((Eq (V (I v)) (L l))#t) = (if v = v' \<and> l \<notin> set l' then True else has_distinguishing (In (I v') l') t)" |
"has_distinguishing (In (I v) l) ((In (I v') l')#t) = (if v = v' \<and> set l' \<supset> set l then True else has_distinguishing (In (I v) l) t)" |
"has_distinguishing g (h#t) = has_distinguishing g t"
lemma has_distinguishing: "has_distinguishing g G \<Longrightarrow> (\<exists>v l. g = (Eq (V v) (L l))) \<or> (\<exists>v l. g = In v l)"
proof(induct G)
case (Cons a G)
then show ?case
apply (cases g)
apply simp
apply (case_tac x21)
apply simp
apply (case_tac x22)
by auto
qed auto
lemma has_distinguishing_Eq: "has_distinguishing (Eq (V v) (L l)) G \<Longrightarrow> \<exists>l'. (Eq (V v) (L l')) \<in> set G \<and> l \<noteq> l'"
proof (induct G)
case (Cons a G)
then show ?case
apply (cases a)
apply simp
apply (case_tac x21)
apply simp
apply (case_tac x22)
apply (metis has_distinguishing.simps(2) list.set_intros(1) list.set_intros(2))
by auto
qed auto
lemma ex_mutex: "Eq (V v) (L l) \<in> set G1 \<Longrightarrow>
Eq (V v) (L l') \<in> set G2 \<Longrightarrow>
l \<noteq> l' \<Longrightarrow>
apply_guards G1 s \<Longrightarrow>
\<not> apply_guards G2 s"
apply (simp add: apply_guards_def Bex_def)
apply (rule_tac x="Eq (V v) (L l')" in exI)
apply simp
apply (case_tac "s v")
by auto
lemma has_distinguishing_In:
"has_distinguishing (In v l) G \<Longrightarrow>
(\<exists>l' i. v = I i \<and> Eq (V v) (L l') \<in> set G \<and> l' \<notin> set l) \<or> (\<exists>l' i. v = I i \<and> In v l' \<in> set G \<and> set l' \<supset> set l)"
proof(induct G)
case (Cons a G)
then show ?case
apply (case_tac v)
subgoal for x
apply simp
apply (cases a)
apply simp
subgoal for x21 x22
apply (case_tac x21)
apply simp
apply (case_tac x22)
apply (case_tac x2)
apply fastforce
apply simp+
done
subgoal by simp
subgoal for x41
apply (case_tac x41)
apply (simp, metis)
by auto
by auto
by auto
qed auto
lemma Eq_apply_guards:
"Eq (V v) (L l) \<in> set G1 \<Longrightarrow>
apply_guards G1 s \<Longrightarrow>
s v = Some l"
apply (simp add: apply_guards_rearrange)
apply (simp add: apply_guards_cons)
apply (cases "s v")
apply simp
apply simp
using trilean.distinct(1) by presburger
lemma In_neq_apply_guards:
"In v l \<in> set G2 \<Longrightarrow>
Eq (V v) (L l') \<in> set G1 \<Longrightarrow>
l' \<notin> set l \<Longrightarrow>
apply_guards G1 s \<Longrightarrow>
\<not>apply_guards G2 s"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (simp add: apply_guards_def Bex_def)
apply (rule_tac x="In v l" in exI)
using Eq_apply_guards[of v l' "a#G1" s]
by (simp add: Cons.prems(4) image_iff)
qed auto
lemma In_apply_guards: "In v l \<in> set G1 \<Longrightarrow> apply_guards G1 s \<Longrightarrow> \<exists>v' \<in> set l. s v = Some v'"
apply (simp add: apply_guards_rearrange)
apply (simp add: apply_guards_cons)
apply (cases "s v")
apply simp
apply simp
by (meson image_iff trilean.simps(2))
lemma input_not_constrained_aval_swap_inputs:
"\<not> aexp_constrains a (V (I v)) \<Longrightarrow>
aval a (join_ir i c) = aval a (join_ir (list_update i v x) c)"
apply(induct a rule: aexp_induct_separate_V_cases)
apply simp
apply (metis aexp_constrains.simps(2) aval.simps(2) input2state_nth input2state_out_of_bounds join_ir_def length_list_update not_le nth_list_update_neq vname.simps(5))
using join_ir_def by auto
lemma input_not_constrained_gval_swap_inputs:
"\<not> gexp_constrains a (V (I v)) \<Longrightarrow>
gval a (join_ir i c) = gval a (join_ir (i[v := x]) c)"
proof(induct a)
case (Bc x)
then show ?case
by (metis (full_types) gval.simps(1) gval.simps(2))
next
case (Eq x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (Gt x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (In x1a x2)
then show ?case
apply simp
apply (case_tac "join_ir i c x1a")
apply (case_tac "join_ir (i[v := x]) c x1a")
apply simp
apply (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs option.discI)
apply (case_tac "join_ir (i[v := x]) c x1a")
apply (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs option.discI)
by (metis In.prems aval.simps(2) gexp_constrains.simps(5) input_not_constrained_aval_swap_inputs)
qed auto
lemma test_aux: "\<forall>g\<in>set (removeAll (In (I v) l) G1). \<not> gexp_constrains g (V (I v)) \<Longrightarrow>
apply_guards G1 (join_ir i c) \<Longrightarrow>
x \<in> set l \<Longrightarrow>
apply_guards G1 (join_ir (i[v := x]) c)"
proof(induct G1)
case (Cons a G1)
then show ?case
apply (simp only: apply_guards_cons)
apply (case_tac "a = In (I v) l")
apply simp
apply (case_tac "join_ir i c (I v)")
apply simp
apply (case_tac "join_ir (i[v := x]) c (I v)")
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI)
apply simp
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond nth_list_update_eq option.inject trilean.distinct(1))
apply (case_tac "join_ir (i[v := x]) c (I v)")
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI)
apply simp
using input_not_constrained_gval_swap_inputs by auto
qed auto
lemma test:
assumes
p1: "In (I v) l \<in> set G2" and
p2: "In (I v) l' \<in> set G1" and
p3: "x \<in> set l'" and
p4: "x \<notin> set l" and
p5: "apply_guards G1 (join_ir i c)" and
p6: "length i = a" and
p7: "\<forall>g \<in> set (removeAll (In (I v) l') G1). \<not> gexp_constrains g (V (I v))"
shows "\<exists>i. length i = a \<and> apply_guards G1 (join_ir i c) \<and> (length i = a \<longrightarrow> \<not> apply_guards G2 (join_ir i c))"
apply (rule_tac x="list_update i v x" in exI)
apply standard
apply (simp add: p6)
apply standard
using p3 p5 p7 test_aux apply blast
using p1 p4
apply (simp add: apply_guards_rearrange)
apply (simp add: apply_guards_cons join_ir_def)
apply (case_tac "input2state (i[v := x]) $ v")
apply simp
apply simp
by (metis input2state_nth input2state_within_bounds length_list_update nth_list_update_eq option.inject)
definition get_Ins :: "vname gexp list \<Rightarrow> (nat \<times> value list) list" where
"get_Ins G = map (\<lambda>g. case g of (In (I v) l) \<Rightarrow> (v, l)) (filter (\<lambda>g. case g of (In (I _) _ ) \<Rightarrow> True | _ \<Rightarrow> False) G)"
lemma get_Ins_Cons_equiv: "\<nexists>v l. a = In (I v) l \<Longrightarrow> get_Ins (a # G) = get_Ins G"
apply (simp add: get_Ins_def)
apply (cases a)
apply simp+
apply (metis (full_types) vname.exhaust vname.simps(6))
by simp
lemma Ball_Cons: "(\<forall>x \<in> set (a#l). P x) = (P a \<and> (\<forall>x \<in> set l. P x))"
by simp
lemma In_in_get_Ins: "(In (I v) l \<in> set G) = ((v, l) \<in> set (get_Ins G))"
proof(induct G)
case Nil
then show ?case
by (simp add: get_Ins_def)
next
case (Cons a G)
then show ?case
apply (simp add: get_Ins_def)
apply (cases a)
apply simp+
subgoal for x by (case_tac x, auto)
apply auto
done
qed
definition "check_get_Ins G = (\<forall>(v, l') \<in> set (get_Ins G). \<forall>g \<in> set (removeAll (In (I v) l') G). \<not> gexp_constrains g (V (I v)))"
lemma no_Ins: "[] = get_Ins G \<Longrightarrow> set G - {In (I i) l} = set G"
proof(induct G)
case (Cons a G)
then show ?case
apply (cases a)
apply (simp add: get_Ins_Cons_equiv insert_Diff_if)+
subgoal for x41 x42
apply (case_tac x41)
apply simp
apply (metis In_in_get_Ins equals0D list.set(1) list.set_intros(1))
apply (simp add: get_Ins_Cons_equiv)
done
by (simp add: get_Ins_Cons_equiv insert_Diff_if)
qed auto
lemma test2: "In (I i) l \<in> set (Guards t2) \<Longrightarrow>
In (I i) l' \<in> set (Guards t1) \<Longrightarrow>
length ia = Arity t1 \<Longrightarrow>
apply_guards (Guards t1) (join_ir ia c) \<Longrightarrow>
x \<in> set l' \<Longrightarrow>
x \<notin> set l \<Longrightarrow>
\<forall>(v, l')\<in>insert (0, []) (set (get_Ins (Guards t1))). \<forall>g\<in>set (removeAll (In (I v) l') (Guards t1)). \<not> gexp_constrains g (V (I v)) \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
\<exists>i. length i = Arity t2 \<and> apply_guards (Guards t1) (join_ir i c) \<and> (length i = Arity t2 \<longrightarrow> \<not> apply_guards (Guards t2) (join_ir i c))"
using test[of i l "Guards t2" l' "Guards t1" x ia c "Arity t2"]
apply simp
apply (case_tac "\<forall>g\<in>set (Guards t1) - {In (I i) l'}. \<not> gexp_constrains g (V (I i))")
apply simp
apply simp
using In_in_get_Ins by blast
lemma distinguishing_subsumption:
assumes
p1: "\<exists>g \<in> set (Guards t2). has_distinguishing g (Guards t1)" and
p2: "Arity t1 = Arity t2" and
p3: "\<exists>i. can_take_transition t1 i c" and
p4: "(\<forall>(v, l') \<in> insert (0, []) (set (get_Ins (Guards t1))). \<forall>g \<in> set (removeAll (In (I v) l') (Guards t1)). \<not> gexp_constrains g (V (I v)))"
shows
"\<not> subsumes t2 c t1"
proof-
show ?thesis
apply (rule bad_guards)
apply (simp add: can_take_transition_def can_take_def p2)
apply (insert p1, simp add: Bex_def)
apply (erule exE)
apply (case_tac "\<exists>v l. x = (Eq (V v) (L l))")
apply (metis can_take_def can_take_transition_def ex_mutex p2 p3 has_distinguishing_Eq)
apply (case_tac "\<exists>v l. x = In v l")
defer
using has_distinguishing apply blast
apply clarify
apply (case_tac "\<exists>l' i. v = I i \<and> Eq (V v) (L l') \<in> set (Guards t1) \<and> l' \<notin> set l")
apply (metis In_neq_apply_guards can_take_def can_take_transition_def p2 p3)
apply (case_tac "(\<exists>l' i. v = I i \<and> In v l' \<in> set (Guards t1) \<and> set l' \<supset> set l)")
defer
using has_distinguishing_In apply blast
apply simp
apply (erule conjE)
apply (erule exE)+
apply (erule conjE)
apply (insert p3, simp only: can_take_transition_def can_take_def)
apply (case_tac "\<exists>x. x \<in> set l' \<and> x \<notin> set l")
apply (erule exE)+
apply (erule conjE)+
apply (insert p4 p2)
using test2
apply blast
by auto
qed
definition "lob_distinguished t1 t2 = (
(\<exists>g \<in> set (Guards t2). has_distinguishing g (Guards t1)) \<and>
Arity t1 = Arity t2 \<and>
(\<forall>(v, l') \<in> insert (0, []) (set (get_Ins (Guards t1))). \<forall>g \<in> set (removeAll (In (I v) l') (Guards t1)). \<not> gexp_constrains g (V (I v))))"
lemma must_be_another:
"1 < size (fset_of_list b) \<Longrightarrow>
x \<in> set b \<Longrightarrow>
\<exists>x' \<in> set b. x \<noteq> x'"
proof(induct b)
case (Cons a b)
then show ?case
apply (simp add: Bex_def)
by (metis List.finite_set One_nat_def card.insert card_gt_0_iff card_mono fset_of_list.rep_eq insert_absorb le_0_eq less_nat_zero_code less_numeral_extra(4) not_less_iff_gr_or_eq set_empty2 subsetI)
qed auto
lemma another_swap_inputs:
"apply_guards G (join_ir i c) \<Longrightarrow>
filter (\<lambda>g. gexp_constrains g (V (I a))) G = [In (I a) b] \<Longrightarrow>
xa \<in> set b \<Longrightarrow>
apply_guards G (join_ir (i[a := xa]) c)"
proof(induct G)
case (Cons g G)
then show ?case
apply (simp add: apply_guards_cons)
apply (case_tac "gexp_constrains g (V (I a))")
defer
using input_not_constrained_gval_swap_inputs apply auto[1]
apply simp
apply (case_tac "join_ir i c (I a) \<in> Some ` set b")
defer
apply simp
apply clarify
apply standard
using apply_guards_def input_not_constrained_gval_swap_inputs
apply (simp add: filter_empty_conv)
apply (case_tac "join_ir i c (I a)")
apply simp
apply (case_tac "join_ir (i[a := xa]) c (I a)")
apply simp
apply (metis image_eqI trilean.distinct(1))
apply simp
apply (metis image_eqI trilean.distinct(1))
apply (case_tac "join_ir i c (I a)")
apply simp
apply simp
apply (metis image_eqI trilean.distinct(1))
apply (case_tac "join_ir i c (I a)")
apply simp
apply (case_tac "join_ir (i[a := xa]) c (I a)")
apply simp
apply (metis join_ir_nth le_less_linear length_list_update list_update_beyond option.discI)
apply simp
apply standard
apply (metis (no_types, lifting) Cons.hyps Cons.prems(2) filter_empty_conv removeAll_id set_ConsD test_aux)
by (metis in_these_eq join_ir_nth le_less_linear length_list_update list_update_beyond nth_list_update_eq these_image_Some_eq)
qed auto
lemma lob_distinguished_2_not_subsumes:
"\<exists>(i, l) \<in> set (get_Ins (Guards t2)). filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] \<and>
(\<exists>l' \<in> set l. i < Arity t1 \<and> Eq (V (I i)) (L l') \<in> set (Guards t1) \<and> size (fset_of_list l) > 1) \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
\<exists>i. can_take_transition t2 i c \<Longrightarrow>
\<not> subsumes t1 c t2"
apply (rule bad_guards)
apply simp
apply (simp add: can_take_def can_take_transition_def Bex_def)
apply clarify
apply (case_tac "\<exists>x' \<in> set b. x \<noteq> x'")
defer
apply (simp add: must_be_another)
apply (simp add: Bex_def)
apply (erule exE)
apply (rule_tac x="list_update i a xa" in exI)
apply simp
apply standard
apply (simp add: another_swap_inputs)
by (metis Eq_apply_guards input2state_nth join_ir_def length_list_update nth_list_update_eq option.inject vname.simps(5))
definition "lob_distinguished_2 t1 t2 =
(\<exists>(i, l) \<in> set (get_Ins (Guards t2)). filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] \<and>
(\<exists>l' \<in> set l. i < Arity t1 \<and> Eq (V (I i)) (L l') \<in> set (Guards t1) \<and> size (fset_of_list l) > 1) \<and>
Arity t1 = Arity t2)"
lemma lob_distinguished_3_not_subsumes:
"\<exists>(i, l) \<in> set (get_Ins (Guards t2)). filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] \<and>
(\<exists>(i', l') \<in> set (get_Ins (Guards t1)). i = i' \<and> set l' \<subset> set l) \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
\<exists>i. can_take_transition t2 i c \<Longrightarrow>
\<not> subsumes t1 c t2"
apply (rule bad_guards)
apply simp
apply (simp add: can_take_def can_take_transition_def Bex_def)
apply (erule exE)+
apply (erule conjE)+
apply (erule exE)+
apply (erule conjE)+
apply (case_tac "\<exists>x. x \<in> set b \<and> x \<notin> set ba")
defer
apply auto[1]
apply (erule exE)+
apply (erule conjE)+
apply (rule_tac x="list_update i a x" in exI)
apply simp
apply standard
using another_swap_inputs apply blast
by (metis In_apply_guards In_in_get_Ins input2state_not_None input2state_nth join_ir_def nth_list_update_eq option.distinct(1) option.inject vname.simps(5))
definition "lob_distinguished_3 t1 t2 = (\<exists>(i, l) \<in> set (get_Ins (Guards t2)). filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2) = [(In (I i) l)] \<and>
(\<exists>(i', l') \<in> set (get_Ins (Guards t1)). i = i' \<and> set l' \<subset> set l) \<and>
Arity t1 = Arity t2)"
fun is_In :: "'a gexp \<Rightarrow> bool" where
"is_In (In _ _) = True" |
"is_In _ = False"
text\<open>The ``greatest upper bound'' (gob) heuristic is similar to \texttt{lob} but applies a more
intellegent approach to guard merging.\<close>
definition gob_aux :: "transition \<Rightarrow> transition \<Rightarrow> transition option" where
"gob_aux t1 t2 = (if Outputs t1 = Outputs t2 \<and> Updates t1 = Updates t2 \<and> all_literal_args t1 \<and> all_literal_args t2 then
Some \<lparr>Label = Label t1, Arity = Arity t1, Guards = remdups (filter (Not \<circ> is_In) (merge_guards (Guards t1) (Guards t2))), Outputs = Outputs t1, Updates = Updates t1\<rparr>
else None)"
fun gob :: update_modifier where
"gob t1ID t2ID s new _ old _ = (let
t1 = (get_by_ids new t1ID);
t2 = (get_by_ids new t2ID) in
case gob_aux t1 t2 of
None \<Rightarrow> None |
Some gob_t \<Rightarrow>
Some (replace_transitions new [(t1ID, gob_t), (t2ID, gob_t)])
)"
text\<open>The ``Gung Ho'' heuristic simply drops the guards of both transitions, making them identical.\<close>
definition gung_ho_aux :: "transition \<Rightarrow> transition \<Rightarrow> transition option" where
"gung_ho_aux t1 t2 = (if Outputs t1 = Outputs t2 \<and> Updates t1 = Updates t2 \<and> all_literal_args t1 \<and> all_literal_args t2 then
Some \<lparr>Label = Label t1, Arity = Arity t1, Guards = [], Outputs = Outputs t1, Updates = Updates t1\<rparr>
else None)"
fun gung_ho :: update_modifier where
"gung_ho t1ID t2ID s new _ old _ = (let
t1 = (get_by_ids new t1ID);
t2 = (get_by_ids new t2ID) in
case gung_ho_aux t1 t2 of
None \<Rightarrow> None |
Some gob_t \<Rightarrow>
Some (replace_transitions new [(t1ID, gob_t), (t2ID, gob_t)])
)"
lemma guard_subset_eq_outputs_updates_subsumption:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = Updates t2 \<Longrightarrow>
set (Guards t2) \<subseteq> set (Guards t1) \<Longrightarrow>
subsumes t2 c t1"
apply (simp add: subsumes_def)
by (meson can_take_def can_take_subset can_take_transition_def)
lemma guard_subset_eq_outputs_updates_direct_subsumption:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = Updates t2 \<Longrightarrow>
set (Guards t2) \<subseteq> set (Guards t1) \<Longrightarrow>
directly_subsumes m1 m2 s1 s2 t2 t1"
apply (rule subsumes_in_all_contexts_directly_subsumes)
by (simp add: guard_subset_eq_outputs_updates_subsumption)
lemma unconstrained_input:
"\<forall>g\<in>set G. \<not> gexp_constrains g (V (I i)) \<Longrightarrow>
apply_guards G (join_ir ia c) \<Longrightarrow>
apply_guards G (join_ir (ia[i := x']) c)"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp add: apply_guards_cons)
using input_not_constrained_gval_swap_inputs[of a i ia c x']
by simp
qed auto
lemma each_input_guarded_once_cons:
"\<forall>i\<in>\<Union> (enumerate_gexp_inputs ` set (a # G)). length (filter (\<lambda>g. gexp_constrains g (V (I i))) (a # G)) \<le> 1 \<Longrightarrow>
\<forall>i\<in>\<Union> (enumerate_gexp_inputs ` set G). length (filter (\<lambda>g. gexp_constrains g (V (I i))) G) \<le> 1"
apply (simp add: Ball_def)
apply clarify
proof -
fix x :: nat and xa :: "vname gexp"
assume a1: "\<forall>x. (x \<in> enumerate_gexp_inputs a \<longrightarrow> length (if gexp_constrains a (V (I x)) then a # filter (\<lambda>g. gexp_constrains g (V (I x))) G else filter (\<lambda>g. gexp_constrains g (V (I x))) G) \<le> 1) \<and> ((\<exists>xa\<in>set G. x \<in> enumerate_gexp_inputs xa) \<longrightarrow> length (if gexp_constrains a (V (I x)) then a # filter (\<lambda>g. gexp_constrains g (V (I x))) G else filter (\<lambda>g. gexp_constrains g (V (I x))) G) \<le> 1)"
assume a2: "xa \<in> set G"
assume "x \<in> enumerate_gexp_inputs xa"
then have "if gexp_constrains a (V (I x)) then length (a # filter (\<lambda>g. gexp_constrains g (V (I x))) G) \<le> 1 else length (filter (\<lambda>g. gexp_constrains g (V (I x))) G) \<le> 1"
using a2 a1 by fastforce
then show "length (filter (\<lambda>g. gexp_constrains g (V (I x))) G) \<le> 1"
by (metis (no_types) impossible_Cons le_cases order.trans)
qed
lemma literal_args_can_take:
"\<forall>g\<in>set G. \<exists>i v s. g = Eq (V (I i)) (L v) \<or> g = In (I i) s \<and> s \<noteq> [] \<Longrightarrow>
\<forall>i\<in>\<Union> (enumerate_gexp_inputs ` set G). i < a \<Longrightarrow>
\<forall>i\<in>\<Union> (enumerate_gexp_inputs ` set G). length (filter (\<lambda>g. gexp_constrains g (V (I i))) G) \<le> 1 \<Longrightarrow>
\<exists>i. length i = a \<and> apply_guards G (join_ir i c)"
proof(induct G)
case Nil
then show ?case
using Ex_list_of_length
by auto
next
case (Cons a G)
then show ?case
apply simp
apply (case_tac "\<forall>y\<in>set G. \<forall>i\<in>enumerate_gexp_inputs y. length (filter (\<lambda>g. gexp_constrains g (V (I i))) G) \<le> 1")
defer
using each_input_guarded_once_cons apply auto[1]
apply (simp add: ball_Un)
apply clarsimp
apply (induct a)
apply simp
apply simp
subgoal for _ x2 i ia
apply (case_tac x2)
apply (rule_tac x="list_update i ia x1" in exI)
apply (simp add: apply_guards_cons unconstrained_input filter_empty_conv)
apply simp+
done
apply simp
subgoal for _ x2 i ia
apply (case_tac x2)
apply simp
subgoal for aa
apply (rule_tac x="list_update i ia aa" in exI)
apply (simp add: apply_guards_cons unconstrained_input filter_empty_conv)
done
done
by simp
qed
lemma "(SOME x'. x' \<noteq> (v::value)) \<noteq> v"
proof(induct v)
case (Num x)
then show ?case
by (metis (full_types) someI_ex value.simps(4))
next
case (Str x)
then show ?case
by (metis (full_types) someI_ex value.simps(4))
qed
lemma opposite_gob_subsumption: "\<forall>g \<in> set (Guards t1). \<exists>i v s. g = Eq (V (I i)) (L v) \<or> (g = In (I i) s \<and> s \<noteq> []) \<Longrightarrow>
\<forall>g \<in> set (Guards t2). \<exists>i v s. g = Eq (V (I i)) (L v) \<or> (g = In (I i) s \<and> s \<noteq> []) \<Longrightarrow>
\<exists> i. \<exists>v. Eq (V (I i)) (L v) \<in> set (Guards t1) \<and>
(\<forall>g \<in> set (Guards t2). \<not> gexp_constrains g (V (I i))) \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
\<forall>i \<in> enumerate_inputs t2. i < Arity t2 \<Longrightarrow>
\<forall>i \<in> enumerate_inputs t2. length (filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2)) \<le> 1 \<Longrightarrow>
\<not> subsumes t1 c t2"
apply (rule bad_guards)
apply (simp add: enumerate_inputs_def can_take_transition_def can_take_def Bex_def)
using literal_args_can_take[of "Guards t2" "Arity t2" c]
apply simp
apply clarify
subgoal for i ia v
apply (rule_tac x="list_update ia i (Eps (\<lambda>x'. x' \<noteq> v))" in exI)
apply simp
apply standard
apply (simp add: apply_guards_def)
using input_not_constrained_gval_swap_inputs apply simp
apply (simp add: apply_guards_def Bex_def)
apply (rule_tac x="Eq (V (I i)) (L v)" in exI)
apply (simp add: join_ir_def)
apply (case_tac "input2state (ia[i := SOME x'. x' \<noteq> v]) $ i")
apply simp
apply simp
apply (case_tac "i < length ia")
apply (simp add: input2state_nth)
apply (case_tac v)
apply (metis (mono_tags) someI_ex value.simps(4))
apply (metis (mono_tags) someI_ex value.simps(4))
by (metis input2state_within_bounds length_list_update)
done
fun is_lit_eq :: "vname gexp \<Rightarrow> nat \<Rightarrow> bool" where
"is_lit_eq (Eq (V (I i)) (L v)) i' = (i = i')" |
"is_lit_eq _ _ = False"
lemma "(\<exists>v. Eq (V (I i)) (L v) \<in> set G) = (\<exists>g \<in> set G. is_lit_eq g i)"
by (metis is_lit_eq.elims(2) is_lit_eq.simps(1))
fun is_lit_eq_general :: "vname gexp \<Rightarrow> bool" where
"is_lit_eq_general (Eq (V (I _)) (L _)) = True" |
"is_lit_eq_general _ = False"
fun is_input_in :: "vname gexp \<Rightarrow> bool" where
"is_input_in (In (I i) s) = (s \<noteq> [])" |
"is_input_in _ = False"
definition "opposite_gob t1 t2 = (
(\<forall>g \<in> set (Guards t1). is_lit_eq_general g \<or> is_input_in g) \<and>
(\<forall>g \<in> set (Guards t2). is_lit_eq_general g \<or> is_input_in g) \<and>
(\<exists> i \<in> (enumerate_inputs t1 \<union> enumerate_inputs t2). (\<exists>g \<in> set (Guards t1). is_lit_eq g i) \<and>
(\<forall>g \<in> set (Guards t2). \<not> gexp_constrains g (V (I i)))) \<and>
Arity t1 = Arity t2 \<and>
(\<forall>i \<in> enumerate_inputs t2. i < Arity t2) \<and>
(\<forall>i \<in> enumerate_inputs t2. length (filter (\<lambda>g. gexp_constrains g (V (I i))) (Guards t2)) \<le> 1))"
lemma "is_lit_eq_general g \<or> is_input_in g \<Longrightarrow>
\<exists>i v s. g = Eq (V (I i)) (L v) \<or> g = In (I i) s \<and> s \<noteq> []"
by (meson is_input_in.elims(2) is_lit_eq_general.elims(2))
lemma opposite_gob_directly_subsumption:
"opposite_gob t1 t2 \<Longrightarrow> \<not> subsumes t1 c t2"
apply (rule opposite_gob_subsumption)
unfolding opposite_gob_def
apply (meson is_input_in.elims(2) is_lit_eq_general.elims(2))+
apply (metis is_lit_eq.elims(2))
by auto
fun get_in :: "'a gexp \<Rightarrow> ('a \<times> value list) option" where
"get_in (In v s) = Some (v, s)" |
"get_in _ = None"
lemma not_subset_not_in: "(\<not> s1 \<subseteq> s2) = (\<exists>i. i \<in> s1 \<and> i \<notin> s2)"
by auto
lemma get_in_is: "(get_in x = Some (v, s1)) = (x = In v s1)"
by (induct x, auto)
lemma gval_rearrange:
"g \<in> set G \<Longrightarrow>
gval g s = true \<Longrightarrow>
apply_guards (removeAll g G) s \<Longrightarrow>
apply_guards G s"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp only: apply_guards_cons)
apply standard
apply (metis apply_guards_cons removeAll.simps(2))
by (metis apply_guards_cons removeAll.simps(2) removeAll_id)
qed auto
lemma singleton_list: "(length l = 1) = (\<exists>e. l = [e])"
by (induct l, auto)
lemma remove_restricted:
"g \<in> set G \<Longrightarrow>
gexp_constrains g (V v) \<Longrightarrow>
restricted_once v G \<Longrightarrow>
not_restricted v (removeAll g G)"
apply (simp add: restricted_once_def not_restricted_def singleton_list)
apply clarify
subgoal for e
apply (case_tac "e = g")
defer
apply (metis (no_types, lifting) DiffE Diff_insert_absorb Set.set_insert empty_set filter.simps(2) filter_append in_set_conv_decomp insert_iff list.set(2))
apply (simp add: filter_empty_conv)
proof -
fix e :: "'a gexp"
assume "filter (\<lambda>g. gexp_constrains g (V v)) G = [g]"
then have "{g \<in> set G. gexp_constrains g (V v)} = {g}"
by (metis (no_types) empty_set list.simps(15) set_filter)
then show "\<forall>g\<in>set G - {g}. \<not> gexp_constrains g (V v)"
by blast
qed
done
lemma unrestricted_input_swap:
"not_restricted (I i) G \<Longrightarrow>
apply_guards G (join_ir iaa c) \<Longrightarrow>
apply_guards (removeAll g G) (join_ir (iaa[i := ia]) c)"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp add: apply_guards_cons not_restricted_def)
apply safe
apply (meson neq_Nil_conv)
apply (metis input_not_constrained_gval_swap_inputs list.distinct(1))
by (metis list.distinct(1))
qed auto
lemma apply_guards_remove_restricted:
"g \<in> set G \<Longrightarrow>
gexp_constrains g (V (I i)) \<Longrightarrow>
restricted_once (I i) G \<Longrightarrow>
apply_guards G (join_ir iaa c) \<Longrightarrow>
apply_guards (removeAll g G) (join_ir (iaa[i := ia]) c)"
proof(induct G)
case (Cons a G)
then show ?case
apply simp
apply safe
apply (rule unrestricted_input_swap)
apply (simp add: not_restricted_def restricted_once_def)
apply (meson apply_guards_subset set_subset_Cons)
apply (simp add: apply_guards_rearrange not_restricted_def restricted_once_def unrestricted_input_swap)
by (metis apply_guards_cons filter.simps(2) filter_empty_conv input_not_constrained_gval_swap_inputs list.inject restricted_once_def singleton_list)
qed auto
lemma In_swap_inputs:
"In (I i) s2 \<in> set G \<Longrightarrow>
restricted_once (I i) G \<Longrightarrow>
ia \<in> set s2 \<Longrightarrow>
apply_guards G (join_ir iaa c) \<Longrightarrow>
apply_guards G (join_ir (iaa[i := ia]) c)"
using apply_guards_remove_restricted[of "In (I i) s2" G i iaa c ia]
apply simp
apply (rule gval_rearrange[of "In (I i) s2"])
apply simp
apply (metis filter_empty_conv gval_each_one input_not_constrained_gval_swap_inputs length_0_conv not_restricted_def remove_restricted test_aux)
by blast
definition these :: "'a option list \<Rightarrow> 'a list" where
"these as = map (\<lambda>x. case x of Some y \<Rightarrow> y) (filter (\<lambda>x. x \<noteq> None) as)"
lemma these_cons: "these (a#as) = (case a of None \<Rightarrow> these as | Some x \<Rightarrow> x#(these as))"
apply (cases a)
apply (simp add: these_def)
by (simp add: these_def)
definition get_ins :: "vname gexp list \<Rightarrow> (nat \<times> value list) list" where
"get_ins g = map (\<lambda>(v, s). case v of I i \<Rightarrow> (i, s)) (filter (\<lambda>(v, _). case v of I _ \<Rightarrow> True | R _ \<Rightarrow> False) (these (map get_in g)))"
lemma in_get_ins:
"(I x1a, b) \<in> set (these (map get_in G)) \<Longrightarrow>
In (I x1a) b \<in> set G"
proof(induct G)
case Nil
then show ?case
by (simp add: these_def)
next
case (Cons a G)
then show ?case
apply simp
apply (simp add: these_cons)
apply (cases a)
by auto
qed
lemma restricted_head: "\<forall>v. restricted_once v (Eq (V x2) (L x1) # G) \<or> not_restricted v (Eq (V x2) (L x1) # G) \<Longrightarrow>
not_restricted x2 G"
apply (erule_tac x=x2 in allE)
by (simp add: restricted_once_def not_restricted_def)
fun atomic :: "'a gexp \<Rightarrow> bool" where
"atomic (Eq (V _) (L _)) = True" |
"atomic (In _ _) = True" |
"atomic _ = False"
lemma restricted_max_once_cons: "\<forall>v. restricted_once v (g#gs) \<or> not_restricted v (g#gs) \<Longrightarrow>
\<forall>v. restricted_once v gs \<or> not_restricted v gs"
apply (simp add: restricted_once_def not_restricted_def)
apply safe
subgoal for v
by (erule_tac x=v in allE)
(metis (mono_tags, lifting) list.distinct(1) list.inject singleton_list)
done
lemma not_restricted_swap_inputs:
"not_restricted (I x1a) G \<Longrightarrow>
apply_guards G (join_ir i r) \<Longrightarrow>
apply_guards G (join_ir (i[x1a := x1]) r)"
proof(induct G)
case (Cons a G)
then show ?case
apply (simp add: apply_guards_cons not_restricted_cons)
using input_not_constrained_gval_swap_inputs by auto
qed auto
end

View File

@ -0,0 +1,549 @@
section\<open>PTA Generalisation\<close>
text\<open>The problem with the simplistic heuristics of \cite{foster2019} is that the performance of the
Inference technique is almost entirely dependent on the quality and applicability of the heuristics
provided to it. Producing high quality heuristics often requires some inside knowledge of the system
under inference. If the user has this knowledge already, they are unlikely to require automated
inference. Ideally, we would like something more generally applicable. This theory presents a more
abstract \emph{metaheuristic} which can be implemented with genetic programming.\<close>
theory PTA_Generalisation
imports "../Inference" Same_Register Group_By
begin
hide_const I
datatype value_type = N | S
instantiation value_type :: linorder begin
fun less_value_type :: "value_type \<Rightarrow> value_type \<Rightarrow> bool" where
"less_value_type N S = True" |
"less_value_type _ _ = False"
definition less_eq_value_type :: "value_type \<Rightarrow> value_type \<Rightarrow> bool" where
"less_eq_value_type v1 v2 \<equiv> (v1 < v2 \<or> v1 = v2)"
instance
apply standard
using less_eq_value_type_def less_value_type.elims(2) apply blast
apply (simp add: less_eq_value_type_def)
apply (metis less_eq_value_type_def value_type.exhaust)
using less_eq_value_type_def less_value_type.elims(2) apply blast
by (metis less_eq_value_type_def less_value_type.elims(3) value_type.simps(2))
end
\<comment> \<open>This is a very hacky way of making sure that things with differently typed outputs don't get
lumped together.\<close>
fun typeSig :: "output_function \<Rightarrow> value_type" where
"typeSig (L (value.Str _)) = S" |
"typeSig _ = N"
definition same_structure :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
"same_structure t1 t2 = (
Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
map typeSig (Outputs t1) = map typeSig (Outputs t2)
)"
lemma same_structure_equiv:
"Outputs t1 = [L (Num m)] \<Longrightarrow> Outputs t2 = [L (Num n)] \<Longrightarrow>
same_structure t1 t2 = Transition.same_structure t1 t2"
by (simp add: same_structure_def Transition.same_structure_def)
type_synonym transition_group = "(tids \<times> transition) list"
fun observe_all :: "iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> transition_group" where
"observe_all _ _ _ [] = []" |
"observe_all e s r ((l, i, _)#es) =
(case random_member (i_possible_steps e s r l i) of
(Some (ids, s', t)) \<Rightarrow> (((ids, t)#(observe_all e s' (evaluate_updates t i r) es))) |
_ \<Rightarrow> []
)"
definition transition_groups_exec :: "iEFSM \<Rightarrow> trace \<Rightarrow> (nat \<times> tids \<times> transition) list list" where
"transition_groups_exec e t = group_by (\<lambda>(_, _, t1) (_, _, t2). same_structure t1 t2) (enumerate 0 (observe_all e 0 <> t))"
type_synonym struct = "(label \<times> arity \<times> value_type list)"
text\<open>We need to take the list of transition groups and tag them with the last transition that was
taken which had a different structure.\<close>
fun tag :: "struct option \<Rightarrow> (nat \<times> tids \<times> transition) list list \<Rightarrow> (struct option \<times> struct \<times> (nat \<times> tids \<times> transition) list) list" where
"tag _ [] = []" |
"tag t (g#gs) = (
let
(_, _, head) = hd g;
struct = (Label head, Arity head, map typeSig (Outputs head))
in
(t, struct, g)#(tag (Some struct) gs)
)"
text\<open>We need to group transitions not just by their structure but also by their history - i.e. the
last transition which was taken which had a different structure. We need to order these groups by
their relative positions within the traces such that output and update functions can be inferred in
the correct order.\<close>
definition transition_groups :: "iEFSM \<Rightarrow> log \<Rightarrow> transition_group list" where
"transition_groups e l = (
let
trace_groups = map (transition_groups_exec e) l;
tagged = map (tag None) trace_groups;
flat = sort (fold (@) tagged []);
group_fun = fold (\<lambda>(tag, s, gp) f. f((tag, s) $:= gp@(f$(tag, s)))) flat (K$ []);
grouped = map (\<lambda>x. group_fun $ x) (finfun_to_list group_fun);
inx_groups = map (\<lambda>gp. (Min (set (map fst gp)), map snd gp)) grouped
in
map snd (sort inx_groups)
)"
text\<open>For a given trace group, log, and EFSM, we want to build the training set for that group. That
is, the set of inputs, registers, and expected outputs from those transitions. To do this, we must
walk the traces in the EFSM to obtain the register values.\<close>
fun trace_group_training_set :: "transition_group \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> (inputs \<times> registers \<times> value list) list \<Rightarrow> (inputs \<times> registers \<times> value list) list" where
"trace_group_training_set _ _ _ _ [] train = train" |
"trace_group_training_set gp e s r ((l, i, p)#t) train = (
let
(id, s', transition) = fthe_elem (i_possible_steps e s r l i)
in
if \<exists>(id', _) \<in> set gp. id' = id then
trace_group_training_set gp e s' (evaluate_updates transition i r) t ((i, r, p)#train)
else
trace_group_training_set gp e s' (evaluate_updates transition i r) t train
)"
definition make_training_set :: "iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> (inputs \<times> registers \<times> value list) list" where
"make_training_set e l gp = fold (\<lambda>h a. trace_group_training_set gp e 0 <> h a) l []"
primrec replace_groups :: "transition_group list \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"replace_groups [] e = e" |
"replace_groups (h#t) e = replace_groups t (fold (\<lambda>(id, t) acc. replace_transition acc id t) h e)"
lemma replace_groups_fold [code]:
"replace_groups xs e = fold (\<lambda>h acc'. (fold (\<lambda>(id, t) acc. replace_transition acc id t) h acc')) xs e"
by (induct xs arbitrary: e, auto)
definition insert_updates :: "transition \<Rightarrow> update_function list \<Rightarrow> transition" where
"insert_updates t u = (
let
\<comment> \<open>Want to filter out null updates of the form rn := rn. It doesn't affect anything but it \<close>
\<comment> \<open>does make things look cleaner \<close>
necessary_updates = filter (\<lambda>(r, u). u \<noteq> V (R r)) u
in
t\<lparr>Updates := (filter (\<lambda>(r, _). r \<notin> set (map fst u)) (Updates t))@necessary_updates\<rparr>
)"
fun add_groupwise_updates_trace :: "trace \<Rightarrow> (tids \<times> update_function list) list \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> iEFSM" where
"add_groupwise_updates_trace [] _ e _ _ = e" |
"add_groupwise_updates_trace ((l, i, _)#trace) funs e s r = (
let
(id, s', t) = fthe_elem (i_possible_steps e s r l i);
updated = evaluate_updates t i r;
newUpdates = List.maps snd (filter (\<lambda>(tids, _). set id \<subseteq> set tids) funs);
t' = insert_updates t newUpdates;
updated' = apply_updates (Updates t') (join_ir i r) r;
necessaryUpdates = filter (\<lambda>(r, _). updated $ r \<noteq> updated' $ r) newUpdates;
t'' = insert_updates t necessaryUpdates;
e' = replace_transition e id t''
in
add_groupwise_updates_trace trace funs e' s' updated'
)"
primrec add_groupwise_updates :: "log \<Rightarrow> (tids \<times> update_function list) list \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"add_groupwise_updates [] _ e = e" |
"add_groupwise_updates (h#t) funs e = add_groupwise_updates t funs (add_groupwise_updates_trace h funs e 0 <>)"
lemma fold_add_groupwise_updates [code]:
"add_groupwise_updates log funs e = fold (\<lambda>trace acc. add_groupwise_updates_trace trace funs acc 0 <>) log e"
by (induct log arbitrary: e, auto)
\<comment> \<open>This will be replaced to calls to Z3 in the executable\<close>
definition get_regs :: "(vname \<Rightarrow>f String.literal) \<Rightarrow> inputs \<Rightarrow> vname aexp \<Rightarrow> value \<Rightarrow> registers" where
"get_regs types inputs expression output = Eps (\<lambda>r. aval expression (join_ir inputs r) = Some output)"
declare get_regs_def [code del]
code_printing constant get_regs \<rightharpoonup> (Scala) "Dirties.getRegs"
type_synonym action_info = "(cfstate \<times> registers \<times> registers \<times> inputs \<times> tids \<times> transition)"
type_synonym run_info = "action_info list"
type_synonym targeted_run_info = "(registers \<times> action_info) list"
fun everything_walk :: "output_function \<Rightarrow> nat \<Rightarrow> (vname \<Rightarrow>f String.literal) \<Rightarrow> trace \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> transition_group \<Rightarrow> run_info" where
"everything_walk _ _ _ [] _ _ _ _ = []" |
"everything_walk f fi types ((label, inputs, outputs)#t) oPTA s regs gp = (
let (tid, s', ta) = fthe_elem (i_possible_steps oPTA s regs label inputs) in
\<comment> \<open>Possible steps with a transition we need to modify\<close>
if \<exists>(tid', _) \<in> set gp. tid = tid' then
(s, regs, get_regs types inputs f (outputs!fi), inputs, tid, ta)#(everything_walk f fi types t oPTA s' (evaluate_updates ta inputs regs) gp)
else
let empty = <> in
(s, regs, empty, inputs, tid, ta)#(everything_walk f fi types t oPTA s' (evaluate_updates ta inputs regs) gp)
)"
definition everything_walk_log :: "output_function \<Rightarrow> nat \<Rightarrow> (vname \<Rightarrow>f String.literal) \<Rightarrow> log \<Rightarrow> iEFSM \<Rightarrow> transition_group \<Rightarrow> run_info list" where
"everything_walk_log f fi types log e gp = map (\<lambda>t. everything_walk f fi types t e 0 <> gp) log"
fun target :: "registers \<Rightarrow> run_info \<Rightarrow> targeted_run_info" where
"target _ [] = []" |
"target tRegs ((s, oldregs, regs, inputs, tid, ta)#t) = (
let newTarget = if finfun_to_list regs = [] then tRegs else regs in
(tRegs, s, oldregs, regs, inputs, tid, ta)#target newTarget t
)"
fun target_tail :: "registers \<Rightarrow> run_info \<Rightarrow> targeted_run_info \<Rightarrow> targeted_run_info" where
"target_tail _ [] tt = rev tt" |
"target_tail tRegs ((s, oldregs, regs, inputs, tid, ta)#t) tt = (
let newTarget = if finfun_to_list regs = [] then tRegs else regs in
target_tail newTarget t ((tRegs, s, oldregs, regs, inputs, tid, ta)#tt)
)"
lemma target_tail: "(rev bs)@(target tRegs ts) = target_tail tRegs ts bs"
proof(induct ts arbitrary: bs tRegs)
case (Cons a ts)
then show ?case
apply (cases a)
apply simp
apply standard
by (metis (no_types, lifting) append_eq_append_conv2 rev.simps(2) rev_append rev_swap self_append_conv2)+
qed simp
definition "target_fold tRegs ts b = fst (fold (\<lambda>(s, oldregs, regs, inputs, tid, ta) (acc, tRegs).
let newTarget = if finfun_to_list regs = [] then tRegs else regs in
(acc@[(tRegs, s, oldregs, regs, inputs, tid, ta)], newTarget)
) ts (rev b, tRegs))"
lemma target_tail_fold: "target_tail tRegs ts b = target_fold tRegs ts b"
proof(induct ts arbitrary: tRegs b)
case Nil
then show ?case
by (simp add: target_fold_def)
next
case (Cons a ts)
then show ?case
apply (cases a)
by (simp add: target_fold_def)
qed
lemma target_fold [code]: "target tRegs ts = target_fold tRegs ts []"
by (metis append_self_conv2 rev.simps(1) target_tail_fold target_tail)
\<comment> \<open>This will be replaced by symbolic regression in the executable\<close>
definition get_update :: "label \<Rightarrow> nat \<Rightarrow> value list \<Rightarrow> (inputs \<times> registers \<times> registers) list \<Rightarrow> vname aexp option" where
"get_update _ reg values train = (let
possible_funs = {a. \<forall>(i, r, r') \<in> set train. aval a (join_ir i r) = r' $ reg}
in
if possible_funs = {} then None else Some (Eps (\<lambda>x. x \<in> possible_funs))
)"
declare get_update_def [code del]
code_printing constant get_update \<rightharpoonup> (Scala) "Dirties.getUpdate"
definition get_updates_opt :: "label \<Rightarrow> value list \<Rightarrow> (inputs \<times> registers \<times> registers) list \<Rightarrow> (nat \<times> vname aexp option) list" where
"get_updates_opt l values train = (let
updated_regs = fold List.union (map (finfun_to_list \<circ> snd \<circ> snd) train) [] in
map (\<lambda>r.
let targetValues = remdups (map (\<lambda>(_, _, regs). regs $ r) train) in
if (\<forall>(_, anteriorRegs, posteriorRegs) \<in> set train. anteriorRegs $ r = posteriorRegs $ r) then
(r, Some (V (R r)))
else if length targetValues = 1 \<and> (\<forall>(inputs, anteriorRegs, _) \<in> set train. finfun_to_list anteriorRegs = []) then
case hd targetValues of Some v \<Rightarrow>
(r, Some (L v))
else
(r, get_update l r values train)
) updated_regs
)"
definition finfun_add :: "(('a::linorder) \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f 'b)" where
"finfun_add a b = fold (\<lambda>k f. f(k $:= b $ k)) (finfun_to_list b) a"
definition group_update :: "value list \<Rightarrow> targeted_run_info \<Rightarrow> (tids \<times> (nat \<times> vname aexp) list) option" where
"group_update values l = (
let
(_, (_, _, _, _, _, t)) = hd l;
targeted = filter (\<lambda>(regs, _). finfun_to_list regs \<noteq> []) l;
maybe_updates = get_updates_opt (Label t) values (map (\<lambda>(tRegs, s, oldRegs, regs, inputs, tid, ta). (inputs, finfun_add oldRegs regs, tRegs)) targeted)
in
if \<exists>(_, f_opt) \<in> set maybe_updates. f_opt = None then
None
else
Some (fold List.union (map (\<lambda>(tRegs, s, oldRegs, regs, inputs, tid, ta). tid) l) [], map (\<lambda>(r, f_o). (r, the f_o)) maybe_updates)
)"
fun groupwise_put_updates :: "transition_group list \<Rightarrow> log \<Rightarrow> value list \<Rightarrow> run_info list \<Rightarrow> (nat \<times> (vname aexp \<times> vname \<Rightarrow>f String.literal)) \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"groupwise_put_updates [] _ _ _ _ e = e" |
"groupwise_put_updates (gp#gps) log values walked (o_inx, (op, types)) e = (
let
targeted = map (\<lambda>x. filter (\<lambda>(_, _, _, _, _, id, tran). (id, tran) \<in> set gp) x) (map (\<lambda>w. rev (target <> (rev w))) walked);
group = fold List.union targeted []
in
case group_update values group of
None \<Rightarrow> groupwise_put_updates gps log values walked (o_inx, (op, types)) e |
Some u \<Rightarrow> groupwise_put_updates gps log values walked (o_inx, (op, types)) (make_distinct (add_groupwise_updates log [u] e))
)"
definition updates_for_output :: "log \<Rightarrow> value list \<Rightarrow> transition_group \<Rightarrow> nat \<Rightarrow> vname aexp \<Rightarrow> vname \<Rightarrow>f String.literal \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"updates_for_output log values current o_inx op types e = (
if AExp.enumerate_regs op = {} then e
else
let
walked = everything_walk_log op o_inx types log e current;
groups = transition_groups e log
in
groupwise_put_updates groups log values walked (o_inx, (op, types)) e
)"
type_synonym output_types = "(vname aexp \<times> vname \<Rightarrow>f String.literal)"
fun put_updates :: "log \<Rightarrow> value list \<Rightarrow> transition_group \<Rightarrow> (nat \<times> output_types option) list \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"put_updates _ _ _ [] e = e" |
"put_updates log values gp ((_, None)#ops) e = put_updates log values gp ops e" |
"put_updates log values gp ((o_inx, Some (op, types))#ops) e = (
let
gp' = map (\<lambda>(id, t). (id, t\<lparr>Outputs := list_update (Outputs t) o_inx op\<rparr>)) gp;
generalised_model = fold (\<lambda>(id, t) acc. replace_transition acc id t) gp' e;
e' = updates_for_output log values gp o_inx op types generalised_model
in
if accepts_log (set log) (tm e') then
put_updates log values gp' ops e'
else
put_updates log values gp ops e
)"
fun unzip_3 :: "('a \<times> 'b \<times> 'c) list \<Rightarrow> ('a list \<times> 'b list \<times> 'c list)" where
"unzip_3 [] = ([], [], [])" |
"unzip_3 ((a, b, c)#l) = (
let (as, bs, cs) = unzip_3 l in
(a#as, b#bs, c#cs)
)"
lemma unzip_3: "unzip_3 l = (map fst l, map (fst \<circ> snd) l, map (snd \<circ> snd) l)"
by (induct l, auto)
fun unzip_3_tailrec_rev :: "('a \<times> 'b \<times> 'c) list \<Rightarrow> ('a list \<times> 'b list \<times> 'c list) \<Rightarrow> ('a list \<times> 'b list \<times> 'c list)" where
"unzip_3_tailrec_rev [] (as, bs, cs) = (as, bs, cs)" |
"unzip_3_tailrec_rev ((a, b, c)#t) (as, bs, cs) = unzip_3_tailrec_rev t (a#as, b#bs, c#cs)"
lemma unzip_3_tailrec_rev: "unzip_3_tailrec_rev l (as, bs, cs) = ((map_tailrec_rev fst l as), (map_tailrec_rev (fst \<circ> snd) l bs), (map_tailrec_rev (snd \<circ> snd) l cs))"
by (induct l arbitrary: as bs cs, auto)
definition "unzip_3_tailrec l = (let (as, bs, cs) = unzip_3_tailrec_rev l ([],[],[]) in (rev as, rev bs, rev cs))"
lemma unzip_3_tailrec [code]: "unzip_3 l = unzip_3_tailrec l"
apply (simp only: unzip_3_tailrec_def unzip_3_tailrec_rev)
by (simp add: Let_def map_tailrec_rev unzip_3 map_eq_map_tailrec)
text\<open>We want to return an aexp which, when evaluated in the correct context accounts for the literal
input-output pairs within the training set. This will be replaced by symbolic regression in the
executable\<close>
definition get_output :: "label \<Rightarrow> nat \<Rightarrow> value list \<Rightarrow> (inputs \<times> registers \<times> value) list \<Rightarrow> (vname aexp \<times> (vname \<Rightarrow>f String.literal)) option" where
"get_output _ maxReg values train = (let
possible_funs = {a. \<forall>(i, r, p) \<in> set train. aval a (join_ir i r) = Some p}
in
if possible_funs = {} then None else Some (Eps (\<lambda>x. x \<in> possible_funs), (K$ STR ''int''))
)"
declare get_output_def [code del]
code_printing constant get_output \<rightharpoonup> (Scala) "Dirties.getOutput"
definition get_outputs :: "label \<Rightarrow> nat \<Rightarrow> value list \<Rightarrow> inputs list \<Rightarrow> registers list \<Rightarrow> value list list \<Rightarrow> (vname aexp \<times> (vname \<Rightarrow>f String.literal)) option list" where
"get_outputs l maxReg values I r outputs = map_tailrec (\<lambda>(maxReg, ps). get_output l maxReg values (zip I (zip r ps))) (enumerate maxReg (transpose outputs))"
definition enumerate_exec_values :: "trace \<Rightarrow> value list" where
"enumerate_exec_values vs = fold (\<lambda>(_, i, p) I. List.union (List.union i p) I) vs []"
definition enumerate_log_values :: "log \<Rightarrow> value list" where
"enumerate_log_values l = fold (\<lambda>e I. List.union (enumerate_exec_values e) I) l []"
(*This is where the types stuff originates*)
definition generalise_and_update :: "log \<Rightarrow> iEFSM \<Rightarrow> transition_group \<Rightarrow> iEFSM" where
"generalise_and_update log e gp = (
let
label = Label (snd (hd gp));
values = enumerate_log_values log;
new_gp_ts = make_training_set e log gp;
(I, R, P) = unzip_3 new_gp_ts;
max_reg = max_reg_total e;
outputs = get_outputs label max_reg values I R P
in
put_updates log values gp (enumerate 0 outputs) e
)"
text \<open>Splitting structural groups up into subgroups by previous transition can cause different
subgroups to get different updates. We ideally want structural groups to have the same output and
update functions, as structural groups are likely to be instances of the same underlying behaviour.\<close>
definition standardise_group :: "iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> (iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> transition_group) \<Rightarrow> iEFSM" where
"standardise_group e l gp s = (
let
standardised = s e l gp;
e' = replace_transitions e standardised
in
if e' = e then e else
if accepts_log (set l) (tm e') then e' else e
)"
primrec find_outputs :: "output_function list list \<Rightarrow> iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> output_function list option" where
"find_outputs [] _ _ _ = None" |
"find_outputs (h#t) e l g = (
let
outputs = fold (\<lambda>(tids, t) acc. replace_transition acc tids (t\<lparr>Outputs := h\<rparr>)) g e
in
if accepts_log (set l) (tm outputs) then
Some h
else
find_outputs t e l g
)"
primrec find_updates_outputs :: "update_function list list \<Rightarrow> output_function list list \<Rightarrow> iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> (output_function list \<times> update_function list) option" where
"find_updates_outputs [] _ _ _ _ = None" |
"find_updates_outputs (h#t) p e l g = (
let
updates = fold (\<lambda>(tids, t) acc. replace_transition acc tids (t\<lparr>Updates := h\<rparr>)) g e
in
case find_outputs p updates l (map (\<lambda>(id, t). (id,t\<lparr>Updates := h\<rparr>)) g) of
Some pp \<Rightarrow> Some (pp, h) |
None \<Rightarrow> find_updates_outputs t p e l g
)"
definition updates_for :: "update_function list \<Rightarrow> update_function list list" where
"updates_for U = (
let uf = fold (\<lambda>(r, u) f. f(r $:= u#(f $ r))) U (K$ []) in
map (\<lambda>r. map (\<lambda>u. (r, u)) (uf $ r)) (finfun_to_list uf)
)"
definition standardise_group_outputs_updates :: "iEFSM \<Rightarrow> log \<Rightarrow> transition_group \<Rightarrow> transition_group" where
"standardise_group_outputs_updates e l g = (
let
update_groups = product_lists (updates_for (remdups (List.maps (Updates \<circ> snd) g)));
update_groups_subs = fold (List.union \<circ> subseqs) update_groups [];
output_groups = product_lists (transpose (remdups (map (Outputs \<circ> snd) g)))
in
case find_updates_outputs update_groups_subs output_groups e l g of
None \<Rightarrow> g |
Some (p, u) \<Rightarrow> map (\<lambda>(id, t). (id, t\<lparr>Outputs := p, Updates := u\<rparr>)) g
)"
fun find_first_use_of_trace :: "nat \<Rightarrow> trace \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> tids option" where
"find_first_use_of_trace _ [] _ _ _ = None" |
"find_first_use_of_trace rr ((l, i, _)#es) e s r = (
let
(id, s', t) = fthe_elem (i_possible_steps e s r l i)
in
if (\<exists>p \<in> set (Outputs t). aexp_constrains p (V (R rr))) then
Some id
else
find_first_use_of_trace rr es e s' (evaluate_updates t i r)
)"
definition find_first_uses_of :: "nat \<Rightarrow> log \<Rightarrow> iEFSM \<Rightarrow> tids list" where
"find_first_uses_of r l e = List.maps (\<lambda>x. case x of None \<Rightarrow> [] | Some x \<Rightarrow> [x]) (map (\<lambda>t. find_first_use_of_trace r t e 0 <>) l)"
fun find_initialisation_of_trace :: "nat \<Rightarrow> trace \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> (tids \<times> transition) option" where
"find_initialisation_of_trace _ [] _ _ _ = None" |
"find_initialisation_of_trace r' ((l, i, _)#es) e s r = (
let
(tids, s', t) = fthe_elem (i_possible_steps e s r l i)
in
if (\<exists>(rr, u) \<in> set (Updates t). rr = r' \<and> is_lit u) then
Some (tids, t)
else
find_initialisation_of_trace r' es e s' (evaluate_updates t i r)
)"
primrec find_initialisation_of :: "nat \<Rightarrow> iEFSM \<Rightarrow> log \<Rightarrow> (tids \<times> transition) option list" where
"find_initialisation_of _ _ [] = []" |
"find_initialisation_of r e (h#t) = (
case find_initialisation_of_trace r h e 0 <> of
None \<Rightarrow> find_initialisation_of r e t |
Some thing \<Rightarrow> Some thing#(find_initialisation_of r e t)
)"
definition delay_initialisation_of :: "nat \<Rightarrow> log \<Rightarrow> iEFSM \<Rightarrow> tids list \<Rightarrow> iEFSM" where
"delay_initialisation_of r l e tids = fold (\<lambda>x e. case x of
None \<Rightarrow> e |
Some (i_tids, t) \<Rightarrow>
let
origins = map (\<lambda>id. origin id e) tids;
init_val = snd (hd (filter (\<lambda>(r', _). r = r') (Updates t)));
e' = fimage (\<lambda>(id, (origin', dest), tr).
\<comment> \<open>Add the initialisation update to incoming transitions\<close>
if dest \<in> set origins then
(id, (origin', dest), tr\<lparr>Updates := List.insert (r, init_val) (Updates tr)\<rparr>)
\<comment> \<open>Strip the initialisation update from the original initialising transition\<close>
else if id = i_tids then
(id, (origin', dest), tr\<lparr>Updates := filter (\<lambda>(r', _). r \<noteq> r') (Updates tr)\<rparr>)
else
(id, (origin', dest), tr)
) e
in
\<comment> \<open>We don't want to update a register twice so just leave it\<close>
if accepts_log (set l) (tm e') then
e'
else
e
) (find_initialisation_of r e l) e"
fun groupwise_generalise_and_update :: "log \<Rightarrow> iEFSM \<Rightarrow> transition_group list \<Rightarrow> iEFSM" where
"groupwise_generalise_and_update _ e [] = e" |
"groupwise_generalise_and_update log e (gp#t) = (
let
e' = generalise_and_update log e gp;
rep = snd (hd (gp));
structural_group = fimage (\<lambda>(i, _, t). (i, t)) (ffilter (\<lambda>(_, _, t). same_structure rep t) e');
delayed = fold (\<lambda>r acc. delay_initialisation_of r log acc (find_first_uses_of r log acc)) (sorted_list_of_set (all_regs e')) e';
standardised = standardise_group delayed log (sorted_list_of_fset structural_group) standardise_group_outputs_updates;
structural_group2 = fimage (\<lambda>(_, _, t). (Outputs t, Updates t)) (ffilter (\<lambda>(_, _, t). Label rep = Label t \<and> Arity rep = Arity t \<and> length (Outputs rep) = length (Outputs t)) standardised)
in
\<comment> \<open>If we manage to standardise a structural group, we do not need to evolve outputs and
updates for the other historical subgroups so can filter them out.\<close>
if fis_singleton structural_group2 then
groupwise_generalise_and_update log (merge_regs standardised (accepts_log (set log))) (filter (\<lambda>g. set g \<inter> fset structural_group = {}) t)
else
groupwise_generalise_and_update log (merge_regs standardised (accepts_log (set log))) t
)"
definition drop_all_guards :: "iEFSM \<Rightarrow> iEFSM \<Rightarrow> log \<Rightarrow> update_modifier \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"drop_all_guards e pta log m np = (let
derestricted = fimage (\<lambda>(id, tf, tran). (id, tf, tran\<lparr>Guards := []\<rparr>)) e;
nondeterministic_pairs = sorted_list_of_fset (np derestricted)
in
case resolve_nondeterminism {} nondeterministic_pairs pta derestricted m (accepts_log (set log)) np of
(None, _) \<Rightarrow> pta |
(Some resolved, _) \<Rightarrow> resolved
)"
definition updated_regs :: "transition \<Rightarrow> nat set" where
"updated_regs t = set (map fst (Updates t))"
definition fewer_updates :: "transition \<Rightarrow> transition fset \<Rightarrow> transition option" where
"fewer_updates t tt = (
let p = ffilter (\<lambda>t'. same_structure t t' \<and> Outputs t = Outputs t' \<and> updated_regs t' \<subset> updated_regs t) tt in
if p = {||} then None else Some (snd (fMin (fimage (\<lambda>t. (length (Updates t), t)) p))))"
fun remove_spurious_updates_aux :: "iEFSM \<Rightarrow> transition_group \<Rightarrow> transition fset \<Rightarrow> log \<Rightarrow> iEFSM" where
"remove_spurious_updates_aux e [] _ _ = e" |
"remove_spurious_updates_aux e ((tid, t)#ts) tt l = (
case fewer_updates t tt of
None \<Rightarrow> remove_spurious_updates_aux e ts tt l |
Some t' \<Rightarrow> (
let e' = replace_transition e tid t' in
if accepts_log (set l) (tm e') then
remove_spurious_updates_aux e' ts tt l
else
remove_spurious_updates_aux e ts tt l
)
)"
(* This goes through and tries to remove spurious updates that get introduced during preprocessing *)
definition remove_spurious_updates :: "iEFSM \<Rightarrow> log \<Rightarrow> iEFSM" where
"remove_spurious_updates e l = (
let transitions = fimage (\<lambda>(tid, _, t). (tid, t)) e in
remove_spurious_updates_aux e (sorted_list_of_fset transitions) (fimage snd transitions) l
)"
definition derestrict :: "iEFSM \<Rightarrow> log \<Rightarrow> update_modifier \<Rightarrow> (iEFSM \<Rightarrow> nondeterministic_pair fset) \<Rightarrow> iEFSM" where
"derestrict pta log m np = (
let
normalised = groupwise_generalise_and_update log pta (transition_groups pta log)
in
drop_all_guards normalised pta log m np
)"
definition "drop_pta_guards pta log m np = drop_all_guards pta pta log m np"
end

View File

@ -0,0 +1,42 @@
section\<open>Same Register\<close>
text\<open>The \texttt{same\_register} heuristic aims to replace registers which are used in the same way.\<close>
theory Same_Register
imports "../Inference"
begin
definition replace_with :: "iEFSM \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> iEFSM" where
"replace_with e r1 r2 = (fimage (\<lambda>(u, tf, t). (u, tf,Transition.rename_regs (id(r1:=r2)) t)) e)"
fun merge_if_same :: "iEFSM \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat) list \<Rightarrow> iEFSM" where
"merge_if_same e _ [] = e" |
"merge_if_same e check ((r1, r2)#rs) = (
let transitions = fimage (snd \<circ> snd) e in
if \<exists>(t1, t2) |\<in>| ffilter (\<lambda>(t1, t2). t1 < t2) (transitions |\<times>| transitions).
same_structure t1 t2 \<and> r1 \<in> enumerate_regs t1 \<and> r2 \<in> enumerate_regs t2
then
let newE = replace_with e r1 r2 in
if check (tm newE) then
merge_if_same newE check rs
else
merge_if_same e check rs
else
merge_if_same e check rs
)"
definition merge_regs :: "iEFSM \<Rightarrow> (transition_matrix \<Rightarrow> bool) \<Rightarrow> iEFSM" where
"merge_regs e check = (
let
regs = all_regs e;
reg_pairs = sorted_list_of_set (Set.filter (\<lambda>(r1, r2). r1 < r2) (regs \<times> regs))
in
merge_if_same e check reg_pairs
)"
fun same_register :: update_modifier where
"same_register t1ID t2ID s new _ old check = (
let new' = merge_regs new check in
if new' = new then None else Some new'
)"
end

View File

@ -0,0 +1,283 @@
chapter\<open>Heuristics\<close>
text\<open>As part of this inference technique, we make use of certain \emph{heuristics} to abstract away
concrete values into registers. This allows us to generalise from examples of behaviour. These
heuristics are as follows.
\begin{description}
\item [Store and Reuse] - This heuristic aims to recognise when input values are subsequently used
as an output. Such behaviour is generalised by storing the relevant input in a register, and
replacing the literal output with the content of the register. This enables the EFSM to
\emph{predict} how the underlying system might behave when faced with unseen inputs.
\item [Increment and Reset] - This heuristic is a naive attempt to introduce additive behaviour.
The idea here is that if we want to merge two transitions with identical input values and different
numeric outputs, for example $\textit{coin}:1[i_0=50]/o_0:=50$ and $\textit{coin}:1[i_0=50]/o_0:=100$,
then the behaviour must depend on the value of an internal variable. This heuristic works by
dropping the input guard and adding an update to a fresh register, in this case summing the current
register value with the input. A similar principle can be applied to other numeric functions such as
subtraction.
\item [Same Register] - Because of the way heuristics are applied, it is possible for different
registers to be introduced to serve the same purpose. This heuristic attempts to identify when this
has happened and merge the two registers.
\item [Least Upper Bound] - In certain situations, transitions may produce the same output for
different inputs. This technique forms the least upper bound of the transition guards
--- their disjunction --- such that they can be merged into a single behaviour.
\item [Distinguishing Guards] - Under certain circumstances, we explicitly do not want to merge
two transitions into one. This heuristic resolves nondeterminism between transitions by attempting
to find apply mutually exclusive guards to each transition such that their behaviour is distinguished.
\end{description}\<close>
section\<open>Store and Reuse\<close>
text\<open>An obvious candidate for generalisation is the ``store and reuse'' pattern. This manifests
itself when the input of one transition is subsequently used as the output of another. Recognising
this usage pattern allows us to introduce a \emph{storage register} to abstract away concrete data
values and replace two transitions whose outputs differ with a single transition that outputs the
content of the register.\<close>
theory Store_Reuse
imports "../Inference"
begin
datatype ioTag = In | Out
instantiation ioTag :: linorder begin
fun less_ioTag :: "ioTag \<Rightarrow> ioTag \<Rightarrow> bool" where
"In < Out = True" |
"Out < _ = False" |
"In < In = False"
definition less_eq_ioTag :: "ioTag \<Rightarrow> ioTag \<Rightarrow> bool" where
"less_eq_ioTag x y = (x < y \<or> x = y)"
declare less_eq_ioTag_def [simp]
instance
apply standard
using less_ioTag.elims(2) apply fastforce
apply simp
apply (metis ioTag.exhaust less_eq_ioTag_def)
using less_eq_ioTag_def less_ioTag.elims(2) apply blast
by (metis (full_types) ioTag.exhaust less_eq_ioTag_def less_ioTag.simps(1))
end
type_synonym index = "nat \<times> ioTag \<times> nat"
fun lookup :: "index \<Rightarrow> trace \<Rightarrow> value" where
"lookup (actionNo, In, inx) t = (let (_, inputs, _) = nth t actionNo in nth inputs inx)" |
"lookup (actionNo, Out, inx) t = (let (_, _, outputs) = nth t actionNo in nth outputs inx)"
abbreviation actionNum :: "index \<Rightarrow> nat" where
"actionNum i \<equiv> fst i"
abbreviation ioTag :: "index \<Rightarrow> ioTag" where
"ioTag i \<equiv> fst (snd i)"
abbreviation inx :: "index \<Rightarrow> nat" where
"inx i \<equiv> snd (snd i)"
primrec index :: "value list \<Rightarrow> nat \<Rightarrow> ioTag \<Rightarrow> nat \<Rightarrow> index fset" where
"index [] _ _ _ = {||}" |
"index (h#t) actionNo io ind = finsert (actionNo, io, ind) (index t actionNo io (ind + 1))"
definition io_index :: "nat \<Rightarrow> value list \<Rightarrow> value list \<Rightarrow> index fset" where
"io_index actionNo inputs outputs = (index inputs actionNo In 0) |\<union>| (index outputs actionNo Out 0)"
definition indices :: "trace \<Rightarrow> index fset" where
"indices e = foldl (|\<union>|) {||} (map (\<lambda>(actionNo, (label, inputs, outputs)). io_index actionNo inputs outputs) (enumerate 0 e))"
definition get_by_id_intratrace_matches :: "trace \<Rightarrow> (index \<times> index) fset" where
"get_by_id_intratrace_matches e = ffilter (\<lambda>(a, b). lookup a e = lookup b e \<and> actionNum a \<le> actionNum b \<and> a \<noteq> b) (indices e |\<times>| indices e)"
(*
If the EFSM is nondeterministic, we need to make sure it chooses the right path so that it recognises
the input trace.
*)
definition i_step :: "execution \<Rightarrow> iEFSM \<Rightarrow> cfstate \<Rightarrow> registers \<Rightarrow> label \<Rightarrow> inputs \<Rightarrow> (transition \<times> cfstate \<times> tids \<times> registers) option" where
"i_step tr e s r l i = (let
poss_steps = (i_possible_steps e s r l i);
possibilities = ffilter (\<lambda>(u, s', t). recognises_execution (tm e) s' (evaluate_updates t i r) tr) poss_steps in
case random_member possibilities of
None \<Rightarrow> None |
Some (u, s', t) \<Rightarrow>
Some (t, s', u, (evaluate_updates t i r))
)"
type_synonym match = "(((transition \<times> tids) \<times> ioTag \<times> nat) \<times> ((transition \<times> tids) \<times> ioTag \<times> nat))"
definition "exec2trace t = map (\<lambda>(label, inputs, _). (label, inputs)) t"
primrec (nonexhaustive) walk_up_to :: "nat \<Rightarrow> iEFSM \<Rightarrow> nat \<Rightarrow> registers \<Rightarrow> trace \<Rightarrow> (transition \<times> tids)" where
"walk_up_to n e s r (h#t) =
(case (i_step (exec2trace t) e s r (fst h) (fst (snd h))) of
(Some (transition, s', uid, updated)) \<Rightarrow> (case n of 0 \<Rightarrow> (transition, uid) | Suc m \<Rightarrow> walk_up_to m e s' updated t)
)"
definition find_intertrace_matches_aux :: "(index \<times> index) fset \<Rightarrow> iEFSM \<Rightarrow> trace \<Rightarrow> match fset" where
"find_intertrace_matches_aux intras e t = fimage (\<lambda>((e1, io1, inx1), (e2, io2, inx2)). (((walk_up_to e1 e 0 <> t), io1, inx1), ((walk_up_to e2 e 0 <> t), io2, inx2))) intras"
definition find_intertrace_matches :: "log \<Rightarrow> iEFSM \<Rightarrow> match list" where
"find_intertrace_matches l e = filter (\<lambda>((e1, io1, inx1), (e2, io2, inx2)). e1 \<noteq> e2) (concat (map (\<lambda>(t, m). sorted_list_of_fset (find_intertrace_matches_aux m e t)) (zip l (map get_by_id_intratrace_matches l))))"
definition total_max_input :: "iEFSM \<Rightarrow> nat" where
"total_max_input e = (case EFSM.max_input (tm e) of None \<Rightarrow> 0 | Some i \<Rightarrow> i)"
definition total_max_reg :: "iEFSM \<Rightarrow> nat" where
"total_max_reg e = (case EFSM.max_reg (tm e) of None \<Rightarrow> 0 | Some i \<Rightarrow> i)"
definition remove_guard_add_update :: "transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> transition" where
"remove_guard_add_update t inputX outputX = \<lparr>
Label = (Label t), Arity = (Arity t),
Guards = (filter (\<lambda>g. \<not> gexp_constrains g (V (vname.I inputX))) (Guards t)),
Outputs = (Outputs t),
Updates = (outputX, (V (vname.I inputX)))#(Updates t)
\<rparr>"
definition generalise_output :: "transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> transition" where
"generalise_output t regX outputX = \<lparr>
Label = (Label t),
Arity = (Arity t),
Guards = (Guards t),
Outputs = list_update (Outputs t) outputX (V (R regX)),
Updates = (Updates t)
\<rparr>"
definition is_generalised_output_of :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"is_generalised_output_of t' t r p = (t' = generalise_output t r p)"
primrec count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
"count _ [] = 0" |
"count a (h#t) = (if a = h then 1+(count a t) else count a t)"
definition replaceAll :: "iEFSM \<Rightarrow> transition \<Rightarrow> transition \<Rightarrow> iEFSM" where
"replaceAll e old new = fimage (\<lambda>(uid, (from, dest), t). if t = old then (uid, (from, dest), new) else (uid, (from, dest), t)) e"
primrec generalise_transitions :: "((((transition \<times> tids) \<times> ioTag \<times> nat) \<times> (transition \<times> tids) \<times> ioTag \<times> nat) \<times>
((transition \<times> tids) \<times> ioTag \<times> nat) \<times> (transition \<times> tids) \<times> ioTag \<times> nat) list \<Rightarrow> iEFSM \<Rightarrow> iEFSM" where
"generalise_transitions [] e = e" |
"generalise_transitions (h#t) e = (let
((((orig1, u1), _), (orig2, u2), _), (((gen1, u1'), _), (gen2, u2), _)) = h in
generalise_transitions t (replaceAll (replaceAll e orig1 gen1) orig2 gen2))"
definition strip_uids :: "(((transition \<times> tids) \<times> ioTag \<times> nat) \<times> (transition \<times> tids) \<times> ioTag \<times> nat) \<Rightarrow> ((transition \<times> ioTag \<times> nat) \<times> (transition \<times> ioTag \<times> nat))" where
"strip_uids x = (let (((t1, u1), io1, in1), (t2, u2), io2, in2) = x in ((t1, io1, in1), (t2, io2, in2)))"
definition modify :: "match list \<Rightarrow> tids \<Rightarrow> tids \<Rightarrow> iEFSM \<Rightarrow> iEFSM option" where
"modify matches u1 u2 old = (let relevant = filter (\<lambda>(((_, u1'), io, _), (_, u2'), io', _). io = In \<and> io' = Out \<and> (u1 = u1' \<or> u2 = u1' \<or> u1 = u2' \<or> u2 = u2')) matches;
newReg = case max_reg old of None \<Rightarrow> 1 | Some r \<Rightarrow> r + 1;
replacements = map (\<lambda>(((t1, u1), io1, inx1), (t2, u2), io2, inx2). (((remove_guard_add_update t1 inx1 newReg, u1), io1, inx1), (generalise_output t2 newReg inx2, u2), io2, inx2)) relevant;
comparisons = zip relevant replacements;
stripped_replacements = map strip_uids replacements;
to_replace = filter (\<lambda>(_, s). count (strip_uids s) stripped_replacements > 1) comparisons in
if to_replace = [] then None else Some ((generalise_transitions to_replace old))
)"
(* type_synonym update_modifier = "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> (iEFSM \<times> (nat \<Rightarrow> nat) \<times> (nat \<Rightarrow> nat)) option" *)
definition heuristic_1 :: "log \<Rightarrow> update_modifier" where
"heuristic_1 l t1 t2 s new _ old check = (case modify (find_intertrace_matches l old) t1 t2 new of
None \<Rightarrow> None |
Some e \<Rightarrow> if check (tm e) then Some e else None
)"
lemma remove_guard_add_update_preserves_outputs:
"Outputs (remove_guard_add_update t i r) = Outputs t"
by (simp add: remove_guard_add_update_def)
lemma remove_guard_add_update_preserves_label:
"Label (remove_guard_add_update t i r) = Label t"
by (simp add: remove_guard_add_update_def)
lemma remove_guard_add_update_preserves_arity:
"Arity (remove_guard_add_update t i r) = Arity t"
by (simp add: remove_guard_add_update_def)
lemmas remove_guard_add_update_preserves = remove_guard_add_update_preserves_label
remove_guard_add_update_preserves_arity
remove_guard_add_update_preserves_outputs
definition is_generalisation_of :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"is_generalisation_of t' t i r = (t' = remove_guard_add_update t i r \<and>
i < Arity t \<and>
(\<exists>v. Eq (V (vname.I i)) (L v) \<in> set (Guards t)) \<and>
r \<notin> set (map fst (Updates t)))"
lemma generalise_output_preserves_label:
"Label (generalise_output t r p) = Label t"
by (simp add: generalise_output_def)
lemma generalise_output_preserves_arity:
"Arity (generalise_output t r p) = Arity t"
by (simp add: generalise_output_def)
lemma generalise_output_preserves_guard:
"Guards (generalise_output t r p) = Guards t"
by (simp add: generalise_output_def)
lemma generalise_output_preserves_output_length:
"length (Outputs (generalise_output t r p)) = length (Outputs t)"
by (simp add: generalise_output_def)
lemma generalise_output_preserves_updates:
"Updates (generalise_output t r p) = Updates t"
by (simp add: generalise_output_def)
lemmas generalise_output_preserves = generalise_output_preserves_label
generalise_output_preserves_arity
generalise_output_preserves_output_length
generalise_output_preserves_guard
generalise_output_preserves_updates
definition is_proper_generalisation_of :: "transition \<Rightarrow> transition \<Rightarrow> iEFSM \<Rightarrow> bool" where
"is_proper_generalisation_of t' t e = (\<exists>i \<le> total_max_input e. \<exists> r \<le> total_max_reg e.
is_generalisation_of t' t i r \<and>
(\<forall>u \<in> set (Updates t). fst u \<noteq> r) \<and>
(\<forall>i \<le> max_input (tm e). \<forall>u \<in> set (Updates t). fst u \<noteq> r)
)"
(* Recognising the same input used in multiple guards *)
definition generalise_input :: "transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> transition" where
"generalise_input t r i = \<lparr>
Label = Label t,
Arity = Arity t,
Guards = map (\<lambda>g. case g of Eq (V (I i')) (L _) \<Rightarrow> if i = i' then Eq (V (I i)) (V (R r)) else g | _ \<Rightarrow> g) (Guards t),
Outputs = Outputs t,
Updates = Updates t
\<rparr>"
fun structural_count :: "((transition \<times> ioTag \<times> nat) \<times> (transition \<times> ioTag \<times> nat)) \<Rightarrow> ((transition \<times> ioTag \<times> nat) \<times> (transition \<times> ioTag \<times> nat)) list \<Rightarrow> nat" where
"structural_count _ [] = 0" |
"structural_count a (((t1', io1', i1'), (t2', io2', i2'))#t) = (
let ((t1, io1, i1), (t2, io2, i2)) = a in
if same_structure t1 t1' \<and> same_structure t2 t2' \<and>
io1 = io1' \<and> io2 = io2' \<and>
i1 = i1' \<and> i2 = i2'
then
1+(structural_count a t)
else
structural_count a t
)"
definition remove_guards_add_update :: "transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> transition" where
"remove_guards_add_update t inputX outputX = \<lparr>
Label = (Label t), Arity = (Arity t),
Guards = [],
Outputs = (Outputs t),
Updates = (outputX, (V (vname.I inputX)))#(Updates t)
\<rparr>"
definition modify_2 :: "match list \<Rightarrow> tids \<Rightarrow> tids \<Rightarrow> iEFSM \<Rightarrow> iEFSM option" where
"modify_2 matches u1 u2 old = (let relevant = filter (\<lambda>(((_, u1'), io, _), (_, u2'), io', _). io = In \<and> io' = In \<and> (u1 = u1' \<or> u2 = u1' \<or> u1 = u2' \<or> u2 = u2')) matches;
newReg = case max_reg old of None \<Rightarrow> 1 | Some r \<Rightarrow> r + 1;
replacements = map (\<lambda>(((t1, u1), io1, inx1), (t2, u2), io2, inx2).
(((remove_guards_add_update t1 inx1 newReg, u1), io1, inx1),
(generalise_input t2 newReg inx2, u2), io2, inx2)) relevant;
comparisons = zip relevant replacements;
stripped_replacements = map strip_uids replacements;
to_replace = filter (\<lambda>(_, s). structural_count (strip_uids s) stripped_replacements > 1) comparisons in
if to_replace = [] then None else Some ((generalise_transitions to_replace old))
)"
(* type_synonym update_modifier = "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> (iEFSM \<times> (nat \<Rightarrow> nat) \<times> (nat \<Rightarrow> nat)) option" *)
definition heuristic_2 :: "log \<Rightarrow> update_modifier" where
"heuristic_2 l t1 t2 s new _ old check = (case modify_2 (find_intertrace_matches l old) t1 t2 new of
None \<Rightarrow> None |
Some e \<Rightarrow> if check (tm e) then Some e else None
)"
hide_const ioTag.In
end

View File

@ -0,0 +1,695 @@
subsection\<open>Store and Reuse Subsumption\<close>
text\<open>This theory provides proofs of various properties of the \emph{store and reuse} heuristic,
including the preconditions necessary for the transitions it introduces to directly subsume their
ungeneralised counterparts.\<close>
theory Store_Reuse_Subsumption
imports Store_Reuse
begin
lemma generalisation_of_preserves:
"is_generalisation_of t' t i r \<Longrightarrow>
Label t = Label t' \<and>
Arity t = Arity t' \<and>
(Outputs t) = (Outputs t')"
apply (simp add: is_generalisation_of_def)
using remove_guard_add_update_preserves by auto
lemma is_generalisation_of_guard_subset:
"is_generalisation_of t' t i r \<Longrightarrow> set (Guards t') \<subseteq> set (Guards t)"
by (simp add: is_generalisation_of_def remove_guard_add_update_def)
lemma is_generalisation_of_medial:
"is_generalisation_of t' t i r \<Longrightarrow>
can_take_transition t ip rg \<longrightarrow> can_take_transition t' ip rg"
using is_generalisation_of_guard_subset can_take_subset generalisation_of_preserves
by (metis (no_types, lifting) can_take_def can_take_transition_def)
lemma is_generalisation_of_preserves_reg:
"is_generalisation_of t' t i r \<Longrightarrow>
evaluate_updates t ia c $ r = c $ r"
by (simp add: is_generalisation_of_def r_not_updated_stays_the_same)
lemma apply_updates_foldr:
"apply_updates u old = foldr (\<lambda>h r. r(fst h $:= aval (snd h) old)) (rev u)"
by (simp add: apply_updates_def foldr_conv_fold)
lemma is_generalisation_of_preserves_reg_2:
assumes gen: "is_generalisation_of t' t i r"
and dif: "ra \<noteq> r"
shows "evaluate_updates t ia c $ ra = apply_updates (Updates t') (join_ir ia c) c $ ra"
using assms
apply (simp add: apply_updates_def is_generalisation_of_def remove_guard_add_update_def del: fold.simps)
by (simp add: apply_updates_def[symmetric] apply_updates_cons)
lemma is_generalisation_of_apply_guards:
"is_generalisation_of t' t i r \<Longrightarrow>
apply_guards (Guards t) j \<Longrightarrow>
apply_guards (Guards t') j"
using is_generalisation_of_guard_subset apply_guards_subset by blast
text \<open>If we drop the guard and add an update, and the updated register is undefined in the context,
c, then the generalised transition subsumes the specific one.\<close>
lemma is_generalisation_of_subsumes_original:
"is_generalisation_of t' t i r \<Longrightarrow>
c $ r = None \<Longrightarrow>
subsumes t' c t"
apply (simp add: subsumes_def generalisation_of_preserves can_take_transition_def can_take_def posterior_separate_def)
by (metis is_generalisation_of_apply_guards is_generalisation_of_preserves_reg is_generalisation_of_preserves_reg_2)
lemma generalise_output_posterior:
"posterior (generalise_output t p r) i ra = posterior t i ra"
by (simp add: can_take_def generalise_output_preserves posterior_def)
lemma generalise_output_eq: "(Outputs t) ! r = L v \<Longrightarrow>
c $ p = Some v \<Longrightarrow>
evaluate_outputs t i c = apply_outputs (list_update (Outputs t) r (V (R p))) (join_ir i c)"
apply (rule nth_equalityI)
apply (simp add: apply_outputs_preserves_length)
subgoal for j apply (case_tac "j = r")
apply (simp add: apply_outputs_literal apply_outputs_preserves_length apply_outputs_register)
by (simp add: apply_outputs_preserves_length apply_outputs_unupdated)
done
text\<open>This shows that if we can guarantee that the value of a particular register is the literal
output then the generalised output subsumes the specific output.\<close>
lemma generalise_output_subsumes_original:
"Outputs t ! r = L v \<Longrightarrow>
c $ p = Some v \<Longrightarrow>
subsumes (generalise_output t p r) c t"
by (simp add: can_take_transition_def generalise_output_def generalise_output_eq subsumes_def)
primrec stored_reused_aux_per_reg :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
"stored_reused_aux_per_reg t' t 0 p = (
if is_generalised_output_of t' t 0 p then
Some (0, p)
else
None
)" |
"stored_reused_aux_per_reg t' t (Suc r) p = (
if is_generalised_output_of t' t (Suc r) p then
Some (Suc r, p)
else
stored_reused_aux_per_reg t' t r p
)"
primrec stored_reused_aux :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
"stored_reused_aux t' t r 0 = stored_reused_aux_per_reg t' t r 0" |
"stored_reused_aux t' t r (Suc p) = (case stored_reused_aux_per_reg t' t r (Suc p) of
Some x \<Rightarrow> Some x |
None \<Rightarrow> stored_reused_aux t' t r p
)"
definition stored_reused :: "transition \<Rightarrow> transition \<Rightarrow> (nat \<times> nat) option" where
"stored_reused t' t = stored_reused_aux t' t (max (Transition.total_max_reg t) (Transition.total_max_reg t')) (max (length (Outputs t)) (length (Outputs t')))"
lemma stored_reused_aux_is_generalised_output_of:
"stored_reused_aux t' t mr mp = Some (p, r) \<Longrightarrow>
is_generalised_output_of t' t p r"
proof(induct mr)
case 0
then show ?case
proof(induct mp)
case 0
then show ?case
apply simp
by (metis option.distinct(1) option.inject prod.inject)
next
case (Suc mp)
then show ?case
apply (case_tac "is_generalised_output_of t' t 0 (Suc mp)")
by auto
qed
next
case (Suc mr)
then show ?case
proof(induct mp)
case 0
then show ?case
apply simp
by (metis option.inject prod.inject)
next
case (Suc mp)
then show ?case
apply simp
apply (case_tac "stored_reused_aux_per_reg t' t mr (Suc mp)")
apply simp
apply (case_tac "is_generalised_output_of t' t (Suc mr) (Suc mp)")
apply simp
apply simp
apply simp
apply (case_tac "is_generalised_output_of t' t (Suc mr) (Suc mp)")
by auto
qed
qed
lemma stored_reused_is_generalised_output_of:
"stored_reused t' t = Some (p, r) \<Longrightarrow>
is_generalised_output_of t' t p r"
by (simp add: stored_reused_def stored_reused_aux_is_generalised_output_of)
lemma is_generalised_output_of_subsumes:
"is_generalised_output_of t' t r p \<Longrightarrow>
nth (Outputs t) p = L v \<Longrightarrow>
c $ r = Some v \<Longrightarrow>
subsumes t' c t"
apply (simp add: subsumes_def generalise_output_preserves can_take_transition_def can_take_def posterior_separate_def)
by (simp add: generalise_output_def generalise_output_eq is_generalised_output_of_def)
lemma lists_neq_if:
"\<exists>i. l ! i \<noteq> l' ! i \<Longrightarrow> l \<noteq> l'"
by auto
lemma is_generalised_output_of_does_not_subsume:
"is_generalised_output_of t' t r p \<Longrightarrow>
p < length (Outputs t) \<Longrightarrow>
nth (Outputs t) p = L v \<Longrightarrow>
c $ r \<noteq> Some v \<Longrightarrow>
\<exists>i. can_take_transition t i c \<Longrightarrow>
\<not>subsumes t' c t"
apply (rule bad_outputs)
apply clarify
subgoal for i
apply (rule_tac x=i in exI)
apply simp
apply (rule lists_neq_if)
apply (rule_tac x=p in exI)
by (simp add: is_generalised_output_of_def generalise_output_def apply_outputs_nth join_ir_def)
done
text\<open>This shows that we can use the model checker to test whether the relevant register is the
correct value for direct subsumption.\<close>
lemma generalise_output_directly_subsumes_original:
"stored_reused t' t = Some (r, p) \<Longrightarrow>
nth (Outputs t) p = L v \<Longrightarrow>
(\<forall>c1 c2 t. obtains s c1 e1 0 <> t \<and> obtains s' c2 e2 0 <> t \<longrightarrow> c2 $ r = Some v) \<Longrightarrow>
directly_subsumes e1 e2 s s' t' t"
apply (simp add: directly_subsumes_def)
apply standard
by (metis is_generalised_output_of_subsumes stored_reused_aux_is_generalised_output_of stored_reused_def)
definition "generalise_output_context_check v r s1 s2 e1 e2 =
(\<forall>c1 c2 t. obtains s1 c1 (tm e1) 0 <> t \<and> obtains s2 c2 (tm e2) 0 <> t \<longrightarrow> c2 $ r = Some v)"
lemma generalise_output_context_check_directly_subsumes_original:
"stored_reused t' t = Some (r, p) \<Longrightarrow>
nth (Outputs t) p = L v \<Longrightarrow>
generalise_output_context_check v r s s' e1 e2 \<Longrightarrow>
directly_subsumes (tm e1) (tm e2) s s' t' t "
by (simp add: generalise_output_context_check_def generalise_output_directly_subsumes_original)
definition generalise_output_direct_subsumption :: "transition \<Rightarrow> transition \<Rightarrow> iEFSM \<Rightarrow> iEFSM \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"generalise_output_direct_subsumption t' t e e' s s' = (case stored_reused t' t of
None \<Rightarrow> False |
Some (r, p) \<Rightarrow>
(case nth (Outputs t) p of
L v \<Rightarrow> generalise_output_context_check v r s s' e e' |
_ \<Rightarrow> False)
)"
text\<open>This allows us to just run the two functions for quick subsumption.\<close>
lemma generalise_output_directly_subsumes_original_executable:
"generalise_output_direct_subsumption t' t e e' s s' \<Longrightarrow>
directly_subsumes (tm e) (tm e') s s' t' t"
apply (simp add: generalise_output_direct_subsumption_def)
apply (case_tac "stored_reused t' t")
apply simp
apply simp
subgoal for a
apply (case_tac a)
apply simp
subgoal for _ b
apply (case_tac "Outputs t ! b")
apply (simp add: generalise_output_context_check_directly_subsumes_original)
by auto
done
done
lemma original_does_not_subsume_generalised_output:
"stored_reused t' t = Some (p, r) \<Longrightarrow>
r < length (Outputs t) \<Longrightarrow>
nth (Outputs t) r = L v \<Longrightarrow>
\<exists>a c1 tt. obtains s c1 e1 0 <> tt \<and> obtains s' a e 0 <> tt \<and> a $ p \<noteq> Some v \<and> (\<exists>i. can_take_transition t i a) \<Longrightarrow>
\<not>directly_subsumes e1 e s s' t' t"
apply (simp add: directly_subsumes_def)
apply clarify
subgoal for a c1 tt i
apply (rule_tac x=c1 in exI)
apply (rule_tac x=a in exI)
using stored_reused_is_generalised_output_of[of t' t p r]
is_generalised_output_of_does_not_subsume[of t' t p r v]
by auto
done
(* t' is the generalised transition *)
primrec input_i_stored_in_reg :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
"input_i_stored_in_reg t' t i 0 = (if is_generalisation_of t' t i 0 then Some (i, 0) else None)" |
"input_i_stored_in_reg t' t i (Suc r) = (if is_generalisation_of t' t i (Suc r) then Some (i, (Suc r)) else input_i_stored_in_reg t' t i r)"
(* t' is the generalised transition *)
primrec input_stored_in_reg_aux :: "transition \<Rightarrow> transition \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where
"input_stored_in_reg_aux t' t 0 r = input_i_stored_in_reg t' t 0 r" |
"input_stored_in_reg_aux t' t (Suc i) r = (case input_i_stored_in_reg t' t (Suc i) r of
None \<Rightarrow> input_i_stored_in_reg t' t i r |
Some (i, r) \<Rightarrow> Some (i, r)
) "
(* t' is the generalised transition *)
definition input_stored_in_reg :: "transition \<Rightarrow> transition \<Rightarrow> iEFSM \<Rightarrow> (nat \<times> nat) option" where
"input_stored_in_reg t' t e = (
case input_stored_in_reg_aux t' t (total_max_reg e) (max (Arity t) (Arity t')) of
None \<Rightarrow> None |
Some (i, r) \<Rightarrow>
if length (filter (\<lambda>(r', u). r' = r) (Updates t')) = 1 then
Some (i, r)
else None
)"
definition initially_undefined_context_check :: "transition_matrix \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"initially_undefined_context_check e r s = (\<forall>t a. obtains s a e 0 <> t \<longrightarrow> a $ r = None)"
lemma no_incoming_to_zero:
"\<forall>((from, to), t)|\<in>|e. 0 < to \<Longrightarrow>
(aaa, ba) |\<in>| possible_steps e s d l i \<Longrightarrow>
aaa \<noteq> 0"
proof(induct e)
case empty
then show ?case
by (simp add: possible_steps_def)
next
case (insert x e)
then show ?case
apply (cases x)
subgoal for a b
apply (case_tac a)
apply (simp add: possible_steps_def ffilter_finsert)
subgoal for aa bb
apply (case_tac "aa = s \<and> Label b = l \<and> length i = Arity b \<and> apply_guards (Guards b) (join_ir i d)")
apply simp
apply blast
by simp
done
done
qed
lemma no_return_to_zero:
"\<forall>((from, to), t)|\<in>|e. 0 < to \<Longrightarrow>
\<forall>r n. \<not> visits 0 e (Suc n) r t"
proof(induct t)
case Nil
then show ?case
by (simp add: no_further_steps)
next
case (Cons a t)
then show ?case
apply clarify
apply (rule visits.cases)
apply simp
apply simp
defer
apply simp
apply clarify
apply simp
by (metis no_incoming_to_zero not0_implies_Suc)
qed
lemma no_accepting_return_to_zero:
"\<forall>((from, to), t)|\<in>|e. to \<noteq> 0 \<Longrightarrow>
recognises (e) (a#t) \<Longrightarrow>
\<not>visits 0 (e) 0 <> (a#t)"
apply clarify
apply (rule visits.cases)
apply simp
apply simp
apply clarify
apply simp
by (metis no_incoming_to_zero no_return_to_zero old.nat.exhaust)
lemma no_return_to_zero_must_be_empty:
"\<forall>((from, to), t)|\<in>|e. to \<noteq> 0 \<Longrightarrow>
obtains 0 a e s r t \<Longrightarrow>
t = []"
proof(induct t arbitrary: s r)
case Nil
then show ?case
by simp
next
case (Cons a t)
then show ?case
apply simp
apply (rule obtains.cases)
apply simp
apply simp
by (metis (no_types, lifting) case_prodE fBexE list.inject no_further_steps no_incoming_to_zero unobtainable_if)
qed
definition "no_illegal_updates t r = (\<forall>u \<in> set (Updates t). fst u \<noteq> r)"
lemma input_stored_in_reg_aux_is_generalisation_aux:
"input_stored_in_reg_aux t' t mr mi = Some (i, r) \<Longrightarrow>
is_generalisation_of t' t i r"
proof(induct mi)
case 0
then show ?case
proof(induct mr)
case 0
then show ?case
apply (case_tac "is_generalisation_of t' t 0 0")
by auto
next
case (Suc mr)
then show ?case
apply simp
apply (case_tac "is_generalisation_of t' t (Suc mr) 0")
apply simp
apply simp
apply (case_tac "is_generalisation_of t' t mr 0")
by auto
qed
next
case (Suc mi)
then show ?case
proof(induct mr)
case 0
then show ?case
apply (case_tac "is_generalisation_of t' t 0 (Suc mi)")
by auto
next
case (Suc mr)
then show ?case
apply simp
apply (case_tac "is_generalisation_of t' t (Suc mr) (Suc mi)")
apply simp
apply simp
apply (case_tac "input_i_stored_in_reg t' t (Suc mr) mi")
apply simp
apply (case_tac "is_generalisation_of t' t mr (Suc mi)")
by auto
qed
qed
lemma input_stored_in_reg_is_generalisation:
"input_stored_in_reg t' t e = Some (i, r) \<Longrightarrow> is_generalisation_of t' t i r"
apply (simp add: input_stored_in_reg_def)
apply (cases "input_stored_in_reg_aux t' t (total_max_reg e) (max (Arity t) (Arity t'))")
apply simp
subgoal for a
apply (case_tac a)
apply simp
subgoal for _ b
apply (case_tac "length (filter (\<lambda>(r', u). r' = b) (Updates t')) = 1")
apply (simp add: input_stored_in_reg_aux_is_generalisation_aux)
by simp
done
done
(*
This allows us to call these three functions for direct subsumption of generalised
*)
lemma generalised_directly_subsumes_original:
"input_stored_in_reg t' t e = Some (i, r) \<Longrightarrow>
initially_undefined_context_check (tm e) r s' \<Longrightarrow>
no_illegal_updates t r \<Longrightarrow>
directly_subsumes (tm e1) (tm e) s s' t' t"
apply (simp add: directly_subsumes_def)
apply standard
apply (meson finfun_const.rep_eq input_stored_in_reg_is_generalisation is_generalisation_of_subsumes_original)
apply (rule is_generalisation_of_subsumes_original)
using input_stored_in_reg_is_generalisation apply blast
by (simp add: initially_undefined_context_check_def)
definition drop_guard_add_update_direct_subsumption :: "transition \<Rightarrow> transition \<Rightarrow> iEFSM \<Rightarrow> nat \<Rightarrow> bool" where
"drop_guard_add_update_direct_subsumption t' t e s' = (
case input_stored_in_reg t' t e of
None \<Rightarrow> False |
Some (i, r) \<Rightarrow>
if no_illegal_updates t r then
initially_undefined_context_check (tm e) r s'
else False
)"
lemma drop_guard_add_update_direct_subsumption_implies_direct_subsumption:
"drop_guard_add_update_direct_subsumption t' t e s' \<Longrightarrow>
directly_subsumes (tm e1) (tm e) s s' t' t"
apply (simp add: drop_guard_add_update_direct_subsumption_def)
apply (case_tac "input_stored_in_reg t' t e")
apply simp+
subgoal for a
apply (case_tac a)
apply simp
subgoal for _ b
apply (case_tac "no_illegal_updates t b")
apply (simp add: generalised_directly_subsumes_original)
by simp
done
done
lemma is_generalisation_of_constrains_input:
"is_generalisation_of t' t i r \<Longrightarrow>
\<exists>v. gexp.Eq (V (vname.I i)) (L v) \<in> set (Guards t)"
by (simp add: is_generalisation_of_def)
lemma is_generalisation_of_derestricts_input:
"is_generalisation_of t' t i r \<Longrightarrow>
\<forall>g \<in> set (Guards t'). \<not> gexp_constrains g (V (vname.I i))"
by (simp add: is_generalisation_of_def remove_guard_add_update_def)
lemma is_generalisation_of_same_arity:
"is_generalisation_of t' t i r \<Longrightarrow> Arity t = Arity t'"
by (simp add: is_generalisation_of_def remove_guard_add_update_def)
lemma is_generalisation_of_i_lt_arity:
"is_generalisation_of t' t i r \<Longrightarrow> i < Arity t"
by (simp add: is_generalisation_of_def)
lemma "\<forall>i. \<not> can_take_transition t i r \<and> \<not> can_take_transition t' i r \<Longrightarrow>
Label t = Label t' \<Longrightarrow>
Arity t = Arity t' \<Longrightarrow>
subsumes t' r t"
by (simp add: subsumes_def posterior_separate_def can_take_transition_def)
lemma input_not_constrained_aval_swap_inputs:
"\<not> aexp_constrains a (V (I v)) \<Longrightarrow> aval a (join_ir i c) = aval a (join_ir (list_update i v x) c)"
apply(induct a rule: aexp_induct_separate_V_cases)
apply simp
apply (metis aexp_constrains.simps(2) aval.simps(2) input2state_nth input2state_out_of_bounds join_ir_def length_list_update not_le nth_list_update_neq vname.simps(5))
using join_ir_def by auto
lemma aval_unconstrained:
" \<not> aexp_constrains a (V (vname.I i)) \<Longrightarrow>
i < length ia \<Longrightarrow>
v = ia ! i \<Longrightarrow>
v' \<noteq> v \<Longrightarrow>
aval a (join_ir ia c) = aval a (join_ir (list_update ia i v') c)"
apply(induct a rule: aexp_induct_separate_V_cases)
using input_not_constrained_aval_swap_inputs by blast+
lemma input_not_constrained_gval_swap_inputs:
"\<not> gexp_constrains a (V (I v)) \<Longrightarrow>
gval a (join_ir i c) = gval a (join_ir (i[v := x]) c)"
proof(induct a)
case (Bc x)
then show ?case
by (metis (full_types) gval.simps(1) gval.simps(2))
next
case (Eq x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (Gt x1a x2)
then show ?case
using input_not_constrained_aval_swap_inputs by auto
next
case (In x1a x2)
then show ?case
apply simp
apply (case_tac "join_ir i c x1a")
apply simp
apply (case_tac "join_ir (i[v := x]) c x1a")
apply simp
apply simp
apply (metis aexp.inject(2) aexp_constrains.simps(2) aval.simps(2) input_not_constrained_aval_swap_inputs option.discI)
apply (case_tac "join_ir i c x1a")
apply simp
apply (case_tac "join_ir (i[v := x]) c x1a")
apply simp
apply (metis aexp.inject(2) aexp_constrains.simps(2) aval.simps(2) input_not_constrained_aval_swap_inputs option.discI)
apply simp
by (metis (no_types, lifting) datastate(1) input2state_within_bounds join_ir_R join_ir_nth le_less_linear list_update_beyond nth_list_update option.inject vname.case(1) vname.exhaust)
qed auto
text\<open>If input $i$ is stored in register $r$ by transition $t$ then if we can take transition,
$t^\prime$ then for some input $ia$ then transition $t$ does not subsume $t^\prime$.\<close>
lemma input_stored_in_reg_not_subsumed:
"input_stored_in_reg t' t e = Some (i, r) \<Longrightarrow>
\<exists>ia. can_take_transition t' ia c \<Longrightarrow>
\<not> subsumes t c t'"
using input_stored_in_reg_is_generalisation[of t' t e i r]
using is_generalisation_of_constrains_input[of t' t i r]
using is_generalisation_of_derestricts_input[of t' t i r]
apply simp
apply (rule bad_guards)
apply clarify
subgoal for ia v
apply (simp add: can_take_transition_def can_take_def)
apply clarify
apply (case_tac "v")
subgoal for x1
apply (rule_tac x="list_update ia i (Str _)" in exI)
apply simp
apply standard
apply (simp add: apply_guards_def)
apply (metis input_not_constrained_gval_swap_inputs)
apply (simp add: apply_guards_def Bex_def)
apply standard
apply (rule_tac x="Eq (V (vname.I i)) (L (Num x1))" in exI)
apply (simp add: join_ir_def input2state_nth is_generalisation_of_i_lt_arity str_not_num)
done
subgoal for x2
apply (rule_tac x="list_update ia i (Num _)" in exI)
apply simp
apply standard
apply (simp add: apply_guards_def)
apply (metis input_not_constrained_gval_swap_inputs)
apply (simp add: apply_guards_def Bex_def)
apply standard
apply (rule_tac x="Eq (V (vname.I i)) (L (value.Str x2))" in exI)
by (simp add: join_ir_def input2state_nth is_generalisation_of_i_lt_arity str_not_num)
done
done
lemma aval_updated:
"(r, u) \<in> set U \<Longrightarrow>
r \<notin> set (map fst (removeAll (r, u) U)) \<Longrightarrow>
apply_updates U s c $ r = aval u s"
proof(induct U rule: rev_induct)
case (snoc a U)
then show ?case
apply (case_tac "(r, u) = a")
using apply_updates_foldr by auto
qed auto
lemma can_take_append_subset:
"set (Guards t') \<subset> set (Guards t) \<Longrightarrow>
can_take a (Guards t @ Guards t') ia c = can_take a (Guards t) ia c"
by (metis apply_guards_append apply_guards_subset_append can_take_def dual_order.strict_implies_order)
text\<open>Transitions of the form $t = \textit{select}:1[i_0=x]$ do not subsume transitions
of the form $t^\prime = select:1/r_1:=i_1$.\<close>
lemma general_not_subsume_orig: "Arity t' = Arity t \<Longrightarrow>
set (Guards t') \<subset> set (Guards t) \<Longrightarrow>
(r, (V (I i))) \<in> set (Updates t') \<Longrightarrow>
r \<notin> set (map fst (removeAll (r, V (I i)) (Updates t'))) \<Longrightarrow>
r \<notin> set (map fst (Updates t)) \<Longrightarrow>
\<exists>i. can_take_transition t i c \<Longrightarrow>
c $ r = None \<Longrightarrow>
i < Arity t \<Longrightarrow>
\<not> subsumes t c t'"
apply (rule inconsistent_updates)
apply (erule_tac exE)
subgoal for ia
apply (rule_tac x="evaluate_updates t ia c" in exI)
apply (rule_tac x="apply_updates (Updates t') (join_ir ia c) c" in exI)
apply standard
apply (rule_tac x=ia in exI)
apply (metis can_take_def can_take_transition_def can_take_subset posterior_separate_def psubsetE)
apply (rule_tac x=r in exI)
apply (simp add: r_not_updated_stays_the_same)
apply (rule_tac x="\<lambda>x. x = None" in exI)
by (simp add: aval_updated can_take_transition_def can_take_def)
done
lemma input_stored_in_reg_updates_reg:
"input_stored_in_reg t2 t1 a = Some (i, r) \<Longrightarrow>
(r, V (I i)) \<in> set (Updates t2)"
using input_stored_in_reg_is_generalisation[of t2 t1 a i r]
apply simp
by (simp add: is_generalisation_of_def remove_guard_add_update_def)
definition "diff_outputs_ctx e1 e2 s1 s2 t1 t2 =
(if Outputs t1 = Outputs t2 then False else
(\<exists>p c1 r. obtains s1 c1 e1 0 <> p \<and>
obtains s2 r e2 0 <> p \<and>
(\<exists>i. can_take_transition t1 i r \<and> can_take_transition t2 i r \<and>
evaluate_outputs t1 i r \<noteq> evaluate_outputs t2 i r)
))"
lemma diff_outputs_direct_subsumption:
"diff_outputs_ctx e1 e2 s1 s2 t1 t2 \<Longrightarrow>
\<not> directly_subsumes e1 e2 s1 s2 t1 t2"
apply (simp add: directly_subsumes_def diff_outputs_ctx_def)
apply (case_tac "Outputs t1 = Outputs t2")
apply simp
apply clarsimp
subgoal for _ c1 r
apply (rule_tac x=c1 in exI)
apply (rule_tac x=r in exI)
using bad_outputs by force
done
definition not_updated :: "nat \<Rightarrow> transition \<Rightarrow> bool" where
"not_updated r t = (filter (\<lambda>(r', _). r' = r) (Updates t) = [])"
lemma not_updated: assumes "not_updated r t2"
shows "apply_updates (Updates t2) s s' $ r = s' $ r"
proof-
have not_updated_aux: "\<And>t2. filter (\<lambda>(r', _). r' = r) t2 = [] \<Longrightarrow>
apply_updates t2 s s' $ r = s' $ r"
apply (rule r_not_updated_stays_the_same)
by (metis (mono_tags, lifting) filter_empty_conv imageE prod.case_eq_if)
show ?thesis
using assms
by (simp add: not_updated_def not_updated_aux)
qed
lemma one_extra_update_subsumes: "Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
set (Guards t1) \<subseteq> set (Guards t2) \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = (r, u) # Updates t2 \<Longrightarrow>
not_updated r t2 \<Longrightarrow>
c $ r = None \<Longrightarrow>
subsumes t1 c t2"
apply (simp add: subsumes_def posterior_separate_def can_take_transition_def can_take_def)
by (metis apply_guards_subset apply_updates_cons not_updated)
lemma one_extra_update_directly_subsumes:
"Label t1 = Label t2 \<Longrightarrow>
Arity t1 = Arity t2 \<Longrightarrow>
set (Guards t1) \<subseteq> set (Guards t2) \<Longrightarrow>
Outputs t1 = Outputs t2 \<Longrightarrow>
Updates t1 = (r, u)#(Updates t2) \<Longrightarrow>
not_updated r t2 \<Longrightarrow>
initially_undefined_context_check e2 r s2 \<Longrightarrow>
directly_subsumes e1 e2 s1 s2 t1 t2"
apply (simp add: directly_subsumes_def)
apply standard
apply (meson one_extra_update_subsumes finfun_const_apply)
apply (simp add: initially_undefined_context_check_def)
using obtainable_def one_extra_update_subsumes by auto
definition "one_extra_update t1 t2 s2 e2 = (
Label t1 = Label t2 \<and>
Arity t1 = Arity t2 \<and>
set (Guards t1) \<subseteq> set (Guards t2) \<and>
Outputs t1 = Outputs t2 \<and>
Updates t1 \<noteq> [] \<and>
tl (Updates t1) = (Updates t2) \<and>
(\<exists>r \<in> set (map fst (Updates t1)). fst (hd (Updates t1)) = r \<and>
not_updated r t2 \<and>
initially_undefined_context_check e2 r s2)
)"
lemma must_be_an_update:
"U1 \<noteq> [] \<Longrightarrow>
fst (hd U1) = r \<and> tl U1 = U2 \<Longrightarrow>
\<exists>u. U1 = (r, u)#(U2)"
by (metis eq_fst_iff hd_Cons_tl)
lemma one_extra_update_direct_subsumption:
"one_extra_update t1 t2 s2 e2 \<Longrightarrow> directly_subsumes e1 e2 s1 s2 t1 t2"
apply (insert must_be_an_update[of "Updates t1" r "Updates t2"])
apply (simp add: one_extra_update_def)
by (metis eq_fst_iff hd_Cons_tl one_extra_update_directly_subsumes)
end

View File

@ -0,0 +1,53 @@
subsection\<open>Weak Subsumption\<close>
text\<open>Unfortunately, the \emph{direct subsumption} relation cannot be transformed into executable
code. To solve this problem, \cite{foster2019} advocates for the use of a model checker, but this
turns out to be prohibitively slow for all but the smallest of examples. To solve this problem, we
must make a practical compromise and use another heuristic: the \emph{weak subsumption} heuristic.
This heuristic simply tries to delete each transition in turn and runs the original traces used to
build the PTA are still accepted. If so, this is taken as an acceptable substitute for direct
subsumption.
The acceptability of this, with respect to model behaviour, is justified by the fact that the
original traces are checked for acceptance. In situations where one transition genuinely does
directly subsume the other, the merge will go ahead as normal. In situations where one transition
does not directly subsume the other, the merge may still go ahead if replacing one transition with
the other still allows the model to accept the original traces. In this case, the heuristic makes an
overgeneralisation, but this is deemed to be acceptable since this is what heuristics are for. This
approach is clearly not as formal as we would like, but the compromise is necessary to allow models
to be inferred in reasonable time.\<close>
theory Weak_Subsumption
imports "../Inference"
begin
definition maxBy :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
"maxBy f a b = (if (f a > f b) then a else b)"
fun weak_subsumption :: "update_modifier" where
"weak_subsumption t1ID t2ID s new _ old check = (let
t1 = get_by_ids new t1ID;
t2 = get_by_ids new t2ID
in
if
same_structure t1 t2
then
let
maxT = maxBy (\<lambda>x. ((length \<circ> Updates) x, map snd (Updates x))) t1 t2;
minT = if maxT = t1 then t2 else t1;
newEFSMmax = replace_all new [t1ID, t2ID] maxT in
\<comment> \<open>Most of the time, we'll want the transition with the most updates so start with that one\<close>
if check (tm newEFSMmax) then
Some newEFSMmax
else
\<comment> \<open>There may be other occasions where we want to try the other transition\<close>
\<comment> \<open>e.g. if their updates are equal but one has a different guard\<close>
let newEFSMmin = replace_all new [t1ID, t2ID] minT in
if check (tm newEFSMmin) then
Some newEFSMmin
else
None
else
None
)"
end