Commit 18687427 authored by Yanjun Jiang's avatar Yanjun Jiang
Browse files

Clean up unused files.

These files should be deleted in the support refinement commit. For
some reason this is forgetten. Now we clean them up.
parent ebcd28b3
Loading
Loading
Loading
Loading
+0 −17
Original line number Diff line number Diff line
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
        <name>momThreeLayerTable</name>
        <comment></comment>
        <projects>
        </projects>
        <buildSpec>
                <buildCommand>
                        <name>org.rodinp.core.rodinbuilder</name>
                        <arguments>
                        </arguments>
                </buildCommand>
        </buildSpec>
        <natures>
                <nature>org.rodinp.core.rodinnature</nature>
        </natures>
</projectDescription>
+0 −73
Original line number Diff line number Diff line
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase" version="5">
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="x" org.eventb.core.identifier="x"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="y" org.eventb.core.identifier="y"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="z" org.eventb.core.identifier="z"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="w" org.eventb.core.identifier="w"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="output1" org.eventb.core.identifier="output1"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="output2" org.eventb.core.identifier="output2"/>
<org.eventb.core.invariant name="Invariant1" org.eventb.core.label="inv1" org.eventb.core.predicate="x ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant2" org.eventb.core.label="inv2" org.eventb.core.predicate="y ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant3" org.eventb.core.label="inv3" org.eventb.core.predicate="z ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant4" org.eventb.core.label="inv4" org.eventb.core.predicate="w ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant5" org.eventb.core.label="inv5" org.eventb.core.predicate="output1 ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant6" org.eventb.core.label="inv6" org.eventb.core.predicate="output2 ∈ ℤ"/>
<org.eventb.core.event name="Event0" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="InitAction1" org.eventb.core.assignment="x :∈ ℤ" org.eventb.core.label="act1"/>
<org.eventb.core.action name="InitAction2" org.eventb.core.assignment="y :∈ ℤ" org.eventb.core.label="act2"/>
<org.eventb.core.action name="InitAction3" org.eventb.core.assignment="z :∈ ℤ" org.eventb.core.label="act3"/>
<org.eventb.core.action name="InitAction4" org.eventb.core.assignment="w :∈ ℤ" org.eventb.core.label="act4"/>
<org.eventb.core.action name="InitAction5" org.eventb.core.assignment="output1 :∈ ℤ" org.eventb.core.label="act5"/>
<org.eventb.core.action name="InitAction6" org.eventb.core.assignment="output2 :∈ ℤ" org.eventb.core.label="act6"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event1_1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt1_1">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="y ≥ 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 1" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 9" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event1_2_1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt1_2_1">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z &gt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 2" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 10" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event1_2_2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt1_2_2">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z = 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 3" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 11" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event1_2_3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt1_2_3">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z &lt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 4" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 12" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x = 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 5" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 13" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event3_1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt3_1">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="w &gt; 1"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 6" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 14" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event3_2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt3_2">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="w = 1"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 7" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 15" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event3_3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt3_3">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="w &lt; 1"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output1 ≔ 8" org.eventb.core.label="act1"/>
<org.eventb.core.action name="Action2" org.eventb.core.assignment="output2 ≔ 16" org.eventb.core.label="act2"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
 No newline at end of file
+0 −17
Original line number Diff line number Diff line
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
        <name>sixLayerTable</name>
        <comment></comment>
        <projects>
        </projects>
        <buildSpec>
                <buildCommand>
                        <name>org.rodinp.core.rodinbuilder</name>
                        <arguments>
                        </arguments>
                </buildCommand>
        </buildSpec>
        <natures>
                <nature>org.rodinp.core.rodinnature</nature>
        </natures>
</projectDescription>
+0 −74
Original line number Diff line number Diff line
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase" version="5">
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable1" org.eventb.core.identifier="x"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable2" org.eventb.core.identifier="y"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable3" org.eventb.core.identifier="z"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable4" org.eventb.core.identifier="w"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable5" org.eventb.core.identifier="m"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable6" org.eventb.core.identifier="n"/>
<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute="" de.prob.units.unitPragmaAttribute="" name="Variable7" org.eventb.core.identifier="output"/>
<org.eventb.core.invariant name="Invariant1" org.eventb.core.label="inv1" org.eventb.core.predicate="x ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant2" org.eventb.core.label="inv2" org.eventb.core.predicate="y ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant3" org.eventb.core.label="inv3" org.eventb.core.predicate="z ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant4" org.eventb.core.label="inv4" org.eventb.core.predicate="w ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant5" org.eventb.core.label="inv5" org.eventb.core.predicate="m ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant6" org.eventb.core.label="inv6" org.eventb.core.predicate="n ∈ ℤ"/>
<org.eventb.core.invariant name="Invariant7" org.eventb.core.label="inv7" org.eventb.core.predicate="output ∈ ℤ"/>
<org.eventb.core.event name="Event0" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="InitAction1" org.eventb.core.assignment="x :∈ ℤ" org.eventb.core.label="act1"/>
<org.eventb.core.action name="InitAction2" org.eventb.core.assignment="y :∈ ℤ" org.eventb.core.label="act2"/>
<org.eventb.core.action name="InitAction3" org.eventb.core.assignment="z :∈ ℤ" org.eventb.core.label="act3"/>
<org.eventb.core.action name="InitAction4" org.eventb.core.assignment="w :∈ ℤ" org.eventb.core.label="act4"/>
<org.eventb.core.action name="InitAction5" org.eventb.core.assignment="m :∈ ℤ" org.eventb.core.label="act5"/>
<org.eventb.core.action name="InitAction6" org.eventb.core.assignment="n :∈ ℤ" org.eventb.core.label="act6"/>
<org.eventb.core.action name="InitAction7" org.eventb.core.assignment="output :∈ ℤ" org.eventb.core.label="act7"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt1">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="y ≥ 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 1" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z &gt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 2" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt3">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="m &gt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="z = 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard4" org.eventb.core.label="grd4" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard5" org.eventb.core.label="grd5" org.eventb.core.predicate="n &gt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 3" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event4" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt4">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="y &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="x &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z &lt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 4" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event5" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt5">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x = 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 5" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event6" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt6">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="w &gt; 1"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 6" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event7" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt7">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="n &gt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="m &gt; 0"/>
<org.eventb.core.guard name="Guard3" org.eventb.core.label="grd3" org.eventb.core.predicate="z &gt; 0"/>
<org.eventb.core.guard name="Guard4" org.eventb.core.label="grd4" org.eventb.core.predicate="w = 1"/>
<org.eventb.core.guard name="Guard5" org.eventb.core.label="grd5" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard6" org.eventb.core.label="grd6" org.eventb.core.predicate="y &gt; 0"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 7" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="Event8" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt8">
<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="x &lt; 0"/>
<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="w &lt; 1"/>
<org.eventb.core.action name="Action1" org.eventb.core.assignment="output ≔ 8" org.eventb.core.label="act1"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
 No newline at end of file
+0 −17
Original line number Diff line number Diff line
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
        <name>momThreeLayerTable</name>
        <comment></comment>
        <projects>
        </projects>
        <buildSpec>
                <buildCommand>
                        <name>org.rodinp.core.rodinbuilder</name>
                        <arguments>
                        </arguments>
                </buildCommand>
        </buildSpec>
        <natures>
                <nature>org.rodinp.core.rodinnature</nature>
        </natures>
</projectDescription>
Loading