Commit 0fc934da authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Add three more test cases to cover more scenarios. 

Until now we have test cases for one layer table, two layers table, three layerstable and one Simple Insulin Infusion Pump (IIP) table.
parent ae92736c

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

+1 −1
Original line number Diff line number Diff line
@@ -61,7 +61,7 @@ final public class EventBGenerator implements CheckerGenerator{ 
            case Equals:

                return "=";

            case NotEquals:

                return "/=";

                return "≠";

        }

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

    }

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

+198 −1
Original line number Diff line number Diff line
@@ -49,7 +49,7 @@ import static org.junit.Assert.assertEquals; 
public class EventBTableGeneratorTest {



    @Test

    public void exerciseEventBGenerator() {

    public void testOneLayerTableEventBGenerator() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();
@@ -82,5 +82,202 @@ public class EventBTableGeneratorTest { 
        assertEquals(expected, out);

    }



    @Test

    public void testTwoLayerTableEventBGenerator() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



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

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

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



        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("z > 0"));

        nextGrid.add(new HierarchicalCell("z == 0"));

        nextGrid.add(new HierarchicalCell("z < 0"));



        VariableCollection variableCollection = variableParser.parseVariables("x,z");

        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(variableCollection, grid);

        String out  = eventBTableGenerator.generateEventBXml();



        String expected = "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n" +

        "<org.eventb.core.machineFile org.eventb.core.configuration=\"org.eventb.core.fwd;de.prob.units.mchBase\" version=\"5\">\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"x\" org.eventb.core.identifier=\"x\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"z\" org.eventb.core.identifier=\"z\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"outputVariable\" org.eventb.core.identifier=\"outputVar\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant1\" org.eventb.core.label=\"inv1\" org.eventb.core.predicate=\"x ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant2\" org.eventb.core.label=\"inv2\" org.eventb.core.predicate=\"z ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"outputInvariant\" org.eventb.core.label=\"outputInv\" org.eventb.core.predicate=\"output ∈ ℤ\"/>\n" +

        "<org.eventb.core.event name=\"Event0\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"INITIALISATION\">\n" +

        "<org.eventb.core.action name=\"InitAction1\" org.eventb.core.assignment=\"x ≔ 0\" org.eventb.core.label=\"act1\"/>\n" +

        "<org.eventb.core.action name=\"InitAction2\" org.eventb.core.assignment=\"z ≔ 0\" org.eventb.core.label=\"act2\"/>\n" +

        "<org.eventb.core.action name=\"OutputAction\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act0\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event1\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt1\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &gt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 1\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event2\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt2\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &lt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 2\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event3\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt3\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x = 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"z &gt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 3\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event4\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt4\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x = 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"z = 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 4\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event5\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt5\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x = 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"z &lt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 5\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "</org.eventb.core.machineFile>";

        assertEquals(expected, out);



    }





    @Test

    public void testThreeLayerTableEventBGenerator() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



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

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

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



        List<HierarchicalCell> nextGrid = topCells.get(0).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("y >= 0"));

        nextGrid.add(new HierarchicalCell("y < 0"));

        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z > 0"));

        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));

        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z < 0"));



        //reset pointer nextGrid to x < 0 grid.

        nextGrid = topCells.get(2).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("w > 1"));

        nextGrid.add(new HierarchicalCell("w == 1"));

        nextGrid.add(new HierarchicalCell("w < 1"));



        VariableCollection variableCollection = variableParser.parseVariables("x,y,z,w");

        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(variableCollection, grid);

        String out  = eventBTableGenerator.generateEventBXml();



        String expected = "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n" +

        "<org.eventb.core.machineFile org.eventb.core.configuration=\"org.eventb.core.fwd;de.prob.units.mchBase\" version=\"5\">\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"x\" org.eventb.core.identifier=\"x\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"y\" org.eventb.core.identifier=\"y\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"z\" org.eventb.core.identifier=\"z\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"w\" org.eventb.core.identifier=\"w\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"outputVariable\" org.eventb.core.identifier=\"outputVar\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant1\" org.eventb.core.label=\"inv1\" org.eventb.core.predicate=\"x ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant2\" org.eventb.core.label=\"inv2\" org.eventb.core.predicate=\"y ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant3\" org.eventb.core.label=\"inv3\" org.eventb.core.predicate=\"z ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant4\" org.eventb.core.label=\"inv4\" org.eventb.core.predicate=\"w ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"outputInvariant\" org.eventb.core.label=\"outputInv\" org.eventb.core.predicate=\"output ∈ ℤ\"/>\n" +

        "<org.eventb.core.event name=\"Event0\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"INITIALISATION\">\n" +

        "<org.eventb.core.action name=\"InitAction1\" org.eventb.core.assignment=\"x ≔ 0\" org.eventb.core.label=\"act1\"/>\n" +

        "<org.eventb.core.action name=\"InitAction2\" org.eventb.core.assignment=\"y ≔ 0\" org.eventb.core.label=\"act2\"/>\n" +

        "<org.eventb.core.action name=\"InitAction3\" org.eventb.core.assignment=\"z ≔ 0\" org.eventb.core.label=\"act3\"/>\n" +

        "<org.eventb.core.action name=\"InitAction4\" org.eventb.core.assignment=\"w ≔ 0\" org.eventb.core.label=\"act4\"/>\n" +

        "<org.eventb.core.action name=\"OutputAction\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act0\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event1\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt1\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x = 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 1\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event2\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt2\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &gt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"y ≥ 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 2\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event3\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt3\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"y &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"x &gt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard3\" org.eventb.core.label=\"grd3\" org.eventb.core.predicate=\"z &gt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 3\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event4\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt4\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"y &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"x &gt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard3\" org.eventb.core.label=\"grd3\" org.eventb.core.predicate=\"z = 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 4\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event5\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt5\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"y &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"x &gt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard3\" org.eventb.core.label=\"grd3\" org.eventb.core.predicate=\"z &lt; 0\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 5\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event6\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt6\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"w &gt; 1\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 6\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event7\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt7\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"w = 1\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 7\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event8\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt8\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"x &lt; 0\"/>\n" +

        "<org.eventb.core.guard name=\"Guard2\" org.eventb.core.label=\"grd2\" org.eventb.core.predicate=\"w &lt; 1\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 8\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "</org.eventb.core.machineFile>";

        assertEquals(expected, out);



    }





    @Test

    public void testIIPTableEventBGenerator() {

        //C_pwrStatus is treated as enumerate here. It can choose values from

        //POST:0 NC:1 Ready:2 Standby:3 OffReq 4

        //C_pwrConfirm is treated as enumerate here. It can choose values from

        //False:0 True:1





        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        //if I use c_pwrStatus, error would occur

        topCells.add(new HierarchicalCell("cPwrStatus == 4"));

        topCells.add(new HierarchicalCell("cPwrStatus ~= 4"));







        VariableCollection variableCollection = variableParser.parseVariables("cPwrStatus");

        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(variableCollection, grid);

        String out  = eventBTableGenerator.generateEventBXml();



        String expected = "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n" +

        "<org.eventb.core.machineFile org.eventb.core.configuration=\"org.eventb.core.fwd;de.prob.units.mchBase\" version=\"5\">\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"cPwrStatus\" org.eventb.core.identifier=\"cPwrStatus\"/>\n" +

        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"outputVariable\" org.eventb.core.identifier=\"outputVar\"/>\n" +

        "<org.eventb.core.invariant name=\"Invariant1\" org.eventb.core.label=\"inv1\" org.eventb.core.predicate=\"cPwrStatus ∈ ℤ\"/>\n" +

        "<org.eventb.core.invariant name=\"outputInvariant\" org.eventb.core.label=\"outputInv\" org.eventb.core.predicate=\"output ∈ ℤ\"/>\n" +

        "<org.eventb.core.event name=\"Event0\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"INITIALISATION\">\n" +

        "<org.eventb.core.action name=\"InitAction1\" org.eventb.core.assignment=\"cPwrStatus ≔ 0\" org.eventb.core.label=\"act1\"/>\n" +

        "<org.eventb.core.action name=\"OutputAction\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act0\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event1\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt1\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"cPwrStatus = 4\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 1\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "<org.eventb.core.event name=\"Event2\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt2\">\n" +

        "<org.eventb.core.guard name=\"Guard1\" org.eventb.core.label=\"grd1\" org.eventb.core.predicate=\"cPwrStatus ≠ 4\"/>\n" +

        "<org.eventb.core.action name=\"Action1\" org.eventb.core.assignment=\"output ≔ 2\" org.eventb.core.label=\"act1\"/>\n" +

        "</org.eventb.core.event>\n" +

        "</org.eventb.core.machineFile>";

        assertEquals(expected, out);



    }



    VariableParser variableParser = new VariableParser();

}