Merge branch 'randriu:master' into belief-exploration

.github/workflows/buildtest.yml

@@ -33,8 +33,6 @@ jobs:
         uses: actions/checkout@v4
       - name: Build paynt image from Dockerfile
         run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS}
-      - name: Build paynt image with learner dependencies
-        run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }}
       - name: Login into docker
         # Only login if using master on original repo (and not for pull requests or forks)
         if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
@@ -43,7 +41,27 @@ jobs:
         # Only deploy if using master on original repo (and not for pull requests or forks)
         if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
         run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }}
-      - name: Deploy paynt image with learner dependencies
-        # Only deploy if using master on original repo (and not for pull requests or forks)
-        if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
-        run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }}
+
+  # deploy-learning:
+  #   name: Deploy on latest with learning dependencies (${{ matrix.buildType.name }})
+  #   runs-on: ubuntu-latestx
+  #   strategy:
+  #     matrix:
+  #       buildType:
+  #         - {name: "Release", imageName : "randriu/paynt", dockerTag: "latest", setupArgs: ""}
+  #     fail-fast: false
+  #   steps:
+  #     - name: Git clone
+  #       uses: actions/checkout@v4
+  #     - name: Build paynt image from Dockerfile
+  #       run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS}
+  #     - name: Build paynt image with learner dependencies
+  #       run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }}
+  #     - name: Login into docker
+  #       # Only login if using master on original repo (and not for pull requests or forks)
+  #       if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
+  #       run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin
+  #     - name: Deploy paynt image with learner dependencies
+  #       # Only deploy if using master on original repo (and not for pull requests or forks)
+  #       if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master'
+  #       run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }}

Dockerfile

@@ -22,5 +22,3 @@ WORKDIR /opt/paynt
 
 # (optional) install paynt
 RUN pip install -e .
-
-# TODO tests

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"]

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"]

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

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

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;
+

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

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