Skip to content

Commit

Permalink
pgcl2heyvl: remove doc comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@umutdural
umutdural committed Feb 20, 2025
1 parent 74edc98 commit 88a6958
Show file tree
Hide file tree
Showing 43 changed files with 0 additions and 1,352 deletions.
190 changes: 0 additions & 190 deletions pgcl/examples-heyvl/2drwalk.heyvl
View file
Original file line number Diff line number Diff line change
@@ -1,195 +1,5 @@
// Auto-generated by pgcl2heyvl from 2drwalk.pgcl
//
// HeyVL file to show
// 2 * ((n + 1) - d) >= ert[C](0)
// using k-induction with k = 1 and invariant = 2 * ((n + 1) - d)
// for the pGCL program C:
//
// nat x;
// nat y;
// nat d;
// nat n;
// while (d < n) {
// if (0 < x) {
// if (0 < y) {
// {
// x := x + 2;
// d := d + 2;
// } [1/4] {
// {
// y := y + 2;
// d := d + 2;
// } [1/3] {
// {
// x := x - 1;
// d := d - 1;
// } [1/2] {
// y := y - 1;
// d := d - 1;
// }
// }
// }
// } else {
// if (y < 0) {
// {
// x := x + 2;
// d := d + 2;
// } [1/4] {
// {
// y := y + 1;
// d := d - 1;
// } [1/3] {
// {
// x := x - 1;
// d := d - 1;
// } [1/2] {
// y := y - 2;
// d := d + 2;
// }
// }
// }
// } else {
// {
// x := x + 2;
// d := d + 2;
// } [1/4] {
// {
// y := y + 1;
// d := d + 1;
// } [1/3] {
// {
// x := x - 1;
// d := d - 1;
// } [1/2] {
// y := y - 1;
// d := d + 1;
// }
// }
// }
// }
// }
// } else {
// if (x < 0) {
// if (0 < y) {
// {
// x := x + 1;
// d := d - 1;
// } [1/4] {
// {
// y := y + 2;
// d := d + 2;
// } [1/3] {
// {
// x := x - 2;
// d := d + 2;
// } [1/2] {
// y := y - 1;
// d := d - 1;
// }
// }
// }
// } else {
// if (y < 0) {
// {
// x := x + 1;
// d := d - 1;
// } [1/4] {
// {
// y := y + 1;
// d := d - 1;
// } [1/3] {
// {
// x := x - 2;
// d := d + 2;
// } [1/2] {
// y := y - 2;
// d := d + 2;
// }
// }
// }
// } else {
// {
// x := x + 1;
// d := d - 1;
// } [1/4] {
// {
// y := y + 1;
// d := d + 1;
// } [1/3] {
// {
// x := x - 2;
// d := d + 2;
// } [1/2] {
// y := y - 1;
// d := d + 1;
// }
// }
// }
// }
// }
// } else {
// if (0 < y) {
// {
// x := x + 1;
// d := d + 1;
// } [1/4] {
// {
// y := y + 2;
// d := d + 2;
// } [1/3] {
// {
// x := x - 1;
// d := d + 1;
// } [1/2] {
// y := y - 1;
// d := d - 1;
// }
// }
// }
// } else {
// if (y < 0) {
// {
// x := x + 1;
// d := d + 1;
// } [1/4] {
// {
// y := y + 1;
// d := d - 1;
// } [1/3] {
// {
// x := x - 1;
// d := d + 1;
// } [1/2] {
// y := y - 2;
// d := d + 2;
// }
// }
// }
// } else {
// {
// x := x + 1;
// d := d + 1;
// } [1/4] {
// {
// y := y + 1;
// d := d + 1;
// } [1/3] {
// {
// x := x - 1;
// d := d + 1;
// } [1/2] {
// y := y - 1;
// d := d + 1;
// }
// }
// }
// }
// }
// }
// }
// tick(1);
// }

@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)
Expand Down
26 changes: 0 additions & 26 deletions pgcl/examples-heyvl/C4B_t303.heyvl
View file
Original file line number Diff line number Diff line change
@@ -1,31 +1,5 @@
// Auto-generated by pgcl2heyvl from C4B_t303.pgcl
//
// HeyVL file to show
// (0.5 * (x + 2)) + (0.5 * (y + 2)) >= ert[C](0)
// using k-induction with k = 3 and invariant = (0.5 * (x + 2)) + (0.5 * (y + 2))
// for the pGCL program C:
//
// nat x;
// nat y;
// nat t;
// nat r;
// while (0 < x) {
// {
// r := 1;
// } [1/3] {
// {
// r := 2;
// } [1/2] {
// r := 3;
// }
// }
// x := x - r;
// t := x;
// x := y;
// y := t;
// tick(1);
// }

@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))
Expand Down
18 changes: 0 additions & 18 deletions pgcl/examples-heyvl/ast-rule.heyvl
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,5 @@
// Auto-generated by pgcl2heyvl from ast-rule.pgcl
//
// HeyVL file to show that C is almost-surely terminating
// using AST rule by McIver et al. (2018) with
// invariant = true, variant = (3 * [!((x % 2) == 0)]) + (([10 <= x] * (x - 10)) + ([!(10 <= x)] * (10 - x))), probability function p(v) = 0.5, decrease function d(v) = 2
// for the pGCL program C:
//
// nat x;
// while (not (x = 10)) {
// if ((x % 2) = 0) {
// {
// x := x - 2;
// } [1/2] {
// x := x + 2;
// }
// } else {
// x := x + 1;
// }
// }

proc main(init_x: UInt) -> (x: UInt)
{
var prob_choice: Bool
Expand Down
22 changes: 0 additions & 22 deletions pgcl/examples-heyvl/ast-rule2.heyvl
View file
Original file line number Diff line number Diff line change
@@ -1,27 +1,5 @@
// Auto-generated by pgcl2heyvl from ast-rule2.pgcl
//
// HeyVL file to show that C is almost-surely terminating
// using AST rule by McIver et al. (2018) with
// invariant = true, variant = [0 < x] + [(1 <= x) && (x <= 2)], probability function p(v) = 0.5, decrease function d(v) = 1
// for the pGCL program C:
//
// nat x;
// while (0 < x) {
// if (x = 1) {
// {
// x := 0;
// } [1/2] {
// x := x + 1;
// }
// } else {
// if (3 <= x) {
// x := 0;
// } else {
// x := x + 1;
// }
// }
// }

proc main(init_x: UInt) -> (x: UInt)
{
var prob_choice: Bool
Expand Down
90 changes: 0 additions & 90 deletions pgcl/examples-heyvl/bayesian_network.heyvl
View file
Original file line number Diff line number Diff line change
@@ -1,95 +1,5 @@
// Auto-generated by pgcl2heyvl from bayesian_network.pgcl
//
// HeyVL file to show
// 5 * n >= ert[C](0)
// using k-induction with k = 1 and invariant = 5 * n
// for the pGCL program C:
//
// nat i;
// nat d;
// nat s;
// nat l;
// nat g;
// nat n;
// while (0 < n) {
// {
// i := 1;
// } [0.3] {
// i := 0;
// }
// tick(1);
// {
// d := 1;
// } [0.4] {
// d := 0;
// }
// tick(1);
// if ((i < 1) & (d < 1)) {
// {
// g := 1;
// } [0.7] {
// g := 0;
// }
// tick(1);
// } else {
// if ((i < 1) & (0 < d)) {
// {
// g := 1;
// } [0.95] {
// g := 0;
// }
// tick(1);
// } else {
// if ((0 < i) & (d < 1)) {
// {
// g := 1;
// } [0.1] {
// g := 0;
// }
// tick(1);
// } else {
// {
// g := 1;
// } [0.5] {
// g := 0;
// }
// tick(1);
// }
// }
// }
// if (i < 1) {
// {
// s := 1;
// } [0.05] {
// s := 0;
// }
// tick(1);
// } else {
// {
// s := 1;
// } [0.8] {
// s := 0;
// }
// tick(1);
// }
// if (g < 1) {
// {
// l := 1;
// } [0.1] {
// l := 0;
// }
// tick(1);
// } else {
// {
// l := 1;
// } [0.6] {
// l := 0;
// }
// tick(1);
// }
// n := n - 1;
// }

@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
Expand Down
Loading

0 comments on commit 88a6958

Please sign in to comment.