Permalink
Browse files

refinement for lifeness

  • Loading branch information...
1 parent be28610 commit fb917de33328d729a0a1c483bbfa62025fb5bacf Adrian Friedli committed Dec 2, 2010
Showing with 48,796 additions and 14,385 deletions.
  1. +1 −1 rodin/ctx6_conv_utils.bcc
  2. +2 −2 rodin/ctx6_conv_utils.bpo
  3. +1 −0 rodin/ctx6_conv_utils.bpr
  4. +2 −2 rodin/ctx6_conv_utils.buc
  5. +6 −6 rodin/lift02_main_engine.bcm
  6. +55 −12 rodin/lift02_main_engine.bpo
  7. +354 −0 rodin/lift02_main_engine.bpr
  8. +7 −2 rodin/lift02_main_engine.bps
  9. +7 −7 rodin/lift02_main_engine.bum
  10. +4 −4 rodin/lift03_door_engine.bcm
  11. +2 −2 rodin/lift03_door_engine.bpo
  12. +65 −64 rodin/lift04_phys_main_engine.bcm
  13. +146 −75 rodin/lift04_phys_main_engine.bpo
  14. +1,243 −530 rodin/lift04_phys_main_engine.bpr
  15. +10 −2 rodin/lift04_phys_main_engine.bps
  16. +21 −18 rodin/lift04_phys_main_engine.bum
  17. +60 −59 rodin/lift05_phys_door.bcm
  18. +39 −38 rodin/lift05_phys_door.bpo
  19. +65 −64 rodin/lift06_buttons.bcm
  20. +41 −40 rodin/lift06_buttons.bpo
  21. +70 −69 rodin/lift07_up_buttons.bcm
  22. +46 −45 rodin/lift07_up_buttons.bpo
  23. +77 −76 rodin/lift08_down_buttons.bcm
  24. +51 −50 rodin/lift08_down_buttons.bpo
  25. +152 −145 rodin/lift09_scheduler.bcm
  26. +89 −82 rodin/lift09_scheduler.bpo
  27. +1,039 −937 rodin/lift09_scheduler.bpr
  28. +59 −53 rodin/lift09_scheduler.bum
  29. +207 −198 rodin/lift10_final.bcm
  30. +517 −500 rodin/lift10_final.bpo
  31. +12 −0 rodin/lift10_final.bpr
  32. +157 −156 rodin/lift10_final.bps
  33. +53 −48 rodin/lift10_final.bum
  34. +159 −165 rodin/lift11_conv_add_req.bcm
  35. +228 −90 rodin/lift11_conv_add_req.bpo
  36. +8,046 −2 rodin/lift11_conv_add_req.bpr
  37. +19 −2 rodin/lift11_conv_add_req.bps
  38. +51 −64 rodin/lift11_conv_add_req.bum
  39. +108 −114 rodin/lift12_conv_lights.bcm
  40. +80 −86 rodin/lift12_conv_lights.bpo
  41. +108 −114 rodin/lift13_conv_lights.bcm
  42. +80 −86 rodin/lift13_conv_lights.bpo
  43. +108 −114 rodin/lift14_conv_lights.bcm
  44. +80 −86 rodin/lift14_conv_lights.bpo
  45. +108 −114 rodin/lift15_conv_lights.bcm
  46. +80 −86 rodin/lift15_conv_lights.bpo
  47. +1,304 −1,146 rodin/lift15_conv_lights.bpr
  48. +108 −114 rodin/lift16_conv_lights.bcm
  49. +80 −86 rodin/lift16_conv_lights.bpo
  50. +108 −114 rodin/lift17_conv_lights.bcm
  51. +80 −86 rodin/lift17_conv_lights.bpo
  52. +108 −114 rodin/lift18_conv_lights.bcm
  53. +80 −86 rodin/lift18_conv_lights.bpo
  54. +108 −114 rodin/lift19_conv_lights.bcm
  55. +80 −86 rodin/lift19_conv_lights.bpo
  56. +991 −840 rodin/lift19_conv_lights.bpr
  57. +109 −115 rodin/lift20_conv_schedule.bcm
  58. +214 −220 rodin/lift20_conv_schedule.bpo
  59. +1,387 −1,116 rodin/lift20_conv_schedule.bpr
  60. +49 −49 rodin/lift20_conv_schedule.bps
  61. +109 −115 rodin/lift21_conv_move.bcm
  62. +186 −192 rodin/lift21_conv_move.bpo
  63. +147 −146 rodin/lift21_conv_move.bpr
  64. +21 −21 rodin/lift21_conv_move.bps
  65. +109 −115 rodin/lift22_conv_move.bcm
  66. +185 −191 rodin/lift22_conv_move.bpo
  67. +20 −20 rodin/lift22_conv_move.bps
  68. +109 −115 rodin/lift23_conv_move.bcm
  69. +183 −189 rodin/lift23_conv_move.bpo
  70. +18 −18 rodin/lift23_conv_move.bps
  71. +109 −115 rodin/lift24_conv_move.bcm
  72. +183 −189 rodin/lift24_conv_move.bpo
  73. +18 −18 rodin/lift24_conv_move.bps
  74. +109 −115 rodin/lift25_conv_move.bcm
  75. +180 −186 rodin/lift25_conv_move.bpo
  76. +15 −15 rodin/lift25_conv_move.bps
  77. +109 −115 rodin/lift26_conv_move.bcm
  78. +179 −185 rodin/lift26_conv_move.bpo
  79. +14 −14 rodin/lift26_conv_move.bps
  80. +110 −116 rodin/lift27_conv_door.bcm
  81. +191 −197 rodin/lift27_conv_door.bpo
  82. +448 −416 rodin/lift27_conv_door.bpr
  83. +26 −26 rodin/lift27_conv_door.bps
  84. +110 −116 rodin/lift28_conv_door.bcm
  85. +178 −184 rodin/lift28_conv_door.bpo
  86. +12 −12 rodin/lift28_conv_door.bps
  87. +110 −116 rodin/lift29_conv_door.bcm
  88. +177 −183 rodin/lift29_conv_door.bpo
  89. +11 −11 rodin/lift29_conv_door.bps
  90. +110 −116 rodin/lift30_conv_door.bcm
  91. +176 −182 rodin/lift30_conv_door.bpo
  92. +10 −10 rodin/lift30_conv_door.bps
  93. +110 −116 rodin/lift31_conv_door.bcm
  94. +183 −189 rodin/lift31_conv_door.bpo
  95. +17 −17 rodin/lift31_conv_door.bps
  96. +110 −116 rodin/lift32_conv_door.bcm
  97. +174 −180 rodin/lift32_conv_door.bpo
  98. +8 −8 rodin/lift32_conv_door.bps
  99. +110 −116 rodin/lift33_conv_door.bcm
  100. +173 −179 rodin/lift33_conv_door.bpo
  101. +7 −7 rodin/lift33_conv_door.bps
  102. +110 −116 rodin/lift34_conv_door.bcm
  103. +172 −178 rodin/lift34_conv_door.bpo
  104. +6 −6 rodin/lift34_conv_door.bps
  105. +110 −116 rodin/lift35_conv_door.bcm
  106. +171 −177 rodin/lift35_conv_door.bpo
  107. +5 −5 rodin/lift35_conv_door.bps
  108. +164 −166 rodin/lift36_conv_buttons.bcm
  109. +384 −183 rodin/lift36_conv_buttons.bpo
  110. +17,481 −0 rodin/lift36_conv_buttons.bpr
  111. +30 −7 rodin/lift36_conv_buttons.bps
  112. +52 −48 rodin/lift36_conv_buttons.bum
  113. +534 −0 rodin/lift37_lifeness.bcm
  114. +566 −0 rodin/lift37_lifeness.bpo
  115. +5,570 −0 rodin/lift37_lifeness.bpr
  116. +4 −0 rodin/lift37_lifeness.bps
  117. +152 −0 rodin/lift37_lifeness.bum
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
-<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx5_scheduler.bcc|org.eventb.core.scContextFile#ctx5_scheduler" org.eventb.core.source="/ProvenLift/ctx6_conv_utils.buc|org.eventb.core.contextFile#ctx6_conv_utils|org.eventb.core.extendsContext#_FysWEfiGEd-5bJQIzgxuHg"/>
+<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx5_scheduler.bcc|org.eventb.core.scContextFile#ctx5_scheduler" org.eventb.core.source="/ProvenLift/ctx6_conv_utils.buc|org.eventb.core.contextFile#ctx6_conv_utils|org.eventb.core.extendsContext#_wb47EP4sEd-KA9ifxghDLw"/>
<org.eventb.core.scInternalContext name="ctx1_floors">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1_1" org.eventb.core.predicate="LAST_FLOOR∈ℕ1" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.axiom#_lTa6wdd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="LAST_FLOOR" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.constant#_lTa6wNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
@@ -1,5 +1,5 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="0">
+<org.eventb.core.poFile org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="LAST_FLOOR" org.eventb.core.type="ℤ"/>
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="LAST_FLOOR∈ℕ1" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.axiom#_lTa6wdd9Ed-Dle0at0Xgqg"/>
@@ -56,7 +56,7 @@
<org.eventb.core.poPredicateSet name="HYPAXM2" org.eventb.core.parentSet="/ProvenLift/ctx6_conv_utils.bpo|org.eventb.core.poFile#ctx6_conv_utils|org.eventb.core.poPredicateSet#HYPAXM1" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="∀pos⦂ℤ·pos∈0 ‥ LAST_FLOOR⇒reachable(SCHEDULER_DOWN ↦ pos)=0 ‥ pos" org.eventb.core.source="/ProvenLift/ctx6_conv_utils.buc|org.eventb.core.contextFile#ctx6_conv_utils|org.eventb.core.axiom#_FyuyUPiGEd-5bJQIzgxuHg"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/ProvenLift/ctx6_conv_utils.bpo|org.eventb.core.poFile#ctx6_conv_utils|org.eventb.core.poPredicateSet#HYPAXM2" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/ProvenLift/ctx6_conv_utils.bpo|org.eventb.core.poFile#ctx6_conv_utils|org.eventb.core.poPredicateSet#HYPAXM2" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="∀pos⦂ℤ·pos∈0 ‥ LAST_FLOOR⇒reachable(SCHEDULER_WAIT ↦ pos)=0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/ctx6_conv_utils.buc|org.eventb.core.contextFile#ctx6_conv_utils|org.eventb.core.axiom#_Fys9IPiGEd-5bJQIzgxuHg"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>
@@ -369,4 +369,5 @@
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="¬DOOR_OPENED=DOOR_HALF"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="∀pos⦂ℤ·pos∈0 ‥ LAST_FLOOR⇒reachable(SCHEDULER_UP ↦ pos)=pos ‥ LAST_FLOOR"/>
</org.eventb.core.prProof>
+<org.eventb.core.prProof name="f/THM"/>
</org.eventb.core.prFile>
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1290684064198" org.eventb.texttools.text_representation="context ctx6_conv_utils extends ctx5_scheduler&#10;&#10;constants reachable&#10;&#10;axioms&#10; @axm1 reachable ∈ SCHEDULER_STRATEGY × 0‥LAST_FLOOR → ℙ(0‥LAST_FLOOR)&#10; @axm2 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_UP↦pos) = pos‥LAST_FLOOR&#10; @axm3 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_DOWN↦pos) = 0‥pos&#10; @axm4 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_WAIT↦pos) = 0‥LAST_FLOOR&#10;&#10;end&#10;" version="3">
-<org.eventb.core.extendsContext name="_FysWEfiGEd-5bJQIzgxuHg" org.eventb.core.target="ctx5_scheduler"/>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1291305402602" org.eventb.texttools.text_representation="context ctx6_conv_utils extends ctx5_scheduler&#10;&#10;constants reachable&#10;&#10;axioms&#10; @axm1 reachable ∈ SCHEDULER_STRATEGY × 0‥LAST_FLOOR → ℙ(0‥LAST_FLOOR)&#10; @axm2 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_UP↦pos) = pos‥LAST_FLOOR&#10; @axm3 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_DOWN↦pos) = 0‥pos&#10; @axm4 ∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_WAIT↦pos) = 0‥LAST_FLOOR&#10;end&#10;" version="3">
+<org.eventb.core.extendsContext name="_wb47EP4sEd-KA9ifxghDLw" org.eventb.core.target="ctx5_scheduler"/>
<org.eventb.core.constant name="_FysWEviGEd-5bJQIzgxuHg" org.eventb.core.identifier="reachable"/>
<org.eventb.core.axiom name="_FytkMPiGEd-5bJQIzgxuHg" org.eventb.core.label="axm1" org.eventb.core.predicate="reachable ∈ SCHEDULER_STRATEGY × 0‥LAST_FLOOR → ℙ(0‥LAST_FLOOR)"/>
<org.eventb.core.axiom name="_FyuLQPiGEd-5bJQIzgxuHg" org.eventb.core.label="axm2" org.eventb.core.predicate="∀pos·pos∈0‥LAST_FLOOR ⇒ reachable(SCHEDULER_UP↦pos) = pos‥LAST_FLOOR"/>
@@ -1,7 +1,7 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
-<org.eventb.core.scRefinesMachine name="REF" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.refinesMachine#_d3ZPEPS-Ed-43_jmKUh78g"/>
-<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx2_main_engine.bcc" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.seesContext#_d3ZPEfS-Ed-43_jmKUh78g"/>
+<org.eventb.core.scRefinesMachine name="REF" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.refinesMachine#_SGJXwPvTEd-J48UG_gxxdg"/>
+<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx2_main_engine.bcc" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.seesContext#_SGJXwfvTEd-J48UG_gxxdg"/>
<org.eventb.core.scInternalContext name="ctx1_floors">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1_1" org.eventb.core.predicate="LAST_FLOOR∈ℕ1" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.axiom#_lTa6wdd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="LAST_FLOOR" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.constant#_lTa6wNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
@@ -23,6 +23,7 @@
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="dlf1_1" org.eventb.core.predicate="PhyElevatorFloor&lt;LAST_FLOOR∨0&lt;PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.invariant#_VO9DcNqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV3" org.eventb.core.label="inv2_1" org.eventb.core.predicate="ctrlCableCommand∈CABLE_COMMAND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.invariant#_1cMqQNd_Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV4" org.eventb.core.label="inv2_2" org.eventb.core.predicate="last_stop∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.invariant#_yC1egNqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
+<org.eventb.core.scInvariant name="INV5" org.eventb.core.label="inv2_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP⇒last_stop=PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.invariant#_SGJXwvvTEd-J48UG_gxxdg" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="PhyElevatorFloor" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.variable#_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="ctrlCableCommand" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.variable#_1cMDMtd_Ed-Dle0at0Xgqg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scVariable name="last_stop" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.variable#_d3ZPEvS-Ed-43_jmKUh78g" org.eventb.core.type="ℤ"/>
@@ -36,10 +37,9 @@
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC2sodqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="PhyElevatorFloor&lt;LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC2sotqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_WIND" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.action#_yC2so9qwEd-O4vbSPlarTw"/>
-<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ PhyElevatorFloor" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.action#_d3Z2IPS-Ed-43_jmKUh78g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="move_up" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm|org.eventb.core.scMachineFile#lift01_floors|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_d3adMPS-Ed-43_jmKUh78g"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm|org.eventb.core.scMachineFile#lift01_floors|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_SGJ-0PvTEd-J48UG_gxxdg"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="PhyElevatorFloor&lt;LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_9uFS0dd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorFloor ≔ PhyElevatorFloor+1" org.eventb.core.label="act1_1" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.action#_9uF54Nd9Ed-Dle0at0Xgqg"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_yC3TsdqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
@@ -48,10 +48,9 @@
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC36wdqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="PhyElevatorFloor&gt;0" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC36wtqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_UNWIND" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.action#_yC4h0NqwEd-O4vbSPlarTw"/>
-<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ PhyElevatorFloor" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.action#_d3adMfS-Ed-43_jmKUh78g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT4" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="move_down" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm|org.eventb.core.scMachineFile#lift01_floors|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_d3bEQPS-Ed-43_jmKUh78g"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift01_floors.bcm|org.eventb.core.scMachineFile#lift01_floors|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_SGKl4PvTEd-J48UG_gxxdg"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="0&lt;PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_9uGg8Nd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorFloor ≔ PhyElevatorFloor − 1" org.eventb.core.label="act1_1" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.action#_9uGg8dd9Ed-Dle0at0Xgqg"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_yC4h0tqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
@@ -60,5 +59,6 @@
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I4tqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="last_stop≠PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I49qwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_STOP" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.action#_yC5v8NqwEd-O4vbSPlarTw"/>
+<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ PhyElevatorFloor" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.action#_d3adMfS-Ed-43_jmKUh78g"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
Oops, something went wrong. Retry.

0 comments on commit fb917de

Please sign in to comment.