Permalink
Browse files

first half of convergence for door events

  • Loading branch information...
1 parent 5cfe9c1 commit a664d9aacb222dba398d1d261995dc4a09a1e763 Adrian Friedli committed Nov 26, 2010
Showing with 14,648 additions and 884 deletions.
  1. +7 −7 rodin/lift03_door_engine.bcm
  2. +3 −3 rodin/lift03_door_engine.bpo
  3. +1 −1 rodin/lift03_door_engine.bps
  4. +8 −8 rodin/lift03_door_engine.bum
  5. +3 −3 rodin/lift04_phys_main_engine.bpo
  6. +1 −1 rodin/lift04_phys_main_engine.bps
  7. +2 −2 rodin/lift05_phys_door.bpo
  8. +2 −2 rodin/lift06_buttons.bpo
  9. +2 −2 rodin/lift07_up_buttons.bpo
  10. +43 −43 rodin/lift08_down_buttons.bcm
  11. +12 −12 rodin/lift08_down_buttons.bpo
  12. +3 −3 rodin/lift08_down_buttons.bps
  13. +39 −39 rodin/lift08_down_buttons.bum
  14. +51 −49 rodin/lift09_scheduler.bcm
  15. +56 −54 rodin/lift09_scheduler.bpo
  16. +16 −16 rodin/lift09_scheduler.bps
  17. +46 −44 rodin/lift09_scheduler.bum
  18. +3 −1 rodin/lift10_final.bcm
  19. +5 −3 rodin/lift10_final.bpo
  20. +8 −6 rodin/lift11_conv_add_req.bcm
  21. +8 −6 rodin/lift11_conv_add_req.bpo
  22. +8 −6 rodin/lift12_conv_lights.bcm
  23. +9 −7 rodin/lift12_conv_lights.bpo
  24. +1 −1 rodin/lift12_conv_lights.bps
  25. +8 −6 rodin/lift13_conv_lights.bcm
  26. +9 −7 rodin/lift13_conv_lights.bpo
  27. +1 −1 rodin/lift13_conv_lights.bps
  28. +8 −6 rodin/lift14_conv_lights.bcm
  29. +9 −7 rodin/lift14_conv_lights.bpo
  30. +1 −1 rodin/lift14_conv_lights.bps
  31. +8 −6 rodin/lift15_conv_lights.bcm
  32. +10 −8 rodin/lift15_conv_lights.bpo
  33. +126 −120 rodin/lift15_conv_lights.bpr
  34. +2 −2 rodin/lift15_conv_lights.bps
  35. +8 −6 rodin/lift16_conv_lights.bcm
  36. +9 −7 rodin/lift16_conv_lights.bpo
  37. +1 −1 rodin/lift16_conv_lights.bps
  38. +8 −6 rodin/lift17_conv_lights.bcm
  39. +9 −7 rodin/lift17_conv_lights.bpo
  40. +1 −1 rodin/lift17_conv_lights.bps
  41. +8 −6 rodin/lift18_conv_lights.bcm
  42. +9 −7 rodin/lift18_conv_lights.bpo
  43. +1 −1 rodin/lift18_conv_lights.bps
  44. +8 −6 rodin/lift19_conv_lights.bcm
  45. +10 −8 rodin/lift19_conv_lights.bpo
  46. +125 −119 rodin/lift19_conv_lights.bpr
  47. +2 −2 rodin/lift19_conv_lights.bps
  48. +8 −6 rodin/lift20_conv_schedule.bcm
  49. +10 −8 rodin/lift20_conv_schedule.bpo
  50. +126 −124 rodin/lift20_conv_schedule.bpr
  51. +2 −2 rodin/lift20_conv_schedule.bps
  52. +8 −6 rodin/lift21_conv_move.bcm
  53. +9 −7 rodin/lift21_conv_move.bpo
  54. +1 −1 rodin/lift21_conv_move.bps
  55. +8 −6 rodin/lift22_conv_move.bcm
  56. +9 −7 rodin/lift22_conv_move.bpo
  57. +1 −1 rodin/lift22_conv_move.bps
  58. +8 −6 rodin/lift23_conv_move.bcm
  59. +9 −7 rodin/lift23_conv_move.bpo
  60. +1 −1 rodin/lift23_conv_move.bps
  61. +8 −6 rodin/lift24_conv_move.bcm
  62. +9 −7 rodin/lift24_conv_move.bpo
  63. +1 −1 rodin/lift24_conv_move.bps
  64. +8 −6 rodin/lift25_conv_move.bcm
  65. +9 −7 rodin/lift25_conv_move.bpo
  66. +1 −1 rodin/lift25_conv_move.bps
  67. +8 −6 rodin/lift26_conv_move.bcm
  68. +9 −7 rodin/lift26_conv_move.bpo
  69. +1 −1 rodin/lift26_conv_move.bps
  70. +536 −0 rodin/lift27_conv_door.bcm
  71. +698 −0 rodin/lift27_conv_door.bpo
  72. +3,684 −0 rodin/lift27_conv_door.bpr
  73. +23 −0 rodin/lift27_conv_door.bps
  74. +153 −0 rodin/lift27_conv_door.bum
  75. +536 −0 rodin/lift28_conv_door.bcm
  76. +621 −0 rodin/lift28_conv_door.bpo
  77. +2,856 −0 rodin/lift28_conv_door.bpr
  78. +12 −0 rodin/lift28_conv_door.bps
  79. +152 −0 rodin/lift28_conv_door.bum
  80. +536 −0 rodin/lift29_conv_door.bcm
  81. +614 −0 rodin/lift29_conv_door.bpo
  82. +813 −0 rodin/lift29_conv_door.bpr
  83. +11 −0 rodin/lift29_conv_door.bps
  84. +152 −0 rodin/lift29_conv_door.bum
  85. +536 −0 rodin/lift30_conv_door.bcm
  86. +607 −0 rodin/lift30_conv_door.bpo
  87. +974 −0 rodin/lift30_conv_door.bpr
  88. +10 −0 rodin/lift30_conv_door.bps
  89. +152 −0 rodin/lift30_conv_door.bum
@@ -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/lift02_main_engine.bcm" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.refinesMachine#_EoD4gPYhEd-UnYOzyke7oQ"/>
-<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx3_door_engine.bcc" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.seesContext#_EoEfkPYhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesMachine name="REF" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.refinesMachine#_jsqpEPmPEd-4S-prP9DsJw"/>
+<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx3_door_engine.bcc" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.seesContext#_jsqpEfmPEd-4S-prP9DsJw"/>
<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="ℤ"/>
@@ -58,35 +58,35 @@
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_CLOSE" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.action#_HKj0QdqzEd-7IuFxCL4SWw"/>
</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="start_move_up" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_EoFtsPYhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_jsr3MPmPEd-4S-prP9DsJw"/>
<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.scGuard name="GRD2" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_SjnaYdq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT5" 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/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_EoGUwPYhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_jsr3MfmPEd-4S-prP9DsJw"/>
<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.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"/>
<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.scEvent>
<org.eventb.core.scEvent name="EVT6" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="start_move_down" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_EoGUwfYhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_jsr3MvmPEd-4S-prP9DsJw"/>
<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.scGuard name="GRD2" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_SjoBcdq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT7" 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/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_EoGUwvYhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_jsseQPmPEd-4S-prP9DsJw"/>
<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.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"/>
<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.scEvent>
<org.eventb.core.scEvent name="EVT8" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="stop" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_EoGUw_YhEd-UnYOzyke7oQ"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift02_main_engine.bcm|org.eventb.core.scMachineFile#lift02_main_engine|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_jsseQfmPEd-4S-prP9DsJw"/>
<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"/>
@@ -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="CTXHYP" 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"/>
@@ -45,7 +45,7 @@
<org.eventb.core.poIdentifier name="last_stop'" org.eventb.core.type="ℤ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT0" org.eventb.core.parentSet="/ProvenLift/lift03_door_engine.bpo|org.eventb.core.poFile#lift03_door_engine|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="0"/>
-<org.eventb.core.poSequent name="open_door/inv3_2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
+<org.eventb.core.poSequent name="open_door/inv3_2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift03_door_engine.bpo|org.eventb.core.poFile#lift03_door_engine|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒DOOR_OPEN=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.invariant#_Sjk-INq3Ed-AAt710HomgA"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw"/>
@@ -56,7 +56,7 @@
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/ProvenLift/lift03_door_engine.bpo|org.eventb.core.poFile#lift03_door_engine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="ctrlDoorCommand'" org.eventb.core.type="DOOR_COMMAND"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poPredicateSet name="EVTALLHYPEVT1" org.eventb.core.parentSet="/ProvenLift/lift03_door_engine.bpo|org.eventb.core.poFile#lift03_door_engine|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="EVTALLHYPEVT1" org.eventb.core.parentSet="/ProvenLift/lift03_door_engine.bpo|org.eventb.core.poFile#lift03_door_engine|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_HKjNMNqzEd-7IuFxCL4SWw"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="ctrlDoorCommand≠DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_pVt4EPS0Ed-43_jmKUh78g"/>
</org.eventb.core.poPredicateSet>
@@ -1,7 +1,7 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile>
<org.eventb.core.psStatus name="INITIALISATION/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="open_door/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="2" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="stop_door/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="close_door/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="start_move_up/inv3_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
Oops, something went wrong.

0 comments on commit a664d9a

Please sign in to comment.