189 lines
8.4 KiB
Plaintext
189 lines
8.4 KiB
Plaintext
chapter\<open>Models\<close>
|
|
text\<open>In this chapter, we present our formalisation of EFSMs from \cite{foster2018}. We first
|
|
define transitions, before defining EFSMs as finite sets of transitions between states. Finally,
|
|
we provide a framework of function definitions and key lemmas such that LTL properties over EFSMs
|
|
can be more easily specified and proven.\<close>
|
|
|
|
section\<open>Transitions\<close>
|
|
text\<open>Here we define the transitions which make up EFSMs. As per \cite{foster2018}, each transition
|
|
has a label and an arity and, optionally, guards, outputs, and updates. To implement this, we use
|
|
the record type such that each component of the transition can be accessed.\<close>
|
|
|
|
theory Transition
|
|
imports GExp
|
|
begin
|
|
|
|
type_synonym label = String.literal
|
|
type_synonym arity = nat
|
|
type_synonym guard = "vname gexp"
|
|
type_synonym inputs = "value list"
|
|
type_synonym outputs = "value option list"
|
|
type_synonym output_function = "vname aexp"
|
|
type_synonym update_function = "nat \<times> vname aexp"
|
|
|
|
text_raw\<open>\snip{transitiontype}{1}{2}{%\<close>
|
|
record transition =
|
|
Label :: String.literal
|
|
Arity :: nat
|
|
Guards :: "guard list"
|
|
Outputs :: "output_function list"
|
|
Updates :: "update_function list"
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
definition same_structure :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
|
|
"same_structure t1 t2 = (
|
|
Label t1 = Label t2 \<and>
|
|
Arity t1 = Arity t2 \<and>
|
|
length (Outputs t1) = length (Outputs t2)
|
|
)"
|
|
|
|
definition enumerate_inputs :: "transition \<Rightarrow> nat set" where
|
|
"enumerate_inputs t = (\<Union> (set (map enumerate_gexp_inputs (Guards t)))) \<union>
|
|
(\<Union> (set (map enumerate_aexp_inputs (Outputs t)))) \<union>
|
|
(\<Union> (set (map (\<lambda>(_, u). enumerate_aexp_inputs u) (Updates t))))"
|
|
|
|
definition max_input :: "transition \<Rightarrow> nat option" where
|
|
"max_input t = (if enumerate_inputs t = {} then None else Some (Max (enumerate_inputs t)))"
|
|
|
|
definition total_max_input :: "transition \<Rightarrow> nat" where
|
|
"total_max_input t = (case max_input t of None \<Rightarrow> 0 | Some a \<Rightarrow> a)"
|
|
|
|
definition enumerate_regs :: "transition \<Rightarrow> nat set" where
|
|
"enumerate_regs t = (\<Union> (set (map GExp.enumerate_regs (Guards t)))) \<union>
|
|
(\<Union> (set (map AExp.enumerate_regs (Outputs t)))) \<union>
|
|
(\<Union> (set (map (\<lambda>(_, u). AExp.enumerate_regs u) (Updates t)))) \<union>
|
|
(\<Union> (set (map (\<lambda>(r, _). AExp.enumerate_regs (V (R r))) (Updates t))))"
|
|
|
|
definition max_reg :: "transition \<Rightarrow> nat option" where
|
|
"max_reg t = (if enumerate_regs t = {} then None else Some (Max (enumerate_regs t)))"
|
|
|
|
definition total_max_reg :: "transition \<Rightarrow> nat" where
|
|
"total_max_reg t = (case max_reg t of None \<Rightarrow> 0 | Some a \<Rightarrow> a)"
|
|
|
|
definition enumerate_ints :: "transition \<Rightarrow> int set" where
|
|
"enumerate_ints t = (\<Union> (set (map enumerate_gexp_ints (Guards t)))) \<union>
|
|
(\<Union> (set (map enumerate_aexp_ints (Outputs t)))) \<union>
|
|
(\<Union> (set (map (\<lambda>(_, u). enumerate_aexp_ints u) (Updates t)))) \<union>
|
|
(\<Union> (set (map (\<lambda>(r, _). enumerate_aexp_ints (V (R r))) (Updates t))))"
|
|
|
|
definition valid_transition :: "transition \<Rightarrow> bool" where
|
|
"valid_transition t = (\<forall>i \<in> enumerate_inputs t. i < Arity t)"
|
|
|
|
definition can_take :: "nat \<Rightarrow> vname gexp list \<Rightarrow> inputs \<Rightarrow> registers \<Rightarrow> bool" where
|
|
"can_take a g i r = (length i = a \<and> apply_guards g (join_ir i r))"
|
|
|
|
lemma can_take_empty [simp]: "length i = a \<Longrightarrow> can_take a [] i c"
|
|
by (simp add: can_take_def)
|
|
|
|
lemma can_take_subset_append:
|
|
assumes "set (Guards t) \<subseteq> set (Guards t')"
|
|
shows "can_take a (Guards t @ Guards t') i c = can_take a (Guards t') i c"
|
|
using assms
|
|
by (simp add: apply_guards_subset_append can_take_def)
|
|
|
|
definition "can_take_transition t i r = can_take (Arity t) (Guards t) i r"
|
|
|
|
lemmas can_take = can_take_def can_take_transition_def
|
|
|
|
lemma can_take_transition_empty_guard:
|
|
"Guards t = [] \<Longrightarrow> \<exists>i. can_take_transition t i c"
|
|
by (simp add: can_take_transition_def can_take_def Ex_list_of_length)
|
|
|
|
lemma can_take_subset: "length i = Arity t \<Longrightarrow>
|
|
Arity t = Arity t' \<Longrightarrow>
|
|
set (Guards t') \<subseteq> set (Guards t) \<Longrightarrow>
|
|
can_take_transition t i r \<Longrightarrow>
|
|
can_take_transition t' i r"
|
|
by (simp add: can_take_transition_def can_take_def apply_guards_subset)
|
|
|
|
lemma valid_list_can_take:
|
|
"\<forall>g \<in> set (Guards t). valid g \<Longrightarrow> \<exists>i. can_take_transition t i c"
|
|
by (simp add: can_take_transition_def can_take_def apply_guards_def valid_def Ex_list_of_length)
|
|
|
|
lemma cant_take_if:
|
|
"\<exists>g \<in> set (Guards t). gval g (join_ir i r) \<noteq> true \<Longrightarrow>
|
|
\<not> can_take_transition t i r"
|
|
using apply_guards_cons apply_guards_rearrange can_take_def can_take_transition_def by blast
|
|
|
|
definition apply_outputs :: "'a aexp list \<Rightarrow> 'a datastate \<Rightarrow> value option list" where
|
|
"apply_outputs p s = map (\<lambda>p. aval p s) p"
|
|
|
|
abbreviation "evaluate_outputs t i r \<equiv> apply_outputs (Outputs t) (join_ir i r)"
|
|
|
|
lemma apply_outputs_nth:
|
|
"i < length p \<Longrightarrow> apply_outputs p s ! i = aval (p ! i) s"
|
|
by (simp add: apply_outputs_def)
|
|
|
|
lemmas apply_outputs = datastate apply_outputs_def value_plus_def value_minus_def value_times_def
|
|
|
|
lemma apply_outputs_empty [simp]: "apply_outputs [] s = []"
|
|
by (simp add: apply_outputs_def)
|
|
|
|
lemma apply_outputs_preserves_length: "length (apply_outputs p s) = length p"
|
|
by (simp add: apply_outputs_def)
|
|
|
|
lemma apply_outputs_literal: assumes "P ! r = L v"
|
|
and "r < length P"
|
|
shows "apply_outputs P s ! r = Some v"
|
|
by (simp add: assms apply_outputs_nth)
|
|
|
|
lemma apply_outputs_register: assumes "r < length P"
|
|
shows "apply_outputs (list_update P r (V (R p))) (join_ir i c) ! r = c $ p"
|
|
by (metis apply_outputs_nth assms aval.simps(2) join_ir_R length_list_update nth_list_update_eq)
|
|
|
|
lemma apply_outputs_unupdated: assumes "ia \<noteq> r"
|
|
and "ia < length P"
|
|
shows "apply_outputs P j ! ia = apply_outputs (list_update P r v)j ! ia"
|
|
by (metis apply_outputs_nth assms(1) assms(2) length_list_update nth_list_update_neq)
|
|
|
|
definition apply_updates :: "update_function list \<Rightarrow> vname datastate \<Rightarrow> registers \<Rightarrow> registers" where
|
|
"apply_updates u old = fold (\<lambda>h r. r(fst h $:= aval (snd h) old)) u"
|
|
|
|
abbreviation "evaluate_updates t i r \<equiv> apply_updates (Updates t) (join_ir i r) r"
|
|
|
|
lemma apply_updates_cons: "ra \<noteq> r \<Longrightarrow>
|
|
apply_updates u (join_ir ia c) c $ ra = apply_updates ((r, a) # u) (join_ir ia c) c $ ra"
|
|
proof(induct u rule: rev_induct)
|
|
case Nil
|
|
then show ?case
|
|
by (simp add: apply_updates_def)
|
|
next
|
|
case (snoc u us)
|
|
then show ?case
|
|
apply (cases u)
|
|
apply (simp add: apply_updates_def)
|
|
by (case_tac "ra = aa", auto)
|
|
qed
|
|
|
|
lemma update_twice:
|
|
"apply_updates [(r, a), (r, b)] s regs = regs (r $:= aval b s)"
|
|
by (simp add: apply_updates_def)
|
|
|
|
lemma r_not_updated_stays_the_same:
|
|
"r \<notin> fst ` set U \<Longrightarrow> apply_updates U c d $ r = d $ r"
|
|
using apply_updates_def
|
|
by (induct U rule: rev_induct, auto)
|
|
|
|
definition rename_regs :: "(nat \<Rightarrow> nat) \<Rightarrow> transition \<Rightarrow> transition" where
|
|
"rename_regs f t = t\<lparr>
|
|
Guards := map (GExp.rename_regs f) (Guards t),
|
|
Outputs := map (AExp.rename_regs f) (Outputs t),
|
|
Updates := map (\<lambda>(r, u). (f r, AExp.rename_regs f u)) (Updates t)
|
|
\<rparr>"
|
|
|
|
definition eq_upto_rename_strong :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
|
|
"eq_upto_rename_strong t1 t2 = (\<exists>f. bij f \<and> rename_regs f t1 = t2)"
|
|
|
|
inductive eq_upto_rename :: "transition \<Rightarrow> transition \<Rightarrow> bool" where
|
|
"Label t1 = Label t2 \<Longrightarrow>
|
|
Arity t2 = Arity t2 \<Longrightarrow>
|
|
apply_guards (map (GExp.rename_regs f) (Guards t1)) = apply_guards (Guards t2) \<Longrightarrow>
|
|
|
|
apply_outputs (map (AExp.rename_regs f) (Outputs t1)) = apply_outputs (Outputs t2) \<Longrightarrow>
|
|
|
|
apply_updates (map (\<lambda>(r, u). (f r, AExp.rename_regs f u)) (Updates t1)) = apply_updates (Updates t2) \<Longrightarrow>
|
|
|
|
eq_upto_rename t1 t2"
|
|
|
|
end
|