--- a/IOA/example/Receiver.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Receiver.thy Wed Jun 21 15:12:40 1995 +0200
@@ -33,57 +33,57 @@
rbit_def "rbit == fst o snd o snd o snd"
rsending_def "rsending == snd o snd o snd o snd"
-receiver_asig_def "receiver_asig == \
-\ <UN pkt. {R_pkt(pkt)}, \
-\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
-\ insert(C_m_r, UN m. {C_r_r(m)})>"
+receiver_asig_def "receiver_asig ==
+ <UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+ insert(C_m_r, UN m. {C_r_r(m)})>"
-receiver_trans_def "receiver_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ S_msg(m) => False | \
-\ R_msg(m) => rq(s) = (m # rq(t)) & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(t)=rsending(s) | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => rq(t) = rq(s) & \
-\ rsent(t) = rsent(s) & \
-\ rrcvd(t) = addm(rrcvd(s),pkt) & \
-\ rbit(t) = rbit(s) & \
-\ rsending(t) = rsending(s) | \
-\ S_ack(b) => b = rbit(s) & \
-\ rq(t) = rq(s) & \
-\ rsent(t) = addm(rsent(s),rbit(s)) & \
-\ rrcvd(t) = rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(s) & \
-\ rsending(t) | \
-\ R_ack(b) => False | \
-\ C_m_s => False | \
-\ C_m_r => count(rsent(s),~rbit(s)) < countm(rrcvd(s),%y.hdr(y)=rbit(s)) & \
-\ rq(t) = rq(s) & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(s) & \
-\ ~rsending(t) | \
-\ C_r_s => False | \
-\ C_r_r(m) => count(rsent(s),rbit(s)) <= countm(rrcvd(s),%y.hdr(y)=rbit(s)) & \
-\ count(rsent(s),~rbit(s)) < count(rrcvd(s),<rbit(s),m>) & \
-\ rq(t) = rq(s)@[m] & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t) = (~rbit(s)) & \
-\ ~rsending(s) & \
-\ rsending(t)}"
+receiver_trans_def "receiver_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => False |
+ R_msg(m) => rq(s) = (m # rq(t)) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(t)=rsending(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => rq(t) = rq(s) &
+ rsent(t) = rsent(s) &
+ rrcvd(t) = addm(rrcvd(s),pkt) &
+ rbit(t) = rbit(s) &
+ rsending(t) = rsending(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rsent(t) = addm(rsent(s),rbit(s)) &
+ rrcvd(t) = rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ rsending(t) |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => count(rsent(s),~rbit(s)) < countm(rrcvd(s),%y.hdr(y)=rbit(s)) &
+ rq(t) = rq(s) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ ~rsending(t) |
+ C_r_s => False |
+ C_r_r(m) => count(rsent(s),rbit(s)) <= countm(rrcvd(s),%y.hdr(y)=rbit(s)) &
+ count(rsent(s),~rbit(s)) < count(rrcvd(s),<rbit(s),m>) &
+ rq(t) = rq(s)@[m] &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t) = (~rbit(s)) &
+ ~rsending(s) &
+ rsending(t)}"
-receiver_ioa_def "receiver_ioa == \
-\ <receiver_asig, {<[],{|},{|},False,False>}, receiver_trans>"
+receiver_ioa_def "receiver_ioa ==
+ <receiver_asig, {<[],{|},{|},False,False>}, receiver_trans>"
end