sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

moved pgcl to own example repo 

Former-commit-id: 97dbffbf94 [formerly e020a1148b]
Former-commit-id: 310b7dd18d
tempestpy_adaptions
sjunges 8 years ago
parent
cb8189d171
commit
277d70bc16
42 changed files with 0 additions and 2658 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 58
      examples/pgcl/coupon/coupon10-classic.pgcl
  2. 60
      examples/pgcl/coupon/coupon10-cost.pgcl
  3. 62
      examples/pgcl/coupon/coupon10-observe.pgcl
  4. 60
      examples/pgcl/coupon/coupon10.pgcl
  5. 24
      examples/pgcl/coupon/coupon3-classic.pgcl
  6. 28
      examples/pgcl/coupon/coupon3-cost.pgcl
  7. 30
      examples/pgcl/coupon/coupon3-observe.pgcl
  8. 28
      examples/pgcl/coupon/coupon3.pgcl
  9. 34
      examples/pgcl/coupon/coupon4-observe.pgcl
  10. 32
      examples/pgcl/coupon/coupon5-classic.pgcl
  11. 36
      examples/pgcl/coupon/coupon5-cost.pgcl
  12. 38
      examples/pgcl/coupon/coupon5-observe.pgcl
  13. 36
      examples/pgcl/coupon/coupon5.pgcl
  14. 40
      examples/pgcl/coupon/coupon7-classic.pgcl
  15. 44
      examples/pgcl/coupon/coupon7-cost.pgcl
  16. 46
      examples/pgcl/coupon/coupon7-observe.pgcl
  17. 44
      examples/pgcl/coupon/coupon7.pgcl
  18. 35
      examples/pgcl/crowds/crowds100-100-observeOther.pgcl
  19. 34
      examples/pgcl/crowds/crowds100-100.pgcl
  20. 35
      examples/pgcl/crowds/crowds100-60-observeOther.pgcl
  21. 34
      examples/pgcl/crowds/crowds100-60-param.pgcl
  22. 34
      examples/pgcl/crowds/crowds100-60.pgcl
  23. 36
      examples/pgcl/crowds/crowds100-80-observeOther.pgcl
  24. 34
      examples/pgcl/crowds/crowds100-80.pgcl
  25. 34
      examples/pgcl/crowds/crowds3-3-param.pgcl
  26. 34
      examples/pgcl/crowds/crowds3-3.pgcl
  27. 33
      examples/pgcl/crowds/crowds3-5-param.pgcl
  28. 34
      examples/pgcl/crowds/crowds3-5.pgcl
  29. 34
      examples/pgcl/crowds/crowds5-20-param.pgcl
  30. 34
      examples/pgcl/crowds/crowds5-20.pgcl
  31. 108
      examples/pgcl/herman/herman10-det.pgcl
  32. 108
      examples/pgcl/herman/herman10.pgcl
  33. 138
      examples/pgcl/herman/herman13-det.pgcl
  34. 138
      examples/pgcl/herman/herman13.pgcl
  35. 178
      examples/pgcl/herman/herman17-det.pgcl
  36. 178
      examples/pgcl/herman/herman17.pgcl
  37. 218
      examples/pgcl/herman/herman21-det.pgcl
  38. 218
      examples/pgcl/herman/herman21.pgcl
  39. 77
      examples/pgcl/herman/herman7-det.pgcl
  40. 77
      examples/pgcl/herman/herman7.pgcl
  41. 49
      examples/pgcl/lotkavolterra.pgcl
  42. 26
      examples/pgcl/robot.pgcl

58
examples/pgcl/coupon/coupon10-classic.pgcl
View File

@ -1,58 +0,0 @@
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;
}
}
}

60
examples/pgcl/coupon/coupon10-cost.pgcl
View File

@ -1,60 +0,0 @@
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;
}
}
}

62
examples/pgcl/coupon/coupon10-observe.pgcl
View File

@ -1,62 +0,0 @@
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;
}
}
}

60
examples/pgcl/coupon/coupon10.pgcl
View File

@ -1,60 +0,0 @@
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;
}
}
}

24
examples/pgcl/coupon/coupon3-classic.pgcl
View File

@ -1,24 +0,0 @@
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;
}
}
}

28
examples/pgcl/coupon/coupon3-cost.pgcl
View File

@ -1,28 +0,0 @@
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;
}
}
}

30
examples/pgcl/coupon/coupon3-observe.pgcl
View File

@ -1,30 +0,0 @@
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;
}
}
}

28
examples/pgcl/coupon/coupon3.pgcl
View File

@ -1,28 +0,0 @@
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;
}
}
}

34
examples/pgcl/coupon/coupon4-observe.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}
}

32
examples/pgcl/coupon/coupon5-classic.pgcl
View File

@ -1,32 +0,0 @@
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;
}
}
}

36
examples/pgcl/coupon/coupon5-cost.pgcl
View File

@ -1,36 +0,0 @@
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;
}
}
}

38
examples/pgcl/coupon/coupon5-observe.pgcl
View File

@ -1,38 +0,0 @@
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;
}
}
}

36
examples/pgcl/coupon/coupon5.pgcl
View File

@ -1,36 +0,0 @@
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;
}
}
}

40
examples/pgcl/coupon/coupon7-classic.pgcl
View File

@ -1,40 +0,0 @@
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;
}
}
}

44
examples/pgcl/coupon/coupon7-cost.pgcl
View File

@ -1,44 +0,0 @@
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;
}
}
}

46
examples/pgcl/coupon/coupon7-observe.pgcl
View File

@ -1,46 +0,0 @@
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;
}
}
}

44
examples/pgcl/coupon/coupon7.pgcl
View File

@ -1,44 +0,0 @@
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;
}
}
}

35
examples/pgcl/crowds/crowds100-100-observeOther.pgcl
View File

@ -1,35 +0,0 @@
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);
}

34
examples/pgcl/crowds/crowds100-100.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

35
examples/pgcl/crowds/crowds100-60-observeOther.pgcl
View File

@ -1,35 +0,0 @@
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);
}

34
examples/pgcl/crowds/crowds100-60-param.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds100-60.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

36
examples/pgcl/crowds/crowds100-80-observeOther.pgcl
View File

@ -1,36 +0,0 @@
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);
}

34
examples/pgcl/crowds/crowds100-80.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds3-3-param.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds3-3.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

33
examples/pgcl/crowds/crowds3-5-param.pgcl
View File

@ -1,33 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds3-5.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds5-20-param.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

34
examples/pgcl/crowds/crowds5-20.pgcl
View File

@ -1,34 +0,0 @@
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;
}
}

108
examples/pgcl/herman/herman10-det.pgcl
View File

@ -1,108 +0,0 @@
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;
}
}

108
examples/pgcl/herman/herman10.pgcl
View File

@ -1,108 +0,0 @@
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;
}
}

138
examples/pgcl/herman/herman13-det.pgcl
View File

@ -1,138 +0,0 @@
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;
}
}

138
examples/pgcl/herman/herman13.pgcl
View File

@ -1,138 +0,0 @@
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;
}
}

178
examples/pgcl/herman/herman17-det.pgcl
View File

@ -1,178 +0,0 @@
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;
}
}

178
examples/pgcl/herman/herman17.pgcl
View File

@ -1,178 +0,0 @@
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;
}
}

218
examples/pgcl/herman/herman21-det.pgcl
View File

@ -1,218 +0,0 @@
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;
}
}

218
examples/pgcl/herman/herman21.pgcl
View File

@ -1,218 +0,0 @@
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;
}
}

77
examples/pgcl/herman/herman7-det.pgcl
View File

@ -1,77 +0,0 @@
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;
}
}

77
examples/pgcl/herman/herman7.pgcl
View File

@ -1,77 +0,0 @@
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;
}
}

49
examples/pgcl/lotkavolterra.pgcl
View File

@ -1,49 +0,0 @@
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;
} } }
}
}

26
examples/pgcl/robot.pgcl
View File

@ -1,26 +0,0 @@
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;}}}
}
}
Write Preview
Loading…
Cancel
Save