clean project

copton · Dec 3, 2010 · 3810e93 · 3810e93
1 parent ae8991b
commit 3810e93
Show file tree

Hide file tree

Showing 55 changed files with 2,275 additions and 2,275 deletions.
diff --git a/rodin/ctx6_conv_utils.bpo b/rodin/ctx6_conv_utils.bpo
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="2">
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
 <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="2">
+<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.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>
diff --git a/rodin/lift11_conv_add_req.bpo b/rodin/lift11_conv_add_req.bpo
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="3">
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
 <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"/>
@@ -443,7 +443,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/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
+<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_UP/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="0">
 <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTALLHYPEVT25"/>
 <org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="schedule=SCHEDULER_WAIT∧−1∉requests⇒request_served=TRUE" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.invariant#_EdQF4PlyEd-F0OvBKAXwJQ"/>
 <org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_4Ue1gf4MEd-Vo467mFpzFA"/>
@@ -458,13 +458,13 @@
 <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/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTIDENTEVT25" org.eventb.core.poStamp="3">
+<org.eventb.core.poPredicateSet name="EVTALLHYPEVT25" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTIDENTEVT25" org.eventb.core.poStamp="0">
 <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∧(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/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
+<org.eventb.core.poSequent name="ELEVATOR_REACHES_FLOOR_UP/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="0">
 <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTALLHYPEVT26"/>
 <org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="schedule=SCHEDULER_WAIT∧PhyElevatorFloor+1∉requests⇒request_served=TRUE" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.invariant#_EdQF4PlyEd-F0OvBKAXwJQ"/>
 <org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_4Ue1g_4MEd-Vo467mFpzFA"/>
@@ -484,7 +484,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/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
+<org.eventb.core.poSequent name="ELEVATOR_LEAVES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="0">
 <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTALLHYPEVT27"/>
 <org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="schedule=SCHEDULER_WAIT∧−1∉requests⇒request_served=TRUE" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.invariant#_EdQF4PlyEd-F0OvBKAXwJQ"/>
 <org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_4Ue1hf4MEd-Vo467mFpzFA"/>
@@ -500,13 +500,13 @@
 <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/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTIDENTEVT27" org.eventb.core.poStamp="3">
+<org.eventb.core.poPredicateSet name="EVTALLHYPEVT27" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTIDENTEVT27" org.eventb.core.poStamp="0">
 <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∧(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/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
+<org.eventb.core.poSequent name="ELEVATOR_REACHES_FLOOR_DOWN/inv11_1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="0">
 <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ProvenLift/lift11_conv_add_req.bpo|org.eventb.core.poFile#lift11_conv_add_req|org.eventb.core.poPredicateSet#EVTALLHYPEVT28"/>
 <org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="schedule=SCHEDULER_WAIT∧PhyElevatorFloor∉requests⇒request_served=TRUE" org.eventb.core.source="/ProvenLift/lift11_conv_add_req.bum|org.eventb.core.machineFile#lift11_conv_add_req|org.eventb.core.invariant#_EdQF4PlyEd-F0OvBKAXwJQ"/>
 <org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_4Ufckf4MEd-Vo467mFpzFA"/>

diff --git a/rodin/lift11_conv_add_req.bps b/rodin/lift11_conv_add_req.bps
@@ -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="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="ELEVATOR_LEAVES_FLOOR_UP/inv11_1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" 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="0" 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="0" 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="0" 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"/>