From add96619d079a1b4c98b33184ec87936345ba6ea Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 31 Dec 2020 16:41:56 +0000 Subject: [PATCH] Fix some examples/tests: duplicate actions not allowed in a state. --- prism-examples/pomdps/crypt/crypt3.prism | 11 +-- prism-examples/pomdps/crypt/crypt4.prism | 13 +-- prism-examples/pomdps/crypt/crypt5.prism | 15 ++-- prism-examples/pomdps/crypt/crypt6.prism | 17 ++-- prism-examples/poptas/pump/pump.prism | 4 +- .../poptas/repudiation/repudiation.prism | 2 +- .../repudiation/repudiation_complex.prism | 6 +- .../poptas/task_graph/task_graph.prism | 52 +++++++----- .../poptas/task_graph/task_graph_prob.prism | 80 +++++++++++-------- .../functionality/verify/pomdps/crypt3.prism | 11 +-- .../verify/poptas/pump_popta.prism | 4 +- .../verify/poptas/pump_popta_deadline.prism | 4 +- 12 files changed, 124 insertions(+), 95 deletions(-) diff --git a/prism-examples/pomdps/crypt/crypt3.prism b/prism-examples/pomdps/crypt/crypt3.prism index e2e43e17..0bf851e9 100644 --- a/prism-examples/pomdps/crypt/crypt3.prism +++ b/prism-examples/pomdps/crypt/crypt3.prism @@ -65,7 +65,7 @@ module crypt2 =crypt1[coin1=coin2, s1=s2, p1=p2, agree1=agree2, coin2=coin3, cho module crypt3 coin3 : [0..2]; - s3 : [0..1]; + s3 : [0..2]; agree3 : [0..1]; guess : [0..3]; correct : [0..1]; @@ -82,11 +82,12 @@ module crypt3 [choose3] s3=0 & coin3>0 & coin1>0 & !(coin3=coin1) & (pay=p3) -> (s3'=1) & (agree3'=1); // after everyone has announced guess who payed - [done] s3=1 & guess=0 -> (guess'=1); - [done] s3=1 & guess=0 -> (guess'=2); + [done] s3=1 -> (s3'=2); + [guess1] s3=2 & guess=0 -> (guess'=1); + [guess2] s3=2 & guess=0 -> (guess'=2); // check whether guessed correctly - [check] s3=1 & guess>0 & guess=pay -> (correct'=1); - [check] s3=1 & guess>0 & !(guess=pay) -> true; + [check] s3=2 & guess>0 & guess=pay -> (correct'=1); + [check] s3=2 & guess>0 & !(guess=pay) -> true; endmodule diff --git a/prism-examples/pomdps/crypt/crypt4.prism b/prism-examples/pomdps/crypt/crypt4.prism index 8825d02f..e8ea4526 100644 --- a/prism-examples/pomdps/crypt/crypt4.prism +++ b/prism-examples/pomdps/crypt/crypt4.prism @@ -68,7 +68,7 @@ module crypt3 =crypt1[coin1=coin3, s1=s3, p1=p3, agree1=agree3, coin2=coin4, cho module crypt4 coin4 : [0..2]; - s4 : [0..1]; + s4 : [0..2]; agree4 : [0..1]; guess : [0..3]; correct : [0..1]; @@ -85,12 +85,13 @@ module crypt4 [choose4] s4=0 & coin4>0 & coin1>0 & !(coin4=coin1) & (pay=p4) -> (s4'=1) & (agree4'=1); // after everyone has announced guess who payed - [done] s4=1 & guess=0 -> (guess'=1); - [done] s4=1 & guess=0 -> (guess'=2); - [done] s4=1 & guess=0 -> (guess'=3); + [done] s4=1 -> (s4'=2); + [guess1] s4=2 & guess=0 -> (guess'=1); + [guess2] s4=2 & guess=0 -> (guess'=2); + [guess3] s4=2 & guess=0 -> (guess'=3); // check whether guessed correctly - [check] s4=1 & guess>0 & guess=pay -> (correct'=1); - [check] s4=1 & guess>0 & !(guess=pay) -> true; + [check] s4=2 & guess>0 & guess=pay -> (correct'=1); + [check] s4=2 & guess>0 & !(guess=pay) -> true; endmodule diff --git a/prism-examples/pomdps/crypt/crypt5.prism b/prism-examples/pomdps/crypt/crypt5.prism index db7b9478..2d8b77dc 100644 --- a/prism-examples/pomdps/crypt/crypt5.prism +++ b/prism-examples/pomdps/crypt/crypt5.prism @@ -70,7 +70,7 @@ module crypt4 =crypt1[coin1=coin4, s1=s4, p1=p4, agree1=agree4, coin2=coin5, cho module crypt5 coin5 : [0..2]; - s5 : [0..1]; + s5 : [0..2]; agree5 : [0..1]; guess : [0..3]; correct : [0..1]; @@ -87,13 +87,14 @@ module crypt5 [choose5] s5=0 & coin5>0 & coin1>0 & !(coin5=coin1) & (pay=p5) -> (s5'=1) & (agree5'=1); // after everyone has announced guess who payed - [done] s5=1 & guess=0 -> (guess'=1); - [done] s5=1 & guess=0 -> (guess'=2); - [done] s5=1 & guess=0 -> (guess'=3); - [done] s5=1 & guess=0 -> (guess'=4); + [done] s5=1 -> (s5'=2); + [guess1] s5=2 & guess=0 -> (guess'=1); + [guess2] s5=2 & guess=0 -> (guess'=2); + [guess3] s5=2 & guess=0 -> (guess'=3); + [guess4] s5=2 & guess=0 -> (guess'=4); // check whether guessed correctly - [check] s5=1 & guess>0 & guess=pay -> (correct'=1); - [check] s5=1 & guess>0 & !(guess=pay) -> true; + [check] s5=2 & guess>0 & guess=pay -> (correct'=1); + [check] s5=2 & guess>0 & !(guess=pay) -> true; endmodule diff --git a/prism-examples/pomdps/crypt/crypt6.prism b/prism-examples/pomdps/crypt/crypt6.prism index 3f989b11..bc0bd809 100644 --- a/prism-examples/pomdps/crypt/crypt6.prism +++ b/prism-examples/pomdps/crypt/crypt6.prism @@ -72,7 +72,7 @@ module crypt5 =crypt1[coin1=coin5, s1=s5, p1=p5, agree1=agree5, coin2=coin6, cho module crypt6 coin6 : [0..2]; - s6 : [0..1]; + s6 : [0..2]; agree6 : [0..1]; guess : [0..5]; correct : [0..1]; @@ -89,14 +89,15 @@ module crypt6 [choose6] s6=0 & coin6>0 & coin1>0 & !(coin6=coin1) & (pay=p6) -> (s6'=1) & (agree6'=1); // after everyone has announced guess who payed - [done] s6=1 & guess=0 -> (guess'=1); - [done] s6=1 & guess=0 -> (guess'=2); - [done] s6=1 & guess=0 -> (guess'=3); - [done] s6=1 & guess=0 -> (guess'=4); - [done] s6=1 & guess=0 -> (guess'=5); + [done] s6=1 -> (s6'=2); + [guess1] s6=2 & guess=0 -> (guess'=1); + [guess2] s6=2 & guess=0 -> (guess'=2); + [guess3] s6=2 & guess=0 -> (guess'=3); + [guess4] s6=2 & guess=0 -> (guess'=4); + [guess5] s6=2 & guess=0 -> (guess'=5); // check whether guessed correctly - [check] s6=1 & guess>0 & guess=pay -> (correct'=1); - [check] s6=1 & guess>0 & !(guess=pay) -> true; + [check] s6=2 & guess>0 & guess=pay -> (correct'=1); + [check] s6=2 & guess>0 & !(guess=pay) -> true; endmodule diff --git a/prism-examples/poptas/pump/pump.prism b/prism-examples/poptas/pump/pump.prism index 85c6c832..aeda601e 100644 --- a/prism-examples/poptas/pump/pump.prism +++ b/prism-examples/poptas/pump/pump.prism @@ -104,8 +104,8 @@ module low [nack_l] l=1 & x=Tout -> (l'=0) & (x'=0); // timeout (nack) // when finished sending immediately guess value high was trying to send - [] l=2 & guess=-1 & x=0 -> (guess'=0); - [] l=2 & guess=-1 & x=0 -> (guess'=1); + [guess0] l=2 & guess=-1 & x=0 -> (guess'=0); + [guess1] l=2 & guess=-1 & x=0 -> (guess'=1); // and then immediately check if it is correct [] l=2 & guess>=0 & guess=bit & x=0 -> (l'=3) & (correct'=1); [] l=2 & guess>=0 & guess!=bit & x=0 -> (l'=3); diff --git a/prism-examples/poptas/repudiation/repudiation.prism b/prism-examples/poptas/repudiation/repudiation.prism index caa79992..3b6d4dbe 100644 --- a/prism-examples/poptas/repudiation/repudiation.prism +++ b/prism-examples/poptas/repudiation/repudiation.prism @@ -88,7 +88,7 @@ module originator [ack] o=2 & ack (o'=1) & (ack'=min(ack+1,K)) & (x'=0); // not last [ack] o=2 & ack=N-1 & x<=AD -> (o'=3) & (ack'=min(ack+1,K)) & (x'=0); // last // no ack arrives within time bound - [] o=2 & x>=AD -> (o'=3) & (x'=0); // ack not arrived within expected interval (stop) + [noack] o=2 & x>=AD -> (o'=3) & (x'=0); // ack not arrived within expected interval (stop) endmodule diff --git a/prism-examples/poptas/repudiation/repudiation_complex.prism b/prism-examples/poptas/repudiation/repudiation_complex.prism index c739db4b..4c0a43fb 100644 --- a/prism-examples/poptas/repudiation/repudiation_complex.prism +++ b/prism-examples/poptas/repudiation/repudiation_complex.prism @@ -88,7 +88,7 @@ module originator [ack] o=2 & ack (o'=1) & (ack'=min(ack+1,K)) & (x'=0); // not last [ack] o=2 & ack=N-1 & x<=AD -> (o'=3) & (ack'=min(ack+1,K)) & (x'=0); // last // no ack arrives within time bound - [] o=2 & x>=AD -> (o'=4) & (x'=0); // ack not arrived within expected interval (stop) + [noack] o=2 & x>=AD -> (o'=4) & (x'=0); // ack not arrived within expected interval (stop) endmodule @@ -124,8 +124,8 @@ module malicious_recipient [ack] r=2 & y>=ad -> (r'=1); // send ack // try and decode - [] r=2 -> (r'=3); // decode probabilistically - [] r=2 -> (r'=4); // decode correctly + [decp] r=2 -> (r'=3); // decode probabilistically + [dec] r=2 -> (r'=4); // decode correctly // decoding probabilistically (if fails can try again or send ack) [] r=3 & y>=3 -> 0.75 : (r'=2) & (y'=0) + 0.25 : (r'=5) & (y'=0); diff --git a/prism-examples/poptas/task_graph/task_graph.prism b/prism-examples/poptas/task_graph/task_graph.prism index e70059b7..d576c85b 100644 --- a/prism-examples/poptas/task_graph/task_graph.prism +++ b/prism-examples/poptas/task_graph/task_graph.prism @@ -25,28 +25,28 @@ module scheduler task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)) // start task 1 - [p1_add] task1=0 -> (task1'=1); - [p2_add] task1=0 -> (task1'=2); + [p1_add1] task1=0 -> (task1'=1); + [p2_add1] task1=0 -> (task1'=2); // start task 2 - [p1_mult] task2=0 -> (task2'=1); - [p2_mult] task2=0 -> (task2'=2); + [p1_mult2] task2=0 -> (task2'=1); + [p2_mult2] task2=0 -> (task2'=2); // start task 3 (must wait for task 1 to complete) - [p1_mult] task3=0 & task1=3 -> (task3'=1); - [p2_mult] task3=0 & task1=3 -> (task3'=2); + [p1_mult3] task3=0 & task1=3 -> (task3'=1); + [p2_mult3] task3=0 & task1=3 -> (task3'=2); // start task 4 (must wait for tasks 1 and 2 to complete) - [p1_add] task4=0 & task1=3 & task2=3 -> (task4'=1); - [p2_add] task4=0 & task1=3 & task2=3 -> (task4'=2); + [p1_add4] task4=0 & task1=3 & task2=3 -> (task4'=1); + [p2_add4] task4=0 & task1=3 & task2=3 -> (task4'=2); // start task 5 (must wait for task 3 to complete) - [p1_mult] task5=0 & task3=3 -> (task5'=1); - [p2_mult] task5=0 & task3=3 -> (task5'=2); + [p1_mult5] task5=0 & task3=3 -> (task5'=1); + [p2_mult5] task5=0 & task3=3 -> (task5'=2); // start task 6 (must wait for tasks 4 and 5 to complete) - [p1_add] task6=0 & task4=3 & task5=3 -> (task6'=1); - [p2_add] task6=0 & task4=3 & task5=3 -> (task6'=2); + [p1_add6] task6=0 & task4=3 & task5=3 -> (task6'=1); + [p2_add6] task6=0 & task4=3 & task5=3 -> (task6'=2); // a task finishes on processor 1 [p1_done] task1=1 -> (task1'=3); @@ -91,16 +91,24 @@ module P1 [start] p1=0 -> 0.5 : (p1'=1) & (sleep1'=0) + 0.5 : (p1'=1) & (sleep1'=1); // start from sleep state - [p1_add] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add - [p1_mult] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_add1] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_add4] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_add6] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_mult2] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_mult3] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_mult5] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply // start from idle state - [p1_add] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add - [p1_mult] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_add1] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_add4] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_add6] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_mult2] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_mult3] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_mult5] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply // wake from sleep - [] p1=2 & x1=4 -> (p1'=4) & (x1'=0); // add - [] p1=3 & x1=4 -> (p1'=5) & (x1'=0); // multiply + [p1] p1=2 & x1=4 -> (p1'=4) & (x1'=0); // add + [p1] p1=3 & x1=4 -> (p1'=5) & (x1'=0); // multiply // finish [p1_done] p1=4 & x1=2 -> (1-sleep) : (p1'=1) @@ -122,8 +130,12 @@ module P2 endinvariant // start - [p2_add] p2=0 -> (p2'=1) & (x2'=0); // add - [p2_mult] p2=0 -> (p2'=2) & (x2'=0); // multiply + [p2_add1] p2=0 -> (p2'=1) & (x2'=0); // add + [p2_add4] p2=0 -> (p2'=1) & (x2'=0); // add + [p2_add6] p2=0 -> (p2'=1) & (x2'=0); // add + [p2_mult2] p2=0 -> (p2'=2) & (x2'=0); // multiply + [p2_mult3] p2=0 -> (p2'=2) & (x2'=0); // multiply + [p2_mult5] p2=0 -> (p2'=2) & (x2'=0); // multiply // finish [p2_done] p2=1 & x2=5 -> (p2'=0); // add diff --git a/prism-examples/poptas/task_graph/task_graph_prob.prism b/prism-examples/poptas/task_graph/task_graph_prob.prism index b903b26b..c183b5ec 100644 --- a/prism-examples/poptas/task_graph/task_graph_prob.prism +++ b/prism-examples/poptas/task_graph/task_graph_prob.prism @@ -25,28 +25,28 @@ module scheduler task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)) // start task 1 - [p1_add] task1=0 -> (task1'=1); - [p2_add] task1=0 -> (task1'=2); + [p1_add1] task1=0 -> (task1'=1); + [p2_add1] task1=0 -> (task1'=2); // start task 2 - [p1_mult] task2=0 -> (task2'=1); - [p2_mult] task2=0 -> (task2'=2); + [p1_mult2] task2=0 -> (task2'=1); + [p2_mult2] task2=0 -> (task2'=2); // start task 3 (must wait for task 1 to complete) - [p1_mult] task3=0 & task1=3 -> (task3'=1); - [p2_mult] task3=0 & task1=3 -> (task3'=2); + [p1_mult3] task3=0 & task1=3 -> (task3'=1); + [p2_mult3] task3=0 & task1=3 -> (task3'=2); // start task 4 (must wait for tasks 1 and 2 to complete) - [p1_add] task4=0 & task1=3 & task2=3 -> (task4'=1); - [p2_add] task4=0 & task1=3 & task2=3 -> (task4'=2); + [p1_add4] task4=0 & task1=3 & task2=3 -> (task4'=1); + [p2_add4] task4=0 & task1=3 & task2=3 -> (task4'=2); // start task 5 (must wait for task 3 to complete) - [p1_mult] task5=0 & task3=3 -> (task5'=1); - [p2_mult] task5=0 & task3=3 -> (task5'=2); + [p1_mult5] task5=0 & task3=3 -> (task5'=1); + [p2_mult5] task5=0 & task3=3 -> (task5'=2); // start task 6 (must wait for tasks 4 and 5 to complete) - [p1_add] task6=0 & task4=3 & task5=3 -> (task6'=1); - [p2_add] task6=0 & task4=3 & task5=3 -> (task6'=2); + [p1_add6] task6=0 & task4=3 & task5=3 -> (task6'=1); + [p2_add6] task6=0 & task4=3 & task5=3 -> (task6'=2); // a task finishes on processor 1 [p1_done] task1=1 -> (task1'=3); @@ -96,30 +96,38 @@ module P1 [start] p1=0 -> 0.5 : (p1'=1) & (sleep1'=0) + 0.5 : (p1'=1) & (sleep1'=1); // start from sleep state - [p1_add] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add - [p1_mult] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_add1] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_add4] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_add6] p1=1 & sleep1=1 -> (p1'=2) & (x1'=0) & (sleep1'=0); // add + [p1_mult2] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_mult3] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply + [p1_mult5] p1=1 & sleep1=1 -> (p1'=3) & (x1'=0) & (sleep1'=0); // multiply // start from idle state - [p1_add] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add - [p1_mult] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_add1] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_add4] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_add6] p1=1 & sleep1=0 -> (p1'=4) & (x1'=0); // add + [p1_mult2] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_mult3] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply + [p1_mult5] p1=1 & sleep1=0 -> (p1'=5) & (x1'=0); // multiply // wake from sleep - [] p1=2 & x1=4 -> (p1'=4) & (x1'=0); // add - [] p1=3 & x1=4 -> (p1'=5) & (x1'=0); // multiply + [p1] p1=2 & x1=4 -> (p1'=4) & (x1'=0); // add + [p1] p1=3 & x1=4 -> (p1'=5) & (x1'=0); // multiply // adding - [] p1=4 & x1=1 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0) - + 2/3 : (c1'=1) & (x1'=0); - [] p1=4 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0) - + 1/2 : (c1'=2) & (x1'=0); - [] p1=4 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0); + [p1] p1=4 & x1=1 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0) + + 2/3 : (c1'=1) & (x1'=0); + [p1] p1=4 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0) + + 1/2 : (c1'=2) & (x1'=0); + [p1] p1=4 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0); // multiplying - [] p1=5 & x1=2 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0) - + 2/3 : (c1'=1) & (x1'=0); - [] p1=5 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0) - + 1/2 : (c1'=2) & (x1'=0); - [] p1=5 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0); + [p1] p1=5 & x1=2 & c1=0 -> 1/3 : (p1'=6) & (x1'=0) & (c1'=0) + + 2/3 : (c1'=1) & (x1'=0); + [p1] p1=5 & x1=1 & c1=1 -> 1/2 : (p1'=6) & (x1'=0) & (c1'=0) + + 1/2 : (c1'=2) & (x1'=0); + [p1] p1=5 & x1=1 & c1=2 -> (p1'=6) & (x1'=0) & (c1'=0); // done [p1_done] p1=6 -> (1-sleep) : (p1'=1) + sleep : (p1'=1) & (sleep1'=1); @@ -143,15 +151,19 @@ module P2 endinvariant // addition - [p2_add] (p2=0) -> (p2'=1) & (x2'=0); // start - [] (p2=1) & (x2=4) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); - [] (p2=1) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); + [p2_add1] (p2=0) -> (p2'=1) & (x2'=0); // start + [p2_add4] (p2=0) -> (p2'=1) & (x2'=0); // start + [p2_add6] (p2=0) -> (p2'=1) & (x2'=0); // start + [p2] (p2=1) & (x2=4) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); + [p2] (p2=1) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); [p2_done] (p2=1) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0); // multi - [p2_mult] (p2=0) -> (p2'=2) & (x2'=0); // start - [] (p2=2) & (x2=6) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); - [] (p2=2) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); + [p2_mult2] (p2=0) -> (p2'=2) & (x2'=0); // start + [p2_mult3] (p2=0) -> (p2'=2) & (x2'=0); // start + [p2_mult5] (p2=0) -> (p2'=2) & (x2'=0); // start + [p2] (p2=2) & (x2=6) & (c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0); + [p2] (p2=2) & (x2=1) & (c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0); [p2_done] (p2=2) & (x2=1) & (c2=2) -> (p2'=0) & (x2'=0) & (c2'=0); // done diff --git a/prism-tests/functionality/verify/pomdps/crypt3.prism b/prism-tests/functionality/verify/pomdps/crypt3.prism index e2e43e17..0bf851e9 100644 --- a/prism-tests/functionality/verify/pomdps/crypt3.prism +++ b/prism-tests/functionality/verify/pomdps/crypt3.prism @@ -65,7 +65,7 @@ module crypt2 =crypt1[coin1=coin2, s1=s2, p1=p2, agree1=agree2, coin2=coin3, cho module crypt3 coin3 : [0..2]; - s3 : [0..1]; + s3 : [0..2]; agree3 : [0..1]; guess : [0..3]; correct : [0..1]; @@ -82,11 +82,12 @@ module crypt3 [choose3] s3=0 & coin3>0 & coin1>0 & !(coin3=coin1) & (pay=p3) -> (s3'=1) & (agree3'=1); // after everyone has announced guess who payed - [done] s3=1 & guess=0 -> (guess'=1); - [done] s3=1 & guess=0 -> (guess'=2); + [done] s3=1 -> (s3'=2); + [guess1] s3=2 & guess=0 -> (guess'=1); + [guess2] s3=2 & guess=0 -> (guess'=2); // check whether guessed correctly - [check] s3=1 & guess>0 & guess=pay -> (correct'=1); - [check] s3=1 & guess>0 & !(guess=pay) -> true; + [check] s3=2 & guess>0 & guess=pay -> (correct'=1); + [check] s3=2 & guess>0 & !(guess=pay) -> true; endmodule diff --git a/prism-tests/functionality/verify/poptas/pump_popta.prism b/prism-tests/functionality/verify/poptas/pump_popta.prism index 2c1faf50..436aa864 100644 --- a/prism-tests/functionality/verify/poptas/pump_popta.prism +++ b/prism-tests/functionality/verify/poptas/pump_popta.prism @@ -104,8 +104,8 @@ module low [nack_l] l=1 & x=Tout -> (l'=0) & (x'=0); // timeout (nack) // when finished sending immediately guess value high was trying to send - [] l=2 & guess=-1 & x=0 -> (guess'=0); - [] l=2 & guess=-1 & x=0 -> (guess'=1); + [guess0] l=2 & guess=-1 & x=0 -> (guess'=0); + [guess1] l=2 & guess=-1 & x=0 -> (guess'=1); // and then immediately check if it is correct [] l=2 & guess>=0 & guess=bit & x=0 -> (l'=3) & (correct'=1); [] l=2 & guess>=0 & guess!=bit & x=0 -> (l'=3); diff --git a/prism-tests/functionality/verify/poptas/pump_popta_deadline.prism b/prism-tests/functionality/verify/poptas/pump_popta_deadline.prism index 43869836..60a8c0e2 100644 --- a/prism-tests/functionality/verify/poptas/pump_popta_deadline.prism +++ b/prism-tests/functionality/verify/poptas/pump_popta_deadline.prism @@ -61,8 +61,8 @@ module low [ack_l] l=1&m (l'=0) & (m'=m+1) & (x'=0); [ack_l] l=1&m=N&x<=Tout -> (l'=2) & (x'=0); [nack_l] l=1&x=Tout -> (l'=0) & (x'=0); - [] l=2&guess=-1&x=0 -> (guess'=0); - [] l=2&guess=-1&x=0 -> (guess'=1); + [guess0] l=2&guess=-1&x=0 -> (guess'=0); + [guess1] l=2&guess=-1&x=0 -> (guess'=1); [] l=2&guess>=0&guess=bit&x=0&t<=D -> (l'=3) & (correct'=1); [] l=2&guess>=0&guess!=bit&x=0&t<=D -> (l'=3); [time] (l=0=>x+1<=0)&(l=1=>x+1<=Tout)&(l=2=>x+1<=0)&(l=3=>true) -> 1.0 : (x'=min(x+1, 11));