pgcl2heyvl: replace @k-induction(1,..) with @invariant(...)

pgcl/examples-heyvl/2drwalk.heyvl

@@ -200,7 +200,7 @@ coproc main(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x: UInt,
     y = init_y
     d = init_d
     n = init_n
-    @k_induction(1, 2 * ((n + 1) - d))
+    @invariant(2 * ((n + 1) - d))
     while d < n {
         if 0 < x {
             if 0 < y {

pgcl/examples-heyvl/bayesian_network.heyvl

@@ -102,7 +102,7 @@ coproc main(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_g: UInt
     l = init_l
     g = init_g
     n = init_n
-    @k_induction(1, 5 * n)
+    @invariant(5 * n)
     while 0 < n {
         prob_choice = flip(0.3)
         if prob_choice {

pgcl/examples-heyvl/condand.heyvl

@@ -24,7 +24,7 @@ coproc main(init_n: UInt, init_m: UInt) -> (n: UInt, m: UInt)
     var prob_choice: Bool
     n = init_n
     m = init_m
-    @k_induction(1, m + n)
+    @invariant(m + n)
     while (0 < n) && (0 < m) {
         prob_choice = flip((1/2))
         if prob_choice {

pgcl/examples-heyvl/esc_spline_ast.heyvl

@@ -18,7 +18,7 @@ proc main(init_x: UInt) -> (x: UInt)
 {
     var prob_choice: Bool
     x = init_x
-    @ast(true, x, v, 1/(v+1), 1)
+    @ast(true, x, v, 1 / (v + 1), 1)
     while 0 < x {
         prob_choice = flip(1 / (x + 1))
         if prob_choice {

pgcl/examples-heyvl/fcall.heyvl

@@ -27,7 +27,7 @@ coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: U
     x = init_x
     n = init_n
     r = init_r
-    @k_induction(1, 2 * (n - x))
+    @invariant(2 * (n - x))
     while x < n {
         prob_choice = flip((1/2))
         if prob_choice {

pgcl/examples-heyvl/hyper.heyvl

@@ -31,7 +31,7 @@ coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: U
     x = init_x
     n = init_n
     r = init_r
-    @k_induction(1, 5 * (n - x))
+    @invariant(5 * (n - x))
     while (x + 2) <= n {
         prob_choice = flip((117/145))
         if prob_choice {

pgcl/examples-heyvl/linear01.heyvl

@@ -22,7 +22,7 @@ coproc main(init_x: UInt) -> (x: UInt)
 {
     var prob_choice: Bool
     x = init_x
-    @k_induction(1, 0.6 * x)
+    @invariant(0.6 * x)
     while 2 <= x {
         prob_choice = flip((1/3))
         if prob_choice {

pgcl/examples-heyvl/nested-rabin.heyvl

@@ -34,10 +34,10 @@ proc main(init_i: UInt, init_n: UInt, init_d: UInt) -> (i: UInt, n: UInt, d: UIn
     i = init_i
     n = init_n
     d = init_d
-    @k_induction(1, [(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3))))
+    @invariant([(n <= 5) && (i <= 5)] * ([1 == i] + ([1 < i] * (2/3))))
     while 1 < i {
         n = i
-        @k_induction(1, ([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))))))
+        @invariant(([(n <= 5) && (i <= 5)] * [(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32))))))) + ((([i == n] * n) * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))) + ([i == (n + 1)] * (((((([n == 0] * 1) + ([n == 1] * (1/2))) + ([n == 2] * (1/4))) + ([n == 3] * (1/8))) + ([n == 4] * (1/16))) + ([n == 5] * (1/32)))))))
         while 0 < n {
             prob_choice = flip(0.5)
             if prob_choice {

pgcl/examples-heyvl/prdwalk.heyvl

@@ -56,7 +56,7 @@ coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: U
     x = init_x
     n = init_n
     r = init_r
-    @k_induction(1, 1.14286 * ((n + 4) - x))
+    @invariant(1.14286 * ((n + 4) - x))
     while x < n {
         prob_choice = flip((1/2))
         if prob_choice {

pgcl/examples-heyvl/prspeed.heyvl

@@ -44,7 +44,7 @@ coproc main(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt) -> (x: UInt,
     y = init_y
     m = init_m
     n = init_n
-    @k_induction(1, (2 * (m - y)) + (0.6666667 * (n - x)))
+    @invariant((2 * (m - y)) + (0.6666667 * (n - x)))
     while (x + 3) <= n {
         if y < m {
             prob_choice = flip((1/2))

pgcl/examples-heyvl/rabin1.heyvl

@@ -38,7 +38,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
-    @k_induction(1, ([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1))
+    @invariant(([((1 < i) && (i < 2)) && (phase == 0)] * (2/3)) + ([!(((1 < i) && (i < 2)) && (phase == 0))] * 1))
     while (1 < i) || (phase == 1) {
         if phase == 0 {
             n = i

pgcl/examples-heyvl/rabin1_wlp.heyvl

@@ -38,7 +38,7 @@ proc main(init_i: UInt, init_n: UInt, init_d: UInt, init_phase: UInt) -> (i: UIn
     n = init_n
     d = init_d
     phase = init_phase
-    @k_induction(1, [((1 < i) && (i < 2)) && (phase == 0)] * (2/3))
+    @invariant([((1 < i) && (i < 2)) && (phase == 0)] * (2/3))
     while (1 < i) || (phase == 1) {
         if phase == 0 {
             n = i

pgcl/examples-heyvl/rdspeed.heyvl

@@ -48,7 +48,7 @@ coproc main(init_x: UInt, init_y: UInt, init_m: UInt, init_n: UInt, init_r: UInt
     m = init_m
     n = init_n
     r = init_r
-    @k_induction(1, (2 * (m - y)) + (0.666667 * (n - x)))
+    @invariant((2 * (m - y)) + (0.666667 * (n - x)))
     while (x + 3) <= n {
         if y < m {
             prob_choice = flip((1/2))

pgcl/examples-heyvl/rdwalk.heyvl

@@ -24,7 +24,7 @@ coproc main(init_x: UInt, init_n: UInt) -> (x: UInt, n: UInt)
     var prob_choice: Bool
     x = init_x
     n = init_n
-    @k_induction(1, 2 * ((n + 1) - x))
+    @invariant(2 * ((n + 1) - x))
     while x < n {
         prob_choice = flip((1/2))
         if prob_choice {

pgcl/examples-heyvl/sprdwalk.heyvl

@@ -27,7 +27,7 @@ coproc main(init_x: UInt, init_n: UInt, init_r: UInt) -> (x: UInt, n: UInt, r: U
     x = init_x
     n = init_n
     r = init_r
-    @k_induction(1, 2 * (n - x))
+    @invariant(2 * (n - x))
     while x < n {
         prob_choice = flip((1/2))
         if prob_choice {

pgcl/examples-heyvl/test_ost.heyvl

@@ -1,39 +1 @@
-// Auto-generated by pgcl2heyvl from test_ost.pgcl
-//
-// HeyVL file to show that
-//     b + [a] <= wp[C](b)
-// using the Optional Stopping Theorem from Aiming Low is Harder paper with
-// invariant = b + [a], c = 1 and
-// past-invariant = 2 * [a] is used to show that C is PAST by showing
-//      2 * [a] >= ert[C](0)
-// for the pGCL program C:
-//
-//     bool a;
-//     nat b;
-//     nat k;
-//     while (a) {
-//         {
-//             a := false;
-//         } [0.5] {
-//             b := b + 1;
-//         }
-//         k := k + 1;
-//     }
-
-proc main(init_a: Bool, init_b: UInt, init_k: UInt) -> (a: Bool, b: UInt, k: UInt)
-{
-    var prob_choice: Bool
-    a = init_a
-    b = init_b
-    k = init_k
-    @ost(b + [a], 2 * [a], 1, b)
-    while a {
-        prob_choice = flip(0.5)
-        if prob_choice {
-            a = false
-        } else {
-            b = b + 1
-        }
-        k = k + 1
-    }
-}
+Error: You need to provide a --past-invariant parameter.

pgcl/pgcl2heyvl/pgcl2heyvl/encode.py

@@ -108,7 +108,8 @@ def encode_k_ind(program: Program, post: Expr, pre: Expr, calculus: Calculus,
     else:
         raise Exception("unsupported calculus.")
 
-    loop_annotation_stack = [(Encoding.K_INDUCTION, [k, _encode_expr(inv)]) for (k, inv) in loop_annotations]
+
+    loop_annotation_stack = [(Encoding.INVARIANT, [_encode_expr(inv)]) if k == 1 else (Encoding.K_INDUCTION, [k, _encode_expr(inv)]) for (k, inv) in loop_annotations]
 
     prob_choice_decl = []
     if _has_prob_choices(program):