From 54507afd74f3e413e1f54179cb289ce49663cb69 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 5 Feb 2024 23:14:14 +0100 Subject: [PATCH] Added command line option for precision; TAC models Q1/Q2/case studies --- .../{dpm-b => dpm-large}/easy.props | 0 .../{dpm-b => dpm-large}/lost.props | 0 .../{dpm-b => dpm-large}/power.props | 0 .../{dpm-b => dpm-large}/sketch.props | 0 .../{dpm-b => dpm-large}/sketch.templ | 0 models/tac24/dpm-demo/sketch.templ | 8 +- models/tac24/dpm/sketch.props | 2 + models/tac24/dpm/sketch.templ | 259 ++++++++++++++++++ models/tac24/grid-10-sl-4fsc/easy.props | 1 - models/tac24/grid-av-4fsc/easy.props | 1 - .../sketch.props | 0 .../sketch.templ | 2 +- .../tac24/{grid-av-4fsc => grid}/sketch.props | 0 .../tac24/{grid-av-4fsc => grid}/sketch.templ | 0 models/tac24/herman/sketch.props | 1 + models/tac24/herman/sketch.templ | 240 ++++++++++++++++ models/tac24/maze/sketch.props | 1 + models/tac24/maze/sketch.templ | 209 ++++++++++++++ paynt/cli.py | 8 +- paynt/parser/sketch.py | 4 +- 20 files changed, 725 insertions(+), 11 deletions(-) rename models/tac24/case-studies/{dpm-b => dpm-large}/easy.props (100%) rename models/tac24/case-studies/{dpm-b => dpm-large}/lost.props (100%) rename models/tac24/case-studies/{dpm-b => dpm-large}/power.props (100%) rename models/tac24/case-studies/{dpm-b => dpm-large}/sketch.props (100%) rename models/tac24/case-studies/{dpm-b => dpm-large}/sketch.templ (100%) create mode 100644 models/tac24/dpm/sketch.props create mode 100644 models/tac24/dpm/sketch.templ delete mode 100644 models/tac24/grid-10-sl-4fsc/easy.props delete mode 100644 models/tac24/grid-av-4fsc/easy.props rename models/tac24/{grid-meet-2fsc => grid-meet-sl-2fsc}/sketch.props (100%) rename models/tac24/{grid-meet-2fsc => grid-meet-sl-2fsc}/sketch.templ (99%) rename models/tac24/{grid-av-4fsc => grid}/sketch.props (100%) rename models/tac24/{grid-av-4fsc => grid}/sketch.templ (100%) create mode 100644 models/tac24/herman/sketch.props create mode 100644 models/tac24/herman/sketch.templ create mode 100644 models/tac24/maze/sketch.props create mode 100644 models/tac24/maze/sketch.templ diff --git a/models/tac24/case-studies/dpm-b/easy.props b/models/tac24/case-studies/dpm-large/easy.props similarity index 100% rename from models/tac24/case-studies/dpm-b/easy.props rename to models/tac24/case-studies/dpm-large/easy.props diff --git a/models/tac24/case-studies/dpm-b/lost.props b/models/tac24/case-studies/dpm-large/lost.props similarity index 100% rename from models/tac24/case-studies/dpm-b/lost.props rename to models/tac24/case-studies/dpm-large/lost.props diff --git a/models/tac24/case-studies/dpm-b/power.props b/models/tac24/case-studies/dpm-large/power.props similarity index 100% rename from models/tac24/case-studies/dpm-b/power.props rename to models/tac24/case-studies/dpm-large/power.props diff --git a/models/tac24/case-studies/dpm-b/sketch.props b/models/tac24/case-studies/dpm-large/sketch.props similarity index 100% rename from models/tac24/case-studies/dpm-b/sketch.props rename to models/tac24/case-studies/dpm-large/sketch.props diff --git a/models/tac24/case-studies/dpm-b/sketch.templ b/models/tac24/case-studies/dpm-large/sketch.templ similarity index 100% rename from models/tac24/case-studies/dpm-b/sketch.templ rename to models/tac24/case-studies/dpm-large/sketch.templ diff --git a/models/tac24/dpm-demo/sketch.templ b/models/tac24/dpm-demo/sketch.templ index 5c1fe2467..bf5a47e06 100644 --- a/models/tac24/dpm-demo/sketch.templ +++ b/models/tac24/dpm-demo/sketch.templ @@ -17,10 +17,10 @@ const int q_init = 0; // profiles desired at observation levels // 0 - sleep, 1 - idle, 2 - active -hole int P1 in {0,1,2}; -hole int P2 in {0,1,2}; -hole int P3 in {0,1,2}; -hole int P4 in {0,1,2}; +hole int P1 in {2}; +hole int P2 in {2}; +hole int P3 in {2}; +hole int P4 in {2}; // observation level thresholds hole double T1 in {0.0,0.1,0.2,0.3,0.4}; diff --git a/models/tac24/dpm/sketch.props b/models/tac24/dpm/sketch.props new file mode 100644 index 000000000..8fa26537b --- /dev/null +++ b/models/tac24/dpm/sketch.props @@ -0,0 +1,2 @@ +R{"lostH"} <= 1 [ F "finished" ] +R{"power"}min = ? [ F "finished" ] \ No newline at end of file diff --git a/models/tac24/dpm/sketch.templ b/models/tac24/dpm/sketch.templ new file mode 100644 index 000000000..abf45e134 --- /dev/null +++ b/models/tac24/dpm/sketch.templ @@ -0,0 +1,259 @@ +dtmc + +// To make it more challenging, we can extend the model and consider low and high priority requests +// using two request queues. + +const int CMAX = 10; + +hole int X11 in {0,1,2}; +hole int X21 in {0,1,2}; +hole int X31 in {0,1,2}; +hole int X41 in {0,1,2}; +hole int X12 in {0,1,2}; +hole int X22 in {0,1,2}; +hole int X32 in {0,1,2}; +hole int X42 in {0,1,2}; +hole int X13 in {0,1,2}; +hole int X23 in {0,1,2}; +hole int X33 in {0,1,2}; +hole int X43 in {0,1,2}; +hole int X14 in {0,1,2}; +hole int X24 in {0,1,2}; +hole int X34 in {0,1,2}; +hole int X44 in {0,1,2}; + + +const int LT1 = 3; +const int LT2 = 5; +const int LT3 = 7; +const int HT1 = 3; +const int HT2 = 5; +const int HT3 = 7; + +// This system can achieve + +//R{"power"}<= 18000 [ F (bat=0) ] + +//R{"lostH"}<= 0.3 [ F (bat=0) ] + +//R{"lostL"}<= 0.6 [ F (bat=0) ] + + +module CLOCK + + c : [0..1]; + + [tick1] bat>0 & c=0 -> (c'=1); + [tick2] bat>0 & c=1 -> (c'=0); + +endmodule + +// POWER MANAGER + +module PM + + pm : [0..3] init 3; + // 0 - go to active + // 1 - go to active for LOW + // 2 - go to idle + // 3 - go to sleep + + + [tick1] qL*10 <= LT1*CMAX & q*10 <= HT1*CMAX -> (pm'=X11); + + [tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX & q*10 <= HT1*CMAX -> (pm'=X21); + + [tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX & q*10 <= HT1*CMAX -> (pm'=X31); + + [tick1] qL*10 > LT3*CMAX & q*10 <= HT1*CMAX -> (pm'=X41); + + [tick1] qL*10 <= LT1*CMAX & q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X12); + + [tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX & q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X22); + + [tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX & q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X32); + + [tick1] qL*10 > LT3*CMAX & q*10 > HT1*CMAX & q*10 <= HT2*CMAX -> (pm'=X42); + + [tick1] qL*10 <= LT1*CMAX & q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X13); + + [tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX & q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X23); + + [tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX & q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X33); + + [tick1] qL*10 > LT3*CMAX & q*10 > HT2*CMAX & q*10 <= HT3*CMAX -> (pm'=X43); + + [tick1] qL*10 <= LT1*CMAX & q*10 > HT3*CMAX -> (pm'=X14); + + [tick1] qL*10 > LT1*CMAX & qL*10 <= LT2*CMAX & q*10 > HT3*CMAX -> (pm'=X24); + + [tick1] qL*10 > LT2*CMAX & qL*10 <= LT3*CMAX & q*10 > HT3*CMAX -> (pm'=X34); + + [tick1] qL*10 > LT3*CMAX & q*10 > HT3*CMAX -> (pm'=X44); + +endmodule + +// SERVICE PROVIDER + +module SP + + sp : [0..8] init 3; + // 0 active + // 1 active for LOW + // 2 idle + // 3 sleep + + // 4 active_both_to_sleep + // 5 idle_to_sleep + + // 6 sleep_to_idle + // 7 sleep_to_active + // 8 sleep_to_active_L + + // states where PM has no control (transient states) + + [tick2] sp=4 -> 0.9 : (sp'=4) + 0.1 : (sp'=3); + [tick2] sp=5 -> 0.9 : (sp'=5) + 0.1 : (sp'=3); + + [tick2] sp=6 -> 0.9 : (sp'=6) + 0.1 : (sp'=2); + + [tick2] sp=7 -> 0.9 : (sp'=7) + 0.1 : (sp'=0); + [tick2] sp=8 -> 0.9 : (sp'=8) + 0.1 : (sp'=1); + + + // states where PM has control + // goto_active + [tick2] sp=0 & pm=0 -> (sp'=0); // from active + [tick2] sp=1 & pm=0 -> (sp'=0); // from activeL + [tick2] sp=2 & pm=0 -> (sp'=0); // from idle + [tick2] sp=3 & pm=0 -> (sp'=7); // from sleep + + + // goto_active_L + [tick2] sp=0 & pm=1 -> (sp'=1); // from active + [tick2] sp=1 & pm=1 -> (sp'=1); // from activeL + [tick2] sp=2 & pm=1 -> (sp'=1); // from idle + [tick2] sp=3 & pm=1 -> (sp'=8); // from sleep + + // goto_idle + [tick2] sp=0 & pm=2 -> (sp'=2); // from active + [tick2] sp=1 & pm=2 -> (sp'=2); // from active_L + [tick2] sp=2 & pm=2 -> (sp'=2); // from idle + [tick2] sp=3 & pm=2 -> (sp'=6); // from sleep + + // goto_sleep + [tick2] sp=0 & pm=3 -> (sp'=4); // from active + [tick2] sp=1 & pm=3 -> (sp'=4); // from active_L + [tick2] sp=2 & pm=3 -> (sp'=5); // idle + [tick2] sp=3 & pm=3 -> (sp'=3); // sleep + +endmodule + + +// SERVICE REQUESTER +module SR + + //a two-queue varinat + + sr : [0..2] init 0; // 0 - idle, 1 - Hreq, 2-Lreq + + [tick2] sr=0 -> 0.898: (sr'=0) + 0.051: (sr'=1) + 0.051: (sr'=2); + [tick2] sr=1 -> 0.254: (sr'=0) + 0.373: (sr'=1) + 0.373: (sr'=2); + [tick2] sr=2 -> 0.254: (sr'=0) + 0.373: (sr'=1) + 0.373: (sr'=2); + +endmodule + + +// SERVICE REQUEST QUEUES +module SRQ + + q : [0..CMAX] init 0; + qL : [0..CMAX] init 0; + + [tick2] sr=0 & sp!=0 & sp!=1 -> true; // do not serve and nothing arrives + + [tick2] sr=1 & sp!=0 & sp!=1 -> (q'=min(q+1,CMAX)); // do not serve and a request arrives + [tick2] sr=2 & sp!=0 & sp!=1 -> (qL'=min(qL+1,CMAX)); // do not serve and a request arrives + + [tick2] sr=0 & sp=0 -> (q'=max(q-1,0)); // serve and nothing arrives + [tick2] sr=0 & sp=1 -> (qL'=max(qL-1,0)); // serve and nothing arrives + + // serve and a request arrives arrives -- it actually performs two actions + [tick2] sr=2 & sp=0 -> (q'=max(q-1,0)) & (qL'=min(qL+1,CMAX)); + [tick2] sr=1 & sp=1 -> (qL'=max(qL-1,0)) & (q'=min(q+1,CMAX)); + + [tick2] sr=1 & sp=0 -> true; + [tick2] sr=2 & sp=1 -> true; + +endmodule + + + + + +// BATTERY +module BAT + + bat : [0..1] init 1; // 0 empty, 1 - operational + + [] bat=0 -> (bat'=0); // loop when battery empty + + [tick2] bat=1 -> 0.01 : (bat'=0) + 0.99 : (bat'=1); + +endmodule + +// queue size +rewards "queueH" + + c=1 : q; + +endrewards + +rewards "queueL" + + c=1 : qL; + +endrewards + +// customers lost +rewards "lostH" + + [tick2] q=CMAX & sr=1 & sp!=0 : 1; + +endrewards + +rewards "lostL" + + [tick2] qL=CMAX & sr=2 & sp!=1 : 1; + +endrewards + + +// power consumption +rewards "power" + +// in contrasr to the PRISM model we assume that the transient states have the power consuption +// equal to the source state + + sp=1 & c=1 : 2.5; + sp=0 & c=1 : 2.5; + sp=4 & c=1 : 2.5; + + sp=2 & c=1 : 1.5; + sp=5 & c=1 : 1.5; + + sp=3 & c=1 : 0.1; + sp=6 & c=1 : 0.1; + sp=7 & c=1 : 0.1; + sp=8 & c=1 : 0.1; + +endrewards + +// time +rewards "time" + + [tick2] true : 1; + +endrewards + +label "finished" = bat = 0; \ No newline at end of file diff --git a/models/tac24/grid-10-sl-4fsc/easy.props b/models/tac24/grid-10-sl-4fsc/easy.props deleted file mode 100644 index 197417691..000000000 --- a/models/tac24/grid-10-sl-4fsc/easy.props +++ /dev/null @@ -1 +0,0 @@ -R{"steps"}<=100 [ F "goal" ] \ No newline at end of file diff --git a/models/tac24/grid-av-4fsc/easy.props b/models/tac24/grid-av-4fsc/easy.props deleted file mode 100644 index 436d4e008..000000000 --- a/models/tac24/grid-av-4fsc/easy.props +++ /dev/null @@ -1 +0,0 @@ -P>=0.928 [ F "goal" ] \ No newline at end of file diff --git a/models/tac24/grid-meet-2fsc/sketch.props b/models/tac24/grid-meet-sl-2fsc/sketch.props similarity index 100% rename from models/tac24/grid-meet-2fsc/sketch.props rename to models/tac24/grid-meet-sl-2fsc/sketch.props diff --git a/models/tac24/grid-meet-2fsc/sketch.templ b/models/tac24/grid-meet-sl-2fsc/sketch.templ similarity index 99% rename from models/tac24/grid-meet-2fsc/sketch.templ rename to models/tac24/grid-meet-sl-2fsc/sketch.templ index 5b200191b..fa5b39c03 100644 --- a/models/tac24/grid-meet-2fsc/sketch.templ +++ b/models/tac24/grid-meet-sl-2fsc/sketch.templ @@ -39,7 +39,7 @@ formula y2d = d2 ? (ya2-1) : ya2; formula x2l = l2 ? (xa2-1) : xa2; -const double sl=0; +const double sl=0.1; // agent 1 holes hole int M1_0_1 in {0,1}; diff --git a/models/tac24/grid-av-4fsc/sketch.props b/models/tac24/grid/sketch.props similarity index 100% rename from models/tac24/grid-av-4fsc/sketch.props rename to models/tac24/grid/sketch.props diff --git a/models/tac24/grid-av-4fsc/sketch.templ b/models/tac24/grid/sketch.templ similarity index 100% rename from models/tac24/grid-av-4fsc/sketch.templ rename to models/tac24/grid/sketch.templ diff --git a/models/tac24/herman/sketch.props b/models/tac24/herman/sketch.props new file mode 100644 index 000000000..b94a3dc54 --- /dev/null +++ b/models/tac24/herman/sketch.props @@ -0,0 +1 @@ +R{"steps"}<=3.5 [F "stable"] \ No newline at end of file diff --git a/models/tac24/herman/sketch.templ b/models/tac24/herman/sketch.templ new file mode 100644 index 000000000..2800bb6f2 --- /dev/null +++ b/models/tac24/herman/sketch.templ @@ -0,0 +1,240 @@ +// herman's self stabilising algorithm [Her90] +// gxn/dxp 13/07/02 + +// the procotol is synchronous with no nondeterminism (a DTMC) +dtmc + +const int CMAX = 0; + +const int STATIONS = 5; +const int MAXMEM = 1; + +const double P_START=0; +const double P_STEP=0.01; + +const double p0 = P_START; +const double p1 = p0+P_STEP; +const double p2 = p1+P_STEP; +const double p3 = p2+P_STEP; +const double p4 = p3+P_STEP; +const double p5 = p4+P_STEP; +const double p6 = p5+P_STEP; +const double p7 = p6+P_STEP; +const double p8 = p7+P_STEP; +const double p9 = p8+P_STEP; +const double p10 = p9+P_STEP; +const double p11 = p10+P_STEP; +const double p12 = p11+P_STEP; +const double p13 = p12+P_STEP; +const double p14 = p13+P_STEP; +const double p15 = p14+P_STEP; +const double p16 = p15+P_STEP; +const double p17 = p16+P_STEP; +const double p18 = p17+P_STEP; +const double p19 = p18+P_STEP; +const double p20 = p19+P_STEP; +const double p21 = p20+P_STEP; +const double p22 = p21+P_STEP; +const double p23 = p22+P_STEP; +const double p24 = p23+P_STEP; +const double p25 = p24+P_STEP; +const double p26 = p25+P_STEP; +const double p27 = p26+P_STEP; +const double p28 = p27+P_STEP; +const double p29 = p28+P_STEP; + +hole int M0LFAIR in {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24}; +hole int M0HFAIR in {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24}; +hole int M1LFAIR in {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24}; +hole int M1HFAIR in {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24}; +hole int MxxA in {0,1}; +hole int MxxB in {0,1}; +hole int MxxC in {0,1}; + +module initialise + start : [0..1] init 0; + [go] start = 0 -> (start'=1); + [step1] start = 1 -> true; +endmodule + +module controller + round : [0..STATIONS] init 1; + + [sync] round = 0 -> (round'=1); + [step1] round = 1 -> (round'=2); + [step2] round = 2 -> (round'=3); + [step3] round = 3 -> (round'=4); + [step4] round = 4 -> (round'=5); + //[step5] round = 5 -> (round'=6); + //[step6] round = 6 -> (round'=7); + [step7] round = STATIONS -> (round'=0); + + //syncs : [0..CMAX] init 0; //+ + //[sync] round = 0 -> (round'=1) & (syncs'=min(syncs+1,CMAX)); + +endmodule + +// module for process 1 +module process1 + + // boolean variable for process 1 + x1 : [0..1] init 0; + y1 : [0..1] init 0; + m1 : [0..1] init 0; + + [go] true -> 1: (x1'=1); + // [go] true -> 0.5: (x1'=0) + 0.5: (x1'=1); + + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=0 -> p0 : (y1'=0) & (m1'=MxxA) + 1-p0 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=1 -> p1 : (y1'=0) & (m1'=MxxA) + 1-p1 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=2 -> p2 : (y1'=0) & (m1'=MxxA) + 1-p2 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=3 -> p3 : (y1'=0) & (m1'=MxxA) + 1-p3 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=4 -> p4 : (y1'=0) & (m1'=MxxA) + 1-p4 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=5 -> p5 : (y1'=0) & (m1'=MxxA) + 1-p5 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=6 -> p6 : (y1'=0) & (m1'=MxxA) + 1-p6 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=7 -> p7 : (y1'=0) & (m1'=MxxA) + 1-p7 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=8 -> p8 : (y1'=0) & (m1'=MxxA) + 1-p8 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=9 -> p9 : (y1'=0) & (m1'=MxxA) + 1-p9 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=10-> p10 : (y1'=0) & (m1'=MxxA) + 1-p10 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=11-> p11 : (y1'=0) & (m1'=MxxA) + 1-p11 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=12-> p12 : (y1'=0) & (m1'=MxxA) + 1-p12 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=13-> p13 : (y1'=0) & (m1'=MxxA) + 1-p13 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=14-> p14 : (y1'=0) & (m1'=MxxA) + 1-p14 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=15-> p15 : (y1'=0) & (m1'=MxxA) + 1-p15 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=16-> p16 : (y1'=0) & (m1'=MxxA) + 1-p16 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=17-> p17 : (y1'=0) & (m1'=MxxA) + 1-p17 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=18-> p18 : (y1'=0) & (m1'=MxxA) + 1-p18 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=19-> p19 : (y1'=0) & (m1'=MxxA) + 1-p19 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=20-> p20 : (y1'=0) & (m1'=MxxA) + 1-p20 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=21-> p21 : (y1'=0) & (m1'=MxxA) + 1-p21 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=22-> p22 : (y1'=0) & (m1'=MxxA) + 1-p22 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=23-> p23 : (y1'=0) & (m1'=MxxA) + 1-p23 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=24-> p24 : (y1'=0) & (m1'=MxxA) + 1-p24 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=25-> p25 : (y1'=0) & (m1'=MxxA) + 1-p25 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=26-> p26 : (y1'=0) & (m1'=MxxA) + 1-p26 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=27-> p27 : (y1'=0) & (m1'=MxxA) + 1-p27 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=28-> p28 : (y1'=0) & (m1'=MxxA) + 1-p28 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 0 & M0LFAIR=29-> p29 : (y1'=0) & (m1'=MxxA) + 1-p29 : (y1'=1) & (m1'=MxxB); + + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=0 -> p0 : (y1'=0) & (m1'=MxxA) + 1-p0 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=1 -> p1 : (y1'=0) & (m1'=MxxA) + 1-p1 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=2 -> p2 : (y1'=0) & (m1'=MxxA) + 1-p2 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=3 -> p3 : (y1'=0) & (m1'=MxxA) + 1-p3 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=4 -> p4 : (y1'=0) & (m1'=MxxA) + 1-p4 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=5 -> p5 : (y1'=0) & (m1'=MxxA) + 1-p5 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=6 -> p6 : (y1'=0) & (m1'=MxxA) + 1-p6 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=7 -> p7 : (y1'=0) & (m1'=MxxA) + 1-p7 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=8 -> p8 : (y1'=0) & (m1'=MxxA) + 1-p8 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=9 -> p9 : (y1'=0) & (m1'=MxxA) + 1-p9 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=10-> p10 : (y1'=0) & (m1'=MxxA) + 1-p10 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=11-> p11 : (y1'=0) & (m1'=MxxA) + 1-p11 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=12-> p12 : (y1'=0) & (m1'=MxxA) + 1-p12 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=13-> p13 : (y1'=0) & (m1'=MxxA) + 1-p13 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=14-> p14 : (y1'=0) & (m1'=MxxA) + 1-p14 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=15-> p15 : (y1'=0) & (m1'=MxxA) + 1-p15 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=16-> p16 : (y1'=0) & (m1'=MxxA) + 1-p16 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=17-> p17 : (y1'=0) & (m1'=MxxA) + 1-p17 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=18-> p18 : (y1'=0) & (m1'=MxxA) + 1-p18 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=19-> p19 : (y1'=0) & (m1'=MxxA) + 1-p19 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=20-> p20 : (y1'=0) & (m1'=MxxA) + 1-p20 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=21-> p21 : (y1'=0) & (m1'=MxxA) + 1-p21 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=22-> p22 : (y1'=0) & (m1'=MxxA) + 1-p22 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=23-> p23 : (y1'=0) & (m1'=MxxA) + 1-p23 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=24-> p24 : (y1'=0) & (m1'=MxxA) + 1-p24 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=25-> p25 : (y1'=0) & (m1'=MxxA) + 1-p25 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=26-> p26 : (y1'=0) & (m1'=MxxA) + 1-p26 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=27-> p27 : (y1'=0) & (m1'=MxxA) + 1-p27 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=28-> p28 : (y1'=0) & (m1'=MxxA) + 1-p28 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 0 & x1 = 1 & M0HFAIR=29-> p29 : (y1'=0) & (m1'=MxxA) + 1-p29 : (y1'=1) & (m1'=MxxB); + + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=0 -> p0 : (y1'=0) & (m1'=MxxA) + 1-p0 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=1 -> p1 : (y1'=0) & (m1'=MxxA) + 1-p1 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=2 -> p2 : (y1'=0) & (m1'=MxxA) + 1-p2 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=3 -> p3 : (y1'=0) & (m1'=MxxA) + 1-p3 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=4 -> p4 : (y1'=0) & (m1'=MxxA) + 1-p4 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=5 -> p5 : (y1'=0) & (m1'=MxxA) + 1-p5 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=6 -> p6 : (y1'=0) & (m1'=MxxA) + 1-p6 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=7 -> p7 : (y1'=0) & (m1'=MxxA) + 1-p7 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=8 -> p8 : (y1'=0) & (m1'=MxxA) + 1-p8 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=9 -> p9 : (y1'=0) & (m1'=MxxA) + 1-p9 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=10-> p10 : (y1'=0) & (m1'=MxxA) + 1-p10 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=11-> p11 : (y1'=0) & (m1'=MxxA) + 1-p11 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=12-> p12 : (y1'=0) & (m1'=MxxA) + 1-p12 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=13-> p13 : (y1'=0) & (m1'=MxxA) + 1-p13 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=14-> p14 : (y1'=0) & (m1'=MxxA) + 1-p14 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=15-> p15 : (y1'=0) & (m1'=MxxA) + 1-p15 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=16-> p16 : (y1'=0) & (m1'=MxxA) + 1-p16 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=17-> p17 : (y1'=0) & (m1'=MxxA) + 1-p17 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=18-> p18 : (y1'=0) & (m1'=MxxA) + 1-p18 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=19-> p19 : (y1'=0) & (m1'=MxxA) + 1-p19 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=20-> p20 : (y1'=0) & (m1'=MxxA) + 1-p20 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=21-> p21 : (y1'=0) & (m1'=MxxA) + 1-p21 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=22-> p22 : (y1'=0) & (m1'=MxxA) + 1-p22 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=23-> p23 : (y1'=0) & (m1'=MxxA) + 1-p23 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=24-> p24 : (y1'=0) & (m1'=MxxA) + 1-p24 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=25-> p25 : (y1'=0) & (m1'=MxxA) + 1-p25 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=26-> p26 : (y1'=0) & (m1'=MxxA) + 1-p26 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=27-> p27 : (y1'=0) & (m1'=MxxA) + 1-p27 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=28-> p28 : (y1'=0) & (m1'=MxxA) + 1-p28 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 0 & M1LFAIR=29-> p29 : (y1'=0) & (m1'=MxxA) + 1-p29 : (y1'=1) & (m1'=MxxB); + + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=0 -> p0 : (y1'=0) & (m1'=MxxA) + 1-p0 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=1 -> p1 : (y1'=0) & (m1'=MxxA) + 1-p1 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=2 -> p2 : (y1'=0) & (m1'=MxxA) + 1-p2 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=3 -> p3 : (y1'=0) & (m1'=MxxA) + 1-p3 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=4 -> p4 : (y1'=0) & (m1'=MxxA) + 1-p4 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=5 -> p5 : (y1'=0) & (m1'=MxxA) + 1-p5 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=6 -> p6 : (y1'=0) & (m1'=MxxA) + 1-p6 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=7 -> p7 : (y1'=0) & (m1'=MxxA) + 1-p7 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=8 -> p8 : (y1'=0) & (m1'=MxxA) + 1-p8 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=9 -> p9 : (y1'=0) & (m1'=MxxA) + 1-p9 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=10-> p10 : (y1'=0) & (m1'=MxxA) + 1-p10 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=11-> p11 : (y1'=0) & (m1'=MxxA) + 1-p11 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=12-> p12 : (y1'=0) & (m1'=MxxA) + 1-p12 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=13-> p13 : (y1'=0) & (m1'=MxxA) + 1-p13 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=14-> p14 : (y1'=0) & (m1'=MxxA) + 1-p14 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=15-> p15 : (y1'=0) & (m1'=MxxA) + 1-p15 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=16-> p16 : (y1'=0) & (m1'=MxxA) + 1-p16 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=17-> p17 : (y1'=0) & (m1'=MxxA) + 1-p17 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=18-> p18 : (y1'=0) & (m1'=MxxA) + 1-p18 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=19-> p19 : (y1'=0) & (m1'=MxxA) + 1-p19 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=20-> p20 : (y1'=0) & (m1'=MxxA) + 1-p20 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=21-> p21 : (y1'=0) & (m1'=MxxA) + 1-p21 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=22-> p22 : (y1'=0) & (m1'=MxxA) + 1-p22 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=23-> p23 : (y1'=0) & (m1'=MxxA) + 1-p23 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=24-> p24 : (y1'=0) & (m1'=MxxA) + 1-p24 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=25-> p25 : (y1'=0) & (m1'=MxxA) + 1-p25 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=26-> p26 : (y1'=0) & (m1'=MxxA) + 1-p26 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=27-> p27 : (y1'=0) & (m1'=MxxA) + 1-p27 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=28-> p28 : (y1'=0) & (m1'=MxxA) + 1-p28 : (y1'=1) & (m1'=MxxB); + [step1] (x1=x7) & m1 = 1 & x1 = 1 & M1HFAIR=29-> p29 : (y1'=0) & (m1'=MxxA) + 1-p29 : (y1'=1) & (m1'=MxxB); + + [step1] !(x1=x7) & m1 = 0 & x1 = 0 -> (y1'=x7) & (m1'=MxxC); + [step1] !(x1=x7) & m1 = 0 & x1 = 1 -> (y1'=x7) & (m1'=MxxC); + [step1] !(x1=x7) & m1 = 1 & x1 = 0 -> (y1'=x7) & (m1'=MxxC); + [step1] !(x1=x7) & m1 = 1 & x1 = 1 -> (y1'=x7) & (m1'=MxxC); + + [sync] true -> (x1' = y1) & (y1' = 0); + +endmodule + +// add further processes through renaming +module process2 = process1 [ x1=x2, y1=y2, x7=x1, m1=m2, step1=step2 ] endmodule +module process3 = process1 [ x1=x3, y1=y3, x7=x2, m1=m3, step1=step3 ] endmodule +module process4 = process1 [ x1=x4, y1=y4, x7=x3, m1=m4, step1=step4 ] endmodule +//module process5 = process1 [ x1=x5, y1=y5, x7=x4, m1=m5, step1=step5 ] endmodule +//module process6 = process1 [ x1=x6, y1=y6, x7=x5, m1=m6 step1=step6 ] endmodule +module process7 = process1 [ x1=x7, y1=y7, x7=x4, m1=m7, step1=step7 ] endmodule + +// full step counter +rewards "steps" + round = 0 : 1; +endrewards + +// formula, for use in properties: number of tokens +// (i.e. number of processes that have the same value as the process to their left) +formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x7?1:0)+(x7=x1?1:0); +//formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x1?1:0); + +// label - stable configurations (1 token) +label "stable" = round =1 & num_tokens=1; diff --git a/models/tac24/maze/sketch.props b/models/tac24/maze/sketch.props new file mode 100644 index 000000000..15e7f0101 --- /dev/null +++ b/models/tac24/maze/sketch.props @@ -0,0 +1 @@ +R{"steps"}min=? [F "goal"] diff --git a/models/tac24/maze/sketch.templ b/models/tac24/maze/sketch.templ new file mode 100644 index 000000000..091e27822 --- /dev/null +++ b/models/tac24/maze/sketch.templ @@ -0,0 +1,209 @@ +// maze example (POMDP) +// slightly extends that presented in +// Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University +// Encoding in PRISM by gxn 29/01/16 +// Adapted as a family with memory by Sebastian Junges + + + +// state space (value of variable "s") + +// 0 1 2 3 4 +// 5 6 7 +// 8 9 10 +// 11 13 12 + +// 13 is the target + +dtmc + +const int CMAX = 0; +//const double THRESHOLD; + +// o=0 - observation in initial state +// o=1 - west and north walls (s0) +// o=2 - north and south walls (s1 and s3) +// o=3 - north wall (s2) +// o=4 - east and north wall (s4) +// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10) +// o=6 - east, west and south walls (s11 and s12) +hole int M_0_1 in {0,1}; +hole int M_0_2 in {0,1}; +hole int M_0_3 in {0,1}; +hole int M_0_4 in {0,1}; +hole int M_0_5 in {0,1}; +hole int M_0_6 in {0,1}; +hole int M_1_1 in {0,1}; +hole int M_1_2 in {0,1}; +hole int M_1_3 in {0,1}; +hole int M_1_4 in {0,1}; +hole int M_1_5 in {0,1}; +hole int M_1_6 in {0,1}; +hole int P_0_1 in {2,3}; +hole int P_0_2 in {2,4}; +hole int P_0_3 in {2,3,4}; +hole int P_0_4 in {3,4}; +hole int P_0_5 in {1,3}; +hole int P_0_6 in {1}; +hole int P_1_1 in {2,3}; +hole int P_1_2 in {2,4}; +hole int P_1_3 in {2,3,4}; +hole int P_1_4 in {3,4}; +hole int P_1_5 in {1,3}; +hole int P_1_6 in {1}; + +module actuator + v : [0..4] init 0; + + [steer_north] v = 0 -> 0.8: (v'=1) + 0.08: (v'=4) + 0.08: (v'=2) + 0.04: (v'=3); + [steer_east] v = 0 -> 0.8: (v'=2) + 0.08: (v'=1) + 0.08: (v'=3) + 0.04: (v'=4); + [steer_south] v = 0 -> 0.8: (v'=3) + 0.08: (v'=4) + 0.08: (v'=2) + 0.04: (v'=1); + [steer_west] v = 0 -> 0.8: (v'=4) + 0.08: (v'=1) + 0.08: (v'=3) + 0.04: (v'=2); + + [north] s != 13 & v = 1 -> (v'=0); + [east] s != 13 & v = 2 -> (v'=0); + [south] s != 13 & v = 3 -> (v'=0); + [west] s != 13 & v = 4 -> (v'=0); + [done] v != 0 -> (v'=0); + +endmodule + +module strategy + pick : [0..4] init 0; + mem : [0..1] init 0; + [] v = 0 & pick = 0 & mem = 0 & o = 1 -> (mem'=M_0_1) & (pick'=P_0_1); + [] v = 0 & pick = 0 & mem = 0 & o = 2 -> (mem'=M_0_2) & (pick'=P_0_2); + [] v = 0 & pick = 0 & mem = 0 & o = 3 -> (mem'=M_0_3) & (pick'=P_0_3); + [] v = 0 & pick = 0 & mem = 0 & o = 4 -> (mem'=M_0_4) & (pick'=P_0_4); + [] v = 0 & pick = 0 & mem = 0 & o = 5 -> (mem'=M_0_5) & (pick'=P_0_5); + [] v = 0 & pick = 0 & mem = 0 & o = 6 -> (mem'=M_0_6) & (pick'=P_0_6); + [] v = 0 & pick = 0 & mem = 1 & o = 1 -> (mem'=M_1_1) & (pick'=P_1_1); + [] v = 0 & pick = 0 & mem = 1 & o = 2 -> (mem'=M_1_2) & (pick'=P_1_2); + [] v = 0 & pick = 0 & mem = 1 & o = 3 -> (mem'=M_1_3) & (pick'=P_1_3); + [] v = 0 & pick = 0 & mem = 1 & o = 4 -> (mem'=M_1_4) & (pick'=P_1_4); + [] v = 0 & pick = 0 & mem = 1 & o = 5 -> (mem'=M_1_5) & (pick'=P_1_5); + [] v = 0 & pick = 0 & mem = 1 & o = 6 -> (mem'=M_1_6) & (pick'=P_1_6); + [steer_north] pick=1 -> (pick'=0); + [steer_east] pick=2 -> (pick'=0); + [steer_south] pick=3 -> (pick'=0); + [steer_west] pick=4 -> (pick'=0); +endmodule + + + +module maze + + s : [-1..13]; + o : [0..7]; + + // initialisation + [] s=-1 -> 1/13 : (s'=0) & (o'=1) + + 1/13 : (s'=1) & (o'=2) + + 1/13 : (s'=2) & (o'=3) + + 1/13 : (s'=3) & (o'=2) + + 1/13 : (s'=4) & (o'=4) + + 1/13 : (s'=5) & (o'=5) + + 1/13 : (s'=6) & (o'=5) + + 1/13 : (s'=7) & (o'=5) + + 1/13 : (s'=8) & (o'=5) + + 1/13 : (s'=9) & (o'=5) + + 1/13 : (s'=10) & (o'=5) + + 1/13 : (s'=11) & (o'=6) + + 1/13 : (s'=12) & (o'=6); + + // moving around the maze + + [east] s=0 -> (s'=1) & (o'=2); + [west] s=0 -> (s'=0); + [north] s=0 -> (s'=0); + [south] s=0 -> (s'=5) & (o'=5); + + [east] s=1 -> (s'=2) & (o'=3); + [west] s=1 -> (s'=0) & (o'=1); + [north] s=1 -> (s'=1); + [south] s=1 -> (s'=1); + + [east] s=2 -> (s'=3) & (o'=2); + [west] s=2 -> (s'=1) & (o'=2); + [north] s=2 -> (s'=2); + [south] s=2 -> (s'=6) & (o'=5); + + [east] s=3 -> (s'=4) & (o'=4); + [west] s=3 -> (s'=2) & (o'=3); + [north] s=3 -> (s'=3); + [south] s=3 -> (s'=3); + + [east] s=4 -> (s'=4); + [west] s=4 -> (s'=3) & (o'=2); + [north] s=4 -> (s'=4); + [south] s=4 -> (s'=7) & (o'=5); + + [east] s=5 -> (s'=5); + [west] s=5 -> (s'=5); + [north] s=5 -> (s'=0) & (o'=1); + [south] s=5 -> (s'=8); + + [east] s=6 -> (s'=6); + [west] s=6 -> (s'=6); + [north] s=6 -> (s'=2) & (o'=3); + [south] s=6 -> (s'=9); + + [east] s=7 -> (s'=7); + [west] s=7 -> (s'=7); + [north] s=7 -> (s'=4) & (o'=4); + [south] s=7 -> (s'=10); + + [east] s=8 -> (s'=8); + [west] s=8 -> (s'=8); + [north] s=8 -> (s'=5); + [south] s=8 -> (s'=11) & (o'=6); + + [east] s=9 -> (s'=9); + [west] s=9 -> (s'=9); + [north] s=9 -> (s'=6); + [south] s=9 -> (s'=13) & (o'=6); + + [east] s=10 -> (s'=10); + [west] s=10 -> (s'=10); + [north] s=10 -> (s'=7); + [south] s=10 -> (s'=12) & (o'=6); + + [east] s=11 -> (s'=11); + [west] s=11 -> (s'=11); + [north] s=11 -> (s'=8) & (o'=5); + [south] s=11 -> (s'=11); + + [east] s=12 -> (s'=12); + [west] s=12 -> (s'=12); + [north] s=12 -> (s'=10) & (o'=5); + [south] s=12 -> (s'=12); + + // loop when we reach the target + [done] s=13 -> true; + +endmodule + +module counter + c : [0..CMAX] init 0; + [east] true -> (c'=min(CMAX, c+1)); + [west] true -> (c'=min(CMAX, c+1)); + [north] true -> (c'=min(CMAX, c+1)); + [south] true -> (c'=min(CMAX, c+1)); + +endmodule + +// reward structure (number of steps to reach the target) +rewards "steps" + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards + +// target observation +label "goal" = s=13; +label "traps" = s=11 | s=12; diff --git a/paynt/cli.py b/paynt/cli.py index 8acd3475e..cb9627800 100644 --- a/paynt/cli.py +++ b/paynt/cli.py @@ -58,6 +58,8 @@ def setup_logger(log_path = None): help="discount factor") @click.option("--optimum-threshold", type=click.FLOAT, help="known optimum bound") +@click.option("--precision", type=click.FLOAT, default=1e-4, + help="model checking precision") @click.option("--export", type=click.Choice(['jani', 'drn', 'pomdp']), @@ -133,7 +135,7 @@ def setup_logger(log_path = None): help="run profiling") def paynt_run( - project, sketch, props, relative_error, discount_factor, optimum_threshold, + project, sketch, props, relative_error, discount_factor, optimum_threshold, precision, export, method, incomplete_search, disable_expected_visits, @@ -175,8 +177,8 @@ def paynt_run( sketch_path = os.path.join(project, sketch) properties_path = os.path.join(project, props) if all_in_one is None: - quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, discount_factor) - synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer (quotient, method, fsc_synthesis, storm_control) + quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, discount_factor, precision) + synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control) synthesizer.run(optimum_threshold, export_evaluation) else: all_in_one_program, specification, family = paynt.parser.sketch.Sketch.load_sketch_as_all_in_one(sketch_path, properties_path) diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index f26f88b2d..9c624091e 100644 --- a/paynt/parser/sketch.py +++ b/paynt/parser/sketch.py @@ -57,7 +57,7 @@ class Sketch: @classmethod def load_sketch(cls, sketch_path, properties_path, - export=None, relative_error=0, discount_factor=1): + export=None, relative_error=0, discount_factor=1, precision=1e-4): assert discount_factor>0 and discount_factor<=1, "discount factor must be in the interval (0,1]" @@ -70,6 +70,8 @@ def load_sketch(cls, sketch_path, properties_path, decpomdp_manager = None obs_evaluator = None + paynt.verification.property.Property.model_checking_precision = precision + # check path if not os.path.isfile(sketch_path): raise ValueError(f"the sketch file {sketch_path} does not exist")