Theory Increment_Reset

section‹Increment and Reset›
text‹The ``increment and reset'' heuristic proposed in \<^cite>‹"foster2019"› is a naive way of
introducing an incrementing register into a model. This this theory implements that heuristic.›

theory Increment_Reset
  imports "../Inference"
begin

definition initialiseReg :: "transition ⇒ nat ⇒ transition" where
  "initialiseReg t newReg = ⦇Label = Label t, Arity = Arity t, Guards = Guards t, Outputs = Outputs t, Updates = ((newReg, L (Num 0))#Updates t)⦈"

definition "guardMatch t1 t2  = (∃n n'. Guards t1 = [gexp.Eq (V (vname.I 0)) (L (Num n))] ∧ Guards t2 = [gexp.Eq (V (vname.I 0)) (L (Num n'))])"
definition "outputMatch t1 t2 = (∃m m'. Outputs t1 = [L (Num m)] ∧ Outputs t2 = [L (Num m')])"

lemma guard_match_commute: "guardMatch t1 t2 = guardMatch t2 t1"
  apply (simp add: guardMatch_def)
  by auto

lemma guard_match_length:
  "length (Guards t1) ≠ 1 ∨ length (Guards t2) ≠ 1 ⟹ ¬ guardMatch t1 t2"
  apply (simp add: guardMatch_def)
  by auto

fun insert_increment :: update_modifier where
  "insert_increment t1ID t2ID s new _ old check = (let
     t1 = get_by_ids new t1ID;
     t2 = get_by_ids new t2ID in
     if guardMatch t1 t2 ∧ outputMatch t1 t2 then let
          r = case max_reg new of None ⇒ 1 | Some r ⇒ r+ 1;
          newReg = R r;
          newT1 = ⦇Label = Label t1, Arity = Arity t1, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t1)⦈;
          newT2 = ⦇Label = Label t2, Arity = Arity t2, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t2)⦈;
          to_initialise = ffilter (λ(uid, (from, to), t). (to = dest t1ID new ∨ to = dest t2ID new) ∧ t ≠ t1 ∧ t ≠ t2) new;
          initialisedTrans = fimage (λ(uid, (from, to), t). (uid, initialiseReg t r)) to_initialise;
          initialised = replace_transitions new (sorted_list_of_fset initialisedTrans);
          rep = replace_transitions new [(t1ID, newT1), (t2ID, newT2)]
     in
          if check (tm rep) then Some rep else None
     else
       None
     )"

definition struct_replace_all :: "iEFSM ⇒ transition ⇒ transition ⇒ iEFSM" where
  "struct_replace_all e old new = (let
    to_replace = ffilter (λ(uid, (from, dest), t). same_structure t old) e;
    replacements = fimage (λ(uid, (from, to), t). (uid, new)) to_replace
    in
    replace_transitions e (sorted_list_of_fset replacements))"

lemma output_match_symmetry: "(outputMatch t1 t2) = (outputMatch t2 t1)"
  apply (simp add: outputMatch_def)
  by auto

lemma guard_match_symmetry: "(guardMatch t1 t2) = (guardMatch t2 t1)"
  apply (simp add: guardMatch_def)
  by auto

fun insert_increment_2 :: update_modifier where
  "insert_increment_2 t1ID t2ID s new _ old check = (let
     t1 = get_by_ids new t1ID;
     t2 = get_by_ids new t2ID in
     if guardMatch t1 t2 ∧ outputMatch t1 t2 then let
          r = case max_reg new of None ⇒ 1 | Some r ⇒ r + 1;
          newReg = R r;
          newT1 = ⦇Label = Label t1, Arity = Arity t1, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t1)⦈;
          newT2 = ⦇Label = Label t2, Arity = Arity t2, Guards = [], Outputs = [Plus (V newReg) (V (vname.I 0))], Updates=((r, Plus (V newReg) (V (vname.I 0)))#Updates t2)⦈;
          to_initialise = ffilter (λ(uid, (from, to), t). (to = dest t1ID new ∨ to = dest t2ID new) ∧ t ≠ t1 ∧ t ≠ t2) new;
          initialisedTrans = fimage (λ(uid, (from, to), t). (uid, initialiseReg t r)) to_initialise;
          initialised = replace_transitions new (sorted_list_of_fset initialisedTrans);
          rep = struct_replace_all (struct_replace_all initialised t2 newT2) t1 newT1
      in
          if check (tm rep) then Some rep else None
     else
       None
     )"

fun guardMatch_alt_2 :: "vname gexp list ⇒ bool" where
  "guardMatch_alt_2 [(gexp.Eq (V (vname.I i)) (L (Num n)))] = (i = 1)" |
  "guardMatch_alt_2 _ = False"

fun outputMatch_alt_2 :: "vname aexp list ⇒ bool" where
  "outputMatch_alt_2 [(L (Num n))] = True" |
  "outputMatch_alt_2 _ = False"

end