Theory SelectionStrategies

section‹Selection Strategies›
text‹The strategy used to idenfity and prioritise states to be merged plays a big part in how the
final model turns out. This theory file presents a number of different selection strategies.›

theory SelectionStrategies
imports Inference
begin

(* One point if they're equal *)
text‹The simplest strategy is to assign one point for each shared pair of transitions.›
definition exactly_equal :: strategy where
  "exactly_equal t1ID t2ID e = bool2nat ((get_by_ids e t1ID) = (get_by_ids e t2ID))"

text‹Another simple strategy is to look at the labels and arities of outgoing transitions of each
state. Pairs of states are ranked by how many transitions with the same label and arity they have in
common.›
definition naive_score :: strategy where
  "naive_score t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID
  in
  bool2nat (Label t1 = Label t2 ∧ Arity t1 = Arity t2 ∧ length (Outputs t1) = length (Outputs t2))
)"

text‹Building off the above strategy, it makes sense to give transitions an extra ``bonus point'' if
they are exactly equal.›
definition naive_score_eq_bonus :: strategy where
  "naive_score_eq_bonus t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID
  in
  score_transitions t1 t2
)"

(* One point each for equal label, arity, and outputs *)
text‹Another strategy is to assign bonus points for each shared output.›
definition naive_score_outputs :: strategy where
  "naive_score_outputs t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID
  in
    bool2nat (Label t1 = Label t2) + bool2nat (Arity t1 = Arity t2) + bool2nat (Outputs t1 = Outputs t2)
)"

(* Functions with same label, and input and output arities contribute one point for each guard    *)
(* and output they share. *)
text‹Along similar lines, we can assign additional bonus points for shared guards.›
definition naive_score_comprehensive :: strategy where
  "naive_score_comprehensive t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID
  in
  if Label t1 = Label t2 ∧ Arity t1 = Arity t2 then
    if length (Outputs t1) = length (Outputs t2) then
      card (set (Guards t1) ∩ set (Guards t2)) + length (filter (λ(p1, p2). p1 = p2) (zip (Outputs t1) (Outputs t2)))
    else 0
  else 0
)"

(* Functions with same label, and input and output arities contribute one point for each guard    *)
(* and output they share. Transitions which are exactly equal get a very high score. *)
text‹This strategy is similar to the one above except that transitions which are exactly equal get
100 bonus points. ›
definition naive_score_comprehensive_eq_high :: strategy where
  "naive_score_comprehensive_eq_high t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID
  in
  if t1 = t2 then
    100
  else
    if Label t1 = Label t2 ∧ Arity t1 = Arity t2 then
      if length (Outputs t1) = length (Outputs t2) then
        card (set (Guards t1) ∩ set (Guards t2)) + length (filter (λ(p1, p2). p1 = p2) (zip (Outputs t1) (Outputs t2)))
      else 0
    else 0
)"

(* One point if one subsumes the other *)
text‹We can incorporate the subsumption relation into the scoring of merges such that a pair of
states receives one point for each pair of transitions where one directly subsumes the other.›
definition naive_score_subsumption :: "strategy" where
  "naive_score_subsumption t1ID t2ID e = (
  let
    t1 = get_by_ids e t1ID;
    t2 = get_by_ids e t2ID;
    s = origin t1ID e
  in
  bool2nat (directly_subsumes (tm e) (tm e) s s t1 t2) + bool2nat (directly_subsumes (tm e) (tm e) s s t2 t1)
)"

(* Orders by the origin state so we merge leaves first *)
text‹An alternative strategy is to simply score merges based on the states' proximity to the origin.›
definition leaves :: strategy where
  "leaves t1ID t2ID e = (
    let
      t1 = get_by_ids e t1ID;
      t2 = get_by_ids e t2ID
    in
    if (Label t1 = Label t2 ∧ Arity t1 = Arity t2 ∧ length (Outputs t1) = length (Outputs t2)) then
      origin t1ID e + origin t2ID e
    else
      0)"

end