60 lines
1.1 KiB
Promela
60 lines
1.1 KiB
Promela
mtype = { DATA0, DATA1, ACK0, ACK1 }
|
|
|
|
chan AtoB = [1] of { mtype }
|
|
chan BtoA = [1] of { mtype }
|
|
|
|
mtype ackA, ackB;
|
|
byte seqA = 0;
|
|
byte seqB = 0;
|
|
|
|
mtype packetA, packetB;
|
|
|
|
active proctype A()
|
|
{
|
|
do
|
|
::
|
|
if
|
|
:: seqA == 0 -> packetA = DATA0
|
|
:: else -> packetA = DATA1
|
|
fi;
|
|
AtoB!packetA;
|
|
do
|
|
:: BtoA?ackA ->
|
|
if
|
|
:: (seqA == 0 && ackA == ACK0) || (seqA == 1 && ackA == ACK1) ->
|
|
seqA = 1 - seqA;
|
|
break
|
|
:: else -> skip;
|
|
fi
|
|
::
|
|
AtoB!packetA
|
|
od
|
|
od
|
|
}
|
|
|
|
active proctype B()
|
|
{
|
|
do
|
|
:: AtoB?packetB ->
|
|
if
|
|
:: (seqB == 0 && packetB == DATA0) || (seqB == 1 && packetB == DATA1) ->
|
|
if
|
|
:: seqB == 0 -> ackB = ACK0
|
|
:: else -> ackB = ACK1
|
|
fi;
|
|
BtoA!ackB;
|
|
seqB = 1 - seqB;
|
|
:: else ->
|
|
if
|
|
:: seqB == 0 -> ackB = ACK1
|
|
:: else -> ackB = ACK0
|
|
fi;
|
|
BtoA!ackB;
|
|
fi
|
|
od
|
|
}
|
|
|
|
ltl liveness {
|
|
always ((packetA != packetB) implies eventually (packetA == packetB))
|
|
}
|