s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Tidy up of PTA examples. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2169 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
c3626c54b0
commit
5c59047e2f
18 changed files with 5 additions and 6035 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 100
      prism-examples/pta/csma/abst/csma1-digital.nm
  2. 106
      prism-examples/pta/csma/abst/csma1-test.nm
  3. 109
      prism-examples/pta/csma/abst/csma2-digital.nm
  4. 122
      prism-examples/pta/csma/abst/csma3-digital.nm
  5. 139
      prism-examples/pta/csma/abst/csma4-digital.nm
  6. 8
      prism-examples/pta/csma/full/auto
  7. 2203
      prism-examples/pta/csma/full/csma-digital.nm
  8. 2208
      prism-examples/pta/csma/full/csma-slots.nm
  9. 74
      prism-examples/pta/firewire/abst/firewire-digital.nm
  10. 82
      prism-examples/pta/firewire/abst/firewire-max.nm
  11. 167
      prism-examples/pta/firewire/impl/firewire-digital.nm
  12. 9
      prism-examples/pta/tests-prism.sh
  13. 13
      prism-examples/pta/zeroconf/auto
  14. 42
      prism-examples/pta/zeroconf/zeroconf-digital.nm
  15. 299
      prism-examples/pta/zeroconf/zeroconf-full.nm
  16. 3
      prism-examples/pta/zeroconf/zeroconf-full.pctl
  17. 277
      prism-examples/pta/zeroconf/zeroconf-full4.nm
  18. 79
      prism-examples/pta/zeroconf/zeroconf-simple.nm

100
prism-examples/pta/csma/abst/csma1-digital.nm
View File

@ -1,100 +0,0 @@
// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
// gxn/dxp 04/12/01
nondeterministic
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
//----------------------------------------------------------------------------------------------------------------------------
// actual parameters
const int K=1; // exponential backoff limit
const int slot=2*sigma; // length of slot
const int M=floor(pow(2, K)); // max number of slots to wait
const int sigma=26;
const int lambda=808;
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clock of bus
y : [0..sigma+1];
// station starts sending
[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
// message being sent
[busy1] (b=1) & (y>=sigma) -> (b'=1);
[busy2] (b=1) & (y>=sigma) -> (b'=1);
// station finishes
[end1] (b=1) -> (b'=0) & (y'=0);
[end2] (b=1) -> (b'=0) & (y'=0);
// collision detected
[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
// time transitions
[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..4];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 -done (since sending only one message)
// LOCAL CLOCK
x1 : [0..max(lambda,M*slot)+1];
// COLLISION COUNTER
cd1 : [0..K];
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
// transmitting
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected
// set backoff (no time can pass in this state)
// first retransmission
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot)
+ 1/2 : (s1'=3) & (x1'=1*slot);
// wait until backoff counter reaches 0 then send again
[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
// finished backoff
[send1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
// finished
[done] (s1=4) -> true;
[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule

106
prism-examples/pta/csma/abst/csma1-test.nm
View File

@ -1,106 +0,0 @@
// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
// gxn/dxp 04/12/01
pta
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
//----------------------------------------------------------------------------------------------------------------------------
// actual parameters
const int K=1; // exponential backoff limit
const int slot=2*sigma; // length of slot
const int sigma=26;
const int lambda=808;
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clock of bus
y : clock;
invariant
(b=0 => true) &
(b=1 => true) &
(b=2 => y<=sigma)
endinvariant
// station starts sending
[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
// message being sent
[busy1] (b=1) & (y>=sigma) -> (b'=1);
[busy2] (b=1) & (y>=sigma) -> (b'=1);
// station finishes
[end1] (b=1) -> (b'=0) & (y'=0);
[end2] (b=1) -> (b'=0) & (y'=0);
// collision detected
[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..4];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 -done (since sending only one message)
// LOCAL CLOCK
x1 : clock;
invariant
(s1=0 => x1=0) &
(s1=1 => x1<=lambda) &
(s1=2 => x1<=0) &
(s1=3 => x1<=104) &
(s1=4 => true)
endinvariant
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0); // detects channel is busy so go into backoff
// transmitting
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0); // collision detected
// set backoff (no time can pass in this state)
// first retransmission
[] s1=2 -> 1/2 : (s1'=3) & (x1'=0)
+ 1/2 : (s1'=3) & (x1'=52);
// finished backoff
[send1] s1=3 & x1>=104 -> (s1'=1) & (x1'=0); // channel free
[busy1] s1=3 & x1>=104 -> (s1'=2) & (x1'=0); // channel busy
// once finished nothing matters
[done] s1=4 -> true;
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,send1=send2,busy1=busy2,end1=end2] endmodule
//----------------------------------------------------------------------------------------------------------------------------
// LABELS
label "done" = s1=4 & s2=4;

109
prism-examples/pta/csma/abst/csma2-digital.nm
View File

@ -1,109 +0,0 @@
// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
// gxn/dxp 04/12/01
nondeterministic
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
//----------------------------------------------------------------------------------------------------------------------------
// actual parameters
const int K=2; // exponential backoff limit
const int slot=2*sigma; // length of slot
const int M=floor(pow(2, K)); // max number of slots to wait
const int sigma=26;
const int lambda=808;
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clock of bus
y : [0..sigma+1];
// station starts sending
[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send1] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
[send2] (b=1) & (y<=sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
// message being sent
[busy1] (b=1) & (y>=sigma) -> (b'=1);
[busy2] (b=1) & (y>=sigma) -> (b'=1);
// station finishes
[end1] (b=1) -> (b'=0) & (y'=0);
[end2] (b=1) -> (b'=0) & (y'=0);
// collision detected
[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
// time transitions
[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..4];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 -done (since sending only one message)
// LOCAL CLOCK
x1 : [0..max(lambda,M*slot)+1];
// COLLISION COUNTER
cd1 : [0..K];
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
// transmitting
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected
// set backoff (no time can pass in this state)
// first retransmission
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot)
+ 1/2 : (s1'=3) & (x1'=1*slot);
// second retransmission
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+ 1/4 : (s1'=3) & (x1'=1*slot)
+ 1/4 : (s1'=3) & (x1'=2*slot)
+ 1/4 : (s1'=3) & (x1'=3*slot);
// wait until backoff counter reaches 0 then send again
[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
// finished backoff
[send1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
// finished
[done] (s1=4) -> true;
[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule

122
prism-examples/pta/csma/abst/csma3-digital.nm
View File

@ -1,122 +0,0 @@
// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
// gxn/dxp 04/12/01
nondeterministic
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
//----------------------------------------------------------------------------------------------------------------------------
// actual parameters
const int K=3; // exponential backoff limit
const int slot=2*sigma; // length of slot
const int M=floor(pow(2, K)); // max number of slots to wait
const int sigma=26;
const int lambda=808;
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clock of bus
y : [0..sigma+1];
// station starts sending
[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send1] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
[send2] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
// message being sent
[busy1] (b=1) & (y>=sigma) -> (b'=1);
[busy2] (b=1) & (y>=sigma) -> (b'=1);
// station finishes
[end1] (b=1) -> (b'=0) & (y'=0);
[end2] (b=1) -> (b'=0) & (y'=0);
// collision detected
[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
// time transitions
[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..4];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 -done (since sending only one message)
// LOCAL CLOCK
x1 : [0..max(lambda,M*slot)+1];
// COLLISION COUNTER
cd1 : [0..K];
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
// transmitting
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected
// set backoff (no time can pass in this state)
// first retransmission
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot)
+ 1/2 : (s1'=3) & (x1'=1*slot);
// second retransmission
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+ 1/4 : (s1'=3) & (x1'=1*slot)
+ 1/4 : (s1'=3) & (x1'=2*slot)
+ 1/4 : (s1'=3) & (x1'=3*slot);
// thrid retransmission
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot)
+ 1/8 : (s1'=3) & (x1'=1*slot)
+ 1/8 : (s1'=3) & (x1'=2*slot)
+ 1/8 : (s1'=3) & (x1'=3*slot)
+ 1/8 : (s1'=3) & (x1'=4*slot)
+ 1/8 : (s1'=3) & (x1'=5*slot)
+ 1/8 : (s1'=3) & (x1'=6*slot)
+ 1/8 : (s1'=3) & (x1'=7*slot);
// wait until backoff counter reaches 0 then send again
[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=3) & (x1<8*slot) -> (x1'=x1+1); // let time pass (in slot)
// finished backoff
[send1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=3 & (x1=8*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=3 & (x1=8*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
// finished
[done] (s1=4) -> true;
[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule

139
prism-examples/pta/csma/abst/csma4-digital.nm
View File

@ -1,139 +0,0 @@
// CSMA/CD protocol - probabilistic version of kronos model adapted to model a single station
// gxn/dxp 04/12/01
nondeterministic
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
// actual parameters
const int K=4; // exponential backoff limit
const int slot=2*sigma; // length of slot
const int M=floor(pow(2, K)); // max number of slots to wait
const int sigma=26;
const int lambda=808;
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clock of bus
y : [0..sigma+1];
// station starts sending
[send1] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send2] (b=0) -> (b'=1) & (y'=0); // no message being sent
[send1] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
[send2] (b=1) & (y<sigma) -> (b'=2) & (y'=0); // message being sent (move to collision)
// message being sent
[busy1] (b=1) & (y>=sigma) -> (b'=1);
[busy2] (b=1) & (y>=sigma) -> (b'=1);
// station finishes
[end1] (b=1) -> (b'=0) & (y'=0);
[end2] (b=1) -> (b'=0) & (y'=0);
// collision detected
[cd] (b=2) & (y<=sigma) -> (b'=0) & (y'=0);
// time transitions
[time] (b=0) -> (y'=min(y+1,sigma+1)); // value of y does not matter in state 0
[time] (b=1) -> (y'=min(y+1,sigma+1)); // no invariant in state 1
[time] (b=2) & (y<sigma) -> (y'=min(y+1,sigma+1)); // invariant in state 2
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..4];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 -done (since sending only one message)
// LOCAL CLOCK
x1 : [0..max(lambda,M*slot)+1];
// COLLISION COUNTER
cd1 : [0..K];
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
// transmitting
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected
// set backoff (no time can pass in this state)
// first retransmission
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (x1'=0*slot)
+ 1/2 : (s1'=3) & (x1'=1*slot);
// second retransmission
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (x1'=0*slot)
+ 1/4 : (s1'=3) & (x1'=1*slot)
+ 1/4 : (s1'=3) & (x1'=2*slot)
+ 1/4 : (s1'=3) & (x1'=3*slot);
// thrid retransmission
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (x1'=0*slot)
+ 1/8 : (s1'=3) & (x1'=1*slot)
+ 1/8 : (s1'=3) & (x1'=2*slot)
+ 1/8 : (s1'=3) & (x1'=3*slot)
+ 1/8 : (s1'=3) & (x1'=4*slot)
+ 1/8 : (s1'=3) & (x1'=5*slot)
+ 1/8 : (s1'=3) & (x1'=6*slot)
+ 1/8 : (s1'=3) & (x1'=7*slot);
// fourth retransmission
[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (x1'=0*slot)
+ 1/16 : (s1'=3) & (x1'=1*slot)
+ 1/16 : (s1'=3) & (x1'=2*slot)
+ 1/16 : (s1'=3) & (x1'=3*slot)
+ 1/16 : (s1'=3) & (x1'=4*slot)
+ 1/16 : (s1'=3) & (x1'=5*slot)
+ 1/16 : (s1'=3) & (x1'=6*slot)
+ 1/16 : (s1'=3) & (x1'=7*slot)
+ 1/16 : (s1'=3) & (x1'=8*slot)
+ 1/16 : (s1'=3) & (x1'=9*slot)
+ 1/16 : (s1'=3) & (x1'=10*slot)
+ 1/16 : (s1'=3) & (x1'=11*slot)
+ 1/16 : (s1'=3) & (x1'=12*slot)
+ 1/16 : (s1'=3) & (x1'=13*slot)
+ 1/16 : (s1'=3) & (x1'=14*slot)
+ 1/16 : (s1'=3) & (x1'=15*slot);
// wait until backoff counter reaches 0 then send again
[time] (s1=3) & (cd1=1) & (x1<2*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=2) & (x1<4*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=3) & (x1<8*slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (cd1=4) & (x1<16*slot) -> (x1'=x1+1); // let time pass (in slot)
// finished backoff
[send1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=1 & (x1=2*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=2 & (x1=4*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=3 & (x1=8*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=3 & (x1=8*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
[send1] (s1=3) & cd1=4 & (x1=16*slot) -> (s1'=1) & (x1'=0); // channel free
[busy1] (s1=3) & cd1=4 & (x1=16*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
// finished
[done] (s1=4) -> true;
[time] (s1=4) -> (x1'=min(x1+1,max(lambda,M*slot)+1));
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule

8
prism-examples/pta/csma/full/auto
View File

@ -5,7 +5,7 @@ prism csma.nm collisions.pctl -const bmax=2,K=8 -aroptions refine=all,nopre,opt
prism csma.nm collisions.pctl -const bmax=4,K=4 -aroptions refine=all,nopre,opt
prism csma.nm collisions.pctl -const bmax=4,K=8 -aroptions refine=all,nopre,opt
prism csma.nm time.pctl -const bmax=1,K=0 -aroptions refine=all,nopre,opt
prism csma.nm time.pctl -const bmax=2,K=0 -aroptions refine=all,nopre,opt
prism csma.nm time.pctl -const bmax=3,K=0 -aroptions refine=all,nopre,opt
prism csma.nm time.pctl -const bmax=4,K=0 -aroptions refine=all,nopre,opt
#prism csma.nm time.pctl -const bmax=1,K=0 -aroptions refine=all,nopre,opt
#prism csma.nm time.pctl -const bmax=2,K=0 -aroptions refine=all,nopre,opt
#prism csma.nm time.pctl -const bmax=3,K=0 -aroptions refine=all,nopre,opt
#prism csma.nm time.pctl -const bmax=4,K=0 -aroptions refine=all,nopre,opt

2203
prism-examples/pta/csma/full/csma-digital.nm
File diff suppressed because it is too large
View File

2208
prism-examples/pta/csma/full/csma-slots.nm
File diff suppressed because it is too large
View File

74
prism-examples/pta/firewire/abst/firewire-digital.nm
View File

@ -1,74 +0,0 @@
// discrete version of abstract firewire protocol
// gxn 23/05/2001
nondeterministic
// wire delay
const int delay;
// probability of choosing fast and slow
const double fast;
const double slow = 1-fast;
// maximal constant
const int kx = 167;
module abstract_firewire
// clock
x : [0..kx+1];
// local state
s : [0..9];
// 0 -start_start
// 1 -fast_start
// 2 -start_fast
// 3 -start_slow
// 4 -slow_start
// 5 -fast_fast
// 6 -fast_slow
// 7 -slow_fast
// 8 -slow_slow
// 9 -done
// initial state
[time] s=0 & x<delay -> (x'=min(x+1,kx+1));
[round] s=0 -> fast : (s'=1) + slow : (s'=4);
[round] s=0 -> fast : (s'=2) + slow : (s'=3);
// fast_start
[time] s=1 & x<delay -> (x'=min(x+1,kx+1));
[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
// start_fast
[time] s=2 & x<delay -> (x'=min(x+1,kx+1));
[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
// start_slow
[time] s=3 & x<delay -> (x'=min(x+1,kx+1));
[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
// slow_start
[time] s=4 & x<delay -> (x'=min(x+1,kx+1));
[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
// fast_fast
[time] s=5 & (x<85) -> (x'=min(x+1,kx+1));
[] s=5 & (x>=76) -> (s'=0) & (x'=0);
[] s=5 & (x>=76-delay) -> (s'=9) & (x'=0);
// fast_slow
[time] s=6 & x<167 -> (x'=min(x+1,kx+1));
[] s=6 & x>=159-delay -> (s'=9) & (x'=0);
// slow_fast
[time] s=7 & x<167 -> (x'=min(x+1,kx+1));
[] s=7 & x>=159-delay -> (s'=9) & (x'=0);
// slow_slow
[time] s=8 & x<167 -> (x'=min(x+1,kx+1));
[] s=8 & x>=159 -> (s'=0) & (x'=0);
[] s=8 & x>=159-delay -> (s'=9) & (x'=0);
// done
[] s=9 -> (s'=s);
endmodule
// labels
label "done" = (s=9);
rewards
[time] true : 1;
endrewards

82
prism-examples/pta/firewire/abst/firewire-max.nm
View File

@ -1,82 +0,0 @@
// Abstract model of Firewire protocol (PTA model)
// dxp/gxn 08/07/09
pta
// maximum and minimum delays
// fast
const int rc_fast_max = 850;
const int rc_fast_min = 760;
// slow
const int rc_slow_max = 1670;
const int rc_slow_min = 1590;
// delay caused by the wire length
const int delay;
// probability of choosing fast and slow
const double fast = 0.5;
const double slow = 1-fast;
const int T;
module abstract_firewire
// clock
x : clock;
z : clock;
// local state
s : [0..9];
// 0 - start_start
// 1 - fast_start
// 2 - start_fast
// 3 - start_slow
// 4 - slow_start
// 5 - fast_fast
// 6 - fast_slow
// 7 - slow_fast
// 8 - slow_slow
// 9 - done
// clock invariant
invariant
(s=0 => x<=delay) &
(s=1 => x<=delay) &
(s=2 => x<=delay) &
(s=3 => x<=delay) &
(s=4 => x<=delay) &
(s=5 => x<=rc_fast_max) &
(s=6 => x<=rc_slow_max) &
(s=7 => x<=rc_slow_max) &
(s=8 => x<=rc_slow_max) &
(s=9 => x<=0)
endinvariant
// start_start (initial state)
[] s=0 -> fast : (s'=1) + slow : (s'=4);
[] s=0 -> fast : (s'=2) + slow : (s'=3);
// fast_start
[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
// start_fast
[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
// start_slow
[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
// slow_start
[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
// fast_fast
[] s=5 & (x>=rc_fast_min) -> (s'=0) & (x'=0);
[] s=5 & (x>=rc_fast_min-delay) -> (s'=9) & (x'=0);
// fast_slow
[] s=6 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
// slow_fast
[] s=7 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
// slow_slow
[] s=8 & x>=rc_slow_min -> (s'=0) & (x'=0);
[] s=8 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
// done
[] s=9 & z>=T -> (s'=10);
[] s=9 & z<T -> (s'=11);
[] s>9 -> true;
endmodule
// labels
label "done_after" = (s=10);

167
prism-examples/pta/firewire/impl/firewire-digital.nm
View File

@ -1,167 +0,0 @@
// firewire protocol with integer semantics
// dxp/gxn 14/06/01
// CLOCKS
// x1 (x2) clock for node1 (node2)
// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
// maximum and minimum delays
// fast
const int rc_fast_max = 85;
const int rc_fast_min = 76;
// slow
const int rc_slow_max = 167;
const int rc_slow_min = 159;
// delay caused by the wire length
const int delay;
// probability of choosing fast
const double fast = 0.5;
const double slow = 1-fast;
module wire12
// local state
w12 : [0..9];
// 0 - empty
// 1 - rec_req
// 2 - rec_req_ack
// 3 - rec_ack
// 4 - rec_ack_idle
// 5 - rec_idle
// 6 - rec_idle_req
// 7 - rec_ack_req
// 8 - rec_req_idle
// 9 - rec_idle_ack
// clock for wire12
y1 : [0..delay+1];
y2 : [0..delay+1];
// empty
// do not need y1 and y2 to increase as always reset when this state is left
// similarly can reset y1 and y2 when we re-enter this state
[snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0);
[snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0);
[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0);
[time] w12=0 -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_req
[snd_req12] w12=1 -> (w12'=1);
[rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_ack12] w12=1 -> (w12'=2) & (y2'=0);
[snd_idle12] w12=1 -> (w12'=8) & (y2'=0);
[time] w12=1 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_req_ack
[snd_ack12] w12=2 -> (w12'=2);
[rec_req12] w12=2 -> (w12'=3);
[time] w12=2 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack
[snd_ack12] w12=3 -> (w12'=3);
[rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_idle12] w12=3 -> (w12'=4) & (y2'=0);
[snd_req12] w12=3 -> (w12'=7) & (y2'=0);
[time] w12=3 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack_idle
[snd_idle12] w12=4 -> (w12'=4);
[rec_ack12] w12=4 -> (w12'=5);
[time] w12=4 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle
[snd_idle12] w12=5 -> (w12'=5);
[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_req12] w12=5 -> (w12'=6) & (y2'=0);
[snd_ack12] w12=5 -> (w12'=9) & (y2'=0);
[time] w12=5 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle_req
[snd_req12] w12=6 -> (w12'=6);
[rec_idle12] w12=6 -> (w12'=1);
[time] w12=6 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack_req
[snd_req12] w12=7 -> (w12'=7);
[rec_ack12] w12=7 -> (w12'=1);
[time] w12=7 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_req_idle
[snd_idle12] w12=8 -> (w12'=8);
[rec_req12] w12=8 -> (w12'=5);
[time] w12=8 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle_ack
[snd_ack12] w12=9 -> (w12'=9);
[rec_idle12] w12=9 -> (w12'=3);
[time] w12=9 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
endmodule
module node1
// clock for node1
x1 : [0..168];
// local state
s1 : [0..8];
// 0 - root contention
// 1 - rec_idle
// 2 - rec_req_fast
// 3 - rec_req_slow
// 4 - rec_idle_fast
// 5 - rec_idle_slow
// 6 - snd_req
// 7- almost_root
// 8 - almost_child
// added resets to x1 when not considered again until after rest
// removed root and child (using almost root and almost child)
// root contention immediate state)
[snd_idle12] s1=0 & x1=0 -> fast : (s1'=2) + slow : (s1'=3);
[rec_idle21] s1=0 & x1=0 -> (s1'=1);
// rec_idle immediate state)
[snd_idle12] s1=1 & x1=0 -> fast : (s1'=4) + slow : (s1'=5);
[rec_req21] s1=1 & x1=0 -> (s1'=0);
// rec_req_fast
[rec_idle21] s1=2 -> (s1'=4);
[snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
[time] s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168));
// rec_req_slow
[rec_idle21] s1=3 -> (s1'=5);
[snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
[time] s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168));
// rec_idle_fast
[rec_req21] s1=4 -> (s1'=2);
[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
[time] s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168));
// rec_idle_slow
[rec_req21] s1=5 -> (s1'=3);
[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
[time] s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168));
// snd_req
// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1
// also can set x1 to 0 upon entering this state
[rec_req21] s1=6 -> (s1'=0) & (x1'=0);
[rec_ack21] s1=6 -> (s1'=8) & (x1'=0);
[time] s1=6 -> (x1'=min(x1+1,168));
// almost root (immediate)
// loop in final states to remove deadlock
[loop] s1=7 & s2=8 -> (s1'=s1);
[loop] s1=8 & s2=7 -> (s1'=s1);
[time] s1=7 -> (x1'=min(x1+1,168));
[time] s1=8 -> (x1'=min(x1+1,168));
endmodule
// construct remaining automata through renaming
module wire21=wire12[w12=w21, y1=z1, y2=z2,
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,
rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21]
endmodule
module node2=node1[s1=s2, s2=s1, x1=x2,
rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12,
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,done1=done2,done2=done1]
endmodule
// reward structures
// time
rewards "time"
[time] true : 1;
endrewards
// time nodes sending
rewards "time_sending"
[time] (w12>0 | w21>0) : 1;
endrewards

9
prism-examples/pta/tests-prism.sh
View File

@ -1,9 +0,0 @@
prism-benchmark -exec prism-explicit -logs logs csma
prism-benchmark -exec prism-explicit -logs logs csma/abst
prism-benchmark -exec prism-explicit -logs logs firewire/impl
prism-benchmark -exec prism-explicit -logs logs firewire/abst
prism-benchmark -exec prism-explicit -logs logs zeroconf
prism-benchmark -exec prism-explicit -logs logs repudiation/honest
prism-benchmark -exec prism-explicit -logs logs repudiation/malicious

13
prism-examples/pta/zeroconf/auto
View File

@ -1,20 +1,9 @@
#!/bin/csh
# full (multi-variable)
prism zeroconf.nm incorrect.pctl -aroptions refine=all,nopre,opt
prism zeroconf.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt
prism zeroconf.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt
prism zeroconf.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt
prism zeroconf.nm time.pctl -aroptions refine=all,nopre,opt
# simple (single variable)
prism zeroconf-simple.nm incorrect.pctl -aroptions refine=all,nopre,opt
prism zeroconf-simple.nm deadline.pctl -const T=100 -aroptions refine=all,nopre,opt
prism zeroconf-simple.nm deadline.pctl -const T=150 -aroptions refine=all,nopre,opt
prism zeroconf-simple.nm deadline.pctl -const T=200 -aroptions refine=all,nopre,opt
#prism zeroconf.nm time.pctl -aroptions refine=all,nopre,opt

42
prism-examples/pta/zeroconf/zeroconf-digital.nm
View File

@ -1,42 +0,0 @@
// prism model of pta version of zeroconf
// using digitial clocks
mdp
module sender
s : [0..2]; //local state
probes : [0..4]; // probes sent
ip : [0..2]; // ip address not chosen, fresh or in use
x : [0..21]; // local clock
// selct probe
// [] s=0 -> 0.99969242125984251969 : (s'=1) & (ip'=0) + 0.00030757874015748031 : (s'=1) & (ip'=1);
[] s=0 -> 0.5 : (s'=1) & (ip'=1) + 0.5 : (s'=1) & (ip'=2);
// send probes
[time] s=1 & x<20 -> (x'=x+1);
[send_used] s=1 & x=20 & ip=2 & probes<4 -> (probes'=probes+1) & (x'=0);
[send_fresh] s=1 & x=20 & ip=1 & probes<4 -> (probes'=probes+1) & (x'=0);
[] s=1 & x=20 & probes=4 -> (s'=2) & (x'=0);
[recv] s=1 -> (s'=0) & (x'=0) & (ip'=0) & (probes'=0);
[time] s=2 -> (x'=min(21,x+1));
endmodule
module environment
e : [0..2]; // ready, send reply
y : [0..6];
[time] e=0 -> (y'=min(y+1,6));
[send_fresh] e=0 -> true;
[send_used] e=0 -> 0.1 : (e'=0) + 0.9 : (e'=1);
[time] e>0 & y<5 -> (y'=y+1);
[] e=1 & y>=1 -> 0.1 : (e'=0) & (y'=0) + 0.9 : (e'=2) & (y'=0);
[recv] e=2 & y>=1 -> (e'=0) & (y'=0);
endmodule

299
prism-examples/pta/zeroconf/zeroconf-full.nm
View File

@ -1,299 +0,0 @@
// IPv4: PTA model with digitial clocks
// one concrete host attempting to choose an ip address
// when a number of (abstract) hosts have already got ip addresses
// gxn/dxp/jzs 02/05/03
// reset or noreset model
const bool reset=true;
//-------------------------------------------------------------
// we suppose that
// - the abstract hosts have already picked their addresses
// and always defend their addresses
// - the concrete host never picks the same ip address twice
// (this can happen only with a verys small probability)
// under these assumptions we do not need message types because:
// 1) since messages to the concrete host will never be a probe,
// this host will react to all messages in the same way
// 2) since the abstract hosts always defend their addresses,
// all messages from the host will get an arp reply if the ip matches
// following from the above assumptions we require only three abstract IP addresses
// (0,1 and 2) which correspond to the following sets of IP addresses:
// 0 - the IP addresses of the abstract hosts which the concrete host
// previously tried to configure
// 1 - an IP address of an abstract host which the concrete host is
// currently trying to configure
// 2 - a fresh IP address which the concrete host is currently trying to configure
// if the host picks an address that is being used it may end up picking another ip address
// in which case there may still be messages corresponding to the old ip address
// to be sent both from and to the host which the host should now disregard
// (since it will never pick the same ip address)
// to deal with this situation: when a host picks a new ip address we reconfigure the
// messages that are still be be sent or are being sent by changing the ip address to 0
// (an old ip address of the host)
// all the messages from the abstract hosts for the 'old' address (in fact the
// set of old addresses since it may have started again more than once)
// can arrive in any order since they are equivalent to the host - it ignores then all
// also the messages for the old and new address will come from different hosts
// (the ones with that ip address) which we model by allowing them to arrive in any order
// i.e. not neccessarily in the order they where sent
//-------------------------------------------------------------
// model is an pta
pta
//-------------------------------------------------------------
// VARIABLES
const int N=1000; // number of abstract hosts
const int K=2; // number of probes to send
const double loss = 0.1; // probability of message loss
// PROBABILITIES
const double old = N/65024; // probability pick an ip address being used
const double new = (1-old); // probability pick a new ip address
// TIMING CONSTANTS
const int CONSEC = 2; // time interval between sending consecutive probles
const int TRANSTIME = 1; // upper bound on transmission time delay
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions
const int DEFEND = 10;
const int TIME_MAX_X = 60; // max value of clock x
const int TIME_MAX_Y = 10; // max value of clock y
const int TIME_MAX_Z = 1; // max value of clock z
// OTHER CONSTANTS
const int MAXCOLL = 10; // maximum number of collisions before long wait
// size of buffers for other hosts
const int B0 = 20; // buffer size for one abstract host
const int B1 = 8; // buffer sizes for all abstract hosts
//-------------------------------------------------------------
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
module environment
// buffer of concrete host
b_ip7 : [0..2]; // ip address of message in buffer position 8
b_ip6 : [0..2]; // ip address of message in buffer position 7
b_ip5 : [0..2]; // ip address of message in buffer position 6
b_ip4 : [0..2]; // ip address of message in buffer position 5
b_ip3 : [0..2]; // ip address of message in buffer position 4
b_ip2 : [0..2]; // ip address of message in buffer position 3
b_ip1 : [0..2]; // ip address of message in buffer position 2
b_ip0 : [0..2]; // ip address of message in buffer position 1
n : [0..8]; // number of places in the buffer used (from host)
// messages to be sent from abstract hosts to concrete host
n0 : [0..B0]; // number of messages which do not have the host's current ip address
n1 : [0..B1]; // number of messages which have the host's current ip address
b : [0..2]; // local state
// 0 - idle
// 1 - sending message from concrete host
// 2 - sending message from abstract host
z : clock; // clock of environment (needed for the time to send a message)
ip_mess : [0..2]; // ip in the current message being sent
// 0 - different from concrete host
// 1 - same as the concrete host and in use
// 2 - same as the concrete host and not in use
invariant
(b=0 & n=0 & n0=0 & n1=0 => true) & // nothing to send
(b=0 & !(n=0 & n0=0 & n1=0) => z<=0) & // something to send
(b>0 => z<=1) // sending
endinvariant
// RESET/RECONFIG: when host is about to choose new ip address
// suppose that the host cannot choose the same ip address
// (since happens with very small probability).
// Therefore all messages will have a different ip address,
// i.e. all n1 messages become n0 ones.
// Note this include any message currently being sent (ip is set to zero 0)
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers
& (ip_mess'=0) // message being set
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model)
& (b_ip7'=0)
& (b_ip6'=0)
& (b_ip5'=0)
& (b_ip4'=0)
& (b_ip3'=0)
& (b_ip2'=0)
& (b_ip1'=0)
& (b_ip0'=0);
// note: prevent anything else from happening when reconfiguration needs to take place
// get messages to be sent (so message has same ip address as host)
[send1] n=0 -> (b_ip0'=1) & (n'=n+1);
[send1] n=1 -> (b_ip1'=1) & (n'=n+1);
[send1] n=2 -> (b_ip2'=1) & (n'=n+1);
[send1] n=3 -> (b_ip3'=1) & (n'=n+1);
[send1] n=4 -> (b_ip4'=1) & (n'=n+1);
[send1] n=5 -> (b_ip5'=1) & (n'=n+1);
[send1] n=6 -> (b_ip6'=1) & (n'=n+1);
[send1] n=7 -> (b_ip7'=1) & (n'=n+1);
[send1] n=8 -> (n'=n); // buffer full so lose message
[send2] n=0 -> (b_ip0'=2) & (n'=n+1);
[send2] n=1 -> (b_ip1'=2) & (n'=n+1);
[send2] n=2 -> (b_ip2'=2) & (n'=n+1);
[send2] n=3 -> (b_ip3'=2) & (n'=n+1);
[send2] n=4 -> (b_ip4'=2) & (n'=n+1);
[send2] n=5 -> (b_ip5'=2) & (n'=n+1);
[send2] n=6 -> (b_ip6'=2) & (n'=n+1);
[send2] n=7 -> (b_ip7'=2) & (n'=n+1);
[send2] n=8 -> (n'=n); // buffer full so lose message
// start sending message from host
[a] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0)
& (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
& (b_ip5'=b_ip6)
& (b_ip4'=b_ip5)
& (b_ip3'=b_ip4)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1) // send message
+ loss : (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
& (b_ip5'=b_ip6)
& (b_ip4'=b_ip5)
& (b_ip3'=b_ip4)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1); // lose message
// start sending message to host
[a] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
[a] b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
// finish sending message from host
[a] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
[a] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
[a] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
// finish sending message to host
[rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec2] b=2 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
endmodule
//-------------------------------------------------------------
// CONCRETE HOST
module host0
x : clock; // first clock of the host
y : clock; // second clock of the host
coll : [0..MAXCOLL]; // number of address collisions
probes : [0..K]; // counter (number of probes sent)
mess : [0..1]; // need to send a message or not
defend : [0..1]; // defend (if =1, try to defend IP address)
ip : [1..2]; // ip address (1 - in use & 2 - fresh)
l : [0..4] init 1; // location
// 0 : RECONFIGURE
// 1 : RANDOM
// 2 : WAITSP
// 3 : WAITSG
// 4 : USE
invariant
(l=0 => x<=0) &
(l=1 & coll<MAXCOLL => x<=0) &
(l=1 & coll=MAXCOLL => x<=LONGWAIT) &
(l=2 => x<=CONSEC) &
(l=3 => x<=CONSEC) &
(l=4 => true)
endinvariant
// needed to prevent environment from moving before a reset
[a] l>0 -> true;
// RECONFIGURE
[reset] l=0 -> (l'=1);
// RANDOM (choose IP address)
[rec0] (l=1) -> true; // get message (ignore since have no ip address)
[rec1] (l=1) -> true; // get message (ignore since have no ip address)
[rec2] (l=1) -> true; // get message (ignore since have no ip address)
// small number of collisions (choose straight away)
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// large number of collisions: (wait for LONGWAIT)
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// WAITSP
// send probe
[send1] l=2 & ip=1 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
[send2] l=2 & ip=2 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
// sent K probes and waited 2 seconds
[] l=2 & probes=K & x>=2 -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
// get message and ip does not match: ignore
[rec0] l=2 & 0!=ip -> (l'=l);
[rec1] l=2 & 1!=ip -> (l'=l);
[rec2] l=2 & 2!=ip -> (l'=l);
// get a message with matching ip: reconfigure
[rec0] l=2 & 0=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
[rec1] l=2 & 1=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
[rec2] l=2 & 2=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
// receive message and same ip: defend
[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
// receive message and same ip: defer
[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
// receive message and different ip
[rec0] l=3 & mess=0 & 0!=ip -> (l'=l);
[rec1] l=3 & mess=0 & 1!=ip -> (l'=l);
[rec2] l=3 & mess=0 & 2!=ip -> (l'=l);
// send probe reply or message for defence
[send1] l=3 & mess=1 & ip=1 -> (mess'=0);
[send2] l=3 & mess=1 & ip=2 -> (mess'=0);
// send first gratuitous arp message
[send1] l=3 & mess=0 & probes<1 & ip=1 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
[send2] l=3 & mess=0 & probes<1 & ip=2 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
// send second gratuitous arp message (move to use)
[send1] l=3 & mess=0 & probes=1 & ip=1 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[send2] l=3 & mess=0 & probes=1 & ip=2 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
// USE (only interested in reaching this state so do not need to add anything here)
[] l=4 -> true;
endmodule
//-------------------------------------------------------------
rewards "time"
true : 1;
endrewards
label "done" = l=4;
label "done_error" = l=4 & ip=0;
label "done_fresh" = l=4 & ip=1;

3
prism-examples/pta/zeroconf/zeroconf-full.pctl
View File

@ -1,3 +0,0 @@
Pmin=?[F "done"]
Pmin=?[F "done_fresh"]
Pmax=?[F "done_error"]

277
prism-examples/pta/zeroconf/zeroconf-full4.nm
View File

@ -1,277 +0,0 @@
// IPv4: PTA model with digitial clocks
// one concrete host attempting to choose an ip address
// when a number of (abstract) hosts have already got ip addresses
// gxn/dxp/jzs 02/05/03
// reset or noreset model
const bool reset=true;
//-------------------------------------------------------------
// we suppose that
// - the abstract hosts have already picked their addresses
// and always defend their addresses
// - the concrete host never picks the same ip address twice
// (this can happen only with a verys small probability)
// under these assumptions we do not need message types because:
// 1) since messages to the concrete host will never be a probe,
// this host will react to all messages in the same way
// 2) since the abstract hosts always defend their addresses,
// all messages from the host will get an arp reply if the ip matches
// following from the above assumptions we require only three abstract IP addresses
// (0,1 and 2) which correspond to the following sets of IP addresses:
// 0 - the IP addresses of the abstract hosts which the concrete host
// previously tried to configure
// 1 - an IP address of an abstract host which the concrete host is
// currently trying to configure
// 2 - a fresh IP address which the concrete host is currently trying to configure
// if the host picks an address that is being used it may end up picking another ip address
// in which case there may still be messages corresponding to the old ip address
// to be sent both from and to the host which the host should now disregard
// (since it will never pick the same ip address)
// to deal with this situation: when a host picks a new ip address we reconfigure the
// messages that are still be be sent or are being sent by changing the ip address to 0
// (an old ip address of the host)
// all the messages from the abstract hosts for the 'old' address (in fact the
// set of old addresses since it may have started again more than once)
// can arrive in any order since they are equivalent to the host - it ignores then all
// also the messages for the old and new address will come from different hosts
// (the ones with that ip address) which we model by allowing them to arrive in any order
// i.e. not neccessarily in the order they where sent
//-------------------------------------------------------------
// model is an pta
pta
//-------------------------------------------------------------
// VARIABLES
const int N=1000; // number of abstract hosts
const int K=2; // number of probes to send
const double loss = 0.1; // probability of message loss
// PROBABILITIES
const double old = N/65024; // probability pick an ip address being used
const double new = (1-old); // probability pick a new ip address
// TIMING CONSTANTS
const int CONSEC = 2; // time interval between sending consecutive probles
const int TRANSTIME = 1; // upper bound on transmission time delay
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions
const int DEFEND = 10;
const int TIME_MAX_X = 60; // max value of clock x
const int TIME_MAX_Y = 10; // max value of clock y
const int TIME_MAX_Z = 1; // max value of clock z
// OTHER CONSTANTS
const int MAXCOLL = 10; // maximum number of collisions before long wait
// size of buffers for other hosts
//const int B0 = 20; // buffer size for one abstract host
//const int B1 = 8; // buffer sizes for all abstract hosts
const int B0 = 4; // buffer size for one abstract host
const int B1 = 4; // buffer sizes for all abstract hosts
//-------------------------------------------------------------
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
module environment
// buffer of concrete host
b_ip3 : [0..2]; // ip address of message in buffer position 4
b_ip2 : [0..2]; // ip address of message in buffer position 3
b_ip1 : [0..2]; // ip address of message in buffer position 2
b_ip0 : [0..2]; // ip address of message in buffer position 1
n : [0..4]; // number of places in the buffer used (from host)
// messages to be sent from abstract hosts to concrete host
n0 : [0..B0]; // number of messages which do not have the host's current ip address
n1 : [0..B1]; // number of messages which have the host's current ip address
b : [0..2]; // local state
// 0 - idle
// 1 - sending message from concrete host
// 2 - sending message from abstract host
z : clock; // clock of environment (needed for the time to send a message)
ip_mess : [0..2]; // ip in the current message being sent
// 0 - different from concrete host
// 1 - same as the concrete host and in use
// 2 - same as the concrete host and not in use
invariant
(b=0 & n=0 & n0=0 & n1=0 => true) & // nothing to send
(b=0 & !(n=0 & n0=0 & n1=0) => z<=0) & // something to send
(b>0 => z<=1) // sending
endinvariant
// RESET/RECONFIG: when host is about to choose new ip address
// suppose that the host cannot choose the same ip address
// (since happens with very small probability).
// Therefore all messages will have a different ip address,
// i.e. all n1 messages become n0 ones.
// Note this include any message currently being sent (ip is set to zero 0)
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers
& (ip_mess'=0) // message being set
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model)
& (b_ip3'=0)
& (b_ip2'=0)
& (b_ip1'=0)
& (b_ip0'=0);
// note: prevent anything else from happening when reconfiguration needs to take place
// get messages to be sent (so message has same ip address as host)
[send1] n=0 -> (b_ip0'=1) & (n'=n+1);
[send1] n=1 -> (b_ip1'=1) & (n'=n+1);
[send1] n=2 -> (b_ip2'=1) & (n'=n+1);
[send1] n=3 -> (b_ip3'=1) & (n'=n+1);
[send1] n=4 -> (n'=n); // buffer full so lose message
[send2] n=0 -> (b_ip0'=2) & (n'=n+1);
[send2] n=1 -> (b_ip1'=2) & (n'=n+1);
[send2] n=2 -> (b_ip2'=2) & (n'=n+1);
[send2] n=3 -> (b_ip3'=2) & (n'=n+1);
[send2] n=4 -> (n'=n); // buffer full so lose message
// start sending message from host
[a] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0)
& (n'=n-1)
& (b_ip3'=0)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1) // send message
+ loss : (n'=n-1)
& (b_ip3'=0)
& (b_ip2'=b_ip3)
& (b_ip1'=b_ip2)
& (b_ip0'=b_ip1); // lose message
// start sending message to host
[a] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
[a] b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
// finish sending message from host
[a] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
[a] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
[a] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
// finish sending message to host
[rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0);
[rec2] b=2 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
endmodule
//-------------------------------------------------------------
// CONCRETE HOST
module host0
x : clock; // first clock of the host
y : clock; // second clock of the host
coll : [0..MAXCOLL]; // number of address collisions
probes : [0..K]; // counter (number of probes sent)
mess : [0..1]; // need to send a message or not
defend : [0..1]; // defend (if =1, try to defend IP address)
ip : [1..2]; // ip address (1 - in use & 2 - fresh)
l : [0..4] init 1; // location
// 0 : RECONFIGURE
// 1 : RANDOM
// 2 : WAITSP
// 3 : WAITSG
// 4 : USE
invariant
(l=0 => x<=0) &
(l=1 & coll<MAXCOLL => x<=0) &
(l=1 & coll=MAXCOLL => x<=LONGWAIT) &
(l=2 => x<=CONSEC) &
(l=3 => x<=CONSEC) &
(l=4 => true)
endinvariant
// needed to prevent environment from moving before a reset
[a] l>0 -> true;
// RECONFIGURE
[reset] l=0 -> (l'=1);
// RANDOM (choose IP address)
[rec0] (l=1) -> true; // get message (ignore since have no ip address)
[rec1] (l=1) -> true; // get message (ignore since have no ip address)
[rec2] (l=1) -> true; // get message (ignore since have no ip address)
// small number of collisions (choose straight away)
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// large number of collisions: (wait for LONGWAIT)
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1)
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1)
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2);
// WAITSP
// send probe
[send1] l=2 & ip=1 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
[send2] l=2 & ip=2 & probes<K & x>=2 -> (x'=0) & (probes'=probes+1);
// sent K probes and waited 2 seconds
[] l=2 & probes=K & x>=2 -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
// get message and ip does not match: ignore
[rec0] l=2 & 0!=ip -> (l'=l);
[rec1] l=2 & 1!=ip -> (l'=l);
[rec2] l=2 & 2!=ip -> (l'=l);
// get a message with matching ip: reconfigure
[rec0] l=2 & 0=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
[rec1] l=2 & 1=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
[rec2] l=2 & 2=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
// receive message and same ip: defend
[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
// receive message and same ip: defer
[rec0] l=3 & mess=0 & 0=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
[rec1] l=3 & mess=0 & 1=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
[rec2] l=3 & mess=0 & 2=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
// receive message and different ip
[rec0] l=3 & mess=0 & 0!=ip -> (l'=l);
[rec1] l=3 & mess=0 & 1!=ip -> (l'=l);
[rec2] l=3 & mess=0 & 2!=ip -> (l'=l);
// send probe reply or message for defence
[send1] l=3 & mess=1 & ip=1 -> (mess'=0);
[send2] l=3 & mess=1 & ip=2 -> (mess'=0);
// send first gratuitous arp message
[send1] l=3 & mess=0 & probes<1 & ip=1 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
[send2] l=3 & mess=0 & probes<1 & ip=2 & x>=CONSEC -> (x'=0) & (probes'=probes+1);
// send second gratuitous arp message (move to use)
[send1] l=3 & mess=0 & probes=1 & ip=1 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
[send2] l=3 & mess=0 & probes=1 & ip=2 & x>=CONSEC -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
// USE (only interested in reaching this state so do not need to add anything here)
[] l=4 -> true;
endmodule
//-------------------------------------------------------------
rewards "time"
true : 1;
endrewards
label "done" = l=4;
label "done_error" = l=4 & ip=0;
label "done_fresh" = l=4 & ip=1;

79
prism-examples/pta/zeroconf/zeroconf-simple.nm
View File

@ -1,79 +0,0 @@
pta
module sender
sender : [0..12] init 0;
// 0 - reconf
// 1 used0
// 2 used1
// 3 used2
// 4 used3
// 5 used_wait
// 6 used_use
// 7 fresh0
// 8 fresh1
// 9 fresh2
// 10 fresh3
// 11 fresh_wait
// 12 fresh_use
x : clock;
invariant
(sender=0 => x<=0) &
(sender>=1 & sender<=10 => x<=20) &
(sender>10 => true)
endinvariant
// reconfiguring
[] sender=0 ->0.5 : (sender'=1) + 0.5 : (sender'=7);
[recv] sender=1 -> (sender'=0) & (x'=0);
[recv] sender=2 -> (sender'=0) & (x'=0);
[recv] sender=3 -> (sender'=0) & (x'=0);
[recv] sender=4 -> (sender'=0) & (x'=0);
[recv] sender=5 -> (sender'=0) & (x'=0);
[recv] sender=7 -> (sender'=0) & (x'=0);
[recv] sender=8 -> (sender'=0) & (x'=0);
[recv] sender=9 -> (sender'=0) & (x'=0);
[recv] sender=10 -> (sender'=0) & (x'=0);
[recv] sender=11 -> (sender'=0) & (x'=0);
// sending fresh
[send_used] sender=1 & x>=20 -> (sender'=2) & (x'=0);
[send_used] sender=2 & x>=20 -> (sender'=3) & (x'=0);
[send_used] sender=3 & x>=20 -> (sender'=4) & (x'=0);
[send_used] sender=4 & x>=20 -> (sender'=5) & (x'=0);
// sending used
[send_fresh] sender=7 & x>=20 -> (sender'=8) & (x'=0);
[send_fresh] sender=8 & x>=20 -> (sender'=9) & (x'=0);
[send_fresh] sender=9 & x>=20 -> (sender'=10) & (x'=0);
[send_fresh] sender=10 & x>=20 -> (sender'=11) & (x'=0);
// finished
[] sender=5 & x>=20 -> (sender'=6) & (x'=0);
[] sender=11 & x>=20 -> (sender'=12) & (x'=0);
[] sender=6 -> (sender'=6);
[] sender=12 -> (sender'=12);
endmodule
module environment
env : [0..2] init 0;
// 0,1,2 - ready,send,reply
y : clock;
invariant
(env=0 => true) &
(env>=1 => y<=5)
endinvariant
[send_fresh] env=0 -> true;
[send_used] env=0 -> 0.1 : (env'=0) & (y'=0) + 0.9 : (env'=1) & (y'=0);
[] env=1 & y>=1 -> 0.1 : (env'=0) & (y'=0) + 0.9 : (env'=2) & (y'=0);
[recv] env=2 & y>=1 -> (env'=0) & (y'=0);
endmodule
label "incorrect" = sender=6;
Write Preview
Loading…
Cancel
Save