Theory EFSM_LTL
section‹LTL for EFSMs›
text‹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.›
theory EFSM_LTL
imports "Extended_Finite_State_Machines.EFSM" "HOL-Library.Linear_Temporal_Logic_on_Streams"
begin
text_raw‹\snip{statedef}{1}{2}{%›
record state =
statename :: "nat option"
datastate :: registers
action :: action
"output" :: outputs
text_raw‹}%endsnip›
text_raw‹\snip{whitebox}{1}{2}{%›
type_synonym whitebox_trace = "state stream"
text_raw‹}%endsnip›
type_synonym property = "whitebox_trace ⇒ bool"
abbreviation label :: "state ⇒ String.literal" where
"label s ≡ fst (action s)"
abbreviation inputs :: "state ⇒ value list" where
"inputs s ≡ snd (action s)"
text_raw‹\snip{ltlStep}{1}{2}{%›
fun ltl_step :: "transition_matrix ⇒ cfstate option ⇒ registers ⇒ action ⇒ (nat option × outputs × 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 (λx. x |∈| possibilities) in
(Some s', (evaluate_outputs t i r), (evaluate_updates t i r))
)"
text_raw‹}%endsnip›
lemma ltl_step_singleton:
"∃t. possible_steps e n r (fst v) (snd v) = {|(aa, t)|} ∧ evaluate_outputs t (snd v) r = b ∧ evaluate_updates t (snd v) r = c⟹
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 = {||} ⟹ 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) = {||} ⟹ 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 (λx. x |∈| 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: "∀(s', t) |∈| (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 ∨ xa |∈| S'")
apply simp
apply (insert assms(2))
apply (simp add: Ball_def)
by (metis (mono_tags, lifting) fst_conv prod.case_eq_if snd_conv someI_ex)
done
text‹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.›
text_raw‹\snip{makeFullObservation}{1}{2}{%›
primcorec make_full_observation :: "transition_matrix ⇒ cfstate option ⇒ registers ⇒ outputs ⇒ action stream ⇒ whitebox_trace" where
"make_full_observation e s d p i = (
let (s', o', d') = ltl_step e s d (shd i) in
⦇statename = s, datastate = d, action=(shd i), output = p⦈##(make_full_observation e s' d' o' (stl i))
)"
text_raw‹}%endsnip›
text_raw‹\snip{watch}{1}{2}{%›
abbreviation watch :: "transition_matrix ⇒ action stream ⇒ whitebox_trace" where
"watch e i ≡ (make_full_observation e (Some 0) <> [] i)"
text_raw‹}%endsnip›
subsection‹Expressing Properties›
text‹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.›
subsubsection‹State Equality›
text‹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.›
abbreviation state_eq :: "cfstate option ⇒ whitebox_trace ⇒ bool" where
"state_eq v s ≡ statename (shd s) = v"
lemma state_eq_holds: "state_eq s = holds (λx. statename x = s)"
apply (rule ext)
by (simp add: holds_def)
lemma state_eq_None_not_Some: "state_eq None s ⟹ ¬ state_eq (Some n) s"
by simp
subsubsection‹Label Equality›
text‹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.›
abbreviation "label_eq v s ≡ fst (action (shd s)) = (String.implode v)"
lemma watch_label: "label_eq l (watch e t) = (fst (shd t) = String.implode l)"
by simp
subsubsection‹Input Equality›
text‹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.›
abbreviation "input_eq v s ≡ inputs (shd s) = v"
subsubsection‹Action Equality›
text‹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.›
abbreviation "action_eq e ≡ label_eq (fst e) aand input_eq (snd e)"
subsubsection‹Output Equality›
text‹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.›
abbreviation "output_eq v s ≡ output (shd s) = v"
text_raw‹\snip{ltlVName}{1}{2}{%›