From 1220251ad7e47886a28ed12c40eb0d048cec9dbc Mon Sep 17 00:00:00 2001
From: Filip Macak <filip.macak1999@gmail.com>
Date: Wed, 3 Jul 2024 13:32:41 +0200
Subject: [PATCH] Updated POSG models to be consistent with Dave

---
 models/posg/dice-and-coin/sketch.templ           | 1 +
 models/posg/dice-and-coin2/sketch.templ          | 1 +
 models/posg/dodge-8/sketch.templ                 | 2 ++
 models/posg/models-for-dave/dice-and-coin.prism  | 1 +
 models/posg/models-for-dave/dice-and-coin2.prism | 1 +
 models/posg/models-for-dave/dodge8.prism         | 2 ++
 models/posg/models-for-dave/multi-dodge4.prism   | 2 ++
 models/posg/multi-dodge4/sketch.templ            | 2 ++
 8 files changed, 12 insertions(+)

diff --git a/models/posg/dice-and-coin/sketch.templ b/models/posg/dice-and-coin/sketch.templ
index 05fda93a9..3bc73bf50 100644
--- 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
index eae326732..eae5c8412 100644
--- 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
index 9beaf5b0c..cbc0d0da5 100755
--- 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
index e982146dc..178916efd 100644
--- 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
index 48b1d70dd..045f89a16 100644
--- 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
index 1f6e0cffb..fd0e82d3c 100755
--- 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
index 771ee9449..8a9357da7 100755
--- 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
index 60fa1e104..13c7ce6f3 100755
--- 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);