# Theory FSM_Impl

```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```