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

Started working on generating EventB projects from tabular expressions. 

For now, only single output single grid tables are supported, and only with simple one operator expressions.
Each row in the conditions grid corresponds a single event in EventB, with each cell in the row corresponding to a guard for the event.
parent 7300fcf8

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBTableGenerator.java

0 → 100644
+72 −0
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.EventBGenerator;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator;

import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;



/**

 *

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

 */

final public class EventBTableGenerator {



    public EventBTableGenerator(VariableCollection variableDefinitions, HierarchicalGrid grid) {

        m_variableDefinitions = variableDefinitions;

        m_grid  = grid;

    }



    public String generateEventBXml(){

        final String versionEncodingXml = "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";

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

        final String machineFileCfgPostXml = "</org.eventb.core.machineFile>";



        //Step 1: Generate the Pre Xml

        m_output += versionEncodingXml;

        m_output += machineFileCfgPreXml;



        //Step 2: Generate the Variables & Invariants Xml

        m_output += m_eventBGenerator.GenerateVariablesDeclaration(m_variableDefinitions);



        //Step 3: Generate the Events Xml

        m_output  += HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(m_grid, (new HierarchicalGridEventBGenerator(m_variableDefinitions)));



        //Step 3: Generate the Post Xml

        m_output += machineFileCfgPostXml;



        return m_output;

    }



    String m_output = "";

    HierarchicalGrid m_grid;

    VariableCollection m_variableDefinitions;

    EventBGenerator m_eventBGenerator = new EventBGenerator();

}

src/main/java/ca/mcscert/jtet/eventbgenerator/HierarchicalGridEventBGenerator.java

0 → 100644
+136 −0
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.BooleanVariableType;

import ca.mcscert.jtet.expression.EventBGenerator;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator;



import java.util.ArrayDeque;

import java.util.Deque;



/**

 * This class generate common non-initialisation events

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

 */

final public class HierarchicalGridEventBGenerator implements HierarchcialGridCheckerGenerator {



    public HierarchicalGridEventBGenerator(VariableCollection variableDefinitions) {

        m_variableDefinitions = variableDefinitions;

    }



    private String getCurrentEventName(){

        return "Event" + m_currentEventNo;

    }



    private String generateEventLabelXml(int eventNo) {

        return "<org.eventb.core.event name=\"" + getCurrentEventName() + "\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"evt" + eventNo + "\">\n";

    }



    private String generateEventGuardXml(int guardNo, String guard) {

        return "<org.eventb.core.guard name=\"Guard" + guardNo + "\" org.eventb.core.label=\"grd" + + guardNo + "\" org.eventb.core.predicate=\"" + guard +"\"/>\n";

    }



    private String generateEventActionXmlPre() {

        int actionNo = 1;

        return "<org.eventb.core.action name=\"Action" + actionNo + "\" org.eventb.core.assignment=\"output ≔ " + m_currentEventNo +"\"";

    }



    private String generateEventActionXmlPost(int actionNo) {

        return " org.eventb.core.label=\"act" + actionNo + "\"/>\n";

    }



    private String generateEventActionsXml(int actionNo) {

        return generateEventActionXmlPre() + generateEventActionXmlPost(actionNo);

    }





    private String generateEventXml(String currentCellContent) {

        String ret = "";

        final String eventXmlPost = "</org.eventb.core.event>\n";

        int guardNo = 1;

        ret += generateEventLabelXml(m_currentEventNo);



        for (String parentCellContent: m_parentCellsEventBCode){

            ret += generateEventGuardXml(guardNo++, parentCellContent);

        }

        ret += generateEventGuardXml(guardNo, currentCellContent);

        ret += generateEventActionsXml(1);

        ret += eventXmlPost;



        return ret;

    }





    private void outputCell(String currentCellContent) {

        m_eventsXml += generateEventXml(currentCellContent);

    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

        m_parentCellsEventBCode.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, m_booleanType));

    }



    @Override

    public void ascendFromGrid() {

        m_parentCellsEventBCode.removeFirst();

    }



    @Override

    public void handleEdgeCell(Cell cell) {

    }



    @Override

    public void handleLeafCell(Cell cell) {

        m_currentEventNo++;

        String parsedCellCode = handleCell(cell);

        outputCell(parsedCellCode);

    }



    public String handleCell(Cell cell) {

        return MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, m_booleanType);

    }



    @Override

    public String getFinalString() {

        return m_eventsXml;

    }



    Deque<String> m_parentCellsEventBCode = new ArrayDeque<String>();

    int m_currentEventNo = 0;



    String m_eventsXml = "";



    VariableCollection m_variableDefinitions;

    static BooleanVariableType m_booleanType = new BooleanVariableType();

    EventBGenerator m_eventBGenerator = new EventBGenerator();

}

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

0 → 100644
+233 −0
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.expression;



import org.apache.commons.lang3.StringUtils;

import java.util.Map;



/**

 *

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

 */

final public class EventBGenerator implements CheckerGenerator{



    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {

            case Addition:

                return "+";

            case Minus:

                return "-";

            case Multiplication:

                return "*";

            case Division:

                return "/";

            case Exponentiation:

                return "^";

            case GreaterThen:

                return "&gt;";

            case GreaterThenEqual:

                return "≥";

            case LessThen:

                return "&lt;";

            case LessThenEqual:

                return "≤";

            case Equals:

                return "=";

            case NotEquals:

                return "/=";

        }

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

    }



    protected static String ConvertToOutputOp(BinaryOperation op) {

        return GetInfixSymbolFor(op);

    }



    @Override

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

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

    }



    @Override

    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {

          return "(" + EventBGenerator.ConvertToOutputOp(op) + " " + expression + ")";

    }





    private static String ConvertToOutputOp(UnaryOperation op) {

        switch (op) {

            case Negation:

                return "NOT";

            case Minus:

                    return "-";

        }

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

    }



    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "ℤ";

        } else {

            throw new IllegalArgumentException("EventB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

    }



    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

        String variablesRelatedXml = "";



        variablesRelatedXml += generateVariablesXml(variableCollection);

        variablesRelatedXml += generateOutputVariableXml();

        variablesRelatedXml += generateInvariantsXml(variableCollection);

        variablesRelatedXml += generateOutputInvariantXml();

        variablesRelatedXml += generateInitEventXml(variableCollection);



        return variablesRelatedXml;

    }



    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {

            if (value.contains(".")) {

                String[] fraction = value.split("\\.");



                String res = "(";

                res += StringUtils.join(fraction, "");

                res += "/1" + StringUtils.repeat('0', fraction[1].length()) + ")";



                return res;

            } else {

                return value;

            }

        }  else {

            throw new IllegalArgumentException("Can't cast literal to that type!");

        }

    }



    private String generateVariablesXml(VariableCollection variableCollection) {

        final String variableXmlPost = "\"/>\n";

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the variables one by one.

        for(Variable var : vars.values()) {

            ret += generateVariableXmlPre(var.name());

            ret += var.name();

            ret += variableXmlPost;

        }



        return ret;

    }



    private String generateInvariantXmlPre(int invariantNum) {

        return "<org.eventb.core.invariant name=\""  + "Invariant" + invariantNum + "\" org.eventb.core.label=\""  + "inv" + invariantNum + "\" org.eventb.core.predicate=\"";

    }



    private String generateVariableXmlPre(String variableName) {

        return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\""  + variableName +"\" org.eventb.core.identifier=\"";

    }



    private String generateOutputVariableXml() {

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

    }



    private String generateOutputInvariantXml() {

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

    }



    private String generateInvariantsXml(VariableCollection variableCollection) {

        String ret = "";

        int  invariantsNum = 1;

        final String invariantXmlPost = "\"/>\n";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Invariants one by one.

        for (Variable var : vars.values()) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.name();

            ret += " ∈ ";

            ret += GenerateVariableType(var.type());

            ret += invariantXmlPost;

            invariantsNum++;

        }



        return ret;

    }



    private String generateInitEventXmlPre() {

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

    }



    private String generateInitEventXmlPost() {

        return "</org.eventb.core.event>\n";

    }



    private String generateInitEventOutputActionXml(int actionNo) {

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

    }



    private String generateInitEventActionXmlPre(int actionNo) {



        return "<org.eventb.core.action name=\"InitAction" + actionNo  + "\" org.eventb.core.assignment=\"";

    }



    private String generateInitEventActionXmlPost(int actionNo) {



        return "\" org.eventb.core.label=\"act" + actionNo + "\"/>";

    }



    private String generateInitEventXml(VariableCollection variableCollection) {

        String ret = "";

        ret += generateInitEventXmlPre();

        ret += generateInitEventActionsXml(variableCollection);

        ret += generateInitEventOutputActionXml(0);

        ret += generateInitEventXmlPost();



        return ret;

    }



    private String generateInitEventActionsXml(VariableCollection variableCollection) {

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Initialisation actions one by one.

        int actionNo = 0;

        for (Variable var : vars.values()) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.name();

            ret += " ≔ 0";

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

        }



        return ret;

    }

}

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

0 → 100644
+86 −0
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.VariableCollection;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tablularexpression.HierarchicalCell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;



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 exerciseEventBGenerator() {

        HierarchicalGrid grid = new HierarchicalGrid();

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



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

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



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

        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=\"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=\"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=\"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 &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);

    }



    VariableParser variableParser = new VariableParser();

}

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

+14 −0
Original line number Diff line number Diff line
@@ -77,6 +77,20 @@ public class GenericVariableDeclarationGeneratorTest { 
                        "x:BITVECTOR(8);\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\ny:MyEnum;\n"

                },

                {new EventBGenerator(),

                        "<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=\"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=\"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=\"OutputAction\" org.eventb.core.assignment=\"output ≔ 0\" org.eventb.core.label=\"act0\"/>\n" +

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

                        null,

                        null,

                        null,

                        null

                }

        });

    }