Theory Store_Reuse

chapter‹Heuristics›
text‹As part of this inference technique, we make use of certain \emph{heuristics} to abstract away
concrete values into registers. This allows us to generalise from examples of behaviour. These
heuristics are as follows.

\begin{description}
  \item [Store and Reuse] - This heuristic aims to recognise when input values are subsequently used
as an output. Such behaviour is generalised by storing the relevant input in a register, and
replacing the literal output with the content of the register. This enables the EFSM to
\emph{predict} how the underlying system might behave when faced with unseen inputs.
  \item [Increment and Reset] - This heuristic is a naive attempt to introduce additive behaviour.
The idea here is that if we want to merge two transitions with identical input values and different
numeric outputs, for example $\textit{coin}:1[i_0=50]/o_0:=50$ and $\textit{coin}:1[i_0=50]/o_0:=100$,
then the behaviour must depend on the value of an internal variable. This heuristic works by
dropping the input guard and adding an update to a fresh register, in this case summing the current
register value with the input. A similar principle can be applied to other numeric functions such as
subtraction.
  \item [Same Register] - Because of the way heuristics are applied, it is possible for different
registers to be introduced to serve the same purpose. This heuristic attempts to identify when this
has happened and merge the two registers.
  \item [Least Upper Bound] - In certain situations, transitions may produce the same output for
different inputs. This technique forms the least upper bound of the transition guards
--- their disjunction --- such that they can be merged into a single behaviour.
  \item [Distinguishing Guards] - Under certain circumstances, we explicitly do not want to merge
two transitions into one. This heuristic resolves nondeterminism between transitions by attempting
to find apply mutually exclusive guards to each transition such that their behaviour is distinguished.
\end{description}›

section‹Store and Reuse›
text‹An obvious candidate for generalisation is the ``store and reuse'' pattern. This manifests
itself  when the input of one transition is subsequently used as the output of another. Recognising
this usage pattern allows us to introduce a \emph{storage register} to abstract away concrete data
values and replace two transitions whose outputs differ with a single transition that outputs the
content of the register.›

theory Store_Reuse
imports "../Inference"
begin
datatype ioTag = In | Out

instantiation ioTag :: linorder begin
fun less_ioTag :: "ioTag  ioTag  bool" where
  "In < Out = True" |
  "Out < _ = False" |
  "In < In = False"

definition less_eq_ioTag :: "ioTag  ioTag  bool" where
  "less_eq_ioTag x y = (x < y  x = y)"
declare less_eq_ioTag_def [simp]

instance
  apply standard
  using less_ioTag.elims(2) apply fastforce
     apply simp
    apply (metis ioTag.exhaust less_eq_ioTag_def)
  using less_eq_ioTag_def less_ioTag.elims(2) apply blast
  by (metis (full_types) ioTag.exhaust less_eq_ioTag_def less_ioTag.simps(1))
end

type_synonym index = "nat × ioTag × nat"

fun lookup :: "index  trace  value" where
  "lookup (actionNo, In, inx) t = (let (_, inputs, _) = nth t actionNo in nth inputs inx)" |
  "lookup (actionNo, Out, inx) t = (let (_, _, outputs) = nth t actionNo in nth outputs inx)"

abbreviation actionNum :: "index  nat" where
  "actionNum i  fst i"

abbreviation ioTag :: "index  ioTag" where
  "ioTag i  fst (snd i)"

abbreviation inx :: "index  nat" where
  "inx i  snd (snd i)"

primrec index :: "value list  nat  ioTag  nat  index fset" where
  "index [] _ _ _ = {||}" |
  "index (h#t) actionNo io ind = finsert (actionNo, io, ind) (index t actionNo io (ind + 1))"

definition io_index :: "nat  value list  value list  index fset" where
  "io_index actionNo inputs outputs = (index inputs actionNo In 0) |∪| (index outputs actionNo Out 0)"

definition indices :: "trace  index fset" where
  "indices e = foldl (|∪|) {||} (map (λ(actionNo, (label, inputs, outputs)). io_index actionNo inputs outputs) (enumerate 0 e))"

definition get_by_id_intratrace_matches :: "trace  (index × index) fset" where
  "get_by_id_intratrace_matches e = ffilter (λ(a, b). lookup a e = lookup b e  actionNum a  actionNum b  a  b) (indices e |×| indices e)"

(*
  If the EFSM is nondeterministic, we need to make sure it chooses the right path so that it recognises
  the input trace.
*)
definition i_step :: "execution  iEFSM  cfstate  registers  label  inputs  (transition × cfstate × tids × registers) option" where
  "i_step tr e s r l i = (let
    poss_steps = (i_possible_steps e s r l i);
    possibilities = ffilter (λ(u, s', t). recognises_execution (tm e) s' (evaluate_updates t i r) tr) poss_steps in
    case random_member possibilities of
      None  None |
      Some (u, s', t) 
      Some (t, s', u, (evaluate_updates t i r))
  )"

type_synonym match = "(((transition × tids) × ioTag × nat) × ((transition × tids) × ioTag × nat))"

definition "exec2trace t = map (λ(label, inputs, _). (label, inputs)) t"
primrec (nonexhaustive) walk_up_to :: "nat  iEFSM  nat  registers  trace  (transition × tids)" where
  "walk_up_to n e s r (h#t) =
    (case (i_step (exec2trace t) e s r (fst h) (fst (snd h))) of
      (Some (transition, s', uid, updated))  (case n of 0  (transition, uid) | Suc m  walk_up_to m e s' updated t)
    )"

definition find_intertrace_matches_aux :: "(index × index) fset  iEFSM  trace  match fset" where
  "find_intertrace_matches_aux intras e t = fimage (λ((e1, io1, inx1), (e2, io2, inx2)). (((walk_up_to e1 e 0 <> t), io1, inx1), ((walk_up_to e2 e 0 <> t), io2, inx2))) intras"

definition find_intertrace_matches :: "log  iEFSM  match list" where
  "find_intertrace_matches l e = filter (λ((e1, io1, inx1), (e2, io2, inx2)). e1  e2) (concat (map (λ(t, m). sorted_list_of_fset (find_intertrace_matches_aux m e t)) (zip l (map get_by_id_intratrace_matches l))))"

definition total_max_input :: "iEFSM  nat" where
  "total_max_input e = (case EFSM.max_input (tm e) of None  0 | Some i  i)"

definition total_max_reg :: "iEFSM  nat" where
  "total_max_reg e = (case EFSM.max_reg (tm e) of None  0 | Some i  i)"

definition remove_guard_add_update :: "transition  nat  nat  transition" where
  "remove_guard_add_update t inputX outputX = 
    Label = (Label t), Arity = (Arity t),
    Guards = (filter (λg. ¬ gexp_constrains g (V (vname.I inputX))) (Guards t)),
    Outputs = (Outputs t),
    Updates = (outputX, (V (vname.I inputX)))#(Updates t)
  "

definition generalise_output :: "transition  nat  nat  transition" where
  "generalise_output t regX outputX = 
      Label = (Label t),
      Arity = (Arity t),
      Guards = (Guards t),
      Outputs = list_update (Outputs t) outputX (V (R regX)),
      Updates = (Updates t)
    "

definition is_generalised_output_of :: "transition  transition  nat  nat  bool" where
  "is_generalised_output_of t' t r p = (t' = generalise_output t r p)"

primrec count :: "'a  'a list  nat" where
  "count _ [] = 0" |
  "count a (h#t) = (if a = h then 1+(count a t) else count a t)"

definition replaceAll :: "iEFSM  transition  transition  iEFSM" where
  "replaceAll e old new = fimage (λ(uid, (from, dest), t). if t = old then (uid, (from, dest), new) else (uid, (from, dest), t)) e"

primrec generalise_transitions :: "((((transition × tids) × ioTag × nat) × (transition × tids) × ioTag × nat) ×
     ((transition × tids) × ioTag × nat) × (transition × tids) × ioTag × nat) list  iEFSM  iEFSM" where
  "generalise_transitions [] e = e" |
  "generalise_transitions (h#t) e = (let
    ((((orig1, u1), _), (orig2, u2), _), (((gen1, u1'), _), (gen2, u2), _)) = h in
   generalise_transitions t (replaceAll (replaceAll e orig1 gen1) orig2 gen2))"

definition strip_uids :: "(((transition × tids) × ioTag × nat) × (transition × tids) × ioTag × nat)  ((transition × ioTag × nat) × (transition × ioTag × nat))" where
  "strip_uids x = (let (((t1, u1), io1, in1), (t2, u2), io2, in2) = x in ((t1, io1, in1), (t2, io2, in2)))"

definition modify :: "match list  tids  tids  iEFSM  iEFSM option" where
  "modify matches u1 u2 old = (let relevant = filter (λ(((_, u1'), io, _), (_, u2'), io', _). io = In  io' = Out  (u1 = u1'  u2 = u1'  u1 = u2'  u2 = u2')) matches;
                                   newReg = case max_reg old of None  1 | Some r  r + 1;
                                   replacements = map (λ(((t1, u1), io1, inx1), (t2, u2), io2, inx2). (((remove_guard_add_update t1 inx1 newReg, u1), io1, inx1), (generalise_output t2 newReg inx2, u2), io2, inx2)) relevant;
                                   comparisons = zip relevant replacements;
                                   stripped_replacements = map strip_uids replacements;
                                   to_replace = filter (λ(_, s). count (strip_uids s) stripped_replacements > 1) comparisons in
                                if to_replace = [] then None else Some ((generalise_transitions to_replace old))
                              )"

(* type_synonym update_modifier = "transition ⇒ transition ⇒ nat ⇒ iEFSM ⇒ iEFSM ⇒ (iEFSM × (nat ⇒ nat) × (nat ⇒ nat)) option" *)
definition heuristic_1 :: "log  update_modifier" where
  "heuristic_1 l t1 t2 s new _ old check = (case modify (find_intertrace_matches l old) t1 t2 new of
    None  None |
    Some e  if check (tm e) then Some e else None
  )"

lemma remove_guard_add_update_preserves_outputs:
  "Outputs (remove_guard_add_update t i r) = Outputs t"
  by (simp add: remove_guard_add_update_def)

lemma remove_guard_add_update_preserves_label:
  "Label (remove_guard_add_update t i r) = Label t"
  by (simp add: remove_guard_add_update_def)

lemma remove_guard_add_update_preserves_arity:
  "Arity (remove_guard_add_update t i r) = Arity t"
  by (simp add: remove_guard_add_update_def)

lemmas remove_guard_add_update_preserves = remove_guard_add_update_preserves_label
                                           remove_guard_add_update_preserves_arity
                                           remove_guard_add_update_preserves_outputs

definition is_generalisation_of :: "transition  transition  nat  nat  bool" where
  "is_generalisation_of t' t i r = (t' = remove_guard_add_update t i r 
                                    i < Arity t 
                                    (v. Eq (V (vname.I i)) (L v)  set (Guards t)) 
                                    r  set (map fst (Updates t)))"

lemma generalise_output_preserves_label:
  "Label (generalise_output t r p) = Label t"
  by (simp add: generalise_output_def)

lemma generalise_output_preserves_arity:
  "Arity (generalise_output t r p) = Arity t"
  by (simp add: generalise_output_def)

lemma generalise_output_preserves_guard:
  "Guards (generalise_output t r p) = Guards t"
  by (simp add: generalise_output_def)

lemma generalise_output_preserves_output_length:
  "length (Outputs (generalise_output t r p)) = length (Outputs t)"
  by (simp add: generalise_output_def)

lemma generalise_output_preserves_updates:
  "Updates (generalise_output t r p) = Updates t"
  by (simp add: generalise_output_def)

lemmas generalise_output_preserves = generalise_output_preserves_label
                                     generalise_output_preserves_arity
                                     generalise_output_preserves_output_length
                                     generalise_output_preserves_guard
                                     generalise_output_preserves_updates

definition is_proper_generalisation_of :: "transition  transition  iEFSM  bool" where
 "is_proper_generalisation_of t' t e = (i  total_max_input e.  r  total_max_reg e.
                                        is_generalisation_of t' t i r 
                                        (u  set (Updates t). fst u  r) 
                                        (i  max_input (tm e). u  set (Updates t). fst u  r)
                                       )"

(* Recognising the same input used in multiple guards *)
definition generalise_input :: "transition  nat  nat  transition" where
  "generalise_input t r i = 
      Label = Label t,
      Arity = Arity t,
      Guards = map (λg. case g of Eq (V (I i')) (L _)  if i = i' then Eq (V (I i)) (V (R r)) else g | _  g) (Guards t),
      Outputs = Outputs t,
      Updates = Updates t
    "

fun structural_count :: "((transition × ioTag × nat) × (transition × ioTag × nat))  ((transition × ioTag × nat) × (transition × ioTag × nat)) list  nat" where
  "structural_count _ [] = 0" |
  "structural_count a (((t1', io1', i1'), (t2', io2', i2'))#t) = (
    let ((t1, io1, i1), (t2, io2, i2)) = a in
    if same_structure t1 t1'  same_structure t2 t2' 
       io1 = io1'  io2 = io2' 
       i1 = i1'  i2 = i2'
    then
      1+(structural_count a t)
    else
      structural_count a t
    )"

definition remove_guards_add_update :: "transition  nat  nat  transition" where
  "remove_guards_add_update t inputX outputX = 
    Label = (Label t), Arity = (Arity t),
    Guards = [],
    Outputs = (Outputs t),
    Updates = (outputX, (V (vname.I inputX)))#(Updates t)
  "

definition modify_2 :: "match list  tids  tids  iEFSM  iEFSM option" where
  "modify_2 matches u1 u2 old = (let relevant = filter (λ(((_, u1'), io, _), (_, u2'), io', _). io = In  io' = In  (u1 = u1'  u2 = u1'  u1 = u2'  u2 = u2')) matches;
                                   newReg = case max_reg old of None  1 | Some r  r + 1;
                                   replacements = map (λ(((t1, u1), io1, inx1), (t2, u2), io2, inx2).
                                                  (((remove_guards_add_update t1 inx1 newReg, u1), io1, inx1),
                                                    (generalise_input t2 newReg inx2, u2), io2, inx2)) relevant;
                                   comparisons = zip relevant replacements;
                                   stripped_replacements = map strip_uids replacements;
                                   to_replace = filter (λ(_, s). structural_count (strip_uids s) stripped_replacements > 1) comparisons in
                                if to_replace = [] then None else Some ((generalise_transitions to_replace old))
                              )"

(* type_synonym update_modifier = "transition ⇒ transition ⇒ nat ⇒ iEFSM ⇒ iEFSM ⇒ (iEFSM × (nat ⇒ nat) × (nat ⇒ nat)) option" *)
definition heuristic_2 :: "log  update_modifier" where
  "heuristic_2 l t1 t2 s new _ old check = (case modify_2 (find_intertrace_matches l old) t1 t2 new of
    None  None |
    Some e  if check (tm e) then Some e else None
  )"
hide_const ioTag.In

end