POSGs initial commit

models/posg/dodge-8/sketch.props

@@ -0,0 +1 @@
+P>0.9 [F "goal"]

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
+

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

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

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()