diff --git a/examples/.DS_Store b/examples/.DS_Store new file mode 100644 index 000000000..ebf6cdce9 Binary files /dev/null and b/examples/.DS_Store differ diff --git a/examples/pdtmc/.DS_Store b/examples/pdtmc/.DS_Store new file mode 100644 index 000000000..583f89c5f Binary files /dev/null and b/examples/pdtmc/.DS_Store differ diff --git a/examples/pdtmc/brp/brp_128-2.pm b/examples/pdtmc/brp/brp_128-2.pm new file mode 100644 index 000000000..0a408fd03 --- /dev/null +++ b/examples/pdtmc/brp/brp_128-2.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-3.pm b/examples/pdtmc/brp/brp_128-3.pm new file mode 100644 index 000000000..9c42792b9 --- /dev/null +++ b/examples/pdtmc/brp/brp_128-3.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-4.pm b/examples/pdtmc/brp/brp_128-4.pm new file mode 100644 index 000000000..c71199649 --- /dev/null +++ b/examples/pdtmc/brp/brp_128-4.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-5.pm b/examples/pdtmc/brp/brp_128-5.pm new file mode 100644 index 000000000..962953a09 --- /dev/null +++ b/examples/pdtmc/brp/brp_128-5.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-2.pm b/examples/pdtmc/brp/brp_256-2.pm new file mode 100644 index 000000000..2e0780909 --- /dev/null +++ b/examples/pdtmc/brp/brp_256-2.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-3.pm b/examples/pdtmc/brp/brp_256-3.pm new file mode 100644 index 000000000..5b62bc35e --- /dev/null +++ b/examples/pdtmc/brp/brp_256-3.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-4.pm b/examples/pdtmc/brp/brp_256-4.pm new file mode 100644 index 000000000..d0300b04e --- /dev/null +++ b/examples/pdtmc/brp/brp_256-4.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-5.pm b/examples/pdtmc/brp/brp_256-5.pm new file mode 100644 index 000000000..456d710a0 --- /dev/null +++ b/examples/pdtmc/brp/brp_256-5.pm @@ -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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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; \ No newline at end of file diff --git a/examples/pdtmc/crowds/crowds_10-5.pm b/examples/pdtmc/crowds/crowds_10-5.pm new file mode 100644 index 000000000..dcf6e7930 --- /dev/null +++ b/examples/pdtmc/crowds/crowds_10-5.pm @@ -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 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (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; + diff --git a/examples/pdtmc/crowds/crowds_15-5.pm b/examples/pdtmc/crowds/crowds_15-5.pm new file mode 100644 index 000000000..cc55c713b --- /dev/null +++ b/examples/pdtmc/crowds/crowds_15-5.pm @@ -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 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (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; \ No newline at end of file diff --git a/examples/pdtmc/crowds/crowds_3-5.pm b/examples/pdtmc/crowds/crowds_3-5.pm new file mode 100644 index 000000000..83b51ad27 --- /dev/null +++ b/examples/pdtmc/crowds/crowds_3-5.pm @@ -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 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (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; + diff --git a/examples/pdtmc/crowds/crowds_5-10.pm b/examples/pdtmc/crowds/crowds_5-10.pm new file mode 100644 index 000000000..0e7c45815 --- /dev/null +++ b/examples/pdtmc/crowds/crowds_5-10.pm @@ -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 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (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; + diff --git a/examples/pdtmc/crowds/crowds_5-5.pm b/examples/pdtmc/crowds/crowds_5-5.pm new file mode 100644 index 000000000..7471ea431 --- /dev/null +++ b/examples/pdtmc/crowds/crowds_5-5.pm @@ -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 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (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; diff --git a/examples/pdtmc/nand/nand_20-1.pm b/examples/pdtmc/nand/nand_20-1.pm new file mode 100644 index 000000000..babaecbe3 --- /dev/null +++ b/examples/pdtmc/nand/nand_20-1.pm @@ -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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 + diff --git a/examples/pdtmc/nand/nand_20-2.pm b/examples/pdtmc/nand/nand_20-2.pm new file mode 100644 index 000000000..164a03e0f --- /dev/null +++ b/examples/pdtmc/nand/nand_20-2.pm @@ -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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 + diff --git a/examples/pdtmc/nand/nand_20-3.pm b/examples/pdtmc/nand/nand_20-3.pm new file mode 100644 index 000000000..5131d1290 --- /dev/null +++ b/examples/pdtmc/nand/nand_20-3.pm @@ -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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 + diff --git a/examples/pdtmc/nand/nand_20-4.pm b/examples/pdtmc/nand/nand_20-4.pm new file mode 100644 index 000000000..047f8ac5e --- /dev/null +++ b/examples/pdtmc/nand/nand_20-4.pm @@ -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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 + diff --git a/examples/pdtmc/nand/nand_20-5.pm b/examples/pdtmc/nand/nand_20-5.pm new file mode 100644 index 000000000..2043bb018 --- /dev/null +++ b/examples/pdtmc/nand/nand_20-5.pm @@ -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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 +