renamed tac archive to jair; added some dec-pomdp sketches

models/archive/jair24-synthesis/dec-pomdp/dec-tiger/sketch.props

@@ -0,0 +1,8 @@
+R[exp]{"rew"}max=? [C{0.9}]
+
+//R{"rew"}max=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]

models/archive/jair24-synthesis/dec-pomdp/dec-tiger/sketch.templ

@@ -0,0 +1,144 @@
+
+dtmc
+
+
+const double discount=1;
+
+// agent 1 holes
+hole int M1_0_0 in {0,1};
+hole int M1_0_1 in {0,1};
+hole int M1_1_0 in {0,1};
+hole int M1_1_1 in {0,1};
+hole int P1_0_0 in {0,1,2};
+hole int P1_0_1 in {0,1,2};
+hole int P1_1_0 in {0,1,2};
+hole int P1_1_1 in {0,1,2};
+
+// agent 2 holes
+hole int M2_0_1 in {0,1};
+hole int M2_0_0 in {0,1};
+hole int M2_1_1 in {0,1};
+hole int M2_1_0 in {0,1};
+hole int P2_0_1 in {0,1,2};
+hole int P2_0_0 in {0,1,2};
+hole int P2_1_1 in {0,1,2};
+hole int P2_1_0 in {0,1,2};
+
+hole int INIT_A1 in {0,1,2};
+hole int INIT_A2 in {0,1,2};
+
+module strategy1
+	mem : [0..1] init 0;
+
+	[act]  mem=0 & o1=0  -> (mem'=M1_0_0);
+	[act]  mem=0 & o1=1 -> (mem'=M1_0_1);
+	[act]  mem=1 & o1=0  -> (mem'=M1_1_0);
+	[act]  mem=1 & o1=1 -> (mem'=M1_1_1);
+endmodule
+
+module strategy2
+	mem2 : [0..1] init 0;
+
+	[act]  mem2=0 & o2=0  -> (mem2'=M2_0_0);
+	[act]  mem2=0 & o2=1  -> (mem2'=M2_0_1);
+	[act]  mem2=1 & o2=0  -> (mem2'=M2_1_0);
+	[act]  mem2=1 & o2=1  -> (mem2'=M2_1_1);
+endmodule
+
+
+module tiger
+
+	pos : [0..1] init 0;
+    o1 : [0..1] init 0;
+    o2 : [0..1] init 0;
+    act : [0..2] init 0;
+    act2 : [0..2] init 0;
+
+    [in] true -> 0.5: (pos'=0)&(act'=INIT_A1)&(act2'=INIT_A2) + 0.5: (pos'=1)&(act'=INIT_A1)&(act2'=INIT_A2);
+
+    [choose] o1=0 & o2=0 & mem=0 & mem2=0 -> 1: (act'=P1_0_0)&(act2'=P2_0_0);
+    [choose] o1=0 & o2=0 & mem=1 & mem2=0 -> 1: (act'=P1_1_0)&(act2'=P2_0_0);
+    [choose] o1=0 & o2=0 & mem=0 & mem2=1 -> 1: (act'=P1_0_0)&(act2'=P2_1_0);
+    [choose] o1=0 & o2=0 & mem=1 & mem2=1 -> 1: (act'=P1_1_0)&(act2'=P2_1_0);
+
+    [choose] o1=1 & o2=0 & mem=0 & mem2=0 -> 1: (act'=P1_0_1)&(act2'=P2_0_0);
+    [choose] o1=1 & o2=0 & mem=1 & mem2=0 -> 1: (act'=P1_1_1)&(act2'=P2_0_0);
+    [choose] o1=1 & o2=0 & mem=0 & mem2=1 -> 1: (act'=P1_0_1)&(act2'=P2_1_0);
+    [choose] o1=1 & o2=0 & mem=1 & mem2=1 -> 1: (act'=P1_1_1)&(act2'=P2_1_0);
+
+    [choose] o1=0 & o2=1 & mem=0 & mem2=0 -> 1: (act'=P1_0_0)&(act2'=P2_0_1);
+    [choose] o1=0 & o2=1 & mem=1 & mem2=0 -> 1: (act'=P1_1_0)&(act2'=P2_0_1);
+    [choose] o1=0 & o2=1 & mem=0 & mem2=1 -> 1: (act'=P1_0_0)&(act2'=P2_1_1);
+    [choose] o1=0 & o2=1 & mem=1 & mem2=1 -> 1: (act'=P1_1_0)&(act2'=P2_1_1);
+
+    [choose] o1=1 & o2=1 & mem=0 & mem2=0 -> 1: (act'=P1_0_1)&(act2'=P2_0_1);
+    [choose] o1=1 & o2=1 & mem=1 & mem2=0 -> 1: (act'=P1_1_1)&(act2'=P2_0_1);
+    [choose] o1=1 & o2=1 & mem=0 & mem2=1 -> 1: (act'=P1_0_1)&(act2'=P2_1_1);
+    [choose] o1=1 & o2=1 & mem=1 & mem2=1 -> 1: (act'=P1_1_1)&(act2'=P2_1_1);
+
+
+	[act] pos=0 & act=0 & act2=0 -> 0.7225: (o1'=0)&(o2'=0) + 0.1275: (o1'=0)&(o2'=1) + 0.1275: (o1'=1)&(o2'=0) + 0.0225: (o1'=1)&(o2'=1);
+    [act] pos=1 & act=0 & act2=0 -> 0.7225: (o1'=1)&(o2'=1) + 0.1275: (o1'=0)&(o2'=1) + 0.1275: (o1'=1)&(o2'=0) + 0.0225: (o1'=0)&(o2'=0);
+
+    //[act] act!=0 | act2!=0 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+
+    [act] pos=0 & act=0 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=0 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=1 & act2=0 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=2 & act2=0 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=1 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=1 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=2 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=0 & act=2 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+
+    [act] pos=1 & act=0 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=0 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=1 & act2=0 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=2 & act2=0 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=1 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=1 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=2 & act2=1 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+    [act] pos=1 & act=2 & act2=2 -> 0.125: (pos'=0)&(o1'=0)&(o2'=0) + 0.125: (pos'=0)&(o1'=0)&(o2'=1) + 0.125: (pos'=0)&(o1'=1)&(o2'=0) + 0.125: (pos'=0)&(o1'=1)&(o2'=1) + (pos'=1)&(o1'=0)&(o2'=0) + 0.125: (pos'=1)&(o1'=0)&(o2'=1) + 0.125: (pos'=1)&(o1'=1)&(o2'=0) + 0.125: (pos'=1)&(o1'=1)&(o2'=1);
+
+endmodule
+
+
+module df
+    sink : bool init false;
+    [act] !sink -> discount: true + 1-discount: (sink'=true);
+endmodule
+
+module clk
+    c : [0..2] init 0;
+    [in] c=0 -> 1: (c'=2);
+    [choose] c=1 -> 1: (c'=2);
+    [act] c=2 -> 1: (c'=1);
+endmodule
+
+// reward
+rewards "rew"
+	c=2 & pos=0 & act=0 & act2=0 : -2;
+    c=2 & pos=1 & act=0 & act2=0 : -2;
+
+    c=2 & pos=0 & act=0 & act2=1 : -101;
+    c=2 & pos=0 & act=0 & act2=2 : 9;
+    c=2 & pos=0 & act=1 & act2=0 : -101;
+    c=2 & pos=0 & act=2 & act2=0 : 9;
+    c=2 & pos=0 & act=1 & act2=1 : -50;
+    c=2 & pos=0 & act=1 & act2=2 : -100;
+    c=2 & pos=0 & act=2 & act2=1 : -100;
+    c=2 & pos=0 & act=2 & act2=2 : 20;
+
+    c=2 & pos=1 & act=0 & act2=1 : 9;
+    c=2 & pos=1 & act=0 & act2=2 : -101;
+    c=2 & pos=1 & act=1 & act2=0 : 9;
+    c=2 & pos=1 & act=2 & act2=0 : -101;
+    c=2 & pos=1 & act=1 & act2=1 : 20;
+    c=2 & pos=1 & act=1 & act2=2 : -100;
+    c=2 & pos=1 & act=2 & act2=1 : -100;
+    c=2 & pos=1 & act=2 & act2=2 : -50;
+endrewards
+
+// target
+label "goal" = sink=true;
+

models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.props

@@ -0,0 +1,6 @@
+R{"moves"}max=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]

models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-2fsc-discount/sketch.templ

@@ -0,0 +1,155 @@
+
+dtmc
+
+// 7 | x x x x x x x x
+// 6 | x x x          
+// 5 | x x A   x x x x
+// 4 | x x x   x x x x
+// 3 | x x x   x   x x
+// 2 | x x x x x   A x
+// 1 |     x x x   x x
+// 0 |     x x x   x x
+// y _________________
+//   x 0 1 2 3 4 5 6 7
+
+
+// agent1 can go in this direction
+formula u1 = ya1<7 & !(xa1=3 & ya1=2) & !(ya1=5 & xa1>3);
+formula r1 = xa1<7 & !(xa1=4 & ya1<4) & !(xa1=2 & (ya1>2 & ya1<7));
+formula d1 = ya1>0 & !(ya1=2 & xa1<2) & !(ya1=7 & xa1>2) & !(ya1=4 & xa1=5);
+formula l1 = xa1>0 & !(xa1=2 & ya1<2) & !(xa1=6 & ya1<4) & !(xa1=4 & (ya1>2 & ya1<6));
+
+// updates of coordinates (if possible)
+formula y1u = u1 ? (ya1+1) : ya1;
+formula x1r = r1 ? (xa1+1) : xa1;
+formula y1d = d1 ? (ya1-1) : ya1;
+formula x1l = l1 ? (xa1-1) : xa1;
+
+
+// agent2 can go in this direction
+formula u2 = ya2<7 & !(xa2=3 & ya2=2) & !(ya2=5 & xa2>3);
+formula r2 = xa2<7 & !(xa2=4 & ya2<4) & !(xa2=2 & (ya2>2 & ya2<7));
+formula d2 = ya2>0 & !(ya2=2 & xa2<2) & !(ya2=7 & xa2>2) & !(ya2=4 & xa2=5);
+formula l2 = xa2>0 & !(xa2=2 & ya2<2) & !(xa2=6 & ya2<4) & !(xa2=4 & (ya2>2 & ya2<6));
+
+// updates of coordinates (if possible)
+formula y2u = u2 ? (ya2+1) : ya2;
+formula x2r = r2 ? (xa2+1) : xa2;
+formula y2d = d2 ? (ya2-1) : ya2;
+formula x2l = l2 ? (xa2-1) : xa2;
+
+
+const double sl=0.1;
+
+// agent 1 holes
+hole int M1_0_1 in {0,1};
+hole int M1_0_0 in {0,1};
+hole int M1_1_1 in {0,1};
+hole int M1_1_0 in {0,1};
+hole int P1_0_1 in {1,2,3,4};
+hole int P1_0_0 in {1,2,3,4};
+hole int P1_1_1 in {1,2,3,4};
+hole int P1_1_0 in {1,2,3,4};
+
+// agent 2 holes
+hole int M2_0_1 in {0,1};
+hole int M2_0_0 in {0,1};
+hole int M2_1_1 in {0,1};
+hole int M2_1_0 in {0,1};
+hole int P2_0_1 in {1,2,3,4};
+hole int P2_0_0 in {1,2,3,4};
+hole int P2_1_1 in {1,2,3,4};
+hole int P2_1_0 in {1,2,3,4};
+
+module strategy1
+	mem : [0..1] init 0;
+
+	[move]  mem=0 & r1  -> (mem'=M1_0_1);
+	[move]  mem=0 & !r1 -> (mem'=M1_0_0);
+	[move]  mem=1 & r1  -> (mem'=M1_1_1);
+	[move]  mem=1 & !r1 -> (mem'=M1_1_0);
+endmodule
+
+module grid1
+
+	xa1 : [0..7] init 2; // agent1 x coordinate
+	ya1 : [0..7] init 5; // agent1 y coordinate
+
+
+	[move]   mem=0 & r1 &  P1_0_1=1 -> 1-sl: (ya1'=y1u) + sl: true;
+    [move]   mem=0 & r1 &  P1_0_1=2 -> 1-sl: (xa1'=x1r) + sl: true;
+    [move]   mem=0 & r1 &  P1_0_1=3 -> 1-sl: (ya1'=y1d) + sl: true;
+    [move]   mem=0 & r1 &  P1_0_1=4 -> 1-sl: (xa1'=x1l) + sl: true;
+
+	[move]   mem=0 & !r1 & P1_0_0=1 -> 1-sl: (ya1'=y1u) + sl: true;
+    [move]   mem=0 & !r1 & P1_0_0=2 -> 1-sl: (xa1'=x1r) + sl: true;
+    [move]   mem=0 & !r1 & P1_0_0=3 -> 1-sl: (ya1'=y1d) + sl: true;
+    [move]   mem=0 & !r1 & P1_0_0=4 -> 1-sl: (xa1'=x1l) + sl: true;
+
+	[move]   mem=1 & r1 &  P1_1_1=1 -> 1-sl: (ya1'=y1u) + sl: true;
+    [move]   mem=1 & r1 &  P1_1_1=2 -> 1-sl: (xa1'=x1r) + sl: true;
+    [move]   mem=1 & r1 &  P1_1_1=3 -> 1-sl: (ya1'=y1d) + sl: true;
+    [move]   mem=1 & r1 &  P1_1_1=4 -> 1-sl: (xa1'=x1l) + sl: true;
+
+	[move]   mem=1 & !r1 & P1_1_0=1 -> 1-sl: (ya1'=y1u) + sl: true;
+    [move]   mem=1 & !r1 & P1_1_0=2 -> 1-sl: (xa1'=x1r) + sl: true;
+    [move]   mem=1 & !r1 & P1_1_0=3 -> 1-sl: (ya1'=y1d) + sl: true;
+    [move]   mem=1 & !r1 & P1_1_0=4 -> 1-sl: (xa1'=x1l) + sl: true;
+
+endmodule
+
+
+module strategy2
+	mem2 : [0..1] init 0;
+
+	[move]  mem2=0 & l2  -> (mem2'=M2_0_1);
+	[move]  mem2=0 & !l2 -> (mem2'=M2_0_0);
+	[move]  mem2=1 & l2  -> (mem2'=M2_1_1);
+	[move]  mem2=1 & !l2 -> (mem2'=M2_1_0);
+endmodule
+
+
+module grid2
+
+	xa2 : [0..7] init 6; // agent2 x coordinate
+	ya2 : [0..7] init 2; // agent2 y coordinate
+
+	[move]   mem2=0 & l2 &  P2_0_1=1 -> 1-sl: (ya2'=y2u) + sl: true;
+    [move]   mem2=0 & l2 &  P2_0_1=2 -> 1-sl: (xa2'=x2r) + sl: true;
+    [move]   mem2=0 & l2 &  P2_0_1=3 -> 1-sl: (ya2'=y2d) + sl: true;
+    [move]   mem2=0 & l2 &  P2_0_1=4 -> 1-sl: (xa2'=x2l) + sl: true;
+
+	[move]   mem2=0 & !l2 & P2_0_0=1 -> 1-sl: (ya2'=y2u) + sl: true;
+    [move]   mem2=0 & !l2 & P2_0_0=2 -> 1-sl: (xa2'=x2r) + sl: true;
+    [move]   mem2=0 & !l2 & P2_0_0=3 -> 1-sl: (ya2'=y2d) + sl: true;
+    [move]   mem2=0 & !l2 & P2_0_0=4 -> 1-sl: (xa2'=x2l) + sl: true;
+
+	[move]   mem2=1 & l2 &  P2_1_1=1 -> 1-sl: (ya2'=y2u) + sl: true;
+    [move]   mem2=1 & l2 &  P2_1_1=2 -> 1-sl: (xa2'=x2r) + sl: true;
+    [move]   mem2=1 & l2 &  P2_1_1=3 -> 1-sl: (ya2'=y2d) + sl: true;
+    [move]   mem2=1 & l2 &  P2_1_1=4 -> 1-sl: (xa2'=x2l) + sl: true;
+
+	[move]   mem2=1 & !l2 & P2_1_0=1 -> 1-sl: (ya2'=y2u) + sl: true;
+    [move]   mem2=1 & !l2 & P2_1_0=2 -> 1-sl: (xa2'=x2r) + sl: true;
+    [move]   mem2=1 & !l2 & P2_1_0=3 -> 1-sl: (ya2'=y2d) + sl: true;
+    [move]   mem2=1 & !l2 & P2_1_0=4 -> 1-sl: (xa2'=x2l) + sl: true;
+endmodule
+
+const double discount = 0.99;
+
+module df
+    sink : bool init false;
+    [move] !sink & !meet -> discount: true + 1-discount: (sink'=true);
+    [move] !sink & meet ->  1: (sink'=true);
+endmodule
+
+// reward
+rewards "moves"
+	!sink: -1;
+endrewards
+
+formula meet = (xa1=xa2) & (ya1=ya2);
+
+// target
+label "goal" = sink=true;
+

models/archive/jair24-synthesis/dec-pomdp/grid-meet-sl-3fsc-discount/sketch.props

@@ -0,0 +1,6 @@
+R{"moves"}max=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]