Theory Distinguishing_Guards

section‹Distinguishing Guards›
text‹If we cannot resolve the nondeterminism which arises from merging states by merging
transitions, we might then conclude that those states should not be merged. Alternatively, we could
consider the possibility of \emph{value-dependent} behaviour. This theory presents a heuristic which
tries to find a guard which distinguishes between a pair of transitions.›

theory Distinguishing_Guards
imports "../Inference"
begin

hide_const uids

definition put_updates :: "tids  update_function list  iEFSM  iEFSM" where
  "put_updates uids updates iefsm = fimage (λ(uid, fromTo, tran).
      case uid of [u] 
      if u  set uids then
        (uid, fromTo, Label = Label tran, Arity = Arity tran, Guards = Guards tran, Outputs = Outputs tran, Updates = (Updates tran)@updates)
      else
        (uid, fromTo, tran)
      ) iefsm"

definition transfer_updates :: "iEFSM  iEFSM  iEFSM" where
  "transfer_updates e pta = fold (λ(tids, (from, to), tran) acc. put_updates tids (Updates tran) acc) (sorted_list_of_fset e) pta"

fun trace_collect_training_sets :: "trace  iEFSM  cfstate  registers  tids  tids  (inputs × registers) list  (inputs × registers) list  ((inputs × registers) list × (inputs × registers) list)" where
  "trace_collect_training_sets [] uPTA s registers T1 T2 G1 G2 = (G1, G2)" |
  "trace_collect_training_sets ((label, inputs, outputs)#t) uPTA s registers T1 T2 G1 G2 = (
    let
      (uids, s', tran) = fthe_elem (ffilter (λ(uids, s', tran). evaluate_outputs tran inputs registers = map Some outputs) (i_possible_steps uPTA s registers label inputs));
      updated = (evaluate_updates tran inputs registers)
    in
    if hd uids  set T1 then
      trace_collect_training_sets t uPTA s' updated T1 T2 ((inputs, registers)#G1) G2
    else if hd uids  set T2 then
      trace_collect_training_sets t uPTA s' updated T1 T2 G1 ((inputs, registers)#G2)
    else
      trace_collect_training_sets t uPTA s' updated T1 T2 G1 G2
  )"

primrec collect_training_sets :: "log  iEFSM  tids  tids  (inputs × registers) list  (inputs × registers) list  ((inputs × registers) list × (inputs × registers) list)" where
  "collect_training_sets [] uPTA T1 T2 G1 G2 = (G1, G2)" |
  "collect_training_sets (h#t) uPTA T1 T2 G1 G2 = (
    let (G1a, G2a) = trace_collect_training_sets h uPTA 0 <> T1 T2 [] [] in
    collect_training_sets t uPTA T1 T2 (List.union G1 G1a) (List.union G2 G2a)
  )"

definition find_distinguishing_guards :: "(inputs × registers) list  (inputs × registers) list  (vname gexp × vname gexp) option" where
  "find_distinguishing_guards G1 G2 = (
    let gs = {(g1, g2).
      ((i, r)  set G1. gval g1 (join_ir i r) = true) 
      ((i, r)  set G2. gval g2 (join_ir i r) = true) 
      (i r. ¬ (gval g1 (join_ir i r) = true  gval g2 (join_ir i r) = true))
    } in
    if gs = {} then None else Some (Eps (λg. g  gs))
  )"
declare find_distinguishing_guards_def [code del]
code_printing constant find_distinguishing_guards  (Scala) "Dirties.findDistinguishingGuards"

definition add_guard :: "transition  vname gexp  transition" where
  "add_guard t g = tGuards := List.insert g (Guards t)"

definition distinguish :: "log  update_modifier" where
  "distinguish log t1ID t2ID s destMerge preDestMerge old check = (
    let
      t1 = get_by_ids destMerge t1ID;
      t2 = get_by_ids destMerge t2ID;
      uPTA = transfer_updates destMerge (make_pta log);
      (G1, G2) = collect_training_sets log uPTA t1ID t2ID [] []
    in
      case find_distinguishing_guards G1 G2 of
        None  None |
        Some (g1, g2)  (
          let rep = replace_transitions preDestMerge [(t1ID, add_guard t1 g1), (t2ID, add_guard t2 g2)] in
          if check (tm rep) then Some rep else None
        )
  )"

definition can_still_take_ctx :: "transition_matrix  transition_matrix  cfstate  cfstate  transition  transition  bool" where
  "can_still_take_ctx e1 e2 s1 s2 t1 t2 = (
    t. recognises e1 t  visits s1 e1 0 <> t  recognises e2 t  visits s2 e2 0 <> t 
    (a. obtains s2 a e2 0 <> t   (i. can_take_transition t2 i a  can_take_transition t1 i a))
  )"

lemma distinguishing_guard_subsumption:
"Label t1 = Label t2 
 Arity t1 = Arity t2 
 Outputs t1 = Outputs t2 
 Updates t1 = Updates t2 
 can_still_take_ctx e1 e2 s1 s2 t1 t2 
 recognises e1 p 
 visits s1 e1 0 <> p 
 obtains s2 c e2 0 <> p 
 subsumes t1 c t2"
  apply (simp add: subsumes_def can_still_take_ctx_def)
  apply (erule_tac x=p in allE)
  apply simp
  by (simp add: obtains_recognises obtains_visits)

definition "recognises_and_visits_both a b s s' = (
  p c1 c2. obtains s c1 a 0 <> p  obtains s' c2 b 0 <> p)"

definition "can_still_take e1 e2 s1 s2 t1 t2 = (
  Label t1 = Label t2 
  Arity t1 = Arity t2 
  Outputs t1 = Outputs t2 
  Updates t1 = Updates t2 
  can_still_take_ctx e1 e2 s1 s2 t1 t2 
  recognises_and_visits_both e1 e2 s1 s2)"

lemma can_still_take_direct_subsumption:
  "can_still_take e1 e2 s1 s2 t1 t2 
  directly_subsumes e1 e2 s1 s2 t1 t2"
  apply (simp add: directly_subsumes_def can_still_take_def)
  apply standard
  by (meson distinguishing_guard_subsumption obtains_visits obtains_recognises recognises_and_visits_both_def)

end