From 201dcafed899e18c265dfc0fd2050dfb693b86bb Mon Sep 17 00:00:00 2001
From: Roman Andriushchenko <iandri@fit.vut.cz>
Date: Wed, 19 Jun 2024 15:05:06 +0200
Subject: [PATCH] POSGs initial commit

---
 models/posg/dodge-8/sketch.props |  1 +
 models/posg/dodge-8/sketch.templ | 70 ++++++++++++++++++++++++++++++++
 paynt/parser/sketch.py           |  3 ++
 paynt/quotient/models.py         |  1 +
 paynt/quotient/posg.py           | 27 ++++++++++++
 5 files changed, 102 insertions(+)
 create mode 100755 models/posg/dodge-8/sketch.props
 create mode 100755 models/posg/dodge-8/sketch.templ
 create mode 100644 paynt/quotient/posg.py

diff --git a/models/posg/dodge-8/sketch.props b/models/posg/dodge-8/sketch.props
new file mode 100755
index 000000000..923c9e7b1
--- /dev/null
+++ b/models/posg/dodge-8/sketch.props
@@ -0,0 +1 @@
+P>0.9 [F "goal"]
\ No newline at end of file
diff --git a/models/posg/dodge-8/sketch.templ b/models/posg/dodge-8/sketch.templ
new file mode 100755
index 000000000..080706d33
--- /dev/null
+++ b/models/posg/dodge-8/sketch.templ
@@ -0,0 +1,70 @@
+pomdp
+
+const int N=8;
+const int xMIN = 1;
+const int yMIN = 1;
+const int xMAX = N;
+const int yMAX = N;
+
+
+formula crash = (x1=x2 & y1=y2);
+formula goal = (x1=xMAX & y1=yMAX);
+formula done = goal | crash;
+
+observable "x1" = x1;
+
+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;
+label "__player_1_state__" = clk=0;
+
+
+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/paynt/parser/sketch.py b/paynt/parser/sketch.py
index 6fbb8d1b6..dd773e6e8 100644
--- a/paynt/parser/sketch.py
+++ b/paynt/parser/sketch.py
@@ -9,6 +9,7 @@
 import paynt.quotient.quotient
 import paynt.quotient.pomdp
 import paynt.quotient.decpomdp
+import paynt.quotient.posg
 import paynt.quotient.mdp_family
 import paynt.quotient.pomdp_family
 import paynt.verification.property
@@ -221,6 +222,8 @@ def build_quotient_container(cls, prism, jani_unfolder, explicit_quotient, famil
             assert explicit_quotient.is_nondeterministic_model
             if decpomdp_manager is not None and decpomdp_manager.num_agents > 1:
                 quotient_container = paynt.quotient.decpomdp.DecPomdpQuotient(decpomdp_manager, specification)
+            elif explicit_quotient.labeling.contains_label(paynt.quotient.posg.PosgQuotient.PLAYER_1_STATE_LABEL):
+                quotient_container = paynt.quotient.posg.PosgQuotient(explicit_quotient, specification)
             else:
                 quotient_container = paynt.quotient.pomdp.PomdpQuotient(explicit_quotient, specification, decpomdp_manager)
         return quotient_container
diff --git a/paynt/quotient/models.py b/paynt/quotient/models.py
index ff68fa0b1..1a6b75aa7 100644
--- a/paynt/quotient/models.py
+++ b/paynt/quotient/models.py
@@ -20,6 +20,7 @@ def initialize(cls, specification):
         cls.builder_options.set_build_state_valuations(True)
         cls.builder_options.set_add_overlapping_guards_label()
         cls.builder_options.set_build_observation_valuations(True)
+        cls.builder_options.set_build_all_labels(True)
         # cls.builder_options.set_exploration_checks(True)
 
     @classmethod
diff --git a/paynt/quotient/posg.py b/paynt/quotient/posg.py
new file mode 100644
index 000000000..367b82ba2
--- /dev/null
+++ b/paynt/quotient/posg.py
@@ -0,0 +1,27 @@
+import paynt.quotient.quotient
+import paynt.quotient.pomdp
+
+import logging
+logger = logging.getLogger(__name__)
+
+
+class PosgQuotient(paynt.quotient.quotient.Quotient):
+
+    # label associated with states of Player 1
+    PLAYER_1_STATE_LABEL = "__player_1_state__"
+
+    
+    def __init__(self, quotient_mdp, specification):
+        super().__init__(quotient_mdp = quotient_mdp, specification = specification)
+
+        # TODO Antonin
+        self.coloring = None
+        self.family = None
+        self.design_space = None
+
+        pomdp = self.quotient_mdp
+        print(type(pomdp), dir(pomdp))
+        print(dir(pomdp.labeling))
+        # print(pomdp.labeling.get_states("__player_1_state__"))
+
+        exit()