# 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"
by auto

lemma guard_match_length:
"length (Guards t1) ≠ 1 ∨ length (Guards t2) ≠ 1 ⟹ ¬ guardMatch t1 t2"
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)"
by auto

lemma guard_match_symmetry: "(guardMatch t1 t2) = (guardMatch t2 t1)"
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
```