Permalink
Browse files

realy corrected guards (and proved 2 new invariants depending on them)

  • Loading branch information...
1 parent 4ddf562 commit c7991161105319d8c50c78f7b3f181838b6d7ffc Adrian Friedli committed Dec 2, 2010
Showing with 15,976 additions and 16,538 deletions.
  1. +49 −49 rodin/lift11_conv_add_req.bcm
  2. +13 −13 rodin/lift11_conv_add_req.bpo
  3. +4 −4 rodin/lift11_conv_add_req.bps
  4. +50 −50 rodin/lift11_conv_add_req.bum
  5. +2 −2 rodin/lift12_conv_lights.bcm
  6. +7 −7 rodin/lift12_conv_lights.bpo
  7. +2 −2 rodin/lift12_conv_lights.bps
  8. +2 −2 rodin/lift13_conv_lights.bcm
  9. +7 −7 rodin/lift13_conv_lights.bpo
  10. +2 −2 rodin/lift13_conv_lights.bps
  11. +2 −2 rodin/lift14_conv_lights.bcm
  12. +7 −7 rodin/lift14_conv_lights.bpo
  13. +2 −2 rodin/lift14_conv_lights.bps
  14. +2 −2 rodin/lift15_conv_lights.bcm
  15. +9 −9 rodin/lift15_conv_lights.bpo
  16. +4 −4 rodin/lift15_conv_lights.bps
  17. +2 −2 rodin/lift16_conv_lights.bcm
  18. +7 −7 rodin/lift16_conv_lights.bpo
  19. +2 −2 rodin/lift16_conv_lights.bps
  20. +2 −2 rodin/lift17_conv_lights.bcm
  21. +7 −7 rodin/lift17_conv_lights.bpo
  22. +2 −2 rodin/lift17_conv_lights.bps
  23. +2 −2 rodin/lift18_conv_lights.bcm
  24. +7 −7 rodin/lift18_conv_lights.bpo
  25. +2 −2 rodin/lift18_conv_lights.bps
  26. +2 −2 rodin/lift19_conv_lights.bcm
  27. +9 −9 rodin/lift19_conv_lights.bpo
  28. +4 −4 rodin/lift19_conv_lights.bps
  29. +2 −2 rodin/lift20_conv_schedule.bcm
  30. +9 −9 rodin/lift20_conv_schedule.bpo
  31. +4 −4 rodin/lift20_conv_schedule.bps
  32. +2 −2 rodin/lift21_conv_move.bcm
  33. +7 −7 rodin/lift21_conv_move.bpo
  34. +2 −2 rodin/lift21_conv_move.bps
  35. +2 −2 rodin/lift22_conv_move.bcm
  36. +7 −7 rodin/lift22_conv_move.bpo
  37. +2 −2 rodin/lift22_conv_move.bps
  38. +2 −2 rodin/lift23_conv_move.bcm
  39. +7 −7 rodin/lift23_conv_move.bpo
  40. +2 −2 rodin/lift23_conv_move.bps
  41. +2 −2 rodin/lift24_conv_move.bcm
  42. +7 −7 rodin/lift24_conv_move.bpo
  43. +46 −46 rodin/lift24_conv_move.bpr
  44. +2 −2 rodin/lift24_conv_move.bps
  45. +2 −2 rodin/lift25_conv_move.bcm
  46. +6 −6 rodin/lift25_conv_move.bpo
  47. +1 −1 rodin/lift25_conv_move.bps
  48. +2 −2 rodin/lift26_conv_move.bcm
  49. +5 −5 rodin/lift26_conv_move.bpo
  50. +2 −2 rodin/lift27_conv_door.bcm
  51. +5 −5 rodin/lift27_conv_door.bpo
  52. +2 −2 rodin/lift28_conv_door.bcm
  53. +5 −5 rodin/lift28_conv_door.bpo
  54. +2 −2 rodin/lift29_conv_door.bcm
  55. +5 −5 rodin/lift29_conv_door.bpo
  56. +2 −2 rodin/lift30_conv_door.bcm
  57. +5 −5 rodin/lift30_conv_door.bpo
  58. +2 −2 rodin/lift31_conv_door.bcm
  59. +5 −5 rodin/lift31_conv_door.bpo
  60. +2 −2 rodin/lift32_conv_door.bcm
  61. +5 −5 rodin/lift32_conv_door.bpo
  62. +2 −2 rodin/lift33_conv_door.bcm
  63. +5 −5 rodin/lift33_conv_door.bpo
  64. +2 −2 rodin/lift34_conv_door.bcm
  65. +5 −5 rodin/lift34_conv_door.bpo
  66. +2 −2 rodin/lift35_conv_door.bcm
  67. +5 −5 rodin/lift35_conv_door.bpo
  68. +53 −50 rodin/lift36_conv_buttons.bcm
  69. +544 −145 rodin/lift36_conv_buttons.bpo
  70. +11,231 −3,134 rodin/lift36_conv_buttons.bpr
  71. +79 −35 rodin/lift36_conv_buttons.bps
  72. +52 −49 rodin/lift36_conv_buttons.bum
  73. +54 −51 rodin/lift37_lifeness.bcm
  74. +90 −87 rodin/lift37_lifeness.bpo
  75. +3,427 −12,541 rodin/lift37_lifeness.bpr
  76. +1 −1 rodin/lift37_lifeness.bps
  77. +49 −49 rodin/lift37_lifeness.bum
Oops, something went wrong.
Oops, something went wrong.
@@ -7,10 +7,10 @@
<org.eventb.core.psStatus name="turn_up_button_light_off/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="turn_floor_button_light_on/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="turn_floor_button_light_off/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="stop/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="switch_schedule_to_up/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="resume_schedule_up/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
Oops, something went wrong.
@@ -375,7 +375,7 @@
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyMttq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyzwNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyzwdq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
-<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_VpaFUv5TEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-YflyEd-F0OvBKAXwJQ" org.eventb.core.theorem="false"/>
+<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨(snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∧(snsrElevatorFloor∉ctrlDownButtonLightsSet∨snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests≠(∅ ⦂ ℙ(ℤ))))" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_tKu5Qf5hEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-YflyEd-F0OvBKAXwJQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ TRUE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.action#_aGyzwtq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.action#_aGyzw9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrElevatorFloor ≔ −1" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.action#_aGyzxNq-Ed-L_e8_V4iXIg"/>
@@ -396,7 +396,7 @@
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B49q-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠0" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B5Nq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B5dq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
-<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_VpasYf5TEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-ZvlyEd-F0OvBKAXwJQ" org.eventb.core.theorem="false"/>
+<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨(snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet∧(snsrElevatorFloor∉ctrlUpButtonLightsSet∨0 ‥ (snsrElevatorFloor − 1)∩requests≠(∅ ⦂ ℙ(ℤ))))" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_tKvgUP5hEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-ZvlyEd-F0OvBKAXwJQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ TRUE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.action#_aG0o8Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyElevatorFloor ≔ PhyElevatorFloor − 1" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.action#_aG0o8dq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.action#_aG0o8tq-Ed-L_e8_V4iXIg"/>
@@ -1,5 +1,5 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="1">
+<org.eventb.core.poFile org.eventb.core.poStamp="3">
<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"/>
@@ -533,7 +533,7 @@
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="PhyDoorEngine≠DOOR_STOP" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4OA2Ed-73py7lbE8bg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4eA2Ed-73py7lbE8bg"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="1">
+<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTALLHYPEVT25"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="snsrFloorButtonsSet ∖ ctrlFloorButtonLightsSet⊆snsrFloorButtonsSet ∖ ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift12_conv_lights.bum|org.eventb.core.machineFile#lift12_conv_lights|org.eventb.core.variant#_us4UgPfqEd-vgams47i3xA"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/ProvenLift/lift12_conv_lights.bum|org.eventb.core.machineFile#lift12_conv_lights|org.eventb.core.variant#_us4UgPfqEd-vgams47i3xA"/>
@@ -546,11 +546,11 @@
<org.eventb.core.poIdentifier name="PhyCableEngine'" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.poIdentifier name="snsrCableEngine'" org.eventb.core.type="CABLE_COMMAND"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poPredicateSet name="EVTALLHYPEVT25" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTIDENTEVT25" org.eventb.core.poStamp="1">
+<org.eventb.core.poPredicateSet name="EVTALLHYPEVT25" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTIDENTEVT25" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyMttq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="PhyElevatorFloor≠LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyzwNq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CamPcPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGyzwdq-Ed-L_e8_V4iXIg"/>
-<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_VpaFUv5TEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-YflyEd-F0OvBKAXwJQ"/>
+<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨(snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∧(snsrElevatorFloor∉ctrlDownButtonLightsSet∨snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests≠(∅ ⦂ ℙ(ℤ))))" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_tKu5Qf5hEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-YflyEd-F0OvBKAXwJQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTALLHYPEVT26"/>
@@ -570,7 +570,7 @@
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_Cam2gPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGza0dq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_Cam2gPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aGza0tq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="1">
+<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTALLHYPEVT27"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="snsrFloorButtonsSet ∖ ctrlFloorButtonLightsSet⊆snsrFloorButtonsSet ∖ ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift12_conv_lights.bum|org.eventb.core.machineFile#lift12_conv_lights|org.eventb.core.variant#_us4UgPfqEd-vgams47i3xA"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/ProvenLift/lift12_conv_lights.bum|org.eventb.core.machineFile#lift12_conv_lights|org.eventb.core.variant#_us4UgPfqEd-vgams47i3xA"/>
@@ -584,11 +584,11 @@
<org.eventb.core.poIdentifier name="snsrCableEngine'" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.poIdentifier name="PhyElevatorFloor'" org.eventb.core.type="ℤ"/>
</org.eventb.core.poPredicateSet>
-<org.eventb.core.poPredicateSet name="EVTALLHYPEVT27" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTIDENTEVT27" org.eventb.core.poStamp="1">
+<org.eventb.core.poPredicateSet name="EVTALLHYPEVT27" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTIDENTEVT27" org.eventb.core.poStamp="3">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B49q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="PhyElevatorFloor≠0" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B5Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_CandkPvUEd-J48UG_gxxdg|org.eventb.core.guard#_aG0B5dq-Ed-L_e8_V4iXIg"/>
-<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_VpasYf5TEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-ZvlyEd-F0OvBKAXwJQ"/>
+<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="snsrElevatorFloor=last_stop∨(snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet∧(snsrElevatorFloor∉ctrlUpButtonLightsSet∨0 ‥ (snsrElevatorFloor − 1)∩requests≠(∅ ⦂ ℙ(ℤ))))" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.event#_tKvgUP5hEd-RbO_JCG3Adw|org.eventb.core.guard#_EdU-ZvlyEd-F0OvBKAXwJQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift12_conv_lights.bpo|org.eventb.core.poFile#lift12_conv_lights|org.eventb.core.poPredicateSet#EVTALLHYPEVT28"/>
@@ -22,9 +22,9 @@
<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
Oops, something went wrong.

0 comments on commit c799116

Please sign in to comment.