(* Title: HOL/IOA/example/Channels.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
The (faulty) transmission channels (both directions)
*)
Channels = IOA + Action + Multiset +
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"
defs
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