--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Channels.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,61 @@
+Channels = IOA + Action + Multiset + "Lemmas" + Packet +
+
+consts
+
+srch_asig,
+rsch_asig :: "'m action signature"
+
+srch_trans :: "('m action, 'm packet multiset)transition set"
+rsch_trans :: "('m action, bool multiset)transition set"
+
+srch_ioa :: "('m action, 'm packet multiset)ioa"
+rsch_ioa :: "('m action, bool multiset)ioa"
+
+rules
+
+srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \
+\ UN pkt. {R_pkt(pkt)}, \
+\ {}>"
+
+rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \
+\ UN b. {R_ack(b)}, \
+\ {}>"
+
+srch_trans_def "srch_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in \
+\ case fst(snd(tr)) \
+\ of S_msg(m) => False | \
+\ R_msg(m) => False | \
+\ S_pkt(pkt) => t = addm(s, pkt) | \
+\ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | \
+\ S_ack(b) => False | \
+\ R_ack(b) => False | \
+\ C_m_s => False | \
+\ C_m_r => False | \
+\ C_r_s => False | \
+\ C_r_r(m) => False}"
+
+rsch_trans_def "rsch_trans == \
+\ {tr. let s = fst(tr); \
+\ t = snd(snd(tr)) \
+\ in \
+\ case fst(snd(tr)) \
+\ of \
+\ S_msg(m) => False | \
+\ R_msg(m) => False | \
+\ S_pkt(pkt) => False | \
+\ R_pkt(pkt) => False | \
+\ S_ack(b) => t = addm(s,b) | \
+\ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | \
+\ C_m_s => False | \
+\ C_m_r => False | \
+\ C_r_s => False | \
+\ C_r_r(m) => False}"
+
+
+srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
+rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>"
+
+end