Commit 661dbfb5 authored by Yanjun Jiang's avatar Yanjun Jiang
Browse files

Support Complex Expression. 

From this version on, the tool support complex expression like: (1*(1+1)+2).
This is realized by add parentheses to the EventBGenerator generated expression.
Also fix the problem of using wrong EventB symbols in the result XML before.
parent 18687427

src/main/java/ca/mcscert/jtet/expression/EventBGenerator.java

+12 −6
Original line number Diff line number Diff line
@@ -43,11 +43,11 @@ final public class EventBGenerator implements CheckerGenerator{ 
            case Addition:

                return "+";

            case Minus:

                return "-";

                return "−";

            case Multiplication:

                return "*";

                return "∗";

            case Division:

                return "/";

                return "÷";

            case Exponentiation:

                return "^";

            case GreaterThen:
@@ -62,6 +62,12 @@ final public class EventBGenerator implements CheckerGenerator{ 
                return "=";

            case NotEquals:

                return "≠";

            case BooleanAnd:

                return "∧";

            case BooleanOr:

                return "∨";

            case Implies:

                return "⇒";

        }

        throw new RuntimeException("Should never happen!");

    }
@@ -72,7 +78,7 @@ final public class EventBGenerator implements CheckerGenerator{ 


    @Override

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

          return /*"(" +*/ lhsExp + " " + EventBGenerator.ConvertToOutputOp(op) + " " + rhsExp /*+ ")"*/;

          return "(" + lhsExp + " " + EventBGenerator.ConvertToOutputOp(op) + " " + rhsExp + ")";

    }



    @Override
@@ -84,9 +90,9 @@ final public class EventBGenerator implements CheckerGenerator{ 
    private static String ConvertToOutputOp(UnaryOperation op) {

        switch (op) {

            case Negation:

                return "NOT";

                return "¬";

            case Minus:

                    return "-";

                return "−";

        }

        throw new IllegalArgumentException("Unhandled operation: " + op);

    }

src/test/java/ca/mcscert/jtet/eventbgenerator/ParameterizedEventBTableGeneratorTest.java

+1 −1
Original line number Diff line number Diff line
@@ -125,7 +125,7 @@ public class ParameterizedEventBTableGeneratorTest { 
        HierarchicalGrid leftGrid = table.getLeftGrid();



        List<HierarchicalCell> cells = leftGrid.getSubHiearchy();

        cells.add(new HierarchicalCell("x > 0"));

        cells.add(new HierarchicalCell("x > 3-3"));

        cells.add(new HierarchicalCell("x == 0"));

        cells.add(new HierarchicalCell("x < 0"));

src/test/java/ca/mcscert/jtet/expression/GenericOperationGeneratorTest.java

+5 −0
Original line number Diff line number Diff line
@@ -62,6 +62,11 @@ public class GenericOperationGeneratorTest { 
                        "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",

                        null,

                        null

                },

                {new EventBGenerator(),

                        "((((x ∗ 5) = (1 ÷ (− 4))) ∨ (((x &gt; (8 + 3)) ∧ (9 &lt; (x − 2))) ∨ ((x ≥ 12) ∨ ((¬ (34 ≤ (− x))) ∨ (5 &gt; 4))))) ⇒ (x ≠ 5))",

                        null,

                        null

                }

        });

    }

src/test/resources/expected/NR/IIP/IIP.bum

+2 −2
Original line number Diff line number Diff line
@@ -9,11 +9,11 @@ 
<org.eventb.core.action name="InitAction2" org.eventb.core.assignment="cPwrConfirm :∈ ℤ" org.eventb.core.label="act2"/>

</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="cPwrStatus = 4"/>

<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="(cPwrStatus = 4)"/>

<org.eventb.core.action name="Action1" org.eventb.core.assignment="cPwrConfirm ≔ 0" 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="cPwrStatus ≠ 4"/>

<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="(cPwrStatus ≠ 4)"/>

<org.eventb.core.action name="Action1" org.eventb.core.assignment="cPwrConfirm ≔ 1" org.eventb.core.label="act1"/>

</org.eventb.core.event>

</org.eventb.core.machineFile>
 
 No newline at end of file

src/test/resources/expected/NR/oneLayerTable/oneLayerTable.bum

+2 −2
Original line number Diff line number Diff line
@@ -9,11 +9,11 @@ 
<org.eventb.core.action name="InitAction2" org.eventb.core.assignment="output :∈ ℤ" org.eventb.core.label="act2"/>

</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 ≥ 0"/>

<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 ≔ 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="x &lt; 0"/>

<org.eventb.core.guard name="Guard1" org.eventb.core.label="grd1" org.eventb.core.predicate="(x &lt; 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.machineFile>
 
 No newline at end of file