From ccb0ea77b2748701d36a7ddc5b4019fbd40c8e72 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Tue, 6 Aug 2024 12:23:01 +0200 Subject: [PATCH] decision tree enumeration --- models/mdp/dice/sketch.props | 5 - models/mdp/dice/sketch.templ | 21 - models/mdp/firewire/sketch.props | 10 + models/mdp/firewire/sketch.templ | 174 +++ models/mdp/maze/memory/sketch.props | 1 - models/mdp/maze/memory/sketch.templ | 70 -- models/mdp/maze/sketch.templ | 8 - models/mdp/pacman/sketch.props | 1 + models/mdp/pacman/sketch.templ | 1106 +++++++++++++++++ models/mdp/resource-gathering/sketch.props | 1 + models/mdp/resource-gathering/sketch.templ | 95 ++ models/mdp/zeroconf/sketch.props | 4 - models/mdp/zeroconf/sketch.templ | 258 ---- paynt/parser/sketch.py | 3 +- paynt/quotient/mdp.py | 173 +-- paynt/synthesizer/all_in_one.py | 2 +- paynt/synthesizer/decision_tree.py | 136 ++ paynt/synthesizer/statistic.py | 2 - paynt/synthesizer/synthesizer.py | 23 +- paynt/synthesizer/synthesizer_ar.py | 3 - .../src/synthesis/quotient/ColoringSmt.cpp | 81 +- .../src/synthesis/quotient/ColoringSmt.h | 22 +- .../synthesis/quotient/ColoringSmtFull.cpp | 274 ++++ .../src/synthesis/quotient/ColoringSmtFull.h | 109 ++ payntbind/src/synthesis/quotient/Family.cpp | 4 +- payntbind/src/synthesis/quotient/Family.h | 2 +- payntbind/src/synthesis/quotient/TreeNode.cpp | 305 +++++ payntbind/src/synthesis/quotient/TreeNode.h | 161 +++ payntbind/src/synthesis/quotient/bindings.cpp | 22 +- .../translation/choiceTransformation.cpp | 58 +- .../translation/choiceTransformation.h | 11 +- 31 files changed, 2617 insertions(+), 528 deletions(-) delete mode 100644 models/mdp/dice/sketch.props delete mode 100644 models/mdp/dice/sketch.templ create mode 100755 models/mdp/firewire/sketch.props create mode 100644 models/mdp/firewire/sketch.templ delete mode 100644 models/mdp/maze/memory/sketch.props delete mode 100644 models/mdp/maze/memory/sketch.templ create mode 100755 models/mdp/pacman/sketch.props create mode 100644 models/mdp/pacman/sketch.templ create mode 100755 models/mdp/resource-gathering/sketch.props create mode 100644 models/mdp/resource-gathering/sketch.templ delete mode 100644 models/mdp/zeroconf/sketch.props delete mode 100644 models/mdp/zeroconf/sketch.templ create mode 100644 paynt/synthesizer/decision_tree.py create mode 100644 payntbind/src/synthesis/quotient/ColoringSmtFull.cpp create mode 100644 payntbind/src/synthesis/quotient/ColoringSmtFull.h create mode 100644 payntbind/src/synthesis/quotient/TreeNode.cpp create mode 100644 payntbind/src/synthesis/quotient/TreeNode.h diff --git a/models/mdp/dice/sketch.props b/models/mdp/dice/sketch.props deleted file mode 100644 index 03bd1d68e..000000000 --- a/models/mdp/dice/sketch.props +++ /dev/null @@ -1,5 +0,0 @@ -R{"steps"}min=? [F finished]; -//R{"steps"}<=THRESHOLD [F finished]; -//P>=0.49 [F heads]; -//P>=0.49 [F tails]; - diff --git a/models/mdp/dice/sketch.templ b/models/mdp/dice/sketch.templ deleted file mode 100644 index 4003e83ca..000000000 --- a/models/mdp/dice/sketch.templ +++ /dev/null @@ -1,21 +0,0 @@ -mdp - -hole int s0h in {0,1,2}; -hole int s0t in {0,1,2}; -hole double p in {0.5,0.6}; - -module dice - s : [0..2] init 0; - [] s=1 | s=2 -> true; - [] s=0 -> p : (s' = s0h) + 1-p : (s' = s0t); - [] s=0 -> p : (s' = s0h) + 1-p : (s' = s0t); -endmodule - -formula heads = (s = 2); -formula tails = (s = 1); - -formula finished = heads | tails; - -rewards "steps" - true : 1; -endrewards diff --git a/models/mdp/firewire/sketch.props b/models/mdp/firewire/sketch.props new file mode 100755 index 000000000..22d64feea --- /dev/null +++ b/models/mdp/firewire/sketch.props @@ -0,0 +1,10 @@ +// A leader is always eventually elected with probability 1 +// "elected": P>=1 [ F "done" ]; +// Maximum expected time to elect a leader +// "time_max": R{"time"}max=? [ F "done" ]; +// Minimum expected time to elect a leader +R{"time"}min=? [ F "done" ]; +// Maximum expected time spent sending before electing a leader +// "time_sending": R{"time_sending"}max=? [ F "done" ]; +// Minimum probability of completing within deadline +// "deadline": Pmin=? [ F^{rew{"time"}<=deadline} ((s1=8) & (s2=7)) | ((s1=7) & (s2=8))]; diff --git a/models/mdp/firewire/sketch.templ b/models/mdp/firewire/sketch.templ new file mode 100644 index 000000000..5d99fb5bc --- /dev/null +++ b/models/mdp/firewire/sketch.templ @@ -0,0 +1,174 @@ +// firewire protocol with integer semantics +// dxp/gxn 14/06/01 + +mdp + +// CLOCKS +// x1 (x2) clock for node1 (node2) +// y1 and y2 (z1 and z2) clocks for wire12 (wire21) + +// maximum and minimum delays +// fast +const int rc_fast_max = 85; +const int rc_fast_min = 76; +// slow +const int rc_slow_max = 167; +const int rc_slow_min = 159; +// delay caused by the wire length +const int delay = 2; +// probability of choosing fast +const double fast = 0.5; +const double slow=1-fast; + +module wire12 + + // local state + w12 : [0..9]; + // 0 - empty + // 1 - rec_req + // 2 - rec_req_ack + // 3 - rec_ack + // 4 - rec_ack_idle + // 5 - rec_idle + // 6 - rec_idle_req + // 7 - rec_ack_req + // 8 - rec_req_idle + // 9 - rec_idle_ack + + // clock for wire12 + y1 : [0..delay+1]; + y2 : [0..delay+1]; + + // empty + // do not need y1 and y2 to increase as always reset when this state is left + // similarly can reset y1 and y2 when we re-enter this state + [snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); + [snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); + [snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); + [time] w12=0 -> (w12'=w12); + // rec_req + [snd_req12] w12=1 -> (w12'=1); + [rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_ack12] w12=1 -> (w12'=2) & (y2'=0); + [snd_idle12] w12=1 -> (w12'=8) & (y2'=0); + [time] w12=1 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_ack + [snd_ack12] w12=2 -> (w12'=2); + [rec_req12] w12=2 -> (w12'=3); + [time] w12=2 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack + [snd_ack12] w12=3 -> (w12'=3); + [rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_idle12] w12=3 -> (w12'=4) & (y2'=0); + [snd_req12] w12=3 -> (w12'=7) & (y2'=0); + [time] w12=3 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_idle + [snd_idle12] w12=4 -> (w12'=4); + [rec_ack12] w12=4 -> (w12'=5); + [time] w12=4 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle + [snd_idle12] w12=5 -> (w12'=5); + [rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_req12] w12=5 -> (w12'=6) & (y2'=0); + [snd_ack12] w12=5 -> (w12'=9) & (y2'=0); + [time] w12=5 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_req + [snd_req12] w12=6 -> (w12'=6); + [rec_idle12] w12=6 -> (w12'=1); + [time] w12=6 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_req + [snd_req12] w12=7 -> (w12'=7); + [rec_ack12] w12=7 -> (w12'=1); + [time] w12=7 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_idle + [snd_idle12] w12=8 -> (w12'=8); + [rec_req12] w12=8 -> (w12'=5); + [time] w12=8 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_ack + [snd_ack12] w12=9 -> (w12'=9); + [rec_idle12] w12=9 -> (w12'=3); + [time] w12=9 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + +endmodule + +module node1 + + // clock for node1 + x1 : [0..168]; + + // local state + s1 : [0..8]; + // 0 - root contention + // 1 - rec_idle + // 2 - rec_req_fast + // 3 - rec_req_slow + // 4 - rec_idle_fast + // 5 - rec_idle_slow + // 6 - snd_req + // 7- almost_root + // 8 - almost_child + + // added resets to x1 when not considered again until after rest + // removed root and child (using almost root and almost child) + + // root contention immediate state) + [snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); + [rec_idle21] s1=0 -> (s1'=1); + // rec_idle immediate state) + [snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); + [rec_req21] s1=1 -> (s1'=0); + // rec_req_fast + [rec_idle21] s1=2 -> (s1'=4); + [snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); + [time] s1=2 & x1 (x1'=min(x1+1,168)); + // rec_req_slow + [rec_idle21] s1=3 -> (s1'=5); + [snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); + [time] s1=3 & x1 (x1'=min(x1+1,168)); + // rec_idle_fast + [rec_req21] s1=4 -> (s1'=2); + [snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); + [time] s1=4 & x1 (x1'=min(x1+1,168)); + // rec_idle_slow + [rec_req21] s1=5 -> (s1'=3); + [snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); + [time] s1=5 & x1 (x1'=min(x1+1,168)); + // snd_req + // do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 + // also can set x1 to 0 upon entering this state + [rec_req21] s1=6 -> (s1'=0); + [rec_ack21] s1=6 -> (s1'=8); + [time] s1=6 -> (s1'=s1); + // almost root (immediate) + // loop in final states to remove deadlock + [] s1=7 & s2=8 -> (s1'=s1); + [] s1=8 & s2=7 -> (s1'=s1); + [time] s1=7 -> (s1'=s1); + [time] s1=8 -> (s1'=s1); + +endmodule + +// construct remaining automata through renaming +module wire21=wire12[w12=w21, y1=z1, y2=z2, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, + rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] +endmodule +module node2=node1[s1=s2, s2=s1, x1=x2, + rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] +endmodule + +// labels +label "done" = (s1=8 & s2=7) | (s1=7 & s2=8); + +// reward structures + +// time +rewards "time" + [time] true : 1; +endrewards + +// time nodes sending +rewards "time_sending" + [time] (w12>0 | w21>0) : 1; +endrewards diff --git a/models/mdp/maze/memory/sketch.props b/models/mdp/maze/memory/sketch.props deleted file mode 100644 index 58121ac47..000000000 --- a/models/mdp/maze/memory/sketch.props +++ /dev/null @@ -1 +0,0 @@ -Pmax=? [F goal] \ No newline at end of file diff --git a/models/mdp/maze/memory/sketch.templ b/models/mdp/maze/memory/sketch.templ deleted file mode 100644 index 535572f30..000000000 --- a/models/mdp/maze/memory/sketch.templ +++ /dev/null @@ -1,70 +0,0 @@ -mdp - -// 3 | x x x x x -// 2 | x x x -// 1 | x x x -// 0 | x x x -// y ____________ -// x 0 1 2 3 4 - -// can go in this direction -formula u = y<3; -formula r = y=3 & x<4; -formula d = y>0 & (x=0 | x=2 | x=4); -formula l = y=3 & x>0; - -// target cell -formula goal = x=2 & y=0; -formula bad = (x=0 & y=0); - -// initial states -init ((x=1)&(y=3)) | ((x=0)&(y=1)) endinit; - -// updates of coordinates (if possible) -formula yu = u ? (y+1) : y; -formula xr = r ? (x+1) : x; -formula yd = d ? (y-1) : y; -formula xl = l ? (x-1) : x; - - -module memory - - mem: [0..2] init 0; - [up] true -> (mem'=0); - [up] true -> (mem'=1); - [up] true -> (mem'=2); - //[up] true -> (mem'=3); - - [right] true -> (mem'=0); - [right] true -> (mem'=1); - [right] true -> (mem'=2); - //[right] true -> (mem'=3); - - [down] true -> (mem'=0); - [down] true -> (mem'=1); - [down] true -> (mem'=2); - //[down] true -> (mem'=3); - - [left] true -> (mem'=0); - [left] true -> (mem'=1); - [left] true -> (mem'=2); - //[left] true -> (mem'=3); - -endmodule - - -module maze - - x : [0..4]; - y : [0..3]; - - // moving around the maze (all combinations) - [up] !bad -> 0.8: (y'=yu) + 0.08: (x'=xr) + 0.08: (x'=xl) + 0.04: (y'=yd); - [right] !bad -> 0.8: (x'=xr) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xl); - [down] !bad -> 0.8: (y'=yd) + 0.08: (x'=xr) + 0.08: (x'=xl) + 0.04: (y'=yu); - [left] !bad -> 0.8: (x'=xl) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xr); - -endmodule - - - diff --git a/models/mdp/maze/sketch.templ b/models/mdp/maze/sketch.templ index ee55b6587..399c248c7 100644 --- a/models/mdp/maze/sketch.templ +++ b/models/mdp/maze/sketch.templ @@ -65,15 +65,7 @@ module maze [right] true -> 0.8: (x'=xr) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xl); [down] true -> 0.8: (y'=yd) + 0.08: (x'=xr) + 0.08: (x'=xl) + 0.04: (y'=yu); [left] true -> 0.8: (x'=xl) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xr); - -endmodule -module test - var : bool init false; - [up] true -> (var'=true); - [right] true -> (var'=false); - [down] true -> (var'=false); - [left] true -> (var'=false); endmodule // rewards diff --git a/models/mdp/pacman/sketch.props b/models/mdp/pacman/sketch.props new file mode 100755 index 000000000..3408c89a9 --- /dev/null +++ b/models/mdp/pacman/sketch.props @@ -0,0 +1 @@ +"crash": Pmin=? [F "Crash"] diff --git a/models/mdp/pacman/sketch.templ b/models/mdp/pacman/sketch.templ new file mode 100644 index 000000000..88e79091c --- /dev/null +++ b/models/mdp/pacman/sketch.templ @@ -0,0 +1,1106 @@ +// %%%%%%%%%%%% +// %..........% +// %.%.%%.%.%.% +// %.%.%%.%.%.% +// %..........% +// %%%.%.%%%%.% +// %...%......% +// %%%%%%%%%%%% + +mdp + +//CONSTANTS +const xSize = 11; +const ySize = 7; + +const MAXSTEPS = 5; + +formula deactive0 = (xG0 = 0); +formula deactive1 = (xG1 = 0); + +module arbiter + pMove : [0 .. 2] init 0; //token to determine who is allowed to move + steps : [0 .. MAXSTEPS] init 0; //number of steps we plan ahead + + [g0] (pMove = 0) & !deactive0 & ((xG0 < xP ? xP - xG0 : xG0 - xP) + (yG0 < yP ? yP - yG0 : yG0 - yP) <= 2*(MAXSTEPS - steps)) -> 1:(pMove' = 1); + [stop0] (pMove = 0) & (deactive0 | ((xG0 < xP ? xP - xG0 : xG0 - xP) + (yG0 < yP ? yP - yG0 : yG0 - yP) > 2*(MAXSTEPS - steps))) -> 1:(pMove' = 1); + [g1] (pMove = 1) & !deactive1 & ((xG1 < xP ? xP - xG1 : xG1 - xP) + (yG1 < yP ? yP - yG1 : yG1 - yP) <= 2*(MAXSTEPS - steps)) -> 1:(pMove' = 2); + [stop1] (pMove = 1) & (deactive1 | ((xG1 < xP ? xP - xG1 : xG1 - xP) + (yG1 < yP ? yP - yG1 : yG1 - yP) > 2*(MAXSTEPS - steps))) -> 1:(pMove' = 2); + + + [p] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1); + [left] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1); + [right] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1); + [up] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1); + [down] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1); + + [] (pMove = 2 & (steps = MAXSTEPS | (deactive0 & deactive1))) -> 1:(pMove'=2); +endmodule + + +//GHOST#0 +module ghost0 + xG0 : [0..xSize] init 3; // x position of Ghost + yG0 : [0..ySize] init 4; // y position of Ghost + dG0 : [0..3] init 0; //direction of ghost (0=right, 1=up, 2=left, 3=down) + + [p] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1); + [p] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0); + [right] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1); + [right] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0); + [left] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1); + [left] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0); + [down] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1); + [down] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0); + [up] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1); + [up] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0); + + + [stop0] true -> 1:(xG0'=0) & (yG0'=0); + //horizontal corridor + [g0] (yG0=1 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=1 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=1 & xG0 >=4 & xG0 <=5 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=1 & xG0 >=4 & xG0 <=5 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=1 & xG0 >=7 & xG0 <=7 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=1 & xG0 >=7 & xG0 <=7 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=1 & xG0 >=9 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=1 & xG0 >=9 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=4 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=4 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=4 & xG0 >=4 & xG0 <=4 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=4 & xG0 >=4 & xG0 <=4 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=4 & xG0 >=7 & xG0 <=7 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=4 & xG0 >=7 & xG0 <=7 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=4 & xG0 >=9 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=4 & xG0 >=9 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=6 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=6 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + //horizontal corridor + [g0] (yG0=6 & xG0 >=6 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); + [g0] (yG0=6 & xG0 >=6 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); + + //vertical corridor + [g0] (xG0=1 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=1 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=3 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=3 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=3 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=3 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=5 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=5 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=6 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=6 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=8 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=8 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=10 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=10 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + //vertical corridor + [g0] (xG0=10 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=10 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); + + //deadends + [g0] (xG0=1 & yG0=6) -> 1: (xG0'=xG0+1) & (dG0'=0); + + //corners + [g0] (xG0=1 & yG0=1 & (dG0=2 | dG0=1))-> 1: (yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=1 & yG0=1 & (dG0=3 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0); + [g0] (xG0=1 & yG0=4 & (dG0=2 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3); + [g0] (xG0=1 & yG0=4 & (dG0=1 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0); + [g0] (xG0=3 & yG0=6 & (dG0=0 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3); + [g0] (xG0=3 & yG0=6 & (dG0=1 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2); + [g0] (xG0=5 & yG0=6 & (dG0=2 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3); + [g0] (xG0=5 & yG0=6 & (dG0=1 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0); + [g0] (xG0=10 & yG0=1 & (dG0=0 | dG0=1))-> 1: (yG0'=yG0+1) & (dG0'=1); + [g0] (xG0=10 & yG0=1 & (dG0=3 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2); + [g0] (xG0=10 & yG0=6 & (dG0=0 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3); + [g0] (xG0=10 & yG0=6 & (dG0=1 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2); + + + //crossing at position (3, 1) [t-up crossing] + + //- positioning pacman = r + + [g0] (xG0=3 & yG0=1 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=3 & yG0=1 & dG0=3 & xG0 0.92: (xG0'=xG0+1) & (dG0'=0) + 0.08: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=3 & yG0=1 & dG0=2 & xG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g0] (xG0=3 & yG0=1 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=3 & yG0=1 & dG0=3 & yG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving down -> continues to go right or left + [g0] (xG0=3 & yG0=1 & dG0=2 & yG0 0.8: (yG0'=yG0+1) & (dG0'=1) + 0.2: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g0] (xG0=3 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=3 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=3 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g0] (xG0=3 & yG0=1 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=3 & yG0=1 & dG0=3 & xG0 0.78: (xG0'=xG0+1) & (dG0'=0) + 0.22: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=3 & yG0=1 & dG0=2 & xG0 0.86: (yG0'=yG0+1) & (dG0'=1) + 0.14: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g0] (xG0=3 & yG0=1 & dG0=0 & xG0>xP & yG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=3 & yG0=1 & dG0=3 & xG0>xP & yG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=3 & yG0=1 & dG0=2 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g0] (xG0=3 & yG0=1 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (6, 1) [t-up crossing] + + //- positioning pacman = r + + [g0] (xG0=6 & yG0=1 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=6 & yG0=1 & dG0=3 & xG0 0.64: (xG0'=xG0+1) & (dG0'=0) + 0.36: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=6 & yG0=1 & dG0=2 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g0] (xG0=6 & yG0=1 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=6 & yG0=1 & dG0=3 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=6 & yG0=1 & dG0=2 & yG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g0] (xG0=6 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=6 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving down -> continues to go right or left + [g0] (xG0=6 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 0.22: (yG0'=yG0+1) & (dG0'=1) + 0.78: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g0] (xG0=6 & yG0=1 & dG0=0 & xG0 0.46: (xG0'=xG0+1) & (dG0'=0) + 0.54: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=6 & yG0=1 & dG0=3 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving down -> continues to go right or left + [g0] (xG0=6 & yG0=1 & dG0=2 & xG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g0] (xG0=6 & yG0=1 & dG0=0 & xG0>xP & yG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=6 & yG0=1 & dG0=3 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=6 & yG0=1 & dG0=2 & xG0>xP & yG0 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.67: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g0] (xG0=6 & yG0=1 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (8, 1) [t-up crossing] + + //- positioning pacman = r + + [g0] (xG0=8 & yG0=1 & dG0=0 & xG0 0.4: (xG0'=xG0+1) & (dG0'=0) + 0.6: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=8 & yG0=1 & dG0=3 & xG0 0.92: (xG0'=xG0+1) & (dG0'=0) + 0.08: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=8 & yG0=1 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g0] (xG0=8 & yG0=1 & dG0=0 & yG0 0.4: (xG0'=xG0+1) & (dG0'=0) + 0.6: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=8 & yG0=1 & dG0=3 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=8 & yG0=1 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g0] (xG0=8 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=8 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=8 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g0] (xG0=8 & yG0=1 & dG0=0 & xG0 0.36: (xG0'=xG0+1) & (dG0'=0) + 0.64: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=8 & yG0=1 & dG0=3 & xG0 0.75: (xG0'=xG0+1) & (dG0'=0) + 0.25: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=8 & yG0=1 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g0] (xG0=8 & yG0=1 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=8 & yG0=1 & dG0=3 & xG0>xP & yG0 0.2: (xG0'=xG0+1) & (dG0'=0) + 0.8: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=8 & yG0=1 & dG0=2 & xG0>xP & yG0 0.67: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g0] (xG0=8 & yG0=1 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (3, 4) [center crossing] + + //- positioning pacman = r + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0 0.61: (xG0'=xG0+1) & (dG0'=0) + 0.26: (xG0'=xG0-1) & (dG0'=2) + 0.13: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u + + [g0] (xG0=3 & yG0=4 & dG0=0 & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & yG0 0.16: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1) + 0.17: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & yG0 0.28: (yG0'=yG0+1) & (dG0'=1) + 0.43: (xG0'=xG0-1) & (dG0'=2) + 0.29: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = l + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.34: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d + + [g0] (xG0=3 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u-r + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.25: (xG0'=xG0-1) & (dG0'=2) + 0.25: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u-l + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0 0.34: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d-r + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0yP ) -> 0.67: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d-l + + [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right, up or down + [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right, up or left + [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go up, left or down + [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go right, left or down + + //- position pacman == position ghost + + [g0] (xG0=3 & yG0=4 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (5, 4) [t-up crossing] + + //- positioning pacman = r + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0 0.89: (xG0'=xG0+1) & (dG0'=0) + 0.11: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g0] (xG0=5 & yG0=4 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & yG0 0.83: (yG0'=yG0+1) & (dG0'=1) + 0.17: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.17: (xG0'=xG0+1) & (dG0'=0) + 0.83: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.17: (yG0'=yG0+1) & (dG0'=1) + 0.83: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d + + [g0] (xG0=5 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0 0.75: (yG0'=yG0+1) & (dG0'=1) + 0.25: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d-r + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0yP ) -> 0.95: (xG0'=xG0+1) & (dG0'=0) + 0.05: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d-l + + [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0+1) & (dG0'=1); // ghost is moving to the right -> continues to go right or up + [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 0.11: (xG0'=xG0+1) & (dG0'=0) + 0.89: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go right or left + [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g0] (xG0=5 & yG0=4 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (6, 4) [t-down crossing] + + //- positioning pacman = r + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0 0.57: (xG0'=xG0+1) & (dG0'=0) + 0.43: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u + + [g0] (xG0=6 & yG0=4 & dG0=0 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = l + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.75: (xG0'=xG0-1) & (dG0'=2) + 0.25: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d + + [g0] (xG0=6 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-r + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0 0.89: (xG0'=xG0+1) & (dG0'=0) + 0.11: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-l + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0 0.67: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-r + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0yP ) -> 0.69: (xG0'=xG0+1) & (dG0'=0) + 0.31: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0yP ) -> 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.67: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-l + + [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving left -> continues to go left or down + + //- position pacman == position ghost + + [g0] (xG0=6 & yG0=4 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (8, 4) [t-down crossing] + + //- positioning pacman = r + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u + + [g0] (xG0=8 & yG0=4 & dG0=0 & yG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = l + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 0.44: (xG0'=xG0+1) & (dG0'=0) + 0.56: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.83: (xG0'=xG0-1) & (dG0'=2) + 0.17: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d + + [g0] (xG0=8 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.43: (xG0'=xG0+1) & (dG0'=0) + 0.57: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-r + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-l + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0 0.83: (xG0'=xG0-1) & (dG0'=2) + 0.17: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-r + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0yP ) -> 0.56: (xG0'=xG0+1) & (dG0'=0) + 0.44: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-l + + [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go right or down + [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go right or left + [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving left -> continues to go left or down + + //- position pacman == position ghost + + [g0] (xG0=8 & yG0=4 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); + + //crossing at position (10, 4) [t-left crossing] + + //- positioning pacman = u + + [g0] (xG0=10 & yG0=4 & dG0=0 & yG0 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go up or down + [g0] (xG0=10 & yG0=4 & dG0=1 & yG0 0.45: (yG0'=yG0+1) & (dG0'=1) + 0.55: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go up or left + [g0] (xG0=10 & yG0=4 & dG0=3 & yG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = l + + [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go up or down + [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go up or left + [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.79: (xG0'=xG0-1) & (dG0'=2) + 0.21: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = d + + [g0] (xG0=10 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.2: (yG0'=yG0+1) & (dG0'=1) + 0.8: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go up or down + [g0] (xG0=10 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go up or left + [g0] (xG0=10 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = u-l + + [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0 0.75: (yG0'=yG0+1) & (dG0'=1) + 0.25: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go up or down + [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0 0.44: (yG0'=yG0+1) & (dG0'=1) + 0.56: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go up or left + [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2); // ghost is moving down -> continues to go left or down + + //- positioning pacman = d-l + + [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3); // ghost is moving to the right -> continues to go up or down + [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2); // ghost is moving up -> continues to go up or left + [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3); // ghost is moving down -> continues to go left or down + + //- position pacman == position ghost + + [g0] (xG0=10 & yG0=4 & xG0=xP & yG0=yP) -> 1: (xG0'=xG0); +endmodule + +//GHOST#1 +module ghost1 + xG1 : [0..xSize] init 3; // x position of Ghost + yG1 : [0..ySize] init 4; // y position of Ghost + dG1 : [0..3] init 0; //direction of ghost (0=right, 1=up, 2=left, 3=down) + + [p] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0); + [p] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1); + [right] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0); + [right] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1); + [left] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0); + [left] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1); + [down] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0); + [down] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1); + [up] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0); + [up] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1); + + [stop1] true -> 1:(xG1'=0) & (yG1'=0); + + + //horizontal corridor + [g1] (yG1=1 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=1 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=1 & xG1 >=4 & xG1 <=5 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=1 & xG1 >=4 & xG1 <=5 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=1 & xG1 >=7 & xG1 <=7 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=1 & xG1 >=7 & xG1 <=7 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=1 & xG1 >=9 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=1 & xG1 >=9 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=4 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=4 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=4 & xG1 >=4 & xG1 <=4 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=4 & xG1 >=4 & xG1 <=4 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=4 & xG1 >=7 & xG1 <=7 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=4 & xG1 >=7 & xG1 <=7 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=4 & xG1 >=9 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=4 & xG1 >=9 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=6 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=6 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + //horizontal corridor + [g1] (yG1=6 & xG1 >=6 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); + [g1] (yG1=6 & xG1 >=6 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); + + //vertical corridor + [g1] (xG1=1 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=1 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=3 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=3 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=3 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=3 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=5 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=5 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=6 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=6 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=8 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=8 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=10 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=10 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + //vertical corridor + [g1] (xG1=10 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=10 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); + + //deadends + [g1] (xG1=1 & yG1=6) -> 1: (xG1'=xG1+1) & (dG1'=0); + + //corners + [g1] (xG1=1 & yG1=1 & (dG1=2 | dG1=1))-> 1: (yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=1 & yG1=1 & (dG1=3 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0); + [g1] (xG1=1 & yG1=4 & (dG1=2 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3); + [g1] (xG1=1 & yG1=4 & (dG1=1 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0); + [g1] (xG1=3 & yG1=6 & (dG1=0 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3); + [g1] (xG1=3 & yG1=6 & (dG1=1 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2); + [g1] (xG1=5 & yG1=6 & (dG1=2 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3); + [g1] (xG1=5 & yG1=6 & (dG1=1 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0); + [g1] (xG1=10 & yG1=1 & (dG1=0 | dG1=1))-> 1: (yG1'=yG1+1) & (dG1'=1); + [g1] (xG1=10 & yG1=1 & (dG1=3 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2); + [g1] (xG1=10 & yG1=6 & (dG1=0 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3); + [g1] (xG1=10 & yG1=6 & (dG1=1 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2); + + + //crossing at position (3, 1) [t-up crossing] + + //- positioning pacman = r + + [g1] (xG1=3 & yG1=1 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=3 & yG1=1 & dG1=3 & xG1 0.92: (xG1'=xG1+1) & (dG1'=0) + 0.08: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=3 & yG1=1 & dG1=2 & xG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g1] (xG1=3 & yG1=1 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=3 & yG1=1 & dG1=3 & yG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving down -> continues to go right or left + [g1] (xG1=3 & yG1=1 & dG1=2 & yG1 0.8: (yG1'=yG1+1) & (dG1'=1) + 0.2: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g1] (xG1=3 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=3 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=3 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g1] (xG1=3 & yG1=1 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=3 & yG1=1 & dG1=3 & xG1 0.78: (xG1'=xG1+1) & (dG1'=0) + 0.22: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=3 & yG1=1 & dG1=2 & xG1 0.86: (yG1'=yG1+1) & (dG1'=1) + 0.14: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g1] (xG1=3 & yG1=1 & dG1=0 & xG1>xP & yG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=3 & yG1=1 & dG1=3 & xG1>xP & yG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=3 & yG1=1 & dG1=2 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g1] (xG1=3 & yG1=1 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (6, 1) [t-up crossing] + + //- positioning pacman = r + + [g1] (xG1=6 & yG1=1 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=6 & yG1=1 & dG1=3 & xG1 0.64: (xG1'=xG1+1) & (dG1'=0) + 0.36: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=6 & yG1=1 & dG1=2 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g1] (xG1=6 & yG1=1 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=6 & yG1=1 & dG1=3 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=6 & yG1=1 & dG1=2 & yG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g1] (xG1=6 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=6 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving down -> continues to go right or left + [g1] (xG1=6 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 0.22: (yG1'=yG1+1) & (dG1'=1) + 0.78: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g1] (xG1=6 & yG1=1 & dG1=0 & xG1 0.46: (xG1'=xG1+1) & (dG1'=0) + 0.54: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=6 & yG1=1 & dG1=3 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving down -> continues to go right or left + [g1] (xG1=6 & yG1=1 & dG1=2 & xG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g1] (xG1=6 & yG1=1 & dG1=0 & xG1>xP & yG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=6 & yG1=1 & dG1=3 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=6 & yG1=1 & dG1=2 & xG1>xP & yG1 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.67: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g1] (xG1=6 & yG1=1 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (8, 1) [t-up crossing] + + //- positioning pacman = r + + [g1] (xG1=8 & yG1=1 & dG1=0 & xG1 0.4: (xG1'=xG1+1) & (dG1'=0) + 0.6: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=8 & yG1=1 & dG1=3 & xG1 0.92: (xG1'=xG1+1) & (dG1'=0) + 0.08: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=8 & yG1=1 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g1] (xG1=8 & yG1=1 & dG1=0 & yG1 0.4: (xG1'=xG1+1) & (dG1'=0) + 0.6: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=8 & yG1=1 & dG1=3 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=8 & yG1=1 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g1] (xG1=8 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=8 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=8 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g1] (xG1=8 & yG1=1 & dG1=0 & xG1 0.36: (xG1'=xG1+1) & (dG1'=0) + 0.64: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=8 & yG1=1 & dG1=3 & xG1 0.75: (xG1'=xG1+1) & (dG1'=0) + 0.25: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=8 & yG1=1 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g1] (xG1=8 & yG1=1 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=8 & yG1=1 & dG1=3 & xG1>xP & yG1 0.2: (xG1'=xG1+1) & (dG1'=0) + 0.8: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=8 & yG1=1 & dG1=2 & xG1>xP & yG1 0.67: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g1] (xG1=8 & yG1=1 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (3, 4) [center crossing] + + //- positioning pacman = r + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1 0.61: (xG1'=xG1+1) & (dG1'=0) + 0.26: (xG1'=xG1-1) & (dG1'=2) + 0.13: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u + + [g1] (xG1=3 & yG1=4 & dG1=0 & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & yG1 0.16: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1) + 0.17: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & yG1 0.28: (yG1'=yG1+1) & (dG1'=1) + 0.43: (xG1'=xG1-1) & (dG1'=2) + 0.29: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = l + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.34: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d + + [g1] (xG1=3 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u-r + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.25: (xG1'=xG1-1) & (dG1'=2) + 0.25: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = u-l + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1 0.34: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d-r + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1yP ) -> 0.67: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- positioning pacman = d-l + + [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right, up or down + [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right, up or left + [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go up, left or down + [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go right, left or down + + //- position pacman == position ghost + + [g1] (xG1=3 & yG1=4 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (5, 4) [t-up crossing] + + //- positioning pacman = r + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1 0.89: (xG1'=xG1+1) & (dG1'=0) + 0.11: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u + + [g1] (xG1=5 & yG1=4 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & yG1 0.83: (yG1'=yG1+1) & (dG1'=1) + 0.17: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = l + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.17: (xG1'=xG1+1) & (dG1'=0) + 0.83: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.17: (yG1'=yG1+1) & (dG1'=1) + 0.83: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d + + [g1] (xG1=5 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-r + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1 0.75: (yG1'=yG1+1) & (dG1'=1) + 0.25: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = u-l + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d-r + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1yP ) -> 0.95: (xG1'=xG1+1) & (dG1'=0) + 0.05: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- positioning pacman = d-l + + [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1+1) & (dG1'=1); // ghost is moving to the right -> continues to go right or up + [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 0.11: (xG1'=xG1+1) & (dG1'=0) + 0.89: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go right or left + [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving to the left -> continues to go up or left + + //- position pacman == position ghost + + [g1] (xG1=5 & yG1=4 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (6, 4) [t-down crossing] + + //- positioning pacman = r + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1 0.57: (xG1'=xG1+1) & (dG1'=0) + 0.43: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u + + [g1] (xG1=6 & yG1=4 & dG1=0 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = l + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.75: (xG1'=xG1-1) & (dG1'=2) + 0.25: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d + + [g1] (xG1=6 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-r + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1 0.89: (xG1'=xG1+1) & (dG1'=0) + 0.11: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-l + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1 0.67: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-r + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1yP ) -> 0.69: (xG1'=xG1+1) & (dG1'=0) + 0.31: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1yP ) -> 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.67: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-l + + [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving left -> continues to go left or down + + //- position pacman == position ghost + + [g1] (xG1=6 & yG1=4 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (8, 4) [t-down crossing] + + //- positioning pacman = r + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u + + [g1] (xG1=8 & yG1=4 & dG1=0 & yG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = l + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 0.44: (xG1'=xG1+1) & (dG1'=0) + 0.56: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.83: (xG1'=xG1-1) & (dG1'=2) + 0.17: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d + + [g1] (xG1=8 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.43: (xG1'=xG1+1) & (dG1'=0) + 0.57: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-r + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving left -> continues to go left or down + + //- positioning pacman = u-l + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1 0.83: (xG1'=xG1-1) & (dG1'=2) + 0.17: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-r + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1yP ) -> 0.56: (xG1'=xG1+1) & (dG1'=0) + 0.44: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- positioning pacman = d-l + + [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go right or down + [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go right or left + [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving left -> continues to go left or down + + //- position pacman == position ghost + + [g1] (xG1=8 & yG1=4 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); + + //crossing at position (10, 4) [t-left crossing] + + //- positioning pacman = u + + [g1] (xG1=10 & yG1=4 & dG1=0 & yG1 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go up or down + [g1] (xG1=10 & yG1=4 & dG1=1 & yG1 0.45: (yG1'=yG1+1) & (dG1'=1) + 0.55: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go up or left + [g1] (xG1=10 & yG1=4 & dG1=3 & yG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = l + + [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go up or down + [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go up or left + [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.79: (xG1'=xG1-1) & (dG1'=2) + 0.21: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = d + + [g1] (xG1=10 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.2: (yG1'=yG1+1) & (dG1'=1) + 0.8: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go up or down + [g1] (xG1=10 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go up or left + [g1] (xG1=10 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go left or down + + //- positioning pacman = u-l + + [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1 0.75: (yG1'=yG1+1) & (dG1'=1) + 0.25: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go up or down + [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1 0.44: (yG1'=yG1+1) & (dG1'=1) + 0.56: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go up or left + [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2); // ghost is moving down -> continues to go left or down + + //- positioning pacman = d-l + + [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3); // ghost is moving to the right -> continues to go up or down + [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2); // ghost is moving up -> continues to go up or left + [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3); // ghost is moving down -> continues to go left or down + + //- position pacman == position ghost + + [g1] (xG1=10 & yG1=4 & xG1=xP & yG1=yP) -> 1: (xG1'=xG1); +endmodule + +//PACMAN +module pacman + xP : [1..xSize] init 1;// x position of Pacman + yP : [1..ySize] init 1;// y position of Pacman + dP : [0 .. 3] init 0; //direction of pacman (0=right, 1=up, 2=left, 3=down) + + //horizontal corridor + [p] (yP=1 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=1 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=1 & xP >=4 & xP <=5 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=1 & xP >=4 & xP <=5 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=1 & xP >=7 & xP <=7 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=1 & xP >=7 & xP <=7 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=1 & xP >=9 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=1 & xP >=9 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=4 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=4 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=4 & xP >=4 & xP <=4 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=4 & xP >=4 & xP <=4 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=4 & xP >=7 & xP <=7 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=4 & xP >=7 & xP <=7 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=4 & xP >=9 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=4 & xP >=9 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=6 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=6 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + //horizontal corridor + [p] (yP=6 & xP >=6 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); + [p] (yP=6 & xP >=6 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); + + //vertical corridor + [p] (xP=1 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=1 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=3 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=3 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=3 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=3 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=5 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=5 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=6 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=6 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=8 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=8 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=10 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=10 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + //vertical corridor + [p] (xP=10 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); + [p] (xP=10 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); + + //deadends + [p] (xP=1 & yP=6) -> 1: (xP'=xP+1) & (dP'=0); + + //corners + [p] (xP=1 & yP=1 & (dP=2 | dP=1))-> 1: (yP'=yP+1) & (dP'=1); + [p] (xP=1 & yP=1 & (dP=3 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0); + [p] (xP=1 & yP=4 & (dP=2 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3); + [p] (xP=1 & yP=4 & (dP=1 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0); + [p] (xP=3 & yP=6 & (dP=0 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3); + [p] (xP=3 & yP=6 & (dP=1 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2); + [p] (xP=5 & yP=6 & (dP=2 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3); + [p] (xP=5 & yP=6 & (dP=1 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0); + [p] (xP=10 & yP=1 & (dP=0 | dP=1))-> 1: (yP'=yP+1) & (dP'=1); + [p] (xP=10 & yP=1 & (dP=3 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2); + [p] (xP=10 & yP=6 & (dP=0 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3); + [p] (xP=10 & yP=6 & (dP=1 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2); + + // crossing at position(3, 1) + + [right] (xP=3 & yP=1) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=3 & yP=1) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=3 & yP=1) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=3 & yP=1 & pMove=2) -> 1: (xP'=xP); + + // crossing at position(6, 1) + + [right] (xP=6 & yP=1) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=6 & yP=1) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=6 & yP=1) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=6 & yP=1 & pMove=2) -> 1: (xP'=xP); + + // crossing at position(8, 1) + + [right] (xP=8 & yP=1) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=8 & yP=1) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=8 & yP=1) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=8 & yP=1 & pMove=2) -> 1: (xP'=xP); + + // crossing at position(3, 4) + + [right] (xP=3 & yP=4) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=3 & yP=4) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=3 & yP=4) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=3 & yP=4) -> 1: (yP'=yP-1) & (dP'=3); + + // crossing at position(5, 4) + + [right] (xP=5 & yP=4) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=5 & yP=4) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=5 & yP=4) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=5 & yP=4 & pMove=2) -> 1: (xP'=xP); + + // crossing at position(6, 4) + + [right] (xP=6 & yP=4) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=6 & yP=4 & pMove=2) -> 1: (xP'=xP); + [left] (xP=6 & yP=4) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=6 & yP=4) -> 1: (yP'=yP-1) & (dP'=3); + + // crossing at position(8, 4) + + [right] (xP=8 & yP=4) -> 1: (xP'=xP+1) & (dP'=0); + [up] (xP=8 & yP=4 & pMove=2) -> 1: (xP'=xP); + [left] (xP=8 & yP=4) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=8 & yP=4) -> 1: (yP'=yP-1) & (dP'=3); + + // crossing at position(10, 4) + + [right] (xP=10 & yP=4 & pMove=2) -> 1: (xP'=xP); + [up] (xP=10 & yP=4) -> 1: (yP'=yP+1) & (dP'=1); + [left] (xP=10 & yP=4) -> 1: (xP'=xP-1) & (dP'=2); + [down] (xP=10 & yP=4) -> 1: (yP'=yP-1) & (dP'=3); + +endmodule + +//CRASH +label "Crash" = (xP = xG0 & yP = yG0) | (xP = xG1 & yP = yG1); +//label "Safe" = deactive0 & deactive1; + diff --git a/models/mdp/resource-gathering/sketch.props b/models/mdp/resource-gathering/sketch.props new file mode 100755 index 000000000..d1a6ffca6 --- /dev/null +++ b/models/mdp/resource-gathering/sketch.props @@ -0,0 +1 @@ +R{"steps"}min=? [F "success"]; \ No newline at end of file diff --git a/models/mdp/resource-gathering/sketch.templ b/models/mdp/resource-gathering/sketch.templ new file mode 100644 index 000000000..284bf0c4e --- /dev/null +++ b/models/mdp/resource-gathering/sketch.templ @@ -0,0 +1,95 @@ +mdp + +const int WIDTH = 5; +const int HEIGHT = 5; +const int XINIT = 3; +const int YINIT = 1; + +const int GOLD_TO_COLLECT = 1; // Set to 0 to avoid unfolding +const int GEM_TO_COLLECT = 0; // Set to 0 to avoid unfolding + +const double pAttack = 1/10; + +formula left_of_gold = x=2 & y=5; +formula right_of_gold = x=4 & y=5; +formula below_of_gold = (x=3 & y=4); +formula above_of_gold = false; +formula left_of_gem = (x=4 & y=4); +formula right_of_gem = false; +formula below_of_gem = (x=5 & y=3); +formula above_of_gem = (x=5 & y=5); +formula left_of_home = x=2 & y=1; +formula right_of_home = x=4 & y=1; +formula above_of_home = x=3 & y=2; +formula below_of_home = false; +formula left_of_enemy = (x=3 & y=5) | (x=2 & y=4); +formula right_of_enemy = (x=5 & y=5) | (x=4 & y=4); +formula above_of_enemy = x=3 & y=5; +formula below_of_enemy = (x=3 & y=3) | (x=4 & y=4); + +module robot + + gold : bool init false; + gem : bool init false; + attacked : bool init false; + + x : [1..WIDTH] init XINIT; + y : [1..HEIGHT] init YINIT; + + [right] !left_of_enemy & x (attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); + [left] !right_of_enemy & x>1 -> (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); + [top] !below_of_enemy & y (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); + [down] !above_of_enemy & y>1 -> (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); + + [right] left_of_enemy & x pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); + [left] right_of_enemy & x>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); + [top] below_of_enemy & y pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); + [down] above_of_enemy & y>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); +endmodule + +rewards "attacks" + attacked : 1; +endrewards + +rewards "rew_gold" + [right] left_of_home & gold : 1; + [left] right_of_home & gold : 1; + [top] below_of_home & gold : 1; + [down] above_of_home & gold : 1; +endrewards + +rewards "rew_gem" + [right] left_of_home & gem : 1; + [left] right_of_home & gem : 1; + [top] below_of_home & gem : 1; + [down] above_of_home & gem: 1; +endrewards + +module goldcounter + + required_gold : [0..GOLD_TO_COLLECT] init GOLD_TO_COLLECT; + + [right] true -> (required_gold'=max(0, required_gold - (left_of_home & gold ? 1: 0))); + [left] true -> (required_gold'=max(0, required_gold - (right_of_home & gold ? 1 : 0))); + [top] true -> (required_gold'=max(0, required_gold - (below_of_home & gold ? 1 : 0))); + [down] true -> (required_gold'=max(0, required_gold - (above_of_home & gold ? 1 : 0))); +endmodule + +module gemcounter + + required_gem : [0..GEM_TO_COLLECT] init GEM_TO_COLLECT; + + [right] true -> (required_gem'=max(0, required_gem - (left_of_home & gem ? 1: 0))); + [left] true -> (required_gem'=max(0, required_gem - (right_of_home & gem ? 1 : 0))); + [top] true -> (required_gem'=max(0, required_gem - (below_of_home & gem ? 1 : 0))); + [down] true -> (required_gem'=max(0, required_gem - (above_of_home & gem ? 1 : 0))); +endmodule + +label "success" = required_gold=0 & required_gem=0; + +rewards "steps" + [right] true: 1; + [left] true: 1; + [top] true: 1; + [down] true: 1; +endrewards diff --git a/models/mdp/zeroconf/sketch.props b/models/mdp/zeroconf/sketch.props deleted file mode 100644 index 26954192d..000000000 --- a/models/mdp/zeroconf/sketch.props +++ /dev/null @@ -1,4 +0,0 @@ -// Maximum probability of configuring correctly -Pmax=? [ F (l=4 & ip=1) ]; -// Minimum probability of configuring correctly -//Pmin=? [ F (l=4 & ip=1) ]; diff --git a/models/mdp/zeroconf/sketch.templ b/models/mdp/zeroconf/sketch.templ deleted file mode 100644 index 383efdd4b..000000000 --- a/models/mdp/zeroconf/sketch.templ +++ /dev/null @@ -1,258 +0,0 @@ -// IPv4: PTA model with digitial clocks -// one concrete host attempting to choose an ip address -// when a number of (abstract) hosts have already got ip addresses -// gxn/dxp/jzs 02/05/03 - -//------------------------------------------------------------- - -// we suppose that -// - the abstract hosts have already picked their addresses -// and always defend their addresses -// - the concrete host never picks the same ip address twice -// (this can happen only with a verys small probability) - -// under these assumptions we do not need message types because: -// 1) since messages to the concrete host will never be a probe, -// this host will react to all messages in the same way -// 2) since the abstract hosts always defend their addresses, -// all messages from the host will get an arp reply if the ip matches - -// following from the above assumptions we require only three abstract IP addresses -// (0,1 and 2) which correspond to the following sets of IP addresses: - -// 0 - the IP addresses of the abstract hosts which the concrete host -// previously tried to configure -// 1 - an IP address of an abstract host which the concrete host is -// currently trying to configure -// 2 - a fresh IP address which the concrete host is currently trying to configure - -// if the host picks an address that is being used it may end up picking another ip address -// in which case there may still be messages corresponding to the old ip address -// to be sent both from and to the host which the host should now disregard -// (since it will never pick the same ip address) - -// to deal with this situation: when a host picks a new ip address we reconfigure the -// messages that are still be be sent or are being sent by changing the ip address to 0 -// (an old ip address of the host) - -// all the messages from the abstract hosts for the 'old' address (in fact the -// set of old addresses since it may have started again more than once) -// can arrive in any order since they are equivalent to the host - it ignores then all - -// also the messages for the old and new address will come from different hosts -// (the ones with that ip address) which we model by allowing them to arrive in any order -// i.e. not neccessarily in the order they where sent - -//------------------------------------------------------------- -// model is an mdp -mdp - -//------------------------------------------------------------- -// VARIABLES -// reset or noreset model -const bool reset; - -const int N; // number of abstract hosts -const int K; // number of probes to send -const double loss = 0.1; // probability of message loss - -// PROBABILITIES -const double old = N/65024; // probability pick an ip address being used -const double new = (1-old); // probability pick a new ip address - -// TIMING CONSTANTS -const int CONSEC = 2; // time interval between sending consecutive probles -const int TRANSTIME = 1; // upper bound on transmission time delay -const int LONGWAIT = 60; // minimum time delay after a high number of address collisions -const int DEFEND = 10; - -const int TIME_MAX_X = 60; // max value of clock x -const int TIME_MAX_Y = 10; // max value of clock y -const int TIME_MAX_Z = 1; // max value of clock z - -// OTHER CONSTANTS -const int MAXCOLL = 10; // maximum number of collisions before long wait -// size of buffers for other hosts -const int B0 = 20; // buffer size for one abstract host -const int B1 = 8; // buffer sizes for all abstract hosts - -//------------------------------------------------------------- -// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts -module environment - - // buffer of concrete host - b_ip7 : [0..2]; // ip address of message in buffer position 8 - b_ip6 : [0..2]; // ip address of message in buffer position 7 - b_ip5 : [0..2]; // ip address of message in buffer position 6 - b_ip4 : [0..2]; // ip address of message in buffer position 5 - b_ip3 : [0..2]; // ip address of message in buffer position 4 - b_ip2 : [0..2]; // ip address of message in buffer position 3 - b_ip1 : [0..2]; // ip address of message in buffer position 2 - b_ip0 : [0..2]; // ip address of message in buffer position 1 - n : [0..8]; // number of places in the buffer used (from host) - - // messages to be sent from abstract hosts to concrete host - n0 : [0..B0]; // number of messages which do not have the host's current ip address - n1 : [0..B1]; // number of messages which have the host's current ip address - - b : [0..2]; // local state - // 0 - idle - // 1 - sending message from concrete host - // 2 - sending message from abstract host - - z : [0..1]; // clock of environment (needed for the time to send a message) - - ip_mess : [0..2]; // ip in the current message being sent - // 0 - different from concrete host - // 1 - same as the concrete host and in use - // 2 - same as the concrete host and not in use - - // RESET/RECONFIG: when host is about to choose new ip address - // suppose that the host cannot choose the same ip address - // (since happens with very small probability). - // Therefore all messages will have a different ip address, - // i.e. all n1 messages become n0 ones. - // Note this include any message currently being sent (ip is set to zero 0) - [reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers - & (ip_mess'=0) // message being set - & (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) - & (b_ip7'=0) - & (b_ip6'=0) - & (b_ip5'=0) - & (b_ip4'=0) - & (b_ip3'=0) - & (b_ip2'=0) - & (b_ip1'=0) - & (b_ip0'=0); - // note: prevent anything else from happening when reconfiguration needs to take place - - // time passage (only if no messages to send or sending a message) - [time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message - [time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message - - // get messages to be sent (so message has same ip address as host) - [send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1); - [send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1); - [send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1); - [send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1); - [send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1); - [send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1); - [send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1); - [send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1); - [send] l>0 & n=8 -> (n'=n); // buffer full so lose message - - // start sending message from host - [] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) - & (n'=n-1) - & (b_ip7'=0) - & (b_ip6'=b_ip7) - & (b_ip5'=b_ip6) - & (b_ip4'=b_ip5) - & (b_ip3'=b_ip4) - & (b_ip2'=b_ip3) - & (b_ip1'=b_ip2) - & (b_ip0'=b_ip1) // send message - + loss : (n'=n-1) - & (b_ip7'=0) - & (b_ip6'=b_ip7) - & (b_ip5'=b_ip6) - & (b_ip4'=b_ip5) - & (b_ip3'=b_ip4) - & (b_ip2'=b_ip3) - & (b_ip1'=b_ip2) - & (b_ip0'=b_ip1); // lose message - - // start sending message to host - [] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip - [] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip - - // finish sending message from host - [] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); - [] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); - [] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); - - // finish sending message to host - [rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0); - -endmodule - -//------------------------------------------------------------- -// CONCRETE HOST -module host0 - - x : [0..TIME_MAX_X]; // first clock of the host - y : [0..TIME_MAX_Y]; // second clock of the host - - coll : [0..MAXCOLL]; // number of address collisions - probes : [0..K]; // counter (number of probes sent) - mess : [0..1]; // need to send a message or not - defend : [0..1]; // defend (if =1, try to defend IP address) - - ip : [1..2]; // ip address (1 - in use & 2 - fresh) - - l : [0..4] init 1; // location - // 0 : RECONFIGURE - // 1 : RANDOM - // 2 : WAITSP - // 3 : WAITSG - // 4 : USE - - // RECONFIGURE - [reset] l=0 -> (l'=1); - - // RANDOM (choose IP address) - [rec] (l=1) -> true; // get message (ignore since have no ip address) - // small number of collisions (choose straight away) - [] l=1 & coll 1/3*old : (l'=2) & (ip'=1) & (x'=0) - + 1/3*old : (l'=2) & (ip'=1) & (x'=1) - + 1/3*old : (l'=2) & (ip'=1) & (x'=2) - + 1/3*new : (l'=2) & (ip'=2) & (x'=0) - + 1/3*new : (l'=2) & (ip'=2) & (x'=1) - + 1/3*new : (l'=2) & (ip'=2) & (x'=2); - // large number of collisions: (wait for LONGWAIT) - [time] l=1 & coll=MAXCOLL & x (x'=min(x+1,TIME_MAX_X)); - [] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) - + 1/3*old : (l'=2) & (ip'=1) & (x'=1) - + 1/3*old : (l'=2) & (ip'=1) & (x'=2) - + 1/3*new : (l'=2) & (ip'=2) & (x'=0) - + 1/3*new : (l'=2) & (ip'=2) & (x'=1) - + 1/3*new : (l'=2) & (ip'=2) & (x'=2); - - // WAITSP - // let time pass - [time] l=2 & x<2 -> (x'=min(x+1,2)); - // send probe - [send] l=2 & x=2 & probes (x'=0) & (probes'=probes+1); - // sent K probes and waited 2 seconds - [] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0); - // get message and ip does not match: ignore - [rec] l=2 & ip_mess!=ip -> (l'=l); - // get a message with matching ip: reconfigure - [rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0); - - // WAITSG (sends two gratuitious arp probes) - // time passage - [time] l=3 & mess=0 & defend=0 & x (x'=min(x+1,TIME_MAX_X)); - [time] l=3 & mess=0 & defend=1 & x (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND)); - - // receive message and same ip: defend - [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0); - // receive message and same ip: defer - [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0); - // receive message and different ip - [rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l); - - - // send probe reply or message for defence - [send] l=3 & mess=1 -> (mess'=0); - // send first gratuitous arp message - [send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1); - // send second gratuitous arp message (move to use) - [send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0); - - // USE (only interested in reaching this state so do not need to add anything here) - [] l=4 -> true; - -endmodule - - diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index 2f86bc538..d12d86f48 100644 --- a/paynt/parser/sketch.py +++ b/paynt/parser/sketch.py @@ -120,7 +120,8 @@ def load_sketch(cls, sketch_path, properties_path, updated = payntbind.synthesis.addMissingChoiceLabels(explicit_quotient) if updated is not None: explicit_quotient = updated - payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.choice_labeling) + if not payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.nondeterministic_choice_indices,explicit_quotient.choice_labeling,False): + logger.warning("WARNING: choice labeling for the quotient is not canonic") make_rewards_action_based(explicit_quotient) logger.debug("constructed explicit quotient having {} states and {} actions".format( diff --git a/paynt/quotient/mdp.py b/paynt/quotient/mdp.py index a644a3b38..bd3469c3c 100644 --- a/paynt/quotient/mdp.py +++ b/paynt/quotient/mdp.py @@ -66,9 +66,15 @@ class DecisionTreeNode: def __init__(self, parent): self.parent = parent - self.is_terminal = True self.variable_index = None + self.child_false = None + self.child_true = None self.hole = None + self.identifier = None + + @property + def is_terminal(self): + return self.variable_index is None @property def child_nodes(self): @@ -82,11 +88,10 @@ def set_variable(self, variable_index:int): ''' Associate (an index of) a variable with the node. ''' - assert self.is_terminal, "redefining existing variable for a tree node" - self.is_terminal = False + if self.is_terminal: + self.child_false = DecisionTreeNode(self) + self.child_true = DecisionTreeNode(self) self.variable_index = variable_index - self.child_false = DecisionTreeNode(self) - self.child_true = DecisionTreeNode(self) def set_variable_by_name(self, variable_name:str, decision_tree): variable_index = [variable.name for variable in decision_tree.variables].index(variable_name) @@ -101,14 +106,13 @@ def create_hole(self, family, action_labels, variables): self.hole = family.num_holes if self.is_terminal: prefix = "A" - option_labels = action_labels #+ ["__dont_care__"] + option_labels = action_labels else: prefix = variables[self.variable_index].name option_labels = variables[self.variable_index].hole_domain hole_name = f"{prefix}_{self.hole}" family.add_hole(hole_name, option_labels) - def collect_bounds(self): lower_bounds = [] upper_bounds = [] @@ -122,28 +126,39 @@ def collect_bounds(self): node = node.parent return lower_bounds,upper_bounds + def assign_identifiers(self, identifier): + self.identifier = identifier + if self.is_terminal: + return self.identifier + identifier = self.child_true.assign_identifiers(identifier+1) + identifier = self.child_false.assign_identifiers(identifier+1) + return identifier class DecisionTree: def __init__(self, model): - - self.model = model self.variables = Variable.from_model(model) logger.debug(f"found the following variables: {[str(v) for v in self.variables]}") - self.num_nodes = 0 + self.reset() + + def reset(self): self.root = DecisionTreeNode(None) - def build_coloring(self): - coloring = None - return coloring + def set_depth(self, depth:int): + self.reset() + for level in range(depth): + for node in self.collect_terminals(): + node.set_variable(0) def collect_nodes(self, node_condition=None): + if node_condition is None: + node_condition = lambda node : True node_queue = [self.root] output_nodes = [] while node_queue: node = node_queue.pop(0) - if node_condition is None or node_condition(node): + if node_condition(node): output_nodes.append(node) node_queue += node.child_nodes return output_nodes @@ -162,42 +177,16 @@ def create_family(self, action_labels): node.create_hole(family, action_labels, self.variables) return family -def custom_decision_tree(mdp): - dt = DecisionTree(mdp) - decide = lambda node,var_name : node.set_variable_by_name(var_name,dt) - - # model = "maze" - model = "obstacles" - - if model == "maze": - decide(dt.root,"clk") - main = dt.root.child_false - - # decide(decide, "y") - # decide(decide.child_true, "x") - # decide(decide.child_true.child_true, "x") - - # decide(main,"y") - # decide(main.child_false,"x") - # decide(main.child_true,"x") - # decide(main.child_true.child_true,"x") - - decide(main, "y") - decide(main.child_false, "x") - decide(main.child_false.child_true, "x") - decide(main.child_true, "x") - decide(main.child_true.child_true, "x") - - if model == "obstacles": - decide(dt.root, "x") - decide(dt.root.child_true, "x") - decide(dt.root.child_true.child_true, "y") - decide(dt.root.child_true.child_false, "y") - decide(dt.root.child_false, "x") - decide(dt.root.child_false.child_true, "y") - decide(dt.root.child_false.child_false, "y") - - return dt + def to_list(self): + self.root.assign_identifiers(0) + num_nodes = len(self.collect_nodes()) + node_info = [ None for node in range(num_nodes) ] + for node in self.collect_nodes(): + parent = num_nodes if node.parent is None else node.parent.identifier + child_true = num_nodes if node.is_terminal else node.child_true.identifier + child_false = num_nodes if node.is_terminal else node.child_false.identifier + node_info[node.identifier] = (parent,child_true,child_false) + return node_info @@ -205,44 +194,72 @@ class MdpQuotient(paynt.quotient.quotient.Quotient): def __init__(self, mdp, specification): super().__init__(specification=specification) - updated = payntbind.synthesis.restoreActionsInAbsorbingStates(mdp) if updated is not None: mdp = updated - self.quotient_mdp = mdp - paynt_mdp = paynt.models.models.Mdp(mdp) - logger.info(f"optimal scheduler has value: {paynt_mdp.model_check_property(self.get_property())}") self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(mdp) self.action_labels,self.choice_to_action = payntbind.synthesis.extractActionLabels(mdp) + self.decision_tree = DecisionTree(mdp) + + self.coloring = None + self.design_space = None - decision_tree = custom_decision_tree(mdp) - family = decision_tree.create_family(self.action_labels) - print("family = ", family) + self.is_action_hole = None + + def decide(self, node, var_name): + node.set_variable_by_name(var_name,self.decision_tree) + + ''' + Build the design space and coloring corresponding to the current decision tree. + ''' + def build_coloring(self): + family = self.decision_tree.create_family(self.action_labels) + # print("family = ", family) hole_bounds = [None for hole in range(family.num_holes)] - for node in decision_tree.collect_nodes(): + for node in self.decision_tree.collect_nodes(): hole_bounds[node.hole] = node.collect_bounds() # print("hole bounds = ", hole_bounds) - sv = mdp.state_valuations hole_variable = ["" for _ in range(family.num_holes)] hole_domain = [[] for h in range(family.num_holes)] - for node in decision_tree.collect_nonterminals(): - hole_variable[node.hole] = decision_tree.variables[node.variable_index].name + for node in self.decision_tree.collect_nonterminals(): + hole_variable[node.hole] = self.decision_tree.variables[node.variable_index].name hole_domain[node.hole] = family.hole_to_option_labels[node.hole] # print("hole variables = ", hole_variable) # print("hole domain = ", hole_domain) - self.decision_tree = decision_tree self.is_action_hole = [var == "" for var in hole_variable] self.coloring = payntbind.synthesis.ColoringSmt( - mdp.nondeterministic_choice_indices, self.choice_to_action, - mdp.state_valuations, - hole_variable, hole_bounds, - family.family, hole_domain + self.quotient_mdp.nondeterministic_choice_indices, self.choice_to_action, + self.quotient_mdp.state_valuations, + hole_variable, hole_bounds, hole_domain ) self.design_space = paynt.family.family.DesignSpace(family) + def build_coloring_full(self): + + variables = self.decision_tree.variables + variable_name = [v.name for v in variables] + variable_domain = [v.domain for v in variables] + tree_list = self.decision_tree.to_list() + self.coloring = payntbind.synthesis.ColoringSmtFull( + self.quotient_mdp.nondeterministic_choice_indices, self.choice_to_action, + self.quotient_mdp.state_valuations, + variable_name, variable_domain, tree_list + ) + # reconstruct the family + family = paynt.family.family.Family() + for hole_name,hole_type in self.coloring.getFamilyInfo(): + if hole_type == "__action__": + option_labels = self.action_labels + elif hole_type == "__decision__": + option_labels = variable_name + else: + variable = variable_name.index(hole_type) + option_labels = variables[variable].hole_domain + family.add_hole(hole_name, option_labels) + self.design_space = paynt.family.family.DesignSpace(family) def build_unsat_result(self): constraints_result = paynt.verification.property_result.ConstraintsResult([]) @@ -280,16 +297,17 @@ def scheduler_is_consistent(self, mdp, prop, result): state_to_choice = self.scheduler_to_state_to_choice(mdp, scheduler) choices = self.state_to_choice_to_choices(state_to_choice) consistent,hole_selection = self.areChoicesConsistent(choices, mdp) - # print(consistent, hole_selection) + # print(consistent,hole_selection) # convert selection to actual hole options - for hole,values in enumerate(hole_selection): - if self.is_action_hole[hole]: - continue - hole_selection[hole] = [self.design_space.hole_to_option_labels[hole].index(value) for value in values] + # for hole,values in enumerate(hole_selection): + # if self.is_action_hole[hole]: + # continue + # hole_selection[hole] = [self.design_space.hole_to_option_labels[hole].index(value) for value in values] for hole,options in enumerate(hole_selection): for option in options: - assert option in mdp.design_space.hole_options(hole), f"option {option} is not in the family" + assert option in mdp.design_space.hole_options(hole), \ + f"option {option} for hole {hole} ({mdp.design_space.hole_name(hole)}) is not in the family" return hole_selection, consistent @@ -348,10 +366,13 @@ def split(self, family): else: assert len(hole_assignments[splitter]) == 1 splitter_option = hole_assignments[splitter][0] - index = family.hole_options(splitter).index(splitter_option) - assert index < family.hole_num_options(splitter)-1 - options = mdp.design_space.hole_options(splitter) - core_suboptions = [options[:index+1], options[index+1:]] + subfamily_options = family.hole_options(splitter) + index = subfamily_options.index(splitter_option) + if index == 0: + core_suboptions = [subfamily_options[:1], subfamily_options[1:]] + else: + core_suboptions = [subfamily_options[:index], subfamily_options[index:]] + for options in core_suboptions: assert len(options) > 0 other_suboptions = [] new_design_space = mdp.design_space.copy() diff --git a/paynt/synthesizer/all_in_one.py b/paynt/synthesizer/all_in_one.py index f3ccd1cfd..0d21b2cea 100644 --- a/paynt/synthesizer/all_in_one.py +++ b/paynt/synthesizer/all_in_one.py @@ -39,7 +39,7 @@ def __init__(self, all_in_one_program, specification, approach, memory_limit_mb, logger.info(f"constructed all in one MDP having {self.model.nr_states} states and {self.model.nr_choices} actions") - def run(self): + def synthesize(self, optimum_threshold=None): all_in_one_timer = paynt.utils.profiler.Timer() logger.info(f"starting all in one analysis") diff --git a/paynt/synthesizer/decision_tree.py b/paynt/synthesizer/decision_tree.py new file mode 100644 index 000000000..01174f0ca --- /dev/null +++ b/paynt/synthesizer/decision_tree.py @@ -0,0 +1,136 @@ +import paynt.synthesizer.synthesizer_ar +import paynt.quotient.mdp + +import logging +logger = logging.getLogger(__name__) + +class SynthesizerDecisionTree(paynt.synthesizer.synthesizer_ar.SynthesizerAR): + + @property + def method_name(self): + return "AR (decision tree)" + + def verify_family(self, family): + self.stat.iteration_smt() + self.quotient.build(family) + if family.mdp is None: + return + self.stat.iteration_mdp(family.mdp.states) + res = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices) + if res.improving_assignment == "any": + res.improving_assignment = family + family.analysis_result = res + + + def set_decision_tree(self): + dt = self.quotient.decision_tree + + # model = "maze" + model = "obstacles" + + if model == "maze": + self.quotient.decide(dt.root,"clk") + main = dt.root.child_false + + # decide(decide, "y") + # decide(decide.child_true, "x") + # decide(decide.child_true.child_true, "x") + + # decide(main,"y") + # decide(main.child_false,"x") + # decide(main.child_true,"x") + # decide(main.child_true.child_true,"x") + + self.quotient.decide(main, "y") + self.quotient.decide(main.child_false, "x") + self.quotient.decide(main.child_false.child_true, "x") + self.quotient.decide(main.child_true, "x") + self.quotient.decide(main.child_true.child_true, "x") + + if model == "obstacles": + self.quotient.decide(dt.root, "x") + self.quotient.decide(dt.root.child_true, "x") + self.quotient.decide(dt.root.child_true.child_true, "y") + self.quotient.decide(dt.root.child_true.child_false, "y") + self.quotient.decide(dt.root.child_false, "x") + self.quotient.decide(dt.root.child_false.child_true, "y") + self.quotient.decide(dt.root.child_false.child_false, "y") + + + def evaluate_tree(self): + # self.quotient.build_coloring() + self.quotient.build_coloring_full() + assignment = self.synthesize(keep_optimum=True, print_stats=True) + if assignment is not None: + self.best_assignment = assignment + self.best_configuration = self.configuration.copy() + if self.quotient.specification.has_optimality: + logger.info(f"new optimum found: {self.quotient.specification.optimality.optimum}") + print("synthesized, OK") + exit() + + + def configuration_init(self): + self.configuration = [0 for node in self.quotient.decision_tree.collect_nonterminals()] + + def configuration_next(self): + num_variables = len(self.quotient.decision_tree.variables) + for node_index,variable in reversed(list(enumerate(self.configuration))): + variable_new = (variable+1) % num_variables + self.configuration[node_index] = variable_new + if variable_new != 0: + return True + return False + + def configuration_evaluate(self): + logger.debug(f"synthesizing configuration: {self.configuration}") + nodes = self.quotient.decision_tree.collect_nonterminals() + for node,variable in zip(nodes,self.configuration): + node.set_variable(variable) + self.evaluate_tree() + + def iterate_tree(self, depth:int): + self.quotient.decision_tree.set_depth(depth) + self.configuration_init() + while True: + self.configuration_evaluate() + configuration_valid = self.configuration_next() + if not configuration_valid: + break + + def iterate_trees(self, max_depth:int): + for depth in range(max_depth+1): + self.iterate_tree(depth) + + + def run(self, optimum_threshold=None, export_evaluation=None): + paynt_mdp = paynt.models.models.Mdp(self.quotient.quotient_mdp) + mc_result = paynt_mdp.model_check_property(self.quotient.get_property()) + logger.info(f"optimal scheduler has value: {mc_result}") + + if self.quotient.specification.has_optimality: + # optimum_threshold = mc_result.value * (1 + 0.1) + # optimum_threshold = mc_result.value * (1 - 0.1) + # optimum_threshold = 7 + pass + + if self.quotient.specification.has_optimality and optimum_threshold is not None: + self.quotient.specification.optimality.update_optimum(optimum_threshold) + logger.debug(f"optimality threshold set to {optimum_threshold}") + + self.best_assignment = None + self.best_configuration = None + # self.iterate_trees(max_depth = 3) + self.iterate_tree(2) + + if self.best_assignment is not None: + logger.info(f"admissible assignment found: {self.best_assignment}") + logger.info(f"assignment was constructed for the following configuration: {self.best_configuration}") + if self.quotient.specification.has_optimality: + logger.info(f"best assignment has value {self.quotient.specification.optimality.optimum}") + else: + logger.info("no admissible assignment found") + + # print("payntbind::selectCompatibleChoices = ", self.quotient.coloring.selectCompatibleChoicesTime()) + + return self.best_assignment diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py index 3896eef20..d772f0a1d 100644 --- a/paynt/synthesizer/statistic.py +++ b/paynt/synthesizer/statistic.py @@ -251,8 +251,6 @@ def get_summary(self): def print(self): print(self.get_summary(),end="") - print("payntbind::selectCompatibleChoices = ", self.quotient.coloring.selectCompatibleChoicesTime()) - # self.print_mdp_family_table_entries() def print_mdp_family_table_entries(self): diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py index f12837f9c..afe3c790e 100644 --- a/paynt/synthesizer/synthesizer.py +++ b/paynt/synthesizer/synthesizer.py @@ -19,6 +19,7 @@ class Synthesizer: def choose_synthesizer(quotient, method, fsc_synthesis, storm_control): # hiding imports here to avoid mutual top-level imports + import paynt.quotient.mdp import paynt.quotient.pomdp import paynt.quotient.decpomdp import paynt.quotient.mdp_family @@ -30,11 +31,14 @@ def choose_synthesizer(quotient, method, fsc_synthesis, storm_control): import paynt.synthesizer.synthesizer_pomdp import paynt.synthesizer.synthesizer_decpomdp import paynt.synthesizer.policy_tree + import paynt.synthesizer.decision_tree if isinstance(quotient, paynt.quotient.pomdp_family.PomdpFamilyQuotient): logger.info("nothing to do with the POMDP sketch, aborting...") exit(0) + if isinstance(quotient, paynt.quotient.mdp.MdpQuotient): + return paynt.synthesizer.decision_tree.SynthesizerDecisionTree(quotient) # FSC synthesis for POMDPs if isinstance(quotient, paynt.quotient.pomdp.PomdpQuotient) and fsc_synthesis: return paynt.synthesizer.synthesizer_pomdp.SynthesizerPomdp(quotient, method, storm_control) @@ -48,7 +52,8 @@ def choose_synthesizer(quotient, method, fsc_synthesis, storm_control): else: return paynt.synthesizer.policy_tree.SynthesizerPolicyTree(quotient) - # Synthesis engines + + # synthesis engines if method == "onebyone": return paynt.synthesizer.synthesizer_onebyone.SynthesizerOneByOne(quotient) if method == "ar": @@ -64,8 +69,8 @@ def choose_synthesizer(quotient, method, fsc_synthesis, storm_control): def __init__(self, quotient): self.quotient = quotient - self.stat = paynt.synthesizer.statistic.Statistic(self) - self.explored = 0 + self.stat = None + self.explored = None @property def method_name(self): @@ -100,6 +105,8 @@ def evaluate(self, family=None, prop=None, keep_value_only=False, print_stats=Tr if prop is None: prop = self.quotient.get_property() + self.stat = paynt.synthesizer.statistic.Statistic(self) + self.explored = 0 logger.info("evaluation initiated, design space: {}".format(family.size)) self.stat.start(family) evaluations = self.evaluate_all(family, prop, keep_value_only) @@ -133,18 +140,20 @@ def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, re if family.constraint_indices is None: family.constraint_indices = list(range(len(self.quotient.specification.constraints))) - if optimum_threshold is not None: + if self.quotient.specification.has_optimality and optimum_threshold is not None: self.quotient.specification.optimality.update_optimum(optimum_threshold) logger.debug(f"optimality threshold set to {optimum_threshold}") - logger.info("synthesis initiated, design space: {}".format(family.size_or_order)) + self.stat = paynt.synthesizer.statistic.Statistic(self) + self.explored = 0 + # logger.info("synthesis initiated, design space: {}".format(family.size_or_order)) self.stat.start(family) assignment = self.synthesize_one(family) if assignment is not None and assignment.size > 1 and not return_all: assignment = assignment.pick_any() self.stat.finished_synthesis(assignment) - logger.info("synthesis finished, printing synthesized assignment below:") - logger.info(assignment) + # logger.info("synthesis finished, printing synthesized assignment below:") + # logger.info(assignment) if assignment is not None and assignment.size == 1: dtmc = self.quotient.build_assignment(assignment) diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py index 6f3ca798e..7d33c7d92 100644 --- a/paynt/synthesizer/synthesizer_ar.py +++ b/paynt/synthesizer/synthesizer_ar.py @@ -12,10 +12,7 @@ def method_name(self): return "AR" def verify_family(self, family): - # self.stat.iteration_smt() self.quotient.build(family) - if family.mdp is None: - return self.stat.iteration_mdp(family.mdp.states) res = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices) if res.improving_assignment == "any": diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index 4826667d2..6809b55cd 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -13,23 +13,22 @@ ColoringSmt::ColoringSmt( storm::storage::sparse::StateValuations const& state_valuations, std::vector const& hole_to_variable_name, std::vector,std::vector>> hole_bounds, - synthesis::Family const& family, std::vector> hole_domain -) : choice_to_action(choice_to_action), row_groups(row_groups), family(family), hole_domain(hole_domain), solver(context) { - - num_actions = 1 + *max_element(choice_to_action.begin(),choice_to_action.end()); +) : choice_to_action(choice_to_action), row_groups(row_groups), hole_domain(hole_domain), solver(context) { + + uint64_t num_holes = hole_bounds.size(); std::vector variables; auto const& valuation = state_valuations.at(0); for(auto x = valuation.begin(); x != valuation.end(); ++x) { variables.push_back(x.getVariable()); } - std::vector hole_variable(family.numHoles(),variables.size()); + std::vector hole_variable(num_holes,variables.size()); - hole_corresponds_to_program_variable = storm::storage::BitVector(family.numHoles()); + hole_corresponds_to_program_variable = BitVector(num_holes); // create solver variables for each hole - for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + for(uint64_t hole = 0; hole < num_holes; ++hole) { std::string const& var_name = hole_to_variable_name[hole]; bool corresponds_to_program_variable = (var_name != ""); hole_corresponds_to_program_variable.set(hole,corresponds_to_program_variable); @@ -52,10 +51,10 @@ ColoringSmt::ColoringSmt( } // create formula describing hole relationships - for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { - uint64_t var = hole_variable[hole]; + for(uint64_t hole = 0; hole < num_holes; ++hole) { z3::expr_vector restriction_clauses(context); if(hole_corresponds_to_program_variable[hole]) { + uint64_t var = hole_variable[hole]; // see if any of its bounds is a hole associated with the same variable auto solver_variable = hole_to_solver_variable[hole]; auto const& [lower_bounds,upper_bounds] = hole_bounds[hole]; @@ -66,7 +65,7 @@ ColoringSmt::ColoringSmt( } for(auto bound: upper_bounds) { if(hole_variable[bound] == var) { - restriction_clauses.push_back(solver_variable <= hole_to_solver_variable[bound]); + restriction_clauses.push_back(solver_variable < hole_to_solver_variable[bound]); } } } @@ -78,16 +77,16 @@ ColoringSmt::ColoringSmt( for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { uint64_t action = choice_to_action[choice]; - std::vector terminals; + std::vector paths; std::vector>> terminal_evaluation; z3::expr_vector clauses(context); std::vector clause_label; // for each action hole, create clauses that describe this choice selection for(uint64_t hole: ~hole_corresponds_to_program_variable) { auto const& [lower_bounds,upper_bounds] = hole_bounds[hole]; - z3::expr_vector terminal_atoms(context); + z3::expr_vector path(context); std::vector> evaluation; - terminal_atoms.push_back((hole_to_solver_variable[hole] == (int)action)); + path.push_back((hole_to_solver_variable[hole] == (int)action)); evaluation.emplace_back(hole,(int)action); // add atoms describing lower and upper bounds @@ -97,27 +96,27 @@ ColoringSmt::ColoringSmt( auto program_variable = variables[hole_variable[bound]]; auto solver_variable = hole_to_solver_variable[bound]; int value = getVariableValueAtState(state_valuations,state,program_variable); - terminal_atoms.push_back(value <= solver_variable); + path.push_back(value <= solver_variable); evaluation.emplace_back(bound,value); } for(auto bound: upper_bounds) { auto program_variable = variables[hole_variable[bound]]; auto solver_variable = hole_to_solver_variable[bound]; int value = getVariableValueAtState(state_valuations,state,program_variable); - terminal_atoms.push_back(value > solver_variable); + path.push_back(value > solver_variable); evaluation.emplace_back(bound,value); } uint64_t clause_index = clauses.size(); std::string label = "c" + std::to_string(choice) + "_" + std::to_string(clause_index); - terminals.push_back(terminal_atoms); + paths.push_back(path); terminal_evaluation.push_back(evaluation); - clauses.push_back(z3::mk_or(terminal_atoms)); + clauses.push_back(z3::mk_or(path)); clause_label.push_back(label); } - choice_terminal.push_back(terminals); + choice_path.push_back(paths); choice_clause.push_back(clauses); - choice_terminal_evaluation.push_back(terminal_evaluation); + choice_path_evaluation.push_back(terminal_evaluation); choice_clause_label.push_back(clause_label); } } @@ -133,14 +132,13 @@ const uint64_t ColoringSmt::numChoices() const { } int ColoringSmt::getVariableValueAtState( - storm::storage::sparse::StateValuations const& state_valuations, uint64_t state, storm::expressions::Variable variable + storm::storage::sparse::StateValuations const& state_valuations, uint64_t state, storm::expressions::Variable variable ) const { if(variable.hasBooleanType()) { return (int)state_valuations.getBooleanValue(state,variable); } else { return state_valuations.getIntegerValue(state,variable); } - } void ColoringSmt::addHoleEncoding(Family const& family, uint64_t hole) { @@ -154,8 +152,8 @@ void ColoringSmt::addHoleEncoding(Family const& family, uint64_t hole) { // convention: hole options in the family are ordered int domain_min = domain[family_options.front()]; int domain_max = domain[family_options.back()]; - // z3::expr encoding = (domain_min <= solver_variable) and (solver_variable <= domain_max) and hole_restriction[hole]; - z3::expr encoding = (domain_min <= solver_variable) and (solver_variable <= domain_max); + z3::expr encoding = (domain_min <= solver_variable) and (solver_variable <= domain_max) and hole_restriction[hole]; + // z3::expr encoding = (domain_min <= solver_variable) and (solver_variable <= domain_max); solver.add(encoding, label_str); } else { // action hole @@ -203,7 +201,6 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamily, BitVecto // check individual choices std::vector> state_enabled_choices(numStates()); for(uint64_t state = 0; state < numStates(); ++state) { - bool all_choices_disabled = true; for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { if(not base_choices[choice]) { continue; @@ -214,13 +211,12 @@ BitVector ColoringSmt::selectCompatibleChoices(Family const& subfamily, BitVecto z3::check_result result = solver.check(); selectCompatibleChoicesTimer.stop(); if(result == z3::sat) { - all_choices_disabled = false; selection.set(choice,true); state_enabled_choices[state].push_back(choice); } solver.pop(); } - if(all_choices_disabled) { + if(state_enabled_choices[state].empty()) { solver.pop(); selection.clear(); return selection; @@ -250,17 +246,20 @@ std::pair>> ColoringSmt::areChoicesConsis solver.push(); addFamilyEncoding(subfamily); + solver.push(); for(auto choice: choices) { addChoiceEncoding(choice); } z3::check_result result = solver.check(); - std::vector> hole_options(family.numHoles()); - std::vector> hole_options_vector(family.numHoles()); + uint64_t num_holes = subfamily.numHoles(); + std::vector> hole_options(num_holes); + std::vector> hole_options_vector(num_holes); if(result == z3::sat) { z3::model model = solver.get_model(); solver.pop(); - for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + solver.pop(); + for(uint64_t hole = 0; hole < num_holes; ++hole) { z3::expr solver_variable = hole_to_solver_variable[hole]; uint64_t value = model.eval(solver_variable).get_numeral_int64(); hole_options_vector[hole].push_back(value); @@ -270,37 +269,33 @@ std::pair>> ColoringSmt::areChoicesConsis z3::expr_vector unsat_core = solver.unsat_core(); solver.pop(); - for(auto expr: unsat_core) { + for(z3::expr expr: unsat_core) { std::istringstream iss(expr.decl().name().str()); char prefix; iss >> prefix; if(prefix == 'h') { continue; } - // choice clause - uint64_t choice,clause; iss >> choice; iss >> prefix; iss >> clause; + uint64_t choice,path; iss >> choice; iss >> prefix; iss >> path; uint64_t action = choice_to_action[choice]; - uint64_t action_hole; - // filter clauses that are unsat within the subfamily - // std::cout << "checking: " << choice_clause[choice][clause] << std::endl; - solver.push(); - addFamilyEncoding(subfamily); - for(uint64_t terminal = 0; terminal < choice_terminal[choice][clause].size(); ++terminal) { + // filter paths that are unsat within the subfamily + // std::cout << "checking: " << choice_path[choice][path] << std::endl; + for(uint64_t terminal = 0; terminal < choice_path[choice][path].size(); ++terminal) { solver.push(); - solver.add(choice_terminal[choice][clause][terminal]); + solver.add(choice_path[choice][path][terminal]); auto result = solver.check(); solver.pop(); if(result == z3::unsat) { continue; } - // std::cout << choice_terminal[choice][clause][terminal] << std::endl; - auto const& [hole,value] = choice_terminal_evaluation[choice][clause][terminal]; + // std::cout << choice_path[choice][path][terminal] << std::endl; + auto const& [hole,value] = choice_path_evaluation[choice][path][terminal]; hole_options[hole].insert(value); } - solver.pop(); } + solver.pop(); - for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + for(uint64_t hole = 0; hole < num_holes; ++hole) { hole_options_vector[hole].assign(hole_options[hole].begin(),hole_options[hole].end()); } return std::make_pair(false,hole_options_vector); diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.h b/payntbind/src/synthesis/quotient/ColoringSmt.h index 66c8fff53..d72bb6087 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.h +++ b/payntbind/src/synthesis/quotient/ColoringSmt.h @@ -26,7 +26,6 @@ class ColoringSmt { storm::storage::sparse::StateValuations const& state_valuations, std::vector const& hole_to_variable_name, std::vector,std::vector>> hole_bounds, - Family const& family, std::vector> hole_domain ); @@ -48,17 +47,15 @@ class ColoringSmt { protected: - /** Number of MDP actions. */ - uint64_t num_actions; + /** Row groups of the quotient. */ + const std::vector row_groups; /** For each choice, its unique action. */ const std::vector choice_to_action; - /** Row groups of the quotient. */ - std::vector row_groups; /** Number of states in the quotient. */ const uint64_t numStates() const; /** Number of choices in the quotient. */ const uint64_t numChoices() const; - + /** SMT solver context. */ z3::context context; /** SMT solver. */ @@ -68,24 +65,17 @@ class ColoringSmt { /** For each hole, an expression describing its relation to other holes. */ std::vector hole_restriction; - /** - * For each choice, its color expressed as a list of conjuncts (clauses) of - * disjuncts of atomic clauses (terminals). - * */ - std::vector> choice_terminal; + /** For each choice, its color expressed as a list of paths consisting of steps. */ + std::vector> choice_path; /** For each terminal, a (unique) hole assignment involved. */ - std::vector>>> choice_terminal_evaluation; + std::vector>>> choice_path_evaluation; /** For each choice, its color expressed as a list of clauses. */ std::vector choice_clause; /** For each clause, a predefined label. */ std::vector> choice_clause_label; - - - /** Reference to the unrefined family. */ - const Family family; /** For each hole associated with an integer variable, a list of its integer options. */ std::vector> hole_domain; /** For each hole, whether it corresponds to a variable (and not to action selection). */ diff --git a/payntbind/src/synthesis/quotient/ColoringSmtFull.cpp b/payntbind/src/synthesis/quotient/ColoringSmtFull.cpp new file mode 100644 index 000000000..e2170946f --- /dev/null +++ b/payntbind/src/synthesis/quotient/ColoringSmtFull.cpp @@ -0,0 +1,274 @@ +#include "ColoringSmtFull.h" + +#include +#include +#include + +#include + +namespace synthesis { + +ColoringSmtFull::ColoringSmtFull( + std::vector const& row_groups, + std::vector const& choice_to_action, + storm::storage::sparse::StateValuations const& state_valuations, + std::vector const& variable_name, + std::vector> const& variable_domain, + std::vector> const& tree_list +) : choice_to_action(choice_to_action), row_groups(row_groups), + variable_name(variable_name), variable_domain(variable_domain), + solver(ctx), substitution_variables(ctx) { + + // extract variables in the order of variable_name + std::vector program_variables; + auto const& valuation = state_valuations.at(0); + for(auto const& name: variable_name) { + bool variable_found = false; + for(auto x = valuation.begin(); x != valuation.end(); ++x) { + storm::expressions::Variable const& program_variable = x.getVariable(); + if(program_variable.getName() == name) { + program_variables.push_back(program_variable); + variable_found = true; + break; + } + } + STORM_LOG_THROW(variable_found, storm::exceptions::InvalidArgumentException, "unexpected variable name"); + } + + // create the tree + uint64_t num_nodes = tree_list.size(); + uint64_t num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())-1; + for(uint64_t node = 0; node < num_nodes; ++node) { + auto [parent,child_true,child_false] = tree_list[node]; + STORM_LOG_THROW( + (child_true != num_nodes) == (child_false != num_nodes), storm::exceptions::InvalidArgumentException, + "inner node has only one child" + ); + if(child_true != num_nodes) { + tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain)); + } else { + tree.push_back(std::make_shared(node,ctx,num_actions)); + } + } + getRoot()->createTree(tree_list,tree); + + // create substitution variables + for(auto const& name: variable_name) { + substitution_variables.push_back(ctx.int_const(name.c_str())); + } + substitution_variables.push_back(ctx.int_const("act")); + getRoot()->createHoles(family); + getRoot()->createPaths(substitution_variables); + + // collect all path expressions + std::vector path_expressions; + for(std::vector> const& path: getRoot()->paths) { + z3::expr_vector path_expression(ctx); + getRoot()->loadPathExpression(path,path_expression); + path_expressions.push_back(path_expression); + } + + // create choice substitutions + for(uint64_t state = 0; state < numStates(); ++state) { + std::vector state_substitution; + for(uint64_t variable = 0; variable < variable_name.size(); ++variable) { + storm::expressions::Variable const& program_variable = program_variables[variable]; + int value = getVariableValueAtState(state_valuations,state,program_variable); + state_substitution.push_back(value); + } + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + uint64_t action = choice_to_action[choice]; + std::vector substitution = state_substitution; + substitution.push_back(action); + choice_substitution.push_back(substitution); + z3::expr_vector substitution_expr(ctx); + for(int64_t value: substitution) { + substitution_expr.push_back(ctx.int_val(value)); + } + choice_substitution_expr.push_back(substitution_expr); + } + } + + // create choice colors + for(uint64_t state = 0; state < numStates(); ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + std::vector path_step_of_choice; + z3::expr_vector paths(ctx); + std::vector clause_label; + + // evaluate each path and create the corresponding colors + for(z3::expr_vector const& path_expression: path_expressions) { + z3::expr_vector path_step(ctx); + for(z3::expr step: path_expression) { + path_step.push_back(step.substitute(substitution_variables,choice_substitution_expr[choice])); + } + // TODO check if the clause can be satisfied + uint64_t path_index = paths.size(); + path_step_of_choice.push_back(path_step); + paths.push_back(z3::mk_or(path_step)); + std::string label = "c" + std::to_string(choice) + "_" + std::to_string(path_index); + clause_label.push_back(label); + } + + choice_path_step.push_back(path_step_of_choice); + choice_path.push_back(paths); + choice_path_label.push_back(clause_label); + } + } +} + +const uint64_t ColoringSmtFull::numStates() const { + return row_groups.size()-1; +} + +const uint64_t ColoringSmtFull::numChoices() const { + return choice_to_action.size(); +} + +uint64_t ColoringSmtFull::numNodes() const { + return tree.size(); +} + +std::shared_ptr ColoringSmtFull::getRoot() { + return tree[0]; +} + +const uint64_t ColoringSmtFull::numVariables() const { + return variable_name.size(); +} + +int ColoringSmtFull::getVariableValueAtState( + storm::storage::sparse::StateValuations const& state_valuations, uint64_t state, storm::expressions::Variable variable +) const { + if(variable.hasBooleanType()) { + return (int)state_valuations.getBooleanValue(state,variable); + } else { + return state_valuations.getIntegerValue(state,variable); + } +} + +std::vector> ColoringSmtFull::getFamilyInfo() { + std::vector> hole_info(family.numHoles()); + getRoot()->loadHoleInfo(hole_info); + return hole_info; +} + + +void ColoringSmtFull::addChoiceEncoding(uint64_t choice, bool add_label) { + if(not add_label) { + solver.add(choice_path[choice]); + return; + } + auto const& paths = choice_path[choice]; + for(uint64_t path = 0; path < paths.size(); ++path) { + solver.add(paths[path], choice_path_label[choice][path].c_str()); + } +} + +BitVector ColoringSmtFull::selectCompatibleChoices(Family const& subfamily) { + return selectCompatibleChoices(subfamily,BitVector(numChoices(),true)); +} + +BitVector ColoringSmtFull::selectCompatibleChoices(Family const& subfamily, BitVector const& base_choices) { + BitVector selection(numChoices(),false); + + // check if the subfamily itself satisfies hole restrictions + solver.push(); + getRoot()->addFamilyEncoding(subfamily,solver); + if(solver.check() == z3::unsat) { + solver.pop(); + std::cout << "family is UNSAT" << std::endl; + return selection; + } + + // check individual choices + std::vector> state_enabled_choices(numStates()); + for(uint64_t state = 0; state < numStates(); ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + if(not base_choices[choice]) { + continue; + } + solver.push(); + selectCompatibleChoicesTimer.start(); + addChoiceEncoding(choice,false); + z3::check_result result = solver.check(); + selectCompatibleChoicesTimer.stop(); + solver.pop(); + if(result == z3::sat) { + selection.set(choice,true); + state_enabled_choices[state].push_back(choice); + } + } + if(state_enabled_choices[state].empty()) { + solver.pop(); + selection.clear(); + std::cout << "no choice enabled in state " << state << std::endl; + return selection; + } + } + + // check selected choices simultaneously + solver.push(); + for(std::vector const& choices: state_enabled_choices) { + z3::expr_vector enabled_choices(ctx); + for(uint64_t choice: choices) { + enabled_choices.push_back(z3::mk_and(choice_path[choice])); + } + solver.add(z3::mk_or(enabled_choices)); + } + if(solver.check() == z3::unsat) { + std::cout << "no consistent scheduler exists " << std::endl; + selection.clear(); + } + solver.pop(); + + solver.pop(); + return selection; +} + + +std::pair>> ColoringSmtFull::areChoicesConsistent(BitVector const& choices, Family const& subfamily) { + + solver.push(); + getRoot()->addFamilyEncoding(subfamily,solver); + solver.push(); + for(auto choice: choices) { + addChoiceEncoding(choice,true); + } + z3::check_result result = solver.check(); + + std::vector> hole_options(family.numHoles()); + std::vector> hole_options_vector(family.numHoles()); + if(result == z3::sat) { + z3::model model = solver.get_model(); + solver.pop(); + solver.pop(); + getRoot()->loadHoleAssignmentFromModel(model,hole_options_vector); + return std::make_pair(true,hole_options_vector); + } + + z3::expr_vector unsat_core = solver.unsat_core(); + solver.pop(); + for(z3::expr expr: unsat_core) { + std::istringstream iss(expr.decl().name().str()); + char prefix; iss >> prefix; + if(prefix == 'h') { + continue; + } + + uint64_t choice,path; iss >> choice; iss >> prefix; iss >> path; + uint64_t action = choice_to_action[choice]; + std::cout << "checking: " << choice_path[choice][path] << std::endl; + getRoot()->loadHoleAssignmentOfPath( + solver, getRoot()->paths[path], choice_path_step[choice][path], choice_substitution[choice], substitution_variables, choice_substitution_expr[choice], hole_options + ); + } + solver.pop(); + + for(uint64_t hole = 0; hole < family.numHoles(); ++hole) { + hole_options_vector[hole].assign(hole_options[hole].begin(),hole_options[hole].end()); + } + return std::make_pair(false,hole_options_vector); +} + +} \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/ColoringSmtFull.h b/payntbind/src/synthesis/quotient/ColoringSmtFull.h new file mode 100644 index 000000000..3ad72e75e --- /dev/null +++ b/payntbind/src/synthesis/quotient/ColoringSmtFull.h @@ -0,0 +1,109 @@ +#pragma once + +#include "src/synthesis/quotient/Family.h" +#include "src/synthesis/quotient/TreeNode.h" + +#include +#include +#include + +#include +#include +#include + +#include + +namespace synthesis { + +using BitVector = storm::storage::BitVector; + +class ColoringSmtFull { +public: + + ColoringSmtFull( + std::vector const& row_groups, + std::vector const& choice_to_action, + storm::storage::sparse::StateValuations const& state_valuations, + std::vector const& variable_name, + std::vector> const& variable_domain, + std::vector> const& tree_list + ); + + std::vector> getFamilyInfo(); + + /** Get a mask of choices compatible with the family. */ + BitVector selectCompatibleChoices(Family const& subfamily); + /** Get a mask of sub-choices of \p base_choices compatible with the family. */ + BitVector selectCompatibleChoices(Family const& subfamily, BitVector const& base_choices); + + storm::utility::Stopwatch selectCompatibleChoicesTimer; + uint64_t selectCompatibleChoicesTime() { + return (uint64_t) selectCompatibleChoicesTimer.getTimeInMilliseconds(); + } + /** + * Verify whether the given choices have an associated non-conficting hole assignment (within the given family). + * @return a pair (A,B) where A is true iff the choice selection is consistent; B is either satisfying hole assignment + * if A holds, or a counterexample to be used for splitting. + * */ + std::pair>> areChoicesConsistent(BitVector const& choices, Family const& subfamily); + +protected: + + /** Number of MDP actions. */ + uint64_t num_actions; + /** Row groups of the quotient. */ + const std::vector row_groups; + /** For each choice, its unique action. */ + const std::vector choice_to_action; + /** Number of states in the quotient. */ + const uint64_t numStates() const; + /** Number of choices in the quotient. */ + const uint64_t numChoices() const; + + /** For each variable, its name. */ + const std::vector variable_name; + /** For each variable, a list of its options. */ + const std::vector> variable_domain; + /** Number of (relevant) program variables. */ + const uint64_t numVariables() const; + + /** A list of tree nodes. */ + std::vector> tree; + /** Number of tree nodes. */ + uint64_t numNodes() const; + /** Retreive tree root. */ + std::shared_ptr getRoot(); + + + + /** Unrefined family. */ + Family family; + /** SMT solver context. */ + z3::context ctx; + /** SMT solver. */ + z3::solver solver; + + /** A list of solver variables, one for each program variable and the last one for the action selection. */ + z3::expr_vector substitution_variables; + /** For each choice, the corresponding substitution. */ + std::vector> choice_substitution; + /** For each choice, the corresponding substitution (SMT expression). */ + std::vector choice_substitution_expr; + + /** For each choice, its color expressed as a list of paths consisting of steps. */ + std::vector> choice_path_step; + /** For each choice, its color expressed as a list of paths. */ + std::vector choice_path; + /** For each clause, a predefined label. */ + std::vector> choice_path_label; + + int getVariableValueAtState( + storm::storage::sparse::StateValuations const& state_valuations, uint64_t state, + storm::expressions::Variable variable + ) const; + + /** Create SMT encoding for the given choice. */ + void addChoiceEncoding(uint64_t choice, bool add_label); +}; + +} \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/Family.cpp b/payntbind/src/synthesis/quotient/Family.cpp index 1c485c0db..55c82010f 100644 --- a/payntbind/src/synthesis/quotient/Family.cpp +++ b/payntbind/src/synthesis/quotient/Family.cpp @@ -23,13 +23,15 @@ uint64_t Family::numHoles() const { return hole_options.size(); } -void Family::addHole(uint64_t num_options) { +uint64_t Family::addHole(uint64_t num_options) { + uint64_t hole_index = numHoles(); hole_options_mask.push_back(BitVector(num_options,true)); std::vector options(num_options); for(uint64_t option=0; option const& Family::holeOptions(uint64_t hole) const { diff --git a/payntbind/src/synthesis/quotient/Family.h b/payntbind/src/synthesis/quotient/Family.h index c932e293d..8c03fe44c 100644 --- a/payntbind/src/synthesis/quotient/Family.h +++ b/payntbind/src/synthesis/quotient/Family.h @@ -17,7 +17,7 @@ class Family { Family(Family const& other); uint64_t numHoles() const; - void addHole(uint64_t num_options); + uint64_t addHole(uint64_t num_options); std::vector const& holeOptions(uint64_t hole) const; BitVector const& holeOptionsMask(uint64_t hole) const; diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp new file mode 100644 index 000000000..093d641b8 --- /dev/null +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -0,0 +1,305 @@ +#include "TreeNode.h" + +#include +#include +#include + +#include + +namespace synthesis { + + +TreeNode::HoleInfo::HoleInfo(z3::context& ctx): solver_variable(ctx), restriction(ctx) { + // left intentionally blank +} + +bool TreeNode::verifyExpression(z3::solver & solver, z3::expr const& expr) { + solver.push(); + solver.add(expr); + auto result = solver.check(); + solver.pop(); + return result == z3::sat; +} + +TreeNode::TreeNode(uint64_t identifier, z3::context& ctx) : identifier(identifier), ctx(ctx) { + parent = NULL; + child_true = NULL; + child_false = NULL; + depth = 0; +} + +void TreeNode::createTree( + std::vector> const& tree_list, std::vector> & tree +) { + auto [parent_index,child_true_index,child_false_index] = tree_list[identifier]; + if(parent_index < tree.size()) { + parent = tree[parent_index]; + depth = parent->depth+1; + } + if(child_true_index < tree.size()) { + child_true = tree[child_true_index]; + child_true->createTree(tree_list,tree); + } + if(child_false_index < tree.size()) { + child_false = tree[child_false_index]; + child_false->createTree(tree_list,tree); + } +} + + +bool TreeNode::isRoot() const { + return parent == NULL; +} + +bool TreeNode::isTerminal() const { + return child_true == NULL; +} + +bool TreeNode::isTrueChild() const { + STORM_LOG_THROW(not isRoot(), storm::exceptions::IllegalFunctionCallException, "the node has no parent"); + return identifier == parent->child_true->identifier; +} + + + +TerminalNode::TerminalNode(uint64_t identifier, z3::context & ctx, uint64_t num_actions +) : TreeNode(identifier,ctx), num_actions(num_actions), action_hole(ctx), action_expr(ctx) { + // left intentionally blank +} + +void TerminalNode::createHoles(Family& family) { + action_hole.hole = family.addHole(num_actions); + action_hole.name = "A_" + std::to_string(identifier); + action_hole.solver_variable = ctx.int_const(action_hole.name.c_str()); + action_hole.solver_string = "h" + std::to_string(action_hole.hole); +} + +void TerminalNode::loadHoleInfo(std::vector> & hole_info) const { + hole_info[action_hole.hole] = std::make_pair(action_hole.name,"__action__"); +} + +void TerminalNode::createSteps(z3::expr_vector const& substitution_variables) { + action_expr = action_hole.solver_variable == substitution_variables.back(); +} + +void TerminalNode::createPaths(z3::expr_vector const& substitution_variables) { + createSteps(substitution_variables); + paths.push_back({std::make_pair(true,0)}); +} + +void TerminalNode::loadPathExpression( + std::vector> const& path, z3::expr_vector & path_expression +) const { + STORM_LOG_THROW(path_expression.size() == depth, storm::exceptions::InvalidArgumentException, "path depth error"); + path_expression.push_back(action_expr); +} + +void TerminalNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { + z3::expr_vector options(ctx); + for(uint64_t option: subfamily.holeOptions(action_hole.hole)) { + options.push_back(action_hole.solver_variable == (int)option); + } + solver.add(z3::mk_or(options), action_hole.solver_string.c_str()); + std::cout << z3::mk_or(options) << std::endl; +} + +void TerminalNode::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { + hole_options[action_hole.hole].push_back(action_hole.getModelValue(model)); +} + + + + + + +InnerNode::InnerNode( + uint64_t identifier, + z3::context & ctx, + std::vector const& variable_name, + std::vector> const& variable_domain +) : TreeNode(identifier,ctx), variable_name(variable_name), variable_domain(variable_domain), decision_hole(ctx) { + // left intentionally blank +} + + +const uint64_t InnerNode::numVariables() const { + return variable_name.size(); +} + +const uint64_t InnerNode::variableValueToHoleOption(uint64_t variable, int64_t value) const { + for(uint64_t hole_option = 0; hole_option < variable_domain[variable].size(); ++hole_option) { + if(variable_domain[variable][hole_option] == value) { + return hole_option; + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "hole option not found"); +} + +std::shared_ptr InnerNode::getChild(bool condition) const { + return condition ? child_true : child_false; +} + +std::vector const& InnerNode::getSteps(bool condition) const { + return condition ? steps_true : steps_false; +} + +void InnerNode::createHoles(Family& family) { + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + HoleInfo hole(ctx); + hole.hole = family.addHole(variable_domain[variable].size()-1); + hole.name = variable_name[variable] + "_" + std::to_string(identifier); + hole.solver_variable = ctx.int_const(hole.name.c_str()); + hole.solver_string = "h" + std::to_string(hole.hole); + variable_hole.push_back(hole); + } + decision_hole.hole = family.addHole(numVariables()); + decision_hole.name = "V_" + std::to_string(identifier); + decision_hole.solver_variable = ctx.int_const(decision_hole.name.c_str()); + decision_hole.solver_string = "h" + std::to_string(decision_hole.hole); + + if(not isRoot()) { + // add restrictions + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + z3::expr const& var_node = variable_hole[variable].solver_variable; + z3::expr const& var_parent = std::dynamic_pointer_cast(parent)->variable_hole[variable].solver_variable; + z3::expr const& dv = decision_hole.solver_variable; + if(isTrueChild()) { + variable_hole[variable].restriction = dv != (int)variable or var_node < var_parent; + } else { + variable_hole[variable].restriction = dv != (int)variable or var_node > var_parent; + } + } + } + child_true->createHoles(family); + child_false->createHoles(family); +} + +void InnerNode::loadHoleInfo(std::vector> & hole_info) const { + hole_info[decision_hole.hole] = std::make_pair(decision_hole.name,"__decision__"); + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + HoleInfo const& hole = variable_hole[variable]; + hole_info[hole.hole] = std::make_pair(hole.name,variable_name[variable]); + } + child_true->loadHoleInfo(hole_info); + child_false->loadHoleInfo(hole_info); +} + +void InnerNode::createSteps(z3::expr_vector const& substitution_variables) { + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + z3::expr const& dv = decision_hole.solver_variable; + z3::expr const& vv = variable_hole[variable].solver_variable; + steps_true.push_back( dv == (int)variable and substitution_variables[variable] <= vv); + steps_false.push_back(dv == (int)variable and substitution_variables[variable] > vv); + } +} + +void InnerNode::createPaths(z3::expr_vector const& substitution_variables) { + createSteps(substitution_variables); + child_true->createPaths(substitution_variables); + child_false->createPaths(substitution_variables); + for(bool condition: {true,false}) { + std::shared_ptr child = getChild(condition); + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + for(std::vector> const& suffix: child->paths) { + std::vector> path; + path.emplace_back(condition,variable); + path.insert(path.end(),suffix.begin(),suffix.end()); + paths.push_back(path); + } + } + } +} + +void InnerNode::loadPathExpression( + std::vector> const& path, z3::expr_vector & path_expression +) const { + STORM_LOG_THROW(path_expression.size() == depth, storm::exceptions::InvalidArgumentException, "path depth error"); + auto [step_to_true_child,step] = path[depth]; + std::shared_ptr child = getChild(step_to_true_child); + std::vector const& steps = getSteps(step_to_true_child); + // append NEGATED step condition + path_expression.push_back(not steps[step]); + child->loadPathExpression(path,path_expression); +} + +void InnerNode::addFamilyEncoding(Family const& subfamily, z3::solver& solver) const { + z3::expr_vector options(ctx); + for(uint64_t option: subfamily.holeOptions(decision_hole.hole)) { + options.push_back(decision_hole.solver_variable == (int)option); + } + solver.add(z3::mk_or(options), decision_hole.solver_string.c_str()); + std::cout << z3::mk_or(options) << std::endl; + + // variable holes + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + HoleInfo const& hole = variable_hole[variable]; + std::vector const& family_options = subfamily.holeOptions(hole.hole); + // convention: hole options in the family are ordered + int domain_min = variable_domain[variable][family_options.front()]; + int domain_max = variable_domain[variable][family_options.back()]; + z3::expr encoding = (domain_min <= hole.solver_variable) and (hole.solver_variable <= domain_max); + if(domain_min == domain_max) { + encoding = (hole.solver_variable == domain_min); + } + if(not isRoot()) { + encoding = encoding and hole.restriction; + } + solver.add(encoding, hole.solver_string.c_str()); + std::cout << encoding << std::endl; + } + child_true->addFamilyEncoding(subfamily,solver); + child_false->addFamilyEncoding(subfamily,solver); +} + +void InnerNode::loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const { + hole_options[decision_hole.hole].push_back(decision_hole.getModelValue(model)); + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + HoleInfo const& hole = variable_hole[variable]; + int64_t value = hole.getModelValue(model); + uint64_t hole_option = variableValueToHoleOption(variable,value); + hole_options[hole.hole].push_back(hole_option); + } + child_true->loadHoleAssignmentFromModel(model,hole_options); + child_false->loadHoleAssignmentFromModel(model,hole_options); +} + + +void TerminalNode::loadHoleAssignmentOfPath( + z3::solver & solver, + std::vector> const& path, + z3::expr_vector const& path_expression, + std::vector const& choice_substitution, + z3::expr_vector const& substitution_variables, + z3::expr_vector const& choice_substitution_expr, + std::vector> & hole_options +) const { + bool sat = verifyExpression(solver,path_expression.back()); + if(sat) { + hole_options[action_hole.hole].insert(choice_substitution.back()); + std::cout << action_hole.name << " = " << choice_substitution.back() << std::endl; + } +} + +void InnerNode::loadHoleAssignmentOfPath( + z3::solver & solver, + std::vector> const& path, + z3::expr_vector const& path_expression, + std::vector const& choice_substitution, + z3::expr_vector const& substitution_variables, + z3::expr_vector const& choice_substitution_expr, + std::vector> & hole_options +) const { + auto [step_to_true_child,variable] = path[depth]; + bool sat = verifyExpression(solver,path_expression[depth]); + if(sat) { + hole_options[decision_hole.hole].insert(variable); + std::cout << decision_hole.name << " = " << variable << std::endl; + int64_t value = choice_substitution[variable]; + uint64_t hole_option = variableValueToHoleOption(variable,value); + hole_options[variable_hole[variable].hole].insert(hole_option); + std::cout << variable_hole[variable].name << " = " << hole_option << std::endl; + } + getChild(step_to_true_child)->loadHoleAssignmentOfPath(solver,path,path_expression,choice_substitution,substitution_variables,choice_substitution_expr,hole_options); +} + +} \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h new file mode 100644 index 000000000..2fbb80239 --- /dev/null +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -0,0 +1,161 @@ +#pragma once + +#include "src/synthesis/quotient/Family.h" + +#include +#include +#include + +#include +#include +#include + +#include + +namespace synthesis { + +using BitVector = storm::storage::BitVector; + +class TreeNode { +public: + + class HoleInfo { + public: + uint64_t hole; + std::string name; + z3::expr solver_variable; + std::string solver_string; + z3::expr restriction; + + HoleInfo(z3::context& ctx); + int64_t getModelValue(z3::model const& model) const { + return model.eval(solver_variable).get_numeral_int64(); + } + }; + + static bool verifyExpression(z3::solver & solver, z3::expr const& expr); + + uint64_t identifier; + z3::context& ctx; + + std::shared_ptr parent; + std::shared_ptr child_true; + std::shared_ptr child_false; + + /** Depth of this node in the tree. */ + uint64_t depth; + /** Every possible path (a sequence of steps) that can be taken from this node. */ + std::vector>> paths; + + TreeNode(uint64_t identifier, z3::context& ctx); + + /** Store pointers to parent and children, if exist. */ + void createTree( + std::vector> const& tree_list, std::vector> & tree + ); + + /** Return true if this node has no parent. */ + bool isRoot() const; + /** Return true if this node has no children. */ + bool isTerminal() const; + /** Return true if this node if a true child of its parent. */ + bool isTrueChild() const; + + /** Create all holes and solver variables associated with this node. */ + virtual void createHoles(Family& family) {} + /** Collect name and type (action,decision, or variable) of each hole. */ + virtual void loadHoleInfo(std::vector> & hole_info) const {} + /** Create expressions that describe steps from this node. */ + virtual void createSteps(z3::expr_vector const& substitution_variables) {} + /** Create a list of paths from this node. */ + virtual void createPaths(z3::expr_vector const& substitution_variables) {} + /** Convert path to the path expression. */ + virtual void loadPathExpression(std::vector> const& path, z3::expr_vector & path_expression) const {} + /** Add encoding of hole option in the given family. */ + virtual void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const {} + + /** TODO */ + virtual void loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const {} + /** TODO */ + virtual void loadHoleAssignmentOfPath( + z3::solver & solver, + std::vector> const& path, z3::expr_vector const& path_expression, + std::vector const& choice_substitution, + z3::expr_vector const& substitution_variables, + z3::expr_vector const& choice_substitution_expr, + std::vector> & hole_options + ) const {} + +}; + +class TerminalNode: public TreeNode { +public: + const uint64_t num_actions; + HoleInfo action_hole; + z3::expr action_expr; + + TerminalNode(uint64_t identifier, z3::context & ctx, uint64_t num_actions); + + void createHoles(Family& family) override; + void loadHoleInfo(std::vector> & hole_info) const override; + void createSteps(z3::expr_vector const& substitution_variables) override; + void createPaths(z3::expr_vector const& substitution_variables) override; + void loadPathExpression(std::vector> const& path, z3::expr_vector & path_expression) const override; + void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; + void loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const override; + void loadHoleAssignmentOfPath( + z3::solver & solver, + std::vector> const& path, z3::expr_vector const& path_expression, + std::vector const& choice_substitution, + z3::expr_vector const& substitution_variables, + z3::expr_vector const& choice_substitution_expr, + std::vector> & hole_options + ) const override; +}; + + +class InnerNode: public TreeNode { +public: + + std::vector const& variable_name; + std::vector> const& variable_domain; + + HoleInfo decision_hole; + std::vector variable_hole; + std::vector steps_true; + std::vector steps_false; + + InnerNode( + uint64_t identifier, + z3::context & ctx, + std::vector const& variable_name, + std::vector> const& variable_domain + ); + + const uint64_t numVariables() const; + /** Convert variable value to the corresponding hole option via variable domain. */ + const uint64_t variableValueToHoleOption(uint64_t variable, int64_t value) const; + + /** Retrieve true child of this node if the condition holds, get false child otherwise. */ + std::shared_ptr getChild(bool condition) const; + std::vector const& getSteps(bool condition) const; + + void createHoles(Family& family) override; + void loadHoleInfo(std::vector> & hole_info) const override; + void createSteps(z3::expr_vector const& substitution_variables) override; + void createPaths(z3::expr_vector const& substitution_variables) override; + void loadPathExpression(std::vector> const& path, z3::expr_vector & path_expression) const override; + void addFamilyEncoding(Family const& family, z3::solver & solver) const override; + void loadHoleAssignmentFromModel(z3::model const& model, std::vector> & hole_options) const override; + void loadHoleAssignmentOfPath( + z3::solver & solver, + std::vector> const& path, z3::expr_vector const& path_expression, + std::vector const& choice_substitution, + z3::expr_vector const& substitution_variables, + z3::expr_vector const& choice_substitution_expr, + std::vector> & hole_options + ) const override; + +}; + +} \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp index b8e371ffa..3170afb16 100644 --- a/payntbind/src/synthesis/quotient/bindings.cpp +++ b/payntbind/src/synthesis/quotient/bindings.cpp @@ -4,15 +4,17 @@ #include "Family.h" #include "Coloring.h" #include "ColoringSmt.h" +#include "ColoringSmtFull.h" #include #include -#include #include #include #include +#include + namespace synthesis { template @@ -303,7 +305,6 @@ void bindings_coloring(py::module& m) { storm::storage::sparse::StateValuations const&, std::vector const&, std::vector,std::vector>>, - synthesis::Family const&, std::vector> >()) .def("selectCompatibleChoices", py::overload_cast(&synthesis::ColoringSmt::selectCompatibleChoices)) @@ -312,4 +313,21 @@ void bindings_coloring(py::module& m) { .def("areChoicesConsistent", &synthesis::ColoringSmt::areChoicesConsistent) ; + py::class_(m, "ColoringSmtFull") + .def(py::init< + std::vector const&, + std::vector const&, + storm::storage::sparse::StateValuations const&, + std::vector const&, + std::vector> const&, + std::vector> const& + >()) + // .def_property_readonly("family", &synthesis::ColoringSmtFull::getFamily) + .def("getFamilyInfo", &synthesis::ColoringSmtFull::getFamilyInfo) + .def("selectCompatibleChoices", py::overload_cast(&synthesis::ColoringSmtFull::selectCompatibleChoices)) + .def("selectCompatibleChoices", py::overload_cast(&synthesis::ColoringSmtFull::selectCompatibleChoices)) + .def("selectCompatibleChoicesTime", &synthesis::ColoringSmtFull::selectCompatibleChoicesTime) + .def("areChoicesConsistent", &synthesis::ColoringSmtFull::areChoicesConsistent) + ; + } diff --git a/payntbind/src/synthesis/translation/choiceTransformation.cpp b/payntbind/src/synthesis/translation/choiceTransformation.cpp index aa187f6e7..64442c15f 100644 --- a/payntbind/src/synthesis/translation/choiceTransformation.cpp +++ b/payntbind/src/synthesis/translation/choiceTransformation.cpp @@ -40,11 +40,57 @@ std::shared_ptr> addMissingChoiceLabelsM return storm::utility::builder::buildModelFromComponents(model.getType(),std::move(components)); } -void assertChoiceLabelingIsCanonic(storm::models::sparse::ChoiceLabeling const& choice_labeling) { - for(uint64_t choice = 0; choice < choice_labeling.getNumberOfItems(); ++choice) { - auto const& labels = choice_labeling.getLabelsOfChoice(choice); - STORM_LOG_THROW(labels.size()==1, storm::exceptions::InvalidModelException, "expected exactly 1 label for choice " << choice); +bool assertChoiceLabelingIsCanonic( + std::vector const& row_groups, + storm::models::sparse::ChoiceLabeling const& choice_labeling, + bool throw_on_fail +) { + std::set state_labels; + for(uint64_t state = 0; state < row_groups.size()-1; ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + auto const& labels = choice_labeling.getLabelsOfChoice(choice); + if(labels.size() != 1) { + if(throw_on_fail) { + STORM_LOG_THROW(labels.size() == 1, storm::exceptions::InvalidModelException, "expected exactly 1 label for choice " << choice); + } else { + return false; + } + } + std::string const& label = *(labels.begin()); + if(state_labels.find(label) != state_labels.end()) { + if(throw_on_fail) { + STORM_LOG_THROW(state_labels.find(label) == state_labels.end(), storm::exceptions::InvalidModelException, "label " << label << " is used twice for choices in state " << state); + } else { + return false; + } + } + state_labels.insert(label); + } + state_labels.clear(); + } + return true; +} + +bool isChoiceLabelingCanonic( + std::vector const& row_groups, + storm::models::sparse::ChoiceLabeling const& choice_labeling +) { + std::set state_labels; + for(uint64_t state = 0; state < row_groups.size()-1; ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + auto const& labels = choice_labeling.getLabelsOfChoice(choice); + if(labels.size() != 1) { + return false; + } + std::string const& label = *(labels.begin()); + if(state_labels.find(label) != state_labels.end()) { + return false; + } + state_labels.insert(label); + } + state_labels.clear(); } + return true; } void removeUnusedLabels(storm::models::sparse::ChoiceLabeling & choice_labeling) { @@ -75,7 +121,7 @@ std::pair,std::vector> extractActionLabels( action_labels.push_back(label); } - assertChoiceLabelingIsCanonic(choice_labeling); + assertChoiceLabelingIsCanonic(model.getTransitionMatrix().getRowGroupIndices(), choice_labeling); std::vector choice_to_action(model.getNumberOfChoices()); for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { auto const& labels = choice_labeling.getLabelsOfChoice(choice); @@ -232,7 +278,7 @@ std::shared_ptr> restoreActionsInAbsorbi if(model_canonic == NULL) { return NULL; } - assertChoiceLabelingIsCanonic(model_canonic->getChoiceLabeling()); + assertChoiceLabelingIsCanonic(model_canonic->getTransitionMatrix().getRowGroupIndices(), model_canonic->getChoiceLabeling()); storm::storage::BitVector const& no_action_label_choices = model_canonic->getChoiceLabeling().getChoices(NO_ACTION_LABEL); storm::storage::BitVector absorbing_states(model.getNumberOfStates(),true); for(uint64_t state = 0; state < model.getNumberOfStates(); ++state) { diff --git a/payntbind/src/synthesis/translation/choiceTransformation.h b/payntbind/src/synthesis/translation/choiceTransformation.h index 1d7fb64c4..23373f128 100644 --- a/payntbind/src/synthesis/translation/choiceTransformation.h +++ b/payntbind/src/synthesis/translation/choiceTransformation.h @@ -32,9 +32,16 @@ std::shared_ptr> addMissingChoiceLabelsM ); /** - * Assert that choice labeling is canonic, i.e. each choice has exactly one label. + * Assert that choice labeling is canonic, i.e. each choice has exactly one label and each has at most one choice with + * any given label. + * @param abort_on_fail if true, then an exception is thrown + * @return whether canonicity holds */ -void assertChoiceLabelingIsCanonic(storm::models::sparse::ChoiceLabeling const& choice_labeling); +bool assertChoiceLabelingIsCanonic( + std::vector const& row_groups, + storm::models::sparse::ChoiceLabeling const& choice_labeling, + bool throw_on_fail = true +); /** * Remove labels that have zero associated choices.