From 2adcb2c41bd696219fd93e6aaddda6113dc2ae5c Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Thu, 20 Jun 2024 15:10:18 +0200 Subject: [PATCH] added more POSG examples --- models/posg/dice-and-coin/sketch.props | 1 + models/posg/dice-and-coin/sketch.templ | 41 +++++++ models/posg/dice-and-coin2/sketch.props | 1 + models/posg/dice-and-coin2/sketch.templ | 48 ++++++++ models/posg/dodge-8/sketch.templ | 4 + .../posg/models-for-dave/dice-and-coin.prism | 50 ++++++++ .../posg/models-for-dave/dice-and-coin2.prism | 57 ++++++++++ models/posg/models-for-dave/dodge8.prism | 83 ++++++++++++++ .../posg/models-for-dave/multi-dodge4.prism | 107 ++++++++++++++++++ models/posg/multi-dodge4/sketch.props | 1 + models/posg/multi-dodge4/sketch.templ | 100 ++++++++++++++++ 11 files changed, 493 insertions(+) create mode 100755 models/posg/dice-and-coin/sketch.props create mode 100644 models/posg/dice-and-coin/sketch.templ create mode 100755 models/posg/dice-and-coin2/sketch.props create mode 100644 models/posg/dice-and-coin2/sketch.templ create mode 100644 models/posg/models-for-dave/dice-and-coin.prism create mode 100644 models/posg/models-for-dave/dice-and-coin2.prism create mode 100755 models/posg/models-for-dave/dodge8.prism create mode 100755 models/posg/models-for-dave/multi-dodge4.prism create mode 100755 models/posg/multi-dodge4/sketch.props create mode 100755 models/posg/multi-dodge4/sketch.templ diff --git a/models/posg/dice-and-coin/sketch.props b/models/posg/dice-and-coin/sketch.props new file mode 100755 index 000000000..cd5b6d078 --- /dev/null +++ b/models/posg/dice-and-coin/sketch.props @@ -0,0 +1 @@ +Pmax=? [F "goal"] \ No newline at end of file diff --git a/models/posg/dice-and-coin/sketch.templ b/models/posg/dice-and-coin/sketch.templ new file mode 100644 index 000000000..05fda93a9 --- /dev/null +++ b/models/posg/dice-and-coin/sketch.templ @@ -0,0 +1,41 @@ +// Simple game with dice and coin. In each round cashier (player2) rolls a 6-sided die, +// gambler (player1) can either roll a die and if he gets a higher value he wins or +// he can choose to toss a coin, if its heads he wins and if its tails he loses. +// There's total of TOTAL_ROUNDS rounds and gambler needs to win more than a half of them to win overall. + +pomdp + +const int TOTAL_ROUNDS=3; + +formula done = round=TOTAL_ROUNDS; +formula goal = done & (rounds_won>TOTAL_ROUNDS/2); + +label "goal" = goal; + +observable "small_value" = (value_cashier < 2); +observable "cashier_ready" = value_cashier > 0; +observable "gambler_ready" = value_gambler > 0; + +label "__player_1_state__" = value_cashier != 0 & value_gambler = 0; + +module cashier + value_cashier : [0..6] init 0; + round : [0..TOTAL_ROUNDS] init 0; + + [start] !done & value_cashier = 0 -> 1/6: (value_cashier'=1) + 1/6: (value_cashier'=2) + 1/6: (value_cashier'=3) + 1/6: (value_cashier'=4) + 1/6: (value_cashier'=5) + 1/6: (value_cashier'=6); + + [next] round < TOTAL_ROUNDS -> 1:(value_cashier'=0)&(round'=round+1); +endmodule + + +module gambler + // 1..6 for dice rolls and 7 if coin toss was good + value_gambler : [0..7] init 0; + rounds_won : [0..TOTAL_ROUNDS] init 0; + + [dice] value_cashier != 0 & value_gambler = 0 -> 1/6: (value_gambler'=1) + 1/6: (value_gambler'=2) + 1/6: (value_gambler'=3) + 1/6: (value_gambler'=4) + 1/6: (value_gambler'=5) + 1/6: (value_gambler'=6); + [coin] value_cashier != 0 & value_gambler = 0 -> 1/2: (value_gambler'=1) + 1/2:(value_gambler'=7); + + [next] value_gambler != 0 & value_gambler > value_cashier -> 1: (value_gambler'=0)&(rounds_won'=rounds_won+1); + [next] value_gambler != 0 & value_gambler <= value_cashier -> (value_gambler'=0); +endmodule \ No newline at end of file diff --git a/models/posg/dice-and-coin2/sketch.props b/models/posg/dice-and-coin2/sketch.props new file mode 100755 index 000000000..cd5b6d078 --- /dev/null +++ b/models/posg/dice-and-coin2/sketch.props @@ -0,0 +1 @@ +Pmax=? [F "goal"] \ No newline at end of file diff --git a/models/posg/dice-and-coin2/sketch.templ b/models/posg/dice-and-coin2/sketch.templ new file mode 100644 index 000000000..eae326732 --- /dev/null +++ b/models/posg/dice-and-coin2/sketch.templ @@ -0,0 +1,48 @@ +// Simple game with dice and coin. In each round cashier (player2) rolls a 6-sided die, +// gambler (player1) can either roll a die and if he gets a higher value he wins or +// he can choose to toss a coin, if its heads he wins and if its tails he loses. +// There's total of TOTAL_ROUNDS rounds and gambler needs to win more than a half of them to win overall. + +// In this version cashier can decide to roll the die again in each round before passing the turn to player1. + +pomdp + +const int TOTAL_ROUNDS=3; + +formula done = round=TOTAL_ROUNDS; +formula goal = done & (rounds_won>TOTAL_ROUNDS/2); + +label "goal" = goal; + +observable "small_value" = (value_cashier < 2); +observable "cashier_ready" = value_cashier > 0; +observable "gambler_ready" = value_gambler > 0; +observable "roll_again" = roll_again; + +label "__player_1_state__" = value_cashier != 0 & value_gambler = 0 & roll_again; + +module cashier + value_cashier : [0..6] init 0; + round : [0..TOTAL_ROUNDS] init 0; + roll_again : bool init false; + + [start] !done & !roll_again & value_cashier = 0 -> 1/6: (value_cashier'=1) + 1/6: (value_cashier'=2) + 1/6: (value_cashier'=3) + 1/6: (value_cashier'=4) + 1/6: (value_cashier'=5) + 1/6: (value_cashier'=6); + + [stay] !done & !roll_again & value_cashier > 0 -> 1: (roll_again'=true); + [again] !done & !roll_again & value_cashier > 0 -> 1/6: (value_cashier'=1)&(roll_again'=true) + 1/6: (value_cashier'=2)&(roll_again'=true) + 1/6: (value_cashier'=3)&(roll_again'=true) + 1/6: (value_cashier'=4)&(roll_again'=true) + 1/6: (value_cashier'=5)&(roll_again'=true) + 1/6: (value_cashier'=6)&(roll_again'=true); + + [next] round < TOTAL_ROUNDS -> 1:(value_cashier'=0)&(round'=round+1)&(roll_again'=false); +endmodule + + +module gambler + // 1..6 for dice rolls and 7 if coin toss was good + value_gambler : [0..7] init 0; + rounds_won : [0..TOTAL_ROUNDS] init 0; + + [dice] value_cashier != 0 & value_gambler = 0 -> 1/6: (value_gambler'=1) + 1/6: (value_gambler'=2) + 1/6: (value_gambler'=3) + 1/6: (value_gambler'=4) + 1/6: (value_gambler'=5) + 1/6: (value_gambler'=6); + [coin] value_cashier != 0 & value_gambler = 0 -> 1/2: (value_gambler'=1) + 1/2:(value_gambler'=7); + + [next] value_gambler != 0 & value_gambler > value_cashier -> 1: (value_gambler'=0)&(rounds_won'=rounds_won+1); + [next] value_gambler != 0 & value_gambler <= value_cashier -> (value_gambler'=0); +endmodule \ No newline at end of file diff --git a/models/posg/dodge-8/sketch.templ b/models/posg/dodge-8/sketch.templ index 080706d33..9beaf5b0c 100755 --- a/models/posg/dodge-8/sketch.templ +++ b/models/posg/dodge-8/sketch.templ @@ -1,3 +1,7 @@ +// NxN grid, player1 starts at (1,1) and his goal is to get to (N,N) without crashing into player2 +// player2 starts at (4,4) and wants crash into player1 +// both players have slippery movement + pomdp const int N=8; diff --git a/models/posg/models-for-dave/dice-and-coin.prism b/models/posg/models-for-dave/dice-and-coin.prism new file mode 100644 index 000000000..e982146dc --- /dev/null +++ b/models/posg/models-for-dave/dice-and-coin.prism @@ -0,0 +1,50 @@ +// Simple game with dice and coin. In each round cashier (player2) rolls a 6-sided die, +// gambler (player1) can either roll a die and if he gets a higher value he wins or +// he can choose to toss a coin, if its heads he wins and if its tails he loses. +// There's total of TOTAL_ROUNDS rounds and gambler needs to win more than a half of them to win overall. + +smg + +const int TOTAL_ROUNDS=3; + +player p1 + [dice], [coin] +endplayer + +player p2 + [start], [next] +endplayer + + +formula done = round=TOTAL_ROUNDS; +formula goal = done & (rounds_won>TOTAL_ROUNDS/2); + +label "goal" = goal; + +// DEFINING THE OBSERVATIONS +// player1 cannot observe the cashier's value exactly but only observes if it is 1 or not +observable "small_value" = (value_cashier < 2); +observable "cashier_ready" = value_cashier > 0; +observable "gambler_ready" = value_gambler > 0; + +module cashier + value_cashier : [0..6] init 0; + round : [0..TOTAL_ROUNDS] init 0; + + [start] !done & value_cashier = 0 -> 1/6: (value_cashier'=1) + 1/6: (value_cashier'=2) + 1/6: (value_cashier'=3) + 1/6: (value_cashier'=4) + 1/6: (value_cashier'=5) + 1/6: (value_cashier'=6); + + [next] round < TOTAL_ROUNDS -> 1:(value_cashier'=0)&(round'=round+1); +endmodule + + +module gambler + // 1..6 for dice rolls and 7 if coin toss was good + value_gambler : [0..7] init 0; + rounds_won : [0..TOTAL_ROUNDS] init 0; + + [dice] value_cashier != 0 & value_gambler = 0 -> 1/6: (value_gambler'=1) + 1/6: (value_gambler'=2) + 1/6: (value_gambler'=3) + 1/6: (value_gambler'=4) + 1/6: (value_gambler'=5) + 1/6: (value_gambler'=6); + [coin] value_cashier != 0 & value_gambler = 0 -> 1/2: (value_gambler'=1) + 1/2:(value_gambler'=7); + + [next] value_gambler != 0 & value_gambler > value_cashier -> 1: (value_gambler'=0)&(rounds_won'=rounds_won+1); + [next] value_gambler != 0 & value_gambler <= value_cashier -> (value_gambler'=0); +endmodule \ No newline at end of file diff --git a/models/posg/models-for-dave/dice-and-coin2.prism b/models/posg/models-for-dave/dice-and-coin2.prism new file mode 100644 index 000000000..48b1d70dd --- /dev/null +++ b/models/posg/models-for-dave/dice-and-coin2.prism @@ -0,0 +1,57 @@ +// Simple game with dice and coin. In each round cashier (player2) rolls a 6-sided die, +// gambler (player1) can either roll a die and if he gets a higher value he wins or +// he can choose to toss a coin, if its heads he wins and if its tails he loses. +// There's total of TOTAL_ROUNDS rounds and gambler needs to win more than a half of them to win overall. + +// In this version cashier can decide to roll the die again in each round before passing the turn to player1. + +smg + +const int TOTAL_ROUNDS=3; + +player p1 + [dice], [coin] +endplayer + +player p2 + [start], [next], [stay], [again] +endplayer + + +formula done = round=TOTAL_ROUNDS; +formula goal = done & (rounds_won>TOTAL_ROUNDS/2); + +label "goal" = goal; + +// DEFINING THE OBSERVATIONS +// player1 cannot observe the cashier's value exactly but only observes if it is 1 or not +observable "small_value" = (value_cashier < 2); +observable "cashier_ready" = value_cashier > 0; +observable "gambler_ready" = value_gambler > 0; +observable "roll_again" = roll_again; + +module cashier + value_cashier : [0..6] init 0; + round : [0..TOTAL_ROUNDS] init 0; + roll_again : bool init false; + + [start] !done & !roll_again & value_cashier = 0 -> 1/6: (value_cashier'=1) + 1/6: (value_cashier'=2) + 1/6: (value_cashier'=3) + 1/6: (value_cashier'=4) + 1/6: (value_cashier'=5) + 1/6: (value_cashier'=6); + + [stay] !done & !roll_again & value_cashier > 0 -> 1: (roll_again'=true); + [again] !done & !roll_again & value_cashier > 0 -> 1/6: (value_cashier'=1)&(roll_again'=true) + 1/6: (value_cashier'=2)&(roll_again'=true) + 1/6: (value_cashier'=3)&(roll_again'=true) + 1/6: (value_cashier'=4)&(roll_again'=true) + 1/6: (value_cashier'=5)&(roll_again'=true) + 1/6: (value_cashier'=6)&(roll_again'=true); + + [next] round < TOTAL_ROUNDS -> 1:(value_cashier'=0)&(round'=round+1)&(roll_again'=false); +endmodule + + +module gambler + // 1..6 for dice rolls and 7 if coin toss was good + value_gambler : [0..7] init 0; + rounds_won : [0..TOTAL_ROUNDS] init 0; + + [dice] value_cashier != 0 & roll_again & value_gambler = 0 -> 1/6: (value_gambler'=1) + 1/6: (value_gambler'=2) + 1/6: (value_gambler'=3) + 1/6: (value_gambler'=4) + 1/6: (value_gambler'=5) + 1/6: (value_gambler'=6); + [coin] value_cashier != 0 & roll_again & value_gambler = 0 -> 1/2: (value_gambler'=1) + 1/2:(value_gambler'=7); + + [next] value_gambler != 0 & value_gambler > value_cashier -> 1: (value_gambler'=0)&(rounds_won'=rounds_won+1); + [next] value_gambler != 0 & value_gambler <= value_cashier -> (value_gambler'=0); +endmodule \ No newline at end of file diff --git a/models/posg/models-for-dave/dodge8.prism b/models/posg/models-for-dave/dodge8.prism new file mode 100755 index 000000000..1f6e0cffb --- /dev/null +++ b/models/posg/models-for-dave/dodge8.prism @@ -0,0 +1,83 @@ +// NxN grid, player1 starts at (1,1) and his goal is to get to (N,N) without crashing into player2 +// player2 starts at (4,4) and wants crash into player1 +// both players have slippery movement + +smg + +const int N=8; +const int xMIN = 1; +const int yMIN = 1; +const int xMAX = N; +const int yMAX = N; + +player p1 + player1, [l1], [r1], [d1], [u1] +endplayer + +player p2 + player2, [l2], [r2], [d2], [u2] +endplayer + +// DEFINING THE OBSERVATIONS +// player1 only observes its own x coordinate +observable "x1" = x1; + +formula crash = (x1=x2 & y1=y2); +formula goal = (x1=xMAX & y1=yMAX); +formula done = goal | crash; + +// clock to make the game alternating +formula clk_next = mod(clk+1,2); +module clk + clk : [0..1] init 0; + + [l1] !done & clk=0 -> (clk'=clk_next); + [r1] !done & clk=0 -> (clk'=clk_next); + [d1] !done & clk=0 -> (clk'=clk_next); + [u1] !done & clk=0 -> (clk'=clk_next); + + [l2] !done & clk=1 -> (clk'=clk_next); + [r2] !done & clk=1 -> (clk'=clk_next); + [d2] !done & clk=1 -> (clk'=clk_next); + [u2] !done & clk=1 -> (clk'=clk_next); +endmodule + + +label "goal" = goal; + +const double slip = 0.1; + +const int x1_init = 1; +const int y1_init = 1; + +formula x1right = min(x1+1,xMAX); +formula x1left = max(x1-1,xMIN); +formula y1up = min(y1+1,yMAX); +formula y1down = max(y1-1,yMIN); + +module player1 + x1 : [xMIN..xMAX] init x1_init; + y1 : [yMIN..yMAX] init y1_init; + [l1] true -> 1-slip : (x1'=x1left) + slip : (y1'=y1down); + [r1] true -> 1-slip : (x1'=x1right) + slip : (y1'=y1up); + [d1] true -> 1-slip : (y1'=y1down) + slip : (x1'=x1right); + [u1] true -> 1-slip : (y1'=y1up) + slip : (x1'=x1left); +endmodule + +const int x2_init = 4; +const int y2_init = 4; + +formula x2right = min(x2+1,xMAX); +formula x2left = max(x2-1,xMIN); +formula y2up = min(y2+1,yMAX); +formula y2down = max(y2-1,yMIN); + +module player2 + x2 : [xMIN..xMAX] init x2_init; + y2 : [yMIN..yMAX] init y2_init; + [l2] true -> 1-slip : (x2'=x2left) + slip : (y2'=y2down); + [r2] true -> 1-slip : (x2'=x2right) + slip : (y2'=y2up); + [d2] true -> 1-slip : (y2'=y2down) + slip : (x2'=x2right); + [u2] true -> 1-slip : (y2'=y2up) + slip : (x2'=x2left); +endmodule + diff --git a/models/posg/models-for-dave/multi-dodge4.prism b/models/posg/models-for-dave/multi-dodge4.prism new file mode 100755 index 000000000..771ee9449 --- /dev/null +++ b/models/posg/models-for-dave/multi-dodge4.prism @@ -0,0 +1,107 @@ +// NxN grid, player1 starts at (1,1) and his goal is to get to (N,N) without crashing into any of player2's obstacles +// player2 starts has 3 obstacles he can move (they start at (1,N), (N,1) and (4,4)) and wants crash into player1 with at least one obstacle +// player2 has slippery movement + +smg + +const int N=4; +const int xMIN = 1; +const int yMIN = 1; +const int xMAX = N; +const int yMAX = N; + +player p1 + player1, [l1], [r1], [d1], [u1] +endplayer + +player p2 + player2, [l21], [r21], [d21], [u21], [l22], [r22], [d22], [u22], [l23], [r23], [d23], [u23] +endplayer + +// DEFINING THE OBSERVATIONS +// player1 only observes its location in the grid and coordinate x of all obstacles +observable "x1" = x1; +observable "y1" = y1; +observable "x21" = x21; +observable "x22" = x22; +observable "x23" = x23; + +formula crash = (x1=x21 & y1=y21) | (x1=x22 & y1=y22) | (x1=x23 & y1=y23); +formula goal = (x1=xMAX & y1=yMAX); +formula done = goal | crash; + +// clock to make the game alternating +formula clk_next = mod(clk+1,2); +module clk + clk : [0..1] init 0; + + [l1] !done & clk=0 -> (clk'=clk_next); + [r1] !done & clk=0 -> (clk'=clk_next); + [d1] !done & clk=0 -> (clk'=clk_next); + [u1] !done & clk=0 -> (clk'=clk_next); + + [l21] !done & clk=1 -> (clk'=clk_next); + [r21] !done & clk=1 -> (clk'=clk_next); + [d21] !done & clk=1 -> (clk'=clk_next); + [u21] !done & clk=1 -> (clk'=clk_next); + [l22] !done & clk=1 -> (clk'=clk_next); + [r22] !done & clk=1 -> (clk'=clk_next); + [d22] !done & clk=1 -> (clk'=clk_next); + [u22] !done & clk=1 -> (clk'=clk_next); + [l23] !done & clk=1 -> (clk'=clk_next); + [r23] !done & clk=1 -> (clk'=clk_next); + [d23] !done & clk=1 -> (clk'=clk_next); + [u23] !done & clk=1 -> (clk'=clk_next); +endmodule + + +label "goal" = goal; + +const double slip = 0.4; + +const int x1_init = 1; +const int y1_init = 1; + +formula x1right = min(x1+1,xMAX); +formula x1left = max(x1-1,xMIN); +formula y1up = min(y1+1,yMAX); +formula y1down = max(y1-1,yMIN); + +module player1 + x1 : [xMIN..xMAX] init x1_init; + y1 : [yMIN..yMAX] init y1_init; + [l1] true -> 1: (x1'=x1left); + [r1] true -> 1: (x1'=x1right); + [d1] true -> 1: (y1'=y1down); + [u1] true -> 1: (y1'=y1up); +endmodule + +const int x21_init = 4; +const int y21_init = 4; +const int x22_init = 1; +const int y22_init = N; +const int x23_init = N; +const int y23_init = 1; + + +module player2 + x21 : [xMIN..xMAX] init x21_init; + y21 : [yMIN..yMAX] init y21_init; + x22 : [xMIN..xMAX] init x22_init; + y22 : [yMIN..yMAX] init y22_init; + x23 : [xMIN..xMAX] init x23_init; + y23 : [yMIN..yMAX] init y23_init; + [l21] true -> 1-slip : (x21'=max(x21-1,xMIN)) + slip : (y21'=max(y21-1,yMIN)); + [r21] true -> 1-slip : (x21'=min(x21+1,xMAX)) + slip : (y21'=min(y21+1,yMAX)); + [d21] true -> 1-slip : (y21'=max(y21-1,yMIN)) + slip : (x21'=min(x21+1,xMAX)); + [u21] true -> 1-slip : (y21'=min(y21+1,yMAX)) + slip : (x21'=max(x21-1,xMIN)); + [l22] true -> 1-slip : (x22'=max(x22-1,xMIN)) + slip : (y22'=max(y22-1,yMIN)); + [r22] true -> 1-slip : (x22'=min(x22+1,xMAX)) + slip : (y22'=min(y22+1,yMAX)); + [d22] true -> 1-slip : (y22'=max(y22-1,yMIN)) + slip : (x22'=min(x22+1,xMAX)); + [u22] true -> 1-slip : (y22'=min(y22+1,yMAX)) + slip : (x22'=max(x22-1,xMIN)); + [l23] true -> 1-slip : (x23'=max(x23-1,xMIN)) + slip : (y23'=max(y23-1,yMIN)); + [r23] true -> 1-slip : (x23'=min(x23+1,xMAX)) + slip : (y23'=min(y23+1,yMAX)); + [d23] true -> 1-slip : (y23'=max(y23-1,yMIN)) + slip : (x23'=min(x23+1,xMAX)); + [u23] true -> 1-slip : (y23'=min(y23+1,yMAX)) + slip : (x23'=max(x23-1,xMIN)); +endmodule + diff --git a/models/posg/multi-dodge4/sketch.props b/models/posg/multi-dodge4/sketch.props new file mode 100755 index 000000000..923c9e7b1 --- /dev/null +++ b/models/posg/multi-dodge4/sketch.props @@ -0,0 +1 @@ +P>0.9 [F "goal"] \ No newline at end of file diff --git a/models/posg/multi-dodge4/sketch.templ b/models/posg/multi-dodge4/sketch.templ new file mode 100755 index 000000000..60fa1e104 --- /dev/null +++ b/models/posg/multi-dodge4/sketch.templ @@ -0,0 +1,100 @@ +// NxN grid, player1 starts at (1,1) and his goal is to get to (N,N) without crashing into any of player2's obstacles +// player2 starts has 3 obstacles he can move (they start at (1,N), (N,1) and (4,4)) and wants crash into player1 with at least one obstacle +// player2 has slippery movement + +pomdp + +const int N=4; +const int xMIN = 1; +const int yMIN = 1; +const int xMAX = N; +const int yMAX = N; + +// DEFINING THE OBSERVATIONS +// player1 only observes its location in the grid and coordinate x of all obstacles +observable "x1" = x1; +observable "y1" = y1; +observable "x21" = x21; +observable "x22" = x22; +observable "x23" = x23; + +formula crash = (x1=x21 & y1=y21) | (x1=x22 & y1=y22) | (x1=x23 & y1=y23); +formula goal = (x1=xMAX & y1=yMAX); +formula done = goal | crash; + +// clock to make the game alternating +formula clk_next = mod(clk+1,2); +module clk + clk : [0..1] init 0; + + [l1] !done & clk=0 -> (clk'=clk_next); + [r1] !done & clk=0 -> (clk'=clk_next); + [d1] !done & clk=0 -> (clk'=clk_next); + [u1] !done & clk=0 -> (clk'=clk_next); + + [l21] !done & clk=1 -> (clk'=clk_next); + [r21] !done & clk=1 -> (clk'=clk_next); + [d21] !done & clk=1 -> (clk'=clk_next); + [u21] !done & clk=1 -> (clk'=clk_next); + [l22] !done & clk=1 -> (clk'=clk_next); + [r22] !done & clk=1 -> (clk'=clk_next); + [d22] !done & clk=1 -> (clk'=clk_next); + [u22] !done & clk=1 -> (clk'=clk_next); + [l23] !done & clk=1 -> (clk'=clk_next); + [r23] !done & clk=1 -> (clk'=clk_next); + [d23] !done & clk=1 -> (clk'=clk_next); + [u23] !done & clk=1 -> (clk'=clk_next); +endmodule + + +label "goal" = goal; +label "__player_1_state__" = clk=0; + +const double slip = 0.4; + +const int x1_init = 1; +const int y1_init = 1; + +formula x1right = min(x1+1,xMAX); +formula x1left = max(x1-1,xMIN); +formula y1up = min(y1+1,yMAX); +formula y1down = max(y1-1,yMIN); + +module player1 + x1 : [xMIN..xMAX] init x1_init; + y1 : [yMIN..yMAX] init y1_init; + [l1] true -> 1: (x1'=x1left); + [r1] true -> 1: (x1'=x1right); + [d1] true -> 1: (y1'=y1down); + [u1] true -> 1: (y1'=y1up); +endmodule + +const int x21_init = 4; +const int y21_init = 4; +const int x22_init = 1; +const int y22_init = N; +const int x23_init = N; +const int y23_init = 1; + + +module player2 + x21 : [xMIN..xMAX] init x21_init; + y21 : [yMIN..yMAX] init y21_init; + x22 : [xMIN..xMAX] init x22_init; + y22 : [yMIN..yMAX] init y22_init; + x23 : [xMIN..xMAX] init x23_init; + y23 : [yMIN..yMAX] init y23_init; + [l21] true -> 1-slip : (x21'=max(x21-1,xMIN)) + slip : (y21'=max(y21-1,yMIN)); + [r21] true -> 1-slip : (x21'=min(x21+1,xMAX)) + slip : (y21'=min(y21+1,yMAX)); + [d21] true -> 1-slip : (y21'=max(y21-1,yMIN)) + slip : (x21'=min(x21+1,xMAX)); + [u21] true -> 1-slip : (y21'=min(y21+1,yMAX)) + slip : (x21'=max(x21-1,xMIN)); + [l22] true -> 1-slip : (x22'=max(x22-1,xMIN)) + slip : (y22'=max(y22-1,yMIN)); + [r22] true -> 1-slip : (x22'=min(x22+1,xMAX)) + slip : (y22'=min(y22+1,yMAX)); + [d22] true -> 1-slip : (y22'=max(y22-1,yMIN)) + slip : (x22'=min(x22+1,xMAX)); + [u22] true -> 1-slip : (y22'=min(y22+1,yMAX)) + slip : (x22'=max(x22-1,xMIN)); + [l23] true -> 1-slip : (x23'=max(x23-1,xMIN)) + slip : (y23'=max(y23-1,yMIN)); + [r23] true -> 1-slip : (x23'=min(x23+1,xMAX)) + slip : (y23'=min(y23+1,yMAX)); + [d23] true -> 1-slip : (y23'=max(y23-1,yMIN)) + slip : (x23'=min(x23+1,xMAX)); + [u23] true -> 1-slip : (y23'=min(y23+1,yMAX)) + slip : (x23'=max(x23-1,xMIN)); +endmodule +