API tools faq
paste
Advertisement
Guest User

tlcoutput

a guest
May 24th, 2018
90
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 5.79 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 1803MB heap and 64MB offheap memory (Windows 10 10.0 amd64, Oracle Corporation 1.8.0_60 x86_64).
  3. Parsing file C:\Users\Robbe\Desktop\School\2017-2018\2e-semester\formele-systeemmodellering\tla-oefeningen\tla-project\TrainSystem.tla
  4. Parsing file C:\tla\tla2sany\StandardModules\Naturals.tla
  5. Parsing file C:\Users\Robbe\Desktop\School\2017-2018\2e-semester\formele-systeemmodellering\tla-oefeningen\tla-project\Track.tla
  6. Parsing file C:\Users\Robbe\Desktop\School\2017-2018\2e-semester\formele-systeemmodellering\tla-oefeningen\tla-project\StationTrack.tla
  7. Parsing file C:\Users\Robbe\Desktop\School\2017-2018\2e-semester\formele-systeemmodellering\tla-oefeningen\tla-project\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 TrainSystem
  13. Starting... (2018-05-24 14:08:29)
  14. Computing initial states...
  15. Finished computing initial states: 4096 distinct states generated.
  16. Progress(3) at 2018-05-24 14:08:33: 116391 states generated (116.391 s/min), 36845 distinct states found (36.845 ds/min), 29524 states left on queue.
  17. Error: Invariant countsmall is violated.
  18. Error: The behavior up to this point is:
  19. State 1: <Initial predicate>
  20. /\ tr1 = [state |-> "free"]
  21. /\ tr2 = [state |-> "free"]
  22. /\ tr3 = [state |-> "free"]
  23. /\ tr4 = [state |-> "free"]
  24. /\ trA = [state |-> "free"]
  25. /\ trB = [state |-> "free"]
  26. /\ trC = [state |-> "free"]
  27. /\ trD = [state |-> "free"]
  28. /\ trF = [state |-> "free"]
  29. /\ trG = [state |-> "free"]
  30. /\ count = 0
  31. /\ sw10 = [position |-> 1]
  32. /\ sw11 = [position |-> 1]
  33. /\ sw12 = [position |-> 1]
  34. /\ sw1 = [position |-> 1]
  35. /\ sw2 = [position |-> 1]
  36. /\ sw3 = [position |-> 1]
  37. /\ sw4 = [position |-> 1]
  38. /\ sw5 = [position |-> 1]
  39. /\ sw6 = [position |-> 1]
  40. /\ sw7 = [position |-> 1]
  41. /\ sw8 = [position |-> 1]
  42. /\ sw9 = [position |-> 1]
  43.  
  44. State 2: <Nextlol line 957, col 12 to line 957, col 27 of module TrainSystem>
  45. /\ tr1 = [state |-> "comingWest"]
  46. /\ tr2 = [state |-> "free"]
  47. /\ tr3 = [state |-> "free"]
  48. /\ tr4 = [state |-> "free"]
  49. /\ trA = [state |-> "occupied"]
  50. /\ trB = [state |-> "free"]
  51. /\ trC = [state |-> "free"]
  52. /\ trD = [state |-> "free"]
  53. /\ trF = [state |-> "free"]
  54. /\ trG = [state |-> "free"]
  55. /\ count = 1
  56. /\ sw10 = [position |-> 1]
  57. /\ sw11 = [position |-> 1]
  58. /\ sw12 = [position |-> 1]
  59. /\ sw1 = [position |-> 1]
  60. /\ sw2 = [position |-> 1]
  61. /\ sw3 = [position |-> 1]
  62. /\ sw4 = [position |-> 1]
  63. /\ sw5 = [position |-> 1]
  64. /\ sw6 = [position |-> 1]
  65. /\ sw7 = [position |-> 1]
  66. /\ sw8 = [position |-> 1]
  67. /\ sw9 = [position |-> 1]
  68.  
  69. State 3: <Nextlol line 957, col 12 to line 957, col 27 of module TrainSystem>
  70. /\ tr1 = [state |-> "occupied"]
  71. /\ tr2 = [state |-> "free"]
  72. /\ tr3 = [state |-> "free"]
  73. /\ tr4 = [state |-> "free"]
  74. /\ trA = [state |-> "free"]
  75. /\ trB = [state |-> "free"]
  76. /\ trC = [state |-> "free"]
  77. /\ trD = [state |-> "free"]
  78. /\ trF = [state |-> "free"]
  79. /\ trG = [state |-> "free"]
  80. /\ count = 2
  81. /\ sw10 = [position |-> 1]
  82. /\ sw11 = [position |-> 1]
  83. /\ sw12 = [position |-> 1]
  84. /\ sw1 = [position |-> 1]
  85. /\ sw2 = [position |-> 1]
  86. /\ sw3 = [position |-> 1]
  87. /\ sw4 = [position |-> 1]
  88. /\ sw5 = [position |-> 1]
  89. /\ sw6 = [position |-> 1]
  90. /\ sw7 = [position |-> 1]
  91. /\ sw8 = [position |-> 1]
  92. /\ sw9 = [position |-> 1]
  93.  
  94. State 4: <Nextlol line 957, col 12 to line 957, col 27 of module TrainSystem>
  95. /\ tr1 = [state |-> "leavingEast"]
  96. /\ tr2 = [state |-> "free"]
  97. /\ tr3 = [state |-> "free"]
  98. /\ tr4 = [state |-> "free"]
  99. /\ trA = [state |-> "occupied"]
  100. /\ trB = [state |-> "free"]
  101. /\ trC = [state |-> "free"]
  102. /\ trD = [state |-> "free"]
  103. /\ trF = [state |-> "free"]
  104. /\ trG = [state |-> "free"]
  105. /\ count = 3
  106. /\ sw10 = [position |-> 1]
  107. /\ sw11 = [position |-> 1]
  108. /\ sw12 = [position |-> 1]
  109. /\ sw1 = [position |-> 1]
  110. /\ sw2 = [position |-> 1]
  111. /\ sw3 = [position |-> 1]
  112. /\ sw4 = [position |-> 1]
  113. /\ sw5 = [position |-> 1]
  114. /\ sw6 = [position |-> 1]
  115. /\ sw7 = [position |-> 1]
  116. /\ sw8 = [position |-> 1]
  117. /\ sw9 = [position |-> 1]
  118.  
  119. State 5: <Nextlol line 957, col 12 to line 957, col 27 of module TrainSystem>
  120. /\ tr1 = [state |-> "free"]
  121. /\ tr2 = [state |-> "free"]
  122. /\ tr3 = [state |-> "free"]
  123. /\ tr4 = [state |-> "free"]
  124. /\ trA = [state |-> "free"]
  125. /\ trB = [state |-> "free"]
  126. /\ trC = [state |-> "free"]
  127. /\ trD = [state |-> "free"]
  128. /\ trF = [state |-> "free"]
  129. /\ trG = [state |-> "free"]
  130. /\ count = 4
  131. /\ sw10 = [position |-> 1]
  132. /\ sw11 = [position |-> 1]
  133. /\ sw12 = [position |-> 1]
  134. /\ sw1 = [position |-> 1]
  135. /\ sw2 = [position |-> 1]
  136. /\ sw3 = [position |-> 1]
  137. /\ sw4 = [position |-> 1]
  138. /\ sw5 = [position |-> 1]
  139. /\ sw6 = [position |-> 1]
  140. /\ sw7 = [position |-> 1]
  141. /\ sw8 = [position |-> 1]
  142. /\ sw9 = [position |-> 1]
  143.  
  144. State 6: <Nextlol line 957, col 12 to line 957, col 27 of module TrainSystem>
  145. /\ tr1 = [state |-> "comingWest"]
  146. /\ tr2 = [state |-> "free"]
  147. /\ tr3 = [state |-> "free"]
  148. /\ tr4 = [state |-> "free"]
  149. /\ trA = [state |-> "occupied"]
  150. /\ trB = [state |-> "free"]
  151. /\ trC = [state |-> "free"]
  152. /\ trD = [state |-> "free"]
  153. /\ trF = [state |-> "free"]
  154. /\ trG = [state |-> "free"]
  155. /\ count = 5
  156. /\ sw10 = [position |-> 1]
  157. /\ sw11 = [position |-> 1]
  158. /\ sw12 = [position |-> 1]
  159. /\ sw1 = [position |-> 1]
  160. /\ sw2 = [position |-> 1]
  161. /\ sw3 = [position |-> 1]
  162. /\ sw4 = [position |-> 1]
  163. /\ sw5 = [position |-> 1]
  164. /\ sw6 = [position |-> 1]
  165. /\ sw7 = [position |-> 1]
  166. /\ sw8 = [position |-> 1]
  167. /\ sw9 = [position |-> 1]
  168.  
  169. 2161784 states generated, 352912 distinct states found, 179565 states left on queue.
  170. The depth of the complete state graph search is 6.
  171. The average outdegree of the complete state graph is 2 (minimum is 0, the maximum 18 and the 95th percentile is 5).
  172. Finished in 37s at (2018-05-24 14:09:05)
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!