| changeset 3522 | a34c20f4bf44 |
| parent 3072 | a31419014be5 |
| child 6468 | a7b1669f5365 |
| 3521:bdc51b4c6050 | 3522:a34c20f4bf44 |
|---|---|
50 R_ack(b) => if b = sbit(s) then |
50 R_ack(b) => if b = sbit(s) then |
51 sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else |
51 sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else |
52 sq(t)=sq(s) & sbit(t)=sbit(s)}" |
52 sq(t)=sq(s) & sbit(t)=sbit(s)}" |
53 |
53 |
54 sender_ioa_def "sender_ioa == |
54 sender_ioa_def "sender_ioa == |
55 (sender_asig, {([],True)}, sender_trans)" |
55 (sender_asig, {([],True)}, sender_trans,{},{})" |
56 |
56 |
57 end |
57 end |