Theory AWN_SOS

(*  Title:       AWN_SOS.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Semantics of the Algebra of Wireless Networks"

theory AWN_SOS
imports TransitionSystems AWN
begin

subsection "Table 1: Structural operational semantics for sequential process expressions "

inductive_set
  seqp_sos
  :: "('s, 'm, 'p, 'l) seqp_env  ('s × ('s, 'm, 'p, 'l) seqp, 'm seq_action) transition set"
  for Γ :: "('s, 'm, 'p, 'l) seqp_env"
where
    broadcastT: "((ξ, {l}broadcast(smsg).p),          broadcast (smsg ξ),         (ξ, p))  seqp_sos Γ"
  | groupcastT: "((ξ, {l}groupcast(sips, smsg).p),    groupcast (sips ξ) (smsg ξ), (ξ, p))  seqp_sos Γ"
  | unicastT:   "((ξ, {l}unicast(sip, smsg).p  q),   unicast (sip ξ) (smsg ξ),    (ξ, p))  seqp_sos Γ"
  | notunicastT:"((ξ, {l}unicast(sip, smsg).p  q),    ¬unicast (sip ξ),          (ξ, q))  seqp_sos Γ"
  | sendT:      "((ξ, {l}send(smsg).p),               send (smsg ξ),              (ξ, p))  seqp_sos Γ"
  | deliverT:   "((ξ, {l}deliver(sdata).p),           deliver (sdata ξ),          (ξ, p))  seqp_sos Γ"
  | receiveT:   "((ξ, {l}receive(umsg).p),            receive msg,       (umsg msg ξ, p))  seqp_sos Γ"
  | assignT:    "((ξ, {l}u p),                      τ,                        (u ξ, p))  seqp_sos Γ"

  | callT:      " ((ξ, Γ pn), a, (ξ', p'))  seqp_sos Γ  
                 ((ξ, call(pn)), a, (ξ', p'))  seqp_sos Γ" (* TPB: quite different to Table 1 *)

  | choiceT1:   "((ξ, p), a, (ξ', p'))  seqp_sos Γ   ((ξ, p  q), a, (ξ', p'))  seqp_sos Γ"
  | choiceT2:   "((ξ, q), a, (ξ', q'))  seqp_sos Γ   ((ξ, p  q), a, (ξ', q'))  seqp_sos Γ"

  | guardT:     "ξ'  g ξ  ((ξ, {l}g p), τ, (ξ', p))  seqp_sos Γ"

inductive_cases
      seqp_callTE [elim]:      "((ξ, call(pn)), a, (ξ', q))  seqp_sos Γ"
  and seqp_choiceTE [elim]:    "((ξ, p1  p2), a, (ξ', q))  seqp_sos Γ"

lemma seqp_broadcastTE [elim]:
  "((ξ, {l}broadcast(smsg). p), a, (ξ', q))  seqp_sos Γ;
    a = broadcast (smsg ξ); ξ' = ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}broadcast(smsg). p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_groupcastTE [elim]:
  "((ξ, {l}groupcast(sips, smsg). p), a, (ξ', q))  seqp_sos Γ;
    a = groupcast (sips ξ) (smsg ξ); ξ' = ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}groupcast(sips, smsg). p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_unicastTE [elim]:
  "((ξ, {l}unicast(sip, smsg). p  q), a, (ξ', r))  seqp_sos Γ;
    a = unicast (sip ξ) (smsg ξ); ξ' = ξ; r = p  P;
    a = ¬unicast (sip ξ); ξ' = ξ; r = q  P  P"
  by (ind_cases "((ξ, {l}unicast(sip, smsg). p  q), a, (ξ', r))  seqp_sos Γ") simp_all

lemma seqp_sendTE [elim]:
  "((ξ, {l}send(smsg). p), a, (ξ', q))  seqp_sos Γ;
    a = send (smsg ξ); ξ' = ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}send(smsg). p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_deliverTE [elim]:
  "((ξ, {l}deliver(sdata). p), a, (ξ', q))  seqp_sos Γ;
    a = deliver (sdata ξ); ξ' = ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}deliver(sdata). p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_receiveTE [elim]:
  "((ξ, {l}receive(umsg). p), a, (ξ', q))  seqp_sos Γ;
    msg. a = receive msg; ξ' = umsg msg ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}receive(umsg). p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_assignTE [elim]:
  "((ξ, {l}u p), a, (ξ', q))  seqp_sos Γ; a = τ; ξ' = u ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}u p), a, (ξ', q))  seqp_sos Γ") simp

lemma seqp_guardTE [elim]:
  "((ξ, {l}g p), a, (ξ', q))  seqp_sos Γ; a = τ; ξ'  g ξ; q = p  P  P"
  by (ind_cases "((ξ, {l}g p), a, (ξ', q))  seqp_sos Γ") simp

lemmas seqpTEs =
  seqp_broadcastTE
  seqp_groupcastTE
  seqp_unicastTE
  seqp_sendTE
  seqp_deliverTE
  seqp_receiveTE
  seqp_assignTE
  seqp_callTE
  seqp_choiceTE
  seqp_guardTE

declare seqp_sos.intros [intro]

subsection "Table 2: Structural operational semantics for parallel process expressions "

inductive_set
  parp_sos :: "('s1, 'm seq_action) transition set
                     ('s2, 'm seq_action) transition set
                     ('s1 × 's2, 'm seq_action) transition set"
  for S :: "('s1, 'm seq_action) transition set"
  and T :: "('s2, 'm seq_action) transition set"
where
    parleft:  " (s, a, s')  S; m. a  receive m   ((s, t), a, (s', t))  parp_sos S T"
  | parright: " (t, a, t')  T; m. a  send m   ((s, t), a, (s, t'))  parp_sos S T"
  | parboth:  " (s, receive m, s')  S; (t, send m, t')  T 
               ((s, t), τ, (s', t'))  parp_sos S T"

lemma par_broadcastTE [elim]:
  "((s, t), broadcast m, (s', t'))  parp_sos S T;
    (s, broadcast m, s')  S; t' = t  P;
    (t, broadcast m, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), broadcast m, (s', t'))  parp_sos S T") simp_all

lemma par_groupcastTE [elim]:
  "((s, t), groupcast ips m, (s', t'))  parp_sos S T;
    (s, groupcast ips m, s')  S; t' = t  P;
    (t, groupcast ips m, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), groupcast ips m, (s', t'))  parp_sos S T") simp_all

lemma par_unicastTE [elim]:
  "((s, t), unicast i m, (s', t'))  parp_sos S T;
    (s, unicast i m, s')  S; t' = t  P;
    (t, unicast i m, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), unicast i m, (s', t'))  parp_sos S T") simp_all

lemma par_notunicastTE [elim]:
  "((s, t), notunicast i, (s', t'))  parp_sos S T;
    (s, notunicast i, s')  S; t' = t  P;
    (t, notunicast i, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), notunicast i, (s', t'))  parp_sos S T") simp_all

lemma par_sendTE [elim]:
  "((s, t), send m, (s', t'))  parp_sos S T;
    (s, send m, s')  S; t' = t  P  P"
  by (ind_cases "((s, t), send m, (s', t'))  parp_sos S T") auto

lemma par_deliverTE [elim]:
  "((s, t), deliver d, (s', t'))  parp_sos S T;
    (s, deliver d, s')  S; t' = t  P;
    (t, deliver d, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), deliver d, (s', t'))  parp_sos S T") simp_all

lemma par_receiveTE [elim]:
  "((s, t), receive m, (s', t'))  parp_sos S T;
    (t, receive m, t')  T; s' = s  P  P"
  by (ind_cases "((s, t), receive m, (s', t'))  parp_sos S T") auto

inductive_cases par_tauTE: "((s, t), τ, (s', t'))  parp_sos S T"

lemmas parpTEs =
  par_broadcastTE
  par_groupcastTE
  par_unicastTE
  par_notunicastTE
  par_sendTE
  par_deliverTE
  par_receiveTE

lemma parp_sos_cases [elim]:
  assumes "((s, t), a, (s', t'))  parp_sos S T"
      and " (s, a, s')  S; m. a  receive m; t' = t   P"
      and " (t, a, t')  T; m. a  send m; s' = s   P"
      and "m.  (s, receive m, s')  S; (t, send m, t')  T   P"
    shows "P"
  using assms by cases auto

definition
  par_comp :: "('s1, 'm seq_action) automaton
               ('s2, 'm seq_action) automaton
               ('s1 × 's2, 'm seq_action) automaton"
  ("(_ ⟨⟨ _)" [102, 103] 102)
where
  "s ⟨⟨ t   init = init s × init t, trans = parp_sos (trans s) (trans t) "

lemma trans_par_comp [simp]:
  "trans (s ⟨⟨ t) = parp_sos (trans s) (trans t)"
  unfolding par_comp_def by simp

lemma init_par_comp [simp]:
  "init (s ⟨⟨ t) = init s × init t"
  unfolding par_comp_def by simp

subsection "Table 3: Structural operational semantics for node expressions "

inductive_set
  node_sos :: "('s, 'm seq_action) transition set  ('s net_state, 'm node_action) transition set"
  for S :: "('s, 'm seq_action) transition set"
where
    node_bcast:
    "(s, broadcast m, s')  S  (NodeS i s R, R:*cast(m), NodeS i s' R)  node_sos S"
  | node_gcast:
    "(s, groupcast D m, s')  S  (NodeS i s R, (RD):*cast(m), NodeS i s' R)  node_sos S"
  | node_ucast:
    " (s, unicast d m, s')  S; dR   (NodeS i s R, {d}:*cast(m), NodeS i s' R)  node_sos S"
  | node_notucast:
    " (s, ¬unicast d, s')  S; dR   (NodeS i s R, τ, NodeS i s' R)  node_sos S"
  | node_deliver:
    "(s, deliver d, s')  S  (NodeS i s R, i:deliver(d), NodeS i s' R)  node_sos S"
  | node_receive:
    "(s, receive m, s')  S  (NodeS i s R, {i}¬{}:arrive(m), NodeS i s' R)  node_sos S"
  | node_tau:
    "(s, τ, s')  S          (NodeS i s R, τ, NodeS i s' R)  node_sos S"
  | node_arrive:
    "(NodeS i s R, {}¬{i}:arrive(m),  NodeS i s R)  node_sos S"
  | node_connect1:
    "(NodeS i s R, connect(i, i'),    NodeS i s (R  {i'}))  node_sos S"
  | node_connect2:
    "(NodeS i s R, connect(i', i),    NodeS i s (R  {i'}))  node_sos S"
  | node_disconnect1:
    "(NodeS i s R, disconnect(i, i'), NodeS i s (R - {i'}))  node_sos S"
  | node_disconnect2:
    "(NodeS i s R, disconnect(i', i), NodeS i s (R - {i'}))  node_sos S"
  | node_connect_other:
    " i  i'; i  i''   (NodeS i s R, connect(i', i''), NodeS i s R)  node_sos S"
  | node_disconnect_other:
    " i  i'; i  i''   (NodeS i s R, disconnect(i', i''), NodeS i s R)  node_sos S"

inductive_cases node_arriveTE:  "(NodeS i s R, ii¬ni:arrive(m), NodeS i s' R)  node_sos S"
            and node_arriveTE': "(NodeS i s R, H¬K:arrive(m), s')  node_sos S"
            and node_castTE:    "(NodeS i s R, RM:*cast(m), NodeS i s' R')  node_sos S"
            and node_castTE':   "(NodeS i s R, RM:*cast(m), s')  node_sos S"
            and node_deliverTE: "(NodeS i s R, i:deliver(d), NodeS i s' R)  node_sos S"
            and node_deliverTE': "(s, i:deliver(d), s')  node_sos S"
            and node_deliverTE'': "(NodeS ii s R, i:deliver(d), s')  node_sos S"
            and node_tauTE:     "(NodeS i s R, τ, NodeS i s' R)  node_sos S"
            and node_tauTE':    "(NodeS i s R, τ, s')  node_sos S"
            and node_connectTE: "(NodeS ii s R, connect(i, i'), NodeS ii s' R')  node_sos S"
            and node_connectTE': "(NodeS ii s R, connect(i, i'), s')  node_sos S"
            and node_disconnectTE: "(NodeS ii s R, disconnect(i, i'), NodeS ii s' R')  node_sos S"
            and node_disconnectTE': "(NodeS ii s R, disconnect(i, i'), s')  node_sos S"

lemma node_sos_never_newpkt [simp]:
  assumes "(s, a, s')  node_sos S"
    shows "a  i:newpkt(d, di)"
  using assms by cases auto

lemma arrives_or_not:
  assumes "(NodeS i s R, ii¬ni:arrive(m), NodeS i' s' R')  node_sos S"
    shows "(ii = {i}  ni = {})  (ii = {}  ni = {i})"
  using assms by rule simp_all

definition
  node_comp :: "ip  ('s, 'm seq_action) automaton  ip set
                    ('s net_state, 'm node_action) automaton"
    ("(_ : (_) : _)" [0, 0, 0] 104)
where
  "i : np : Ri   init = {NodeS i s Ri|s. s  init np}, trans = node_sos (trans np) "

lemma trans_node_comp:
  "trans (i : np : Ri) = node_sos (trans np)"
  unfolding node_comp_def by simp

lemma init_node_comp:
  "init (i : np : Ri) = {NodeS i s Ri|s. s  init np}"
  unfolding node_comp_def by simp

lemmas node_comps = trans_node_comp init_node_comp

lemma trans_par_node_comp [simp]:
  "trans (i : s ⟨⟨ t : R) = node_sos (parp_sos (trans s) (trans t))"
  unfolding node_comp_def by simp

lemma snd_par_node_comp [simp]:
  "init (i : s ⟨⟨ t : R) = {NodeS i st R|st. st  init s × init t}"
  unfolding node_comp_def by simp

lemma node_sos_dest_is_net_state:
  assumes "(s, a, s')  node_sos S"
    shows "i' P' R'. s' = NodeS i' P' R'"
  using assms by induct auto

lemma node_sos_dest:
  assumes "(NodeS i p R, a, s')  node_sos S"
    shows "P' R'. s' = NodeS i P' R'"
  using assms assms [THEN node_sos_dest_is_net_state]
  by - (erule node_sos.cases, auto)

lemma node_sos_states [elim]:
  assumes "(ns, a, ns')  node_sos S"
  obtains i s R s' R' where "ns  = NodeS i s  R"
                        and "ns' = NodeS i s' R'"
  proof -
    assume [intro!]: "i s R s' R'. ns = NodeS i s R  ns' = NodeS i s' R'  thesis"
    from assms(1) obtain i s R where "ns = NodeS i s R"
      by (cases ns) auto
    moreover with assms(1) obtain s' R' where "ns' = NodeS i s' R'"
      by (metis node_sos_dest)
    ultimately show thesis ..
  qed

lemma node_sos_cases [elim]:
  "(NodeS i p R, a, NodeS i p' R')  node_sos S 
  (m .        a = R:*cast(m);          R' = R; (p, broadcast m, p')  S   P) 
  (m D.       a = (R  D):*cast(m);    R' = R; (p, groupcast D m, p')  S   P) 
  (d m.       a = {d}:*cast(m);        R' = R; (p, unicast d m, p')  S; d  R   P) 
  (d.         a = τ;                   R' = R; (p, ¬unicast d, p')  S; d  R   P) 
  (d.         a = i:deliver(d);        R' = R; (p, deliver d, p')  S   P) 
  (m.         a = {i}¬{}:arrive(m);    R' = R; (p, receive m, p')  S   P) 
  (             a = τ;                   R' = R; (p, τ, p')  S   P) 
  (m.         a = {}¬{i}:arrive(m);    R' = R; p = p'   P) 
  (i i'.      a = connect(i, i');      R' = R  {i'}; p = p'   P) 
  (i i'.      a = connect(i', i);      R' = R  {i'}; p = p'   P) 
  (i i'.      a = disconnect(i, i');   R' = R - {i'}; p = p'   P) 
  (i i'.      a = disconnect(i', i);   R' = R - {i'}; p = p'   P) 
  (i i' i''.  a = connect(i', i'');    R' = R; p = p'; i  i'; i  i''   P) 
  (i i' i''.  a = disconnect(i', i''); R' = R; p = p'; i  i'; i  i''   P) 
  P"
  by (erule node_sos.cases) simp_all

subsection "Table 4: Structural operational semantics for partial network expressions "

inductive_set
  pnet_sos :: "('s net_state, 'm node_action) transition set
                     ('s net_state, 'm node_action) transition set
                     ('s net_state, 'm node_action) transition set"
  for S :: "('s net_state, 'm node_action) transition set"
  and T :: "('s net_state, 'm node_action) transition set"
where
    pnet_cast1: " (s, R:*cast(m), s')  S; (t, H¬K:arrive(m), t')  T; H  R; K  R = {} 
       (SubnetS s t, R:*cast(m), SubnetS s' t')  pnet_sos S T"

  | pnet_cast2: " (s, H¬K:arrive(m), s')  S; (t, R:*cast(m), t')  T;  H  R; K  R = {} 
       (SubnetS s t, R:*cast(m), SubnetS s' t')  pnet_sos S T"

  | pnet_arrive: " (s, H¬K:arrive(m), s')  S; (t, H'¬K':arrive(m), t')  T 
       (SubnetS s t,  (H  H')¬(K  K'):arrive(m), SubnetS s' t')  pnet_sos S T"

  | pnet_deliver1: "(s, i:deliver(d), s')  S
       (SubnetS s t, i:deliver(d), SubnetS s' t)  pnet_sos S T"
  | pnet_deliver2: " (t, i:deliver(d), t')  T 
       (SubnetS s t, i:deliver(d), SubnetS s t')  pnet_sos S T"

  | pnet_tau1: "(s, τ, s')  S  (SubnetS s t, τ, SubnetS s' t)  pnet_sos S T"
  | pnet_tau2: "(t, τ, t')  T  (SubnetS s t, τ, SubnetS s t')  pnet_sos S T"

  | pnet_connect: " (s, connect(i, i'), s')  S; (t, connect(i, i'), t')  T 
       (SubnetS s t, connect(i, i'), SubnetS s' t')  pnet_sos S T"

  | pnet_disconnect: " (s, disconnect(i, i'), s')  S; (t, disconnect(i, i'), t')  T 
       (SubnetS s t, disconnect(i, i'), SubnetS s' t')  pnet_sos S T"

inductive_cases partial_castTE [elim]:       "(s, R:*cast(m), s')  pnet_sos S T"
            and partial_arriveTE [elim]:     "(s, H¬K:arrive(m), s')  pnet_sos S T"
            and partial_deliverTE [elim]:    "(s, i:deliver(d), s')  pnet_sos S T"
            and partial_tauTE [elim]:        "(s, τ, s')  pnet_sos S T"
            and partial_connectTE [elim]:    "(s, connect(i, i'), s')  pnet_sos S T"
            and partial_disconnectTE [elim]: "(s, disconnect(i, i'), s')  pnet_sos S T"

lemma pnet_sos_never_newpkt:
  assumes "(st, a, st')  pnet_sos S T"
      and "i d di a s s'. (s, a, s')  S  a  i:newpkt(d, di)"
      and "i d di a t t'. (t, a, t')  T  a  i:newpkt(d, di)"
    shows "a  i:newpkt(d, di)"
  using assms(1) by cases (auto dest!: assms(2-3))

fun pnet :: "(ip  ('s, 'm seq_action) automaton)
               net_tree  ('s net_state, 'm node_action) automaton"
where
    "pnet np (i; Ri)  =  i : np i : Ri"
  | "pnet np (p1  p2) =  init = {SubnetS s1 s2 |s1 s2. s1  init (pnet np p1)
                                                       s2  init (pnet np p2)},
                           trans = pnet_sos (trans (pnet np p1)) (trans (pnet np p2)) "

lemma pnet_node_init [elim, simp]:
  assumes "s  init (pnet np i; R)"
    shows "s  { NodeS i s R |s. s  init (np i)}"
  using assms by (simp add: node_comp_def)

lemma pnet_node_init' [elim]:
 assumes "s  init (pnet np i; R)"
 obtains ns where "s = NodeS i ns R"
             and "ns  init (np i)"
   using assms by (auto simp add: node_comp_def)

lemma pnet_node_trans [elim, simp]:
  assumes "(s, a, s')  trans (pnet np i; R)"
    shows "(s, a, s')  node_sos (trans (np i))"
  using assms by (simp add: trans_node_comp)

lemma pnet_never_newpkt':
  assumes "(s, a, s')  trans (pnet np n)"
    shows "i d di. a  i:newpkt(d, di)"
  using assms proof (induction n arbitrary: s a s')
    fix n1 n2 s a s'
    assume IH1: "s a s'. (s, a, s')  trans (pnet np n1)  i d di. a  i:newpkt(d, di)"
       and IH2: "s a s'. (s, a, s')  trans (pnet np n2)  i d di. a  i:newpkt(d, di)"
       and "(s, a, s')  trans (pnet np (n1  n2))"
    show "i d di. a  i:newpkt(d, di)"
    proof (intro allI)
      fix i d di
      from (s, a, s')  trans (pnet np (n1  n2))
        have "(s, a, s')  pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
          by simp
      thus "a  i:newpkt(d, di)"
        by (rule pnet_sos_never_newpkt) (auto dest!: IH1 IH2)
    qed
  qed (simp add: node_comps)

lemma pnet_never_newpkt:
  assumes "(s, a, s')  trans (pnet np n)"
    shows "a  i:newpkt(d, di)"
  proof -
    from assms have "i d di. a  i:newpkt(d, di)"
      by (rule pnet_never_newpkt')
    thus ?thesis by clarsimp
  qed

subsection "Table 5: Structural operational semantics for complete network expressions "

inductive_set
  cnet_sos :: "('s, ('m::msg) node_action) transition set
                     ('s, 'm node_action) transition set"
  for S :: "('s, 'm node_action) transition set"
where
    cnet_connect: "(s, connect(i, i'), s')  S   (s, connect(i, i'), s')  cnet_sos S"
  | cnet_disconnect: "(s, disconnect(i, i'), s')  S   (s, disconnect(i, i'), s')  cnet_sos S"
  | cnet_cast: "(s, R:*cast(m), s')  S   (s, τ, s')  cnet_sos S"
  | cnet_tau: "(s, τ, s')  S   (s, τ, s')  cnet_sos S"
  | cnet_deliver: "(s, i:deliver(d), s')  S   (s, i:deliver(d), s')  cnet_sos S"
  | cnet_newpkt: "(s, {i}¬K:arrive(newpkt(d, di)), s')  S   (s, i:newpkt(d, di), s')  cnet_sos S"

inductive_cases connect_completeTE: "(s, connect(i, i'), s')  cnet_sos S"
            and disconnect_completeTE: "(s, disconnect(i, i'), s')  cnet_sos S"
            and tau_completeTE: "(s, τ, s')  cnet_sos S"
            and deliver_completeTE: "(s, i:deliver(d), s')  cnet_sos S"
            and newpkt_completeTE: "(s, i:newpkt(d, di), s')  cnet_sos S"

lemmas completeTEs = connect_completeTE
                     disconnect_completeTE
                     tau_completeTE
                     deliver_completeTE
                     newpkt_completeTE

lemma complete_no_cast [simp]:
  "(s, R:*cast(m), s')  cnet_sos T"
  proof
    assume "(s, R:*cast(m), s')  cnet_sos T"
    hence "R:*cast(m)  R:*cast(m)"
     by (rule cnet_sos.cases) auto
    thus False by simp
  qed

lemma complete_no_arrive [simp]:
  "(s, ii¬ni:arrive(m), s')  cnet_sos T"
  proof
    assume "(s, ii¬ni:arrive(m), s')  cnet_sos T"
    hence "ii¬ni:arrive(m)  ii¬ni:arrive(m)"
     by (rule cnet_sos.cases) auto
    thus False by simp
  qed

abbreviation
  closed :: "('s net_state, ('m::msg) node_action) automaton  ('s net_state, 'm node_action) automaton"
where
  "closed  (λA. A  trans := cnet_sos (trans A) )"

end