You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
109 lines
2.6 KiB
109 lines
2.6 KiB
#no update for variables
|
|
{
|
|
init
|
|
node ini; true # start protocol
|
|
[
|
|
req||tran send; true; x=0; 1.0
|
|
]
|
|
}
|
|
{
|
|
node send; x<=0 #send first message immediate
|
|
[
|
|
message||tran wait; x=0; null ; 1.0
|
|
]
|
|
}
|
|
{
|
|
# node wait; x<=AD+1 # wait for an ack (added invariant so transition must be taken)
|
|
node wait; x<=5
|
|
[
|
|
#ack||tran send; x>=ad,x<=AD; x=0 ; 0.9 # receive ack (and send another message)
|
|
#ack||tran last; x>=ad,x<=AD; x=0 ; 0.1 # receive ack (and finish)
|
|
ack||tran send; x>=1,x<=4; x=0 ; 0.9
|
|
ack||tran last; x>=1,x<=4; x=0 ; 0.1
|
|
]
|
|
[ # do not receive an ack so end protocol
|
|
#tran early; x>AD; x=0 ; 0.9 # sent random message so no information lost
|
|
#tran error; x>AD; x=0 ; 0.1 # sent last message so security compromised
|
|
tran early; x>4; x=0 ; 0.9
|
|
tran error; x>4; x=0 ; 0.1
|
|
]
|
|
[ # recipient manages to decode message
|
|
# decode||tran sent_random; true; null ; 0.9 # sent random message
|
|
# decode||tran sent_last; true; null ; 0.1 # sent last message
|
|
decode||tran sent_random; true; null ; 0.9
|
|
decode||tran sent_last; true; null ; 0.1
|
|
]
|
|
}
|
|
{
|
|
node last; x=0 # tell recipient have finished
|
|
[
|
|
finished||tran done; x=0; null ; 1.0
|
|
]
|
|
}
|
|
{
|
|
node done; true # finished correctly
|
|
[
|
|
tran done;true;null;1
|
|
]
|
|
}
|
|
{
|
|
node done_early; true # finished early
|
|
[
|
|
tran done_early;true;null;1
|
|
]
|
|
}
|
|
{
|
|
node done_error; true # finished and lost information
|
|
[
|
|
tran done_error;true;null;1
|
|
]
|
|
}
|
|
{
|
|
node early; x=0 # no information lost
|
|
[
|
|
stop||tran done_early;true;null;1
|
|
]
|
|
}
|
|
{
|
|
node error; x=0 # error
|
|
[
|
|
error||tran done_error;true;null;1
|
|
]
|
|
}
|
|
{
|
|
node sent_random; true # need to tell recipient the message was random
|
|
[
|
|
decoded_random||tran wait_random; true; null; 1.0
|
|
]
|
|
}
|
|
{
|
|
node sent_last; true # need to tell recipient the message was the last
|
|
[
|
|
decoded_last||tran wait_last; true; null; 1.0
|
|
]
|
|
}
|
|
{
|
|
# node wait_random; x<=AD+1 # wait for an ack (message random)
|
|
node wait_random; x<=5
|
|
[
|
|
#ack||tran send; x>=ad,x<=AD; x=0 ; 1.0 # receive ack (and send another message)
|
|
ack||tran send; x>=1,x<=4; x=0 ; 1.0
|
|
]
|
|
[ # do not receive an ack so end protocol
|
|
#stop||tran done_early; x>AD; x=0 ; 1.0 # sent random message so no information lost
|
|
stop||tran done_early; x>4; x=0 ; 1.0
|
|
]
|
|
}
|
|
{
|
|
# node wait_last; x<=AD+1 # wait for an ack message is last message)
|
|
node wait_last; x<=5
|
|
[
|
|
#ack||tran last; x>=ad,x<=AD; x=0 ; 1.0 # receive ack (and finish)
|
|
ack||tran last; x>=1,x<=4; x=0 ; 1.0
|
|
]
|
|
[ # do not receive an ack so end protocol
|
|
#error||tran done_error; x>AD; x=0 ; 1.0 # sent last message so security compromised
|
|
error||tran done_error; x>4; x=0 ; 1.0
|
|
]
|
|
*
|
|
|