(* Title: HOL/IOA/NTP/Abschannel.thy
ID: $Id$
Author: Tobias Nipkow and Olaf Mueller
Copyright 1994 TU Muenchen
The (faulty) transmission channel (both directions)
*)
Abschannel = IOA + Action + Multiset +
datatype ('a)act = S('a) | R('a)
consts
ch_asig :: "'a act signature"
ch_trans :: "('a act, 'a multiset)transition set"
ch_ioa :: "('a act, 'a multiset)ioa"
rsch_actions :: "'m action => bool act option"
srch_actions :: "'m action =>(bool * 'm) act option"
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"
defs
srch_asig_def "srch_asig == asig_of(srch_ioa)"
rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
srch_trans_def "srch_trans == trans_of(srch_ioa)"
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
ch_trans_def "ch_trans == \
\ {tr. let s = fst(tr); \
\ t = snd(snd(tr)) \
\ in \
\ case fst(snd(tr)) \
\ of S(b) => t = addm s b | \
\ R(b) => count s b ~= 0 & t = delm s b}"
ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
rsch_actions_def "rsch_actions (act) == \
\ case act of \
\ S_msg(m) => None | \
\ R_msg(m) => None | \
\ S_pkt(packet) => None | \
\ R_pkt(packet) => None | \
\ S_ack(b) => Some(S(b)) | \
\ R_ack(b) => Some(R(b)) | \
\ C_m_s => None | \
\ C_m_r => None | \
\ C_r_s => None | \
\ C_r_r(m) => None"
srch_actions_def "srch_actions (act) == \
\ case act of \
\ S_msg(m) => None | \
\ R_msg(m) => None | \
\ S_pkt(p) => Some(S(p)) | \
\ R_pkt(p) => Some(R(p)) | \
\ S_ack(b) => None | \
\ R_ack(b) => None | \
\ C_m_s => None | \
\ C_m_r => None | \
\ C_r_s => None | \
\ C_r_r(m) => None"
end