Re: ARC model specified in spinroot/promela
- In reply to: Mathew\, Cherry G.*: "Re: ARC model specified in spinroot/promela"
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 02 Sep 2023 17:17:52 UTC
Am 2023-09-02 12:47, schrieb Mathew, Cherry G.*:
> 4) Print trace from debug trail: make spin-trace
(207) root@ttypts/1 # make spin-trace
spin -t spinmodel.pml -p -g # -p (statements) -g (globals) -l (locals)
-s (send) -r (recv)
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5))
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) &&
((len(B2.item_list)<=5))))) && (<> ((p>0)))
Never claim moves to line 5 [(!((p>0)))]
Never claim moves to line 15 [(!((p>0)))]
<<<<<START OF CYCLE>>>>>
spin: trail ends after 272 steps
#processes: 0
queue 2 (item_list):
queue 4 (item_list):
queue 1 (item_list): [1]
queue 3 (item_list): [5][4][3][2]
_x[0].iid = 0
_x[0].cached = 0
_x[1].iid = 1
_x[1].cached = 0
_x[2].iid = 2
_x[2].cached = 0
_x[3].iid = 3
_x[3].cached = 0
_x[4].iid = 4
_x[4].cached = 0
_x[5].iid = 5
_x[5].cached = 0
_x_iid = 6
_item_rep = 5
LRUitem.iid = 0
LRUitem.cached = 0
d1 = 0
d2 = 0
p = 0
sc_lock = 0
272: proc - (ltl_0:1) _spin_nvr.tmp:14 (state 22)
16 processes created
./pan -r spinmodel.pml.trail -g
MSC: ~G 3
1: proc 0 (ltl_0) spinmodel.pml:3 (state 12) [(!((p>0)))]
2: proc 1 (:init:) spinmodel.pml:79 (state 21) [x_iid = 0]
3: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
4: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
5: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
6: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
7: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
8: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
9: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
10: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
11: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
12: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
13: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
14: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
15: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
16: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
17: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
18: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
19: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
20: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
21: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
22: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
23: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
24: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
25: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
26: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
27: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
28: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
29: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
30: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
31: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
32: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
33: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
34: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
35: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
36: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
37: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
38: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
39: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
40: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
41: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
42: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
43: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
44: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
45: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
46: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
47: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
48: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
49: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
50: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
51: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
52: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
53: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
54: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
55: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
56: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
57: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
58: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
59: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
60: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
61: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
62: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
63: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
64: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
65: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
66: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
67: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
68: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
69: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
70: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
71: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
72: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid>=6))]
73: proc 1 (:init:) spinmodel.pml:80 (state 20) [break]
MSC: ~G 15
74: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
75: proc 16 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
76: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
77: proc 16 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
78: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
79: proc 16 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
80: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
81: proc 16 (p_arc) spinmodel.pml:263 (state 120) [else]
82: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
83: proc 16 (p_arc) spinmodel.pml:282 (state 119) [(1)]
84: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
85: proc 16 (p_arc) spinmodel.pml:286 (state 125) [values: 3!5]
85: proc 16 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
86: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
87: proc 16 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
88: proc 16 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
89: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
90: proc 16 (p_arc) -:0 (state 0) [-end-]
91: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
92: proc 15 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
93: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
94: proc 15 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
95: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
96: proc 15 (p_arc) spinmodel.pml:194 (state 7) [values: 4!5]
96: proc 15 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
97: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
98: proc 15 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
99: proc 15 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
100: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
101: proc 15 (p_arc) -:0 (state 0) [-end-]
102: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
103: proc 14 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
104: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
105: proc 14 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
106: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
107: proc 14 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
107: proc 14 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
108: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
109: proc 14 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
110: proc 14 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
111: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
112: proc 14 (p_arc) -:0 (state 0) [-end-]
113: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
114: proc 13 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
115: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
116: proc 13 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
117: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
118: proc 13 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
118: proc 13 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
119: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
120: proc 13 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
121: proc 13 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
122: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
123: proc 13 (p_arc) -:0 (state 0) [-end-]
124: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
125: proc 12 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
126: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
127: proc 12 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
128: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
129: proc 12 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
129: proc 12 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
130: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
131: proc 12 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
132: proc 12 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
133: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
134: proc 12 (p_arc) -:0 (state 0) [-end-]
135: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
136: proc 11 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
137: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
138: proc 11 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
139: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
140: proc 11 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
141: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
142: proc 11 (p_arc) spinmodel.pml:263 (state 120) [else]
143: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
144: proc 11 (p_arc) spinmodel.pml:282 (state 119) [(1)]
145: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
146: proc 11 (p_arc) spinmodel.pml:286 (state 125) [values: 3!4]
146: proc 11 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
147: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
148: proc 11 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
149: proc 11 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
150: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
151: proc 11 (p_arc) -:0 (state 0) [-end-]
152: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
153: proc 10 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
154: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
155: proc 10 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
156: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
157: proc 10 (p_arc) spinmodel.pml:194 (state 7) [values: 4!4]
157: proc 10 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
158: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
159: proc 10 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
160: proc 10 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
161: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
162: proc 10 (p_arc) -:0 (state 0) [-end-]
163: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
164: proc 9 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
165: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
166: proc 9 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
167: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
168: proc 9 (p_arc) spinmodel.pml:201 (state 11) [values: 4!4]
168: proc 9 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
169: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
170: proc 9 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
171: proc 9 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
172: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
173: proc 9 (p_arc) -:0 (state 0) [-end-]
174: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
175: proc 8 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
176: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
177: proc 8 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
178: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
179: proc 8 (p_arc) spinmodel.pml:201 (state 11) [values: 4!4]
179: proc 8 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
180: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
181: proc 8 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
182: proc 8 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
183: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
184: proc 8 (p_arc) -:0 (state 0) [-end-]
185: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
186: proc 7 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
187: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
188: proc 7 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
189: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
190: proc 7 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
191: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
192: proc 7 (p_arc) spinmodel.pml:263 (state 120) [else]
193: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
194: proc 7 (p_arc) spinmodel.pml:282 (state 119) [(1)]
195: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
196: proc 7 (p_arc) spinmodel.pml:286 (state 125) [values: 3!3]
196: proc 7 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
197: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
198: proc 7 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
199: proc 7 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
200: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
201: proc 7 (p_arc) -:0 (state 0) [-end-]
202: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
203: proc 6 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
204: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
205: proc 6 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
206: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
207: proc 6 (p_arc) spinmodel.pml:194 (state 7) [values: 4!3]
207: proc 6 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
208: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
209: proc 6 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
210: proc 6 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
211: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
212: proc 6 (p_arc) -:0 (state 0) [-end-]
213: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
214: proc 5 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
215: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
216: proc 5 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
217: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
218: proc 5 (p_arc) spinmodel.pml:201 (state 11) [values: 4!3]
218: proc 5 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
219: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
220: proc 5 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
221: proc 5 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
222: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
223: proc 5 (p_arc) -:0 (state 0) [-end-]
224: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
225: proc 4 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
226: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
227: proc 4 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
228: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
229: proc 4 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
230: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
231: proc 4 (p_arc) spinmodel.pml:263 (state 120) [else]
232: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
233: proc 4 (p_arc) spinmodel.pml:282 (state 119) [(1)]
234: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
235: proc 4 (p_arc) spinmodel.pml:286 (state 125) [values: 3!2]
235: proc 4 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
236: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
237: proc 4 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
238: proc 4 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
239: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
240: proc 4 (p_arc) -:0 (state 0) [-end-]
241: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
242: proc 3 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
243: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
244: proc 3 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
245: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
246: proc 3 (p_arc) spinmodel.pml:194 (state 7) [values: 4!2]
246: proc 3 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
247: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
248: proc 3 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
249: proc 3 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
250: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
251: proc 3 (p_arc) -:0 (state 0) [-end-]
252: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
253: proc 2 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
254: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
255: proc 2 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
256: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
257: proc 2 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
258: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
259: proc 2 (p_arc) spinmodel.pml:263 (state 120) [else]
260: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
261: proc 2 (p_arc) spinmodel.pml:282 (state 119) [(1)]
262: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
263: proc 2 (p_arc) spinmodel.pml:286 (state 125) [values: 3!1]
263: proc 2 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
264: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
265: proc 2 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
266: proc 2 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
267: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
268: proc 2 (p_arc) -:0 (state 0) [-end-]
269: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
270: proc 1 (:init:) -:0 (state 0) [-end-]
<<<<<START OF CYCLE>>>>>
271: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
272: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
spin: trail ends after 272 steps
#processes 1:
272: proc 0 (ltl_0) spinmodel.pml:15 (state 22) (invalid end state)
(!((p>0)))
global vars:
(struct B1)
chan item_list (=1): len 0:
(struct B2)
chan item_list (=2): len 0:
(struct T1)
chan item_list (=3): len 1: [1,],
(struct T2)
chan item_list (=4): len 4: [5,], [4,], [3,], [2,],
byte p: 0
bit sc_lock: 0
Bye,
Alexander.
--
http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF
http://www.FreeBSD.org netchild@FreeBSD.org : PGP 0x8F31830F9F2772BF