Permalink
Browse files

final refinement with functions instead of sets

  • Loading branch information...
1 parent f8a71fa commit be286103a23624c4da68d554794200f147446b11 Adrian Friedli committed Nov 28, 2010
Showing with 40,850 additions and 2,148 deletions.
  1. +249 −57 rodin/lift10_final.bcm
  2. +1,563 −97 rodin/lift10_final.bpo
  3. +37,425 −661 rodin/lift10_final.bpr
  4. +156 −12 rodin/lift10_final.bps
  5. +270 −134 rodin/lift10_final.bum
  6. +40 −40 rodin/lift13_conv_lights.bpo
  7. +36 −36 rodin/lift13_conv_lights.bps
  8. +39 −39 rodin/lift14_conv_lights.bpo
  9. +35 −35 rodin/lift14_conv_lights.bps
  10. +71 −71 rodin/lift15_conv_lights.bpo
  11. +67 −67 rodin/lift15_conv_lights.bps
  12. +35 −35 rodin/lift16_conv_lights.bpo
  13. +31 −31 rodin/lift16_conv_lights.bps
  14. +34 −34 rodin/lift17_conv_lights.bpo
  15. +30 −30 rodin/lift17_conv_lights.bps
  16. +33 −33 rodin/lift18_conv_lights.bpo
  17. +29 −29 rodin/lift18_conv_lights.bps
  18. +59 −59 rodin/lift19_conv_lights.bpo
  19. +55 −55 rodin/lift19_conv_lights.bps
  20. +53 −53 rodin/lift20_conv_schedule.bpo
  21. +49 −49 rodin/lift20_conv_schedule.bps
  22. +25 −25 rodin/lift21_conv_move.bpo
  23. +21 −21 rodin/lift21_conv_move.bps
  24. +24 −24 rodin/lift22_conv_move.bpo
  25. +20 −20 rodin/lift22_conv_move.bps
  26. +22 −22 rodin/lift23_conv_move.bpo
  27. +18 −18 rodin/lift23_conv_move.bps
  28. +22 −22 rodin/lift24_conv_move.bpo
  29. +18 −18 rodin/lift24_conv_move.bps
  30. +19 −19 rodin/lift25_conv_move.bpo
  31. +15 −15 rodin/lift25_conv_move.bps
  32. +18 −18 rodin/lift26_conv_move.bpo
  33. +14 −14 rodin/lift26_conv_move.bps
  34. +30 −30 rodin/lift27_conv_door.bpo
  35. +26 −26 rodin/lift27_conv_door.bps
  36. +16 −16 rodin/lift28_conv_door.bpo
  37. +12 −12 rodin/lift28_conv_door.bps
  38. +15 −15 rodin/lift29_conv_door.bpo
  39. +11 −11 rodin/lift29_conv_door.bps
  40. +14 −14 rodin/lift30_conv_door.bpo
  41. +10 −10 rodin/lift30_conv_door.bps
  42. +21 −21 rodin/lift31_conv_door.bpo
  43. +17 −17 rodin/lift31_conv_door.bps
  44. +12 −12 rodin/lift32_conv_door.bpo
  45. +8 −8 rodin/lift32_conv_door.bps
  46. +11 −11 rodin/lift33_conv_door.bpo
  47. +7 −7 rodin/lift33_conv_door.bps
  48. +10 −10 rodin/lift34_conv_door.bpo
  49. +6 −6 rodin/lift34_conv_door.bps
  50. +9 −9 rodin/lift35_conv_door.bpo
  51. +5 −5 rodin/lift35_conv_door.bps
  52. +8 −8 rodin/lift36_conv_buttons.bpo
  53. +7 −7 rodin/lift36_conv_buttons.bps
View

Large diffs are not rendered by default.

Oops, something went wrong.
View

Large diffs are not rendered by default.

Oops, something went wrong.
View

Large diffs are not rendered by default.

Oops, something went wrong.
View

Large diffs are not rendered by default.

Oops, something went wrong.
View

Large diffs are not rendered by default.

Oops, something went wrong.

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -1,39 +1,39 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile>
-<org.eventb.core.psStatus name="FIN" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="USER_RELEASES_DOWN_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="USER_RELEASES_UP_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="USER_RELEASES_FLOOR_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_floor_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/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="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_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_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="FIN" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="USER_RELEASES_DOWN_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_ON_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_OFF_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="turn_down_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="turn_down_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="USER_RELEASES_UP_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_ON_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_OFF_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="turn_up_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="turn_up_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="USER_RELEASES_FLOOR_BUTTON/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_ON_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="TURNS_OFF_FLOOR_BUTTON_LIGHT/VAR" 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/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="DOOR_OPENS_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_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<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="0" 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="0" 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"/>
+<org.eventb.core.psStatus name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
</org.eventb.core.psFile>
Oops, something went wrong.

0 comments on commit be28610

Please sign in to comment.