Final JAIR sumbission additions (#41)

* renamed tac archive to jair; added some dec-pomdp sketches * dec-pomdp sketch experiments * more dec-pomdp sketches * finishing the box pushing dec-pomdp sketch * added box pushing 1 and 2 FSC sketch * finalising dec-POMDP sketch benchmark set * dec-POMDP experiments * Finished dec-POMDP sketches for JAIR * Finalising repository for JAIR submission
randriu · May 30, 2024 · a0e12b7 · a0e12b7
1 parent 5b19bfa
commit a0e12b7
Show file tree

Hide file tree

Showing 95 changed files with 8,453 additions and 0 deletions.
diff --git a/...nthesis/case-studies/dpm-large/easy.props → ...nthesis/case-studies/dpm-large/easy.props b/...nthesis/case-studies/dpm-large/easy.props → ...nthesis/case-studies/dpm-large/easy.props
diff --git a/...nthesis/case-studies/dpm-large/lost.props → ...nthesis/case-studies/dpm-large/lost.props b/...nthesis/case-studies/dpm-large/lost.props → ...nthesis/case-studies/dpm-large/lost.props
diff --git a/...thesis/case-studies/dpm-large/power.props → ...thesis/case-studies/dpm-large/power.props b/...thesis/case-studies/dpm-large/power.props → ...thesis/case-studies/dpm-large/power.props
diff --git a/...hesis/case-studies/dpm-large/sketch.props → ...hesis/case-studies/dpm-large/sketch.props b/...hesis/case-studies/dpm-large/sketch.props → ...hesis/case-studies/dpm-large/sketch.props
diff --git a/...hesis/case-studies/dpm-large/sketch.templ → ...hesis/case-studies/dpm-large/sketch.templ b/...hesis/case-studies/dpm-large/sketch.templ → ...hesis/case-studies/dpm-large/sketch.templ
diff --git a/...udies/grid-meet-all-obs-1fsc/sketch.props → ...udies/grid-meet-all-obs-1fsc/sketch.props b/...udies/grid-meet-all-obs-1fsc/sketch.props → ...udies/grid-meet-all-obs-1fsc/sketch.props
diff --git a/...udies/grid-meet-all-obs-1fsc/sketch.templ → ...udies/grid-meet-all-obs-1fsc/sketch.templ b/...udies/grid-meet-all-obs-1fsc/sketch.templ → ...udies/grid-meet-all-obs-1fsc/sketch.templ
diff --git a/...udies/grid-meet-all-obs-2fsc/sketch.props → ...udies/grid-meet-all-obs-2fsc/sketch.props b/...udies/grid-meet-all-obs-2fsc/sketch.props → ...udies/grid-meet-all-obs-2fsc/sketch.props
diff --git a/...udies/grid-meet-all-obs-2fsc/sketch.templ → ...udies/grid-meet-all-obs-2fsc/sketch.templ b/...udies/grid-meet-all-obs-2fsc/sketch.templ → ...udies/grid-meet-all-obs-2fsc/sketch.templ
diff --git a/...udies/grid-meet-all-obs-3fsc/sketch.props → ...udies/grid-meet-all-obs-3fsc/sketch.props b/...udies/grid-meet-all-obs-3fsc/sketch.props → ...udies/grid-meet-all-obs-3fsc/sketch.props
diff --git a/...udies/grid-meet-all-obs-3fsc/sketch.templ → ...udies/grid-meet-all-obs-3fsc/sketch.templ b/...udies/grid-meet-all-obs-3fsc/sketch.templ → ...udies/grid-meet-all-obs-3fsc/sketch.templ
diff --git a/...es/grid-meet-all-obs-sl-1fsc/sketch.props → ...es/grid-meet-all-obs-sl-1fsc/sketch.props b/...es/grid-meet-all-obs-sl-1fsc/sketch.props → ...es/grid-meet-all-obs-sl-1fsc/sketch.props
diff --git a/...es/grid-meet-all-obs-sl-1fsc/sketch.templ → ...es/grid-meet-all-obs-sl-1fsc/sketch.templ b/...es/grid-meet-all-obs-sl-1fsc/sketch.templ → ...es/grid-meet-all-obs-sl-1fsc/sketch.templ
diff --git a/...es/grid-meet-all-obs-sl-2fsc/sketch.props → ...es/grid-meet-all-obs-sl-2fsc/sketch.props b/...es/grid-meet-all-obs-sl-2fsc/sketch.props → ...es/grid-meet-all-obs-sl-2fsc/sketch.props
diff --git a/...es/grid-meet-all-obs-sl-2fsc/sketch.templ → ...es/grid-meet-all-obs-sl-2fsc/sketch.templ b/...es/grid-meet-all-obs-sl-2fsc/sketch.templ → ...es/grid-meet-all-obs-sl-2fsc/sketch.templ
diff --git a/...es/grid-meet-all-obs-sl-3fsc/sketch.props → ...es/grid-meet-all-obs-sl-3fsc/sketch.props b/...es/grid-meet-all-obs-sl-3fsc/sketch.props → ...es/grid-meet-all-obs-sl-3fsc/sketch.props
diff --git a/...es/grid-meet-all-obs-sl-3fsc/sketch.templ → ...es/grid-meet-all-obs-sl-3fsc/sketch.templ b/...es/grid-meet-all-obs-sl-3fsc/sketch.templ → ...es/grid-meet-all-obs-sl-3fsc/sketch.templ
diff --git a/...se-studies/grid-meet-sl-1fsc/sketch.props → ...se-studies/grid-meet-sl-1fsc/sketch.props b/...se-studies/grid-meet-sl-1fsc/sketch.props → ...se-studies/grid-meet-sl-1fsc/sketch.props
diff --git a/...se-studies/grid-meet-sl-1fsc/sketch.templ → ...se-studies/grid-meet-sl-1fsc/sketch.templ b/...se-studies/grid-meet-sl-1fsc/sketch.templ → ...se-studies/grid-meet-sl-1fsc/sketch.templ
diff --git a/...tudies/grid-meet-sl-2fsc-res/sketch.props → ...tudies/grid-meet-sl-2fsc-res/sketch.props b/...tudies/grid-meet-sl-2fsc-res/sketch.props → ...tudies/grid-meet-sl-2fsc-res/sketch.props
diff --git a/...tudies/grid-meet-sl-2fsc-res/sketch.templ → ...tudies/grid-meet-sl-2fsc-res/sketch.templ b/...tudies/grid-meet-sl-2fsc-res/sketch.templ → ...tudies/grid-meet-sl-2fsc-res/sketch.templ
diff --git a/...se-studies/grid-meet-sl-2fsc/sketch.props → ...se-studies/grid-meet-sl-2fsc/sketch.props b/...se-studies/grid-meet-sl-2fsc/sketch.props → ...se-studies/grid-meet-sl-2fsc/sketch.props
diff --git a/...se-studies/grid-meet-sl-2fsc/sketch.templ → ...se-studies/grid-meet-sl-2fsc/sketch.templ b/...se-studies/grid-meet-sl-2fsc/sketch.templ → ...se-studies/grid-meet-sl-2fsc/sketch.templ
diff --git a/...se-studies/grid-meet-sl-3fsc/sketch.props → ...se-studies/grid-meet-sl-3fsc/sketch.props b/...se-studies/grid-meet-sl-3fsc/sketch.props → ...se-studies/grid-meet-sl-3fsc/sketch.props
diff --git a/...se-studies/grid-meet-sl-3fsc/sketch.templ → ...se-studies/grid-meet-sl-3fsc/sketch.templ b/...se-studies/grid-meet-sl-3fsc/sketch.templ → ...se-studies/grid-meet-sl-3fsc/sketch.templ
diff --git a/...hesis/case-studies/grid-meet/sketch.props → ...hesis/case-studies/grid-meet/sketch.props b/...hesis/case-studies/grid-meet/sketch.props → ...hesis/case-studies/grid-meet/sketch.props
diff --git a/...hesis/case-studies/grid-meet/sketch.templ → ...hesis/case-studies/grid-meet/sketch.templ b/...hesis/case-studies/grid-meet/sketch.templ → ...hesis/case-studies/grid-meet/sketch.templ
diff --git a/...esis/case-studies/maze-multi/sketch.props → ...esis/case-studies/maze-multi/sketch.props b/...esis/case-studies/maze-multi/sketch.props → ...esis/case-studies/maze-multi/sketch.props
diff --git a/...esis/case-studies/maze-multi/sketch.templ → ...esis/case-studies/maze-multi/sketch.templ b/...esis/case-studies/maze-multi/sketch.templ → ...esis/case-studies/maze-multi/sketch.templ
diff --git a/...synthesis/cpomdp/iff/constraint_bound.txt → ...synthesis/cpomdp/iff/constraint_bound.txt b/...synthesis/cpomdp/iff/constraint_bound.txt → ...synthesis/cpomdp/iff/constraint_bound.txt
diff --git a/...e/tac24-synthesis/cpomdp/iff/sketch.props → .../jair24-synthesis/cpomdp/iff/sketch.props b/...e/tac24-synthesis/cpomdp/iff/sketch.props → .../jair24-synthesis/cpomdp/iff/sketch.props
diff --git a/...e/tac24-synthesis/cpomdp/iff/sketch.templ → .../jair24-synthesis/cpomdp/iff/sketch.templ b/...e/tac24-synthesis/cpomdp/iff/sketch.templ → .../jair24-synthesis/cpomdp/iff/sketch.templ
diff --git a/...esis/cpomdp/milos-97/constraint_bound.txt → ...esis/cpomdp/milos-97/constraint_bound.txt b/...esis/cpomdp/milos-97/constraint_bound.txt → ...esis/cpomdp/milos-97/constraint_bound.txt
diff --git a/...24-synthesis/cpomdp/milos-97/sketch.props → ...24-synthesis/cpomdp/milos-97/sketch.props b/...24-synthesis/cpomdp/milos-97/sketch.props → ...24-synthesis/cpomdp/milos-97/sketch.props
diff --git a/...24-synthesis/cpomdp/milos-97/sketch.templ → ...24-synthesis/cpomdp/milos-97/sketch.templ b/...24-synthesis/cpomdp/milos-97/sketch.templ → ...24-synthesis/cpomdp/milos-97/sketch.templ
diff --git a/...esis/cpomdp/query-s3/constraint_bound.txt → ...esis/cpomdp/query-s3/constraint_bound.txt b/...esis/cpomdp/query-s3/constraint_bound.txt → ...esis/cpomdp/query-s3/constraint_bound.txt
diff --git a/...24-synthesis/cpomdp/query-s3/sketch.props → ...24-synthesis/cpomdp/query-s3/sketch.props b/...24-synthesis/cpomdp/query-s3/sketch.props → ...24-synthesis/cpomdp/query-s3/sketch.props
diff --git a/...24-synthesis/cpomdp/query-s3/sketch.templ → ...24-synthesis/cpomdp/query-s3/sketch.templ b/...24-synthesis/cpomdp/query-s3/sketch.templ → ...24-synthesis/cpomdp/query-s3/sketch.templ
diff --git a/...esis/cpomdp/query-s4/constraint_bound.txt → ...esis/cpomdp/query-s4/constraint_bound.txt b/...esis/cpomdp/query-s4/constraint_bound.txt → ...esis/cpomdp/query-s4/constraint_bound.txt
diff --git a/...24-synthesis/cpomdp/query-s4/sketch.props → ...24-synthesis/cpomdp/query-s4/sketch.props b/...24-synthesis/cpomdp/query-s4/sketch.props → ...24-synthesis/cpomdp/query-s4/sketch.props
diff --git a/...24-synthesis/cpomdp/query-s4/sketch.templ → ...24-synthesis/cpomdp/query-s4/sketch.templ b/...24-synthesis/cpomdp/query-s4/sketch.templ → ...24-synthesis/cpomdp/query-s4/sketch.templ
diff --git a/...is/cpomdp/tiger-grid/constraint_bound.txt → ...is/cpomdp/tiger-grid/constraint_bound.txt b/...is/cpomdp/tiger-grid/constraint_bound.txt → ...is/cpomdp/tiger-grid/constraint_bound.txt
diff --git a/...-synthesis/cpomdp/tiger-grid/sketch.props → ...-synthesis/cpomdp/tiger-grid/sketch.props b/...-synthesis/cpomdp/tiger-grid/sketch.props → ...-synthesis/cpomdp/tiger-grid/sketch.props
diff --git a/...-synthesis/cpomdp/tiger-grid/sketch.templ → ...-synthesis/cpomdp/tiger-grid/sketch.templ b/...-synthesis/cpomdp/tiger-grid/sketch.templ → ...-synthesis/cpomdp/tiger-grid/sketch.templ
diff --git a/models/archive/jair24-synthesis/dec-pomdp/box-pushing-1fsc/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/box-pushing-1fsc/sketch.props
@@ -0,0 +1,8 @@
+R{"moves"}max=? [F "goal"]
+//Pmin=? [F "goal"]
+//R{"actc"}max=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]
diff --git a/models/archive/jair24-synthesis/dec-pomdp/box-pushing-1fsc/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/box-pushing-1fsc/sketch.templ
diff --git a/models/archive/jair24-synthesis/dec-pomdp/box-pushing-2fsc/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/box-pushing-2fsc/sketch.props
@@ -0,0 +1,8 @@
+R{"moves"}max=? [F "goal"]
+//Pmin=? [F "goal"]
+//R{"actc"}max=? [F "goal"]
+
+//R{"steps"}min=? [F "goal"]
+
+
+//Pmax=? [F "goal"]
diff --git a/models/archive/jair24-synthesis/dec-pomdp/box-pushing-2fsc/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/box-pushing-2fsc/sketch.templ
diff --git a/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-2fsc/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-2fsc/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"]
diff --git a/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-2fsc/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-2fsc/sketch.templ
@@ -0,0 +1,131 @@
+
+dtmc
+
+
+const double discount=0.9;
+
+// 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};
+
+
+module strategy1
+	mem : [0..1] init 0;
+    act : [0..2] init 0;
+
+    [choose]  mem=0 & o1=0  -> (act'=P1_0_0);
+	[choose]  mem=0 & o1=1 ->  (act'=P1_0_1);
+	[choose]  mem=1 & o1=0  -> (act'=P1_1_0);
+	[choose]  mem=1 & o1=1 ->  (act'=P1_1_1);
+
+	[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;
+    act2 : [0..2] init 0;
+
+    [choose]  mem2=0 & o2=0  -> (act2'=P2_0_1);
+	[choose]  mem2=0 & o2=1  -> (act2'=P2_0_0);
+	[choose]  mem2=1 & o2=0  -> (act2'=P2_1_1);
+	[choose]  mem2=1 & o2=1  -> (act2'=P2_1_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;
+
+    [in] true -> 0.5: (pos'=0) + 0.5: (pos'=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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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"
+	!sink & c=2 & pos=0 & act=0 & act2=0 : -2;
+    !sink & c=2 & pos=1 & act=0 & act2=0 : -2;
+
+    !sink & c=2 & pos=0 & act=0 & act2=1 : -101;
+    !sink & c=2 & pos=0 & act=0 & act2=2 : 9;
+    !sink & c=2 & pos=0 & act=1 & act2=0 : -101;
+    !sink & c=2 & pos=0 & act=2 & act2=0 : 9;
+    !sink & c=2 & pos=0 & act=1 & act2=1 : -50;
+    !sink & c=2 & pos=0 & act=1 & act2=2 : -100;
+    !sink & c=2 & pos=0 & act=2 & act2=1 : -100;
+    !sink & c=2 & pos=0 & act=2 & act2=2 : 20;
+
+    !sink & c=2 & pos=1 & act=0 & act2=1 : 9;
+    !sink & c=2 & pos=1 & act=0 & act2=2 : -101;
+    !sink & c=2 & pos=1 & act=1 & act2=0 : 9;
+    !sink & c=2 & pos=1 & act=2 & act2=0 : -101;
+    !sink & c=2 & pos=1 & act=1 & act2=1 : 20;
+    !sink & c=2 & pos=1 & act=1 & act2=2 : -100;
+    !sink & c=2 & pos=1 & act=2 & act2=1 : -100;
+    !sink & c=2 & pos=1 & act=2 & act2=2 : -50;
+endrewards
+
+// target
+label "goal" = sink=true;
+
diff --git a/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-3fsc/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-3fsc/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"]
diff --git a/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-3fsc/sketch.templ b/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-3fsc/sketch.templ
@@ -0,0 +1,147 @@
+
+dtmc
+
+
+const double discount=0.9;
+
+// agent 1 holes
+hole int M1_0_0 in {0,1,2};
+hole int M1_0_1 in {0,1,2};
+hole int M1_1_0 in {0,1,2};
+hole int M1_1_1 in {0,1,2};
+hole int M1_2_0 in {0,1,2};
+hole int M1_2_1 in {0,1,2};
+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};
+hole int P1_2_0 in {0,1,2};
+hole int P1_2_1 in {0,1,2};
+
+// agent 2 holes
+hole int M2_0_1 in {0,1,2};
+hole int M2_0_0 in {0,1,2};
+hole int M2_1_1 in {0,1,2};
+hole int M2_1_0 in {0,1,2};
+hole int M2_2_1 in {0,1,2};
+hole int M2_2_0 in {0,1,2};
+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 P2_2_1 in {0,1,2};
+hole int P2_2_0 in {0,1,2};
+
+
+module strategy1
+	mem : [0..2] init 0;
+    act : [0..2] init 0;
+
+    [choose]  mem=0 & o1=0  -> (act'=P1_0_0);
+	[choose]  mem=0 & o1=1 ->  (act'=P1_0_1);
+	[choose]  mem=1 & o1=0  -> (act'=P1_1_0);
+	[choose]  mem=1 & o1=1 ->  (act'=P1_1_1);
+    [choose]  mem=2 & o1=0  -> (act'=P1_2_0);
+	[choose]  mem=2 & o1=1 ->  (act'=P1_2_1);
+
+	[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);
+    [act]  mem=2 & o1=0  -> (mem'=M1_2_0);
+	[act]  mem=2 & o1=1 ->  (mem'=M1_2_1);
+endmodule
+
+module strategy2
+	mem2 : [0..2] init 0;
+    act2 : [0..2] init 0;
+
+    [choose]  mem2=0 & o2=0  -> (act2'=P2_0_1);
+	[choose]  mem2=0 & o2=1  -> (act2'=P2_0_0);
+	[choose]  mem2=1 & o2=0  -> (act2'=P2_1_1);
+	[choose]  mem2=1 & o2=1  -> (act2'=P2_1_0);
+    [choose]  mem2=2 & o2=0  -> (act2'=P2_2_1);
+	[choose]  mem2=2 & o2=1  -> (act2'=P2_2_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);
+    [act]  mem2=2 & o2=0  -> (mem2'=M2_2_0);
+	[act]  mem2=2 & o2=1  -> (mem2'=M2_2_1);
+endmodule
+
+
+module tiger
+
+	pos : [0..1] init 0;
+    o1 : [0..1] init 0;
+    o2 : [0..1] init 0;
+
+    [in] true -> 0.5: (pos'=0) + 0.5: (pos'=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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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) + 0.125: (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"
+	!sink & c=2 & pos=0 & act=0 & act2=0 : -2;
+    !sink & c=2 & pos=1 & act=0 & act2=0 : -2;
+
+    !sink & c=2 & pos=0 & act=0 & act2=1 : -101;
+    !sink & c=2 & pos=0 & act=0 & act2=2 : 9;
+    !sink & c=2 & pos=0 & act=1 & act2=0 : -101;
+    !sink & c=2 & pos=0 & act=2 & act2=0 : 9;
+    !sink & c=2 & pos=0 & act=1 & act2=1 : -50;
+    !sink & c=2 & pos=0 & act=1 & act2=2 : -100;
+    !sink & c=2 & pos=0 & act=2 & act2=1 : -100;
+    !sink & c=2 & pos=0 & act=2 & act2=2 : 20;
+
+    !sink & c=2 & pos=1 & act=0 & act2=1 : 9;
+    !sink & c=2 & pos=1 & act=0 & act2=2 : -101;
+    !sink & c=2 & pos=1 & act=1 & act2=0 : 9;
+    !sink & c=2 & pos=1 & act=2 & act2=0 : -101;
+    !sink & c=2 & pos=1 & act=1 & act2=1 : 20;
+    !sink & c=2 & pos=1 & act=1 & act2=2 : -100;
+    !sink & c=2 & pos=1 & act=2 & act2=1 : -100;
+    !sink & c=2 & pos=1 & act=2 & act2=2 : -50;
+endrewards
+
+// target
+label "goal" = sink=true;
+
diff --git a/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-4fsc/sketch.props b/models/archive/jair24-synthesis/dec-pomdp/dec-tiger-4fsc/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"]