LKlinke · dominikgeissler · Jan 2, 2025 · Jan 11, 2025 · Jan 15, 2025 · Jan 15, 2025
diff --git a/benchmark_comparison.py b/benchmark_comparison.py
diff --git a/pgfexamples/README.md b/pgfexamples/README.md
@@ -7,17 +7,47 @@ pgfexamples/
 ├── comparison                      # Comparisons with other tools / paradigms
 │   ├── ADDcomparison               # Comparisons with Algebraic Decision Diagrams
 │   └── psicomparison               # Comparisons with Psi
-│       ├── inference               
+│       ├── inference
 │       └── psi_fails               # Examples where Psi fails 
-├── evt_invariants                  # Synthesis of expected visiting time invariants
-├── independence                    # Independent variables
+├── equivalence                     # Equivalence of two programs
+│   ├── loop_free                   # Programs without loops and their counterparts
+│   └── loopy                       # Programs with loops
+│       └── invariants              # ... and their loop-free counterpart
+├── independence                    # Checks for independent variables
 ├── inference                       # Calculation of posterior distribution
 │   ├── loop_free                   # ... without while-loops
 │   │   └── conditioning            # ... with observe-statements
 │   └── loopy                       # ... with while-loops
 │       └── conditioning            # ... with observe-statements 
-├── loop_equivalence                # Equality of loopy and loop-free programs
-│   └── invariants                  # Corresponding loop-free programs
+├── invariant_synthesis             # Synthesis of (expected visiting time) invariants
 └── template_parameter_synthesis    # Equality of loopy and loop-free programs with parameters
-    └── invariants                  # Corresponding loop-free programs
- ```
+    └── invariants                  # Corresponding loop-free programs
+```
+
+## File structure
+
+* Files have a comment in the first line indicating which arguments should be used in order to execute it
+
+> ```bash
+>python prodigy/cli.py METHOD FILE ARGS 
+>```
+> results in
+>```
+># METHOD FILE ARGS
+>```
+> in the first line of the corresponding program or just
+> ```
+> # skip
+> ```
+> if the file should not be automatically tested.
+
+* Naming convention:
+    * In `pgfexamples/equivalence/loop_free` the files are named `file_name.pgcl` for the first and
+      `file_name2.pgcl` for the second program
+    * In `pgfexamples/equivalence/loopy` and `pgfexamples/template_parameter_synthesis` the files are named
+      `file_name.pgcl` in the main folder and their corresponding invariants with `file_name_invariant.pgcl` in the
+      invariants folder
+    * If there are multiple invariant files for one program, e.g. for a nested loop, the invariants are to be marked
+      with numbers indicating the order they should be used (i.e. the invariant for the outer-most while loop has number
+      1 and so on)
+    * Invariants and second programs are to be marked with `skip`
diff --git a/pgfexamples/equivalence/loop_free/bernoulli.pgcl b/pgfexamples/equivalence/loop_free/bernoulli.pgcl
@@ -0,0 +1,4 @@
+# check_equality pgfexamples/equivalence/loop_free/bernoulli.pgcl pgfexamples/equivalence/loop_free/bernoulli2.pgcl
+nat x;
+
+{ x := 0 } [1/3] { x := 1 }
diff --git a/pgfexamples/equivalence/loop_free/bernoulli2.pgcl b/pgfexamples/equivalence/loop_free/bernoulli2.pgcl
@@ -0,0 +1,4 @@
+# skip
+nat x;
+
+x := bernoulli(2/3);
diff --git a/pgfexamples/equivalence/loop_free/dice_sampling.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loop_free/dice_sampling.pgcl pgfexamples/equivalence/loop_free/dice_sampling2.pgcl
+nat dice;
+nat tmp;
+
+tmp := 0;
+
+# Roll a dice
+dice := unif(1,6);
+
diff --git a/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl
@@ -0,0 +1,11 @@
+# skip
+nat dice;
+nat tmp;
+
+# Roll a three-sided dice
+tmp := unif(1,3);
+
+# Flip a coin, leave or increase by 3
+{ dice := tmp; } [1/2] { dice := tmp + 3; }
+
+tmp := 0;
diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl
@@ -0,0 +1,4 @@
+# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl
+nat x
+
+x := unif(1,6)
diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl
@@ -0,0 +1,12 @@
+# skip
+nat x
+
+{x:=1}[1/6]{
+    {x:=2}[1/5]{
+        {x:=3}[1/4]{
+            {x:=4}[1/3]{
+                {x:=5}[1/2]{x:=6}
+            }
+        }
+    }
+}
diff --git a/pgfexamples/equivalence/loopy/17_die_even.pgcl b/pgfexamples/equivalence/loopy/17_die_even.pgcl
@@ -0,0 +1,11 @@
+# check_equality pgfexamples/equivalence/loopy/17_die_even.pgcl pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl
+nat c
+nat x
+nat temp
+
+while (x < 6) {
+    x := unif(1,6)
+    c := c + 1
+    observe(x % 2 = 0)
+    temp := 0
+}
diff --git a/...op_equivalence/bit_flip_conditioning.pgcl → ...ivalence/loopy/bit_flip_conditioning.pgcl b/...op_equivalence/bit_flip_conditioning.pgcl → ...ivalence/loopy/bit_flip_conditioning.pgcl
@@ -1,11 +1,12 @@
+# check_equality pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl
 bool b1
 bool b2
 bool b3
 bool b4
 nat i
 nat temp
 
-while (not ((b1 = 0) & (b2 = 0))) {
+while (b1=1 || b2=1) {
     b1 := bernoulli(1/2)
     b2 := bernoulli(1/2)
     observe( (b1 = 0 & b3 = 0) || (b1 = 1 & b3 = 1) || (b2 = 0 & b4 = 0) || (b2 = 1 & b4 = 1) )

diff --git a/pgfexamples/loop_equivalence/condand.pgcl → pgfexamples/equivalence/loopy/condand.pgcl b/pgfexamples/loop_equivalence/condand.pgcl → pgfexamples/equivalence/loopy/condand.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 

diff --git a/pgfexamples/equivalence/loopy/dep_bern.pgcl b/pgfexamples/equivalence/loopy/dep_bern.pgcl
@@ -0,0 +1,12 @@
+# check_equality pgfexamples/equivalence/loopy/dep_bern.pgcl pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl
+nat c;
+nat m;
+nat n;
+nat tmp;
+
+
+while( c > 0 ){
+    {m := m+1} [1/2] {n:= n+1}
+    c := c-1
+    tmp := 0
+}
diff --git a/pgfexamples/equivalence/loopy/endless_conditioning.pgcl b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl
@@ -0,0 +1,7 @@
+# check_equality pgfexamples/equivalence/loopy/endless_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl
+nat x;
+
+while(x=1){
+{x := 0}[1/2]{x:=1}
+observe(x=1)
+}
diff --git a/pgfexamples/equivalence/loopy/geometric.pgcl b/pgfexamples/equivalence/loopy/geometric.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/geometric.pgcl pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl
+nat x;
+nat c;
+nat temp;
+
+while (x = 1){
+ {x := 0 } [1/2] {c := c+1}
+ temp :=0
+}
diff --git a/pgfexamples/equivalence/loopy/geometric_observe.pgcl b/pgfexamples/equivalence/loopy/geometric_observe.pgcl
@@ -0,0 +1,11 @@
+# check_equality pgfexamples/equivalence/loopy/geometric_observe.pgcl pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl
+nat y;
+nat x;
+nat tmp;
+
+while ( y = 1){
+    {y := 0}[1/2]{y := 1};
+    x := x + 1;
+    observe( x < 3)
+    tmp := 0;
+}
diff --git a/pgfexamples/equivalence/loopy/geometric_shifted.pgcl b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl
@@ -0,0 +1,10 @@
+# check_equality pgfexamples/equivalence/loopy/geometric_shifted.pgcl pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl
+nat x;
+nat c;
+nat temp;
+rparam p;
+
+while (x > 0){
+ {x := 0; c := c + 3 } [1/2] {c := c+1}
+ temp := 0
+}
diff --git a/...nce/invariants/17_die_even_invariant.pgcl → ...opy/invariants/17_die_even_invariant.pgcl b/...nce/invariants/17_die_even_invariant.pgcl → ...opy/invariants/17_die_even_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c
 nat x
 nat temp

diff --git a/...ants/bit_flip_conditioning_invariant.pgcl → ...ants/bit_flip_conditioning_invariant.pgcl b/...ants/bit_flip_conditioning_invariant.pgcl → ...ants/bit_flip_conditioning_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 bool b1
 bool b2
 bool b3

diff --git a/...valence/invariants/condand_invariant.pgcl → ...e/loopy/invariants/condand_invariant.pgcl b/...valence/invariants/condand_invariant.pgcl → ...e/loopy/invariants/condand_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 

diff --git a/...alence/invariants/dep_bern_invariant.pgcl → .../loopy/invariants/dep_bern_invariant.pgcl b/...alence/invariants/dep_bern_invariant.pgcl → .../loopy/invariants/dep_bern_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 nat m;
 nat n;

diff --git a/...iants/endless_conditioning_invariant.pgcl → ...iants/endless_conditioning_invariant.pgcl b/...iants/endless_conditioning_invariant.pgcl → ...iants/endless_conditioning_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 
 if (x = 1){

diff --git a/...lence/invariants/geometric_invariant.pgcl → ...loopy/invariants/geometric_invariant.pgcl b/...lence/invariants/geometric_invariant.pgcl → ...loopy/invariants/geometric_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat temp;

diff --git a/...ivalence/geometric_observe_invariant.pgcl → ...variants/geometric_observe_invariant.pgcl b/...ivalence/geometric_observe_invariant.pgcl → ...variants/geometric_observe_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat y;
 nat x;
 nat tmp;

diff --git a/...variants/geometric_shifted_invariant.pgcl → ...variants/geometric_shifted_invariant.pgcl b/...variants/geometric_shifted_invariant.pgcl → ...variants/geometric_shifted_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat temp;

diff --git a/...alence/invariants/ky_die_2_invariant.pgcl → .../loopy/invariants/ky_die_2_invariant.pgcl b/...alence/invariants/ky_die_2_invariant.pgcl → .../loopy/invariants/ky_die_2_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat die;
 

diff --git a/...ivalence/invariants/ky_die_invariant.pgcl → ...ce/loopy/invariants/ky_die_invariant.pgcl b/...ivalence/invariants/ky_die_invariant.pgcl → ...ce/loopy/invariants/ky_die_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat die;
 

diff --git a/...nce/invariants/n_geometric_invariant.pgcl → ...opy/invariants/n_geometric_invariant.pgcl b/...nce/invariants/n_geometric_invariant.pgcl → ...opy/invariants/n_geometric_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat c;
 nat tmp;

diff --git a/...ce/invariants/nested_while_inv_outer.pgcl → ...y/invariants/nested_while_invariant1.pgcl b/...ce/invariants/nested_while_inv_outer.pgcl → ...y/invariants/nested_while_invariant1.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat y;
 nat c;

diff --git a/...ce/invariants/nested_while_inv_inner.pgcl → ...y/invariants/nested_while_invariant2.pgcl b/...ce/invariants/nested_while_inv_inner.pgcl → ...y/invariants/nested_while_invariant2.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat y;
 nat temp;

diff --git a/...nce/invariants/random_walk_invariant.pgcl → ...opy/invariants/random_walk_invariant.pgcl b/...nce/invariants/random_walk_invariant.pgcl → ...opy/invariants/random_walk_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat s;
 nat c;
 nat tmp;

diff --git a/...ariants/rejection_sampling_invariant.pgcl → ...ariants/rejection_sampling_invariant.pgcl b/...ariants/rejection_sampling_invariant.pgcl → ...ariants/rejection_sampling_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 if(c%2=0){

diff --git a/...ants/running_paper_example_invariant.pgcl → ...ants/running_paper_example_invariant.pgcl b/...ants/running_paper_example_invariant.pgcl → ...ants/running_paper_example_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat x;
 nat c;
 nat tmp;

diff --git a/...nvariants/sequential_loops_first_inv.pgcl → ...variants/sequential_loops_invariant1.pgcl b/...nvariants/sequential_loops_first_inv.pgcl → ...variants/sequential_loops_invariant1.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 nat m;
 nat n;

diff --git a/...variants/sequential_loops_second_inv.pgcl → ...variants/sequential_loops_invariant2.pgcl b/...variants/sequential_loops_second_inv.pgcl → ...variants/sequential_loops_invariant2.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat m;
 nat c;
 nat tmp;

diff --git a/...ts/skip_rejection_sampling_invariant.pgcl → ...ts/skip_rejection_sampling_invariant.pgcl b/...ts/skip_rejection_sampling_invariant.pgcl → ...ts/skip_rejection_sampling_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 if ( not (c%2=0)){

diff --git a/...nce/invariants/trivial_iid_invariant.pgcl → ...opy/invariants/trivial_iid_invariant.pgcl b/...nce/invariants/trivial_iid_invariant.pgcl → ...opy/invariants/trivial_iid_invariant.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat n;
 nat m;
 nat tmp;

diff --git a/pgfexamples/loop_equivalence/ky_die.pgcl → pgfexamples/equivalence/loopy/ky_die.pgcl b/pgfexamples/loop_equivalence/ky_die.pgcl → pgfexamples/equivalence/loopy/ky_die.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/ky_die.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl
 nat s;
 nat die;
 

diff --git a/pgfexamples/loop_equivalence/ky_die_2.pgcl → pgfexamples/equivalence/loopy/ky_die_2.pgcl b/pgfexamples/loop_equivalence/ky_die_2.pgcl → pgfexamples/equivalence/loopy/ky_die_2.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/ky_die_2.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl
 nat s;
 nat die;
 

diff --git a/pgfexamples/equivalence/loopy/n_geometric.pgcl b/pgfexamples/equivalence/loopy/n_geometric.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/n_geometric.pgcl pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl
+nat n;
+nat c;
+nat tmp;
+
+while(n > 0){
+    {n := n - 1 } [1/2] {c := c + 1}
+    tmp := 0
+}
diff --git a/...amples/loop_equivalence/nested_while.pgcl → ...mples/equivalence/loopy/nested_while.pgcl b/...amples/loop_equivalence/nested_while.pgcl → ...mples/equivalence/loopy/nested_while.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/nested_while.pgcl pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl
 nat x;
 nat y;
 nat c;

diff --git a/pgfexamples/equivalence/loopy/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl
@@ -0,0 +1,10 @@
+# check_equality pgfexamples/equivalence/loopy/random_walk.pgcl pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl
+nat s;
+nat c;
+nat tmp;
+
+while(s > 0){
+    {s := s+1} [1/2] {s := s-1}
+    c := c+1
+    tmp := 0
+}
diff --git a/pgfexamples/equivalence/loopy/running_paper_example.pgcl b/pgfexamples/equivalence/loopy/running_paper_example.pgcl
@@ -0,0 +1,9 @@
+# check_equality pgfexamples/equivalence/loopy/running_paper_example.pgcl pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl
+nat x;
+nat c;
+nat tmp;
+
+while(x > 0) {
+ { x := x-1 } [1/2] { c := c+1 }
+ tmp := 0;
+}
diff --git a/...es/loop_equivalence/sequential_loops.pgcl → ...s/equivalence/loopy/sequential_loops.pgcl b/...es/loop_equivalence/sequential_loops.pgcl → ...s/equivalence/loopy/sequential_loops.pgcl
@@ -1,3 +1,4 @@
+# check_equality pgfexamples/equivalence/loopy/sequential_loops.pgcl pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl
 nat c;
 nat m;
 nat n;

diff --git a/..._equivalence/skip_rejection_sampling.pgcl → ...alence/loopy/skip_rejection_sampling.pgcl b/..._equivalence/skip_rejection_sampling.pgcl → ...alence/loopy/skip_rejection_sampling.pgcl
@@ -1,3 +1,4 @@
+# skip
 nat c;
 
 while (c%2=0){

diff --git a/pgfexamples/equivalence/loopy/trivial_iid.pgcl b/pgfexamples/equivalence/loopy/trivial_iid.pgcl
@@ -0,0 +1,12 @@
+# check_equality pgfexamples/equivalence/loopy/trivial_iid.pgcl pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl
+nat n;
+nat m;
+nat tmp;
+
+while (0 < n) {
+ tmp := unif(1,6);
+ m := m + tmp;
+ tmp := 0;
+ n := n-1
+}
+
diff --git a/pgfexamples/evt_invariants/faulty_decrement.pgcl b/pgfexamples/evt_invariants/faulty_decrement.pgcl
diff --git a/pgfexamples/evt_invariants/geometric.pgcl b/pgfexamples/evt_invariants/geometric.pgcl
diff --git a/pgfexamples/evt_invariants/geometric_counter.pgcl b/pgfexamples/evt_invariants/geometric_counter.pgcl
-Original file line number
+Diff line change
@@ -1,3 +1,4 @@
+    # skip
     nat n;
     nat m;
@@ Expand Down @@