diff --git a/examples/pgcl/coupon/coupon10-classic.pgcl b/examples/pgcl/coupon/coupon10-classic.pgcl
new file mode 100644
index 000000000..d1c3cd015
--- /dev/null
+++ b/examples/pgcl/coupon/coupon10-classic.pgcl
@@ -0,0 +1,58 @@
+function coupon10() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+ int coup7 := 0;
+ int coup8 := 0;
+ int coup9 := 0;
+ int coup10 := 0;
+
+ int draw := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
+ draw := unif(0,10);
+ draw2 := unif(0,10);
+ draw3 := unif(0,10);
+ numberDraws := numberDraws + 1;
+
+ if(draw = 0) {
+ coup0 := 1;
+ }
+ if(draw = 1) {
+ coup1 := 1;
+ }
+ if(draw = 2) {
+ coup2 := 1;
+ }
+ if(draw = 3) {
+ coup3 := 1;
+ }
+ if(draw = 4) {
+ coup4 := 1;
+ }
+ if(draw = 5) {
+ coup5 := 1;
+ }
+ if(draw = 6) {
+ coup6 := 1;
+ }
+ if(draw = 7) {
+ coup7 := 1;
+ }
+ if(draw = 8) {
+ coup8 := 1;
+ }
+ if(draw = 9) {
+ coup9 := 1;
+ }
+ if(draw = 10) {
+ coup10 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon10-cost.pgcl b/examples/pgcl/coupon/coupon10-cost.pgcl
new file mode 100644
index 000000000..740da760c
--- /dev/null
+++ b/examples/pgcl/coupon/coupon10-cost.pgcl
@@ -0,0 +1,60 @@
+function coupon10() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+ int coup7 := 0;
+ int coup8 := 0;
+ int coup9 := 0;
+ int coup10 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int cost := 1;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
+ draw1 := unif(0,10);
+ draw2 := unif(0,10);
+ draw3 := unif(0,10);
+ cost := ceil(1.02 * cost);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
+ coup7 := 1;
+ }
+ if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
+ coup8 := 1;
+ }
+ if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
+ coup9 := 1;
+ }
+ if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
+ coup10 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon10-observe.pgcl b/examples/pgcl/coupon/coupon10-observe.pgcl
new file mode 100644
index 000000000..0ccdfb6f7
--- /dev/null
+++ b/examples/pgcl/coupon/coupon10-observe.pgcl
@@ -0,0 +1,62 @@
+function coupon10() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+ int coup7 := 0;
+ int coup8 := 0;
+ int coup9 := 0;
+ int coup10 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
+ draw1 := unif(0,10);
+ draw2 := unif(0,10);
+ draw3 := unif(0,10);
+ numberDraws := numberDraws + 1;
+
+ observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
+ coup7 := 1;
+ }
+ if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
+ coup8 := 1;
+ }
+ if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
+ coup9 := 1;
+ }
+ if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
+ coup10 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon10.pgcl b/examples/pgcl/coupon/coupon10.pgcl
new file mode 100644
index 000000000..95c9eae1e
--- /dev/null
+++ b/examples/pgcl/coupon/coupon10.pgcl
@@ -0,0 +1,60 @@
+function coupon10() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+ int coup7 := 0;
+ int coup8 := 0;
+ int coup9 := 0;
+ int coup10 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
+ draw1 := unif(0,10);
+ draw2 := unif(0,10);
+ draw3 := unif(0,10);
+ numberDraws := numberDraws + 1;
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
+ coup7 := 1;
+ }
+ if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
+ coup8 := 1;
+ }
+ if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
+ coup9 := 1;
+ }
+ if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
+ coup10 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon3-classic.pgcl b/examples/pgcl/coupon/coupon3-classic.pgcl
new file mode 100644
index 000000000..b7c7d5b0d
--- /dev/null
+++ b/examples/pgcl/coupon/coupon3-classic.pgcl
@@ -0,0 +1,24 @@
+function coupon3() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+
+ int draw := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
+ draw := unif(0,2);
+ numberDraws := numberDraws + 1;
+
+ if(draw = 0) {
+ coup0 := 1;
+ }
+ if(draw = 1) {
+ coup1 := 1;
+ }
+ if(draw = 2) {
+ coup2 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon3-cost.pgcl b/examples/pgcl/coupon/coupon3-cost.pgcl
new file mode 100644
index 000000000..6f474942a
--- /dev/null
+++ b/examples/pgcl/coupon/coupon3-cost.pgcl
@@ -0,0 +1,28 @@
+function coupon3() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int cost := 1;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
+ draw1 := unif(0,2);
+ draw2 := unif(0,2);
+ draw3 := unif(0,2);
+ cost := ceil(1.02 * cost);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon3-observe.pgcl b/examples/pgcl/coupon/coupon3-observe.pgcl
new file mode 100644
index 000000000..6f41e7caf
--- /dev/null
+++ b/examples/pgcl/coupon/coupon3-observe.pgcl
@@ -0,0 +1,30 @@
+function coupon3() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
+ draw1 := unif(0,2);
+ draw2 := unif(0,2);
+ draw3 := unif(0,2);
+ numberDraws := numberDraws + 1;
+
+ observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon3.pgcl b/examples/pgcl/coupon/coupon3.pgcl
new file mode 100644
index 000000000..1d4e4e7c6
--- /dev/null
+++ b/examples/pgcl/coupon/coupon3.pgcl
@@ -0,0 +1,28 @@
+function coupon3() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
+ draw1 := unif(0,2);
+ draw2 := unif(0,2);
+ draw3 := unif(0,2);
+ numberDraws := numberDraws + 1;
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon4-observe.pgcl b/examples/pgcl/coupon/coupon4-observe.pgcl
new file mode 100644
index 000000000..fb6d5bcf6
--- /dev/null
+++ b/examples/pgcl/coupon/coupon4-observe.pgcl
@@ -0,0 +1,34 @@
+function coupon4() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1)) {
+ draw1 := unif(0,4);
+ draw2 := unif(0,4);
+ draw3 := unif(0,4);
+ numberDraws := numberDraws + 1;
+
+ observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon5-classic.pgcl b/examples/pgcl/coupon/coupon5-classic.pgcl
new file mode 100644
index 000000000..b27c381cf
--- /dev/null
+++ b/examples/pgcl/coupon/coupon5-classic.pgcl
@@ -0,0 +1,32 @@
+function coupon5() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+
+ int draw := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
+ draw := unif(0,4);
+ numberDraws := numberDraws + 1;
+
+ if(draw = 0) {
+ coup0 := 1;
+ }
+ if(draw = 1) {
+ coup1 := 1;
+ }
+ if(draw = 2) {
+ coup2 := 1;
+ }
+ if(draw = 3) {
+ coup3 := 1;
+ }
+ if(draw = 4) {
+ coup4 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon5-cost.pgcl b/examples/pgcl/coupon/coupon5-cost.pgcl
new file mode 100644
index 000000000..84779cad1
--- /dev/null
+++ b/examples/pgcl/coupon/coupon5-cost.pgcl
@@ -0,0 +1,36 @@
+function coupon5() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int cost := 1;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
+ draw1 := unif(0,4);
+ draw2 := unif(0,4);
+ draw3 := unif(0,4);
+ cost := ceil(1.02 * cost);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon5-observe.pgcl b/examples/pgcl/coupon/coupon5-observe.pgcl
new file mode 100644
index 000000000..734ccd127
--- /dev/null
+++ b/examples/pgcl/coupon/coupon5-observe.pgcl
@@ -0,0 +1,38 @@
+function coupon5() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
+ draw1 := unif(0,4);
+ draw2 := unif(0,4);
+ draw3 := unif(0,4);
+ numberDraws := numberDraws + 1;
+
+ observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon5.pgcl b/examples/pgcl/coupon/coupon5.pgcl
new file mode 100644
index 000000000..aede63e50
--- /dev/null
+++ b/examples/pgcl/coupon/coupon5.pgcl
@@ -0,0 +1,36 @@
+function coupon5() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
+ draw1 := unif(0,4);
+ draw2 := unif(0,4);
+ draw3 := unif(0,4);
+ numberDraws := numberDraws + 1;
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon7-classic.pgcl b/examples/pgcl/coupon/coupon7-classic.pgcl
new file mode 100644
index 000000000..af9156ff1
--- /dev/null
+++ b/examples/pgcl/coupon/coupon7-classic.pgcl
@@ -0,0 +1,40 @@
+function coupon7() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+
+ int draw := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
+ draw := unif(0,6);
+ numberDraws := numberDraws + 1;
+
+ if(draw = 0) {
+ coup0 := 1;
+ }
+ if(draw = 1) {
+ coup1 := 1;
+ }
+ if(draw = 2) {
+ coup2 := 1;
+ }
+ if(draw = 3) {
+ coup3 := 1;
+ }
+ if(draw = 4) {
+ coup4 := 1;
+ }
+ if(draw = 5) {
+ coup5 := 1;
+ }
+ if(draw = 6) {
+ coup6 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon7-cost.pgcl b/examples/pgcl/coupon/coupon7-cost.pgcl
new file mode 100644
index 000000000..d71b367ca
--- /dev/null
+++ b/examples/pgcl/coupon/coupon7-cost.pgcl
@@ -0,0 +1,44 @@
+function coupon7() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int cost := 1;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
+ draw1 := unif(0,6);
+ draw2 := unif(0,6);
+ draw3 := unif(0,6);
+ cost := ceil(1.02 * cost);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon7-observe.pgcl b/examples/pgcl/coupon/coupon7-observe.pgcl
new file mode 100644
index 000000000..89f74bcd9
--- /dev/null
+++ b/examples/pgcl/coupon/coupon7-observe.pgcl
@@ -0,0 +1,46 @@
+function coupon7() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
+ draw1 := unif(0,6);
+ draw2 := unif(0,6);
+ draw3 := unif(0,6);
+ numberDraws := numberDraws + 1;
+
+ observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/coupon/coupon7.pgcl b/examples/pgcl/coupon/coupon7.pgcl
new file mode 100644
index 000000000..43bb38e99
--- /dev/null
+++ b/examples/pgcl/coupon/coupon7.pgcl
@@ -0,0 +1,44 @@
+function coupon7() {
+ int coup0 := 0;
+ int coup1 := 0;
+ int coup2 := 0;
+ int coup3 := 0;
+ int coup4 := 0;
+ int coup5 := 0;
+ int coup6 := 0;
+
+ int draw1 := 0;
+ int draw2 := 0;
+ int draw3 := 0;
+
+ int numberDraws := 0;
+
+ while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
+ draw1 := unif(0,6);
+ draw2 := unif(0,6);
+ draw3 := unif(0,6);
+ numberDraws := numberDraws + 1;
+
+ if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
+ coup0 := 1;
+ }
+ if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
+ coup1 := 1;
+ }
+ if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
+ coup2 := 1;
+ }
+ if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
+ coup3 := 1;
+ }
+ if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
+ coup4 := 1;
+ }
+ if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
+ coup5 := 1;
+ }
+ if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
+ coup6 := 1;
+ }
+ }
+}
diff --git a/examples/pgcl/crowds/crowds100-100-observeOther.pgcl b/examples/pgcl/crowds/crowds100-100-observeOther.pgcl
new file mode 100644
index 000000000..042b1d232
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-100-observeOther.pgcl
@@ -0,0 +1,35 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 100;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+ observe(observeOther > 25);
+}
diff --git a/examples/pgcl/crowds/crowds100-100.pgcl b/examples/pgcl/crowds/crowds100-100.pgcl
new file mode 100644
index 000000000..384340bd2
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-100.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 100;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds100-60-observeOther.pgcl b/examples/pgcl/crowds/crowds100-60-observeOther.pgcl
new file mode 100644
index 000000000..0578344f0
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-60-observeOther.pgcl
@@ -0,0 +1,35 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 60;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+ observe(observeOther > 15);
+}
diff --git a/examples/pgcl/crowds/crowds100-60-param.pgcl b/examples/pgcl/crowds/crowds100-60-param.pgcl
new file mode 100644
index 000000000..92bd1d051
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-60-param.pgcl
@@ -0,0 +1,34 @@
+function crowds(double PF, double bad) {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 60;
+ int observeSender := 0; // in [0, TotalRuns]
+ int observeOther := 0; // in [0, TotalRuns]
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [bad] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [PF]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds100-60.pgcl b/examples/pgcl/crowds/crowds100-60.pgcl
new file mode 100644
index 000000000..5e3ccd71e
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-60.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 60;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds100-80-observeOther.pgcl b/examples/pgcl/crowds/crowds100-80-observeOther.pgcl
new file mode 100644
index 000000000..62a412425
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-80-observeOther.pgcl
@@ -0,0 +1,36 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 80;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ // lastSender := unif(0, 24);
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+ observe(observeOther > 20);
+}
diff --git a/examples/pgcl/crowds/crowds100-80.pgcl b/examples/pgcl/crowds/crowds100-80.pgcl
new file mode 100644
index 000000000..f9fa42758
--- /dev/null
+++ b/examples/pgcl/crowds/crowds100-80.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 80;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/100] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds3-3-param.pgcl b/examples/pgcl/crowds/crowds3-3-param.pgcl
new file mode 100644
index 000000000..8486d0a75
--- /dev/null
+++ b/examples/pgcl/crowds/crowds3-3-param.pgcl
@@ -0,0 +1,34 @@
+function crowds(double PF, double bad) {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 3;
+ int observeSender := 0; // in [0, TotalRuns]
+ int observeOther := 0; // in [0, TotalRuns]
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [bad] {
+ {
+ { lastSender:=0; } [1/3] { lastSender := 1; }
+ }
+ [PF]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds3-3.pgcl b/examples/pgcl/crowds/crowds3-3.pgcl
new file mode 100644
index 000000000..3106f70ca
--- /dev/null
+++ b/examples/pgcl/crowds/crowds3-3.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 3;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/3] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds3-5-param.pgcl b/examples/pgcl/crowds/crowds3-5-param.pgcl
new file mode 100644
index 000000000..177e73cf4
--- /dev/null
+++ b/examples/pgcl/crowds/crowds3-5-param.pgcl
@@ -0,0 +1,33 @@
+function crowds(double PF, double bad) {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 5;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [bad] {
+ { lastSender:=0; } [1/3] { lastSender := 1; }
+ }
+ [PF]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds3-5.pgcl b/examples/pgcl/crowds/crowds3-5.pgcl
new file mode 100644
index 000000000..f43bb6505
--- /dev/null
+++ b/examples/pgcl/crowds/crowds3-5.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 5;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/3] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds5-20-param.pgcl b/examples/pgcl/crowds/crowds5-20-param.pgcl
new file mode 100644
index 000000000..121c29ace
--- /dev/null
+++ b/examples/pgcl/crowds/crowds5-20-param.pgcl
@@ -0,0 +1,34 @@
+function crowds(double PF, double bad) {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 20;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [bad] {
+ {
+ { lastSender:=0; } [1/5] { lastSender := 1; }
+ }
+ [PF]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ // Set up new run.
+ delivered := 0;
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/crowds/crowds5-20.pgcl b/examples/pgcl/crowds/crowds5-20.pgcl
new file mode 100644
index 000000000..c27eae6ff
--- /dev/null
+++ b/examples/pgcl/crowds/crowds5-20.pgcl
@@ -0,0 +1,34 @@
+function crowds() {
+ int delivered := 0;
+ int lastSender := 0;
+ int remainingRuns := 20;
+ int observeSender := 0;
+ int observeOther := 0;
+
+ while(remainingRuns > 0) {
+ while(delivered = 0) {
+ {
+ if(lastSender = 0) {
+ observeSender := observeSender + 1;
+ } else {
+ observeOther := observeOther + 1;
+ }
+ lastSender := 0;
+ delivered := 1;
+ } [0.091] {
+ {
+ { lastSender:=0; } [1/5] { lastSender := 1; }
+ }
+ [0.8]
+ {
+ lastSender := 0;
+ // When not forwarding, the message is delivered here.
+ delivered := 1;
+ }
+ }
+ }
+ delivered := 0;
+ // Set up new run.
+ remainingRuns := remainingRuns - 1;
+ }
+}
diff --git a/examples/pgcl/herman/herman10-det.pgcl b/examples/pgcl/herman/herman10-det.pgcl
new file mode 100644
index 000000000..5c38402aa
--- /dev/null
+++ b/examples/pgcl/herman/herman10-det.pgcl
@@ -0,0 +1,108 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [0.5] {x1 := 1;}
+ {x2 := 0;} [0.5] {x2 := 1;}
+ {x3 := 0;} [0.5] {x3 := 1;}
+ {x4 := 0;} [0.5] {x4 := 1;}
+ {x5 := 0;} [0.5] {x5 := 1;}
+ {x6 := 0;} [0.5] {x6 := 1;}
+ {x7 := 0;} [0.5] {x7 := 1;}
+ {x8 := 0;} [0.5] {x8 := 1;}
+ {x9 := 0;} [0.5] {x9 := 1;}
+ {x10 := 0;} [0.5] {x10 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ if(x1 = oldx10) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx10;
+ }
+ oldx10 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman10.pgcl b/examples/pgcl/herman/herman10.pgcl
new file mode 100644
index 000000000..a2bb9563e
--- /dev/null
+++ b/examples/pgcl/herman/herman10.pgcl
@@ -0,0 +1,108 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [] {x1 := 1;}
+ {x2 := 0;} [] {x2 := 1;}
+ {x3 := 0;} [] {x3 := 1;}
+ {x4 := 0;} [] {x4 := 1;}
+ {x5 := 0;} [] {x5 := 1;}
+ {x6 := 0;} [] {x6 := 1;}
+ {x7 := 0;} [] {x7 := 1;}
+ {x8 := 0;} [] {x8 := 1;}
+ {x9 := 0;} [] {x9 := 1;}
+ {x10 := 0;} [] {x10 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ if(x1 = oldx10) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx10;
+ }
+ oldx10 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman13-det.pgcl b/examples/pgcl/herman/herman13-det.pgcl
new file mode 100644
index 000000000..744c0361e
--- /dev/null
+++ b/examples/pgcl/herman/herman13-det.pgcl
@@ -0,0 +1,138 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [0.5] {x1 := 1;}
+ {x2 := 0;} [0.5] {x2 := 1;}
+ {x3 := 0;} [0.5] {x3 := 1;}
+ {x4 := 0;} [0.5] {x4 := 1;}
+ {x5 := 0;} [0.5] {x5 := 1;}
+ {x6 := 0;} [0.5] {x6 := 1;}
+ {x7 := 0;} [0.5] {x7 := 1;}
+ {x8 := 0;} [0.5] {x8 := 1;}
+ {x9 := 0;} [0.5] {x9 := 1;}
+ {x10 := 0;} [0.5] {x10 := 1;}
+ {x11 := 0;} [0.5] {x11 := 1;}
+ {x12 := 0;} [0.5] {x12 := 1;}
+ {x13 := 0;} [0.5] {x13 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ if(x1 = oldx13) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx13;
+ }
+ oldx13 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman13.pgcl b/examples/pgcl/herman/herman13.pgcl
new file mode 100644
index 000000000..057cf9568
--- /dev/null
+++ b/examples/pgcl/herman/herman13.pgcl
@@ -0,0 +1,138 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [] {x1 := 1;}
+ {x2 := 0;} [] {x2 := 1;}
+ {x3 := 0;} [] {x3 := 1;}
+ {x4 := 0;} [] {x4 := 1;}
+ {x5 := 0;} [] {x5 := 1;}
+ {x6 := 0;} [] {x6 := 1;}
+ {x7 := 0;} [] {x7 := 1;}
+ {x8 := 0;} [] {x8 := 1;}
+ {x9 := 0;} [] {x9 := 1;}
+ {x10 := 0;} [] {x10 := 1;}
+ {x11 := 0;} [] {x11 := 1;}
+ {x12 := 0;} [] {x12 := 1;}
+ {x13 := 0;} [] {x13 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ if(x1 = oldx13) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx13;
+ }
+ oldx13 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman17-det.pgcl b/examples/pgcl/herman/herman17-det.pgcl
new file mode 100644
index 000000000..f572bf2a6
--- /dev/null
+++ b/examples/pgcl/herman/herman17-det.pgcl
@@ -0,0 +1,178 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int x14 := 0;
+ int x15 := 0;
+ int x16 := 0;
+ int x17 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+ int oldx14 := 0;
+ int oldx15 := 0;
+ int oldx16 := 0;
+ int oldx17 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [0.5] {x1 := 1;}
+ {x2 := 0;} [0.5] {x2 := 1;}
+ {x3 := 0;} [0.5] {x3 := 1;}
+ {x4 := 0;} [0.5] {x4 := 1;}
+ {x5 := 0;} [0.5] {x5 := 1;}
+ {x6 := 0;} [0.5] {x6 := 1;}
+ {x7 := 0;} [0.5] {x7 := 1;}
+ {x8 := 0;} [0.5] {x8 := 1;}
+ {x9 := 0;} [0.5] {x9 := 1;}
+ {x10 := 0;} [0.5] {x10 := 1;}
+ {x11 := 0;} [0.5] {x11 := 1;}
+ {x12 := 0;} [0.5] {x12 := 1;}
+ {x13 := 0;} [0.5] {x13 := 1;}
+ {x14 := 0;} [0.5] {x14 := 1;}
+ {x15 := 0;} [0.5] {x15 := 1;}
+ {x16 := 0;} [0.5] {x16 := 1;}
+ {x17 := 0;} [0.5] {x17 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ oldx14 := x14;
+ oldx15 := x15;
+ oldx16 := x16;
+ oldx17 := x17;
+ if(x1 = oldx17) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx17;
+ }
+ oldx17 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ if(x14 = oldx13) {
+ {x14 := 0;} [0.5] {x14 := 1;}
+ } else {
+ x14 := oldx13;
+ }
+ oldx13 := 0;
+ if(x15 = oldx14) {
+ {x15 := 0;} [0.5] {x15 := 1;}
+ } else {
+ x15 := oldx14;
+ }
+ oldx14 := 0;
+ if(x16 = oldx15) {
+ {x16 := 0;} [0.5] {x16 := 1;}
+ } else {
+ x16 := oldx15;
+ }
+ oldx15 := 0;
+ if(x17 = oldx16) {
+ {x17 := 0;} [0.5] {x17 := 1;}
+ } else {
+ x17 := oldx16;
+ }
+ oldx16 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman17.pgcl b/examples/pgcl/herman/herman17.pgcl
new file mode 100644
index 000000000..b8cb86176
--- /dev/null
+++ b/examples/pgcl/herman/herman17.pgcl
@@ -0,0 +1,178 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int x14 := 0;
+ int x15 := 0;
+ int x16 := 0;
+ int x17 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+ int oldx14 := 0;
+ int oldx15 := 0;
+ int oldx16 := 0;
+ int oldx17 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [] {x1 := 1;}
+ {x2 := 0;} [] {x2 := 1;}
+ {x3 := 0;} [] {x3 := 1;}
+ {x4 := 0;} [] {x4 := 1;}
+ {x5 := 0;} [] {x5 := 1;}
+ {x6 := 0;} [] {x6 := 1;}
+ {x7 := 0;} [] {x7 := 1;}
+ {x8 := 0;} [] {x8 := 1;}
+ {x9 := 0;} [] {x9 := 1;}
+ {x10 := 0;} [] {x10 := 1;}
+ {x11 := 0;} [] {x11 := 1;}
+ {x12 := 0;} [] {x12 := 1;}
+ {x13 := 0;} [] {x13 := 1;}
+ {x14 := 0;} [] {x14 := 1;}
+ {x15 := 0;} [] {x15 := 1;}
+ {x16 := 0;} [] {x16 := 1;}
+ {x17 := 0;} [] {x17 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ oldx14 := x14;
+ oldx15 := x15;
+ oldx16 := x16;
+ oldx17 := x17;
+ if(x1 = oldx17) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx17;
+ }
+ oldx17 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ if(x14 = oldx13) {
+ {x14 := 0;} [0.5] {x14 := 1;}
+ } else {
+ x14 := oldx13;
+ }
+ oldx13 := 0;
+ if(x15 = oldx14) {
+ {x15 := 0;} [0.5] {x15 := 1;}
+ } else {
+ x15 := oldx14;
+ }
+ oldx14 := 0;
+ if(x16 = oldx15) {
+ {x16 := 0;} [0.5] {x16 := 1;}
+ } else {
+ x16 := oldx15;
+ }
+ oldx15 := 0;
+ if(x17 = oldx16) {
+ {x17 := 0;} [0.5] {x17 := 1;}
+ } else {
+ x17 := oldx16;
+ }
+ oldx16 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman21-det.pgcl b/examples/pgcl/herman/herman21-det.pgcl
new file mode 100644
index 000000000..a59482d9e
--- /dev/null
+++ b/examples/pgcl/herman/herman21-det.pgcl
@@ -0,0 +1,218 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int x14 := 0;
+ int x15 := 0;
+ int x16 := 0;
+ int x17 := 0;
+ int x18 := 0;
+ int x19 := 0;
+ int x20 := 0;
+ int x21 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+ int oldx14 := 0;
+ int oldx15 := 0;
+ int oldx16 := 0;
+ int oldx17 := 0;
+ int oldx18 := 0;
+ int oldx19 := 0;
+ int oldx20 := 0;
+ int oldx21 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [0.5] {x1 := 1;}
+ {x2 := 0;} [0.5] {x2 := 1;}
+ {x3 := 0;} [0.5] {x3 := 1;}
+ {x4 := 0;} [0.5] {x4 := 1;}
+ {x5 := 0;} [0.5] {x5 := 1;}
+ {x6 := 0;} [0.5] {x6 := 1;}
+ {x7 := 0;} [0.5] {x7 := 1;}
+ {x8 := 0;} [0.5] {x8 := 1;}
+ {x9 := 0;} [0.5] {x9 := 1;}
+ {x10 := 0;} [0.5] {x10 := 1;}
+ {x11 := 0;} [0.5] {x11 := 1;}
+ {x12 := 0;} [0.5] {x12 := 1;}
+ {x13 := 0;} [0.5] {x13 := 1;}
+ {x14 := 0;} [0.5] {x14 := 1;}
+ {x15 := 0;} [0.5] {x15 := 1;}
+ {x16 := 0;} [0.5] {x16 := 1;}
+ {x17 := 0;} [0.5] {x17 := 1;}
+ {x18 := 0;} [0.5] {x18 := 1;}
+ {x19 := 0;} [0.5] {x19 := 1;}
+ {x20 := 0;} [0.5] {x20 := 1;}
+ {x21 := 0;} [0.5] {x21 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ oldx14 := x14;
+ oldx15 := x15;
+ oldx16 := x16;
+ oldx17 := x17;
+ oldx18 := x18;
+ oldx19 := x19;
+ oldx20 := x20;
+ oldx21 := x21;
+ if(x1 = oldx21) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx21;
+ }
+ oldx21 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ if(x14 = oldx13) {
+ {x14 := 0;} [0.5] {x14 := 1;}
+ } else {
+ x14 := oldx13;
+ }
+ oldx13 := 0;
+ if(x15 = oldx14) {
+ {x15 := 0;} [0.5] {x15 := 1;}
+ } else {
+ x15 := oldx14;
+ }
+ oldx14 := 0;
+ if(x16 = oldx15) {
+ {x16 := 0;} [0.5] {x16 := 1;}
+ } else {
+ x16 := oldx15;
+ }
+ oldx15 := 0;
+ if(x17 = oldx16) {
+ {x17 := 0;} [0.5] {x17 := 1;}
+ } else {
+ x17 := oldx16;
+ }
+ oldx16 := 0;
+ if(x18 = oldx17) {
+ {x18 := 0;} [0.5] {x18 := 1;}
+ } else {
+ x18 := oldx17;
+ }
+ oldx17 := 0;
+ if(x19 = oldx18) {
+ {x19 := 0;} [0.5] {x19 := 1;}
+ } else {
+ x19 := oldx18;
+ }
+ oldx18 := 0;
+ if(x20 = oldx19) {
+ {x20 := 0;} [0.5] {x20 := 1;}
+ } else {
+ x20 := oldx19;
+ }
+ oldx19 := 0;
+ if(x21 = oldx20) {
+ {x21 := 0;} [0.5] {x21 := 1;}
+ } else {
+ x21 := oldx20;
+ }
+ oldx20 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman21.pgcl b/examples/pgcl/herman/herman21.pgcl
new file mode 100644
index 000000000..ccc00ca3f
--- /dev/null
+++ b/examples/pgcl/herman/herman21.pgcl
@@ -0,0 +1,218 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int x8 := 0;
+ int x9 := 0;
+ int x10 := 0;
+ int x11 := 0;
+ int x12 := 0;
+ int x13 := 0;
+ int x14 := 0;
+ int x15 := 0;
+ int x16 := 0;
+ int x17 := 0;
+ int x18 := 0;
+ int x19 := 0;
+ int x20 := 0;
+ int x21 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+ int oldx8 := 0;
+ int oldx9 := 0;
+ int oldx10 := 0;
+ int oldx11 := 0;
+ int oldx12 := 0;
+ int oldx13 := 0;
+ int oldx14 := 0;
+ int oldx15 := 0;
+ int oldx16 := 0;
+ int oldx17 := 0;
+ int oldx18 := 0;
+ int oldx19 := 0;
+ int oldx20 := 0;
+ int oldx21 := 0;
+
+ // determine starting token setup on the ring.
+ {x1 := 0;} [] {x1 := 1;}
+ {x2 := 0;} [] {x2 := 1;}
+ {x3 := 0;} [] {x3 := 1;}
+ {x4 := 0;} [] {x4 := 1;}
+ {x5 := 0;} [] {x5 := 1;}
+ {x6 := 0;} [] {x6 := 1;}
+ {x7 := 0;} [] {x7 := 1;}
+ {x8 := 0;} [] {x8 := 1;}
+ {x9 := 0;} [] {x9 := 1;}
+ {x10 := 0;} [] {x10 := 1;}
+ {x11 := 0;} [] {x11 := 1;}
+ {x12 := 0;} [] {x12 := 1;}
+ {x13 := 0;} [] {x13 := 1;}
+ {x14 := 0;} [] {x14 := 1;}
+ {x15 := 0;} [] {x15 := 1;}
+ {x16 := 0;} [] {x16 := 1;}
+ {x17 := 0;} [] {x17 := 1;}
+ {x18 := 0;} [] {x18 := 1;}
+ {x19 := 0;} [] {x19 := 1;}
+ {x20 := 0;} [] {x20 := 1;}
+ {x21 := 0;} [] {x21 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ oldx8 := x8;
+ oldx9 := x9;
+ oldx10 := x10;
+ oldx11 := x11;
+ oldx12 := x12;
+ oldx13 := x13;
+ oldx14 := x14;
+ oldx15 := x15;
+ oldx16 := x16;
+ oldx17 := x17;
+ oldx18 := x18;
+ oldx19 := x19;
+ oldx20 := x20;
+ oldx21 := x21;
+ if(x1 = oldx21) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx21;
+ }
+ oldx21 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ if(x8 = oldx7) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x8 := oldx7;
+ }
+ oldx7 := 0;
+ if(x9 = oldx8) {
+ {x9 := 0;} [0.5] {x9 := 1;}
+ } else {
+ x9 := oldx8;
+ }
+ oldx8 := 0;
+ if(x10 = oldx9) {
+ {x10 := 0;} [0.5] {x10 := 1;}
+ } else {
+ x10 := oldx9;
+ }
+ oldx9 := 0;
+ if(x11 = oldx10) {
+ {x11 := 0;} [0.5] {x11 := 1;}
+ } else {
+ x11 := oldx10;
+ }
+ oldx10 := 0;
+ if(x12 = oldx11) {
+ {x12 := 0;} [0.5] {x12 := 1;}
+ } else {
+ x12 := oldx11;
+ }
+ oldx11 := 0;
+ if(x13 = oldx12) {
+ {x13 := 0;} [0.5] {x13 := 1;}
+ } else {
+ x13 := oldx12;
+ }
+ oldx12 := 0;
+ if(x14 = oldx13) {
+ {x14 := 0;} [0.5] {x14 := 1;}
+ } else {
+ x14 := oldx13;
+ }
+ oldx13 := 0;
+ if(x15 = oldx14) {
+ {x15 := 0;} [0.5] {x15 := 1;}
+ } else {
+ x15 := oldx14;
+ }
+ oldx14 := 0;
+ if(x16 = oldx15) {
+ {x16 := 0;} [0.5] {x16 := 1;}
+ } else {
+ x16 := oldx15;
+ }
+ oldx15 := 0;
+ if(x17 = oldx16) {
+ {x17 := 0;} [0.5] {x17 := 1;}
+ } else {
+ x17 := oldx16;
+ }
+ oldx16 := 0;
+ if(x18 = oldx17) {
+ {x18 := 0;} [0.5] {x18 := 1;}
+ } else {
+ x18 := oldx17;
+ }
+ oldx17 := 0;
+ if(x19 = oldx18) {
+ {x19 := 0;} [0.5] {x19 := 1;}
+ } else {
+ x19 := oldx18;
+ }
+ oldx18 := 0;
+ if(x20 = oldx19) {
+ {x20 := 0;} [0.5] {x20 := 1;}
+ } else {
+ x20 := oldx19;
+ }
+ oldx19 := 0;
+ if(x21 = oldx19) {
+ {x21 := 0;} [0.5] {x21 := 1;}
+ } else {
+ x21 := oldx20;
+ }
+ oldx20 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman7-det.pgcl b/examples/pgcl/herman/herman7-det.pgcl
new file mode 100644
index 000000000..4374e28b0
--- /dev/null
+++ b/examples/pgcl/herman/herman7-det.pgcl
@@ -0,0 +1,77 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+
+ {x1 := 0;} [0.5] {x1 := 1;}
+ {x2 := 0;} [0.5] {x2 := 1;}
+ {x3 := 0;} [0.5] {x3 := 1;}
+ {x4 := 0;} [0.5] {x4 := 1;}
+ {x5 := 0;} [0.5] {x5 := 1;}
+ {x6 := 0;} [0.5] {x6 := 1;}
+ {x7 := 0;} [0.5] {x7 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ if(x1 = oldx7) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx7;
+ }
+ oldx7 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ }
+}
diff --git a/examples/pgcl/herman/herman7.pgcl b/examples/pgcl/herman/herman7.pgcl
new file mode 100644
index 000000000..aca00ece3
--- /dev/null
+++ b/examples/pgcl/herman/herman7.pgcl
@@ -0,0 +1,77 @@
+function herman() {
+ int x1 := 0;
+ int x2 := 0;
+ int x3 := 0;
+ int x4 := 0;
+ int x5 := 0;
+ int x6 := 0;
+ int x7 := 0;
+ int oldx1 := 0;
+ int oldx2 := 0;
+ int oldx3 := 0;
+ int oldx4 := 0;
+ int oldx5 := 0;
+ int oldx6 := 0;
+ int oldx7 := 0;
+
+ {x1 := 0;} [] {x1 := 1;}
+ {x2 := 0;} [] {x2 := 1;}
+ {x3 := 0;} [] {x3 := 1;}
+ {x4 := 0;} [] {x4 := 1;}
+ {x5 := 0;} [] {x5 := 1;}
+ {x6 := 0;} [] {x6 := 1;}
+ {x7 := 0;} [] {x7 := 1;}
+
+ // finds a ring configuration with exactly one token in the ring.
+ while((x1 + x2 + x3 + x4 + x5 + x6 + x7) != 1) {
+ oldx1 := x1;
+ oldx2 := x2;
+ oldx3 := x3;
+ oldx4 := x4;
+ oldx5 := x5;
+ oldx6 := x6;
+ oldx7 := x7;
+ if(x1 = oldx7) {
+ {x1 := 0;} [0.5] {x1 := 1;}
+ } else {
+ x1 := oldx7;
+ }
+ oldx7 := 0;
+ if(x2 = oldx1) {
+ {x2 := 0;} [0.5] {x2 := 1;}
+ } else {
+ x2 := oldx1;
+ }
+ oldx1 := 0;
+ if(x3 = oldx2) {
+ {x3 := 0;} [0.5] {x3 := 1;}
+ } else {
+ x3 := oldx2;
+ }
+ oldx2 := 0;
+ if(x4 = oldx3) {
+ {x4 := 0;} [0.5] {x4 := 1;}
+ } else {
+ x4 := oldx3;
+ }
+ oldx3 := 0;
+ if(x5 = oldx4) {
+ {x5 := 0;} [0.5] {x5 := 1;}
+ } else {
+ x5 := oldx4;
+ }
+ oldx4 := 0;
+ if(x6 = oldx5) {
+ {x6 := 0;} [0.5] {x6 := 1;}
+ } else {
+ x6 := oldx5;
+ }
+ oldx5 := 0;
+ if(x7 = oldx6) {
+ {x7 := 0;} [0.5] {x7 := 1;}
+ } else {
+ x7 := oldx6;
+ }
+ oldx6 := 0;
+ }
+}
diff --git a/examples/pgcl/lotkavolterra.pgcl b/examples/pgcl/lotkavolterra.pgcl
new file mode 100644
index 000000000..0397f0cac
--- /dev/null
+++ b/examples/pgcl/lotkavolterra.pgcl
@@ -0,0 +1,49 @@
+function lotkavolterra() {
+
+ int goats := 100;
+ int tigers := 4;
+ int dwellTime := 0;
+ int curTime := 0;
+ int b := 0;
+
+ while(tigers > 0 & goats > 0) {
+
+ dwellTime := 0;
+ b := 1;
+
+ if(goats > 0 & tigers > 0) {
+
+ // geometric distribution with p = 0.5
+ while (b >= 1) {
+ {b := 1;} [0.5] {b := 0;}
+ dwellTime := dwellTime + 1;
+ }
+ curTime := curTime + dwellTime;
+ {tigers := tigers + 1;} [0.2] {{goats := goats - 1;} [0.1] {tigers := tigers - 1;}}
+
+ } else { if(goats > 0) {
+
+ // geometric distribution with p = 0.5
+ while (b >= 1) {
+ {b := 1;} [0.5] {b := 0;}
+ dwellTime := dwellTime + 1;
+ }
+ curTime := curTime + dwellTime;
+ goats := goats + 1;
+
+ } else { if(tigers > 0) {
+
+ // geometric distribution with p = 0.5
+ while (b >= 1) {
+ {b := 1;} [0.5] {b := 0;}
+ dwellTime := dwellTime + 1;
+ }
+ curTime := curTime + dwellTime;
+ tigers := tigers - 1;
+
+ } } }
+
+ }
+
+}
+
diff --git a/examples/pgcl/robot.pgcl b/examples/pgcl/robot.pgcl
new file mode 100644
index 000000000..ad320ccac
--- /dev/null
+++ b/examples/pgcl/robot.pgcl
@@ -0,0 +1,26 @@
+function robotOnGrid() {
+
+ // robot starts in the lower left corner
+ int robotX := 1; int robotY := 20;
+
+ // janitor starts in the grid middle
+ int janitorX := ceil(20 / 2); int janitorY := ceil(20 / 2);
+
+ // iterates as long as the robot is not in the upper right corner
+ while(!(robotX = 20 & robotY = 1)) {
+
+ // robot perfoms one step at max each iteration
+ // checks whether we can go to the right and the janitor is not there
+ if(robotX < 20 & !((janitorX = robotX + 1) & (janitorY = robotY))) {
+ robotX := robotX + 1;
+ }
+ // checks whether we can go up and the janitor is not there
+ if(robotX = 20 & !((janitorX = robotX) & (janitorY = robotY - 1))) {
+ robotY := robotY - 1;
+ }
+
+ // moves the janitor randomly in one direction, not limited by any borders
+ {janitorX := janitorX + 1;}[0.25]{{janitorX := janitorX - 1;}[1/3]{{janitorY := janitorY + 1;}[0.375]{janitorY := janitorY - 1;}}}
+
+ }
+}
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1a46888ae..7ca492152 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -10,6 +10,7 @@ file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp)
file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.cpp)
+file(GLOB_RECURSE STORM_PGCL_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-pgcl.cpp)
# Additional include files like the storm-config.h
@@ -21,6 +22,7 @@ set(STORM_LIB_HEADERS ${STORM_HEADERS})
list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_HEADERS_CLI})
set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE})
set(STORM_DFT_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_DFT_MAIN_FILE})
+set(STORM_PGCL_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_PGCL_MAIN_FILE})
set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI})
file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.cpp)
@@ -53,6 +55,10 @@ add_executable(storm-dft-main ${STORM_DFT_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
target_link_libraries(storm-dft-main storm) # Adding headers for xcode
set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft")
+add_executable(storm-pgcl-main ${STORM_PGCL_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
+target_link_libraries(storm-pgcl-main storm)
+set_target_properties(storm-pgcl-main PROPERTIES OUTPUT_NAME "storm-pgcl")
+
target_link_libraries(storm ${STORM_LINK_LIBRARIES})
diff --git a/src/parser/PgclParser.cpp b/src/parser/PgclParser.cpp
new file mode 100755
index 000000000..24a10e62f
--- /dev/null
+++ b/src/parser/PgclParser.cpp
@@ -0,0 +1,315 @@
+/*
+ * File: PgclParser.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 1. April 2015, 19:12
+ */
+
+#include "src/parser/PgclParser.h"
+// If the parser fails due to ill-formed data, this exception is thrown.
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+ namespace parser {
+ storm::pgcl::PgclProgram PgclParser::parse(std::string const& filename) {
+ // Create empty program.
+ storm::pgcl::PgclProgram result;
+
+ // Open file and initialize result.
+ std::ifstream inputFileStream(filename, std::ios::in);
+ STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
+
+ // Now try to parse the contents of the file.
+ try {
+ std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
+ result = parseFromString(fileContent, filename);
+ } catch(std::exception& e) {
+ // In case of an exception properly close the file before passing exception.
+ inputFileStream.close();
+ throw e;
+ }
+
+ // Close the stream in case everything went smoothly and return result.
+ inputFileStream.close();
+ return result;
+ }
+
+ storm::pgcl::PgclProgram PgclParser::parseFromString(std::string const& input, std::string const& filename) {
+ PositionIteratorType first(input.begin());
+ PositionIteratorType iter = first;
+ PositionIteratorType last(input.end());
+
+ // Create empty program.
+ storm::pgcl::PgclProgram result;
+
+ // Create grammar.
+ storm::parser::PgclParser grammar(filename, first);
+ try {
+ // Start the parsing run.
+ bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing of PGCL program failed.");
+ STORM_LOG_DEBUG("Parse of PGCL program finished.");
+ } catch(qi::expectation_failure<PositionIteratorType> const& e) {
+ // If the parser expected content different than the one provided, display information about the location of the error.
+ std::size_t lineNumber = boost::spirit::get_line(e.first);
+ // Now propagate exception.
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
+ }
+
+ return result;
+ }
+
+ PgclParser::PgclParser(std::string const& filename, Iterator first) :
+ PgclParser::base_type(program, "PGCL grammar"),
+ annotate(first),
+ expressionManager(std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager())),
+ expressionParser(*expressionManager, invalidIdentifiers) {
+ this->enableExpressions();
+ /*
+ * PGCL grammar is defined here
+ */
+ // Rough program structure
+ program = (qi::lit("function ") >> programName >> qi::lit("(") >> -(doubleDeclaration % qi::lit(",")) >> qi::lit(")") >> qi::lit("{") >>
+ sequenceOfStatements >>
+ qi::lit("}"))
+ [qi::_val = phoenix::bind(&PgclParser::createProgram, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+ sequenceOfStatements %= +(statement);
+
+ // Statements
+ statement %= simpleStatement | compoundStatement;
+ simpleStatement %= assignmentStatement | integerDeclarationStatement | observeStatement;
+ compoundStatement %= ifElseStatement | loopStatement | branchStatement;
+
+ // Simple statements
+ doubleDeclaration = (qi::lit("double ") >> variableName)[qi::_val = phoenix::bind(&PgclParser::declareDoubleVariable, phoenix::ref(*this), qi::_1)];
+ integerDeclarationStatement = (qi::lit("int ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createIntegerDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+
+ assignmentStatement = (variableName >> qi::lit(":=") >> (expression | uniformExpression) >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+ observeStatement = (qi::lit("observe") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)];
+
+ // Compound statements
+ ifElseStatement = (qi::lit("if") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >>
+ sequenceOfStatements >>
+ qi::lit("}") >> -(qi::lit("else") >> qi::lit("{") >>
+ sequenceOfStatements >>
+ qi::lit("}")))
+ [qi::_val = phoenix::bind(&PgclParser::createIfElseStatement, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+ branchStatement = nondeterministicBranch | probabilisticBranch;
+ loopStatement = (qi::lit("while") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >>
+ sequenceOfStatements >>
+ qi::lit("}"))
+ [qi::_val = phoenix::bind(&PgclParser::createLoopStatement, phoenix::ref(*this), qi::_1, qi::_2)];
+ nondeterministicBranch = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[]") >> qi::lit("{") >> sequenceOfStatements>> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createNondeterministicBranch, phoenix::ref(*this), qi::_1, qi::_2)];
+ probabilisticBranch = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[") >> expression >> qi::lit("]") >> qi::lit("{") >> sequenceOfStatements >> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProbabilisticBranch, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
+
+ // Expression and condition building, and basic identifiers
+ expression %= expressionParser;
+ booleanCondition = expressionParser[qi::_val = phoenix::bind(&PgclParser::createBooleanExpression, phoenix::ref(*this), qi::_1)];
+ uniformExpression = (qi::lit("unif") >> qi::lit("(") >> qi::int_ >> qi::lit(",") >> qi::int_ >> qi::lit(")"))[qi::_val = phoenix::bind(&PgclParser::createUniformExpression, phoenix::ref(*this), qi::_1, qi::_2)];
+ variableName %= (+(qi::alnum | qi::lit("_"))) - (qi::lit("int") >> +(qi::alnum | qi::lit("_")));
+ programName %= +(qi::alnum | qi::lit("_"));
+
+ // Enables location tracking for important entities
+ auto setLocationInfoFunction = this->annotate(*qi::_val, qi::_1, qi::_3);
+ qi::on_success(assignmentStatement, setLocationInfoFunction);
+ qi::on_success(observeStatement, setLocationInfoFunction);
+ qi::on_success(nondeterministicBranch, setLocationInfoFunction);
+ qi::on_success(probabilisticBranch, setLocationInfoFunction);
+ qi::on_success(loopStatement, setLocationInfoFunction);
+ qi::on_success(ifElseStatement, setLocationInfoFunction);
+ qi::on_success(integerDeclarationStatement, setLocationInfoFunction);
+
+ // Adds dummy to the 0-th location.
+ std::shared_ptr<storm::pgcl::AssignmentStatement> dummy(new storm::pgcl::AssignmentStatement());
+ this->locationToStatement.insert(this->locationToStatement.begin(), dummy);
+ } // PgclParser()
+
+ void PgclParser::enableExpressions() {
+ (this->expressionParser).setIdentifierMapping(&this->identifiers_);
+ }
+
+ /*
+ * Creators for various program parts. They all follow the basic scheme
+ * to retrieve the subparts of the program part and mold them together
+ * into one new statement. They wrap the statement constructors and
+ * throw excpetions in case something unexpected was parsed, e.g.
+ * (x+5) as a boolean expression, or types of assignments don't match.
+ */
+ storm::pgcl::PgclProgram PgclParser::createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable> > parameters, std::vector<std::shared_ptr<storm::pgcl::Statement> > statements) {
+ // Creates an empty paramter list in case no parameters were given.
+ std::vector<storm::expressions::Variable> params;
+ if(parameters != boost::none) {
+ params = *parameters;
+ }
+ // Creates the actual program.
+ std::shared_ptr<storm::pgcl::PgclProgram> result(
+ new storm::pgcl::PgclProgram(statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, true)
+ );
+ result->back()->setLast(true);
+ // Sets the current program as a parent to all its direct children statements.
+ for(storm::pgcl::iterator it = result->begin(); it != result->end(); ++it) {
+ (*it)->setParentProgram(result);
+ }
+ return *result;
+ }
+
+ storm::expressions::Variable PgclParser::declareDoubleVariable(std::string const& variableName) {
+ storm::expressions::Variable variable = expressionManager->declareRationalVariable(variableName);
+ this->identifiers_.add(variableName, variable.getExpression());
+ return variable;
+ }
+
+ std::shared_ptr<storm::pgcl::AssignmentStatement> PgclParser::createAssignmentStatement(std::string const& variableName, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& assignedExpression) {
+ storm::expressions::Variable variable;
+ if(!(*expressionManager).hasVariable(variableName)) {
+ variable = (*expressionManager).declareIntegerVariable(variableName);
+ } else {
+ variable = (*expressionManager).getVariable(variableName);
+ // Checks if assignment types match.
+ if(assignedExpression.which() == 0 && !(variable.getType() == boost::get<storm::expressions::Expression>(assignedExpression).getType())) {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Wrong type when assigning to " << variableName << ".");
+ }
+ }
+ std::shared_ptr<storm::pgcl::AssignmentStatement> newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression));
+ newAssignment->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment);
+ currentLocationNumber++;
+ return newAssignment;
+ }
+
+ std::shared_ptr<storm::pgcl::AssignmentStatement> PgclParser::createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) {
+ storm::expressions::Variable variable;
+ if(!(*expressionManager).hasVariable(variableName)) {
+ variable = (*expressionManager).declareIntegerVariable(variableName);
+ this->identifiers_.add(variableName, variable.getExpression());
+ } else {
+ // In case that a declaration already happened.
+ variable = (*expressionManager).getVariable(variableName);
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of integer variable " << variableName << " which was already declared previously.");
+ }
+ std::shared_ptr<storm::pgcl::AssignmentStatement> newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression));
+ newAssignment->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment);
+ currentLocationNumber++;
+ return newAssignment;
+ }
+
+ std::shared_ptr<storm::pgcl::ObserveStatement> PgclParser::createObserveStatement(storm::pgcl::BooleanExpression const& condition) {
+ std::shared_ptr<storm::pgcl::ObserveStatement> observe(new storm::pgcl::ObserveStatement(condition));
+ this->observeCreated = true;
+ observe->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, observe);
+ currentLocationNumber++;
+ return observe;
+ }
+
+ std::shared_ptr<storm::pgcl::IfStatement> PgclParser::createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& ifBody, boost::optional<std::vector<std::shared_ptr<storm::pgcl::Statement> > > const& elseBody) {
+ std::shared_ptr<storm::pgcl::PgclProgram> ifBodyProgram(new storm::pgcl::PgclProgram(ifBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::IfStatement> ifElse;
+ if(elseBody) {
+ std::shared_ptr<storm::pgcl::PgclProgram> elseBodyProgram(new storm::pgcl::PgclProgram(*elseBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ ifElse = std::shared_ptr<storm::pgcl::IfStatement>(new storm::pgcl::IfStatement(condition, ifBodyProgram, elseBodyProgram));
+ (*(ifElse->getIfBody()->back())).setLast(true);
+ (*(ifElse->getElseBody()->back())).setLast(true);
+ // Sets the current program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = ifElse->getElseBody()->begin(); it != ifElse->getElseBody()->end(); ++it) {
+ (*it)->setParentProgram(ifElse->getElseBody());
+ (*it)->setParentStatement(ifElse);
+ }
+ for(storm::pgcl::iterator it = ifElse->getIfBody()->begin(); it != ifElse->getIfBody()->end(); ++it) {
+ (*it)->setParentProgram(ifElse->getIfBody());
+ (*it)->setParentStatement(ifElse);
+ }
+ } else {
+ ifElse = std::shared_ptr<storm::pgcl::IfStatement>(new storm::pgcl::IfStatement(condition, ifBodyProgram));
+ (*(ifElse->getIfBody()->back())).setLast(true);
+ // Sets the current program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = ifElse->getIfBody()->begin(); it != ifElse->getIfBody()->end(); ++it) {
+ (*it)->setParentProgram(ifElse->getIfBody());
+ (*it)->setParentStatement(ifElse);
+ }
+ }
+ ifElse->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, ifElse);
+ currentLocationNumber++;
+ return ifElse;
+ }
+
+ std::shared_ptr<storm::pgcl::LoopStatement> PgclParser::createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& body) {
+ std::shared_ptr<storm::pgcl::PgclProgram> bodyProgram(new storm::pgcl::PgclProgram(body, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::LoopStatement> loop(new storm::pgcl::LoopStatement(condition, bodyProgram));
+ this->loopCreated = true;
+ // Sets the current program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = loop->getBody()->begin(); it != loop->getBody()->end(); ++it) {
+ (*it)->setParentProgram(loop->getBody());
+ (*it)->setParentStatement(loop);
+ }
+ (*(loop->getBody()->back())).setLast(true);
+ loop->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, loop);
+ currentLocationNumber++;
+ return loop;
+ }
+
+ std::shared_ptr<storm::pgcl::NondeterministicBranch> PgclParser::createNondeterministicBranch(std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right) {
+ std::shared_ptr<storm::pgcl::PgclProgram> leftProgram(new storm::pgcl::PgclProgram(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::PgclProgram> rightProgram(new storm::pgcl::PgclProgram(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::NondeterministicBranch> branch(new storm::pgcl::NondeterministicBranch(leftProgram, rightProgram));
+ this->nondetCreated = true;
+ // Sets the left program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = branch->getLeftBranch()->begin(); it != branch->getLeftBranch()->end(); ++it) {
+ (*it)->setParentProgram(branch->getLeftBranch());
+ (*it)->setParentStatement(branch);
+ }
+ // Sets the right program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = branch->getRightBranch()->begin(); it != branch->getRightBranch()->end(); ++it) {
+ (*it)->setParentProgram(branch->getRightBranch());
+ (*it)->setParentStatement(branch);
+ }
+ (*(branch->getLeftBranch()->back())).setLast(true);
+ (*(branch->getRightBranch()->back())).setLast(true);
+ branch->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, branch);
+ currentLocationNumber++;
+ return branch;
+ }
+
+ std::shared_ptr<storm::pgcl::ProbabilisticBranch> PgclParser::createProbabilisticBranch(storm::expressions::Expression const& probability, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right) {
+ std::shared_ptr<storm::pgcl::PgclProgram> leftProgram(new storm::pgcl::PgclProgram(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::PgclProgram> rightProgram(new storm::pgcl::PgclProgram(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+ std::shared_ptr<storm::pgcl::ProbabilisticBranch> branch(new storm::pgcl::ProbabilisticBranch(probability, leftProgram, rightProgram));
+ // Sets the left program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = branch->getLeftBranch()->begin(); it != branch->getLeftBranch()->end(); ++it) {
+ (*it)->setParentProgram(branch->getLeftBranch());
+ (*it)->setParentStatement(branch);
+ }
+ // Sets the right program as a parent to all its children statements.
+ for(storm::pgcl::iterator it = branch->getRightBranch()->begin(); it != branch->getRightBranch()->end(); ++it) {
+ (*it)->setParentProgram(branch->getRightBranch());
+ (*it)->setParentStatement(branch);
+ }
+ (*(branch->getLeftBranch()->back())).setLast(true);
+ (*(branch->getRightBranch()->back())).setLast(true);
+ branch->setLocationNumber(this->currentLocationNumber);
+ this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, branch);
+ currentLocationNumber++;
+ return branch;
+ }
+
+ storm::pgcl::BooleanExpression PgclParser::createBooleanExpression(storm::expressions::Expression const& expression) {
+ if(expression.hasBooleanType()) {
+ storm::pgcl::BooleanExpression booleanExpression = storm::pgcl::BooleanExpression(expression);
+ return booleanExpression;
+ } else {
+ // In case that a non-boolean expression was used (e.g. (x+5)).
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Non boolean expression was used in a condition.");
+ }
+ }
+
+ storm::pgcl::UniformExpression PgclParser::createUniformExpression(int const& begin, int const& end) {
+ return storm::pgcl::UniformExpression(begin, end);
+ }
+
+ } // namespace parser
+} // namespace storm
+
diff --git a/src/parser/PgclParser.h b/src/parser/PgclParser.h
new file mode 100755
index 000000000..0ef0db7af
--- /dev/null
+++ b/src/parser/PgclParser.h
@@ -0,0 +1,154 @@
+/*
+ * File: PgclParser.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 1. April 2015, 19:12
+ */
+
+#ifndef PGCLPARSER_H
+#define PGCLPARSER_H
+
+// Includes files for file input.
+#include <fstream>
+#include <memory>
+#include <iomanip>
+// Includes files for building and parsing the PGCL program
+#include "src/parser/SpiritParserDefinitions.h"
+#include "src/parser/ExpressionParser.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/pgcl/PgclProgram.h"
+#include "src/storage/pgcl/AssignmentStatement.h"
+#include "src/storage/pgcl/BooleanExpression.h"
+#include "src/storage/pgcl/UniformExpression.h"
+#include "src/storage/pgcl/IfStatement.h"
+#include "src/storage/pgcl/LoopStatement.h"
+#include "src/storage/pgcl/NondeterministicBranch.h"
+#include "src/storage/pgcl/ObserveStatement.h"
+#include "src/storage/pgcl/ProbabilisticBranch.h"
+#include "src/storage/pgcl/Statement.h"
+
+namespace storm {
+ namespace parser {
+
+ class PgclParser : public qi::grammar<Iterator, storm::pgcl::PgclProgram(), Skipper> {
+ public:
+ /*!
+ * Parses the given file into the PGCL storage classes in case it
+ * complies with the PGCL syntax.
+ *
+ * @param filename the name of the file to parse.
+ * @return The resulting PGCL program.
+ */
+ static storm::pgcl::PgclProgram parse(std::string const& filename);
+
+ /*!
+ * Parses the given input stream into the PGCL storage classes in
+ * case it complies with the PGCL syntax.
+ *
+ * @param input The input string to parse.
+ * @param filename Name of the file from which the input was read.
+ * @return The resulting PGCL program.
+ */
+ static storm::pgcl::PgclProgram parseFromString(std::string const& input, std::string const& filename);
+ private:
+ // Internal constructor used by the parseFromString function.
+ PgclParser(std::string const& filename, Iterator first);
+ // Nonterminals (and their semantic types) of the PGCL grammar.
+ qi::rule<Iterator, storm::pgcl::PgclProgram(), Skipper> program;
+ qi::rule<Iterator, std::vector<std::shared_ptr<storm::pgcl::Statement> >(), Skipper> sequenceOfStatements;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::Statement>(), Skipper> statement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::SimpleStatement>(), Skipper> simpleStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::CompoundStatement>(), Skipper> compoundStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::IfStatement>(), Skipper> ifElseStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::BranchStatement>(), Skipper> branchStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::LoopStatement>(), Skipper> loopStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::NondeterministicBranch>(), Skipper> nondeterministicBranch;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::ProbabilisticBranch>(), Skipper> probabilisticBranch;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> assignmentStatement;
+ qi::rule<Iterator, storm::expressions::Variable(), Skipper> declaration;
+ qi::rule<Iterator, storm::expressions::Variable(), Skipper> doubleDeclaration;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> integerDeclarationStatement;
+ qi::rule<Iterator, std::shared_ptr<storm::pgcl::ObserveStatement>(), Skipper> observeStatement;
+ qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
+ qi::rule<Iterator, storm::pgcl::BooleanExpression(), Skipper> booleanCondition;
+ qi::rule<Iterator, storm::pgcl::UniformExpression(), Skipper> uniformExpression;
+ qi::rule<Iterator, std::string(), Skipper> variableName;
+ qi::rule<Iterator, std::string(), Skipper> programName;
+
+ /// Denotes the invalid identifiers, which are later passed to the expression parser.
+ struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
+ keywordsStruct() {
+ add
+ ("while", 1)
+ ("if", 2)
+ ("observe", 3)
+ ("int", 4)
+ ("function", 5);
+ }
+ };
+
+ /// Initializes the invalid identifier struct.
+ keywordsStruct invalidIdentifiers;
+ /// Is used to store the identifiers of the PGCL program that are found while parsing.
+ qi::symbols<char, storm::expressions::Expression> identifiers_;
+
+ /// Functor used for annotating entities with line number information.
+ class PositionAnnotation {
+ public:
+ typedef void result_type;
+
+ PositionAnnotation(Iterator first) : first(first) {
+ // Intentionally left empty.
+ }
+
+ template<typename Entity, typename First, typename Last>
+ result_type operator()(Entity& entity, First f, Last l) const {
+ entity.setLineNumber(get_line(f));
+ }
+ private:
+ std::string filename;
+ Iterator const first;
+ };
+
+ /// A function used for annotating the entities with their position.
+ phoenix::function<PositionAnnotation> annotate;
+
+ /// Manages the expressions and their parsing externally.
+ std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
+ storm::parser::ExpressionParser expressionParser;
+
+ /// Stores a mapping from location numbers to statements.
+ std::vector<std::shared_ptr<storm::pgcl::Statement> > locationToStatement;
+
+ /// Saves whether a loop statements was created.
+ bool loopCreated = false;
+ /// Saves whether a nondet statements was created.
+ bool nondetCreated = false;
+ /// Saves whether a observe statement was created.
+ bool observeCreated = false;
+
+ /// Stores the unique identifier of the currently parsed statement, starting at 1.
+ std::size_t currentLocationNumber = 1;
+
+ /// Sets the expression parser to a mode where it actually generates valid expressions.
+ void enableExpressions();
+
+ // Constructors for the single program parts. They just wrap the statement constructors and throw exceptions in case something unexpected was parsed.
+ storm::pgcl::PgclProgram createProgram(std::string const& programName, boost::optional<std::vector<storm::expressions::Variable> > parameters, std::vector<std::shared_ptr<storm::pgcl::Statement> > statements);
+ storm::expressions::Variable declareDoubleVariable(std::string const& variableName);
+ std::shared_ptr<storm::pgcl::AssignmentStatement> createAssignmentStatement(std::string const& variableName, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& assignedExpression);
+ std::shared_ptr<storm::pgcl::AssignmentStatement> createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
+ std::shared_ptr<storm::pgcl::ObserveStatement> createObserveStatement(storm::pgcl::BooleanExpression const& condition);
+ std::shared_ptr<storm::pgcl::IfStatement> createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& if_body, boost::optional<std::vector<std::shared_ptr<storm::pgcl::Statement> > > const& else_body);
+ std::shared_ptr<storm::pgcl::LoopStatement> createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& body);
+ std::shared_ptr<storm::pgcl::NondeterministicBranch> createNondeterministicBranch(std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right);
+ std::shared_ptr<storm::pgcl::ProbabilisticBranch> createProbabilisticBranch(storm::expressions::Expression const& probability, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right);
+ storm::pgcl::BooleanExpression createBooleanExpression(storm::expressions::Expression const& expression);
+ storm::pgcl::UniformExpression createUniformExpression(int const& begin, int const& end);
+ };
+ } // namespace parser
+} // namespace storm
+
+#endif /* PGCLPARSER_H */
+
diff --git a/src/settings/modules/PGCLSettings.cpp b/src/settings/modules/PGCLSettings.cpp
new file mode 100644
index 000000000..75e388123
--- /dev/null
+++ b/src/settings/modules/PGCLSettings.cpp
@@ -0,0 +1,41 @@
+#include "src/settings/modules/PGCLSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+ const std::string PGCLSettings::moduleName = "pgcl";
+
+ const std::string PGCLSettings::pgclFileOptionName = "pgclfile";
+ const std::string PGCLSettings::pgclFileOptionShortName = "pgcl";
+
+ PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ }
+
+ bool PGCLSettings::isPgclFileSet() const {
+ return this->getOption(pgclFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string PGCLSettings::getPgclFilename() const {
+ return this->getOption(pgclFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ void PGCLSettings::finalize() {
+
+ }
+
+ bool PGCLSettings::check() const {
+ return true;
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/settings/modules/PGCLSettings.h b/src/settings/modules/PGCLSettings.h
new file mode 100644
index 000000000..211fc8dca
--- /dev/null
+++ b/src/settings/modules/PGCLSettings.h
@@ -0,0 +1,39 @@
+#pragma once
+
+#include "storm-config.h"
+#include "src/settings/modules/ModuleSettings.h"
+
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+ class PGCLSettings : public ModuleSettings {
+ public:
+ /*!
+ * Creates a new PGCL setting
+ */
+ PGCLSettings();
+
+ /**
+ * Retrievew whether the pgcl file option was set
+ */
+ bool isPgclFileSet() const;
+
+ /**
+ * Retrieves the pgcl file name
+ */
+ std::string getPgclFilename() const;
+
+ bool check() const override;
+ void finalize() override;
+
+ static const std::string moduleName;
+
+ private:
+ static const std::string pgclFileOptionName;
+ static const std::string pgclFileOptionShortName;
+
+ };
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/AbstractStatementVisitor.h b/src/storage/pgcl/AbstractStatementVisitor.h
new file mode 100755
index 000000000..9a8cec6d1
--- /dev/null
+++ b/src/storage/pgcl/AbstractStatementVisitor.h
@@ -0,0 +1,33 @@
+//
+// Created by Lukas Westhofen on 22.04.15.
+//
+
+#ifndef STORM_ABSTRACTSTATEVISITOR_H
+#define STORM_ABSTRACTSTATEVISITOR_H
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class implements the visitor part of the visitor pattern. Every
+ * statement accepts such a visitor which then again calls the
+ * corresponding visit method of the visitor object. In such a way
+ * double dynamic dispatching can be realized. Every structure or
+ * function that requires to differentiate between concrete statement
+ * instantiations (such as if statements, assignments statements, ...)
+ * should be handled by a concrete visitor implementation.
+ */
+ class AbstractStatementVisitor {
+ public:
+ // Those functions need to be implemented for every possible
+ // statement instantiation.
+ virtual void visit(class AssignmentStatement&) = 0;
+ virtual void visit(class ObserveStatement&) = 0;
+ virtual void visit(class IfStatement&) = 0;
+ virtual void visit(class LoopStatement&) = 0;
+ virtual void visit(class NondeterministicBranch&) = 0;
+ virtual void visit(class ProbabilisticBranch&) = 0;
+ };
+ }
+}
+
+#endif //STORM_ABSTRACTSTATEVISITOR_H
diff --git a/src/storage/pgcl/AssignmentStatement.cpp b/src/storage/pgcl/AssignmentStatement.cpp
new file mode 100755
index 000000000..ba9702f8f
--- /dev/null
+++ b/src/storage/pgcl/AssignmentStatement.cpp
@@ -0,0 +1,37 @@
+/*
+ * File: AssignmentStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#include "src/storage/pgcl/AssignmentStatement.h"
+
+namespace storm {
+ namespace pgcl {
+ AssignmentStatement::AssignmentStatement(storm::expressions::Variable const& variable, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& expression) :
+ variable(variable), expression(expression) {
+ }
+
+ boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& AssignmentStatement::getExpression() {
+ return this->expression;
+ }
+
+ storm::expressions::Variable const& AssignmentStatement::getVariable() {
+ return this->variable;
+ }
+
+ void AssignmentStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+
+ std::size_t AssignmentStatement::getNumberOfOutgoingTransitions() {
+ if(this->expression.which() == 1) {
+ return boost::get<storm::pgcl::UniformExpression>(this->expression).getEnd() - boost::get<storm::pgcl::UniformExpression>(this->expression).getBegin() + 1;
+ } else {
+ return 1;
+ }
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/AssignmentStatement.h b/src/storage/pgcl/AssignmentStatement.h
new file mode 100755
index 000000000..a49b9033b
--- /dev/null
+++ b/src/storage/pgcl/AssignmentStatement.h
@@ -0,0 +1,59 @@
+/*
+ * File: AssignmentStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#ifndef ASSIGNMENTSTATEMENT_H
+#define ASSIGNMENTSTATEMENT_H
+
+#include "src/storage/pgcl/SimpleStatement.h"
+#include "src/storage/pgcl/UniformExpression.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include <boost/variant/variant.hpp>
+#include <boost/variant/get.hpp>
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents a simple assignment statement of the form
+ * identifier := expression; where the expression is either handled by
+ * the expression manager or is a uniform distribution expression.
+ */
+ class AssignmentStatement : public SimpleStatement {
+ public:
+ AssignmentStatement() = default;
+ /**
+ * Constructs an assignment statement with the variable as the left
+ * side and the expression as the right side of the assignment.
+ * @param variable The left hand variable of the assignment.
+ * @param expression The right hand expression of the assignment.
+ */
+ AssignmentStatement(storm::expressions::Variable const& variable, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& expression);
+ AssignmentStatement(const AssignmentStatement& orig) = default;
+ virtual ~AssignmentStatement() = default;
+ std::size_t getNumberOfOutgoingTransitions();
+ void accept(class AbstractStatementVisitor&);
+ /**
+ * Returns the right hand expression of the assignemnt.
+ * @return The expression of the assignment.
+ */
+ boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& getExpression();
+ /**
+ * Returns the left hand variable of the assignemnt.
+ * @return The variable to which the expression is assigned.
+ */
+ storm::expressions::Variable const& getVariable();
+ private:
+ /// Represents the variable of our assignment statement.
+ storm::expressions::Variable variable;
+ /// Represents the right hand side of our assignment statement.
+ boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> expression;
+ };
+ }
+}
+
+#endif /* ASSIGNMENTSTATEMENT_H */
+
diff --git a/src/storage/pgcl/BooleanExpression.cpp b/src/storage/pgcl/BooleanExpression.cpp
new file mode 100755
index 000000000..c60031ae9
--- /dev/null
+++ b/src/storage/pgcl/BooleanExpression.cpp
@@ -0,0 +1,22 @@
+/*
+ * File: BooleanExpression.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:44
+ */
+
+#include "src/storage/pgcl/BooleanExpression.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+ namespace pgcl {
+ BooleanExpression::BooleanExpression(storm::expressions::Expression const& booleanExpression) :
+ booleanExpression(booleanExpression) {
+ }
+
+ storm::expressions::Expression& BooleanExpression::getBooleanExpression() {
+ return this->booleanExpression;
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/BooleanExpression.h b/src/storage/pgcl/BooleanExpression.h
new file mode 100755
index 000000000..cb6241914
--- /dev/null
+++ b/src/storage/pgcl/BooleanExpression.h
@@ -0,0 +1,42 @@
+/*
+ * File: BooleanExpression.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:44
+ */
+
+#ifndef BOOLEANEXPRESSION_H
+#define BOOLEANEXPRESSION_H
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class wraps an ordinary expression but allows only for boolean
+ * expressions to be handled, e.g. expressions of the form (x < 4) or
+ * (x != y), but not (x + 5).
+ */
+ class BooleanExpression {
+ public:
+ BooleanExpression() = default;
+ /**
+ * Constructs a boolean expression if the given expression is of a
+ * boolean type. Note that it is not checked whether the expression
+ * has a boolean type.
+ * @param booleanExpression The expression of a boolean type.
+ */
+ BooleanExpression(storm::expressions::Expression const& booleanExpression);
+ /**
+ * Returns the expression.
+ * @return The expression of boolean type.
+ */
+ storm::expressions::Expression& getBooleanExpression();
+ private:
+ storm::expressions::Expression booleanExpression;
+ };
+ }
+}
+
+#endif /* BOOLEANEXPRESSION_H */
+
diff --git a/src/storage/pgcl/BranchStatement.cpp b/src/storage/pgcl/BranchStatement.cpp
new file mode 100755
index 000000000..4acd6a55a
--- /dev/null
+++ b/src/storage/pgcl/BranchStatement.cpp
@@ -0,0 +1,25 @@
+/*
+ * File: BranchStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#include "src/storage/pgcl/BranchStatement.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getLeftBranch() {
+ return this->leftBranch;
+ }
+
+ std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getRightBranch() {
+ return this->rightBranch;
+ }
+
+ std::size_t BranchStatement::getNumberOfOutgoingTransitions() {
+ return 2;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/BranchStatement.h b/src/storage/pgcl/BranchStatement.h
new file mode 100755
index 000000000..bd390e2f3
--- /dev/null
+++ b/src/storage/pgcl/BranchStatement.h
@@ -0,0 +1,46 @@
+/*
+ * File: BranchStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#ifndef BRANCHSTATEMENT_H
+#define BRANCHSTATEMENT_H
+
+#include "src/storage/pgcl/PgclProgram.h"
+#include "src/storage/pgcl/CompoundStatement.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This abstract class handles the branching statements. Every branch
+ * statement has a right and a left branch. Since branch statements are
+ * compound statements, every branch is again a complete PGCL program
+ * itself.
+ */
+ class BranchStatement : public CompoundStatement {
+ public:
+ BranchStatement() = default;
+ BranchStatement(const BranchStatement& orig) = default;
+ virtual ~BranchStatement() = default;
+ virtual void accept(class AbstractStatementVisitor&) = 0;
+ std::size_t getNumberOfOutgoingTransitions();
+ /**
+ * Returns the left branch of the statement.
+ * @return The left branch PGCL program.
+ */
+ std::shared_ptr<storm::pgcl::PgclProgram> getLeftBranch();
+ /**
+ * Returns the right branch of the statement.
+ * @return The right branch PGCL program.
+ */
+ std::shared_ptr<storm::pgcl::PgclProgram> getRightBranch();
+ protected:
+ std::shared_ptr<storm::pgcl::PgclProgram> leftBranch;
+ std::shared_ptr<storm::pgcl::PgclProgram> rightBranch;
+ };
+ }
+}
+
+#endif /* BRANCHSTATEMENT_H */
\ No newline at end of file
diff --git a/src/storage/pgcl/CompoundStatement.cpp b/src/storage/pgcl/CompoundStatement.cpp
new file mode 100755
index 000000000..c9ea40a4e
--- /dev/null
+++ b/src/storage/pgcl/CompoundStatement.cpp
@@ -0,0 +1,15 @@
+/*
+ * File: CompoundStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#include "src/storage/pgcl/CompoundStatement.h"
+
+namespace storm {
+ namespace pgcl {
+
+ }
+}
+
diff --git a/src/storage/pgcl/CompoundStatement.h b/src/storage/pgcl/CompoundStatement.h
new file mode 100755
index 000000000..bc075685c
--- /dev/null
+++ b/src/storage/pgcl/CompoundStatement.h
@@ -0,0 +1,32 @@
+/*
+ * File: CompoundStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#ifndef COMPOUNDSTATEMENT_H
+#define COMPOUNDSTATEMENT_H
+
+#include "src/storage/pgcl/Statement.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This abstract class represents compound statements. A compound
+ * statement is a statement which has again a PGCL program as a child.
+ * Examples are if and loop statements.
+ */
+ class CompoundStatement : public Statement {
+ public:
+ CompoundStatement() = default;
+ CompoundStatement(const CompoundStatement& orig) = default;
+ virtual ~CompoundStatement() = default;
+ virtual void accept(class AbstractStatementVisitor&) = 0;
+ private:
+ };
+ }
+}
+
+#endif /* COMPOUNDSTATEMENT_H */
+
diff --git a/src/storage/pgcl/IfStatement.cpp b/src/storage/pgcl/IfStatement.cpp
new file mode 100755
index 000000000..7e62a96ab
--- /dev/null
+++ b/src/storage/pgcl/IfStatement.cpp
@@ -0,0 +1,50 @@
+/*
+ * File: IfStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#include "IfStatement.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+ ifBody(body), condition(condition) {
+ }
+
+ IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody) :
+ ifBody(ifBody), elseBody(elseBody), condition(condition) {
+ this->hasElseBody = true;
+ }
+
+ std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getIfBody() {
+ return this->ifBody;
+ }
+
+ std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getElseBody() {
+ if(this->elseBody) {
+ return this->elseBody;
+ } else {
+ throw "Tried to access non-present else body of if statement.";
+ }
+ }
+
+ bool IfStatement::hasElse() {
+ return this->hasElseBody;
+ }
+
+ storm::pgcl::BooleanExpression& IfStatement::getCondition() {
+ return this->condition;
+ }
+
+ void IfStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+
+ std::size_t IfStatement::getNumberOfOutgoingTransitions() {
+ return 1;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/IfStatement.h b/src/storage/pgcl/IfStatement.h
new file mode 100755
index 000000000..515fc7ecc
--- /dev/null
+++ b/src/storage/pgcl/IfStatement.h
@@ -0,0 +1,78 @@
+/*
+ * File: IfStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#ifndef IFSTATEMENT_H
+#define IFSTATEMENT_H
+
+#include "src/storage/pgcl/CompoundStatement.h"
+#include "src/storage/pgcl/BooleanExpression.h"
+#include "src/storage/pgcl/PgclProgram.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents if statements. Any if statement has a condition
+ * which is saved as a boolean expression, and a statement body which is
+ * again a PGCL program. Thus, an if statement is a compound statement.
+ * It is possibly for if statements to have one else body, but not
+ * mandatory.
+ */
+ class IfStatement : public CompoundStatement {
+ public:
+ IfStatement() = default;
+ /**
+ * Creates an if statement which saves only an if body.
+ * @param condition The guard of the statement body.
+ * @param body The if body.
+ */
+ IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+ /**
+ * Creates an if statement with an if and an else body.
+ * @param condition The guard of the if body.
+ * @param ifBody The if body.
+ * @param elseBody The else body.
+ */
+ IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody);
+ IfStatement(const IfStatement& orig) = default;
+ virtual ~IfStatement() = default;
+ std::size_t getNumberOfOutgoingTransitions();
+ void accept(class AbstractStatementVisitor&);
+ /**
+ * Returns the if body of the if statement.
+ * @return The if body.
+ */
+ std::shared_ptr<storm::pgcl::PgclProgram> getIfBody();
+ /**
+ * Returns the else body of the if statement, if present. Otherwise
+ * it throws an excpetion.
+ * @return The else body.
+ */
+ std::shared_ptr<storm::pgcl::PgclProgram> getElseBody();
+ /**
+ * Returns true iff the if statement has an else body.
+ */
+ bool hasElse();
+ /**
+ * Returns the guard of the if statement.
+ * @return The condition.
+ */
+ storm::pgcl::BooleanExpression& getCondition();
+ private:
+ /// The if body is again a PGCL program.
+ std::shared_ptr<storm::pgcl::PgclProgram> ifBody;
+ /// The else body is again a PGCL program.
+ std::shared_ptr<storm::pgcl::PgclProgram> elseBody;
+ /// Memorizes if an else body was set. Set to false by default.
+ bool hasElseBody = false;
+ /// Saves the guard of the if statement.
+ storm::pgcl::BooleanExpression condition;
+ };
+ }
+}
+
+#endif /* IFSTATEMENT_H */
+
diff --git a/src/storage/pgcl/LoopStatement.cpp b/src/storage/pgcl/LoopStatement.cpp
new file mode 100755
index 000000000..b61b7cede
--- /dev/null
+++ b/src/storage/pgcl/LoopStatement.cpp
@@ -0,0 +1,34 @@
+/*
+ * File: LoopStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#include "src/storage/pgcl/LoopStatement.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ LoopStatement::LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+ body(body), condition(condition) {
+ }
+
+ std::shared_ptr<storm::pgcl::PgclProgram> LoopStatement::getBody() {
+ return this->body;
+ }
+
+ storm::pgcl::BooleanExpression& LoopStatement::getCondition() {
+ return this->condition;
+ }
+
+ void LoopStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+
+ std::size_t LoopStatement::getNumberOfOutgoingTransitions() {
+ return 1;
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/LoopStatement.h b/src/storage/pgcl/LoopStatement.h
new file mode 100755
index 000000000..57196021e
--- /dev/null
+++ b/src/storage/pgcl/LoopStatement.h
@@ -0,0 +1,55 @@
+/*
+ * File: LoopStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#ifndef LOOPSTATEMENT_H
+#define LOOPSTATEMENT_H
+
+#include "src/storage/pgcl/PgclProgram.h"
+#include "src/storage/pgcl/CompoundStatement.h"
+#include "src/storage/pgcl/BooleanExpression.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents a guarded loop statement. The guard is saved as
+ * a boolean expression. The body of the loop is again a PGCL program.
+ */
+ class LoopStatement : public CompoundStatement {
+ public:
+ LoopStatement() = default;
+ /**
+ * Constructs a loop statement initialized with the given condition
+ * and loop body program.
+ * @param condition The guard of the loop.
+ * @param body The body of the loop.
+ */
+ LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+ LoopStatement(const LoopStatement& orig) = default;
+ virtual ~LoopStatement() = default;
+ std::size_t getNumberOfOutgoingTransitions();
+ void accept(class AbstractStatementVisitor&);
+ /**
+ * Returns the loop body program.
+ * @return The loop body program.
+ */
+ std::shared_ptr<storm::pgcl::PgclProgram> getBody();
+ /**
+ * Returns the guard of the loop.
+ * @return The boolean condition of the loop.
+ */
+ storm::pgcl::BooleanExpression& getCondition();
+ private:
+ /// Represents the loop body.
+ std::shared_ptr<storm::pgcl::PgclProgram> body;
+ /// Represents the loop guard.
+ storm::pgcl::BooleanExpression condition;
+ };
+ }
+}
+
+#endif /* LOOPSTATEMENT_H */
+
diff --git a/src/storage/pgcl/NondeterministicBranch.cpp b/src/storage/pgcl/NondeterministicBranch.cpp
new file mode 100755
index 000000000..5080fde2e
--- /dev/null
+++ b/src/storage/pgcl/NondeterministicBranch.cpp
@@ -0,0 +1,27 @@
+/*
+ * File: NondeterministicBranch.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:44
+ */
+
+#include "src/storage/pgcl/NondeterministicBranch.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ NondeterministicBranch::NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) {
+ leftBranch = left;
+ rightBranch = right;
+ }
+
+ void NondeterministicBranch::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+
+ bool NondeterministicBranch::isNondet() {
+ return true;
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/NondeterministicBranch.h b/src/storage/pgcl/NondeterministicBranch.h
new file mode 100755
index 000000000..18b8700d5
--- /dev/null
+++ b/src/storage/pgcl/NondeterministicBranch.h
@@ -0,0 +1,39 @@
+/*
+ * File: NondeterministicBranch.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:44
+ */
+
+#ifndef NONDETERMINISTICBRANCH_H
+#define NONDETERMINISTICBRANCH_H
+
+#include "src/storage/pgcl/BranchStatement.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents a nondeterministic branch that allows for a
+ * nondeterministic path-taking between two subprograms.
+ */
+ class NondeterministicBranch : public BranchStatement {
+ public:
+ NondeterministicBranch() = default;
+ /**
+ * Constructs a nondeterministic branch initialized with the given
+ * left and right subprograms.
+ * @param left The left (first) subprogram of the branch.
+ * @param right The right (second) subprogram of the branch.
+ */
+ NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+ NondeterministicBranch(const NondeterministicBranch& orig) = default;
+ virtual ~NondeterministicBranch() = default;
+ void accept(class AbstractStatementVisitor&);
+ bool isNondet();
+ private:
+ };
+ }
+}
+
+#endif /* NONDETERMINISTICBRANCH_H */
+
diff --git a/src/storage/pgcl/ObserveStatement.cpp b/src/storage/pgcl/ObserveStatement.cpp
new file mode 100755
index 000000000..fcf4f2135
--- /dev/null
+++ b/src/storage/pgcl/ObserveStatement.cpp
@@ -0,0 +1,29 @@
+/*
+ * File: ObserveStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#include "src/storage/pgcl/ObserveStatement.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ ObserveStatement::ObserveStatement(storm::pgcl::BooleanExpression const& condition) : condition(condition) {
+ }
+
+ void ObserveStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+
+ storm::pgcl::BooleanExpression& ObserveStatement::getCondition() {
+ return this->condition;
+ }
+
+ std::size_t ObserveStatement::getNumberOfOutgoingTransitions() {
+ return 1;
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/ObserveStatement.h b/src/storage/pgcl/ObserveStatement.h
new file mode 100755
index 000000000..96461aa6a
--- /dev/null
+++ b/src/storage/pgcl/ObserveStatement.h
@@ -0,0 +1,47 @@
+/*
+ * File: ObserveStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:42
+ */
+
+#ifndef OBSERVESTATEMENT_H
+#define OBSERVESTATEMENT_H
+
+#include "src/storage/pgcl/SimpleStatement.h"
+#include "src/storage/pgcl/BooleanExpression.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents an observe statement. Observe statements
+ * include a condition. If this condition doesn't hold, the program
+ * stops at that point in its execution.
+ */
+ class ObserveStatement : public SimpleStatement {
+ public:
+ ObserveStatement() = default;
+ /**
+ * Constructs an observe statement initialized with the given
+ * condition.
+ * @param condition The condition of the observe statement.
+ */
+ ObserveStatement(storm::pgcl::BooleanExpression const& condition);
+ ObserveStatement(const ObserveStatement& orig) = default;
+ std::size_t getNumberOfOutgoingTransitions();
+ virtual ~ObserveStatement() = default;
+ /**
+ * Returns the condition of the observe statement.
+ * @return The boolean expression of the observe statement.
+ */
+ storm::pgcl::BooleanExpression& getCondition();
+ void accept(class AbstractStatementVisitor&);
+ private:
+ /// Represents the assigned condition.
+ storm::pgcl::BooleanExpression condition;
+ };
+ }
+}
+
+#endif /* OBSERVESTATEMENT_H */
+
diff --git a/src/storage/pgcl/PgclProgram.cpp b/src/storage/pgcl/PgclProgram.cpp
new file mode 100755
index 000000000..1b9d6916a
--- /dev/null
+++ b/src/storage/pgcl/PgclProgram.cpp
@@ -0,0 +1,114 @@
+/*
+ * File: PgclProgram.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:39
+ */
+
+#include "PgclProgram.h"
+#include "StatementPrinterVisitor.h"
+#include <typeinfo>
+
+namespace storm {
+ namespace pgcl {
+ PgclProgram::PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop) :
+ sequenceOfStatements(statements),
+ locationToStatement(locationToStatement),
+ parameters(parameters),
+ expressions(expressions),
+ loop(hasLoop),
+ nondet(hasNondet),
+ observe(hasObserve),
+ top(isTop) {
+ }
+
+ PgclProgram::PgclProgram(vector const &statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop) :
+ sequenceOfStatements(statements),
+ expressions(expressions),
+ loop(hasLoop),
+ nondet(hasNondet),
+ observe(hasObserve),
+ top(isTop) {
+ }
+
+ iterator PgclProgram::begin() {
+ return this->sequenceOfStatements.begin();
+ }
+
+ iterator PgclProgram::end() {
+ return this->sequenceOfStatements.end();
+ }
+
+ bool PgclProgram::empty() {
+ return this->sequenceOfStatements.empty();
+ }
+
+ element PgclProgram::front() {
+ return this->sequenceOfStatements.front();
+ }
+
+ element PgclProgram::back() {
+ return this->sequenceOfStatements.back();
+ }
+
+ unsigned long PgclProgram::size() {
+ return this->sequenceOfStatements.size();
+ }
+
+ element PgclProgram::at(size_type n) {
+ return this->sequenceOfStatements.at(n);
+ }
+
+ iterator PgclProgram::insert(iterator position, const element& statement) {
+ return this->sequenceOfStatements.insert(position, statement);
+ }
+
+ void PgclProgram::clear() {
+ this->sequenceOfStatements.clear();
+ }
+
+ std::shared_ptr<storm::expressions::ExpressionManager> PgclProgram::getExpressionManager() {
+ return this->expressions;
+ }
+
+ std::vector<storm::expressions::Variable> PgclProgram::getParameters() {
+ return this->parameters;
+ }
+
+ bool PgclProgram::hasParameters() const {
+ return !(this->parameters.empty());
+ }
+
+ bool PgclProgram::hasObserve() const {
+ return this->observe;
+ }
+
+ bool PgclProgram::hasNondet() const {
+ return this->nondet;
+ }
+
+ bool PgclProgram::hasLoop() const {
+ return this->loop;
+ }
+
+ vector PgclProgram::getLocationToStatementVector() {
+ return this->locationToStatement;
+ }
+
+ iterator PgclProgram::find(element &statement) {
+ return std::find(this->sequenceOfStatements.begin(), this->sequenceOfStatements.end(), statement);
+ }
+
+ bool PgclProgram::isTop() const {
+ return this->top;
+ }
+
+ std::ostream& operator<<(std::ostream& stream, PgclProgram& program) {
+ storm::pgcl::StatementPrinterVisitor printer(stream);
+ for(iterator statement = program.begin(); statement != program.end(); statement++) {
+ (*statement)->accept(printer);
+ }
+ return stream;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/PgclProgram.h b/src/storage/pgcl/PgclProgram.h
new file mode 100755
index 000000000..acff0c7e1
--- /dev/null
+++ b/src/storage/pgcl/PgclProgram.h
@@ -0,0 +1,170 @@
+/*
+ * File: PgclProgram.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:39
+ */
+
+#ifndef PGCLPROGRAM_H
+#define PGCLPROGRAM_H
+
+#include <vector>
+#include "src/storage/pgcl/Statement.h"
+#include "src/storage/pgcl/StatementPrinterVisitor.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+ namespace pgcl {
+
+ typedef std::shared_ptr<storm::pgcl::Statement> element;
+ typedef std::vector<element> vector;
+ typedef std::vector<element>::iterator iterator;
+ typedef std::vector<element>::const_iterator const_iterator;
+ typedef std::vector<element>::size_type size_type;
+
+ /**
+ * This class represents a complete and functional PGCL program. It
+ * contains an expression manager which keeps track of the current
+ * identifiers and variable valuations. Other than that, it basically
+ * wraps a std::vector of program statements and is intended to be used
+ * as such.
+ */
+ class PgclProgram {
+ public:
+ PgclProgram() = default;
+ /**
+ * Constructs the PGCL program with the given sequence of statements
+ * (they may contain other PGCL programs). The expression manager
+ * handles the expressions and variables of the PGCL program.
+ * @param statements The sequence of statements representing the
+ * program.
+ * @param locationToStatements A vector containing the statement
+ * with location number i at the i-th position.
+ * @param parameters The list of parameters of the program.
+ * @param expressions The manager responsible for the expressions
+ * and variables of the program.
+ * @param hasLoop Whether the program contains a loop
+ * @param hasNondet Whether the program contains a nondeterministic
+ * statement.
+ * @param hasParam Whether the program is parameterized.
+ */
+ PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop);
+ /**
+ * Does the same as the beforementioned constructor, but sets the
+ * location to statement vector to the empty vector. This
+ * constructor should be used for sub-programs, for which the
+ * location to statement relation doesn't make much sense.
+ * @param statements The sequence of statements representing the
+ * program.
+ * @param expressions The manager responsible for the expressions
+ * and variables of the program.
+ * @param hasLoop Whether the program contains a loop
+ * @param hasNondet Whether the program contains a nondeterministic
+ * statement.
+ * @param hasParam Whether the program is parameterized.
+ */
+ PgclProgram(vector const& statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop);
+ PgclProgram(const PgclProgram & orig) = default;
+ PgclProgram & operator=(PgclProgram const& other) = default;
+ iterator begin();
+ iterator end();
+ element front();
+ element back();
+ unsigned long size();
+ element at(size_type n);
+ iterator insert(iterator position, const element& statement);
+ iterator find(element& statement);
+ void clear();
+ bool empty();
+ /**
+ * Returns a vector that has the statement with location number i at
+ * its i-th position. This allows for O(1)-access of statements if
+ * only the location number is given.
+ */
+ vector getLocationToStatementVector();
+ /**
+ * Returns the list of parameters of the PGCL program.
+ */
+ std::vector<storm::expressions::Variable> getParameters();
+ /**
+ * Returns the expression manager of the PGCL program, which is
+ * responsible for managing all expressions and variables of the
+ * the program and all its subprograms.
+ * @return The expression manager of the program.
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> getExpressionManager();
+ /**
+ * Returns true if the program contains a loop statement.
+ * @return True if the program has a loop.
+ */
+ bool hasLoop() const;
+ /**
+ * Returns true if the program contains a nondeterministic
+ * statement.
+ * @return True if the program has a nondeterministic statement.
+ */
+ bool hasNondet() const;
+ /**
+ * Returns true if the program contains an observe statement.
+ * @return True if the program has an observe statement.
+ */
+ bool hasObserve() const;
+ /**
+ * Returns true if the program is parameterized.
+ * @return True if the program has at least one parameter.
+ */
+ bool hasParameters() const;
+ /**
+ * Returns whether the program is no subprogram.
+ * @return True if the program is no subprogram of another
+ * program.
+ */
+ bool isTop() const;
+ private:
+ /**
+ * We are basically wrapping a std::vector which represents the
+ * ordered single statements of the program.
+ */
+ vector sequenceOfStatements;
+ /**
+ * Contains the statement with location i at its i-th position.
+ * Imagine this as the "unrolled" sequence of statements, so the
+ * recursion is resolved here.
+ */
+ vector locationToStatement;
+ /**
+ * Stores the parameters a.k.a. free variables of the PGCL program.
+ */
+ std::vector<storm::expressions::Variable> parameters;
+ /**
+ * Handles the expressions and variables for the whole program.
+ * The expressions of every subprogram are also handled by this
+ * manager. We are using a shared pointer since all subprograms
+ * are referring to that expression manager, too.
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> expressions;
+ /**
+ * Boolean variables to save some properties of the PGCL program.
+ * They are later on used by the model builder to possibly
+ * construct simpler models (e.g. if no loops, params and nondets
+ * are used, a DTMC suffices).
+ * The values are set to true if the PGCL parser hits a loop resp.
+ * nondet resp. observe resp. parameter statement.
+ */
+ bool loop = false;
+ bool nondet = false;
+ bool observe = false;
+ bool top = false;
+ };
+ /**
+ * Prints every statement of the program along with their location
+ * numbers.
+ * @param stream The stream to print the program to.
+ * @param program The program to print.
+ */
+ std::ostream& operator<<(std::ostream& stream, PgclProgram& program);
+ }
+}
+
+#endif /* PGCLPROGRAM_H */
+
diff --git a/src/storage/pgcl/ProbabilisticBranch.cpp b/src/storage/pgcl/ProbabilisticBranch.cpp
new file mode 100755
index 000000000..795284932
--- /dev/null
+++ b/src/storage/pgcl/ProbabilisticBranch.cpp
@@ -0,0 +1,28 @@
+/*
+ * File: ProbabilisticBranch.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:43
+ */
+
+#include "src/storage/pgcl/ProbabilisticBranch.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ ProbabilisticBranch::ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) :
+ probability(probability) {
+ rightBranch = right;
+ leftBranch = left;
+ }
+
+ storm::expressions::Expression& ProbabilisticBranch::getProbability() {
+ return this->probability;
+ }
+
+ void ProbabilisticBranch::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
+ visitor.visit(*this);
+ }
+ }
+}
+
diff --git a/src/storage/pgcl/ProbabilisticBranch.h b/src/storage/pgcl/ProbabilisticBranch.h
new file mode 100755
index 000000000..669f3fb2a
--- /dev/null
+++ b/src/storage/pgcl/ProbabilisticBranch.h
@@ -0,0 +1,51 @@
+/*
+ * File: ProbabilisticBranch.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:43
+ */
+
+#ifndef PROBABILISTICBRANCH_H
+#define PROBABILISTICBRANCH_H
+
+#include "src/storage/pgcl/BranchStatement.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class represents a probabilistic branch. It branches into two
+ * subprograms. The first program is executed with the probability p
+ * given by the assigned expression, the second subprogram is executed
+ * with probability (p - 1).
+ */
+ class ProbabilisticBranch : public BranchStatement {
+ public:
+ ProbabilisticBranch() = default;
+ /**
+ * Constructs a probabilistic branch initialized with the given
+ * probability and the left (first) and right (second) subprograms.
+ * Note that no verification is made whether the probability lies
+ * between 0 and 1 is made here. This is done at runtime of the PGCL
+ * program.
+ * @param probability The expression representing the probability of the branch.
+ * @param left The left (first) subprogram of the branch.
+ * @param right The right (second) subprogram of the branch.
+ */
+ ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+ ProbabilisticBranch(const ProbabilisticBranch& orig) = default;
+ virtual ~ProbabilisticBranch() = default;
+ /**
+ * Returns the expression representing the probability.
+ * @return The expression representing the probability.
+ */
+ storm::expressions::Expression& getProbability();
+ void accept(class AbstractStatementVisitor&);
+ private:
+ /// The expression represents the probability of the branch.
+ storm::expressions::Expression probability;
+ };
+ }
+}
+
+#endif /* PROBABILISTICBRANCH_H */
+
diff --git a/src/storage/pgcl/SimpleStatement.cpp b/src/storage/pgcl/SimpleStatement.cpp
new file mode 100755
index 000000000..b628b5d90
--- /dev/null
+++ b/src/storage/pgcl/SimpleStatement.cpp
@@ -0,0 +1,15 @@
+/*
+ * File: SimpleStatement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#include "src/storage/pgcl/SimpleStatement.h"
+
+namespace storm {
+ namespace pgcl {
+
+ }
+}
+
diff --git a/src/storage/pgcl/SimpleStatement.h b/src/storage/pgcl/SimpleStatement.h
new file mode 100755
index 000000000..252bc0b64
--- /dev/null
+++ b/src/storage/pgcl/SimpleStatement.h
@@ -0,0 +1,30 @@
+/*
+ * File: SimpleStatement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#ifndef SIMPLESTATEMENT_H
+#define SIMPLESTATEMENT_H
+
+#include "src/storage/pgcl/Statement.h"
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ /*
+ * Simple statements are statements not containing other PGCL programs.
+ * Exactly one variable can be part of that statement.
+ */
+ class SimpleStatement : public Statement {
+ public:
+ SimpleStatement() = default;
+ SimpleStatement(const SimpleStatement& orig) = default;
+ virtual ~SimpleStatement() = default;
+ virtual void accept(class AbstractStatementVisitor& visitor) = 0;
+ };
+ }
+}
+#endif /* SIMPLESTATEMENT_H */
+
diff --git a/src/storage/pgcl/Statement.cpp b/src/storage/pgcl/Statement.cpp
new file mode 100755
index 000000000..25aece4d4
--- /dev/null
+++ b/src/storage/pgcl/Statement.cpp
@@ -0,0 +1,64 @@
+/*
+ * File: Statement.cpp
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#include "src/storage/pgcl/Statement.h"
+
+namespace storm {
+ namespace pgcl {
+ const bool Statement::operator==(const Statement& other) const {
+ return (other.locationNumber == this->locationNumber);
+ }
+
+ void Statement::setLineNumber(std::size_t lineNumber) {
+ this->lineNumber = lineNumber;
+ }
+
+ std::size_t Statement::getLineNumber() {
+ return this->lineNumber;
+ }
+
+ std::size_t Statement::getLocationNumber() {
+ return this->locationNumber;
+ }
+
+ void Statement::setLocationNumber(std::size_t locationNumber) {
+ this->locationNumber = locationNumber;
+ }
+
+ bool Statement::isLast() {
+ return this->last;
+ }
+
+ void Statement::setLast(bool isLast) {
+ this->last = isLast;
+ }
+
+ bool Statement::isNondet() {
+ return false;
+ }
+
+ void Statement::setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram) {
+ this->parentProgram = parentProgram;
+ }
+
+ boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > Statement::getParentProgram() {
+ return this->parentProgram;
+ }
+
+ void Statement::setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement) {
+ this->parentStatement = parentStatement;
+ }
+
+ boost::optional<std::shared_ptr<storm::pgcl::Statement> > Statement::getParentStatement() {
+ return this->parentStatement;
+ }
+
+ std::size_t Statement::getNumberOfOutgoingTransitions() {
+ return 1;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/Statement.h b/src/storage/pgcl/Statement.h
new file mode 100755
index 000000000..6afee011e
--- /dev/null
+++ b/src/storage/pgcl/Statement.h
@@ -0,0 +1,114 @@
+/*
+ * File: Statement.h
+ * Author: Lukas Westhofen
+ *
+ * Created on 11. April 2015, 17:41
+ */
+
+#ifndef STATEMENT_H
+#define STATEMENT_H
+
+#include <cstdint>
+#include <memory>
+#include "boost/optional/optional.hpp"
+
+namespace storm {
+ namespace pgcl {
+ class PgclProgram;
+ /**
+ * A PGCL program consists of various statements. Statements can again
+ * save lists of statements as their children. To make life easier, the
+ * line number where that statement was parsed is stored. Additionaly,
+ * a unique non-negative index identifier (the location number) is
+ * saved.
+ */
+ class Statement {
+ public:
+ Statement() = default;
+ Statement(const Statement& orig) = default;
+ virtual ~Statement() = default;
+ /**
+ * Returns true iff the statements are equal, thus having the same
+ * location number.
+ * @param other The other statement to check equality of.
+ * @return True iff the statements are equal.
+ */
+ const bool operator==(const Statement& other) const;
+ /**
+ * Returns the line number inside the string where the PGCL program
+ * was parsed from.
+ * @return The line number of the statement.
+ */
+ std::size_t getLineNumber();
+ /**
+ * Sets the line number during the parsing process.
+ * @param lineNumber The location number of the statement.
+ */
+ void setLineNumber(std::size_t lineNumber);
+ /**
+ * Returns the unique location number of the statement.
+ * @return The line number of the statement.
+ */
+ std::size_t getLocationNumber();
+ /**
+ * Sets the unique location number of the statement.
+ * @param lineNumber The location number of the statement.
+ */
+ void setLocationNumber(std::size_t locationNumber);
+ /**
+ * Returns true if the statement is the last of its direct parent
+ * program.
+ * @return true Whether the statement is the last statement.
+ */
+ bool isLast();
+ /**
+ * Sets the information whether the statement is the last of its
+ * direct parent program.
+ * @param isLast Whether the statement is the last statement.
+ */
+ void setLast(bool isLast);
+ /**
+ * Returns wether the statements represents nondeterminism.
+ */
+ virtual bool isNondet();
+ /**
+ * Returns the number of transitions this statement will produce.
+ */
+ virtual std::size_t getNumberOfOutgoingTransitions();
+ virtual void accept(class AbstractStatementVisitor&) = 0;
+ /**
+ * Sets the parent program of the statement.
+ * @param parentProgram The parent program of the statement.
+ */
+ void setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram);
+ /**
+ * Returns the parent program of the statement.
+ * @return The parent program of the statement.
+ */
+ boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > getParentProgram();
+ /**
+ * Sets the parent statement of the statement.
+ * @param parentProgram The parent statement of the statement.
+ */
+ void setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement);
+ /**
+ * Returns the parent statement of the statement.
+ * @return The parent statement of the statement.
+ */
+ boost::optional<std::shared_ptr<storm::pgcl::Statement> > getParentStatement();
+ protected:
+ /// The parent program of the statement.
+ boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > parentProgram;
+ /// The parent program of the statement.
+ boost::optional<std::shared_ptr<storm::pgcl::Statement> > parentStatement;
+ /// Represents the line number of the statement.
+ std::size_t lineNumber = 0;
+ /// Represents the unique statement location.
+ std::size_t locationNumber = 0;
+ /// If set to true, the statement is the last one of its (sub)program.
+ bool last = false;
+ };
+ }
+}
+#endif /* STATEMENT_H */
+
diff --git a/src/storage/pgcl/StatementPrinterVisitor.cpp b/src/storage/pgcl/StatementPrinterVisitor.cpp
new file mode 100755
index 000000000..849014578
--- /dev/null
+++ b/src/storage/pgcl/StatementPrinterVisitor.cpp
@@ -0,0 +1,97 @@
+//
+// Created by Lukas Westhofen on 21.04.15.
+//
+
+#include "src/storage/pgcl/StatementPrinterVisitor.h"
+
+#include "src/storage/pgcl/AssignmentStatement.h"
+#include "src/storage/pgcl/ObserveStatement.h"
+#include "src/storage/pgcl/IfStatement.h"
+#include "src/storage/pgcl/LoopStatement.h"
+#include "src/storage/pgcl/NondeterministicBranch.h"
+#include "src/storage/pgcl/ProbabilisticBranch.h"
+
+namespace storm {
+ namespace pgcl {
+ StatementPrinterVisitor::StatementPrinterVisitor(std::ostream &stream) : stream(stream) {
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::AssignmentStatement& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ if(statement.getExpression().which() == 0) {
+ storm::expressions::Expression const& expression = boost::get<storm::expressions::Expression>(statement.getExpression());
+ this->stream << statement.getVariable().getType() << " " << statement.getVariable().getName() << " := " << expression << ";" << std::endl;
+ } else {
+ storm::pgcl::UniformExpression const& unif = boost::get<storm::pgcl::UniformExpression>(statement.getExpression());
+ this->stream << statement.getVariable().getType() << " " << statement.getVariable().getName() << " := " << "unif(" << unif.getBegin() << ", " << unif.getEnd() << ");" << std::endl;
+ }
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::ObserveStatement& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ this->stream << "observe(" << statement.getCondition().getBooleanExpression() << ");" << std::endl;
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::IfStatement& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ this->stream << "if(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
+ int i = 1;
+ for(iterator it = (*(statement.getIfBody())).begin(); it != (*(statement.getIfBody())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "}" << std::endl;
+ if(statement.hasElse()) {
+ this->stream << "else {" << std::endl;
+ for(iterator it = (*(statement.getElseBody())).begin(); it != (*(statement.getElseBody())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "}" << std::endl;
+ }
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::LoopStatement& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ this->stream << "while(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
+ int i = 1;
+ for(iterator it = (*(statement.getBody())).begin(); it != (*(statement.getBody())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "}" << std::endl;
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::NondeterministicBranch& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ this->stream << "{" << std::endl;
+ int i = 1;
+ for(iterator it = (*(statement.getLeftBranch())).begin(); it != (*(statement.getLeftBranch())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "} [] {" << std::endl;
+ for(iterator it = (*(statement.getRightBranch())).begin(); it != (*(statement.getRightBranch())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "}" << std::endl;
+ }
+
+ void StatementPrinterVisitor::visit(storm::pgcl::ProbabilisticBranch& statement) {
+ this->stream << statement.getLocationNumber() << ": ";
+ this->stream << "{" << std::endl;
+ int i = 1;
+ for(iterator it = (*(statement.getLeftBranch())).begin(); it != (*(statement.getLeftBranch())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "} [" << statement.getProbability() << "] {" << std::endl;
+ for(iterator it = (*(statement.getRightBranch())).begin(); it != (*(statement.getRightBranch())).end(); ++it) {
+ (*(*it)).accept(*this);
+ i++;
+ }
+ this->stream << "}" << std::endl;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/StatementPrinterVisitor.h b/src/storage/pgcl/StatementPrinterVisitor.h
new file mode 100755
index 000000000..6e3ac9cc6
--- /dev/null
+++ b/src/storage/pgcl/StatementPrinterVisitor.h
@@ -0,0 +1,39 @@
+//
+// Created by Lukas Westhofen on 21.04.15.
+//
+
+#ifndef STORM_STATEMENTVISITOR_H
+#define STORM_STATEMENTVISITOR_H
+
+#include <iostream>
+#include <boost/variant/get.hpp>
+#include "src/storage/pgcl/AbstractStatementVisitor.h"
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This is a sample implementation of a concrete visitor which interface
+ * is defined in AbstractStatementVisitor.h. It prints out various
+ * details of the given statements when the visit method is called.
+ */
+ class StatementPrinterVisitor : public AbstractStatementVisitor {
+ public:
+ /**
+ * Constructs a statement printer which prints its output to the
+ * given stream.
+ * @param stream The stream to print to.
+ */
+ StatementPrinterVisitor(std::ostream& stream);
+ void visit(class AssignmentStatement&);
+ void visit(class ObserveStatement&);
+ void visit(class IfStatement&);
+ void visit(class LoopStatement&);
+ void visit(class NondeterministicBranch&);
+ void visit(class ProbabilisticBranch&);
+ private:
+ std::ostream& stream;
+ };
+ }
+}
+
+#endif //STORM_STATEMENTVISITOR_H
diff --git a/src/storage/pgcl/UniformExpression.cpp b/src/storage/pgcl/UniformExpression.cpp
new file mode 100644
index 000000000..a2c664454
--- /dev/null
+++ b/src/storage/pgcl/UniformExpression.cpp
@@ -0,0 +1,23 @@
+//
+// Created by foxnbk on 16.03.16.
+//
+
+#include "UniformExpression.h"
+
+namespace storm {
+ namespace pgcl {
+ UniformExpression::UniformExpression(int_fast64_t begin, int_fast64_t end) : begin(begin), end(end) {
+ // Intentionally left empty.
+ }
+
+ int_fast64_t UniformExpression::getBegin() const {
+ return this->begin;
+ }
+
+ int_fast64_t UniformExpression::getEnd() const {
+ return this->end;
+ }
+ }
+}
+
+#include "UniformExpression.h"
diff --git a/src/storage/pgcl/UniformExpression.h b/src/storage/pgcl/UniformExpression.h
new file mode 100644
index 000000000..f593f4631
--- /dev/null
+++ b/src/storage/pgcl/UniformExpression.h
@@ -0,0 +1,43 @@
+//
+// Created by Lukas Westhofen on 16.03.16.
+//
+
+#ifndef STORM_UNIFORMEXPRESSION_H
+#define STORM_UNIFORMEXPRESSION_H
+
+#include <stdint.h>
+
+namespace storm {
+ namespace pgcl {
+ /**
+ * This class wraps a uniform distribution expression of the form
+ * unif(k,l) where k <= l are both integers.
+ */
+ class UniformExpression {
+ public:
+ UniformExpression() = default;
+ /**
+ * Constructs a uniform expression with the given beginning and
+ * end.
+ * @param begin The begin of the uniform distribution.
+ * @param begin The end of the uniform distribution.
+ */
+ UniformExpression(int_fast64_t begin, int_fast64_t end);
+ /**
+ * Returns the begin of the uniform distribution.
+ * @return The begin of the uniform distribution.
+ */
+ int_fast64_t getBegin() const;
+ /**
+ * Returns the end of the uniform distribution.
+ * @return The end of the uniform distribution.
+ */
+ int_fast64_t getEnd() const;
+ private:
+ int_fast64_t begin = 0;
+ int_fast64_t end = 0;
+ };
+ }
+}
+
+#endif //STORM_UNIFORMEXPRESSION_H
diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp
new file mode 100644
index 000000000..c756c5636
--- /dev/null
+++ b/src/storm-pgcl.cpp
@@ -0,0 +1,74 @@
+#include "src/parser/PgclParser.h"
+
+#include "logic/Formula.h"
+#include "utility/initialize.h"
+#include "utility/storm.h"
+#include "src/cli/cli.h"
+#include "src/exceptions/BaseException.h"
+#include "src/utility/macros.h"
+#include <boost/lexical_cast.hpp>
+
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/modules/PGCLSettings.h"
+#include "src/settings/modules/CoreSettings.h"
+#include "src/settings/modules/DebugSettings.h"
+//#include "src/settings/modules/CounterexampleGeneratorSettings.h"
+//#include "src/settings/modules/CuddSettings.h"
+//#include "src/settings/modules/SylvanSettings.h"
+#include "src/settings/modules/GmmxxEquationSolverSettings.h"
+#include "src/settings/modules/NativeEquationSolverSettings.h"
+//#include "src/settings/modules/BisimulationSettings.h"
+//#include "src/settings/modules/GlpkSettings.h"
+//#include "src/settings/modules/GurobiSettings.h"
+//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+//#include "src/settings/modules/ParametricSettings.h"
+#include "src/settings/modules/EliminationSettings.h"
+
+/*!
+ * Initialize the settings manager.
+ */
+void initializeSettings() {
+ storm::settings::mutableManager().setName("StoRM-PGCL", "storm-pgcl");
+
+ // Register all known settings modules.
+ storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+ storm::settings::addModule<storm::settings::modules::PGCLSettings>();
+ storm::settings::addModule<storm::settings::modules::CoreSettings>();
+ storm::settings::addModule<storm::settings::modules::DebugSettings>();
+ //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+ //storm::settings::addModule<storm::settings::modules::CuddSettings>();
+ //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
+ storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+ //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+ //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
+ //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
+ //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
+ //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
+ storm::settings::addModule<storm::settings::modules::EliminationSettings>();
+}
+
+int main(const int argc, const char** argv) {
+ try {
+ storm::utility::setUp();
+ storm::cli::printHeader("StoRM-PGCL", argc, argv);
+ initializeSettings();
+
+ bool optionsCorrect = storm::cli::parseOptions(argc, argv);
+ if (!optionsCorrect) {
+ return -1;
+ }
+
+ if(storm::settings::getModule<storm::settings::modules::PGCLSettings>().isPgclFileSet()) {
+ storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getPgclFilename());
+ std::cout << prog << std::endl;
+ }
+
+
+
+ }catch (storm::exceptions::BaseException const& exception) {
+ STORM_LOG_ERROR("An exception caused StoRM-PGCL to terminate. The message of the exception is: " << exception.what());
+ } catch (std::exception const& exception) {
+ STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-PGCL to terminate. The message of this exception is: " << exception.what());
+ }
+}
\ No newline at end of file