Updated POSG models to be consistent with Dave

randriu · Jul 3, 2024 · 1220251 · 1220251
1 parent b4c32b8
commit 1220251
Show file tree

Hide file tree

Showing 8 changed files with 12 additions and 0 deletions.
diff --git a/models/posg/dice-and-coin/sketch.templ b/models/posg/dice-and-coin/sketch.templ
@@ -15,6 +15,7 @@ label "goal" = goal;
 observable "small_value" = (value_cashier < 2);
 observable "cashier_ready" = value_cashier > 0;
 observable "gambler_ready" = value_gambler > 0;
+observable "game_over" = round = TOTAL_ROUNDS;
 
 label "__player_1_state__" = value_cashier != 0 & value_gambler = 0;
 

diff --git a/models/posg/dice-and-coin2/sketch.templ b/models/posg/dice-and-coin2/sketch.templ
@@ -18,6 +18,7 @@ observable "small_value" = (value_cashier < 2);
 observable "cashier_ready" = value_cashier > 0;
 observable "gambler_ready" = value_gambler > 0;
 observable "roll_again" = roll_again;
+observable "game_over" = round = TOTAL_ROUNDS;
 
 label "__player_1_state__" = value_cashier != 0 & value_gambler = 0 & roll_again;
 

diff --git a/models/posg/dodge-8/sketch.templ b/models/posg/dodge-8/sketch.templ
@@ -16,6 +16,8 @@ formula goal = (x1=xMAX & y1=yMAX);
 formula done = goal | crash;
 
 observable "x1" = x1;
+observable "clk" = clk;
+observable "done" = done;
 
 formula clk_next = mod(clk+1,2);
 module clk

diff --git a/models/posg/models-for-dave/dice-and-coin.prism b/models/posg/models-for-dave/dice-and-coin.prism
@@ -26,6 +26,7 @@ label "goal" = goal;
 observable "small_value" = (value_cashier < 2);
 observable "cashier_ready" = value_cashier > 0;
 observable "gambler_ready" = value_gambler > 0;
+observable "game_over" = round = TOTAL_ROUNDS;
 
 module cashier
     value_cashier : [0..6] init 0;

diff --git a/models/posg/models-for-dave/dice-and-coin2.prism b/models/posg/models-for-dave/dice-and-coin2.prism
@@ -29,6 +29,7 @@ observable "small_value" = (value_cashier < 2);
 observable "cashier_ready" = value_cashier > 0;
 observable "gambler_ready" = value_gambler > 0;
 observable "roll_again" = roll_again;
+observable "game_over" = round = TOTAL_ROUNDS;
 
 module cashier
     value_cashier : [0..6] init 0;

diff --git a/models/posg/models-for-dave/dodge8.prism b/models/posg/models-for-dave/dodge8.prism
@@ -21,6 +21,8 @@ endplayer
 // DEFINING THE OBSERVATIONS
 // player1 only observes its own x coordinate
 observable "x1" = x1;
+observable "clk" = clk;
+observable "done" = done;
 
 formula crash = (x1=x2 & y1=y2);
 formula goal = (x1=xMAX & y1=yMAX);

diff --git a/models/posg/models-for-dave/multi-dodge4.prism b/models/posg/models-for-dave/multi-dodge4.prism
@@ -25,6 +25,8 @@ observable "y1" = y1;
 observable "x21" = x21;
 observable "x22" = x22;
 observable "x23" = x23;
+observable "clk" = clk;
+observable "done" = done;
 
 formula crash = (x1=x21 & y1=y21) | (x1=x22 & y1=y22) | (x1=x23 & y1=y23);
 formula goal = (x1=xMAX & y1=yMAX);

diff --git a/models/posg/multi-dodge4/sketch.templ b/models/posg/multi-dodge4/sketch.templ
@@ -17,6 +17,8 @@ observable "y1" = y1;
 observable "x21" = x21;
 observable "x22" = x22;
 observable "x23" = x23;
+observable "clk" = clk;
+observable "done" = done;
 
 formula crash = (x1=x21 & y1=y21) | (x1=x22 & y1=y22) | (x1=x23 & y1=y23);
 formula goal = (x1=xMAX & y1=yMAX);