Standard declarations
UNIT
colset UNIT = unit;
INT
BOOL
STRING
block
DATA
STRING
colset DATA = STRING;
NO
INT
colset NO = INT;
NOxDATA
NO
DATA
colset NOxDATA = product NO * DATA;
NO
n
k
var n,k : NO;
DATA
d
data
var d, data : DATA;
BOOL
success
var success : BOOL;
val AllPackets =
1`(1,"COL" )++
1`(2,"OUR")++
1`(3,"ED ")++
1`(4,"PET")++
1`(5,"RI ")++
1`(6,"NET");
val AllPackets =
1`(1,"COL" )++
1`(2,"OUR")++
1`(3,"ED ")++
1`(4,"PET")++
1`(5,"RI ")++
1`(6,"NET");
Packets
To Send
NOxDATA
AllPackets
B
NOxDATA
Data
Received
DATA
1`""
NextSend
NO
1`1
A
NOxDATA
D
NO
C
NO
NextRec
NO
1`1
Limit
UNIT
3`()
Send
Packet
Transmit
Packet
Receive
Packet
Transmit
Ack
Receive
Ack
(n,d)
if success
then 1`(n,d)
else empty
(n,d)
if n=k
then data^d
else data
n
(n,d)
(n,d)
if n=k
then k+1
else k
n
if success
then 1`n
else empty
n
n
data
k
if n=k
then k+1
else k
k
()
()
if not success
then 1`()
else empty
if not success
then 1`()
else empty
fun CountTokens n =
size(Mark.StateSpaceProtocol'A 1 n) + size(Mark.StateSpaceProtocol'B 1 n) +
size(Mark.StateSpaceProtocol'C 1 n) + size(Mark.StateSpaceProtocol'D 1 n) +
size(Mark.StateSpaceProtocol'Limit 1 n);
PredAllNodes (fn n => CountTokens(n)<>3);
fun StopWait n =
let
val Sender_Seq = ms_to_col (Mark.StateSpaceProtocol'NextSend 1 n);
val Receiver_Seq = ms_to_col (Mark.StateSpaceProtocol'NextRec 1 n);
in
(Sender_Seq - Receiver_Seq) <= 1
end;
val swviolate = PredAllNodes (not o StopWait);
NoOfNodes ();
BEsDead ([Bind.StateSpaceProtocol'Receive_Ack (1,{k=1,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=2,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=3,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=4,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=5,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=6,n=1}),
Bind.StateSpaceProtocol'Receive_Ack (1,{k=7,n=1})
],1);
open Bind
PredAllNodes (fn n => (OutArcs) n = []);
PredAllSccs (SccTerminal);
SccToNodes ~1553;
fun ListHomeMarkings () =
let
val Terminal_Sccs = PredAllSccs (SccTerminal);
in
case Terminal_Sccs of
[scc] => SccToNodes scc
| _ => []
end
ListHomeMarkings ();
fun IsTransitionDead t =
PredAllArcs (fn a => ArcToTI a = t);