abbreviation label :: "state \<Rightarrow> String.literal" where
"label s \<equiv> fst (action s)"
abbreviation inputs :: "state \<Rightarrow> value list" where
"inputs s \<equiv> snd (action s)"
text_raw\<open>\snip{ltlStep}{1}{2}{%\<close>
fun ltl_step :: "transition_matrix \<Rightarrow> cfstate option \<Rightarrow> registers \<Rightarrow> action \<Rightarrow> (nat option \<times> outputs \<times> registers)" where
"ltl_step _ None r _ = (None, [], r)" |
"ltl_step e (Some s) r (l, i) = (let possibilities = possible_steps e s r l i in
if possibilities = {||} then (None, [], r)
else
let (s', t) = Eps (\<lambda>x. x |\<in>| possibilities) in
(Some s', (evaluate_outputs t i r), (evaluate_updates t i r))
)"
text_raw\<open>}%endsnip\<close>
lemma ltl_step_singleton:
"\<exists>t. possible_steps e n r (fst v) (snd v) = {|(aa, t)|} \<and> evaluate_outputs t (snd v) r = b \<and> evaluate_updates t (snd v) r = c\<Longrightarrow>
ltl_step e (Some n) r v = (Some aa, b, c)"
apply (cases v)
by auto
lemma ltl_step_none: "possible_steps e s r a b = {||} \<Longrightarrow> ltl_step e (Some s) r (a, b) = (None, [], r)"
by simp
lemma ltl_step_none_2: "possible_steps e s r (fst ie) (snd ie) = {||} \<Longrightarrow> ltl_step e (Some s) r ie = (None, [], r)"
by (metis ltl_step_none prod.exhaust_sel)
lemma ltl_step_alt: "ltl_step e (Some s) r t = (
let possibilities = possible_steps e s r (fst t) (snd t) in
if possibilities = {||} then
(None, [], r)
else
let (s', t') = Eps (\<lambda>x. x |\<in>| possibilities) in
text\<open>The \textsc{check\_exp} function takes a guard expression and returns true if the guard
expression evaluates to true in the given state.\<close>
type_synonym ltl_gexp = "ltl_vname gexp"
definition join_iro :: "value list \<Rightarrow> registers \<Rightarrow> outputs \<Rightarrow> ltl_vname datastate" where
"join_iro i r p = (\<lambda>x. case x of
Rg n \<Rightarrow> r $ n |
Ip n \<Rightarrow> Some (i ! n) |
Op n \<Rightarrow> p ! n
)"
lemma join_iro_R [simp]: "join_iro i r p (Rg n) = r $ n"
by (simp add: join_iro_def)
abbreviation "check_exp g s \<equiv> (gval g (join_iro (snd (action (shd s))) (datastate (shd s)) (output (shd s))) = trilean.true)"
lemma alw_ev: "alw f = not (ev (\<lambda>s. \<not>f s))"
by simp
lemma alw_state_eq_smap:
"alw (state_eq s) ss = alw (\<lambda>ss. shd ss = s) (smap statename ss)"
apply standard
apply (simp add: alw_iff_sdrop )
by (simp add: alw_mono alw_smap )
subsection\<open>Sink State\<close>
text\<open>Once the sink state is entered, it cannot be left and there are no outputs or updates
henceforth.\<close>
lemma shd_state_is_none: "(state_eq None) (make_full_observation e None r p t)"
by (simp add: )
lemma unfold_observe_none: "make_full_observation e None d p t = (\<lparr>statename = None, datastate = d, action=(shd t), output = p\<rparr>##(make_full_observation e None d [] (stl t)))"
by (simp add: stream.expand)
lemma once_none_always_none_aux:
assumes "\<exists> p r i. j = (make_full_observation e None r p) i"
shows "alw (state_eq None) j"
using assms apply coinduct
apply simp
by fastforce
lemma once_none_always_none: "alw (state_eq None) (make_full_observation e None r p t)"
using once_none_always_none_aux by blast
lemma once_none_nxt_always_none: "alw (nxt (state_eq None)) (make_full_observation e None r p t)"
using once_none_always_none
by (simp add: alw_iff_sdrop del: sdrop.simps)
lemma snth_sconst: "(\<forall>i. s !! i = h) = (s = sconst h)"