pgcl2heyvl: add annotation support, regenerate examples with annotati…

…ons instead of direct encodings
moves-rwth · Feb 20, 2025 · 23aa72a · 23aa72a
1 parent d4fd2ae
commit 23aa72a
Show file tree

Hide file tree

Showing 50 changed files with 1,408 additions and 3,075 deletions.
diff --git a/pgcl/examples-heyvl/2drwalk.heyvl b/pgcl/examples-heyvl/2drwalk.heyvl
@@ -190,7 +190,8 @@
 //         tick(1);
 //     }
 
-coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x: UInt, y: UInt, d: UInt, n: UInt)
+@ert
+coproc main(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x: UInt, y: UInt, d: UInt, n: UInt)
     pre 2 * ((init_n + 1) - init_d)
     post 0
 {
@@ -199,11 +200,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x
     y = init_y
     d = init_d
     n = init_n
-    coassert 2 * ((n + 1) - d)
-    cohavoc d, x, y
-    covalidate
-    coassume 2 * ((n + 1) - d)
-    if d < n {
+    @k_induction(1, 2 * ((n + 1) - d))
+    while d < n {
         if 0 < x {
             if 0 < y {
                 prob_choice = flip((1/4))
@@ -409,7 +407,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_d: UInt, init_n: UInt) -> (x
             }
         }
         tick 1
-        assert 2 * ((n + 1) - d)
-        assume 0
-    } else {}
+    }
 }
diff --git a/pgcl/examples-heyvl/C4B_t303.heyvl b/pgcl/examples-heyvl/C4B_t303.heyvl
@@ -26,7 +26,8 @@
 //         tick(1);
 //     }
 
-coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x: UInt, y: UInt, t: UInt, r: UInt)
+@ert
+coproc main(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x: UInt, y: UInt, t: UInt, r: UInt)
     pre (0.5 * (init_x + 2)) + (0.5 * (init_y + 2))
     post 0
 {
@@ -35,11 +36,8 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x
     y = init_y
     t = init_t
     r = init_r
-    coassert (0.5 * (x + 2)) + (0.5 * (y + 2))
-    cohavoc r, t, x, y
-    covalidate
-    coassume (0.5 * (x + 2)) + (0.5 * (y + 2))
-    if 0 < x {
+    @k_induction(3, (0.5 * (x + 2)) + (0.5 * (y + 2)))
+    while 0 < x {
         prob_choice = flip((1/3))
         if prob_choice {
             r = 1
@@ -56,45 +54,5 @@ coproc k_induction(init_x: UInt, init_y: UInt, init_t: UInt, init_r: UInt) -> (x
         x = y
         y = t
         tick 1
-        assert (0.5 * (x + 2)) + (0.5 * (y + 2))
-        if 0 < x {
-            prob_choice = flip((1/3))
-            if prob_choice {
-                r = 1
-            } else {
-                prob_choice = flip((1/2))
-                if prob_choice {
-                    r = 2
-                } else {
-                    r = 3
-                }
-            }
-            x = x - r
-            t = x
-            x = y
-            y = t
-            tick 1
-            assert (0.5 * (x + 2)) + (0.5 * (y + 2))
-            if 0 < x {
-                prob_choice = flip((1/3))
-                if prob_choice {
-                    r = 1
-                } else {
-                    prob_choice = flip((1/2))
-                    if prob_choice {
-                        r = 2
-                    } else {
-                        r = 3
-                    }
-                }
-                x = x - r
-                t = x
-                x = y
-                y = t
-                tick 1
-                assert (0.5 * (x + 2)) + (0.5 * (y + 2))
-                assume 0
-            } else {}
-        } else {}
-    } else {}
+    }
 }
diff --git a/pgcl/examples-heyvl/ast-rule.heyvl b/pgcl/examples-heyvl/ast-rule.heyvl
@@ -18,26 +18,12 @@
 //         }
 //     }
 
-// forall l. (v <= l) ==> (prob(l) <= prob(v))
-proc prob_antitone(x: UInt, v: UReal) -> ()
-{
-    assert ?(forall l: UReal.  (v <= l) ==> (0.5 <= 0.5))
-}
-
-// forall l. (v <= l) ==> (decrease(l) <= decrease(v))
-proc decrease_antitone(x: UInt, v: UReal) -> ()
-{
-    assert ?(forall l: UReal. (v <= l) ==> (2 <= 2))
-}
-
-// [I] <= \Phi_{[I]}([I])
-proc I_wp_subinvariant(init_x: UInt) -> (x: UInt)
-    pre [true]
-    post [true]
+proc main(init_x: UInt) -> (x: UInt)
 {
     var prob_choice: Bool
     x = init_x
-    if !(x == 10) {
+    @ast(true, (3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))), v, 0.5, 2)
+    while !(x == 10) {
         if (x % 2) == 0 {
             prob_choice = flip((1/2))
             if prob_choice {
@@ -48,51 +34,5 @@ proc I_wp_subinvariant(init_x: UInt) -> (x: UInt)
         } else {
             x = x + 1
         }
-    } else {}
-}
-
-// !G iff V = 0
-proc termination_condition(x: UInt) -> ()
-{
-    assert ?(!(!(x == 10)) == ((3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))) == 0))
-}
-
-// \Phi_{V}(V) <= V
-coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt)
-    pre (3 * [!((init_x % 2) == 0)]) + (([10 <= init_x] * (init_x - 10)) + ([!(10 <= init_x)] * (10 - init_x)))
-    post (3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x)))
-{
-    var prob_choice: Bool
-    x = init_x
-    if !(x == 10) {
-        if (x % 2) == 0 {
-            prob_choice = flip((1/2))
-            if prob_choice {
-                x = x - 2
-            } else {
-                x = x + 2
-            }
-        } else {
-            x = x + 1
-        }
-    } else {}
-}
-
-// [I] * [G] * (p o V) <= \s. wp[P]([V <= V(s) - d(V(s))])(s)
-proc progress_condition(init_x: UInt) -> (x: UInt)
-    pre [true] * ([!(init_x == 10)] * 0.5)
-    post [((3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x)))) <= (((3 * [!((init_x % 2) == 0)]) + (([10 <= init_x] * (init_x - 10)) + ([!(10 <= init_x)] * (10 - init_x)))) - 2)]
-{
-    var prob_choice: Bool
-    x = init_x
-    if (x % 2) == 0 {
-        prob_choice = flip((1/2))
-        if prob_choice {
-            x = x - 2
-        } else {
-            x = x + 2
-        }
-    } else {
-        x = x + 1
     }
 }
diff --git a/pgcl/examples-heyvl/ast-rule2.heyvl b/pgcl/examples-heyvl/ast-rule2.heyvl
@@ -22,26 +22,12 @@
 //         }
 //     }
 
-// forall l. (v <= l) ==> (prob(l) <= prob(v))
-proc prob_antitone(x: UInt, v: UReal) -> ()
-{
-    assert ?(forall l: UReal.  (v <= l) ==> (0.5 <= 0.5))
-}
-
-// forall l. (v <= l) ==> (decrease(l) <= decrease(v))
-proc decrease_antitone(x: UInt, v: UReal) -> ()
-{
-    assert ?(forall l: UReal. (v <= l) ==> (1 <= 1))
-}
-
-// [I] <= \Phi_{[I]}([I])
-proc I_wp_subinvariant(init_x: UInt) -> (x: UInt)
-    pre [true]
-    post [true]
+proc main(init_x: UInt) -> (x: UInt)
 {
     var prob_choice: Bool
     x = init_x
-    if 0 < x {
+    @ast(true, [0 < x] + [(1 <= x) && (x <= 2)], v, 0.5, 1)
+    while 0 < x {
         if x == 1 {
             prob_choice = flip((1/2))
             if prob_choice {
@@ -56,59 +42,5 @@ proc I_wp_subinvariant(init_x: UInt) -> (x: UInt)
                 x = x + 1
             }
         }
-    } else {}
-}
-
-// !G iff V = 0
-proc termination_condition(x: UInt) -> ()
-{
-    assert ?(!(0 < x) == ([0 < x] + [(1 <= x) && (x <= 2)] == 0))
-}
-
-// \Phi_{V}(V) <= V
-coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt)
-    pre [0 < init_x] + [(1 <= init_x) && (init_x <= 2)]
-    post [0 < x] + [(1 <= x) && (x <= 2)]
-{
-    var prob_choice: Bool
-    x = init_x
-    if 0 < x {
-        if x == 1 {
-            prob_choice = flip((1/2))
-            if prob_choice {
-                x = 0
-            } else {
-                x = x + 1
-            }
-        } else {
-            if 3 <= x {
-                x = 0
-            } else {
-                x = x + 1
-            }
-        }
-    } else {}
-}
-
-// [I] * [G] * (p o V) <= \s. wp[P]([V <= V(s) - d(V(s))])(s)
-proc progress_condition(init_x: UInt) -> (x: UInt)
-    pre [true] * ([0 < init_x] * 0.5)
-    post [([0 < x] + [(1 <= x) && (x <= 2)]) <= (([0 < init_x] + [(1 <= init_x) && (init_x <= 2)]) - 1)]
-{
-    var prob_choice: Bool
-    x = init_x
-    if x == 1 {
-        prob_choice = flip((1/2))
-        if prob_choice {
-            x = 0
-        } else {
-            x = x + 1
-        }
-    } else {
-        if 3 <= x {
-            x = 0
-        } else {
-            x = x + 1
-        }
     }
 }
diff --git a/pgcl/examples-heyvl/bayesian_network.heyvl b/pgcl/examples-heyvl/bayesian_network.heyvl
@@ -90,7 +90,8 @@
 //         n := n - 1;
 //     }
 
-coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_g: UInt, init_n: UInt) -> (i: UInt, d: UInt, s: UInt, l: UInt, g: UInt, n: UInt)
+@ert
+coproc main(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_g: UInt, init_n: UInt) -> (i: UInt, d: UInt, s: UInt, l: UInt, g: UInt, n: UInt)
     pre 5 * init_n
     post 0
 {
@@ -101,11 +102,8 @@ coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_
     l = init_l
     g = init_g
     n = init_n
-    coassert 5 * n
-    cohavoc d, g, i, l, n, s
-    covalidate
-    coassume 5 * n
-    if 0 < n {
+    @k_induction(1, 5 * n)
+    while 0 < n {
         prob_choice = flip(0.3)
         if prob_choice {
             i = 1
@@ -192,7 +190,5 @@ coproc k_induction(init_i: UInt, init_d: UInt, init_s: UInt, init_l: UInt, init_
             tick 1
         }
         n = n - 1
-        assert 5 * n
-        assume 0
-    } else {}
+    }
 }
diff --git a/pgcl/examples-heyvl/brp1.heyvl b/pgcl/examples-heyvl/brp1.heyvl
@@ -20,7 +20,8 @@
 //         }
 //     }
 
-coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt)
+@wp
+coproc main(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, init_failed: UInt, init_totalFailed: UInt) -> (toSend: UInt, sent: UInt, maxFailed: UInt, failed: UInt, totalFailed: UInt)
     pre ([init_toSend <= 4] * (init_totalFailed + 1)) + ([!(init_toSend <= 4)] * ∞)
     post totalFailed
 {
@@ -30,11 +31,8 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini
     maxFailed = init_maxFailed
     failed = init_failed
     totalFailed = init_totalFailed
-    coassert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-    cohavoc failed, sent, totalFailed
-    covalidate
-    coassume ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-    if (failed < maxFailed) && (sent < toSend) {
+    @k_induction(5, ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞))
+    while (failed < maxFailed) && (sent < toSend) {
         prob_choice = flip(0.9)
         if prob_choice {
             failed = 0
@@ -43,51 +41,5 @@ coproc k_induction(init_toSend: UInt, init_sent: UInt, init_maxFailed: UInt, ini
             failed = failed + 1
             totalFailed = totalFailed + 1
         }
-        assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-        if (failed < maxFailed) && (sent < toSend) {
-            prob_choice = flip(0.9)
-            if prob_choice {
-                failed = 0
-                sent = sent + 1
-            } else {
-                failed = failed + 1
-                totalFailed = totalFailed + 1
-            }
-            assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-            if (failed < maxFailed) && (sent < toSend) {
-                prob_choice = flip(0.9)
-                if prob_choice {
-                    failed = 0
-                    sent = sent + 1
-                } else {
-                    failed = failed + 1
-                    totalFailed = totalFailed + 1
-                }
-                assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-                if (failed < maxFailed) && (sent < toSend) {
-                    prob_choice = flip(0.9)
-                    if prob_choice {
-                        failed = 0
-                        sent = sent + 1
-                    } else {
-                        failed = failed + 1
-                        totalFailed = totalFailed + 1
-                    }
-                    assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-                    if (failed < maxFailed) && (sent < toSend) {
-                        prob_choice = flip(0.9)
-                        if prob_choice {
-                            failed = 0
-                            sent = sent + 1
-                        } else {
-                            failed = failed + 1
-                            totalFailed = totalFailed + 1
-                        }
-                        assert ([toSend <= 4] * (totalFailed + 1)) + ([!(toSend <= 4)] * ∞)
-                        assume 0
-                    } else {}
-                } else {}
-            } else {}
-        } else {}
-    } else {}
+    }
 }