Theory Transition

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.›

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

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"

record transition =
  Label :: String.literal
  Arity :: nat
  Guards :: "guard list"
  Outputs :: "output_function list"
  Updates :: "update_function list"

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)
  case (snoc u us)
  then show ?case
    apply (cases u)
    apply (simp add: apply_updates_def)
    by (case_tac "ra = aa", auto)

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"