pgcl

Former-commit-id: 63d52fc706 [formerly 90b7939792]
Former-commit-id: 04e29e8c41

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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;
+		}
+	}
+}

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);
+}

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;
+	}
+}

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);
+}

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;
+	}
+}

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;
+	}
+}

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);
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+	}
+}

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;
+
+		} } }
+
+	}
+
+}
+

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;}}}
+
+	}
+}

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})
 
 

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
+

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 */
+

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;
+            }
+        }
+    }
+}

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;
+                
+            };
+        }
+    }
+}

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

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;
+            }
+        }
+    }
+}
+

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 */
+

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;
+        }
+    }
+}
+

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 */
+

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;
+        }
+    }
+}

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 */

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 {
+
+    }
+}
+

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 */
+

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;
+        }
+    }
+}

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 */
+

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;
+        }
+    }
+}
+

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 */
+

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;
+        }
+    }
+}
+

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 */
+

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;
+        }
+    }
+}
+

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 */
+

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;
+        }
+    }
+}

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 */
+

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);
+        }
+    }
+}
+

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 */
+

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 {
+
+    }
+}
+

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 */
+

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;
+        }
+    }
+}

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 */
+

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;
+        }
+    }
+}

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

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"

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

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());
+    }
+}