added more POSG examples

models/posg/dice-and-coin/sketch.props

@@ -0,0 +1 @@
+Pmax=? [F "goal"]

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

models/posg/dice-and-coin2/sketch.props

@@ -0,0 +1 @@
+Pmax=? [F "goal"]

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

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;

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

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

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
+