Theory PTA_Generalisation

section‹PTA Generalisation›
text‹The problem with the simplistic heuristics of \<^cite>‹"foster2019"› is that the performance of the
Inference technique is almost entirely dependent on the quality and applicability of the heuristics
provided to it. Producing high quality heuristics often requires some inside knowledge of the system
under inference. If the user has this knowledge already, they are unlikely to require automated
inference. Ideally, we would like something more generally applicable. This theory presents a more
abstract \emph{metaheuristic} which can be implemented with genetic programming.›

theory PTA_Generalisation
  imports "../Inference" Same_Register Group_By
begin

hide_const I

datatype value_type = N | S

instantiation value_type :: linorder begin
fun less_value_type :: "value_type ⇒ value_type ⇒ bool" where
  "less_value_type N S = True" |
  "less_value_type _ _ = False"

definition less_eq_value_type :: "value_type ⇒ value_type ⇒ bool" where
 "less_eq_value_type v1 v2 ≡ (v1 < v2 ∨ v1 = v2)"

instance
  apply standard
  using less_eq_value_type_def less_value_type.elims(2) apply blast
     apply (simp add: less_eq_value_type_def)
    apply (metis less_eq_value_type_def value_type.exhaust)
  using less_eq_value_type_def less_value_type.elims(2) apply blast
  by (metis less_eq_value_type_def less_value_type.elims(3) value_type.simps(2))

end

― ‹This is a very hacky way of making sure that things with differently typed outputs don't get
    lumped together.›
fun typeSig :: "output_function ⇒ value_type" where
  "typeSig (L (value.Str _)) = S" |
  "typeSig _ = N"

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

lemma same_structure_equiv:
  "Outputs t1 = [L (Num m)] ⟹ Outputs t2 = [L (Num n)] ⟹
   same_structure t1 t2 = Transition.same_structure t1 t2"
  by (simp add: same_structure_def Transition.same_structure_def)

type_synonym transition_group = "(tids × transition) list"

fun observe_all :: "iEFSM ⇒  cfstate ⇒ registers ⇒ trace ⇒ transition_group" where
  "observe_all _ _ _ [] = []" |
  "observe_all e s r ((l, i, _)#es)  =
    (case random_member (i_possible_steps e s r l i)  of
      (Some (ids, s', t)) ⇒ (((ids, t)#(observe_all e s' (evaluate_updates t i r) es))) |
      _ ⇒ []
    )"

definition transition_groups_exec :: "iEFSM ⇒ trace ⇒ (nat × tids × transition) list list" where
  "transition_groups_exec e t = group_by (λ(_, _, t1) (_, _, t2). same_structure t1 t2) (enumerate 0 (observe_all e 0 <> t))"

type_synonym struct = "(label × arity × value_type list)"

text‹We need to take the list of transition groups and tag them with the last transition that was
taken which had a different structure.›
fun tag :: "struct option ⇒ (nat × tids × transition) list list ⇒ (struct option × struct × (nat × tids × transition) list) list" where
  "tag _ [] = []" |
  "tag t (g#gs) = (
    let
      (_, _, head) = hd g;
      struct = (Label head, Arity head, map typeSig (Outputs head))
    in
    (t, struct, g)#(tag (Some struct) gs)
  )"

text‹We need to group transitions not just by their structure but also by their history - i.e. the
last transition which was taken which had a different structure. We need to order these groups by
their relative positions within the traces such that output and update functions can be inferred in
the correct order.›
definition transition_groups :: "iEFSM ⇒ log ⇒ transition_group list" where
  "transition_groups e l = (
    let
      trace_groups = map (transition_groups_exec e) l;
      tagged = map (tag None) trace_groups;
      flat =  sort (fold (@) tagged []);
      group_fun = fold (λ(tag, s, gp) f. f((tag, s) $:= gp@(f$(tag, s)))) flat (K$ []);
      grouped = map (λx. group_fun $ x) (finfun_to_list group_fun);
      inx_groups = map (λgp. (Min (set (map fst gp)), map snd gp)) grouped
    in
      map snd (sort inx_groups)
  )"

text‹For a given trace group, log, and EFSM, we want to build the training set for that group. That
is, the set of inputs, registers, and expected outputs from those transitions. To do this, we must
walk the traces in the EFSM to obtain the register values.›
fun trace_group_training_set :: "transition_group ⇒ iEFSM ⇒ cfstate ⇒ registers ⇒ trace ⇒ (inputs × registers × value list) list ⇒ (inputs × registers × value list) list" where
  "trace_group_training_set _ _ _ _ [] train = train" |
  "trace_group_training_set gp e s r ((l, i, p)#t) train = (
    let
      (id, s', transition) = fthe_elem (i_possible_steps e s r l i)
    in
    if ∃(id', _) ∈ set gp. id' = id then
      trace_group_training_set gp e s' (evaluate_updates transition i r) t ((i, r, p)#train)
    else
      trace_group_training_set gp e s' (evaluate_updates transition i r) t train
  )"

definition make_training_set :: "iEFSM ⇒ log ⇒ transition_group ⇒ (inputs × registers × value list) list" where
  "make_training_set e l gp = fold (λh a. trace_group_training_set gp e 0 <> h a) l []"

primrec replace_groups :: "transition_group list ⇒ iEFSM ⇒ iEFSM" where
  "replace_groups [] e = e" |
  "replace_groups (h#t) e = replace_groups t (fold (λ(id, t) acc. replace_transition acc id t) h e)"

lemma replace_groups_fold [code]:
  "replace_groups xs e = fold (λh acc'. (fold (λ(id, t) acc. replace_transition acc id t) h acc')) xs e"
  by (induct xs arbitrary: e,  auto)

definition insert_updates :: "transition ⇒ update_function list ⇒ transition" where
  "insert_updates t u = (
    let
      ― ‹Want to filter out null updates of the form rn := rn. It doesn't affect anything but it  ›
      ― ‹does make things look cleaner                                                            ›
      necessary_updates = filter (λ(r, u). u ≠ V (R r)) u
    in
    t⦇Updates := (filter (λ(r, _). r ∉ set (map fst u)) (Updates t))@necessary_updates⦈
  )"

fun add_groupwise_updates_trace :: "trace  ⇒ (tids × update_function list) list ⇒ iEFSM ⇒ cfstate ⇒ registers ⇒ iEFSM" where
  "add_groupwise_updates_trace [] _ e _ _ = e" |
  "add_groupwise_updates_trace ((l, i, _)#trace) funs e s r = (
    let
      (id, s', t) = fthe_elem (i_possible_steps e s r l i);
      updated = evaluate_updates t i r;
      newUpdates = List.maps snd (filter (λ(tids, _). set id ⊆ set tids) funs);
      t' = insert_updates t newUpdates;
      updated' = apply_updates (Updates t') (join_ir i r) r;
      necessaryUpdates = filter (λ(r, _). updated $ r ≠ updated' $ r) newUpdates;
      t'' = insert_updates t necessaryUpdates;
      e' = replace_transition e id t''
    in
    add_groupwise_updates_trace trace funs e' s' updated'
  )"

primrec add_groupwise_updates :: "log  ⇒ (tids × update_function list) list ⇒ iEFSM ⇒ iEFSM" where
  "add_groupwise_updates [] _ e = e" |
  "add_groupwise_updates (h#t) funs e = add_groupwise_updates t funs (add_groupwise_updates_trace h funs e 0 <>)"

lemma fold_add_groupwise_updates [code]:
  "add_groupwise_updates log funs e = fold (λtrace acc. add_groupwise_updates_trace trace funs acc 0 <>) log e"
  by (induct log arbitrary: e, auto)

― ‹This will be replaced to calls to Z3 in the executable›
definition get_regs :: "(vname ⇒f String.literal) ⇒ inputs ⇒ vname aexp ⇒ value ⇒ registers" where
  "get_regs types inputs expression output = Eps (λr. aval expression (join_ir inputs r) = Some output)"

declare get_regs_def [code del]
code_printing constant get_regs ⇀ (Scala) "Dirties.getRegs"

type_synonym action_info = "(cfstate × registers × registers × inputs × tids × transition)"
type_synonym run_info = "action_info list"
type_synonym targeted_run_info = "(registers × action_info) list"

fun everything_walk :: "output_function ⇒ nat ⇒ (vname ⇒f String.literal) ⇒ trace ⇒ iEFSM ⇒ cfstate ⇒ registers ⇒ transition_group ⇒ run_info" where
  "everything_walk _ _ _ [] _ _ _ _ = []" |
  "everything_walk f fi types ((label, inputs, outputs)#t) oPTA s regs gp  = (
    let (tid, s', ta) = fthe_elem (i_possible_steps oPTA s regs label inputs) in
     ― ‹Possible steps with a transition we need to modify›
    if ∃(tid', _) ∈ set gp. tid = tid' then
      (s, regs, get_regs types inputs f (outputs!fi), inputs, tid, ta)#(everything_walk f fi types t oPTA s' (evaluate_updates ta inputs regs) gp)
    else
      let empty = <> in
      (s, regs, empty, inputs, tid, ta)#(everything_walk f fi types t oPTA s' (evaluate_updates ta inputs regs) gp)
  )"

definition everything_walk_log :: "output_function ⇒ nat ⇒ (vname ⇒f String.literal) ⇒ log ⇒ iEFSM ⇒ transition_group ⇒ run_info list" where
  "everything_walk_log f fi types log e gp = map (λt. everything_walk f fi types t e 0 <> gp) log"

fun target :: "registers ⇒ run_info ⇒ targeted_run_info" where
  "target _ [] = []" |
  "target tRegs ((s, oldregs, regs, inputs, tid, ta)#t) = (
    let newTarget = if finfun_to_list regs = [] then tRegs else regs in
    (tRegs, s, oldregs, regs, inputs, tid, ta)#target newTarget t
  )"

fun target_tail :: "registers ⇒ run_info ⇒ targeted_run_info ⇒ targeted_run_info" where
  "target_tail _ [] tt = rev tt" |
  "target_tail tRegs ((s, oldregs, regs, inputs, tid, ta)#t) tt = (
    let newTarget = if finfun_to_list regs = [] then tRegs else regs in
    target_tail newTarget t ((tRegs, s, oldregs, regs, inputs, tid, ta)#tt)
  )"

lemma target_tail: "(rev bs)@(target tRegs ts) = target_tail tRegs ts bs"
proof(induct ts arbitrary: bs tRegs)
  case (Cons a ts)
  then show ?case
    apply (cases a)
    apply simp
    apply standard
    by (metis (no_types, lifting) append_eq_append_conv2 rev.simps(2) rev_append rev_swap self_append_conv2)+
qed simp

definition "target_fold tRegs ts b = fst (fold (λ(s, oldregs, regs, inputs, tid, ta) (acc, tRegs).
let newTarget = if finfun_to_list regs = [] then tRegs else regs in
    (acc@[(tRegs, s, oldregs, regs, inputs, tid, ta)], newTarget)
) ts (rev b, tRegs))"

lemma target_tail_fold: "target_tail tRegs ts b = target_fold tRegs ts b"
proof(induct ts arbitrary: tRegs b)
  case Nil
  then show ?case
    by (simp add: target_fold_def)
next
  case (Cons a ts)
  then show ?case
    apply (cases a)
    by (simp add: target_fold_def)
qed

lemma target_fold [code]: "target tRegs ts = target_fold tRegs ts []"
  by (metis append_self_conv2 rev.simps(1) target_tail_fold target_tail)

― ‹This will be replaced by symbolic regression in the executable›
definition get_update :: "label ⇒ nat ⇒ value list ⇒ (inputs × registers × registers) list ⇒ vname aexp option" where
  "get_update _ reg values train = (let
    possible_funs = {a. ∀(i, r, r') ∈ set train. aval a (join_ir i r) = r' $ reg}
    in
    if possible_funs = {} then None else Some (Eps (λx. x ∈ possible_funs))
  )"

declare get_update_def [code del]
code_printing constant get_update ⇀ (Scala) "Dirties.getUpdate"

definition get_updates_opt :: "label ⇒ value list ⇒ (inputs × registers × registers) list ⇒ (nat × vname aexp option) list" where
  "get_updates_opt l values train = (let
    updated_regs = fold List.union (map (finfun_to_list ∘ snd ∘ snd) train) [] in
    map (λr.
      let targetValues = remdups (map (λ(_, _, regs). regs $ r) train) in
      if  (∀(_, anteriorRegs, posteriorRegs) ∈ set train. anteriorRegs $ r = posteriorRegs $ r) then
        (r, Some (V (R r)))
      else if length targetValues = 1 ∧ (∀(inputs, anteriorRegs, _) ∈ set train. finfun_to_list anteriorRegs = []) then
        case hd targetValues of Some v ⇒
        (r, Some (L v))
      else
        (r, get_update l r values train)
    ) updated_regs
  )"

definition finfun_add :: "(('a::linorder) ⇒f 'b) ⇒ ('a ⇒f 'b) ⇒ ('a ⇒f 'b)" where
  "finfun_add a b = fold (λk f. f(k $:= b $ k)) (finfun_to_list b) a"

definition group_update :: "value list ⇒ targeted_run_info ⇒ (tids × (nat × vname aexp) list) option" where
  "group_update values l = (
    let
      (_, (_, _, _, _, _, t)) = hd l;
      targeted = filter (λ(regs, _). finfun_to_list regs ≠ []) l;
      maybe_updates = get_updates_opt (Label t) values (map (λ(tRegs, s, oldRegs, regs, inputs, tid, ta). (inputs, finfun_add oldRegs regs, tRegs)) targeted)
    in
    if ∃(_, f_opt) ∈ set maybe_updates. f_opt = None then
      None
    else
      Some (fold List.union (map (λ(tRegs, s, oldRegs, regs, inputs, tid, ta). tid) l) [], map (λ(r, f_o). (r, the f_o)) maybe_updates)
  )"

fun groupwise_put_updates :: "transition_group list ⇒ log ⇒ value list ⇒ run_info list ⇒ (nat × (vname aexp × vname ⇒f String.literal)) ⇒ iEFSM ⇒ iEFSM" where
  "groupwise_put_updates [] _ _ _ _  e = e" |
  "groupwise_put_updates (gp#gps) log values walked (o_inx, (op, types)) e = (
    let
      targeted = map (λx. filter (λ(_, _, _, _, _, id, tran). (id, tran) ∈ set gp) x) (map (λw. rev (target <> (rev w))) walked);
      group = fold List.union targeted []
    in
    case group_update values group of
      None ⇒ groupwise_put_updates gps log values walked (o_inx, (op, types)) e |
      Some u ⇒ groupwise_put_updates gps log values walked (o_inx, (op, types)) (make_distinct (add_groupwise_updates log [u] e))
  )"

definition updates_for_output :: "log ⇒ value list ⇒ transition_group ⇒ nat ⇒ vname aexp ⇒ vname ⇒f String.literal ⇒ iEFSM ⇒ iEFSM" where
"updates_for_output log values current o_inx op types e = (
  if AExp.enumerate_regs op = {} then e
  else
    let
      walked = everything_walk_log op o_inx types log e current;
      groups = transition_groups e log
    in
    groupwise_put_updates groups log values walked (o_inx, (op, types)) e
  )"

type_synonym output_types = "(vname aexp × vname ⇒f String.literal)"

fun put_updates :: "log ⇒ value list ⇒ transition_group ⇒ (nat × output_types option) list ⇒ iEFSM ⇒ iEFSM" where
  "put_updates _ _ _ [] e = e" |
  "put_updates log values gp ((_, None)#ops) e = put_updates log values gp ops e" |
  "put_updates log values gp ((o_inx, Some (op, types))#ops) e = (
    let
      gp' = map (λ(id, t). (id, t⦇Outputs := list_update (Outputs t) o_inx op⦈)) gp;
      generalised_model = fold (λ(id, t) acc. replace_transition acc id t) gp' e;
      e' = updates_for_output log values gp o_inx op types generalised_model
    in
    if accepts_log (set log) (tm e') then
     put_updates log values gp' ops e'
    else
     put_updates log values gp ops e
  )"

fun unzip_3 :: "('a × 'b × 'c) list ⇒ ('a list × 'b list × 'c list)" where
  "unzip_3 [] = ([], [], [])" |
  "unzip_3 ((a, b, c)#l) = (
    let (as, bs, cs) = unzip_3 l in
    (a#as, b#bs, c#cs)
  )"

lemma unzip_3: "unzip_3 l = (map fst l, map (fst ∘ snd) l, map (snd ∘ snd) l)"
  by (induct l, auto)

fun unzip_3_tailrec_rev :: "('a × 'b × 'c) list ⇒ ('a list × 'b list × 'c list) ⇒ ('a list × 'b list × 'c list)" where
  "unzip_3_tailrec_rev [] (as, bs, cs) = (as, bs, cs)" |
  "unzip_3_tailrec_rev ((a, b, c)#t) (as, bs, cs) = unzip_3_tailrec_rev t (a#as, b#bs, c#cs)"

lemma unzip_3_tailrec_rev: "unzip_3_tailrec_rev l (as, bs, cs) = ((map_tailrec_rev fst l as), (map_tailrec_rev (fst ∘ snd) l bs), (map_tailrec_rev (snd ∘ snd) l cs))"
  by (induct l arbitrary: as bs cs, auto)

definition "unzip_3_tailrec l = (let (as, bs, cs) = unzip_3_tailrec_rev l ([],[],[]) in (rev as, rev bs, rev cs))"

lemma unzip_3_tailrec [code]: "unzip_3 l = unzip_3_tailrec l"
  apply (simp only: unzip_3_tailrec_def unzip_3_tailrec_rev)
  by (simp add: Let_def map_tailrec_rev unzip_3 map_eq_map_tailrec)

text‹We want to return an aexp which, when evaluated in the correct context accounts for the literal
input-output pairs within the training set. This will be replaced by symbolic regression in the
executable›
definition get_output :: "label ⇒ nat ⇒ value list ⇒ (inputs × registers × value) list ⇒ (vname aexp × (vname ⇒f String.literal)) option" where
  "get_output _ maxReg values train = (let
    possible_funs = {a. ∀(i, r, p) ∈ set train. aval a (join_ir i r) = Some p}
    in
    if possible_funs = {} then None else Some (Eps (λx. x ∈ possible_funs), (K$ STR ''int''))
  )"
declare get_output_def [code del]
code_printing constant get_output ⇀ (Scala) "Dirties.getOutput"

definition get_outputs :: "label ⇒ nat ⇒ value list ⇒ inputs list ⇒ registers list ⇒ value list list ⇒ (vname aexp × (vname ⇒f String.literal)) option list" where
  "get_outputs l maxReg values I r outputs = map_tailrec (λ(maxReg, ps). get_output l maxReg values (zip I (zip r ps))) (enumerate maxReg (transpose outputs))"

definition enumerate_exec_values :: "trace ⇒ value list" where
  "enumerate_exec_values vs = fold (λ(_, i, p) I. List.union (List.union i p) I) vs []"

definition enumerate_log_values :: "log ⇒ value list" where
  "enumerate_log_values l = fold (λe I. List.union (enumerate_exec_values e) I) l []"

(*This is where the types stuff originates*)
definition generalise_and_update :: "log ⇒ iEFSM ⇒ transition_group ⇒ iEFSM" where
  "generalise_and_update log e gp = (
    let
      label = Label (snd (hd gp));
      values = enumerate_log_values log;
      new_gp_ts = make_training_set e log gp;
      (I, R, P) = unzip_3 new_gp_ts;
      max_reg = max_reg_total e;
      outputs = get_outputs label max_reg values I R P
    in
      put_updates log values gp (enumerate 0 outputs) e
  )"

text ‹Splitting structural groups up into subgroups by previous transition can cause different
subgroups to get different updates. We ideally want structural groups to have the same output and
update functions, as structural groups are likely to be instances of the same underlying behaviour.›
definition standardise_group :: "iEFSM ⇒ log ⇒ transition_group ⇒ (iEFSM ⇒ log ⇒ transition_group ⇒ transition_group) ⇒ iEFSM" where
  "standardise_group e l gp s = (
    let
      standardised = s e l gp;
      e' = replace_transitions e standardised
    in
      if e' = e then e else
      if accepts_log (set l) (tm e') then e' else e
)"

primrec find_outputs :: "output_function list list ⇒ iEFSM ⇒ log ⇒ transition_group ⇒ output_function list option" where
  "find_outputs [] _ _ _ = None" |
  "find_outputs (h#t) e l g = (
    let
      outputs = fold (λ(tids, t) acc. replace_transition acc tids (t⦇Outputs := h⦈)) g e
    in
      if accepts_log (set l) (tm outputs) then
        Some h
      else
        find_outputs t e l g
  )"

primrec find_updates_outputs :: "update_function list list ⇒ output_function list list ⇒ iEFSM ⇒ log ⇒ transition_group ⇒ (output_function list × update_function list) option" where
  "find_updates_outputs [] _ _ _ _ = None" |
  "find_updates_outputs (h#t) p e l g = (
    let
      updates = fold (λ(tids, t) acc. replace_transition acc tids (t⦇Updates := h⦈)) g e
    in
      case find_outputs p updates l (map (λ(id, t). (id,t⦇Updates := h⦈))  g) of
        Some pp ⇒ Some (pp, h) |
        None ⇒ find_updates_outputs t p e l g
  )"

definition updates_for :: "update_function list ⇒ update_function list list" where
  "updates_for U = (
    let uf = fold (λ(r, u) f. f(r $:= u#(f $ r))) U (K$ []) in
    map (λr. map (λu. (r, u)) (uf $ r)) (finfun_to_list uf)
  )"

definition standardise_group_outputs_updates :: "iEFSM ⇒ log ⇒ transition_group ⇒ transition_group" where
  "standardise_group_outputs_updates e l g = (
    let
      update_groups = product_lists (updates_for (remdups (List.maps (Updates ∘ snd) g)));
      update_groups_subs = fold (List.union ∘ subseqs) update_groups [];
      output_groups = product_lists (transpose (remdups (map (Outputs ∘ snd) g)))
    in
    case find_updates_outputs update_groups_subs output_groups e l g of
      None ⇒ g |
      Some (p, u) ⇒ map (λ(id, t). (id, t⦇Outputs := p, Updates := u⦈)) g
  )"

fun find_first_use_of_trace :: "nat ⇒ trace ⇒ iEFSM ⇒ cfstate ⇒ registers ⇒ tids option" where
  "find_first_use_of_trace _ [] _ _ _ = None" |
  "find_first_use_of_trace rr ((l, i, _)#es) e s r = (
    let
      (id, s', t) = fthe_elem (i_possible_steps e s r l i)
    in
      if (∃p ∈ set (Outputs t). aexp_constrains p (V (R rr))) then
        Some id
      else
        find_first_use_of_trace rr es e s' (evaluate_updates t i r)
  )"

definition find_first_uses_of :: "nat ⇒ log ⇒ iEFSM ⇒ tids list" where
  "find_first_uses_of r l e = List.maps (λx. case x of None ⇒ [] | Some x ⇒ [x]) (map (λt. find_first_use_of_trace r t e 0 <>) l)"

fun find_initialisation_of_trace :: "nat ⇒ trace ⇒ iEFSM ⇒ cfstate ⇒ registers ⇒ (tids × transition) option" where
  "find_initialisation_of_trace _ [] _ _ _ = None" |
  "find_initialisation_of_trace r' ((l, i, _)#es) e s r = (
    let
      (tids, s', t) = fthe_elem (i_possible_steps e s r l i)
    in
    if (∃(rr, u) ∈ set (Updates t). rr = r' ∧ is_lit u) then
      Some (tids, t)
    else
      find_initialisation_of_trace r' es e s' (evaluate_updates t i r)
  )"

primrec find_initialisation_of :: "nat ⇒ iEFSM ⇒ log ⇒ (tids × transition) option list" where
  "find_initialisation_of _ _ [] = []" |
  "find_initialisation_of r e (h#t) = (
    case find_initialisation_of_trace r h e 0 <> of
      None ⇒ find_initialisation_of r e t |
      Some thing ⇒ Some thing#(find_initialisation_of r e t)
  )"

definition delay_initialisation_of :: "nat ⇒ log ⇒ iEFSM ⇒ tids list ⇒ iEFSM" where
  "delay_initialisation_of r l e tids = fold (λx e. case x of
      None ⇒ e |
    Some (i_tids, t) ⇒
      let
        origins = map (λid. origin id e) tids;
        init_val = snd (hd (filter (λ(r', _). r = r') (Updates t)));
        e' = fimage (λ(id, (origin', dest), tr).
        ― ‹Add the initialisation update to incoming transitions›
        if dest ∈ set origins then
          (id, (origin', dest), tr⦇Updates := List.insert (r, init_val) (Updates tr)⦈)
        ― ‹Strip the initialisation update from the original initialising transition›
        else if id = i_tids then
          (id, (origin', dest), tr⦇Updates := filter (λ(r', _). r ≠ r') (Updates tr)⦈)
        else
          (id, (origin', dest), tr)
      ) e
      in
      ― ‹We don't want to update a register twice so just leave it›
      if accepts_log (set l) (tm e') then
        e'
      else
        e
  ) (find_initialisation_of r e l) e"

fun groupwise_generalise_and_update :: "log ⇒ iEFSM ⇒ transition_group list ⇒ iEFSM" where
  "groupwise_generalise_and_update _ e [] = e" |
  "groupwise_generalise_and_update log e (gp#t) = (
        let
          e' = generalise_and_update log e gp;
          rep = snd (hd (gp));
          structural_group = fimage (λ(i, _, t). (i, t)) (ffilter (λ(_, _, t). same_structure rep t) e');
          delayed = fold (λr acc. delay_initialisation_of r log acc (find_first_uses_of r log acc)) (sorted_list_of_set (all_regs e')) e';
          standardised = standardise_group delayed log (sorted_list_of_fset structural_group) standardise_group_outputs_updates;
          structural_group2 = fimage (λ(_, _, t). (Outputs t, Updates t)) (ffilter (λ(_, _, t).  Label rep = Label t ∧ Arity rep = Arity t ∧ length (Outputs rep) = length (Outputs t)) standardised)
        in
        ― ‹If we manage to standardise a structural group, we do not need to evolve outputs and
            updates for the other historical subgroups so can filter them out.›
        if fis_singleton structural_group2 then
          groupwise_generalise_and_update log (merge_regs standardised (accepts_log (set log))) (filter (λg. set g ∩ fset structural_group = {}) t)
        else
          groupwise_generalise_and_update log (merge_regs standardised (accepts_log (set log))) t
  )"

definition drop_all_guards :: "iEFSM ⇒ iEFSM ⇒ log ⇒ update_modifier ⇒ (iEFSM ⇒ nondeterministic_pair fset) ⇒ iEFSM" where
"drop_all_guards e pta log m np = (let
      derestricted = fimage (λ(id, tf, tran). (id, tf, tran⦇Guards := []⦈)) e;
      nondeterministic_pairs = sorted_list_of_fset (np derestricted)
    in
    case resolve_nondeterminism {} nondeterministic_pairs pta derestricted m (accepts_log (set log)) np of
      (None, _) ⇒ pta |
      (Some resolved, _) ⇒ resolved
  )"

definition updated_regs :: "transition ⇒ nat set" where
  "updated_regs t = set (map fst (Updates t))"

definition fewer_updates :: "transition ⇒ transition fset ⇒ transition option" where
  "fewer_updates t tt = (
    let p = ffilter (λt'. same_structure t t' ∧ Outputs t = Outputs t' ∧ updated_regs t' ⊂ updated_regs t) tt in
    if p = {||} then None else Some (snd (fMin (fimage (λt. (length (Updates t), t)) p))))"

fun remove_spurious_updates_aux :: "iEFSM ⇒ transition_group ⇒ transition fset ⇒ log ⇒ iEFSM" where
  "remove_spurious_updates_aux e [] _ _ = e" |
  "remove_spurious_updates_aux e ((tid, t)#ts) tt l = (
    case fewer_updates t tt of
      None ⇒ remove_spurious_updates_aux e ts tt l |
      Some t' ⇒ (
        let e' = replace_transition e tid t' in
        if accepts_log (set l) (tm e') then
          remove_spurious_updates_aux e' ts tt l
        else
          remove_spurious_updates_aux e ts tt l
      )
  )"

(* This goes through and tries to remove spurious updates that get introduced during preprocessing *)
definition remove_spurious_updates :: "iEFSM ⇒ log ⇒ iEFSM" where
  "remove_spurious_updates e l = (
    let transitions = fimage (λ(tid, _, t). (tid, t)) e in
      remove_spurious_updates_aux e (sorted_list_of_fset transitions) (fimage snd transitions) l
  )"

definition derestrict :: "iEFSM ⇒ log ⇒ update_modifier ⇒ (iEFSM ⇒ nondeterministic_pair fset) ⇒ iEFSM" where
  "derestrict pta log m np = (
    let
      normalised = groupwise_generalise_and_update log pta (transition_groups pta log)
    in
      drop_all_guards normalised pta log m np
  )"

definition "drop_pta_guards pta log m np = drop_all_guards pta pta log m np"

end