API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Feb 24th, 2020
97
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 10.27 KB | None | 0 0
raw download clone embed print report
  1. /************************************************
  2. * TP1 Mini Contrôle ferroviaire
  3. * Réalisé par :
  4. * Alex Lacasse (111 239 094)
  5. * Antoine Olivier (111 175 276)
  6. * Philippe Audet (111 238 832)
  7. * Samuel Comeau (111 181 237)
  8. ************************************************/
  9.  
  10. const LA = 5
  11. const LB = 7
  12. const LC = 5
  13.  
  14. A = A[1],
  15. A[i:1..LA] = (when (i < LA && i != 2 && i != 4 ) t[i] -> A[i+1] |
  16. when (i == 2) entreeAB -> t[i] -> sortieAB -> A[i+1] |
  17. when (i == 4) entreeABC -> t[i] -> sortieABC -> A[i+1] |
  18. when (i == LA) t[i] -> A ).
  19.  
  20. ||TrainA = a:A.
  21.  
  22. B = B[1],
  23. B[i:1..LB] = (when (i < LB && i != 2 && i != 4 && i != 6 ) t[i] -> B[i+1] |
  24. when (i == 2) entreeAB -> t[i] -> sortieAB -> B[i+1] |
  25. when (i == 4) entreeBC -> t[i] -> sortieBC -> B[i+1] |
  26. when (i == 6) entreeABC -> t[i] -> sortieABC -> B[i+1] |
  27. when (i == LB) t[i] -> B).
  28.  
  29. ||TrainB = b:B.
  30.  
  31. C = C[1],
  32. C[i:1..LC] = (when (i < LC && i != 2 && i != 4 ) t[i] -> C[i+1] |
  33. when (i == 2) entreeBC -> t[i] -> sortieBC -> C[i+1] |
  34. when (i == 4) entreeABC -> t[i] -> sortieABC -> C[i+1] |
  35. when (i == LC) t[i] -> C ).
  36.  
  37. ||TrainC = c:C.
  38.  
  39. ||Reseau1 = (TrainA || TrainB || TrainC) .
  40.  
  41. /************************************************
  42. * Question #1
  43. * Trace violant la propriété P1 :
  44. * a.t.1 -> a.entreeAB
  45. * b.t.1 -> b.entreeAB
  46. * ERROR
  47. * Trace violant la propriété P2 :
  48. * b.t.1 -> b.entreeAB -> b.t.2 -> b.sortieAB -> b.t.3 -> b.entreeBC
  49. * c.t.1 -> c.entreeBC
  50. * ERROR
  51. * Trace violant la propriété P3 :
  52. * a.t.1 -> a.entreeAB -> a.t.2 -> a.sortieAB -> a.t.3 -> a.entreeABC
  53. * c.t.1 -> c.entreeBC -> c.t.2 -> c.sortieBC -> c.t.3 -> c.entreeABC
  54. * ERROR
  55. ************************************************/
  56. property P1 =({a,b}.entreeAB->{a,b}.sortieAB->P1).
  57. property P2 =({b,c}.entreeBC->{b,c}.sortieBC->P2).
  58. property P3 =({a,b,c}.entreeABC->{a,b,c}.sortieABC->P3).
  59.  
  60. ||TestExclusionMutuelle = (Reseau1 || P1 || P2 || P3).
  61.  
  62. /************************************************
  63. * Question #2
  64. * Preuve que ça marche :
  65. * a.a.t.1 -> a.entreeAB -> a.a.t.2 -> a.sortieAB
  66. * b.b.t.1 (ne peut pas entrer dans entreeAB, car a est déjà entrée)
  67. ************************************************/
  68. ||TrainA2 = a:A / {entreeAB / a.entreeAB, sortieAB / a.sortieAB, entreeABC / a.entreeABC, sortieABC / a.sortieABC }.
  69. ||TrainB2 = b:B / {entreeAB / b.entreeAB, sortieAB / b.sortieAB, entreeBC / b.entreeBC, sortieBC / b.sortieBC, entreeABC / b.entreeABC, sortieABC / b.sortieABC }.
  70. ||TrainC2 = c:C / {entreeBC / c.entreeBC, sortieBC / c.sortieBC, entreeABC / c.entreeABC, sortieABC / c.sortieABC }.
  71.  
  72. LOCK_AB = ( entreeAB -> sortieAB -> LOCK_AB ).
  73. LOCK_BC = ( entreeBC -> sortieBC -> LOCK_BC ).
  74. LOCK_ABC = ( entreeABC -> sortieABC -> LOCK_ABC ).
  75.  
  76. ||Reseau2 = (a:TrainA2 || b:TrainB2 || c:TrainC2 || {a, b, c}::LOCK_AB || {a,b,c}::LOCK_ABC || {a,b,c}::LOCK_BC).
  77.  
  78. /************************************************
  79. * Question #3
  80. ************************************************/
  81. const N=2
  82. range T = 0..N
  83. range ID = 1..N
  84.  
  85. DEPASSE_PAS_AB1 = C1[1],
  86. C1[i:ID] = ( [i].entreeAB -> C1[i%N+1] ).
  87. DEPASSE_PAS_AB2 = C2[1],
  88. C2[i:ID] = ( [i].sortieAB -> C2[i%N+1] ).
  89.  
  90. DEPASSE_PAS_BC1 = C1[1],
  91. C1[i:ID] = ( [i].entreeBC -> C1[i%N+1] ).
  92. DEPASSE_PAS_BC2 = C2[1],
  93. C2[i:ID] = ( [i].sortieBC -> C2[i%N+1] ).
  94.  
  95. DEPASSE_PAS_ABC1 = C1[1],
  96. C1[i:ID] = ( [i].entreeABC -> C1[i%N+1] ).
  97. DEPASSE_PAS_ABC2 = C2[1],
  98. C2[i:ID] = ( [i].sortieABC -> C2[i%N+1] ).
  99.  
  100. ||CONVOI_A = ([i:ID]:TrainA2 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  101. ||CONVOI_B = ([i:ID]:TrainB2 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  102. ||CONVOI_C = ([i:ID]:TrainC2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  103.  
  104. ||TRAINS = (trainA:CONVOI_A || trainB: CONVOI_B || trainC: CONVOI_C).
  105.  
  106. CHEMIN_AB = CHEMIN_AB[0][0],
  107. CHEMIN_AB[na:T][nb:T]= (
  108. when (nb ==0) trainA[i:ID].entreeAB -> CHEMIN_AB[na+1][nb]|
  109. trainA[j:ID].sortieAB -> CHEMIN_AB[na-1][nb]|
  110. when (na ==0) trainB[i:ID].entreeAB -> CHEMIN_AB[na][nb+1]|
  111. trainB[j:ID].sortieAB -> CHEMIN_AB[na][nb-1]).
  112.  
  113. CHEMIN_BC = CHEMIN_BC[0][0],
  114. CHEMIN_BC[nb:T][nc:T]= (
  115. when (nc ==0) trainB[i:ID].entreeBC -> CHEMIN_BC[nb+1][nc]|
  116. trainB[j:ID].sortieBC -> CHEMIN_BC[nb-1][nc]|
  117. when (nb ==0) trainC[i:ID].entreeBC -> CHEMIN_BC[nb][nc+1]|
  118. trainC[j:ID].sortieBC -> CHEMIN_BC[nb][nc-1]).
  119.  
  120. CHEMIN_ABC = CHEMIN_ABC[0][0][0],
  121. CHEMIN_ABC[na:T][nb:T][nc:T]= (
  122. when (nc ==0 && na ==0) trainB[i:ID].entreeABC -> CHEMIN_ABC[na][nb+1][nc]|
  123. trainB[j:ID].sortieABC -> CHEMIN_ABC[na][nb-1][nc]|
  124. when (nc ==0 && nb ==0) trainA[i:ID].entreeABC -> CHEMIN_ABC[na+1][nb][nc]|
  125. trainA[j:ID].sortieABC -> CHEMIN_ABC[na-1][nb][nc]|
  126. when (na ==0 && nb ==0) trainC[i:ID].entreeABC -> CHEMIN_ABC[na][nb][nc+1]|
  127. trainC[j:ID].sortieABC -> CHEMIN_ABC[na][nb][nc-1]).
  128.  
  129. ||Reseau3 = ( CHEMIN_AB || CHEMIN_BC || CHEMIN_ABC || TRAINS).
  130. /************************************************
  131. * Question #4
  132. *Aucun blocage
  133. *On a du progrès
  134. ************************************************/
  135. property P41 = CHEMIN_AB[0][0],
  136. CHEMIN_AB[na:T][nb:T]= (
  137. when (nb ==0) trainA[i:ID].entreeAB -> CHEMIN_AB[na+1][nb]|
  138. trainA[j:ID].sortieAB -> CHEMIN_AB[na-1][nb]|
  139. when (na ==0) trainB[i:ID].entreeAB -> CHEMIN_AB[na][nb+1]|
  140. trainB[j:ID].sortieAB -> CHEMIN_AB[na][nb-1]).
  141.  
  142. property P42 = CHEMIN_BC[0][0],
  143. CHEMIN_BC[nb:T][nc:T]= (
  144. when (nc ==0) trainB[i:ID].entreeBC -> CHEMIN_BC[nb+1][nc]|
  145. trainB[j:ID].sortieBC -> CHEMIN_BC[nb-1][nc]|
  146. when (nb ==0) trainC[i:ID].entreeBC -> CHEMIN_BC[nb][nc+1]|
  147. trainC[j:ID].sortieBC -> CHEMIN_BC[nb][nc-1]).
  148.  
  149. property P43 = CHEMIN_ABC[0][0][0],
  150. CHEMIN_ABC[na:T][nb:T][nc:T]= (
  151. when (nc ==0 && na ==0) trainB[i:ID].entreeABC -> CHEMIN_ABC[na][nb+1][nc]|
  152. trainB[j:ID].sortieABC -> CHEMIN_ABC[na][nb-1][nc]|
  153. when (nc ==0 && nb ==0) trainA[i:ID].entreeABC -> CHEMIN_ABC[na+1][nb][nc]|
  154. trainA[j:ID].sortieABC -> CHEMIN_ABC[na-1][nb][nc]|
  155. when (na ==0 && nb ==0) trainC[i:ID].entreeABC -> CHEMIN_ABC[na][nb][nc+1]|
  156. trainC[j:ID].sortieABC -> CHEMIN_ABC[na][nb][nc-1]).
  157.  
  158. ||Reseau4 = (Reseau3 ||P41 ||P42 ||P43 ).
  159. /************************************************
  160. * Question #5
  161. *Aucun blocage
  162. *On a du progrès
  163. ************************************************/
  164. property P51 = C1[1],
  165. C1[i:ID] = ( [i].entreeAB -> C1[i%N+1] ).
  166. property P52 = C2[1],
  167. C2[i:ID] = ( [i].sortieAB -> C2[i%N+1] ).
  168.  
  169. property P53 = C1[1],
  170. C1[i:ID] = ( [i].entreeBC -> C1[i%N+1] ).
  171. property P54 = C2[1],
  172. C2[i:ID] = ( [i].sortieBC -> C2[i%N+1] ).
  173.  
  174. property P55 = C1[1],
  175. C1[i:ID] = ( [i].entreeABC -> C1[i%N+1] ).
  176. property P56 = C2[1],
  177. C2[i:ID] = ( [i].sortieABC -> C2[i%N+1] ).
  178.  
  179. ||CONVOI_A_5 = ([i:ID]:TrainA2 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 || P51 || P52 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 || P55 || P56 ).
  180. ||CONVOI_B_5 = ([i:ID]:TrainB2 ||DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 || P51 || P52 || P53 || P54 || P55 || P56 ).
  181. ||CONVOI_C_5 = ([i:ID]:TrainC2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ||P53 || P54 || P55 || P56 ).
  182.  
  183. ||TRAINS_5 = (trainA:CONVOI_A_5 || trainB: CONVOI_B_5 || trainC: CONVOI_C_5).
  184.  
  185. ||Reseau5 =(CHEMIN_AB || CHEMIN_BC || CHEMIN_ABC || TRAINS_5 ||P41 ||P42 ||P43).
  186. /************************************************
  187. * Question #6
  188. * Le système est robuste
  189. * Aucun blocage
  190. * On a du progrès
  191. ************************************************/
  192. set ActionsTrainA = {a.{entreeAB, sortieAB, entreeABC, sortieABC}}
  193.  
  194. ||Reseau6 =(Reseau5) >> {[i:1..N].ActionsTrainA}.
  195. /************************************************
  196. * Question #7
  197. * On force l'entrée dans les troncons en alterance.
  198. * pour AB a envoit son premier train et ensuite c'est le tour de b et ainsi de suite.
  199. * le comportement est similaire pour BC et ABC.
  200. * Cependant ceci force l'attente des trains aux tronçons lorsqu'il n'arrive pas dans le bon ordre.
  201. ************************************************/
  202. CHEMIN_AB_ORDRE = (trainA.[1..N].entreeAB -> trainA.[1..N].sortieAB -> trainB.[1..N].entreeAB -> trainB.[1..N].sortieAB -> CHEMIN_AB_ORDRE).
  203.  
  204. CHEMIN_BC_ORDRE = (trainB.[1..N].entreeBC -> trainB.[1..N].sortieBC -> trainC.[1..N].entreeBC -> trainC.[1..N].sortieBC -> CHEMIN_BC_ORDRE).
  205.  
  206. CHEMIN_ABC_ORDRE = (trainA.[1..N].entreeABC -> trainA.[1..N].sortieABC ->trainB.[1..N].entreeABC -> trainB.[1..N].sortieABC -> trainC.[1..N].entreeABC -> trainC.[1..N].sortieABC -> CHEMIN_ABC_ORDRE).
  207.  
  208. ||Reseau7 = (Reseau6 || CHEMIN_AB_ORDRE || CHEMIN_BC_ORDRE || CHEMIN_ABC_ORDRE).
  209.  
  210. /************************************************
  211. * Question #8
  212. ************************************************/
  213. TrainALeger = ( a.entreeAB -> a.sortieAB -> a.entreeABC -> a.sortieABC -> TrainALeger).
  214. TrainBLeger = ( b.entreeAB -> b.sortieAB -> b.entreeBC -> b.sortieBC -> b.entreeABC -> b.sortieABC -> TrainBLeger).
  215. TrainCLeger = ( c.entreeBC -> c.sortieBC -> c.entreeABC -> c.sortieABC -> TrainCLeger).
  216.  
  217. ||TrainA3 = (a:TrainALeger) / {entreeAB / a.a.entreeAB, sortieAB / a.a.sortieAB, entreeABC / a.a.entreeABC, sortieABC / a.a.sortieABC }.
  218. ||TrainB3 = (b:TrainBLeger) / {entreeAB / b.b.entreeAB, sortieAB / b.b.sortieAB, entreeBC / b.b.entreeBC, sortieBC / b.b.sortieBC, entreeABC / b.b.entreeABC, sortieABC / b.b.sortieABC }.
  219. ||TrainC3 = (c:TrainCLeger) / {entreeBC / c.c.entreeBC, sortieBC / c.c.sortieBC, entreeABC / c.c.entreeABC, sortieABC / c.c.sortieABC }.
  220.  
  221. ||CONVOI_A_LEGER = ([i:ID]:TrainA3 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  222. ||CONVOI_B_LEGER = ([i:ID]:TrainB3 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  223. ||CONVOI_C_LEGER = ([i:ID]:TrainC3 || DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
  224.  
  225. ||TRAINSLEGERS = (trainA:CONVOI_A_LEGER || trainB:CONVOI_B_LEGER || trainC:CONVOI_C_LEGER).
  226.  
  227. ||Reseau8 = ( CHEMIN_AB || CHEMIN_BC || CHEMIN_ABC || TRAINSLEGERS).
  228.  
  229. /************************************************
  230. * Question #9
  231. * Le progrès est bel et bien absent
  232. ************************************************/
  233. set ActionsTrainA2 = {entreeAB, sortieAB, entreeABC, sortieABC}
  234.  
  235. ||Reseau9 =(Reseau8) >> {trainA.[1..N].ActionsTrainA2}.
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!