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

Added some new example files. 

Former-commit-id: e7f6d58ddf
main
dehnert 11 years ago
parent
5571e2111c
commit
f909387258
20 changed files with 2435 additions and 0 deletions
Split View
  1. BIN
      examples/.DS_Store
  2. BIN
      examples/pdtmc/.DS_Store
  3. 137
      examples/pdtmc/brp/brp_128-2.pm
  4. 137
      examples/pdtmc/brp/brp_128-3.pm
  5. 137
      examples/pdtmc/brp/brp_128-4.pm
  6. 138
      examples/pdtmc/brp/brp_128-5.pm
  7. 137
      examples/pdtmc/brp/brp_256-2.pm
  8. 137
      examples/pdtmc/brp/brp_256-3.pm
  9. 137
      examples/pdtmc/brp/brp_256-4.pm
  10. 137
      examples/pdtmc/brp/brp_256-5.pm
  11. 193
      examples/pdtmc/crowds/crowds_10-5.pm
  12. 192
      examples/pdtmc/crowds/crowds_15-5.pm
  13. 193
      examples/pdtmc/crowds/crowds_3-5.pm
  14. 193
      examples/pdtmc/crowds/crowds_5-10.pm
  15. 192
      examples/pdtmc/crowds/crowds_5-5.pm
  16. 75
      examples/pdtmc/nand/nand_20-1.pm
  17. 75
      examples/pdtmc/nand/nand_20-2.pm
  18. 75
      examples/pdtmc/nand/nand_20-3.pm
  19. 75
      examples/pdtmc/nand/nand_20-4.pm
  20. 75
      examples/pdtmc/nand/nand_20-5.pm

BIN
examples/.DS_Store
View File

BIN
examples/pdtmc/.DS_Store
View File

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

@ -0,0 +1,137 @@
// 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 = 2;
// 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;

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

@ -0,0 +1,137 @@
// 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;

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

@ -0,0 +1,137 @@
// 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;

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

@ -0,0 +1,138 @@
// 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 = 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;

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

@ -0,0 +1,137 @@
// 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 = 2;
// 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;

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

@ -0,0 +1,137 @@
// 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;

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

@ -0,0 +1,137 @@
// 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;

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

@ -0,0 +1,137 @@
// 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 = 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;

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

@ -0,0 +1,193 @@
// 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 = 0.167; // 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 = 10; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 5; // 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;

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

@ -0,0 +1,192 @@
// 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 = 15; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 5; // 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;

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

@ -0,0 +1,193 @@
// 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 = 3; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 5; // 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;

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

@ -0,0 +1,193 @@
// 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;

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

@ -0,0 +1,192 @@
// 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 = 5; // 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;

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

@ -0,0 +1,75 @@
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N = 20; // number of inputs in each bundle
const int K = 1; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr; //(0.02) probability nand works correctly
const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> (s'=s);
endmodule
label "target" = s=4 & z/N<0.1;
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

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

@ -0,0 +1,75 @@
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N = 20; // number of inputs in each bundle
const int K = 2; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr; //(0.02) probability nand works correctly
const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> (s'=s);
endmodule
label "target" = s=4 & z/N<0.1;
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

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

@ -0,0 +1,75 @@
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N = 20; // number of inputs in each bundle
const int K = 3; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr; //(0.02) probability nand works correctly
const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> (s'=s);
endmodule
label "target" = s=4 & z/N<0.1;
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

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

@ -0,0 +1,75 @@
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N = 20; // number of inputs in each bundle
const int K = 4; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr; //(0.02) probability nand works correctly
const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> (s'=s);
endmodule
label "target" = s=4 & z/N<0.1;
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards

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

@ -0,0 +1,75 @@
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N = 20; // number of inputs in each bundle
const int K = 5; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr; //(0.02) probability nand works correctly
const double prob1; //(0.9) probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> (s'=s);
endmodule
label "target" = s=4 & z/N<0.1;
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards
Write Preview
|||||||
100:0
Loading…
Cancel
Save