Commit 16c9e4b4 authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Add parameterized test case for NonRefinment mode. 

The JUnit paramerized class is used here instead of using a massive
class repeating the various setup/test procedures.
parent 674f46c1

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

deleted100644 → 0
+0 −346
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.ca>

 *

 * Redistribution and use in source and binary forms, with or without

 * modification, are permitted provided that the following conditions are

 * met:

 *

 *     * Redistributions of source code must retain the above copyright

 *       notice, this list of conditions and the following disclaimer.

 *     * Redistributions in binary form must reproduce the above copyright

 *       notice, this list of conditions and the following disclaimer in

 *       the documentation and/or other materials provided with the distribution

 *     * Neither the name of the McMaster Centre for Software Certification nor the names

 *       of its contributors may be used to endorse or promote products derived

 *       from this software without specific prior written permission.

 *

 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"

 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE

 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE

 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE

 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR

 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF

 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS

 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN

 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)

 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

 * POSSIBILITY OF SUCH DAMAGE.

 */

package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tablularexpression.HierarchicalCell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;

import ca.mcscert.jtet.tablularexpression.Table;

import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;



import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.List;



import static org.junit.Assert.assertEquals;



/**

 *

 * @author Yanjun Jiang <jiangy76@mcmaster.ca>

 */

@RunWith(JUnit4.class)

public class EventBTableGeneratorTest {



    @Test

    public void testOneLayerTableEventBGenerator() {



        Table table = new Table("oneLayerTable", variableParser.parseVariables("x,output"));



        /*********construct left conditional Grid***********/

        HierarchicalGrid leftGrid = table.getLeftGrid();

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



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

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





        //construct Output Variables(Acquired from TopGrid in Matlab GUI)

        List<Variable> outputVariables = table.getOutputVariables();

        outputVariables.add(new Variable("output",null));





        //construct output Grid

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 2);

        outputGrid.get(0,0).setContents("1");

        outputGrid.get(0,1).setContents("2");

        table.getVariableOutputs().add(outputGrid);





        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(table);

        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=\"output\" org.eventb.core.identifier=\"output\"/>\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=\"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=\"output ≔ 0\" org.eventb.core.label=\"act2\"/>\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 &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.machineFile>";

        assertEquals(expected, out);

    }





    @Test

    public void testTwoLayerTableEventBGenerator() {

        Table table = new Table("twoLayerTable", variableParser.parseVariables("x,z,output"));



        //construct left condition Grid

        HierarchicalGrid leftGrid = table.getLeftGrid();

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



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

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

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



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

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

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

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





        //construct Output Variables(Acquired from TopGrid in Matlab GUI)

        List<Variable> outputVariables = table.getOutputVariables();

        outputVariables.add(new Variable("output",null));



        //construct output Grid

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 5);

        outputGrid.get(0,0).setContents("1");

        outputGrid.get(0,1).setContents("2");

        outputGrid.get(0,2).setContents("3");

        outputGrid.get(0,3).setContents("4");

        outputGrid.get(0,4).setContents("5");

        table.getVariableOutputs().add(outputGrid);



        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(table);

        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=\"output\" org.eventb.core.identifier=\"output\"/>\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=\"Invariant3\" org.eventb.core.label=\"inv3\" 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=\"InitAction3\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act3\"/>\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 = 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 ≔ 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 = 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 &lt; 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 &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() {

        Table table = new Table("threeLayerTable", variableParser.parseVariables("x,y,z,w,output"));



        //construct left condition Grid

        HierarchicalGrid leftGrid = table.getLeftGrid();

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



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

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

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



        List<HierarchicalCell> nextGrid = cells.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"));



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

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

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

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





        //construct Output Variables(Acquired from TopGrid in Matlab GUI)

        //construct Output Variables(Acquired from TopGrid in Matlab GUI)

        List<Variable> outputVariables = table.getOutputVariables();

        outputVariables.add(new Variable("output",null));





        //construct output Grid

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 8);

        outputGrid.get(0,0).setContents("1");

        outputGrid.get(0,1).setContents("2");

        outputGrid.get(0,2).setContents("3");

        outputGrid.get(0,3).setContents("4");

        outputGrid.get(0,4).setContents("5");

        outputGrid.get(0,5).setContents("6");

        outputGrid.get(0,6).setContents("7");

        outputGrid.get(0,7).setContents("8");

        table.getVariableOutputs().add(outputGrid);



        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(table);

        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=\"output\" org.eventb.core.identifier=\"output\"/>\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=\"Invariant5\" org.eventb.core.label=\"inv5\" 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=\"InitAction5\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act5\"/>\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.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 ≔ 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=\"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 ≔ 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 = 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 &lt; 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.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



        Table table = new Table("IIP", variableParser.parseVariables("cPwrStatus,cPwrConfirm"));



        //construct left condition Grid

        HierarchicalGrid leftGrid = table.getLeftGrid();

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



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

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





        //construct Output Variables(Acquired from TopGrid in Matlab GUI)

        List<Variable> outputVariables = table.getOutputVariables();

        outputVariables.add(new Variable("cPwrConfirm",null));



        //construct outputGrid

        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 2);

        outputGrid.get(0,0).setContents("0");

        outputGrid.get(0,1).setContents("1");

        table.getVariableOutputs().add(outputGrid);



        EventBTableGenerator eventBTableGenerator = new EventBTableGenerator(table);

        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=\"cPwrConfirm\" org.eventb.core.identifier=\"cPwrConfirm\"/>\n" +

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

        "<org.eventb.core.invariant name=\"Invariant2\" org.eventb.core.label=\"inv2\" org.eventb.core.predicate=\"cPwrConfirm ∈ ℤ\"/>\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=\"InitAction2\" org.eventb.core.assignment=\"cPwrConfirm ≔ 0\" org.eventb.core.label=\"act2\"/>\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=\"cPwrConfirm ≔ 0\" 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=\"cPwrConfirm ≔ 1\" org.eventb.core.label=\"act1\"/>\n" +

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

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

        assertEquals(expected, out);



    }



    VariableParser variableParser = new VariableParser();

}

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

0 → 100644
+250 −0

File added.

Preview size limit exceeded, changes collapsed.

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

0 → 100644
+17 −0

File added.

Preview size limit exceeded, changes collapsed.

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

0 → 100644
+19 −0

File added.

Preview size limit exceeded, changes collapsed.

src/test/resources/expected/NR/momThreeLayerTable/.project

0 → 100644
+17 −0

File added.

Preview size limit exceeded, changes collapsed.