Commit 2e852877 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Change EventB to use the new output cell fetching mechanism. 

The EventB generator code can now fetch output cells using the value passed
in.  It also gains support for multiple output tables in the process, since
it's easier to support that now, then include funky hacks for to support only
single variable tables.

Also bring back the momThreeLayer table for testing EventB's multiple output
feature.
parent 5ca0a995

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

+27 −24
Original line number Diff line number Diff line
@@ -46,9 +46,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
        m_refineMode = refineMode;

        m_refineLayerNo = refineLayerNo;

        m_variableDefinitions = table.getVariables();

        m_outputVariable = m_variableDefinitions.getOutputVariables().values().iterator().next();

        m_tableName = table.getTableName();

        m_outputGrid = table.getVariableOutputs().get(m_outputVariable);

    }



    private String generateEventGuardXml(int guardNo, String guard) {
@@ -61,21 +59,25 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 


    private String generateEventActionsXml() {

        String ret = "";

        String outputVariable;

        String outputVariableName;

        String outputValue;

        int actionNo = 0;



        if (m_collectedOutputValues.size() == 1) { // leaf action

            outputValue = m_collectedOutputValues.get(0);

            outputVariable = m_outputVariable.name();

            ret += generateOneEventActionXml(actionNo, outputVariable, outputValue);

        for (Map.Entry<Variable, List<String>> variableOutputs : m_collectedOutputValues.entrySet()) {

            List<String> collectedOutputValues = variableOutputs.getValue();

            Variable outputVariable = variableOutputs.getKey();

            if (collectedOutputValues.size() == 1) { // leaf action

                outputValue = collectedOutputValues.get(0);

                outputVariableName = outputVariable.name();

                ret += generateOneEventActionXml(actionNo, outputVariableName, outputValue);

            } else {

            String topGridName = m_outputVariable.name();

                outputVariableName = outputVariable.name();

                String columnVector = "{";

            columnVector += StringUtils.join(m_collectedOutputValues, ',');

                columnVector += StringUtils.join(collectedOutputValues, ',');

                columnVector += "}";

            ret += "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + topGridName + " :∈ " + columnVector + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";

            m_collectedOutputValues.clear();

                ret += "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + outputVariableName + " :∈ " + columnVector + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";

            }

            actionNo++;

        }



        return ret;
@@ -170,12 +172,11 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 


    @Override

    public void handleLeafCell(Cell cell, Map<Variable, Cell> outputCells) {

        m_tableRowNo++;

        m_subGridCellIndex++;

        generatorGenerateEventNo();



        m_eventBGuards.push(handleConditionCell(cell));

        collectEdgeGridValues();

        collectEdgeGridValues(outputCells);

        if (m_cellLayerNo <= m_refineLayerNo) {

            m_eventsXml += generateEventXml();//outputLeafCells

        }
@@ -188,10 +189,15 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
        }

    }



    private void collectEdgeGridValues() {

        String outputValue = m_outputGrid.get(0, m_tableRowNo - 1).contents();

        String convertedValue = convertMatlabToEventB(outputValue, m_outputVariable.type());

        m_collectedOutputValues.add(convertedValue);

    private void collectEdgeGridValues(Map<Variable, Cell> outputCells) {

        for(Map.Entry<Variable, Cell> outputCell : outputCells.entrySet()) {

            String outputValue = outputCell.getValue().contents();

            String convertedValue = convertMatlabToEventB(outputValue, outputCell.getKey().type());

            if(!m_collectedOutputValues.containsKey(outputCell.getKey())) {

                m_collectedOutputValues.put(outputCell.getKey(), new ArrayList<String>());

            }

            m_collectedOutputValues.get(outputCell.getKey()).add(convertedValue);

        }

    }



    private String convertMatlabToEventB(String outputValue, VariableType variableType) {
@@ -211,7 +217,6 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
        return m_eventsXml;

    }



    int m_tableRowNo = 0;

    int m_cellLayerNo = 0;

    int m_subGridCellIndex = 0;

    int m_refineLayerNo = 0;//is also the current column number
@@ -219,10 +224,8 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    String m_tableName = "";

    String m_eventNo = "";//like evt1_3_2

    String m_parentEventNo = "";//like evt1_3

    TwoDimensionalGrid m_outputGrid;

    VariableCollection m_variableDefinitions;

    final Variable m_outputVariable; // Temporary during refactor, while the single variable support is still in place.

    List<String> m_collectedOutputValues = new ArrayList<String>();

    Map<Variable, List<String>> m_collectedOutputValues = new LinkedHashMap<Variable, List<String>>();

    EventBExpressionGenerator m_eventBExpressionGenerator = new EventBExpressionGenerator();

    Stack<String> m_eventBGuards = new Stack<String>();

    Stack<String> m_oldParentEventNo = new Stack<String>();

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

+60 −5
Original line number Diff line number Diff line
@@ -69,7 +69,11 @@ public class ParameterizedEventBTableGeneratorTest { 
                {

                  makeIIPTable(),

                        1

                }

                },

                {

                        makeMultipleOutputTable(),

                        3

                },

        });

    }
@@ -181,6 +185,55 @@ public class ParameterizedEventBTableGeneratorTest { 
        return table;

    }



    public static Table makeMultipleOutputTable() {

        Variable outputVar1 = new Variable("output1", new RealVariableType());

        Variable outputVar2 = new Variable("output2", new RealVariableType());

        Table table = initialize("momThreeLayerTable", "x,y,z,w", outputVar1, outputVar2);



        HierarchicalGrid leftGrid = table.getLeftGrid();



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

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

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

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



        List<HierarchicalCell> nextGrid = cells.get(0).getSubHierarchy();

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

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

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

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

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



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

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

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

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



        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().put(outputVar1, outputGrid);



        outputGrid = new TwoDimensionalGrid(1, 8);

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

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

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

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

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

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

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

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

        table.getVariableOutputs().put(outputVar2, outputGrid);



        return table;

    }



    public static Table makeIIPTable() {

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

        //False:0 True:1
@@ -203,11 +256,13 @@ public class ParameterizedEventBTableGeneratorTest { 
        return table;

    }



    public static Table initialize(String tableName, String inputVariables, Variable outputVariable) {

        Map<String, Variable> outputVariables = new HashMap<String, Variable>(1);

        outputVariables.put(outputVariable.name(), outputVariable);

    public static Table initialize(String tableName, String inputVariables, Variable...outputVariables) {

        Map<String, Variable> outputVariablesMap = new LinkedHashMap<String, Variable>(1);

        for(Variable outputVariable : outputVariables) {

            outputVariablesMap.put(outputVariable.name(), outputVariable);

        }



        VariableCollection variableCollection = new VariableCollection(m_variableParser.parseVariables(inputVariables), new PartialVariableCollection(outputVariables));

        VariableCollection variableCollection = new VariableCollection(m_variableParser.parseVariables(inputVariables), new PartialVariableCollection(outputVariablesMap));

        return new Table(tableName, variableCollection);

    }

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

0 → 100644
+17 −0
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>

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

0 → 100644
+73 −0
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="(x &gt; 0)"/>

<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="(y &lt; 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="(x &gt; 0)"/>

<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="(y &lt; 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="(x &gt; 0)"/>

<org.eventb.core.guard name="Guard2" org.eventb.core.label="grd2" org.eventb.core.predicate="(y &lt; 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

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

0 → 100644
+17 −0
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>