From fe0f31a335d8205bf839bf9cd41308bba02b1157 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 31 Mar 2008 19:45:31 +0000 Subject: [PATCH] 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 | 26 +++++++++---------- prism-examples/leader/synchronous/leader.pctl | 2 +- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/prism-examples/embedded/embedded.csl b/prism-examples/embedded/embedded.csl index d35b9255..45278422 100644 --- a/prism-examples/embedded/embedded.csl +++ b/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" ] diff --git a/prism-examples/leader/synchronous/leader.pctl b/prism-examples/leader/synchronous/leader.pctl index f925fc31..4b443da5 100644 --- a/prism-examples/leader/synchronous/leader.pctl +++ b/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" ]