API tools faq
paste
Advertisement
Guest User

Untitled

a guest
May 25th, 2018
85
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 13.09 KB | None | 0 0
raw download clone embed print report
  1. TLC2 Version 2.12 of 29 January 2018
  2. Running breadth-first search Model-Checking with 1 worker on 4 cores with 885MB heap and 64MB offheap memory (Windows 10 10.0 amd64, Oracle Corporation 1.8.0_161 x86_64).
  3. Parsing file C:\Temp\tla\TrainSystemSimple.tla
  4. Parsing file C:\Temp\tla\tla2sany\StandardModules\Naturals.tla
  5. Parsing file C:\Temp\tla\Track.tla
  6. Parsing file C:\Temp\tla\StationTrack.tla
  7. Parsing file C:\Temp\tla\Switch.tla
  8. Semantic processing of module Naturals
  9. Semantic processing of module Track
  10. Semantic processing of module StationTrack
  11. Semantic processing of module Switch
  12. Semantic processing of module TrainSystemSimple
  13. Starting... (2018-05-25 20:40:07)
  14. Implied-temporal checking--satisfiability problem has 12 branches.
  15. Computing initial states...
  16. Finished computing initial states: 64 distinct states generated.
  17. Checking 12 branches of temporal properties for the current state space with 17700 total distinct states at (2018-05-25 20:40:11)
  18. Finished checking temporal properties in 00s at 2018-05-25 20:40:12
  19. Progress(6) at 2018-05-25 20:40:12: 5272 states generated (5.272 s/min), 1475 distinct states found (1.475 ds/min), 678 states left on queue.
  20. Checking 12 branches of temporal properties for the current state space with 539328 total distinct states at (2018-05-25 20:41:12)
  21. Error: Temporal properties were violated.
  22.  
  23. Error: The following behavior constitutes a counter-example:
  24.  
  25. State 1: <Initial predicate>
  26. /\ tr1 = [state |-> "free"]
  27. /\ tr2 = [state |-> "free"]
  28. /\ tr3 = [state |-> "free"]
  29. /\ tr4 = [state |-> "free"]
  30. /\ trC = [state |-> "free"]
  31. /\ trD = [state |-> "free"]
  32. /\ trF = [state |-> "free"]
  33. /\ trG = [state |-> "free"]
  34. /\ counter = 0
  35. /\ sw1 = [position |-> 1]
  36. /\ sw2 = [position |-> 1]
  37. /\ sw3 = [position |-> 1]
  38. /\ sw4 = [position |-> 1]
  39. /\ sw5 = [position |-> 1]
  40. /\ sw6 = [position |-> 1]
  41.  
  42. State 2: <SwitchPosition4 line 521, col 20 to line 522, col 105 of module TrainSystemSimple>
  43. /\ tr1 = [state |-> "free"]
  44. /\ tr2 = [state |-> "free"]
  45. /\ tr3 = [state |-> "free"]
  46. /\ tr4 = [state |-> "free"]
  47. /\ trC = [state |-> "free"]
  48. /\ trD = [state |-> "free"]
  49. /\ trF = [state |-> "free"]
  50. /\ trG = [state |-> "free"]
  51. /\ counter = 0
  52. /\ sw1 = [position |-> 1]
  53. /\ sw2 = [position |-> 1]
  54. /\ sw3 = [position |-> 1]
  55. /\ sw4 = [position |-> 2]
  56. /\ sw5 = [position |-> 1]
  57. /\ sw6 = [position |-> 1]
  58.  
  59. State 3: <SwitchPosition6 line 527, col 20 to line 528, col 105 of module TrainSystemSimple>
  60. /\ tr1 = [state |-> "free"]
  61. /\ tr2 = [state |-> "free"]
  62. /\ tr3 = [state |-> "free"]
  63. /\ tr4 = [state |-> "free"]
  64. /\ trC = [state |-> "free"]
  65. /\ trD = [state |-> "free"]
  66. /\ trF = [state |-> "free"]
  67. /\ trG = [state |-> "free"]
  68. /\ counter = 0
  69. /\ sw1 = [position |-> 1]
  70. /\ sw2 = [position |-> 1]
  71. /\ sw3 = [position |-> 1]
  72. /\ sw4 = [position |-> 2]
  73. /\ sw5 = [position |-> 1]
  74. /\ sw6 = [position |-> 2]
  75.  
  76. State 4: <Cto3begin line 111, col 14 to line 115, col 85 of module TrainSystemSimple>
  77. /\ tr1 = [state |-> "free"]
  78. /\ tr2 = [state |-> "free"]
  79. /\ tr3 = [state |-> "coming"]
  80. /\ tr4 = [state |-> "free"]
  81. /\ trC = [state |-> "occupied"]
  82. /\ trD = [state |-> "free"]
  83. /\ trF = [state |-> "free"]
  84. /\ trG = [state |-> "free"]
  85. /\ counter = 1
  86. /\ sw1 = [position |-> 1]
  87. /\ sw2 = [position |-> 1]
  88. /\ sw3 = [position |-> 1]
  89. /\ sw4 = [position |-> 2]
  90. /\ sw5 = [position |-> 1]
  91. /\ sw6 = [position |-> 2]
  92.  
  93. State 5: <Dto4begin line 231, col 14 to line 235, col 85 of module TrainSystemSimple>
  94. /\ tr1 = [state |-> "free"]
  95. /\ tr2 = [state |-> "free"]
  96. /\ tr3 = [state |-> "coming"]
  97. /\ tr4 = [state |-> "coming"]
  98. /\ trC = [state |-> "occupied"]
  99. /\ trD = [state |-> "occupied"]
  100. /\ trF = [state |-> "free"]
  101. /\ trG = [state |-> "free"]
  102. /\ counter = 2
  103. /\ sw1 = [position |-> 1]
  104. /\ sw2 = [position |-> 1]
  105. /\ sw3 = [position |-> 1]
  106. /\ sw4 = [position |-> 2]
  107. /\ sw5 = [position |-> 1]
  108. /\ sw6 = [position |-> 2]
  109.  
  110. State 6: <Cto3end line 117, col 12 to line 120, col 92 of module TrainSystemSimple>
  111. /\ tr1 = [state |-> "free"]
  112. /\ tr2 = [state |-> "free"]
  113. /\ tr3 = [state |-> "occupied"]
  114. /\ tr4 = [state |-> "coming"]
  115. /\ trC = [state |-> "free"]
  116. /\ trD = [state |-> "occupied"]
  117. /\ trF = [state |-> "free"]
  118. /\ trG = [state |-> "free"]
  119. /\ counter = 2
  120. /\ sw1 = [position |-> 1]
  121. /\ sw2 = [position |-> 1]
  122. /\ sw3 = [position |-> 1]
  123. /\ sw4 = [position |-> 2]
  124. /\ sw5 = [position |-> 1]
  125. /\ sw6 = [position |-> 2]
  126.  
  127. State 7: <3toFbegin line 305, col 14 to line 312, col 79 of module TrainSystemSimple>
  128. /\ tr1 = [state |-> "free"]
  129. /\ tr2 = [state |-> "free"]
  130. /\ tr3 = [state |-> "leaving"]
  131. /\ tr4 = [state |-> "coming"]
  132. /\ trC = [state |-> "free"]
  133. /\ trD = [state |-> "occupied"]
  134. /\ trF = [state |-> "occupied"]
  135. /\ trG = [state |-> "occupied"]
  136. /\ counter = 2
  137. /\ sw1 = [position |-> 1]
  138. /\ sw2 = [position |-> 1]
  139. /\ sw3 = [position |-> 1]
  140. /\ sw4 = [position |-> 2]
  141. /\ sw5 = [position |-> 1]
  142. /\ sw6 = [position |-> 2]
  143.  
  144. State 8: <3toFend line 314, col 12 to line 320, col 77 of module TrainSystemSimple>
  145. /\ tr1 = [state |-> "free"]
  146. /\ tr2 = [state |-> "free"]
  147. /\ tr3 = [state |-> "free"]
  148. /\ tr4 = [state |-> "coming"]
  149. /\ trC = [state |-> "free"]
  150. /\ trD = [state |-> "occupied"]
  151. /\ trF = [state |-> "free"]
  152. /\ trG = [state |-> "free"]
  153. /\ counter = 2
  154. /\ sw1 = [position |-> 1]
  155. /\ sw2 = [position |-> 1]
  156. /\ sw3 = [position |-> 1]
  157. /\ sw4 = [position |-> 2]
  158. /\ sw5 = [position |-> 1]
  159. /\ sw6 = [position |-> 2]
  160.  
  161. State 9: <SwitchPosition2 line 515, col 20 to line 516, col 105 of module TrainSystemSimple>
  162. /\ tr1 = [state |-> "free"]
  163. /\ tr2 = [state |-> "free"]
  164. /\ tr3 = [state |-> "free"]
  165. /\ tr4 = [state |-> "coming"]
  166. /\ trC = [state |-> "free"]
  167. /\ trD = [state |-> "occupied"]
  168. /\ trF = [state |-> "free"]
  169. /\ trG = [state |-> "free"]
  170. /\ counter = 2
  171. /\ sw1 = [position |-> 1]
  172. /\ sw2 = [position |-> 2]
  173. /\ sw3 = [position |-> 1]
  174. /\ sw4 = [position |-> 2]
  175. /\ sw5 = [position |-> 1]
  176. /\ sw6 = [position |-> 2]
  177.  
  178. State 10: <SwitchPosition4 line 521, col 20 to line 522, col 105 of module TrainSystemSimple>
  179. /\ tr1 = [state |-> "free"]
  180. /\ tr2 = [state |-> "free"]
  181. /\ tr3 = [state |-> "free"]
  182. /\ tr4 = [state |-> "coming"]
  183. /\ trC = [state |-> "free"]
  184. /\ trD = [state |-> "occupied"]
  185. /\ trF = [state |-> "free"]
  186. /\ trG = [state |-> "free"]
  187. /\ counter = 2
  188. /\ sw1 = [position |-> 1]
  189. /\ sw2 = [position |-> 2]
  190. /\ sw3 = [position |-> 1]
  191. /\ sw4 = [position |-> 1]
  192. /\ sw5 = [position |-> 1]
  193. /\ sw6 = [position |-> 2]
  194.  
  195. State 11: <Fto1begin line 264, col 14 to line 268, col 85 of module TrainSystemSimple>
  196. /\ tr1 = [state |-> "coming"]
  197. /\ tr2 = [state |-> "free"]
  198. /\ tr3 = [state |-> "free"]
  199. /\ tr4 = [state |-> "coming"]
  200. /\ trC = [state |-> "free"]
  201. /\ trD = [state |-> "occupied"]
  202. /\ trF = [state |-> "occupied"]
  203. /\ trG = [state |-> "free"]
  204. /\ counter = 3
  205. /\ sw1 = [position |-> 1]
  206. /\ sw2 = [position |-> 2]
  207. /\ sw3 = [position |-> 1]
  208. /\ sw4 = [position |-> 1]
  209. /\ sw5 = [position |-> 1]
  210. /\ sw6 = [position |-> 2]
  211.  
  212. State 12: <Gto2begin line 384, col 14 to line 388, col 85 of module TrainSystemSimple>
  213. /\ tr1 = [state |-> "coming"]
  214. /\ tr2 = [state |-> "coming"]
  215. /\ tr3 = [state |-> "free"]
  216. /\ tr4 = [state |-> "coming"]
  217. /\ trC = [state |-> "free"]
  218. /\ trD = [state |-> "occupied"]
  219. /\ trF = [state |-> "occupied"]
  220. /\ trG = [state |-> "occupied"]
  221. /\ counter = 0
  222. /\ sw1 = [position |-> 1]
  223. /\ sw2 = [position |-> 2]
  224. /\ sw3 = [position |-> 1]
  225. /\ sw4 = [position |-> 1]
  226. /\ sw5 = [position |-> 1]
  227. /\ sw6 = [position |-> 2]
  228.  
  229. State 13: <SwitchPosition2 line 515, col 20 to line 516, col 105 of module TrainSystemSimple>
  230. /\ tr1 = [state |-> "coming"]
  231. /\ tr2 = [state |-> "coming"]
  232. /\ tr3 = [state |-> "free"]
  233. /\ tr4 = [state |-> "coming"]
  234. /\ trC = [state |-> "free"]
  235. /\ trD = [state |-> "occupied"]
  236. /\ trF = [state |-> "occupied"]
  237. /\ trG = [state |-> "occupied"]
  238. /\ counter = 0
  239. /\ sw1 = [position |-> 1]
  240. /\ sw2 = [position |-> 1]
  241. /\ sw3 = [position |-> 1]
  242. /\ sw4 = [position |-> 1]
  243. /\ sw5 = [position |-> 1]
  244. /\ sw6 = [position |-> 2]
  245.  
  246. State 14: <Fto1end line 270, col 12 to line 273, col 92 of module TrainSystemSimple>
  247. /\ tr1 = [state |-> "occupied"]
  248. /\ tr2 = [state |-> "coming"]
  249. /\ tr3 = [state |-> "free"]
  250. /\ tr4 = [state |-> "coming"]
  251. /\ trC = [state |-> "free"]
  252. /\ trD = [state |-> "occupied"]
  253. /\ trF = [state |-> "free"]
  254. /\ trG = [state |-> "occupied"]
  255. /\ counter = 0
  256. /\ sw1 = [position |-> 1]
  257. /\ sw2 = [position |-> 1]
  258. /\ sw3 = [position |-> 1]
  259. /\ sw4 = [position |-> 1]
  260. /\ sw5 = [position |-> 1]
  261. /\ sw6 = [position |-> 2]
  262.  
  263. State 15: <Dto4end line 237, col 12 to line 240, col 92 of module TrainSystemSimple>
  264. /\ tr1 = [state |-> "occupied"]
  265. /\ tr2 = [state |-> "coming"]
  266. /\ tr3 = [state |-> "free"]
  267. /\ tr4 = [state |-> "occupied"]
  268. /\ trC = [state |-> "free"]
  269. /\ trD = [state |-> "free"]
  270. /\ trF = [state |-> "free"]
  271. /\ trG = [state |-> "occupied"]
  272. /\ counter = 0
  273. /\ sw1 = [position |-> 1]
  274. /\ sw2 = [position |-> 1]
  275. /\ sw3 = [position |-> 1]
  276. /\ sw4 = [position |-> 1]
  277. /\ sw5 = [position |-> 1]
  278. /\ sw6 = [position |-> 2]
  279.  
  280. State 16: <4toDbegin line 242, col 14 to line 246, col 94 of module TrainSystemSimple>
  281. /\ tr1 = [state |-> "occupied"]
  282. /\ tr2 = [state |-> "coming"]
  283. /\ tr3 = [state |-> "free"]
  284. /\ tr4 = [state |-> "leaving"]
  285. /\ trC = [state |-> "free"]
  286. /\ trD = [state |-> "occupied"]
  287. /\ trF = [state |-> "free"]
  288. /\ trG = [state |-> "occupied"]
  289. /\ counter = 0
  290. /\ sw1 = [position |-> 1]
  291. /\ sw2 = [position |-> 1]
  292. /\ sw3 = [position |-> 1]
  293. /\ sw4 = [position |-> 1]
  294. /\ sw5 = [position |-> 1]
  295. /\ sw6 = [position |-> 2]
  296.  
  297. State 17: <4toDend line 248, col 12 to line 251, col 92 of module TrainSystemSimple>
  298. /\ tr1 = [state |-> "occupied"]
  299. /\ tr2 = [state |-> "coming"]
  300. /\ tr3 = [state |-> "free"]
  301. /\ tr4 = [state |-> "free"]
  302. /\ trC = [state |-> "free"]
  303. /\ trD = [state |-> "free"]
  304. /\ trF = [state |-> "free"]
  305. /\ trG = [state |-> "occupied"]
  306. /\ counter = 0
  307. /\ sw1 = [position |-> 1]
  308. /\ sw2 = [position |-> 1]
  309. /\ sw3 = [position |-> 1]
  310. /\ sw4 = [position |-> 1]
  311. /\ sw5 = [position |-> 1]
  312. /\ sw6 = [position |-> 2]
  313.  
  314. State 18: <Gto2end line 390, col 12 to line 393, col 92 of module TrainSystemSimple>
  315. /\ tr1 = [state |-> "occupied"]
  316. /\ tr2 = [state |-> "occupied"]
  317. /\ tr3 = [state |-> "free"]
  318. /\ tr4 = [state |-> "free"]
  319. /\ trC = [state |-> "free"]
  320. /\ trD = [state |-> "free"]
  321. /\ trF = [state |-> "free"]
  322. /\ trG = [state |-> "free"]
  323. /\ counter = 0
  324. /\ sw1 = [position |-> 1]
  325. /\ sw2 = [position |-> 1]
  326. /\ sw3 = [position |-> 1]
  327. /\ sw4 = [position |-> 1]
  328. /\ sw5 = [position |-> 1]
  329. /\ sw6 = [position |-> 2]
  330.  
  331. State 19: <1toFbegin line 253, col 14 to line 257, col 94 of module TrainSystemSimple>
  332. /\ tr1 = [state |-> "leaving"]
  333. /\ tr2 = [state |-> "occupied"]
  334. /\ tr3 = [state |-> "free"]
  335. /\ tr4 = [state |-> "free"]
  336. /\ trC = [state |-> "free"]
  337. /\ trD = [state |-> "free"]
  338. /\ trF = [state |-> "occupied"]
  339. /\ trG = [state |-> "free"]
  340. /\ counter = 0
  341. /\ sw1 = [position |-> 1]
  342. /\ sw2 = [position |-> 1]
  343. /\ sw3 = [position |-> 1]
  344. /\ sw4 = [position |-> 1]
  345. /\ sw5 = [position |-> 1]
  346. /\ sw6 = [position |-> 2]
  347.  
  348. State 20: <SwitchPosition6 line 527, col 20 to line 528, col 105 of module TrainSystemSimple>
  349. /\ tr1 = [state |-> "leaving"]
  350. /\ tr2 = [state |-> "occupied"]
  351. /\ tr3 = [state |-> "free"]
  352. /\ tr4 = [state |-> "free"]
  353. /\ trC = [state |-> "free"]
  354. /\ trD = [state |-> "free"]
  355. /\ trF = [state |-> "occupied"]
  356. /\ trG = [state |-> "free"]
  357. /\ counter = 0
  358. /\ sw1 = [position |-> 1]
  359. /\ sw2 = [position |-> 1]
  360. /\ sw3 = [position |-> 1]
  361. /\ sw4 = [position |-> 1]
  362. /\ sw5 = [position |-> 1]
  363. /\ sw6 = [position |-> 1]
  364.  
  365. State 21: <1toFend line 259, col 12 to line 262, col 92 of module TrainSystemSimple>
  366. /\ tr1 = [state |-> "free"]
  367. /\ tr2 = [state |-> "occupied"]
  368. /\ tr3 = [state |-> "free"]
  369. /\ tr4 = [state |-> "free"]
  370. /\ trC = [state |-> "free"]
  371. /\ trD = [state |-> "free"]
  372. /\ trF = [state |-> "free"]
  373. /\ trG = [state |-> "free"]
  374. /\ counter = 0
  375. /\ sw1 = [position |-> 1]
  376. /\ sw2 = [position |-> 1]
  377. /\ sw3 = [position |-> 1]
  378. /\ sw4 = [position |-> 1]
  379. /\ sw5 = [position |-> 1]
  380. /\ sw6 = [position |-> 1]
  381.  
  382. State 22: <2toGbegin line 373, col 14 to line 377, col 94 of module TrainSystemSimple>
  383. /\ tr1 = [state |-> "free"]
  384. /\ tr2 = [state |-> "leaving"]
  385. /\ tr3 = [state |-> "free"]
  386. /\ tr4 = [state |-> "free"]
  387. /\ trC = [state |-> "free"]
  388. /\ trD = [state |-> "free"]
  389. /\ trF = [state |-> "free"]
  390. /\ trG = [state |-> "occupied"]
  391. /\ counter = 0
  392. /\ sw1 = [position |-> 1]
  393. /\ sw2 = [position |-> 1]
  394. /\ sw3 = [position |-> 1]
  395. /\ sw4 = [position |-> 1]
  396. /\ sw5 = [position |-> 1]
  397. /\ sw6 = [position |-> 1]
  398.  
  399. State 23: <SwitchPosition4 line 521, col 20 to line 522, col 105 of module TrainSystemSimple>
  400. /\ tr1 = [state |-> "free"]
  401. /\ tr2 = [state |-> "leaving"]
  402. /\ tr3 = [state |-> "free"]
  403. /\ tr4 = [state |-> "free"]
  404. /\ trC = [state |-> "free"]
  405. /\ trD = [state |-> "free"]
  406. /\ trF = [state |-> "free"]
  407. /\ trG = [state |-> "occupied"]
  408. /\ counter = 0
  409. /\ sw1 = [position |-> 1]
  410. /\ sw2 = [position |-> 1]
  411. /\ sw3 = [position |-> 1]
  412. /\ sw4 = [position |-> 2]
  413. /\ sw5 = [position |-> 1]
  414. /\ sw6 = [position |-> 1]
  415.  
  416. Back to state 2: <2toGend line 379, col 12 to line 382, col 92 of module TrainSystemSimple>
  417.  
  418. Finished checking temporal properties in 05s at 2018-05-25 20:41:17
  419. 206542 states generated, 44944 distinct states found, 6018 states left on queue.
  420. Finished in 01min 12s at (2018-05-25 20:41:18)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!