Added parentheses to non-trivial time bounds.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@714 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/embedded/embedded.csl

@@ -12,22 +12,22 @@ label "danger" = !down & (i=1 | o=1); // transient fault has occured
 label "up" = !down & !danger; // system is operational
 
 // Probability of any failure occurring within T hours
-P=? [ true U<=T*3600 "down" ]
+P=? [ true U<=(T*3600) "down" ]
 
 // Probability of each failure type occurring first (within T hours)
-P=? [ !"down" U<=T*3600 "fail_sensors" ]
-P=? [ !"down" U<=T*3600 "fail_actuators" ]
-P=? [ !"down" U<=T*3600 "fail_io" ]
-P=? [ !"down" U<=T*3600 "fail_main" ]
+P=? [ !"down" U<=(T*3600) "fail_sensors" ]
+P=? [ !"down" U<=(T*3600) "fail_actuators" ]
+P=? [ !"down" U<=(T*3600) "fail_io" ]
+P=? [ !"down" U<=(T*3600) "fail_main" ]
 
 // Probability of any failure occurring within T days
-P=? [ true U<=T*3600*24 "down" ]
+P=? [ true U<=(T*3600*24) "down" ]
 
 // Probability of each failure type occurring first (within T days)
-P=? [ !"down" U<=T*3600*24 "fail_sensors" ]
-P=? [ !"down" U<=T*3600*24 "fail_actuators" ]
-P=? [ !"down" U<=T*3600*24 "fail_io" ]
-P=? [ !"down" U<=T*3600*24 "fail_main" ]
+P=? [ !"down" U<=(T*3600*24) "fail_sensors" ]
+P=? [ !"down" U<=(T*3600*24) "fail_actuators" ]
+P=? [ !"down" U<=(T*3600*24) "fail_io" ]
+P=? [ !"down" U<=(T*3600*24) "fail_main" ]
 
 
 // Long-run probability of each failure type occurring
@@ -37,9 +37,9 @@ P=? [ !"down" U "fail_io" ]
 P=? [ !"down" U "fail_main" ]
 
 // Expected time spent in "up"/"danger"/"down" by time T
-R{"up"}=? [ C<=T*3600 ]
-R{"danger"}=? [ C<=T*3600 ]
-R{"down"}=? [ C<=T*3600 ]
+R{"up"}=? [ C<=(T*3600) ]
+R{"danger"}=? [ C<=(T*3600) ]
+R{"down"}=? [ C<=(T*3600) ]
 
 // Expected time spent in "up"/"danger" before "down"
 R{"up"}=? [ F "down" ]

prism-examples/leader/synchronous/leader.pctl

@@ -4,7 +4,7 @@ const int L;
 P=? [ F "elected" ]
 
 // Probability that a leader is elected within L rounds
-P=? [ F<=L*(N+1) "elected" ]
+P=? [ F<=(L*(N+1)) "elected" ]
 
 // Expected time (num. rounds) to elect a leader
 R{"num_rounds"}=? [ F "elected" ]