# Theory Transition

```chapter‹Models›
text‹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.›

section‹Transitions›
text‹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.›

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 × vname aexp"

text_raw‹\snip{transitiontype}{1}{2}{%›
record transition =
Label :: String.literal
Arity :: nat
Guards :: "guard list"
Outputs :: "output_function list"
text_raw‹}%endsnip›

definition same_structure :: "transition ⇒ transition ⇒ bool" where
"same_structure t1 t2 = (
Label t1 = Label t2 ∧
Arity t1 = Arity t2 ∧
length (Outputs t1) = length (Outputs t2)
)"

definition enumerate_inputs :: "transition ⇒ nat set" where
"enumerate_inputs t = (⋃ (set (map enumerate_gexp_inputs (Guards t)))) ∪
(⋃ (set (map enumerate_aexp_inputs (Outputs t)))) ∪
(⋃ (set (map (λ(_, u). enumerate_aexp_inputs u) (Updates t))))"

definition max_input :: "transition ⇒ nat option" where
"max_input t = (if enumerate_inputs t = {} then None else Some (Max (enumerate_inputs t)))"

definition total_max_input :: "transition ⇒ nat" where
"total_max_input t = (case max_input t of None ⇒ 0 | Some a ⇒ a)"

definition enumerate_regs :: "transition ⇒ nat set" where
"enumerate_regs t = (⋃ (set (map GExp.enumerate_regs (Guards t)))) ∪
(⋃ (set (map AExp.enumerate_regs (Outputs t)))) ∪
(⋃ (set (map (λ(_, u). AExp.enumerate_regs u) (Updates t)))) ∪
(⋃ (set (map (λ(r, _). AExp.enumerate_regs (V (R r))) (Updates t))))"

definition max_reg :: "transition ⇒ nat option" where
"max_reg t = (if enumerate_regs t = {} then None else Some (Max (enumerate_regs t)))"

definition total_max_reg :: "transition ⇒ nat" where
"total_max_reg t = (case max_reg t of None ⇒ 0 | Some a ⇒ a)"

definition enumerate_ints :: "transition ⇒ int set" where
"enumerate_ints t = (⋃ (set (map enumerate_gexp_ints (Guards t)))) ∪
(⋃ (set (map enumerate_aexp_ints (Outputs t)))) ∪
(⋃ (set (map (λ(_, u). enumerate_aexp_ints u) (Updates t)))) ∪
(⋃ (set (map (λ(r, _). enumerate_aexp_ints (V (R r))) (Updates t))))"

definition valid_transition :: "transition ⇒ bool" where
"valid_transition t = (∀i ∈ enumerate_inputs t. i < Arity t)"

definition can_take :: "nat ⇒ vname gexp list ⇒ inputs ⇒ registers ⇒ bool" where
"can_take a g i r = (length i = a ∧ apply_guards g (join_ir i r))"

lemma can_take_empty [simp]: "length i = a ⟹ can_take a [] i c"

lemma can_take_subset_append:
assumes "set (Guards t) ⊆ set (Guards t')"
shows "can_take a (Guards t @ Guards t') i c = can_take a (Guards t') i c"
using assms

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 = [] ⟹ ∃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 ⟹
Arity t = Arity t' ⟹
set (Guards t') ⊆ set (Guards t) ⟹
can_take_transition t i r ⟹
can_take_transition t' i r"
by (simp add: can_take_transition_def can_take_def apply_guards_subset)

lemma valid_list_can_take:
"∀g ∈ set (Guards t). valid g ⟹ ∃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:
"∃g ∈ set (Guards t). gval g (join_ir i r) ≠ true ⟹
¬ 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 ⇒ 'a datastate ⇒ value option list" where
"apply_outputs p s = map (λp. aval p s) p"

abbreviation "evaluate_outputs t i r ≡ apply_outputs (Outputs t) (join_ir i r)"

lemma apply_outputs_nth:
"i < length p ⟹ apply_outputs p s ! i = aval (p ! i) s"

lemmas apply_outputs = datastate apply_outputs_def value_plus_def value_minus_def value_times_def

lemma apply_outputs_empty [simp]: "apply_outputs [] s = []"

lemma apply_outputs_preserves_length: "length (apply_outputs p s) = length p"

lemma apply_outputs_literal: assumes "P ! r = L v"
and "r < length P"
shows "apply_outputs P s ! r = Some v"

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 ≠ 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 ⇒ vname datastate ⇒ registers ⇒ registers" where
"apply_updates u old = fold (λh r. r(fst h \$:= aval (snd h) old)) u"

lemma apply_updates_cons: "ra ≠ r ⟹
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
next
case (snoc u us)
then show ?case
apply (cases u)
by (case_tac "ra = aa", auto)
qed

lemma update_twice:
"apply_updates [(r, a), (r, b)] s regs = regs (r \$:= aval b s)"

lemma r_not_updated_stays_the_same:
"r ∉ fst ` set U ⟹ apply_updates U c d \$ r = d \$ r"
by (induct U rule: rev_induct, auto)

definition rename_regs :: "(nat ⇒ nat) ⇒ transition ⇒ transition" where
"rename_regs f t = t⦇
Guards  := map (GExp.rename_regs f) (Guards t),
Outputs := map (AExp.rename_regs f) (Outputs t),
Updates := map (λ(r, u). (f r, AExp.rename_regs f u)) (Updates t)
⦈"

definition eq_upto_rename_strong :: "transition ⇒ transition ⇒ bool" where
"eq_upto_rename_strong t1 t2 = (∃f. bij f ∧ rename_regs f t1 = t2)"

inductive eq_upto_rename :: "transition ⇒ transition ⇒ bool" where
"Label t1 = Label t2 ⟹
Arity t2 = Arity t2 ⟹
apply_guards (map (GExp.rename_regs f) (Guards t1)) = apply_guards (Guards t2) ⟹

apply_outputs (map (AExp.rename_regs f) (Outputs t1)) = apply_outputs (Outputs t2) ⟹