Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2012-02-13 16:10:28
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
about Xspin verification output and Never Claim formula
Dear all,
I just finished writing the following code, two processes Robot1 and Robot2, and they repeatedly execute and have several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. I want to verify "connected1 and connected2 are always eventually simultaneously true". So at the last part, I added a 'Never Claim' which was automatically generated by system corresponding to my temporal logic formula representation "[] <> (connected1 == 1) && [] <> (connected2 == 1)", and the system returned a counter-example, but it is as following:
preparing trail, please wait...done
MSC: ~G line 422
1: proc - (never_0) pan_in:422 (state 1) [(!((connected1==1)))]
Never claim moves to line 422 [(!((connected1==1)))]
Starting Robot1 with pid 2
2: proc 0 (:init:) pan_in:410 (state 1) [(run Robot1())]
Starting Robot2 with pid 3
3: proc 0 (:init:) pan_in:410 (state 2) [(run Robot2())]
MSC: ~G line 427
4: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
Never claim moves to line 427 [(!((connected1==1)))]
n 5: proc 2 (Robot2) pan_in:230 (state 2) [printf('%e',direction)] <
6: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
n 7: proc 1 (Robot1) pan_in:27 (state 2) [printf('%e',direction)] <
8: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
10: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 11: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
12: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
14: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 15: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
16: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
17: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
18: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
20: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 21: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
22: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
23: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
24: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
26: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 27: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
28: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
30: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 31: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
32: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
34: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
36: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
38: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
40: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
42: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1 43: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
44: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
46: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 47: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
48: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
50: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 51: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
52: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
54: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 55: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
56: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
57: proc 2 (Robot2) pan_in:271 (state 45) [(((fcon&&(direction==n))&&!(insn2)))] <
2 57: proc 2 (Robot2) pan_in:271 (state 47) [printf('%d',robot2Loc)] <
58: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
59: proc 2 (Robot2) pan_in:360 (state 251) [(fcon)] <
60: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
61: proc 2 (Robot2) pan_in:370 (state 265) [((fcon&&(direction==n)))] <
n 61: proc 2 (Robot2) pan_in:370 (state 267) [printf('%e',direction)] <
62: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
64: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 65: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
66: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
68: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2 69: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
70: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
71: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
72: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
74: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 75: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
76: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
77: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
78: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
80: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2 81: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
82: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
84: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 85: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
86: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
88: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
90: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
92: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
94: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
96: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0 97: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
98: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
100: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1101: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
102: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
104: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0105: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
106: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
108: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0109: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
110: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
111: proc 2 (Robot2) pan_in:288 (state 81) [(((fnocon&&(direction==n))&&!(inss2)))] <
1111: proc 2 (Robot2) pan_in:288 (state 83) [printf('%d',robot2Loc)] <
112: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
113: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
114: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
115: proc 2 (Robot2) pan_in:375 (state 277) [((fnocon&&(direction==n)))] <
s115: proc 2 (Robot2) pan_in:375 (state 279) [printf('%e',direction)] <
116: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
118: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0119: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
120: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
122: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1123: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
124: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
125: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
126: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
128: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0129: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
130: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
131: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
132: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
134: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1135: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
136: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
138: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1139: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
140: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
142: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
144: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
146: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
148: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
150: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0151: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
152: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
154: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0155: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
156: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
158: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1159: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
160: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
162: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0163: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
164: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
165: proc 2 (Robot2) pan_in:330 (state 177) [(((cohcon&&(direction==s))&&!(inse2)))] <
11165: proc 2 (Robot2) pan_in:330 (state 180) [printf('%d',robot2Loc)] <
166: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
167: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
168: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
169: proc 2 (Robot2) pan_in:390 (state 313) [(((cohcon&&(direction==s))&&(nextDirection==e)))] <
e169: proc 2 (Robot2) pan_in:390 (state 315) [printf('%e',direction)] <
170: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
172: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1173: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
174: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
176: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1177: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
178: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
179: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
180: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
182: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1183: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
184: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
185: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
186: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
188: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1189: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
190: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
192: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1193: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
194: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
196: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
198: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
200: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
202: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
204: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1205: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
206: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
208: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0209: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
210: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
212: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0213: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
214: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
216: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0217: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
218: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
219: proc 2 (Robot2) pan_in:279 (state 63) [(((fcon&&(direction==e))&&!(inse2)))] <
21219: proc 2 (Robot2) pan_in:279 (state 65) [printf('%d',robot2Loc)] <
220: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
221: proc 2 (Robot2) pan_in:360 (state 251) [(fcon)] <
222: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
223: proc 2 (Robot2) pan_in:372 (state 271) [((fcon&&(direction==e)))] <
e223: proc 2 (Robot2) pan_in:372 (state 273) [printf('%e',direction)] <
<<<<<START OF CYCLE>>>>>
224: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
226: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2227: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
228: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
230: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1231: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
232: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
233: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
234: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
236: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2237: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
238: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
239: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
240: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
242: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1243: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
244: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
246: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0247: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
248: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
250: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
252: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
254: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
256: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
258: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0259: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
260: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
262: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1263: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
264: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
266: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0267: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
268: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
270: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0271: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
272: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
273: proc 2 (Robot2) pan_in:296 (state 99) [(((fnocon&&(direction==e))&&!(insw2)))] <
11273: proc 2 (Robot2) pan_in:296 (state 101) [printf('%d',robot2Loc)] <
274: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
275: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
276: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
277: proc 2 (Robot2) pan_in:376 (state 280) [((fnocon&&(direction==e)))] <
w277: proc 2 (Robot2) pan_in:376 (state 282) [printf('%e',direction)] <
278: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
280: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1281: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
282: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
284: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1285: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
286: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
287: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
288: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
290: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1291: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
292: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
293: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
294: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
296: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1297: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
298: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
300: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1301: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
302: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
304: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
306: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
308: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
310: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
312: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0313: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
314: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
316: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0317: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
318: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
320: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1321: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
322: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
324: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0325: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
326: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
327: proc 2 (Robot2) pan_in:346 (state 225) [(((cohcon&&(direction==w))&&!(insn2)))] <
12327: proc 2 (Robot2) pan_in:346 (state 228) [printf('%d',robot2Loc)] <
328: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
329: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
330: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
331: proc 2 (Robot2) pan_in:400 (state 337) [(((cohcon&&(direction==w))&&(nextDirection==n)))] <
n331: proc 2 (Robot2) pan_in:400 (state 339) [printf('%e',direction)] <
332: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
334: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1335: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
336: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
338: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2339: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
340: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
341: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
342: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
344: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1345: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
346: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
347: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
348: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
350: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
2351: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
352: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
354: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0355: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
356: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
358: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
360: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
362: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
364: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
366: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0367: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
368: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
370: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1371: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
372: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
374: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0375: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
376: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
378: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0379: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
380: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
381: proc 2 (Robot2) pan_in:288 (state 81) [(((fnocon&&(direction==n))&&!(inss2)))] <
11381: proc 2 (Robot2) pan_in:288 (state 83) [printf('%d',robot2Loc)] <
382: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
383: proc 2 (Robot2) pan_in:361 (state 254) [(fnocon)] <
384: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
385: proc 2 (Robot2) pan_in:375 (state 277) [((fnocon&&(direction==n)))] <
s385: proc 2 (Robot2) pan_in:375 (state 279) [printf('%e',direction)] <
386: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
388: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1389: proc 2 (Robot2) pan_in:237 (state 12) [printf('%d',robot2x)]
390: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
392: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1393: proc 2 (Robot2) pan_in:238 (state 14) [printf('%d',robot2y)]
394: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
395: proc 2 (Robot2) pan_in:243 (state 15) [((robot2x>=robot1x))]
396: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
398: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1399: proc 2 (Robot2) pan_in:243 (state 17) [printf('%d',abs12x)]
400: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
401: proc 2 (Robot2) pan_in:248 (state 23) [((robot2y>=robot1y))]
402: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
404: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1405: proc 2 (Robot2) pan_in:248 (state 25) [printf('%d',abs12y)]
406: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
408: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1409: proc 2 (Robot2) pan_in:252 (state 32) [printf('%d',connected2)]
410: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
412: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
414: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
416: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
418: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
420: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0421: proc 2 (Robot2) pan_in:263 (state 38) [printf('%d',fcon)]
422: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
424: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0425: proc 2 (Robot2) pan_in:264 (state 40) [printf('%d',fnocon)]
426: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
428: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
1429: proc 2 (Robot2) pan_in:265 (state 42) [printf('%d',cohcon)]
430: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
432: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
0433: proc 2 (Robot2) pan_in:266 (state 44) [printf('%d',cohnocon)]
434: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
435: proc 2 (Robot2) pan_in:330 (state 177) [(((cohcon&&(direction==s))&&!(inse2)))] <
21435: proc 2 (Robot2) pan_in:330 (state 180) [printf('%d',robot2Loc)] <
436: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
437: proc 2 (Robot2) pan_in:363 (state 260) [(cohcon)] <
438: proc - (never_0) pan_in:427 (state 7) [(!((connected1==1)))]
439: proc 2 (Robot2) pan_in:390 (state 313) [(((cohcon&&(direction==s))&&(nextDirection==e)))] <
e439: proc 2 (Robot2) pan_in:390 (state 315) [printf('%e',direction)] <
spin: trail ends after 439 steps
#processes: 3
439: proc 2 (Robot2) pan_in:236 (state 351)
439: proc 1 (Robot1) pan_in:35 (state 347)
439: proc 0 (:init:) pan_in:410 (state 4)
MSC: ~G line 426
439: proc - (never_0) pan_in:426 (state 9)
3 processes createdwhich contains a cyclic execution that 'connected2' always changes bewteen 0 and 1 (see step 301, 355, 409), so that satisfies the temporal logic formula. According to my knowledge, SPIN should return a counter-example which doesn't satisfy the temporal logic formula. Is my temporal logic formula representation correct?
Offline
#2 2012-02-13 16:15:51
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
Re: about Xspin verification output and Never Claim formula
Sorry I attach my code as below, many thanks.
bool connected1 = 0; /*connectivity mode, robot1*/
bool connected2 = 0; /*connectivity mode, robot2*/
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};
proctype Robot1()
{
int robot1Loc = 0; /*inital robot location*/
int range =1; /*communication range*/
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0; /*ford == for, for is keyword, so we cannot use it, two motion modes: forward, coherence*/
bool fcon, fnocon, cohcon, cohnocon; /*four alternatives combining the two motion modes and connectivity modes*/
bool insn1, inss1, inse1, insw1;
if /*initially, random direction*/
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
:: robot1x = robot1Loc / 10; printf("%d", robot1x); /*xcoordinate*/
robot1y = robot1Loc % 10; printf ("%d", robot1y); /*ycoordinate*/
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;
connected1 = ((abs12x <= range) || ((lenmax - abs12x) <= range)) && ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected1);
insn1 = (robot1x == robot2x && (robot1y + 1) % lenmax == robot2y); /*if insn1 == 1, robot2 is at one step north of robot1*/
inss1 = (robot1x == robot2x && (robot1y - 1) % lenmax == robot2y);
inse1 = ((robot1x + 1) % lenmax == robot2x && robot1y == robot2y);
insw1 = ((robot1x - 1) % lenmax == robot2x && robot1y == robot2y);
fcon = (ford ==1 && coh == 0 && connected1 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == n && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == n && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == s && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == s && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == s && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == e && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fcon && direction == e && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == e && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == w && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fcon && direction == w && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction == w && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fnocon && direction == n && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc); /*moving south*/
::(fnocon && direction == n && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fnocon && direction == n && inss1) -> (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fnocon && direction == s && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc); /*moving north*/
::(fnocon && direction == s && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(fnocon && direction == s && insn1) -> (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(fnocon && direction == e && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*moving west*/
::(fnocon && direction == e && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fnocon && direction == e && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fnocon && direction == w && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc); /*moving east*/
::(fnocon && direction == w && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fnocon && direction == w && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(cohnocon && direction == n && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == n && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(cohnocon && direction == n && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(cohnocon && direction == s && !inss1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot1Loc);
::(cohnocon && direction == s && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); /*next robot location, moving east*/
::(cohnocon && direction == s && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/
::(cohnocon && direction == e && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == e && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(cohnocon && direction == e && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
::(cohnocon && direction == w && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc);
::(cohnocon && direction == w && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving north*/
::(cohnocon && direction == w && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == n && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10); nextDirection = e; printf ("%d", robot1Loc); /*moving east*/
:: (cohcon && direction == n && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == n && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == n && !insw1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc);
:: (cohcon && direction == n && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == n && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == s && !inse1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc);
:: (cohcon && direction == s && inse1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == s && inse1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == s && !insw1) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc);
:: (cohcon && direction == s && insw1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc); /*next robot location, moving north*/
:: (cohcon && direction == s && insw1) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot1Loc); /*next robot location, moving south*/
:: (cohcon && direction == e && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc);
:: (cohcon && direction == e && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); nextDirection = e; /*next robot location, moving east*/
:: (cohcon && direction == e && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
:: (cohcon && direction == e && !inss1) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); nextDirection = s;printf ("%d", robot1Loc);
:: (cohcon && direction == e && inss1) ->robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc); nextDirection = e; /*next robot location, moving east*/
:: (cohcon && direction == e && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); nextDirection = w; /*next robot location, moving west*/
:: (cohcon && direction == w && !insn1) -> robot1Loc = 10 * (robot1Loc/10) + (((robot1Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot1Loc);
:: (cohcon && direction == w && insn1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc); /*next robot location, moving east*/
:: (cohcon && direction == w && insn1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
:: (cohcon && direction == w && !inss1) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot1Loc);
:: (cohcon && direction == w && inss1) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot1Loc); /*next robot location, moving east*/
:: (cohcon && direction == w && inss1) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot1Loc); /*next robot location, moving west*/
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == w) -> direction = w; printf ("%e", direction);
fi;
od
}
proctype Robot2()
{
int robot2Loc = 1;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;
bool ford =1, coh = 0; /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon;
bool insn2, inss2, inse2, insw2;
if
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;
do
:: robot2x = robot2Loc / 10; printf("%d", robot2x);
robot2y = robot2Loc % 10; printf("%d", robot2y);
if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x; printf ("%d", abs12x);
::(robot2x < robot1x) -> abs12x = robot1x - robot2x; printf("%d", abs12x);
fi;
if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y; printf("%d", abs12y);
::(robot2y < robot1y) -> abs12y = robot1y - robot2y; printf("%d", abs12y);
fi;
connected2 = ((abs12x <= range) || ((lenmax - abs12x) <= range)) && ((abs12y <= range) || ((lenmax - abs12y) <= range)); printf("%d", connected2);
insn2 = (robot2x == robot1x && (robot2y + 1) % lenmax == robot1y);
inss2 = (robot2x == robot1x && (robot2y - 1) % lenmax == robot1y);
inse2 = ((robot2x + 1) % lenmax == robot1x && robot2y == robot1y);
insw2 = ((robot2x - 1) % lenmax == robot1x && robot2y == robot1y);
fcon = (ford ==1 && coh ==0 && connected2 == 1); printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected2 == 0); printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected2== 1); printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected2 == 0); printf ("%d", cohnocon);
/*next location*/
if /*if there are two statements executable, one of them will be selected randomly*/
::(fcon && direction == n && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fcon && direction == n && insn2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
::(fcon && direction == n && insn2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fcon && direction == s && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(fcon && direction == s && inss2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc);
::(fcon && direction == s && inss2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fcon && direction == e && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fcon && direction == e && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == e && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == w && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fcon && direction == w && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction == w && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc);
::(fnocon && direction == n && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc); /*moving south*/
::(fnocon && direction == n && inss2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fnocon && direction == n && inss2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fnocon && direction == s && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(fnocon && direction == s && insn2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(fnocon && direction == s && insn2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(fnocon && direction == e && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == e && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fnocon && direction == e && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(fnocon && direction == w && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(fnocon && direction == w && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(fnocon && direction == w && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(cohnocon && direction == n && !insn2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == n && insn2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(cohnocon && direction == n && insn2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(cohnocon && direction == s && !inss2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); printf ("%d", robot2Loc);
::(cohnocon && direction == s && inss2) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; printf ("%d", robot2Loc); /*moving east*/
::(cohnocon && direction == s && inss2) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc); /*moving west*/
::(cohnocon && direction == e && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == e && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(cohnocon && direction == e && inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
::(cohnocon && direction == w && !insw2) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot2Loc);
::(cohnocon && direction == w && insw2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc); /*moving north*/
::(cohnocon && direction == w && insw2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == n && !inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10); nextDirection = e; printf ("%d", robot2Loc);
:: (cohcon && direction == n && inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == n && inse2) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == n &&!insw2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc);
:: (cohcon && direction == n &&insw2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == n &&insw2 ) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == s &&!inse2) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc);
:: (cohcon && direction == s &&inse2) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == s &&inse2) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == s &&!insw2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc);
:: (cohcon && direction == s &&insw2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc); /*moving north*/
:: (cohcon && direction == s &&insw2 ) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ; nextDirection = s; printf ("%d", robot2Loc); /*moving south*/
:: (cohcon && direction == e &&!insn2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc);
:: (cohcon && direction == e &&insn2 ) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == e &&insn2 ) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == e && !inss2 ) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot2Loc);
:: (cohcon && direction == e && inss2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == e && inss2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == w && !insn2 ) -> robot2Loc = 10 * (robot2Loc/10) + (((robot2Loc % 10) + 1) % lenmax) ; nextDirection = n; printf ("%d", robot2Loc);
:: (cohcon && direction == w && insn2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == w && insn2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
:: (cohcon && direction == w && !inss2 ) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax); nextDirection = s; printf ("%d", robot2Loc);
:: (cohcon && direction == w && inss2 ) ->robot2Loc = (robot2Loc +10) % (lenmax*10) ; nextDirection = e; printf ("%d", robot2Loc); /*moving east*/
:: (cohcon && direction == w && inss2 ) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10); nextDirection = w; printf ("%d", robot2Loc); /*moving west*/
fi;
/*next motion*/
if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;
/*next direction*/
if
:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);
::(fnocon && direction == n) -> direction = s; printf ("%e", direction);
::(fnocon && direction == e) -> direction = w; printf ("%e", direction);
::(fnocon && direction == s) -> direction = n; printf ("%e", direction);
::(fnocon && direction == w) -> direction = e; printf ("%e", direction);
:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == n && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == s && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == e && nextDirection == w) -> direction = w; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == n) -> direction = n; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == s) -> direction = s; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == e) -> direction = e; printf ("%e", direction);
:: (cohcon && direction == w && nextDirection == w) -> direction = w; printf ("%e", direction);
fi;
od
}
init { atomic {run Robot1(); run Robot2()} }
/*
* Formula As Typed: ([] <> (connected1 == 1) && [] <> (connected2 == 1))
* The Never Claim Below Corresponds
* To The Negated Formula !(([] <> (connected1 == 1) && [] <> (connected2 == 1)))
* (formalizing violations of the original)
*/
never { /* !(([] <> (connected1 == 1) && [] <> (connected2 == 1))) */
T0_init:
if
:: (! ((connected2 == 1))) -> goto accept_S5
:: (! ((connected1 == 1))) -> goto accept_S10
:: (1) -> goto T0_init
fi;
accept_S5:
if
:: (! ((connected2 == 1))) -> goto accept_S5
fi;
accept_S10:
if
:: (! ((connected1 == 1))) -> goto accept_S10
fi;
}Offline
#4 2012-02-14 12:55:18
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
Re: about Xspin verification output and Never Claim formula
> spinroot wrote:
> don't you mean <>[] (connected1 ==1 && connected2 == 1) ?
Thanks. I aim to verify for both connected1 and connected2, infinitely often (always eventually) connectedi (i=1,2) are true in a single verification.
I think [] stands for temporal operator 'always in the further', <> stands for temporal operator 'sometime in the further'.
I represent as [] <> (connected1 == 1) && [] <> (connected2 == 1), but it seems SPIN return a counter-example with 'connected2' is always changing between 0 and 1, obviously doesn't satisfy what I aim to verify.
I expect a counter-example with both connected1 and connected2 always remain being 0.
Offline
#5 2012-02-14 16:09:33
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
Re: about Xspin verification output and Never Claim formula
[quote=Chengxiu]obviously doesn't satisfy what I aim to verify [/quote]
sorry I mean a cyclic execution with 'connected2' changing between 0 and 1 is what I don't expect. I expect a cyclic execution with 'connected1' or 'connected2' remain being 0 or both, that's the counter-example of the temporal logic I aim to verify.
Offline
#6 2012-02-14 17:57:35
Re: about Xspin verification output and Never Claim formula
if the requirement is that connected1 and connected2 cannot both simultaneously become and remain true then the claim would be that this is impossible:
<>[] (connected1 != 0 || connected2 != 0)
to verify that claim you have to negate this formula -- to find executions that match a counter-example:
!<>[] (connected1 != 0 || connected2 != 0) which is the same as
[]<> (connected1 == 0 && connected2 == 0)
Offline
#7 2012-02-14 18:13:24
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
Re: about Xspin verification output and Never Claim formula
> spinroot wrote:
> if the requirement is that connected1 and connected2 cannot both simultaneously become and remain true then the claim would be that this is impossible:
<>[] (connected1 != 0 || connected2 != 0)
to verify that claim you have to negate this formula -- to find executions that match a counter-example:
!<>[] (connected1 != 0 || connected2 != 0) which is the same as
[]<> (connected1 == 0 && connected2 == 0)
I think you misunderstand my requirement. my requirement is connected1 and connected2 always eventually (infinitely often) becomes true. both connected1 and connected2 do not need remain true but, if they become false, should eventually become true again.
How to specify a temporal logic for above requirement?
Offline
#8 2012-02-15 06:04:45
Re: about Xspin verification output and Never Claim formula
Okay -- then I think you only forgot to negate the claim
you can generate the never claim with:
spin -f '!([]<> (connected1 == 1) && [] <> (connected2 == 1))'
which would be the same as saying:
spin -f '(<>[] !connected1 || <>[] !connected2)'
since the two parts of this property are independent, you can of course also verify them in two separate steps
(first for connected1 and then for connected2)
Offline
#9 2012-02-16 09:19:53
- Chengxiu
- Member
- Registered: 2011-07-28
- Posts: 19
Re: about Xspin verification output and Never Claim formula
> spinroot wrote:
> Okay -- then I think you only forgot to negate the claim
you can generate the never claim with:
spin -f '!([]<> (connected1 == 1) && [] <> (connected2 == 1))'
which would be the same as saying:
spin -f '(<>[] !connected1 || <>[] !connected2)'
since the two parts of this property are independent, you can of course also verify them in two separate steps
(first for connected1 and then for connected2)
Why should I negate the claim? I think if we aim to verify whether all executions of program exhibit property 'p', we should generate a never claim for 'p'. never claim will produce Buchi automaton for '!q' and SPIN computes the xxx of automatons of all program executions and '!q'. If there is an accepted sequence which satisfies '!p' and must not exhibit property 'p'.
Offline
#10 2012-02-17 04:55:10
Re: about Xspin verification output and Never Claim formula
yes - except you must do the negation yourself if you use a never claim (i.e., one generated with -f)
if you use an inline ltl formula, then the negation will happen automatically,
but not if you explicitly provide a never claim
Offline