pgcl2heyvl: fix bounded mc terminators

moves-rwth · Feb 20, 2025 · 5254be8 · 5254be8
1 parent 88a6958
commit 5254be8
Show file tree

Hide file tree

Showing 8 changed files with 12 additions and 10 deletions.
diff --git a/pgcl/examples-heyvl/refute-brp5_bmc.heyvl b/pgcl/examples-heyvl/refute-brp5_bmc.heyvl
@@ -10,7 +10,7 @@ coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_faile
     maxFailed = init_maxFailed
     failed = init_failed
     totalFailed = init_totalFailed
-    @unroll(14, totalFailed + 1)
+    @unroll(14, 0)
     while (failed < maxFailed) && (sent < toSend) {
         prob_choice = flip(0.9)
         if prob_choice {

diff --git a/pgcl/examples-heyvl/refute-geo2_bmc.heyvl b/pgcl/examples-heyvl/refute-geo2_bmc.heyvl
@@ -7,7 +7,7 @@ coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt)
     var prob_choice: Bool
     c = init_c
     f = init_f
-    @unroll(12, c + 0.99)
+    @unroll(12, 0)
     while f == 1 {
         prob_choice = flip(0.5)
         if prob_choice {

diff --git a/pgcl/examples-heyvl/refute-geo3_bmc.heyvl b/pgcl/examples-heyvl/refute-geo3_bmc.heyvl
@@ -7,7 +7,7 @@ coproc main(init_c: UInt, init_f: UInt) -> (c: UInt, f: UInt)
     var prob_choice: Bool
     c = init_c
     f = init_f
-    @unroll(47, c + 0.999999999999)
+    @unroll(47, 0)
     while f == 1 {
         prob_choice = flip(0.5)
         if prob_choice {

diff --git a/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin3_bmc.heyvl
@@ -9,7 +9,7 @@ coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: U
     n = init_n
     d = init_d
     phase = init_phase
-    @unroll(5, ([((1 < i) && (i < 4)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 4)) && (phase == 0))] * 1))
+    @unroll(5, 0)
     while (1 < i) || (phase == 1) {
         if phase == 0 {
             n = i

diff --git a/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin4_bmc.heyvl
@@ -9,7 +9,7 @@ coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: U
     n = init_n
     d = init_d
     phase = init_phase
-    @unroll(5, ([(1 < i) && (phase == 0)] * (1/3)) + ([!((1 < i) && (phase == 0))] * 1))
+    @unroll(5, 0)
     while (1 < i) || (phase == 1) {
         if phase == 0 {
             n = i

diff --git a/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl b/pgcl/examples-heyvl/refute-rabin5_bmc.heyvl
@@ -9,7 +9,7 @@ coproc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: U
     n = init_n
     d = init_d
     phase = init_phase
-    @unroll(9, ([(1 < i) && (phase == 0)] * 0.6) + ([!((1 < i) && (phase == 0))] * 1))
+    @unroll(9, 0)
     while (1 < i) || (phase == 1) {
         if phase == 0 {
             n = i

diff --git a/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl b/pgcl/examples-heyvl/refute-unif_gen1_bmc.heyvl
@@ -12,7 +12,7 @@ coproc main(init_elow: UInt, init_ehigh: UInt, init_n: UInt, init_v: UInt, init_
     c = init_c
     running = init_running
     i = init_i
-    @unroll(2, ([(((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh)] * 0.49) + ([!((((((((elow + 1) == ehigh) && (n == ((ehigh - elow) + 1))) && (v == 1)) && (c == 0)) && (running == 0)) && !(i < elow)) && (i <= ehigh))] * 1))
+    @unroll(2, 0)
     while running == 0 {
         v = 2 * v
         prob_choice = flip(0.5)

diff --git a/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py b/pgcl/pgcl2heyvl/pgcl2heyvl/encode.py
@@ -171,17 +171,19 @@ def encode_bounded_mc(program: Program, post: Expr, pre: Expr,
     # Replace the variables with their initial versions before encoding
     hey_init_pre = _encode_expr(_to_init_expr(pre))
 
-    global _encode_direction
 
+    global _encode_direction
     if calculus == Calculus.WLP:
         _encode_direction = Direction.DOWN
+        terminator = HeyExpr("1")
     elif calculus == Calculus.WP or calculus == Calculus.ERT:
         _encode_direction = Direction.UP
+        terminator = HeyExpr("0")
     else:
         raise Exception("unsupported calculus.")
 
-    loop_annotation_stack = [(Encoding.UNROLL,  [k, _encode_expr(inv)])
-                              for (k, inv) in loop_annotations]
+    loop_annotation_stack = [(Encoding.UNROLL,  [k, terminator])
+                              for (k, _) in loop_annotations]
 
     prob_choice_decl = []
     if _has_prob_choices(program):