282 lines
13 KiB
Plaintext
282 lines
13 KiB
Plaintext
section\<open>LTL for EFSMs\<close>
|
|
text\<open>This theory builds off the \texttt{Linear\_Temporal\_Logic\_on\_Streams} theory from the HOL
|
|
library and defines functions to ease the expression of LTL properties over EFSMs. Since the LTL
|
|
operators effectively act over traces of models we must find a way to express models as streams.\<close>
|
|
|
|
theory EFSM_LTL
|
|
imports "Extended_Finite_State_Machines-devel.EFSM" "HOL-Library.Linear_Temporal_Logic_on_Streams"
|
|
begin
|
|
|
|
text_raw\<open>\snip{statedef}{1}{2}{%\<close>
|
|
record state =
|
|
statename :: "nat option"
|
|
datastate :: registers
|
|
action :: action
|
|
"output" :: outputs
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
text_raw\<open>\snip{whitebox}{1}{2}{%\<close>
|
|
type_synonym whitebox_trace = "state stream"
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
type_synonym property = "whitebox_trace \<Rightarrow> bool"
|
|
|
|
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
|
|
(Some s', (apply_outputs (Outputs t') (join_ir (snd t) r)), (apply_updates (Updates t') (join_ir (snd t) r) r))
|
|
)"
|
|
by (case_tac t, simp add: Let_def)
|
|
|
|
lemma ltl_step_some:
|
|
assumes "possible_steps e s r l i = {|(s', t)|}"
|
|
and "evaluate_outputs t i r = p"
|
|
and "evaluate_updates t i r = r'"
|
|
shows "ltl_step e (Some s) r (l, i) = (Some s', p, r')"
|
|
by (simp add: assms)
|
|
|
|
lemma ltl_step_cases:
|
|
assumes invalid: "P (None, [], r)"
|
|
and valid: "\<forall>(s', t) |\<in>| (possible_steps e s r l i). P (Some s', (evaluate_outputs t i r), (evaluate_updates t i r))"
|
|
shows "P (ltl_step e (Some s) r (l, i))"
|
|
apply simp
|
|
apply (case_tac "possible_steps e s r l i")
|
|
apply (simp add: invalid)
|
|
apply simp
|
|
subgoal for x S'
|
|
apply (case_tac "SOME xa. xa = x \<or> xa |\<in>| S'")
|
|
apply simp
|
|
apply (insert assms(2))
|
|
apply (simp add: fBall_def Ball_def fmember_def)
|
|
by (metis (mono_tags, lifting) fst_conv prod.case_eq_if snd_conv someI_ex)
|
|
done
|
|
|
|
text\<open>The \texttt{make\_full\_observation} function behaves similarly to \texttt{observe\_execution}
|
|
from the \texttt{EFSM} theory. The main difference in behaviour is what is recorded. While the
|
|
observe execution function simply observes an execution of the EFSM to produce the corresponding
|
|
output for each action, the intention here is to record every detail of execution, including the
|
|
values of internal variables.
|
|
|
|
Thinking of each action as a step forward in time, there are five components which characterise
|
|
a given point in the execution of an EFSM. At each point, the model has a current control state and
|
|
data state. Each action has a label and some input parameters, and its execution may produce
|
|
some observableoutput. It is therefore sufficient to provide a stream of 5-tuples containing the
|
|
current control state, data state, the label and inputs of the action, and computed output. The
|
|
make full observation function can then be defined as in Figure 9.1, with an additional
|
|
function watch defined on top of this which starts the make full observation off in the
|
|
initial control state with the empty data state.
|
|
|
|
Careful inspection of the definition reveals another way that \texttt{make\_full\_observation}
|
|
differs from \texttt{observe\_execution}. Rather than taking a cfstate, it takes a cfstate option.
|
|
The reason for this is that we need to make our EFSM models complete. That is, we need them to be
|
|
able to respond to every action from every state like a DFA. If a model does not recognise a given
|
|
action in a given state, we cannot simply stop processing because we are working with necessarily
|
|
infinite traces. Since these traces are generated by observing action sequences, the make full
|
|
observation function must keep processing whether there is a viable transition or not.
|
|
|
|
To support this, the make full observation adds an implicit ``sink state'' to every EFSM it
|
|
processes by lifting control flow state indices from \texttt{nat} to \texttt{nat option} such that
|
|
state $n$ is seen as state \texttt{Some} $n$. The control flow state \texttt{None} represents a sink
|
|
state. If a model is unable to recognise a particular action from its current state, it moves into
|
|
the \texttt{None} state. From here, the behaviour is constant for the rest of the time --- the
|
|
control flow state remains None; the data state does not change, and no output is produced.\<close>
|
|
|
|
text_raw\<open>\snip{makeFullObservation}{1}{2}{%\<close>
|
|
primcorec make_full_observation :: "transition_matrix \<Rightarrow> cfstate option \<Rightarrow> registers \<Rightarrow> outputs \<Rightarrow> action stream \<Rightarrow> whitebox_trace" where
|
|
"make_full_observation e s d p i = (
|
|
let (s', o', d') = ltl_step e s d (shd i) in
|
|
\<lparr>statename = s, datastate = d, action=(shd i), output = p\<rparr>##(make_full_observation e s' d' o' (stl i))
|
|
)"
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
text_raw\<open>\snip{watch}{1}{2}{%\<close>
|
|
abbreviation watch :: "transition_matrix \<Rightarrow> action stream \<Rightarrow> whitebox_trace" where
|
|
"watch e i \<equiv> (make_full_observation e (Some 0) <> [] i)"
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
subsection\<open>Expressing Properties\<close>
|
|
text\<open>In order to simplify the expression and understanding of properties, this theory defines a
|
|
number of named functions which can be used to express certain properties of EFSMs.\<close>
|
|
|
|
subsubsection\<open>State Equality\<close>
|
|
text\<open>The \textsc{state\_eq} takes a cfstate option representing a control flow state index and
|
|
returns true if this is the control flow state at the head of the full observation.\<close>
|
|
|
|
abbreviation state_eq :: "cfstate option \<Rightarrow> whitebox_trace \<Rightarrow> bool" where
|
|
"state_eq v s \<equiv> statename (shd s) = v"
|
|
|
|
lemma state_eq_holds: "state_eq s = holds (\<lambda>x. statename x = s)"
|
|
apply (rule ext)
|
|
by (simp add: holds_def)
|
|
|
|
lemma state_eq_None_not_Some: "state_eq None s \<Longrightarrow> \<not> state_eq (Some n) s"
|
|
by simp
|
|
|
|
subsubsection\<open>Label Equality\<close>
|
|
text\<open>The \textsc{label\_eq} function takes a string and returns true if this is equal to the label
|
|
at the head of the full observation.\<close>
|
|
|
|
abbreviation "label_eq v s \<equiv> fst (action (shd s)) = (String.implode v)"
|
|
|
|
lemma watch_label: "label_eq l (watch e t) = (fst (shd t) = String.implode l)"
|
|
by (simp add: )
|
|
|
|
subsubsection\<open>Input Equality\<close>
|
|
text\<open>The \textsc{input\_eq} function takes a value list and returns true if this is equal to the
|
|
input at the head of the full observation.\<close>
|
|
|
|
abbreviation "input_eq v s \<equiv> inputs (shd s) = v"
|
|
|
|
subsubsection\<open>Action Equality\<close>
|
|
text\<open>The \textsc{action\_eq} function takes a (label, value list) pair and returns true if this is
|
|
equal to the action at the head of the full observation. This effectively combines
|
|
\texttt{label\_eq} and \texttt{input\_eq} into one function.\<close>
|
|
|
|
abbreviation "action_eq e \<equiv> label_eq (fst e) aand input_eq (snd e)"
|
|
|
|
subsubsection\<open>Output Equality\<close>
|
|
text\<open>The \textsc{output\_eq} function takes a takes a value option list and returns true if this is
|
|
equal to the output at the head of the full observation.\<close>
|
|
|
|
abbreviation "output_eq v s \<equiv> output (shd s) = v"
|
|
|
|
text_raw\<open>\snip{ltlVName}{1}{2}{%\<close>
|
|
datatype ltl_vname = Ip nat | Op nat | Rg nat
|
|
text_raw\<open>}%endsnip\<close>
|
|
|
|
subsubsection\<open>Checking Arbitrary Expressions\<close>
|
|
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)"
|
|
by (auto simp add: sconst_alt sset_range)
|
|
|
|
lemma alw_sconst: "(alw (\<lambda>xs. shd xs = h) t) = (t = sconst h)"
|
|
by (simp add: snth_sconst[symmetric] alw_iff_sdrop)
|
|
|
|
lemma smap_statename_None: "smap statename (make_full_observation e None r p i) = sconst None"
|
|
by (meson EFSM_LTL.alw_sconst alw_state_eq_smap once_none_always_none)
|
|
|
|
lemma alw_not_some: "alw (\<lambda>xs. statename (shd xs) \<noteq> Some s) (make_full_observation e None r p t)"
|
|
by (metis (mono_tags, lifting) alw_mono once_none_always_none option.distinct(1) )
|
|
|
|
lemma state_none: "((state_eq None) impl nxt (state_eq None)) (make_full_observation e s r p t)"
|
|
by (simp add: )
|
|
|
|
lemma state_none_2:
|
|
"(state_eq None) (make_full_observation e s r p t) \<Longrightarrow>
|
|
(state_eq None) (make_full_observation e s r p (stl t))"
|
|
by (simp add: )
|
|
|
|
lemma no_output_none_aux:
|
|
assumes "\<exists> p r i. j = (make_full_observation e None r []) i"
|
|
shows "alw (output_eq []) j"
|
|
using assms apply coinduct
|
|
apply simp
|
|
by fastforce
|
|
|
|
lemma no_output_none: "nxt (alw (output_eq [])) (make_full_observation e None r p t)"
|
|
using no_output_none_aux by auto
|
|
|
|
lemma nxt_alw: "nxt (alw P) s \<Longrightarrow> alw (nxt P) s"
|
|
by (simp add: alw_iff_sdrop)
|
|
|
|
lemma no_output_none_nxt: "alw (nxt (output_eq [])) (make_full_observation e None r p t)"
|
|
using nxt_alw no_output_none by blast
|
|
|
|
lemma no_output_none_if_empty: "alw (output_eq []) (make_full_observation e None r [] t)"
|
|
by (metis (mono_tags, lifting) alw_nxt make_full_observation.simps(1) no_output_none state.select_convs(4))
|
|
|
|
lemma no_updates_none_aux:
|
|
assumes "\<exists> p i. j = (make_full_observation e None r p) i"
|
|
shows "alw (\<lambda>x. datastate (shd x) = r) j"
|
|
using assms apply coinduct
|
|
by fastforce
|
|
|
|
lemma no_updates_none: "alw (\<lambda>x. datastate (shd x) = r) (make_full_observation e None r p t)"
|
|
using no_updates_none_aux by blast
|
|
|
|
lemma action_components: "(label_eq l aand input_eq i) s = (action (shd s) = (String.implode l, i))"
|
|
by (metis fst_conv prod.collapse snd_conv)
|
|
|
|
end
|