Permalink
Browse files

delaying convergence proves until the end

  • Loading branch information...
1 parent bf013bf commit 6e41d24b15c0c63298c661e03d562382f15157be Alexander Bernauer committed Nov 18, 2010
Showing with 7,450 additions and 24,537 deletions.
  1. +3 −3 rodin/lift01_floors.bcm
  2. +4 −4 rodin/lift01_floors.bum
  3. +2 −0 rodin/lift01b_conv_floors.bpo_tmp
  4. +9 −11 rodin/lift02_main_engine.bcm
  5. +12 −111 rodin/lift02_main_engine.bpo
  6. +1 −15 rodin/lift02_main_engine.bps
  7. +10 −12 rodin/lift02_main_engine.bum
  8. +18 −21 rodin/lift03_door_engine.bcm
  9. +25 −152 rodin/lift03_door_engine.bpo
  10. +139 −145 rodin/lift03_door_engine.bpr
  11. +6 −22 rodin/lift03_door_engine.bps
  12. +16 −18 rodin/lift03_door_engine.bum
  13. +68 −71 rodin/lift04_phys_main_engine.bcm
  14. +143 −220 rodin/lift04_phys_main_engine.bpo
  15. +1,134 −1,242 rodin/lift04_phys_main_engine.bpr
  16. +59 −70 rodin/lift04_phys_main_engine.bps
  17. +24 −25 rodin/lift04_phys_main_engine.bum
  18. +0 −185 rodin/lift05_conv_floor_up.bcm
  19. +0 −253 rodin/lift05_conv_floor_up.bpo
  20. +18 −0 rodin/lift05_conv_floor_up.bpr
  21. +0 −12 rodin/lift05_conv_floor_up.bps
  22. +0 −56 rodin/lift05_conv_floor_up.bum
  23. +0 −185 rodin/lift06_conv_floor_down.bcm
  24. +0 −225 rodin/lift06_conv_floor_down.bpo
  25. +18 −0 rodin/lift06_conv_floor_down.bpr
  26. +0 −8 rodin/lift06_conv_floor_down.bps
  27. +0 −56 rodin/lift06_conv_floor_down.bum
  28. +83 −86 rodin/lift07_phys_door.bcm
  29. +89 −180 rodin/lift07_phys_door.bpo
  30. +787 −795 rodin/lift07_phys_door.bpr
  31. +30 −43 rodin/lift07_phys_door.bps
  32. +30 −31 rodin/lift07_phys_door.bum
  33. +0 −266 rodin/lift08_conv_door_open.bcm
  34. +0 −351 rodin/lift08_conv_door_open.bpo
  35. +24 −0 rodin/lift08_conv_door_open.bpr
  36. +0 −14 rodin/lift08_conv_door_open.bps
  37. +0 −78 rodin/lift08_conv_door_open.bum
  38. +0 −266 rodin/lift09_conv_door_close.bcm
  39. +0 −323 rodin/lift09_conv_door_close.bpo
  40. +0 −10 rodin/lift09_conv_door_close.bps
  41. +0 −78 rodin/lift09_conv_door_close.bum
  42. +0 −275 rodin/lift10_conv_door_closed.bcm
  43. +0 −1,187 rodin/lift10_conv_door_closed.bpo
  44. +0 −104 rodin/lift10_conv_door_closed.bps
  45. +0 −87 rodin/lift10_conv_door_closed.bum
  46. +106 −118 rodin/lift11_buttons.bcm
  47. +116 −160 rodin/lift11_buttons.bpo
  48. +572 −678 rodin/lift11_buttons.bpr
  49. +15 −20 rodin/lift11_buttons.bps
  50. +43 −44 rodin/lift11_buttons.bum
  51. +0 −335 rodin/lift12_conv_light_on.bcm
  52. +0 −377 rodin/lift12_conv_light_on.bpo
  53. +2 −0 rodin/lift12_conv_light_on.bpo_tmp
  54. +18 −0 rodin/lift12_conv_light_on.bpr
  55. +0 −7 rodin/lift12_conv_light_on.bps
  56. +0 −100 rodin/lift12_conv_light_on.bum
  57. +0 −335 rodin/lift13_conv_phys_light_on.bcm
  58. +0 −370 rodin/lift13_conv_phys_light_on.bpo
  59. +0 −6 rodin/lift13_conv_phys_light_on.bps
  60. +0 −100 rodin/lift13_conv_phys_light_on.bum
  61. +0 −335 rodin/lift14_conv_phys_light_off.bcm
  62. +0 −363 rodin/lift14_conv_phys_light_off.bpo
  63. +0 −5 rodin/lift14_conv_phys_light_off.bps
  64. +0 −100 rodin/lift14_conv_phys_light_off.bum
  65. +136 −148 rodin/lift15_up_buttons.bcm
  66. +146 −190 rodin/lift15_up_buttons.bpo
  67. +465 −575 rodin/lift15_up_buttons.bpr
  68. +15 −20 rodin/lift15_up_buttons.bps
  69. +56 −57 rodin/lift15_up_buttons.bum
  70. +0 −396 rodin/lift16_conv_light_on.bcm
  71. +0 −444 rodin/lift16_conv_light_on.bpo
  72. +22 −0 rodin/lift16_conv_light_on.bpr
  73. +0 −7 rodin/lift16_conv_light_on.bps
  74. +0 −122 rodin/lift16_conv_light_on.bum
  75. +0 −396 rodin/lift17_conv_phys_light_on.bcm
  76. +0 −437 rodin/lift17_conv_phys_light_on.bpo
  77. +0 −6 rodin/lift17_conv_phys_light_on.bps
  78. +0 −122 rodin/lift17_conv_phys_light_on.bum
  79. +0 −396 rodin/lift18_conv_phys_light_off.bcm
  80. +0 −430 rodin/lift18_conv_phys_light_off.bpo
  81. +0 −5 rodin/lift18_conv_phys_light_off.bps
  82. +0 −122 rodin/lift18_conv_phys_light_off.bum
  83. +146 −158 rodin/lift19_down_buttons.bcm
  84. +152 −196 rodin/lift19_down_buttons.bpo
  85. +805 −935 rodin/lift19_down_buttons.bpr
  86. +15 −20 rodin/lift19_down_buttons.bps
  87. +64 −65 rodin/lift19_down_buttons.bum
  88. +0 −457 rodin/lift20_conv_light_on.bcm
  89. +0 −511 rodin/lift20_conv_light_on.bpo
  90. +26 −0 rodin/lift20_conv_light_on.bpr
  91. +0 −7 rodin/lift20_conv_light_on.bps
  92. +0 −144 rodin/lift20_conv_light_on.bum
  93. +0 −457 rodin/lift21_conv_phys_light_on.bcm
  94. +0 −504 rodin/lift21_conv_phys_light_on.bpo
  95. +0 −6 rodin/lift21_conv_phys_light_on.bps
  96. +0 −144 rodin/lift21_conv_phys_light_on.bum
  97. +0 −457 rodin/lift22_conv_phys_light_off.bcm
  98. +0 −497 rodin/lift22_conv_phys_light_off.bpo
  99. +0 −5 rodin/lift22_conv_phys_light_off.bps
  100. +0 −144 rodin/lift22_conv_phys_light_off.bum
  101. +162 −174 rodin/lift23_scheduler.bcm
  102. +190 −234 rodin/lift23_scheduler.bpo
  103. +1,318 −1,528 rodin/lift23_scheduler.bpr
  104. +30 −35 rodin/lift23_scheduler.bps
  105. +76 −77 rodin/lift23_scheduler.bum
  106. +0 −565 rodin/lift24_final.bcm
  107. +0 −2,071 rodin/lift24_final.bpo
  108. +0 −173 rodin/lift24_final.bps
  109. +0 −351 rodin/lift24_final.bum
  110. +2 −0 rodin/lift2_main_engine.bpo_tmp
View
@@ -1,6 +1,6 @@
<?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.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx1_floors.bcc" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.seesContext#_7dmkQNq6Ed-gPNw0slEBPQ"/>
+<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx1_floors.bcc" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.seesContext#_USLCYfMrEd-CfdFlXM8tVw"/>
<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="ℤ"/>
@@ -12,11 +12,11 @@
<org.eventb.core.scEvent name="EVT0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#'">
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="floor ≔ 0" org.eventb.core.label="act1_1" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#'|org.eventb.core.action#_9uErwNd9Ed-Dle0at0Xgqg"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="move_up" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg">
+<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="move_up" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="floor&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="floor ≔ floor+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="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="move_down" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg">
+<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="move_down" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="0&lt;floor" 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="floor ≔ floor − 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>
View
@@ -1,18 +1,18 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1287408223075" org.eventb.texttools.text_representation="machine ProvenLift_1 sees ctx1_floors&#10;&#10;variables floor&#10;&#10;invariants&#10; @inv1_1 floor ∈ ℕ&#10; @inv1_2 floor ≤ N&#10; @dlf1_1 floor &lt; N ∨ 0 &lt; floor&#10;&#10;events&#10; event INITIALISATION&#10; then&#10; @act1_1 floor ≔ 0&#10; end&#10;&#10; event move_up&#10; where&#10; @grd1_1 floor &lt; N&#10; then&#10; @act1_1 floor ≔ floor + 1&#10; end&#10;&#10; event move_down&#10; where&#10; @grd1_1 0 &lt; floor&#10; then&#10; @act1_1 floor ≔ floor − 1&#10; end&#10;end&#10;" version="5">
-<org.eventb.core.seesContext name="_7dmkQNq6Ed-gPNw0slEBPQ" org.eventb.core.target="ctx1_floors"/>
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1290095319344" org.eventb.texttools.text_representation="machine lift01_floors sees ctx1_floors&#10;&#10;variables floor&#10;&#10;invariants&#10; @inv1_1 floor ∈ ℕ&#10; @inv1_2 floor ≤ LAST_FLOOR&#10; @dlf1_1 floor &lt; LAST_FLOOR ∨ 0 &lt; floor&#10;&#10;events&#10; event INITIALISATION&#10; then&#10; @act1_1 floor ≔ 0&#10; end&#10;&#10; anticipated event move_up&#10; where&#10; @grd1_1 floor &lt; LAST_FLOOR&#10; then&#10; @act1_1 floor ≔ floor + 1&#10; end&#10;&#10; anticipated event move_down&#10; where&#10; @grd1_1 0 &lt; floor&#10; then&#10; @act1_1 floor ≔ floor − 1&#10; end&#10;end&#10;" version="5">
+<org.eventb.core.seesContext name="_USLCYfMrEd-CfdFlXM8tVw" org.eventb.core.target="ctx1_floors"/>
<org.eventb.core.variable name="_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.identifier="floor"/>
<org.eventb.core.invariant name="_9uEEsdd9Ed-Dle0at0Xgqg" org.eventb.core.label="inv1_1" org.eventb.core.predicate="floor ∈ ℕ"/>
<org.eventb.core.invariant name="_9uEEstd9Ed-Dle0at0Xgqg" org.eventb.core.label="inv1_2" org.eventb.core.predicate="floor ≤ LAST_FLOOR"/>
<org.eventb.core.invariant name="_VO9DcNqwEd-O4vbSPlarTw" org.eventb.core.label="dlf1_1" org.eventb.core.predicate="floor &lt; LAST_FLOOR ∨ 0 &lt; floor"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_9uErwNd9Ed-Dle0at0Xgqg" org.eventb.core.assignment="floor ≔ 0" org.eventb.core.label="act1_1"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_9uFS0Nd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="move_up">
+<org.eventb.core.event name="_9uFS0Nd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="move_up">
<org.eventb.core.guard name="_9uFS0dd9Ed-Dle0at0Xgqg" org.eventb.core.label="grd1_1" org.eventb.core.predicate="floor &lt; LAST_FLOOR"/>
<org.eventb.core.action name="_9uF54Nd9Ed-Dle0at0Xgqg" org.eventb.core.assignment="floor ≔ floor + 1" org.eventb.core.label="act1_1"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_9uF54dd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="move_down">
+<org.eventb.core.event name="_9uF54dd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="move_down">
<org.eventb.core.guard name="_9uGg8Nd9Ed-Dle0at0Xgqg" org.eventb.core.label="grd1_1" org.eventb.core.predicate="0 &lt; floor"/>
<org.eventb.core.action name="_9uGg8dd9Ed-Dle0at0Xgqg" org.eventb.core.assignment="floor ≔ floor − 1" org.eventb.core.label="act1_1"/>
</org.eventb.core.event>
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.poFile/>
Oops, something went wrong.

0 comments on commit 6e41d24

Please sign in to comment.