Mitschnitt der Eingaben und Ausgaben auf marvin.cs.tu-dortmund.de laut Uebungsblatt 7. Die mit -bash-3.00$ markierten Stellen sind die Eingaben :-) ---------------------------------------------------------------------------------------- -bash-3.00$ cd examples/App_C -bash-3.00$ ls ex1 ex2 petrinet1 petrinet2 -bash-3.00$ more petrinet1 #define Place byte /* < 256 tokens per place */ Place p1, p2, p3; Place p4, p5, p6; #define inp1(x) (x>0) -> x-- #define inp2(x,y) (x>0&&y>0) -> x--; y-- #define out1(x) x++ #define out2(x,y) x++; y++ init { p1 = 1; p4 = 1; /* initial marking */ do /*t1*/ :: atomic { inp1(p1) -> out1(p2) } /*t2*/ :: atomic { inp2(p2,p4) -> out1(p3) } /*t3*/ :: atomic { inp1(p3) -> out2(p1,p4) } /*t4*/ :: atomic { inp1(p4) -> out1(p5) } /*t5*/ :: atomic { inp2(p1,p5) -> out1(p6) } /*t6*/ :: atomic { inp1(p6) -> out2(p4,p1) } od } -bash-3.00$ spin -v petrinet1 Starting :init: with pid 0 1: proc 0 (:init:) line 13 "petrinet1" (state 1) [p1 = 1] 2: proc 0 (:init:) line 13 "petrinet1" (state 2) [p4 = 1] 3: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 4: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p4>0))] 5: proc 0 (:init:) line 18 "petrinet1" (state 18) [p4 = (p4-1)] 6: proc 0 (:init:) line 18 "petrinet1" (state 19) [p5 = (p5+1)] 7: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 8: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p1>0)&&(p5>0)))] 9: proc 0 (:init:) line 19 "petrinet1" (state 22) [p1 = (p1-1)] 10: proc 0 (:init:) line 19 "petrinet1" (state 23) [p5 = (p5-1)] 11: proc 0 (:init:) line 19 "petrinet1" (state 24) [p6 = (p6+1)] 12: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 13: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p6>0))] 14: proc 0 (:init:) line 20 "petrinet1" (state 27) [p6 = (p6-1)] 15: proc 0 (:init:) line 20 "petrinet1" (state 28) [p4 = (p4+1)] 16: proc 0 (:init:) line 20 "petrinet1" (state 29) [p1 = (p1+1)] 17: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 18: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p4>0))] 19: proc 0 (:init:) line 18 "petrinet1" (state 18) [p4 = (p4-1)] 20: proc 0 (:init:) line 18 "petrinet1" (state 19) [p5 = (p5+1)] 21: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 22: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p1>0)&&(p5>0)))] 23: proc 0 (:init:) line 19 "petrinet1" (state 22) [p1 = (p1-1)] 24: proc 0 (:init:) line 19 "petrinet1" (state 23) [p5 = (p5-1)] 25: proc 0 (:init:) line 19 "petrinet1" (state 24) [p6 = (p6+1)] 26: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 27: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p6>0))] 28: proc 0 (:init:) line 20 "petrinet1" (state 27) [p6 = (p6-1)] 29: proc 0 (:init:) line 20 "petrinet1" (state 28) [p4 = (p4+1)] 30: proc 0 (:init:) line 20 "petrinet1" (state 29) [p1 = (p1+1)] 31: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 32: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p4>0))] 33: proc 0 (:init:) line 18 "petrinet1" (state 18) [p4 = (p4-1)] 34: proc 0 (:init:) line 18 "petrinet1" (state 19) [p5 = (p5+1)] 35: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 36: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p1>0)&&(p5>0)))] 37: proc 0 (:init:) line 19 "petrinet1" (state 22) [p1 = (p1-1)] 38: proc 0 (:init:) line 19 "petrinet1" (state 23) [p5 = (p5-1)] 39: proc 0 (:init:) line 19 "petrinet1" (state 24) [p6 = (p6+1)] 40: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 41: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p6>0))] 42: proc 0 (:init:) line 20 "petrinet1" (state 27) [p6 = (p6-1)] 43: proc 0 (:init:) line 20 "petrinet1" (state 28) [p4 = (p4+1)] 44: proc 0 (:init:) line 20 "petrinet1" (state 29) [p1 = (p1+1)] 45: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 46: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p1>0))] 47: proc 0 (:init:) line 15 "petrinet1" (state 4) [p1 = (p1-1)] 48: proc 0 (:init:) line 15 "petrinet1" (state 5) [p2 = (p2+1)] 49: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 50: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p2>0)&&(p4>0)))] 51: proc 0 (:init:) line 16 "petrinet1" (state 8) [p2 = (p2-1)] 52: proc 0 (:init:) line 16 "petrinet1" (state 9) [p4 = (p4-1)] 53: proc 0 (:init:) line 16 "petrinet1" (state 10) [p3 = (p3+1)] 54: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 55: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p3>0))] 56: proc 0 (:init:) line 17 "petrinet1" (state 13) [p3 = (p3-1)] 57: proc 0 (:init:) line 17 "petrinet1" (state 14) [p1 = (p1+1)] 58: proc 0 (:init:) line 17 "petrinet1" (state 15) [p4 = (p4+1)] 59: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 60: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p1>0))] 61: proc 0 (:init:) line 15 "petrinet1" (state 4) [p1 = (p1-1)] 62: proc 0 (:init:) line 15 "petrinet1" (state 5) [p2 = (p2+1)] 63: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 64: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p2>0)&&(p4>0)))] 65: proc 0 (:init:) line 16 "petrinet1" (state 8) [p2 = (p2-1)] 66: proc 0 (:init:) line 16 "petrinet1" (state 9) [p4 = (p4-1)] 67: proc 0 (:init:) line 16 "petrinet1" (state 10) [p3 = (p3+1)] 68: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 69: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p3>0))] 70: proc 0 (:init:) line 17 "petrinet1" (state 13) [p3 = (p3-1)] 71: proc 0 (:init:) line 17 "petrinet1" (state 14) [p1 = (p1+1)] 72: proc 0 (:init:) line 17 "petrinet1" (state 15) [p4 = (p4+1)] 73: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 74: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p1>0))] 75: proc 0 (:init:) line 15 "petrinet1" (state 4) [p1 = (p1-1)] 76: proc 0 (:init:) line 15 "petrinet1" (state 5) [p2 = (p2+1)] 77: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 78: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p2>0)&&(p4>0)))] 79: proc 0 (:init:) line 16 "petrinet1" (state 8) [p2 = (p2-1)] 80: proc 0 (:init:) line 16 "petrinet1" (state 9) [p4 = (p4-1)] 81: proc 0 (:init:) line 16 "petrinet1" (state 10) [p3 = (p3+1)] 82: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 83: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p3>0))] 84: proc 0 (:init:) line 17 "petrinet1" (state 13) [p3 = (p3-1)] 85: proc 0 (:init:) line 17 "petrinet1" (state 14) [p1 = (p1+1)] 86: proc 0 (:init:) line 17 "petrinet1" (state 15) [p4 = (p4+1)] 87: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 88: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p4>0))] 89: proc 0 (:init:) line 18 "petrinet1" (state 18) [p4 = (p4-1)] 90: proc 0 (:init:) line 18 "petrinet1" (state 19) [p5 = (p5+1)] 91: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 92: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p1>0)&&(p5>0)))] 93: proc 0 (:init:) line 19 "petrinet1" (state 22) [p1 = (p1-1)] 94: proc 0 (:init:) line 19 "petrinet1" (state 23) [p5 = (p5-1)] 95: proc 0 (:init:) line 19 "petrinet1" (state 24) [p6 = (p6+1)] 96: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 97: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p6>0))] 98: proc 0 (:init:) line 20 "petrinet1" (state 27) [p6 = (p6-1)] 99: proc 0 (:init:) line 20 "petrinet1" (state 28) [p4 = (p4+1)] 100: proc 0 (:init:) line 20 "petrinet1" (state 29) [p1 = (p1+1)] 101: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 102: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p1>0))] 103: proc 0 (:init:) line 15 "petrinet1" (state 4) [p1 = (p1-1)] 104: proc 0 (:init:) line 15 "petrinet1" (state 5) [p2 = (p2+1)] 105: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 106: proc 0 (:init:) line 14 "petrinet1" (state 31) [(((p2>0)&&(p4>0)))] 107: proc 0 (:init:) line 16 "petrinet1" (state 8) [p2 = (p2-1)] 108: proc 0 (:init:) line 16 "petrinet1" (state 9) [p4 = (p4-1)] 109: proc 0 (:init:) line 16 "petrinet1" (state 10) [p3 = (p3+1)] 110: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 111: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p3>0))] 112: proc 0 (:init:) line 17 "petrinet1" (state 13) [p3 = (p3-1)] 113: proc 0 (:init:) line 17 "petrinet1" (state 14) [p1 = (p1+1)] 114: proc 0 (:init:) line 17 "petrinet1" (state 15) [p4 = (p4+1)] 115: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 116: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p4>0))] 117: proc 0 (:init:) line 18 "petrinet1" (state 18) [p4 = (p4-1)] 118: proc 0 (:init:) line 18 "petrinet1" (state 19) [p5 = (p5+1)] 119: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] 120: proc 0 (:init:) line 14 "petrinet1" (state 31) [((p1>0))] 121: proc 0 (:init:) line 15 "petrinet1" (state 4) [p1 = (p1-1)] 122: proc 0 (:init:) line 15 "petrinet1" (state 5) [p2 = (p2+1)] 123: proc 0 (:init:) line 22 "petrinet1" (state 32) [.(goto)] timeout #processes: 1 p1 = 0 p2 = 1 p3 = 0 p4 = 0 p5 = 1 p6 = 0 123: proc 0 (:init:) line 14 "petrinet1" (state 31) 1 process created -bash-3.00$ more petrinet2 #define Place byte Place P1, P2, P4, P5, RC, CC, RD, CD; Place p1, p2, p4, p5, rc, cc, rd, cd; #define inp1(x) (x>0) -> x-- #define inp2(x,y) (x>0&&y>0) -> x--; y-- #define out1(x) x++ #define out2(x,y) x++; y++ init { P1 = 1; p1 = 1; /* initial marking */ do :: atomic { inp1(P1) -> out2(rc,P2) } :: atomic { inp2(P2,CC) -> out1(P4) } :: atomic { inp1(P4) -> out2(P5,rd) } :: atomic { inp2(P5,CD) -> out1(P1) } :: atomic { inp2(P1,RC) -> out2(P4,cc) } :: atomic { inp2(P4,RD) -> out2(P1,cd) } :: atomic { inp2(P5,RD) -> out1(P1) } :: atomic { inp1(p1) -> out2(RC,p2) } :: atomic { inp2(p2,cc) -> out1(p4) } :: atomic { inp1(p4) -> out2(p5,RD) } :: atomic { inp2(p5,cd) -> out1(p1) } :: atomic { inp2(p1,rc) -> out2(p4,CC) } :: atomic { inp2(p4,rd) -> out2(p1,CD) } :: atomic { inp2(p5,rd) -> out1(p1) } od } -bash-3.00$ spin -v petrinet2 Starting :init: with pid 0 1: proc 0 (:init:) line 12 "petrinet2" (state 1) [P1 = 1] 2: proc 0 (:init:) line 12 "petrinet2" (state 2) [p1 = 1] 3: proc 0 (:init:) line 30 "petrinet2" (state 78) [.(goto)] 4: proc 0 (:init:) line 13 "petrinet2" (state 77) [((P1>0))] 5: proc 0 (:init:) line 14 "petrinet2" (state 4) [P1 = (P1-1)] 6: proc 0 (:init:) line 14 "petrinet2" (state 5) [rc = (rc+1)] 7: proc 0 (:init:) line 14 "petrinet2" (state 6) [P2 = (P2+1)] 8: proc 0 (:init:) line 30 "petrinet2" (state 78) [.(goto)] 9: proc 0 (:init:) line 13 "petrinet2" (state 77) [((p1>0))] 10: proc 0 (:init:) line 22 "petrinet2" (state 41) [p1 = (p1-1)] 11: proc 0 (:init:) line 22 "petrinet2" (state 42) [RC = (RC+1)] 12: proc 0 (:init:) line 22 "petrinet2" (state 43) [p2 = (p2+1)] 13: proc 0 (:init:) line 30 "petrinet2" (state 78) [.(goto)] timeout #processes: 1 P1 = 0 P2 = 1 P4 = 0 P5 = 0 RC = 1 CC = 0 RD = 0 CD = 0 p1 = 0 p2 = 1 p4 = 0 p5 = 0 rc = 1 cc = 0 rd = 0 cd = 0 13: proc 0 (:init:) line 13 "petrinet2" (state 77) 1 process created