Theory OAWN_SOS
section "Open semantics of the Algebra of Wireless Networks"
theory OAWN_SOS
imports TransitionSystems AWN
begin
text ‹
These are variants of the SOS rules that work against a mixed global/local context, where
the global context is represented by a function @{term σ} mapping ip addresses to states.
›
subsection "Open structural operational semantics for sequential process expressions "
inductive_set
oseqp_sos
:: "('s, 'm, 'p, 'l) seqp_env ⇒ ip
⇒ ((ip ⇒ 's) × ('s, 'm, 'p, 'l) seqp, 'm seq_action) transition set"
for Γ :: "('s, 'm, 'p, 'l) seqp_env"
and i :: ip
where
obroadcastT: "σ' i = σ i ⟹
((σ, {l}broadcast(s⇩m⇩s⇩g).p), broadcast (s⇩m⇩s⇩g (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
| ogroupcastT: "σ' i = σ i ⟹
((σ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g).p), groupcast (s⇩i⇩p⇩s (σ i)) (s⇩m⇩s⇩g (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
| ounicastT: "σ' i = σ i ⟹
((σ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q), unicast (s⇩i⇩p (σ i)) (s⇩m⇩s⇩g (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
| onotunicastT:"σ' i = σ i ⟹
((σ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q), ¬unicast (s⇩i⇩p (σ i)), (σ', q)) ∈ oseqp_sos Γ i"
| osendT: "σ' i = σ i ⟹
((σ, {l}send(s⇩m⇩s⇩g).p), send (s⇩m⇩s⇩g (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
| odeliverT: "σ' i = σ i ⟹
((σ, {l}deliver(s⇩d⇩a⇩t⇩a).p), deliver (s⇩d⇩a⇩t⇩a (σ i)), (σ', p)) ∈ oseqp_sos Γ i"
| oreceiveT: "σ' i = u⇩m⇩s⇩g msg (σ i) ⟹
((σ, {l}receive(u⇩m⇩s⇩g).p), receive msg, (σ', p)) ∈ oseqp_sos Γ i"
| oassignT: "σ' i = u (σ i) ⟹
((σ, {l}⟦u⟧ p), τ, (σ', p)) ∈ oseqp_sos Γ i"
| ocallT: "((σ, Γ pn), a, (σ', p')) ∈ oseqp_sos Γ i ⟹
((σ, call(pn)), a, (σ', p')) ∈ oseqp_sos Γ i"
| ochoiceT1: "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i ⟹
((σ, p ⊕ q), a, (σ', p')) ∈ oseqp_sos Γ i"
| ochoiceT2: "((σ, q), a, (σ', q')) ∈ oseqp_sos Γ i ⟹
((σ, p ⊕ q), a, (σ', q')) ∈ oseqp_sos Γ i"
| oguardT: "σ' i ∈ g (σ i) ⟹ ((σ, {l}⟨g⟩ p), τ, (σ', p)) ∈ oseqp_sos Γ i"
inductive_cases
oseq_callTE [elim]: "((σ, call(pn)), a, (σ', q)) ∈ oseqp_sos Γ i"
and oseq_choiceTE [elim]: "((σ, p1 ⊕ p2), a, (σ', q)) ∈ oseqp_sos Γ i"
lemma oseq_broadcastTE [elim]:
"⟦((σ, {l}broadcast(s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i;
⟦a = broadcast (s⇩m⇩s⇩g (σ i)); σ' i = σ i; q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}broadcast(s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_groupcastTE [elim]:
"⟦((σ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i;
⟦a = groupcast (s⇩i⇩p⇩s (σ i)) (s⇩m⇩s⇩g (σ i)); σ' i = σ i; q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_unicastTE [elim]:
"⟦((σ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q), a, (σ', r)) ∈ oseqp_sos Γ i;
⟦a = unicast (s⇩i⇩p (σ i)) (s⇩m⇩s⇩g (σ i)); σ' i = σ i; r = p⟧ ⟹ P;
⟦a = ¬unicast (s⇩i⇩p (σ i)); σ' i = σ i; r = q⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q), a, (σ', r)) ∈ oseqp_sos Γ i") simp_all
lemma oseq_sendTE [elim]:
"⟦((σ, {l}send(s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i;
⟦a = send (s⇩m⇩s⇩g (σ i)); σ' i = σ i; q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}send(s⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_deliverTE [elim]:
"⟦((σ, {l}deliver(s⇩d⇩a⇩t⇩a). p), a, (σ', q)) ∈ oseqp_sos Γ i;
⟦a = deliver (s⇩d⇩a⇩t⇩a (σ i)); σ' i = σ i; q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}deliver(s⇩d⇩a⇩t⇩a). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_receiveTE [elim]:
"⟦((σ, {l}receive(u⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i;
⋀msg. ⟦a = receive msg; σ' i = u⇩m⇩s⇩g msg (σ i); q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}receive(u⇩m⇩s⇩g). p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_assignTE [elim]:
"⟦((σ, {l}⟦u⟧ p), a, (σ', q)) ∈ oseqp_sos Γ i; ⟦a = τ; σ' i = u (σ i); q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}⟦u⟧ p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemma oseq_guardTE [elim]:
"⟦((σ, {l}⟨g⟩ p), a, (σ', q)) ∈ oseqp_sos Γ i; ⟦a = τ; σ' i ∈ g (σ i); q = p⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, {l}⟨g⟩ p), a, (σ', q)) ∈ oseqp_sos Γ i") simp
lemmas oseqpTEs =
oseq_broadcastTE
oseq_groupcastTE
oseq_unicastTE
oseq_sendTE
oseq_deliverTE
oseq_receiveTE
oseq_assignTE
oseq_callTE
oseq_choiceTE
oseq_guardTE
declare oseqp_sos.intros [intro]
subsection "Open structural operational semantics for parallel process expressions "
inductive_set
oparp_sos :: "ip
⇒ ((ip ⇒ 's) × 's1, 'm seq_action) transition set
⇒ ('s2, 'm seq_action) transition set
⇒ ((ip ⇒ 's) × ('s1 × 's2), 'm seq_action) transition set"
for i :: ip
and S :: "((ip ⇒ 's) × 's1, 'm seq_action) transition set"
and T :: "('s2, 'm seq_action) transition set"
where
oparleft: "⟦ ((σ, s), a, (σ', s')) ∈ S; ⋀m. a ≠ receive m ⟧ ⟹
((σ, (s, t)), a, (σ', (s', t))) ∈ oparp_sos i S T"
| oparright: "⟦ (t, a, t') ∈ T; ⋀m. a ≠ send m; σ' i = σ i ⟧ ⟹
((σ, (s, t)), a, (σ', (s, t'))) ∈ oparp_sos i S T"
| oparboth: "⟦ ((σ, s), receive m, (σ', s')) ∈ S; (t, send m, t') ∈ T ⟧ ⟹
((σ, (s, t)), τ, (σ', (s', t'))) ∈ oparp_sos i S T"
lemma opar_broadcastTE [elim]:
"⟦((σ, (s, t)), broadcast m, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), broadcast m, (σ', s')) ∈ S; t' = t⟧ ⟹ P;
⟦(t, broadcast m, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), broadcast m, (σ', (s', t'))) ∈ oparp_sos i S T") simp_all
lemma opar_groupcastTE [elim]:
"⟦((σ, (s, t)), groupcast ips m, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), groupcast ips m, (σ', s')) ∈ S; t' = t⟧ ⟹ P;
⟦(t, groupcast ips m, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), groupcast ips m, (σ', (s', t'))) ∈ oparp_sos i S T") simp_all
lemma opar_unicastTE [elim]:
"⟦((σ, (s, t)), unicast i m, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), unicast i m, (σ', s')) ∈ S; t' = t⟧ ⟹ P;
⟦(t, unicast i m, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), unicast i m, (σ', (s', t'))) ∈ oparp_sos i S T") simp_all
lemma opar_notunicastTE [elim]:
"⟦((σ, (s, t)), notunicast i, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), notunicast i, (σ', s')) ∈ S; t' = t⟧ ⟹ P;
⟦(t, notunicast i, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), notunicast i, (σ', (s', t'))) ∈ oparp_sos i S T") simp_all
lemma opar_sendTE [elim]:
"⟦((σ, (s, t)), send m, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), send m, (σ', s')) ∈ S; t' = t⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), send m, (σ', (s', t'))) ∈ oparp_sos i S T") auto
lemma opar_deliverTE [elim]:
"⟦((σ, (s, t)), deliver d, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦((σ, s), deliver d, (σ', s')) ∈ S; t' = t⟧ ⟹ P;
⟦(t, deliver d, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), deliver d, (σ', (s', t'))) ∈ oparp_sos i S T") simp_all
lemma opar_receiveTE [elim]:
"⟦((σ, (s, t)), receive m, (σ', (s', t'))) ∈ oparp_sos i S T;
⟦(t, receive m, t') ∈ T; s' = s; σ' i = σ i⟧ ⟹ P⟧ ⟹ P"
by (ind_cases "((σ, (s, t)), receive m, (σ', (s', t'))) ∈ oparp_sos i S T") auto
inductive_cases opar_tauTE: "((σ, (s, t)), τ, (σ', (s', t'))) ∈ oparp_sos i S T"
lemmas oparpTEs =
opar_broadcastTE
opar_groupcastTE
opar_unicastTE
opar_notunicastTE
opar_sendTE
opar_deliverTE
opar_receiveTE
lemma oparp_sos_cases [elim]:
assumes "((σ, (s, t)), a, (σ', (s', t'))) ∈ oparp_sos i 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; σ' i = σ i ⟧ ⟹ P"
and "⋀m. ⟦ a = τ; ((σ, s), receive m, (σ', s')) ∈ S; (t, send m, t') ∈ T ⟧ ⟹ P"
shows "P"
using assms by cases auto
definition extg :: "('a × 'b) × 'c ⇒ 'a × 'b × 'c"
where "extg ≡ λ((σ, l1), l2). (σ, (l1, l2))"
lemma extgsimp [simp]:
"extg ((σ, l1), l2) = (σ, (l1, l2))"
unfolding extg_def by simp
lemma extg_range_prod: "extg ` (i1 × i2) = {(σ, (s1, s2))|σ s1 s2. (σ, s1) ∈ i1 ∧ s2 ∈ i2}"
unfolding image_def extg_def
by (rule Collect_cong) (auto split: prod.split)
definition
opar_comp :: "((ip ⇒ 's) × 's1, 'm seq_action) automaton
⇒ ip
⇒ ('s2, 'm seq_action) automaton
⇒ ((ip ⇒ 's) × 's1 × 's2, 'm seq_action) automaton"
(‹(_ ⟨⟨⇘_⇙ _)› [102, 0, 103] 102)
where
"s ⟨⟨⇘i⇙ t ≡ ⦇ init = extg ` (init s × init t), trans = oparp_sos i (trans s) (trans t) ⦈"
lemma opar_comp_def':
"s ⟨⟨⇘i⇙ t = ⦇ init = {(σ, (s⇩l, t⇩l))|σ s⇩l t⇩l. (σ, s⇩l) ∈ init s ∧ t⇩l ∈ init t},
trans = oparp_sos i (trans s) (trans t) ⦈"
unfolding opar_comp_def extg_def image_def by (auto split: prod.split)
lemma trans_opar_comp [simp]:
"trans (s ⟨⟨⇘i⇙ t) = oparp_sos i (trans s) (trans t)"
unfolding opar_comp_def by simp
lemma init_opar_comp [simp]:
"init (s ⟨⟨⇘i⇙ t) = extg ` (init s × init t)"
unfolding opar_comp_def by simp
subsection "Open structural operational semantics for node expressions "
inductive_set
onode_sos :: "((ip ⇒ 's) × 'l, 'm seq_action) transition set
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
for S :: "((ip ⇒ 's) × 'l, 'm seq_action) transition set"
where
onode_bcast:
"((σ, s), broadcast m, (σ', s')) ∈ S ⟹ ((σ, NodeS i s R), R:*cast(m), (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_gcast:
"((σ, s), groupcast D m, (σ', s')) ∈ S ⟹ ((σ, NodeS i s R), (R∩D):*cast(m), (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_ucast:
"⟦ ((σ, s), unicast d m, (σ', s')) ∈ S; d∈R ⟧ ⟹ ((σ, NodeS i s R), {d}:*cast(m), (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_notucast: "⟦ ((σ, s), ¬unicast d, (σ', s')) ∈ S; d∉R; ∀j. j≠i ⟶ σ' j = σ j ⟧
⟹ ((σ, NodeS i s R), τ, (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_deliver: "⟦ ((σ, s), deliver d, (σ', s')) ∈ S; ∀j. j≠i ⟶ σ' j = σ j ⟧
⟹ ((σ, NodeS i s R), i:deliver(d), (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_tau: "⟦ ((σ, s), τ, (σ', s')) ∈ S; ∀j. j≠i ⟶ σ' j = σ j ⟧
⟹ ((σ, NodeS i s R), τ, (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_receive:
"((σ, s), receive m, (σ', s')) ∈ S ⟹ ((σ, NodeS i s R), {i}¬{}:arrive(m), (σ', NodeS i s' R)) ∈ onode_sos S"
| onode_arrive:
"σ' i = σ i ⟹ ((σ, NodeS i s R), {}¬{i}:arrive(m), (σ', NodeS i s R)) ∈ onode_sos S"
| onode_connect1:
"σ' i = σ i ⟹ ((σ, NodeS i s R), connect(i, i'), (σ', NodeS i s (R ∪ {i'}))) ∈ onode_sos S"
| onode_connect2:
"σ' i = σ i ⟹ ((σ, NodeS i s R), connect(i', i), (σ', NodeS i s (R ∪ {i'}))) ∈ onode_sos S"
| onode_disconnect1:
"σ' i = σ i ⟹ ((σ, NodeS i s R), disconnect(i, i'), (σ', NodeS i s (R - {i'}))) ∈ onode_sos S"
| onode_disconnect2:
"σ' i = σ i ⟹ ((σ, NodeS i s R), disconnect(i', i), (σ', NodeS i s (R - {i'}))) ∈ onode_sos S"
| onode_connect_other:
"⟦ i ≠ i'; i ≠ i''; σ' i = σ i ⟧ ⟹ ((σ, NodeS i s R), connect(i', i''), (σ', NodeS i s R)) ∈ onode_sos S"
| onode_disconnect_other:
"⟦ i ≠ i'; i ≠ i''; σ' i = σ i ⟧ ⟹ ((σ, NodeS i s R), disconnect(i', i''), (σ', NodeS i s R)) ∈ onode_sos S"
inductive_cases
onode_arriveTE [elim]: "((σ, NodeS i s R), ii¬ni:arrive(m), (σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_castTE [elim]: "((σ, NodeS i s R), RR:*cast(m), (σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_deliverTE [elim]: "((σ, NodeS i s R), ii:deliver(d), (σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_connectTE [elim]: "((σ, NodeS i s R), connect(ii, ii'), (σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_disconnectTE [elim]: "((σ, NodeS i s R), disconnect(ii, ii'),(σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_newpktTE [elim]: "((σ, NodeS i s R), ii:newpkt(d, di), (σ', NodeS i' s' R')) ∈ onode_sos S"
and onode_tauTE [elim]: "((σ, NodeS i s R), τ, (σ', NodeS i' s' R')) ∈ onode_sos S"
lemma oarrives_or_not:
assumes "((σ, NodeS i s R), ii¬ni:arrive(m), (σ', NodeS i' s' R')) ∈ onode_sos S"
shows "(ii = {i} ∧ ni = {}) ∨ (ii = {} ∧ ni = {i})"
using assms by rule simp_all
definition
onode_comp :: "ip
⇒ ((ip ⇒ 's) × 'l, 'm seq_action) automaton
⇒ ip set
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) automaton"
(‹(⟨_ : (_) : _⟩⇩o)› [0, 0, 0] 104)
where
"⟨i : onp : R⇩i⟩⇩o ≡ ⦇ init = {(σ, NodeS i s R⇩i)|σ s. (σ, s) ∈ init onp},
trans = onode_sos (trans onp) ⦈"
lemma trans_onode_comp:
"trans (⟨i : S : R⟩⇩o) = onode_sos (trans S)"
unfolding onode_comp_def by simp
lemma init_onode_comp:
"init (⟨i : S : R⟩⇩o) = {(σ, NodeS i s R)|σ s. (σ, s) ∈ init S}"
unfolding onode_comp_def by simp
lemmas onode_comps = trans_onode_comp init_onode_comp
lemma fst_par_onode_comp [simp]:
"trans (⟨i : s ⟨⟨⇘I⇙ t : R⟩⇩o) = onode_sos (oparp_sos I (trans s) (trans t))"
unfolding onode_comp_def by simp
lemma init_par_onode_comp [simp]:
"init (⟨i : s ⟨⟨⇘I⇙ t : R⟩⇩o) = {(σ, NodeS i (s1, s2) R)|σ s1 s2. ((σ, s1), s2) ∈ init s × init t}"
unfolding onode_comp_def by (simp add: extg_range_prod)
lemma onode_sos_dest_is_net_state:
assumes "((σ, p), a, s') ∈ onode_sos S"
shows "∃σ' i' ζ' R'. s' = (σ', NodeS i' ζ' R')"
using assms proof -
assume "((σ, p), a, s') ∈ onode_sos S"
then obtain σ' i' ζ' R' where "s' = (σ', NodeS i' ζ' R')"
by (cases s') (auto elim!: onode_sos.cases)
thus ?thesis by simp
qed
lemma onode_sos_dest_is_net_state':
assumes "((σ, NodeS i p R), a, s') ∈ onode_sos S"
shows "∃σ' ζ' R'. s' = (σ', NodeS i ζ' R')"
using assms proof -
assume "((σ, NodeS i p R), a, s') ∈ onode_sos S"
then obtain σ' ζ' R' where "s' = (σ', NodeS i ζ' R')"
by (cases s') (auto elim!: onode_sos.cases)
thus ?thesis by simp
qed
lemma onode_sos_dest_is_net_state'':
assumes "((σ, NodeS i p R), a, (σ', s')) ∈ onode_sos S"
shows "∃ζ' R'. s' = NodeS i ζ' R'"
proof -
define ns' where "ns' = (σ', s')"
with assms have "((σ, NodeS i p R), a, ns') ∈ onode_sos S" by simp
then obtain σ'' ζ' R' where "ns' = (σ'', NodeS i ζ' R')"
by (metis onode_sos_dest_is_net_state')
hence "s' = NodeS i ζ' R'" by (simp add: ns'_def)
thus ?thesis by simp
qed
lemma onode_sos_src_is_net_state:
assumes "((σ, p), a, s') ∈ onode_sos S"
shows "∃i ζ R. p = NodeS i ζ R"
using assms proof -
assume "((σ, p), a, s') ∈ onode_sos S"
then obtain i ζ R where "p = NodeS i ζ R"
by (cases s') (auto elim!: onode_sos.cases)
thus ?thesis by simp
qed
lemma onode_sos_net_states:
assumes "((σ, s), a, (σ', s')) ∈ onode_sos S"
shows "∃i ζ R ζ' R'. s = NodeS i ζ R ∧ s' = NodeS i ζ' R'"
proof -
from assms obtain i ζ R where "s = NodeS i ζ R"
by (metis onode_sos_src_is_net_state)
moreover with assms obtain ζ' R' where "s' = NodeS i ζ' R'"
by (auto dest!: onode_sos_dest_is_net_state')
ultimately show ?thesis by simp
qed
lemma node_sos_cases [elim]:
"((σ, NodeS i p R), a, (σ', NodeS i p' R')) ∈ onode_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'; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i'. ⟦ a = connect(i, i'); R' = R ∪ {i'}; p = p'; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i'. ⟦ a = connect(i', i); R' = R ∪ {i'}; p = p'; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i'. ⟦ a = disconnect(i, i'); R' = R - {i'}; p = p'; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i'. ⟦ a = disconnect(i', i); R' = R - {i'}; p = p'; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i' i''. ⟦ a = connect(i', i''); R' = R; p = p'; i ≠ i'; i ≠ i''; σ' i = σ i ⟧ ⟹ P) ⟹
(⋀i i' i''. ⟦ a = disconnect(i', i''); R' = R; p = p'; i ≠ i'; i ≠ i''; σ' i = σ i ⟧ ⟹ P) ⟹
P"
by (erule onode_sos.cases) (simp | metis)+
subsection "Open structural operational semantics for partial network expressions "
inductive_set
opnet_sos :: "((ip ⇒ 's) × 'l net_state, 'm node_action) transition set
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) transition set
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
for S :: "((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
and T :: "((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
where
opnet_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')) ∈ opnet_sos S T"
| opnet_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')) ∈ opnet_sos S T"
| opnet_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')) ∈ opnet_sos S T"
| opnet_deliver1:
"((σ, s), i:deliver(d), (σ', s')) ∈ S
⟹ ((σ, SubnetS s t), i:deliver(d), (σ', SubnetS s' t)) ∈ opnet_sos S T"
| opnet_deliver2:
"⟦ ((σ, t), i:deliver(d), (σ', t')) ∈ T ⟧
⟹ ((σ, SubnetS s t), i:deliver(d), (σ', SubnetS s t')) ∈ opnet_sos S T"
| opnet_tau1:
"((σ, s), τ, (σ', s')) ∈ S ⟹ ((σ, SubnetS s t), τ, (σ', SubnetS s' t)) ∈ opnet_sos S T"
| opnet_tau2:
"((σ, t), τ, (σ', t')) ∈ T ⟹ ((σ, SubnetS s t), τ, (σ', SubnetS s t')) ∈ opnet_sos S T"
| opnet_connect:
"⟦ ((σ, s), connect(i, i'), (σ', s')) ∈ S; ((σ, t), connect(i, i'), (σ', t')) ∈ T ⟧
⟹ ((σ, SubnetS s t), connect(i, i'), (σ', SubnetS s' t')) ∈ opnet_sos S T"
| opnet_disconnect:
"⟦ ((σ, s), disconnect(i, i'), (σ', s')) ∈ S; ((σ, t), disconnect(i, i'), (σ', t')) ∈ T ⟧
⟹ ((σ, SubnetS s t), disconnect(i, i'), (σ', SubnetS s' t')) ∈ opnet_sos S T"
inductive_cases opartial_castTE [elim]: "((σ, s), R:*cast(m), (σ', s')) ∈ opnet_sos S T"
and opartial_arriveTE [elim]: "((σ, s), H¬K:arrive(m), (σ', s')) ∈ opnet_sos S T"
and opartial_deliverTE [elim]: "((σ, s), i:deliver(d), (σ', s')) ∈ opnet_sos S T"
and opartial_tauTE [elim]: "((σ, s), τ, (σ', s')) ∈ opnet_sos S T"
and opartial_connectTE [elim]: "((σ, s), connect(i, i'), (σ', s')) ∈ opnet_sos S T"
and opartial_disconnectTE [elim]: "((σ, s), disconnect(i, i'), (σ', s')) ∈ opnet_sos S T"
and opartial_newpktTE [elim]: "((σ, s), i:newpkt(d, di), (σ', s')) ∈ opnet_sos S T"
fun opnet :: "(ip ⇒ ((ip ⇒ 's) × 'l, 'm seq_action) automaton)
⇒ net_tree ⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) automaton"
where
"opnet onp (⟨i; R⇩i⟩) = ⟨i : onp i : R⇩i⟩⇩o"
| "opnet onp (p⇩1 ∥ p⇩2) = ⦇ init = {(σ, SubnetS s⇩1 s⇩2) |σ s⇩1 s⇩2.
(σ, s⇩1) ∈ init (opnet onp p⇩1)
∧ (σ, s⇩2) ∈ init (opnet onp p⇩2)
∧ net_ips s⇩1 ∩ net_ips s⇩2 = {}},
trans = opnet_sos (trans (opnet onp p⇩1)) (trans (opnet onp p⇩2)) ⦈"
lemma opnet_node_init [elim, simp]:
assumes "(σ, s) ∈ init (opnet onp ⟨i; R⟩)"
shows "(σ, s) ∈ { (σ, NodeS i ns R) |σ ns. (σ, ns) ∈ init (onp i)}"
using assms by (simp add: onode_comp_def)
lemma opnet_node_init' [elim]:
assumes "(σ, s) ∈ init (opnet onp ⟨i; R⟩)"
obtains ns where "s = NodeS i ns R"
and "(σ, ns) ∈ init (onp i)"
using assms by (auto simp add: onode_comp_def)
lemma opnet_node_trans [elim, simp]:
assumes "(s, a, s') ∈ trans (opnet onp ⟨i; R⟩)"
shows "(s, a, s') ∈ onode_sos (trans (onp i))"
using assms by (simp add: trans_onode_comp)
subsection "Open structural operational semantics for complete network expressions "
inductive_set
ocnet_sos :: "((ip ⇒ 's) × 'l net_state, 'm::msg node_action) transition set
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
for S :: "((ip ⇒ 's) × 'l net_state, 'm node_action) transition set"
where
ocnet_connect:
"⟦ ((σ, s), connect(i, i'), (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), connect(i, i'), (σ', s')) ∈ ocnet_sos S"
| ocnet_disconnect:
"⟦ ((σ, s), disconnect(i, i'), (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), disconnect(i, i'), (σ', s')) ∈ ocnet_sos S"
| ocnet_cast:
"⟦ ((σ, s), R:*cast(m), (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), τ, (σ', s')) ∈ ocnet_sos S"
| ocnet_tau:
"⟦ ((σ, s), τ, (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), τ, (σ', s')) ∈ ocnet_sos S"
| ocnet_deliver:
"⟦ ((σ, s), i:deliver(d), (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), i:deliver(d), (σ', s')) ∈ ocnet_sos S"
| ocnet_newpkt:
"⟦ ((σ, s), {i}¬K:arrive(newpkt(d, di)), (σ', s')) ∈ S; ∀j. j ∉ net_ips s ⟶ (σ' j = σ j) ⟧
⟹ ((σ, s), i:newpkt(d, di), (σ', s')) ∈ ocnet_sos S"
inductive_cases oconnect_completeTE: "((σ, s), connect(i, i'), (σ', s')) ∈ ocnet_sos S"
and odisconnect_completeTE: "((σ, s), disconnect(i, i'), (σ', s')) ∈ ocnet_sos S"
and otau_completeTE: "((σ, s), τ, (σ', s')) ∈ ocnet_sos S"
and odeliver_completeTE: "((σ, s), i:deliver(d), (σ', s')) ∈ ocnet_sos S"
and onewpkt_completeTE: "((σ, s), i:newpkt(d, di), (σ', s')) ∈ ocnet_sos S"
lemmas ocompleteTEs = oconnect_completeTE
odisconnect_completeTE
otau_completeTE
odeliver_completeTE
onewpkt_completeTE
lemma ocomplete_no_cast [simp]:
"((σ, s), R:*cast(m), (σ', s')) ∉ ocnet_sos T"
proof
assume "((σ, s), R:*cast(m), (σ', s')) ∈ ocnet_sos T"
hence "R:*cast(m) ≠ R:*cast(m)"
by (rule ocnet_sos.cases) auto
thus False by simp
qed
lemma ocomplete_no_arrive [simp]:
"((σ, s), ii¬ni:arrive(m), (σ', s')) ∉ ocnet_sos T"
proof
assume "((σ, s), ii¬ni:arrive(m), (σ', s')) ∈ ocnet_sos T"
hence "ii¬ni:arrive(m) ≠ ii¬ni:arrive(m)"
by (rule ocnet_sos.cases) auto
thus False by simp
qed
lemma ocomplete_no_change [elim]:
assumes "((σ, s), a, (σ', s')) ∈ ocnet_sos T"
and "j ∉ net_ips s"
shows "σ' j = σ j"
using assms by cases simp_all
lemma ocomplete_transE [elim]:
assumes "((σ, ζ), a, (σ', ζ')) ∈ ocnet_sos (trans (opnet onp n))"
obtains a' where "((σ, ζ), a', (σ', ζ')) ∈ trans (opnet onp n)"
using assms by (cases a) (auto elim!: ocompleteTEs [simplified])
abbreviation
oclosed :: "((ip ⇒ 's) × 'l net_state, ('m::msg) node_action) automaton
⇒ ((ip ⇒ 's) × 'l net_state, 'm node_action) automaton"
where
"oclosed ≡ (λA. A ⦇ trans := ocnet_sos (trans A) ⦈)"
end