sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Made the executable not choke if no model file/property was given. Added the benchmark models to the repo (replacing the old ones). 

Former-commit-id: d0a53bcdf4
tempestpy_adaptions
dehnert 10 years ago
parent
36a65392e0
commit
99bcd337f1
30 changed files with 108 additions and 1326 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. 4
      examples/pdtmc/brp/brp_128-2.pm
  2. 139
      examples/pdtmc/brp/brp_128-3.pm
  3. 139
      examples/pdtmc/brp/brp_128-4.pm
  4. 4
      examples/pdtmc/brp/brp_128-5.pm
  5. 4
      examples/pdtmc/brp/brp_16_2.pm
  6. 4
      examples/pdtmc/brp/brp_256-2.pm
  7. 139
      examples/pdtmc/brp/brp_256-3.pm
  8. 139
      examples/pdtmc/brp/brp_256-4.pm
  9. 4
      examples/pdtmc/brp/brp_256-5.pm
  10. 139
      examples/pdtmc/brp/brp_32-4.pm
  11. 139
      examples/pdtmc/brp/brp_64-4.pm
  12. 139
      examples/pdtmc/brp/brp_64-5.pm
  13. 2
      examples/pdtmc/crowds/crowds_10-5.pm
  14. 5
      examples/pdtmc/crowds/crowds_15-5.pm
  15. 6
      examples/pdtmc/crowds/crowds_20-5.pm
  16. 3
      examples/pdtmc/crowds/crowds_3-5.pm
  17. 193
      examples/pdtmc/crowds/crowds_5-10.pm
  18. 2
      examples/pdtmc/crowds/crowds_5-5.pm
  19. 33
      examples/pdtmc/die/die.pm
  20. 4
      examples/pdtmc/nand/nand_10-1.pm
  21. 5
      examples/pdtmc/nand/nand_10-2.pm
  22. 5
      examples/pdtmc/nand/nand_10-3.pm
  23. 5
      examples/pdtmc/nand/nand_10-4.pm
  24. 5
      examples/pdtmc/nand/nand_10-5.pm
  25. 5
      examples/pdtmc/nand/nand_20-1.pm
  26. 4
      examples/pdtmc/nand/nand_20-2.pm
  27. 5
      examples/pdtmc/nand/nand_20-3.pm
  28. 4
      examples/pdtmc/nand/nand_20-4.pm
  29. 4
      examples/pdtmc/nand/nand_20-5.pm
  30. 151
      src/stormParametric.cpp

4
examples/pdtmc/brp/brp_128-2.pm
View File

@ -134,6 +134,4 @@ module channelL
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;
label "target" = s = 5;

139
examples/pdtmc/brp/brp_128-3.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 128;
// maximum number of retransmissions
const int MAX = 3;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

139
examples/pdtmc/brp/brp_128-4.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 128;
// maximum number of retransmissions
const int MAX = 4;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

4
examples/pdtmc/brp/brp_128-5.pm
View File

@ -135,6 +135,4 @@ module channelL
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;
label "target" = s = 5;

4
examples/pdtmc/brp/brp_16_2.pm
View File

@ -134,6 +134,4 @@ module channelL
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;
label "target" = s=5;

4
examples/pdtmc/brp/brp_256-2.pm
View File

@ -134,6 +134,4 @@ module channelL
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;
label "target" = s = 5;

139
examples/pdtmc/brp/brp_256-3.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 256;
// maximum number of retransmissions
const int MAX = 3;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

139
examples/pdtmc/brp/brp_256-4.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 256;
// maximum number of retransmissions
const int MAX = 4;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

4
examples/pdtmc/brp/brp_256-5.pm
View File

@ -134,6 +134,4 @@ module channelL
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;
label "target" = s = 5;

139
examples/pdtmc/brp/brp_32-4.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 32;
// maximum number of retransmissions
const int MAX = 4;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

139
examples/pdtmc/brp/brp_64-4.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 64;
// maximum number of retransmissions
const int MAX = 4;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

139
examples/pdtmc/brp/brp_64-5.pm
View File

@ -1,139 +0,0 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 64;
// maximum number of retransmissions
const int MAX = 5;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "target" = s=5;
label "finished_with_success" = srep=3&rrep=3;
label "two_fragments_transmitted" = s=1&i=2+1;

2
examples/pdtmc/crowds/crowds_10-5.pm
View File

@ -190,4 +190,6 @@ module crowds
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1;
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1;

5
examples/pdtmc/crowds/crowds_15-5.pm
View File

@ -189,4 +189,7 @@ module crowds
endmodule
label "observe0Greater1" = observe0 > 1;
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1;
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1;

6
examples/pdtmc/crowds/crowds_20-5.pm
View File

@ -36,7 +36,7 @@ module crowds
runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances
start: bool init false; // Start the protocol?
run: bool init false; // Run the protocol?
lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg
lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg
good: bool init false; // Crowd member is good?
bad: bool init false; // ... bad?
recordLast: bool init false; // Record last seen crowd member?
@ -189,4 +189,6 @@ module crowds
endmodule
label "observe0Greater1" = observe0 > 1;
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1;
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1;

3
examples/pdtmc/crowds/crowds_3-5.pm
View File

@ -190,4 +190,5 @@ module crowds
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1>1|observe2>1;
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1;

193
examples/pdtmc/crowds/crowds_5-10.pm
View File

@ -1,193 +0,0 @@
// CROWDS [Reiter,Rubin]
// Vitaly Shmatikov, 2002
// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de)
// note:
// Change everything marked CWDSIZ when changing the size of the crowd
// Change everything marked CWDMAX when increasing max size of the crowd
dtmc
// Model parameters
const double PF; // forwarding probability
const double badC; // probability that member is untrustworthy
// Probability of forwarding
// const double PF = 0.8;
// const double notPF = 0.2; // must be 1-PF
// Probability that a crowd member is bad
// const double badC = 0.1;
// const double badC = 0.091;
// const double badC = 0.167;
// const double goodC = 0.909; // must be 1-badC
// const double goodC = 0.833; // must be 1-badC
const int CrowdSize = 5; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 10; // Total number of protocol runs to analyze
const int MaxGood=20; // CWDMAX: maximum number of good crowd members
// Process definitions
module crowds
// Auxiliary variables
launch: bool init true; // Start modeling?
newInstance: bool init false; // Initialize a new protocol instance?
runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances
start: bool init false; // Start the protocol?
run: bool init false; // Run the protocol?
lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg
good: bool init false; // Crowd member is good?
bad: bool init false; // ... bad?
recordLast: bool init false; // Record last seen crowd member?
badObserve: bool init false; // Bad members observes who sent msg?
deliver: bool init false; // Deliver message to destination?
done: bool init false; // Protocol instance finished?
// Counters for attackers' observations
// CWDMAX: 1 counter per each good crowd member
observe0: [0..TotalRuns];
observe1: [0..TotalRuns];
observe2: [0..TotalRuns];
observe3: [0..TotalRuns];
observe4: [0..TotalRuns];
observe5: [0..TotalRuns];
observe6: [0..TotalRuns];
observe7: [0..TotalRuns];
observe8: [0..TotalRuns];
observe9: [0..TotalRuns];
observe10: [0..TotalRuns];
observe11: [0..TotalRuns];
observe12: [0..TotalRuns];
observe13: [0..TotalRuns];
observe14: [0..TotalRuns];
observe15: [0..TotalRuns];
observe16: [0..TotalRuns];
observe17: [0..TotalRuns];
observe18: [0..TotalRuns];
observe19: [0..TotalRuns];
[] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false);
// Set up a newInstance protocol instance
[] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true);
// SENDER
// Start the protocol
[] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false);
// CROWD MEMBERS
// Good or bad crowd member?
[] !good & !bad & !deliver & run ->
1-badC : (good'=true) & (recordLast'=true) & (run'=false) +
badC : (bad'=true) & (badObserve'=true) & (run'=false);
// GOOD MEMBERS
// Forward with probability PF, else deliver
[] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true);
// Record the last crowd member who touched the msg;
// all good members may appear with equal probability
// Note: This is backward. In the real protocol, each honest
// forwarder randomly chooses the next forwarder.
// Here, the identity of an honest forwarder is randomly
// chosen *after* it has forwarded the message.
[] recordLast & CrowdSize=2 ->
1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=3 ->
1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=4 ->
1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=5 ->
1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=10 ->
1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=15 ->
1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=20 ->
1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true);
// BAD MEMBERS
// Remember from whom the message was received and deliver
// CWDMAX: 1 rule per each good crowd member
[] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
// RECIPIENT
// Delivery to destination
[] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false);
// Start a newInstance instance
[] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood);
endmodule
label "observe0Greater1" = observe0 > 1;

2
examples/pdtmc/crowds/crowds_5-5.pm
View File

@ -190,3 +190,5 @@ module crowds
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1;
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1;

33
examples/pdtmc/die/die.pm
View File

@ -1,33 +0,0 @@
// Knuth's model of a fair die using only fair coins
dtmc
const double coinProb;
module die
// local state
s : [0..7] init 0;
// value of the dice
d : [0..6] init 0;
[] s=0 -> coinProb : (s'=1) + (1-coinProb) : (s'=2);
[] s=1 -> coinProb : (s'=3) + (1-coinProb) : (s'=4);
[] s=2 -> coinProb : (s'=5) + (1-coinProb) : (s'=6);
[] s=3 -> coinProb : (s'=1) + (1-coinProb) : (s'=7) & (d'=1);
[] s=4 -> coinProb : (s'=7) & (d'=2) + (1-coinProb) : (s'=7) & (d'=3);
[] s=5 -> coinProb : (s'=7) & (d'=4) + (1-coinProb) : (s'=7) & (d'=5);
[] s=6 -> coinProb : (s'=2) + (1-coinProb) : (s'=7) & (d'=6);
[] s=7 -> 1: (s'=7);
endmodule
rewards "coin_flips"
[] s<7 : 1;
endrewards
label "one" = s=7&d=1;
label "two" = s=7&d=2;
label "three" = s=7&d=3;
label "four" = s=7&d=4;
label "five" = s=7&d=5;
label "six" = s=7&d=6;

4
examples/pdtmc/nand/nand_10-1.pm
View File

@ -67,11 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_10-2.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_10-3.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_10-4.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_10-5.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_20-1.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

4
examples/pdtmc/nand/nand_20-2.pm
View File

@ -67,11 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

5
examples/pdtmc/nand/nand_20-3.pm
View File

@ -67,10 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

4
examples/pdtmc/nand/nand_20-4.pm
View File

@ -67,11 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

4
examples/pdtmc/nand/nand_20-5.pm
View File

@ -67,11 +67,9 @@ module multiplex
endmodule
label "target" = s=4 & z/N<0.1;
label "end" = s=4;
// rewards: final value of gate
rewards
// [] s=0 & (c=N) & (u=M) : z/N;
s=0 & (c=N) & (u=M) : z/N;
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

151
src/stormParametric.cpp
View File

@ -35,88 +35,89 @@ void check() {
// Program Translation Time Measurement, Start
std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
// First, we build the model using the given symbolic model description and constant definitions.
std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename();
std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
if (storm::settings::generalSettings().isPropertySet()) {
formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
}
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString());
std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
// Convert the transition rewards to state rewards if necessary.
if (model->hasTransitionRewards()) {
model->convertTransitionRewardsToStateRewards();
}
// Program Translation Time Measurement, End
std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
model->printModelInformationToStream(std::cout);
if (formula) {
STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported.");
std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'.");
std::cout << "Checking formula " << *formula.get() << std::endl;
if (storm::settings::generalSettings().isSymbolicSet()) {
std::string programFile = storm::settings::generalSettings().getSymbolicModelFilename();
std::string constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get());
options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
*dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
dtmc->printModelInformationToStream(std::cout);
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
if (storm::settings::generalSettings().isPropertySet()) {
formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
}
STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong.");
storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
constraintCollector(*dtmc);
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString());
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get());
ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
// Convert the transition rewards to state rewards if necessary.
if (model->hasTransitionRewards()) {
model->convertTransitionRewardsToStateRewards();
}
// Report the result.
STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
result->writeToStream(std::cout, model->getInitialStates());
if (std::is_same<ValueType, storm::RationalFunction>::value) {
printApproximateResult(valueFunction);
}
std::cout << std::endl;
// Program Translation Time Measurement, End
std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
// Generate derivatives for sensitivity analysis if requested.
if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
auto allVariables = valueFunction.gatherVariables();
model->printModelInformationToStream(std::cout);
if (formula) {
STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported.");
std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
if (!allVariables.empty()) {
std::map<storm::Variable, storm::RationalFunction> derivatives;
for (auto const& variable : allVariables) {
derivatives[variable] = valueFunction.derivative(variable);
}
storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'.");
std::cout << "Checking formula " << *formula.get() << std::endl;
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get());
options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
*dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
dtmc->printModelInformationToStream(std::cout);
}
STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong.");
storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
constraintCollector(*dtmc);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get());
ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
}
// Report the result.
STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
result->writeToStream(std::cout, model->getInitialStates());
if (std::is_same<ValueType, storm::RationalFunction>::value) {
printApproximateResult(valueFunction);
}
std::cout << std::endl;
// Generate derivatives for sensitivity analysis if requested.
if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
auto allVariables = valueFunction.gatherVariables();
std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl;
for (auto const& variableDerivativePair : derivatives) {
std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl;
if (!allVariables.empty()) {
std::map<storm::Variable, storm::RationalFunction> derivatives;
for (auto const& variable : allVariables) {
derivatives[variable] = valueFunction.derivative(variable);
}
std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl;
for (auto const& variableDerivativePair : derivatives) {
std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl;
}
}
}
}
@ -128,17 +129,11 @@ void check() {
*/
int main(const int argc, const char** argv) {
try {
std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
storm::utility::cli::setUp();
storm::utility::cli::printHeader(argc, argv);
bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv);
if (!optionsCorrect) {
return -1;
}
check<storm::RationalFunction>();
std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms." << std::endl << std::endl;
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cli::cleanUp();

Write Preview
Loading…
Cancel
Save