section ‹Underlying FSM Representation›

text ‹This theory contains the underlying datatype for (possibly not well-formed) finite state machines.›

theory FSM_Impl
  imports Util Datatype_Order_Generator.Order_Generator "HOL-Library.FSet"
begin


text ‹A finite state machine (FSM) is represented using its classical definition:›

datatype ('state, 'input, 'output) fsm_impl = FSMI (initial : 'state)  
                                                  (states  : "'state set")
                                                  (inputs  : "'input set")
                                                  (outputs : "'output set")
                                                  (transitions : "('state × 'input × 'output × 'state) set")


subsection ‹Types for Transitions and Paths›

type_synonym ('a,'b,'c) transition = "('a × 'b × 'c × 'a)"
type_synonym ('a,'b,'c) path = "('a,'b,'c) transition list"

abbreviation "t_source (a :: ('a,'b,'c) transition) ≡ fst a" 
abbreviation "t_input (a :: ('a,'b,'c) transition) ≡ fst (snd a)"
abbreviation "t_output (a :: ('a,'b,'c) transition) ≡ fst (snd (snd a))"
abbreviation "t_target (a :: ('a,'b,'c) transition) ≡ snd (snd (snd a))"

subsection ‹Basic Algorithms on FSM›

subsubsection ‹Reading FSMs from Lists›

fun fsm_impl_from_list :: "'a →
                           ('a,'b,'c) transition list →
                           ('a, 'b, 'c) fsm_impl" 
  where
  "fsm_impl_from_list q [] = FSMI q {q} {} {} {}" |
  "fsm_impl_from_list q (t#ts) =
    (let ts' = set (t#ts)
     in FSMI (t_source t)
             ((image t_source ts') ∪ (image t_target ts'))
             (image t_input ts')
             (image t_output ts')
             (ts'))"

fun fsm_impl_from_list' :: "'a → ('a,'b,'c) transition list → ('a, 'b, 'c) fsm_impl" where
  "fsm_impl_from_list' q [] = FSMI q {q} {} {} {}" |
  "fsm_impl_from_list' q (t#ts) = (let tsr = (remdups (t#ts))
                                   in FSMI (t_source t)
                                      (set (remdups ((map t_source tsr) @ (map t_target tsr))))
                                      (set (remdups (map t_input tsr)))
                                      (set (remdups (map t_output tsr)))
                                      (set tsr))"

lemma fsm_impl_from_list_code[code] :
  "fsm_impl_from_list q ts = fsm_impl_from_list' q ts" 
  by (cases ts; auto)


subsubsection ‹Changing the initial State›

fun from_FSMI :: "('a,'b,'c) fsm_impl → 'a → ('a,'b,'c) fsm_impl" where
  "from_FSMI M q = (if q ∈ states M then FSMI q (states M) (inputs M) (outputs M) (transitions M) else M)"


subsubsection ‹Product Construction›

fun product :: "('a,'b,'c) fsm_impl → ('d,'b,'c) fsm_impl → ('a × 'd,'b,'c) fsm_impl" where
  "product A B = FSMI ((initial A, initial B))
                     ((states A) × (states B))
                     (inputs A ∪ inputs B)
                     (outputs A ∪ outputs B)
                     {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}"

lemma product_code_naive[code] :
  "product A B = FSMI ((initial A, initial B))
                     ((states A) × (states B))
                     (inputs A ∪ inputs B)
                     (outputs A ∪ outputs B)
                     (image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) (Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (∪(image (λ tA . image (λ tB . (tA,tB)) (transitions B)) (transitions A)))))"
  (is "?P1 = ?P2")
proof -
  have "(∪(image (λ tA . image (λ tB . (tA,tB)) (transitions B)) (transitions A))) = {(tA,tB) | tA tB . tA ∈ transitions A ∧ tB ∈ transitions B}"
    by auto
  then have "(Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (∪(image (λ tA . image (λ tB . (tA,tB)) (transitions B)) (transitions A)))) = {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}"
    by auto
  then have "image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) (Set.filter (λ((qA,x,y,qA'), (qB,x',y',qB')) . x = x' ∧ y = y') (∪(image (λ tA . image (λ tB . (tA,tB)) (transitions B)) (transitions A))))
              = image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}"
    by auto
  moreover have "image (λ((qA,x,y,qA'), (qB,x',y',qB')) . ((qA,qB),x,y,(qA',qB'))) {((qA,x,y,qA'),(qB,x,y,qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B} = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}"
    by force
  ultimately have "transitions ?P1 = transitions ?P2" 
    unfolding product.simps by auto
  moreover have "initial ?P1 = initial ?P2" by auto
  moreover have "states ?P1 = states ?P2" by auto
  moreover have "inputs ?P1 = inputs ?P2" by auto
  moreover have "outputs ?P1 = outputs ?P2" by auto
  ultimately show ?thesis by auto
qed


subsubsection ‹Filtering Transitions›

fun filter_transitions :: "('a,'b,'c) fsm_impl → (('a,'b,'c) transition → bool) → ('a,'b,'c) fsm_impl" where
  "filter_transitions M P = FSMI (initial M)
                                (states M)
                                (inputs M)
                                (outputs M)
                                (Set.filter P (transitions M))"


subsubsection ‹Filtering States›

fun filter_states :: "('a,'b,'c) fsm_impl → ('a → bool) → ('a,'b,'c) fsm_impl" where
  "filter_states M P = (if P (initial M) then FSMI (initial M)
                                                  (Set.filter P (states M))
                                                  (inputs M)
                                                  (outputs M)
                                                  (Set.filter (λ t . P (t_source t) ∧ P (t_target t)) (transitions M))
                                         else M)"
 
subsubsection ‹Initial Singleton FSMI (For Trivial Preamble)›    

fun initial_singleton :: "('a,'b,'c) fsm_impl → ('a,'b,'c) fsm_impl" where
  "initial_singleton M = FSMI (initial M)
                             {initial M}
                             (inputs M)
                             (outputs M)
                             {}"


subsubsection ‹Canonical Separator›

abbreviation "shift_Inl t ≡ (Inl (t_source t),t_input t, t_output t, Inl (t_target t))"

definition shifted_transitions :: "(('a × 'a) × 'b × 'c × ('a × 'a)) set → ((('a × 'a) + 'd) × 'b × 'c × (('a × 'a) + 'd)) set" where
  "shifted_transitions ts = image shift_Inl ts"

definition distinguishing_transitions :: "(('a × 'b) → 'c set) → 'a → 'a → ('a × 'a) set → 'b set → ((('a × 'a) + 'a) × 'b × 'c × (('a × 'a) + 'a)) set" where
  "distinguishing_transitions f q1 q2 stateSet inputSet = ∪ (Set.image (λ((q1',q2'),x) .
                                                                (image (λy . (Inl (q1',q2'),x,y,Inr q1)) (f (q1',x) - f (q2',x)))
                                                                ∪ (image (λy . (Inl (q1',q2'),x,y,Inr q2)) (f (q2',x) - f (q1',x))))
                                                            (stateSet × inputSet))"



(* Note: parameter P is added to allow usage of different restricted versions of the product machine *)
fun canonical_separator' :: "('a,'b,'c) fsm_impl → (('a × 'a),'b,'c) fsm_impl → 'a → 'a → (('a × 'a) + 'a,'b,'c) fsm_impl" where
  "canonical_separator' M P q1 q2 = (if initial P = (q1,q2)
  then
    (let f' = set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M));
         f = (λqx . (case f' qx of Some yqs → yqs | None → {}));
         shifted_transitions' = shifted_transitions (transitions P);
         distinguishing_transitions_lr = distinguishing_transitions f q1 q2 (states P) (inputs P);
         ts = shifted_transitions' ∪ distinguishing_transitions_lr
     in
  
      FSMI (Inl (q1,q2))
      ((image Inl (states P)) ∪ {Inr q1, Inr q2})
      (inputs M ∪ inputs P)
      (outputs M ∪ outputs P)
      (ts))
  else FSMI (Inl (q1,q2)) {Inl (q1,q2)} {} {} {})"

lemma h_out_impl_helper: "(λ (q,x) . {y . ∃ q' . (q,x,y,q') ∈ A}) = (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) A)) qx of Some yqs → yqs | None → {}))"
proof 
  fix qx 
  show "(λ (q,x) . {y . ∃ q' . (q,x,y,q') ∈ A}) qx = (λqx . (case (set_as_map (image (λ(q,x,y,q') . ((q,x),y)) A)) qx of Some yqs → yqs | None → {})) qx"
  proof -
    obtain q x where "qx = (q,x)" using prod.exhaust by metis
    have **: "∧ z . ((q, x), z) ∈ (λ(q, x, y, q'). ((q, x), y)) ` A = (z ∈ {y . ∃ q' . (q,x,y,q') ∈ A})"
      by force
    show ?thesis unfolding ‹qx = (q,x)› case_prod_conv set_as_map_def 
      unfolding ** by auto
  qed
qed

lemma canonical_separator'_simps :
        "initial (canonical_separator' M P q1 q2) = Inl (q1,q2)"
        "states (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then (image Inl (states P)) ∪ {Inr q1, Inr q2} else {Inl (q1,q2)})"
        "inputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then inputs M ∪ inputs P else {})"
        "outputs (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then outputs M ∪ outputs P else {})"
        "transitions (canonical_separator' M P q1 q2) = (if initial P = (q1,q2) then shifted_transitions (transitions P) ∪ distinguishing_transitions (λ (q,x) . {y . ∃ q' . (q,x,y,q') ∈ transitions M}) q1 q2 (states P) (inputs P) else {})"
  unfolding h_out_impl_helper by (simp add: Let_def)+



subsubsection ‹Generalised Canonical Separator›

text ‹A variation on the state separator that uses states @{text "L"} and @{text "R"} instead of
 @{text "Inr q1"} and @{text "Inr q2"} to indicate targets of transitions in the
 canonical separator that are available only for the left or right component of a state pair›

text ‹Note: this definition of a canonical separator might serve as a way to avoid recalculation
 of state separators for different pairs of states, but is currently not fully
 implemented›

datatype LR = Left | Right
derive linorder LR

definition distinguishing_transitions_LR :: "(('a × 'b) → 'c set) → ('a × 'a) set → 'b set → ((('a × 'a) + LR) × 'b × 'c × (('a × 'a) + LR)) set" where
  "distinguishing_transitions_LR f stateSet inputSet = ∪ (Set.image (λ((q1',q2'),x) .
                                                                (image (λy . (Inl (q1',q2'),x,y,Inr Left)) (f (q1',x) - f (q2',x)))
                                                                ∪ (image (λy . (Inl (q1',q2'),x,y,Inr Right)) (f (q2',x) - f (q1',x))))
                                                            (stateSet × inputSet))"


fun canonical_separator_complete' :: "('a,'b,'c) fsm_impl → (('a × 'a) + LR,'b,'c) fsm_impl" where
  "canonical_separator_complete' M =
    (let P = product M M;
         f' = set_as_map (image (λ(q,x,y,q') . ((q,x),y)) (transitions M));
         f = (λqx . (case f' qx of Some yqs → yqs | None → {}));
         shifted_transitions' = shifted_transitions (transitions P);
         distinguishing_transitions_lr = distinguishing_transitions_LR f (states P) (inputs P);
         ts = shifted_transitions' ∪ distinguishing_transitions_lr
     in
      FSMI (Inl (initial P))
          ((image Inl (states P)) ∪ {Inr Left, Inr Right})
          (inputs M ∪ inputs P)
          (outputs M ∪ outputs P)
          ts )"



subsubsection ‹Adding Transitions›

fun add_transitions :: "('a,'b,'c) fsm_impl → ('a,'b,'c) transition set → ('a,'b,'c) fsm_impl" where
  "add_transitions M ts = (if (∀ t ∈ ts . t_source t ∈ states M ∧ t_input t ∈ inputs M ∧ t_output t ∈ outputs M ∧ t_target t ∈ states M)
    then FSMI (initial M)
             (states M)
             (inputs M)
             (outputs M)
             ((transitions M) ∪ ts)
    else M)"


subsubsection ‹Creating an FSMI without transitions›

fun create_unconnected_FSMI :: "'a → 'a set → 'b set → 'c set → ('a,'b,'c) fsm_impl" where
  "create_unconnected_FSMI q ns ins outs = (if (finite ns ∧ finite ins ∧ finite outs)
    then FSMI q (insert q ns) ins outs {}
    else FSMI q {q} {} {} {})"

fun create_unconnected_fsm_from_lists :: "'a → 'a list → 'b list → 'c list → ('a,'b,'c) fsm_impl" where
  "create_unconnected_fsm_from_lists q ns ins outs = FSMI q (insert q (set ns)) (set ins) (set outs) {}"

fun create_unconnected_fsm_from_fsets :: "'a → 'a fset → 'b fset → 'c fset → ('a,'b,'c) fsm_impl" where
  "create_unconnected_fsm_from_fsets q ns ins outs = FSMI q (insert q (fset ns)) (fset ins) (fset outs) {}"

fun create_fsm_from_sets :: "'a → 'a set → 'b set → 'c set → ('a,'b,'c) transition set → ('a,'b,'c) fsm_impl" where
  "create_fsm_from_sets q qs ins outs ts = (if q ∈ qs ∧ finite qs ∧ finite ins ∧ finite outs
    then add_transitions (FSMI q qs ins outs {}) ts
    else FSMI q {q} {} {} {})"
 

subsection ‹Transition Function h›

text ‹Function @{text "h"} represents the classical view of the transition relation of an FSM @{text "M"} as a
 function: given a state @{text "q"} and an input @{text "x"}, @{text "(h M) (q,x)"} returns all
 possibly reactions @{text "(y,q')"} of @{text "M"} in state @{text "q"} to @{text "x"}, where
 @{text "y"} is the produced output and @{text "q'"} the target state of the reaction transition.›

fun h :: "('state, 'input, 'output) fsm_impl → ('state × 'input) → ('output × 'state) set" where
  "h M (q,x) = { (y,q') . (q,x,y,q') ∈ transitions M }"

fun h_obs :: "('a,'b,'c) fsm_impl → 'a → 'b → 'c → 'a option" where
  "h_obs M q x y = (let
      tgts = snd ` Set.filter (λ (y',q') . y' = y) (h M (q,x))
    in if card tgts = 1
      then Some (the_elem tgts)
      else None)"

lemma h_code[code] : 
  "h M (q,x) = (let m = set_as_map (image (λ(q,x,y,q') . ((q,x),y,q')) (transitions M))
                 in (case m (q,x) of Some yqs → yqs | None → {}))"
  unfolding set_as_map_def by force


subsection ‹Extending FSMs by single elements›

fun add_transition :: "('a,'b,'c) fsm_impl →
                       ('a,'b,'c) transition →
                       ('a,'b,'c) fsm_impl" 
  where
  "add_transition M t =
    (if t_source t ∈ states M ∧ t_input t ∈ inputs M ∧
        t_output t ∈ outputs M ∧ t_target t ∈ states M
     then FSMI (initial M)
               (states M)
               (inputs M)
               (outputs M)
               (insert t (transitions M))
     else M)"

fun add_state :: "('a,'b,'c) fsm_impl → 'a → ('a,'b,'c) fsm_impl" where
  "add_state M q = FSMI (initial M) (insert q (states M)) (inputs M) (outputs M) (transitions M)"

fun add_input :: "('a,'b,'c) fsm_impl → 'b → ('a,'b,'c) fsm_impl" where
  "add_input M x = FSMI (initial M) (states M) (insert x (inputs M)) (outputs M) (transitions M)"

fun add_output :: "('a,'b,'c) fsm_impl → 'c → ('a,'b,'c) fsm_impl" where
  "add_output M y = FSMI (initial M) (states M) (inputs M) (insert y (outputs M)) (transitions M)"

fun add_transition_with_components :: "('a,'b,'c) fsm_impl → ('a,'b,'c) transition → ('a,'b,'c) fsm_impl" where
  "add_transition_with_components M t = add_transition (add_state (add_state (add_input (add_output M (t_output t)) (t_input t)) (t_source t)) (t_target t)) t"

subsection ‹Renaming elements›

fun rename_states :: "('a,'b,'c) fsm_impl → ('a → 'd) → ('d,'b,'c) fsm_impl" where
  "rename_states M f = FSMI (f (initial M))
                            (f ` states M)
                            (inputs M)
                            (outputs M)
                            ((λt . (f (t_source t), t_input t, t_output t, f (t_target t))) ` transitions M)"
                              

end