diff --git a/examples/pdtmc/brp/brp_128-2.pm b/examples/pdtmc/brp/brp_128-2.pm index 94f893676..8e6651399 100644 --- a/examples/pdtmc/brp/brp_128-2.pm +++ b/examples/pdtmc/brp/brp_128-2.pm @@ -134,6 +134,4 @@ module channelL endmodule -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file +label "target" = s = 5; diff --git a/examples/pdtmc/brp/brp_128-3.pm b/examples/pdtmc/brp/brp_128-3.pm deleted file mode 100644 index dda40ac75..000000000 --- a/examples/pdtmc/brp/brp_128-3.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 128; -// maximum number of retransmissions -const int MAX = 3; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-4.pm b/examples/pdtmc/brp/brp_128-4.pm deleted file mode 100644 index 001df7ce4..000000000 --- a/examples/pdtmc/brp/brp_128-4.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 128; -// maximum number of retransmissions -const int MAX = 4; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_128-5.pm b/examples/pdtmc/brp/brp_128-5.pm index 373ec6d71..962953a09 100644 --- a/examples/pdtmc/brp/brp_128-5.pm +++ b/examples/pdtmc/brp/brp_128-5.pm @@ -135,6 +135,4 @@ module channelL endmodule -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file +label "target" = s = 5; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_16_2.pm b/examples/pdtmc/brp/brp_16_2.pm index 3b478303d..7be6c8130 100644 --- a/examples/pdtmc/brp/brp_16_2.pm +++ b/examples/pdtmc/brp/brp_16_2.pm @@ -134,6 +134,4 @@ module channelL endmodule -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file +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 index 3eeb36040..cf89c16bf 100644 --- a/examples/pdtmc/brp/brp_256-2.pm +++ b/examples/pdtmc/brp/brp_256-2.pm @@ -134,6 +134,4 @@ module channelL endmodule -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file +label "target" = s = 5; diff --git a/examples/pdtmc/brp/brp_256-3.pm b/examples/pdtmc/brp/brp_256-3.pm deleted file mode 100644 index 4b4a2dd9d..000000000 --- a/examples/pdtmc/brp/brp_256-3.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 256; -// maximum number of retransmissions -const int MAX = 3; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-4.pm b/examples/pdtmc/brp/brp_256-4.pm deleted file mode 100644 index 6c7dd7553..000000000 --- a/examples/pdtmc/brp/brp_256-4.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 256; -// maximum number of retransmissions -const int MAX = 4; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_256-5.pm b/examples/pdtmc/brp/brp_256-5.pm index cbcb4a6e1..456d710a0 100644 --- a/examples/pdtmc/brp/brp_256-5.pm +++ b/examples/pdtmc/brp/brp_256-5.pm @@ -134,6 +134,4 @@ module channelL endmodule -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file +label "target" = s = 5; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_32-4.pm b/examples/pdtmc/brp/brp_32-4.pm deleted file mode 100644 index 0bba62c8a..000000000 --- a/examples/pdtmc/brp/brp_32-4.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 32; -// maximum number of retransmissions -const int MAX = 4; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_64-4.pm b/examples/pdtmc/brp/brp_64-4.pm deleted file mode 100644 index df8641eb3..000000000 --- a/examples/pdtmc/brp/brp_64-4.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 64; -// maximum number of retransmissions -const int MAX = 4; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/brp/brp_64-5.pm b/examples/pdtmc/brp/brp_64-5.pm deleted file mode 100644 index c500d05a8..000000000 --- a/examples/pdtmc/brp/brp_64-5.pm +++ /dev/null @@ -1,139 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -dtmc - -// number of chunks -const int N = 64; -// maximum number of retransmissions -const int MAX = 5; - -// reliability of channels -const double pL; -const double pK; - -module sender - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [TO_Msg] (s=2) -> (s'=3); - [TO_Ack] (s=2) -> (s'=3); - // retransmit - [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); - [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -// prevents more than one file being sent -module tester - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - k : [0..2]; - - // idle - [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); - // sending - [aG] (k=1) -> (k'=0); - // lost - [TO_Msg] (k=2) -> (k'=0); - -endmodule - -module channelL - - l : [0..2]; - - // idle - [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); - // sending - [aB] (l=1) -> (l'=0); - // lost - [TO_Ack] (l=2) -> (l'=0); - -endmodule - -label "target" = s=5; -label "finished_with_success" = srep=3&rrep=3; -label "two_fragments_transmitted" = s=1&i=2+1; \ No newline at end of file diff --git a/examples/pdtmc/crowds/crowds_10-5.pm b/examples/pdtmc/crowds/crowds_10-5.pm index ab5dbd438..022e93948 100644 --- a/examples/pdtmc/crowds/crowds_10-5.pm +++ b/examples/pdtmc/crowds/crowds_10-5.pm @@ -190,4 +190,6 @@ module crowds endmodule label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1; diff --git a/examples/pdtmc/crowds/crowds_15-5.pm b/examples/pdtmc/crowds/crowds_15-5.pm index cc55c713b..994c2e2dd 100644 --- a/examples/pdtmc/crowds/crowds_15-5.pm +++ b/examples/pdtmc/crowds/crowds_15-5.pm @@ -189,4 +189,7 @@ module crowds endmodule -label "observe0Greater1" = observe0 > 1; \ No newline at end of file +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; + diff --git a/examples/pdtmc/crowds/crowds_20-5.pm b/examples/pdtmc/crowds/crowds_20-5.pm index d3adf6048..d235ff110 100644 --- a/examples/pdtmc/crowds/crowds_20-5.pm +++ b/examples/pdtmc/crowds/crowds_20-5.pm @@ -36,7 +36,7 @@ module crowds runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances start: bool init false; // Start the protocol? run: bool init false; // Run the protocol? - lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg + lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg good: bool init false; // Crowd member is good? bad: bool init false; // ... bad? recordLast: bool init false; // Record last seen crowd member? @@ -189,4 +189,6 @@ module crowds endmodule -label "observe0Greater1" = observe0 > 1; \ No newline at end of file +label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1; +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1; diff --git a/examples/pdtmc/crowds/crowds_3-5.pm b/examples/pdtmc/crowds/crowds_3-5.pm index 83b51ad27..f9eaf9f75 100644 --- a/examples/pdtmc/crowds/crowds_3-5.pm +++ b/examples/pdtmc/crowds/crowds_3-5.pm @@ -190,4 +190,5 @@ module crowds endmodule label "observe0Greater1" = observe0 > 1; - +label "observeIGreater1" = observe1>1|observe2>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1; diff --git a/examples/pdtmc/crowds/crowds_5-10.pm b/examples/pdtmc/crowds/crowds_5-10.pm deleted file mode 100644 index 0e7c45815..000000000 --- a/examples/pdtmc/crowds/crowds_5-10.pm +++ /dev/null @@ -1,193 +0,0 @@ -// CROWDS [Reiter,Rubin] -// Vitaly Shmatikov, 2002 -// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) - -// note: -// Change everything marked CWDSIZ when changing the size of the crowd -// Change everything marked CWDMAX when increasing max size of the crowd - -dtmc - -// Model parameters -const double PF; // forwarding probability -const double badC; // probability that member is untrustworthy - -// Probability of forwarding -// const double PF = 0.8; -// const double notPF = 0.2; // must be 1-PF - -// Probability that a crowd member is bad -// const double badC = 0.1; -// const double badC = 0.091; -// const double badC = 0.167; -// const double goodC = 0.909; // must be 1-badC -// const double goodC = 0.833; // must be 1-badC - -const int CrowdSize = 5; // CWDSIZ: actual number of good crowd members -const int TotalRuns = 10; // Total number of protocol runs to analyze -const int MaxGood=20; // CWDMAX: maximum number of good crowd members - -// Process definitions -module crowds - - // Auxiliary variables - launch: bool init true; // Start modeling? - newInstance: bool init false; // Initialize a new protocol instance? - runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances - start: bool init false; // Start the protocol? - run: bool init false; // Run the protocol? - lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg - good: bool init false; // Crowd member is good? - bad: bool init false; // ... bad? - recordLast: bool init false; // Record last seen crowd member? - badObserve: bool init false; // Bad members observes who sent msg? - deliver: bool init false; // Deliver message to destination? - done: bool init false; // Protocol instance finished? - - // Counters for attackers' observations - // CWDMAX: 1 counter per each good crowd member - observe0: [0..TotalRuns]; - observe1: [0..TotalRuns]; - observe2: [0..TotalRuns]; - observe3: [0..TotalRuns]; - observe4: [0..TotalRuns]; - observe5: [0..TotalRuns]; - observe6: [0..TotalRuns]; - observe7: [0..TotalRuns]; - observe8: [0..TotalRuns]; - observe9: [0..TotalRuns]; - observe10: [0..TotalRuns]; - observe11: [0..TotalRuns]; - observe12: [0..TotalRuns]; - observe13: [0..TotalRuns]; - observe14: [0..TotalRuns]; - observe15: [0..TotalRuns]; - observe16: [0..TotalRuns]; - observe17: [0..TotalRuns]; - observe18: [0..TotalRuns]; - observe19: [0..TotalRuns]; - - [] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false); - // Set up a newInstance protocol instance - [] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true); - - // SENDER - // Start the protocol - [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); - - // CROWD MEMBERS - // Good or bad crowd member? - [] !good & !bad & !deliver & run -> - 1-badC : (good'=true) & (recordLast'=true) & (run'=false) + - badC : (bad'=true) & (badObserve'=true) & (run'=false); - - // GOOD MEMBERS - // Forward with probability PF, else deliver - [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); - // Record the last crowd member who touched the msg; - // all good members may appear with equal probability - // Note: This is backward. In the real protocol, each honest - // forwarder randomly chooses the next forwarder. - // Here, the identity of an honest forwarder is randomly - // chosen *after* it has forwarded the message. - [] recordLast & CrowdSize=2 -> - 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=3 -> - 1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=4 -> - 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + - 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=5 -> - 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + - 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + - 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=10 -> - 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + - 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=15 -> - 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + - 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); - [] recordLast & CrowdSize=20 -> - 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + - 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); - - // BAD MEMBERS - // Remember from whom the message was received and deliver - // CWDMAX: 1 rule per each good crowd member - [] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - [] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false); - - // RECIPIENT - // Delivery to destination - [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); - // Start a newInstance instance - [] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); - -endmodule - -label "observe0Greater1" = observe0 > 1; - diff --git a/examples/pdtmc/crowds/crowds_5-5.pm b/examples/pdtmc/crowds/crowds_5-5.pm index 7471ea431..e936c45b7 100644 --- a/examples/pdtmc/crowds/crowds_5-5.pm +++ b/examples/pdtmc/crowds/crowds_5-5.pm @@ -190,3 +190,5 @@ module crowds endmodule label "observe0Greater1" = observe0 > 1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; diff --git a/examples/pdtmc/die/die.pm b/examples/pdtmc/die/die.pm deleted file mode 100644 index 032323827..000000000 --- a/examples/pdtmc/die/die.pm +++ /dev/null @@ -1,33 +0,0 @@ -// Knuth's model of a fair die using only fair coins -dtmc - -const double coinProb; - -module die - - // local state - s : [0..7] init 0; - // value of the dice - d : [0..6] init 0; - - [] s=0 -> coinProb : (s'=1) + (1-coinProb) : (s'=2); - [] s=1 -> coinProb : (s'=3) + (1-coinProb) : (s'=4); - [] s=2 -> coinProb : (s'=5) + (1-coinProb) : (s'=6); - [] s=3 -> coinProb : (s'=1) + (1-coinProb) : (s'=7) & (d'=1); - [] s=4 -> coinProb : (s'=7) & (d'=2) + (1-coinProb) : (s'=7) & (d'=3); - [] s=5 -> coinProb : (s'=7) & (d'=4) + (1-coinProb) : (s'=7) & (d'=5); - [] s=6 -> coinProb : (s'=2) + (1-coinProb) : (s'=7) & (d'=6); - [] s=7 -> 1: (s'=7); - -endmodule - -rewards "coin_flips" - [] s<7 : 1; -endrewards - -label "one" = s=7&d=1; -label "two" = s=7&d=2; -label "three" = s=7&d=3; -label "four" = s=7&d=4; -label "five" = s=7&d=5; -label "six" = s=7&d=6; diff --git a/examples/pdtmc/nand/nand_10-1.pm b/examples/pdtmc/nand/nand_10-1.pm index b889db7e8..f56664199 100644 --- a/examples/pdtmc/nand/nand_10-1.pm +++ b/examples/pdtmc/nand/nand_10-1.pm @@ -67,11 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards diff --git a/examples/pdtmc/nand/nand_10-2.pm b/examples/pdtmc/nand/nand_10-2.pm index 43b3f54c1..0708144e7 100644 --- a/examples/pdtmc/nand/nand_10-2.pm +++ b/examples/pdtmc/nand/nand_10-2.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_10-3.pm b/examples/pdtmc/nand/nand_10-3.pm index 96f4568e4..566251af3 100644 --- a/examples/pdtmc/nand/nand_10-3.pm +++ b/examples/pdtmc/nand/nand_10-3.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_10-4.pm b/examples/pdtmc/nand/nand_10-4.pm index 995e78f6b..7de796d1d 100644 --- a/examples/pdtmc/nand/nand_10-4.pm +++ b/examples/pdtmc/nand/nand_10-4.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_10-5.pm b/examples/pdtmc/nand/nand_10-5.pm index 2eddb28e9..2b1405c2f 100644 --- a/examples/pdtmc/nand/nand_10-5.pm +++ b/examples/pdtmc/nand/nand_10-5.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_20-1.pm b/examples/pdtmc/nand/nand_20-1.pm index fe8c89c3c..babaecbe3 100644 --- a/examples/pdtmc/nand/nand_20-1.pm +++ b/examples/pdtmc/nand/nand_20-1.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_20-2.pm b/examples/pdtmc/nand/nand_20-2.pm index 29ecfe36d..164a03e0f 100644 --- a/examples/pdtmc/nand/nand_20-2.pm +++ b/examples/pdtmc/nand/nand_20-2.pm @@ -67,11 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards diff --git a/examples/pdtmc/nand/nand_20-3.pm b/examples/pdtmc/nand/nand_20-3.pm index 08662ea7f..5131d1290 100644 --- a/examples/pdtmc/nand/nand_20-3.pm +++ b/examples/pdtmc/nand/nand_20-3.pm @@ -67,10 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards + diff --git a/examples/pdtmc/nand/nand_20-4.pm b/examples/pdtmc/nand/nand_20-4.pm index edcf7b5c6..047f8ac5e 100644 --- a/examples/pdtmc/nand/nand_20-4.pm +++ b/examples/pdtmc/nand/nand_20-4.pm @@ -67,11 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards diff --git a/examples/pdtmc/nand/nand_20-5.pm b/examples/pdtmc/nand/nand_20-5.pm index 2007fa413..2043bb018 100644 --- a/examples/pdtmc/nand/nand_20-5.pm +++ b/examples/pdtmc/nand/nand_20-5.pm @@ -67,11 +67,9 @@ module multiplex endmodule label "target" = s=4 & z/N<0.1; -label "end" = s=4; // rewards: final value of gate rewards - // [] s=0 & (c=N) & (u=M) : z/N; - s=0 & (c=N) & (u=M) : z/N; + [] s=0 & (c=N) & (u=M) : z/N; endrewards diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 9029597c1..bcc7e0d02 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -35,88 +35,89 @@ void check() { // Program Translation Time Measurement, Start std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now(); - // First, we build the model using the given symbolic model description and constant definitions. - std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename(); - std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); - storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - - boost::optional<std::shared_ptr<storm::logic::Formula>> formula; - if (storm::settings::generalSettings().isPropertySet()) { - formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); - } - - typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options; - if (formula) { - options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get()); - } - options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); - - std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options); - - // Convert the transition rewards to state rewards if necessary. - if (model->hasTransitionRewards()) { - model->convertTransitionRewardsToStateRewards(); - } - - // Program Translation Time Measurement, End - std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); - std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; - - model->printModelInformationToStream(std::cout); - - if (formula) { - STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported."); - std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>(); - - storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc); - STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'."); - - std::cout << "Checking formula " << *formula.get() << std::endl; + if (storm::settings::generalSettings().isSymbolicSet()) { + std::string programFile = storm::settings::generalSettings().getSymbolicModelFilename(); + std::string constants = storm::settings::generalSettings().getConstantDefinitionString(); + storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - // Perform bisimulation minimization if requested. - if (storm::settings::generalSettings().isBisimulationSet()) { - typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get()); - options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); - - storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options); - *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>()); - - dtmc->printModelInformationToStream(std::cout); + boost::optional<std::shared_ptr<storm::logic::Formula>> formula; + if (storm::settings::generalSettings().isPropertySet()) { + formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); } - STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong."); - - storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector; - constraintCollector(*dtmc); + typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options; + if (formula) { + options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get()); + } + options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); - std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get()); - ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]; + std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options); - if (storm::settings::parametricSettings().exportResultToFile()) { - storm::utility::exportParametricMcResult(valueFunction, constraintCollector); + // Convert the transition rewards to state rewards if necessary. + if (model->hasTransitionRewards()) { + model->convertTransitionRewardsToStateRewards(); } - // Report the result. - STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); - result->writeToStream(std::cout, model->getInitialStates()); - if (std::is_same<ValueType, storm::RationalFunction>::value) { - printApproximateResult(valueFunction); - } - std::cout << std::endl; + // Program Translation Time Measurement, End + std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); + std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; - // Generate derivatives for sensitivity analysis if requested. - if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) { - auto allVariables = valueFunction.gatherVariables(); + model->printModelInformationToStream(std::cout); + + if (formula) { + STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported."); + std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>(); - if (!allVariables.empty()) { - std::map<storm::Variable, storm::RationalFunction> derivatives; - for (auto const& variable : allVariables) { - derivatives[variable] = valueFunction.derivative(variable); - } + storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc); + STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'."); + + std::cout << "Checking formula " << *formula.get() << std::endl; + + // Perform bisimulation minimization if requested. + if (storm::settings::generalSettings().isBisimulationSet()) { + typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get()); + options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); + + storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options); + *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>()); + + dtmc->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong."); + + storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector; + constraintCollector(*dtmc); + + std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get()); + ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]; + + if (storm::settings::parametricSettings().exportResultToFile()) { + storm::utility::exportParametricMcResult(valueFunction, constraintCollector); + } + + // Report the result. + STORM_PRINT_AND_LOG(std::endl << "Result (initial state): "); + result->writeToStream(std::cout, model->getInitialStates()); + if (std::is_same<ValueType, storm::RationalFunction>::value) { + printApproximateResult(valueFunction); + } + std::cout << std::endl; + + // Generate derivatives for sensitivity analysis if requested. + if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) { + auto allVariables = valueFunction.gatherVariables(); - std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl; - for (auto const& variableDerivativePair : derivatives) { - std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl; + if (!allVariables.empty()) { + std::map<storm::Variable, storm::RationalFunction> derivatives; + for (auto const& variable : allVariables) { + derivatives[variable] = valueFunction.derivative(variable); + } + + std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl; + for (auto const& variableDerivativePair : derivatives) { + std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl; + } } } } @@ -128,17 +129,11 @@ void check() { */ int main(const int argc, const char** argv) { try { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); storm::utility::cli::setUp(); storm::utility::cli::printHeader(argc, argv); bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv); - if (!optionsCorrect) { - return -1; - } check<storm::RationalFunction>(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - std::cout << std::endl << "Total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms." << std::endl << std::endl; // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp();