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