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"
  Updates :: "update_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"
  by (simp add: can_take_def)

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
  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 = [] ⟹ ∃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"
  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 ≠ 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"

abbreviation "evaluate_updates t i r ≡ apply_updates (Updates t) (join_ir i r) r"

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
    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 ∉ fst ` set U ⟹ apply_updates U c d $ r = d $ r"
  using apply_updates_def
  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) ⟹

   apply_updates (map (λ(r, u). (f r, AExp.rename_regs f u)) (Updates t1)) = apply_updates (Updates t2) ⟹

   eq_upto_rename t1 t2"

end