Commit 0c7f72a3 authored by Yanjun Jiang's avatar Yanjun Jiang
Browse files

Convert ouput value properly. 

Convert the output values in the output Grid from Matlab format to EventB supported
format symbols properly and then collect them while traversing cells. So that we can
also have complex expression in the result Grid. Aslo, the bug that outputVariables
in test cases have no type has been fixed. The realVariableType is mainly used for the
outputVariables now.
parent 661dbfb5

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

+11 −9
Original line number Diff line number Diff line
@@ -28,10 +28,7 @@ 
 */

package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.EventBGenerator;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.*;

import org.apache.commons.lang3.StringUtils;
@@ -151,7 +148,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 


        m_cellLayerNo++;

        m_parentEventNo = m_eventNo;

        m_eventBGuards.push(handleCell(cell));

        m_eventBGuards.push(handleConditionCell(cell));

    }



    @Override
@@ -177,7 +174,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
        m_subGridCellIndex++;

        generatorGenerateEventNo();



        m_eventBGuards.push(handleCell(cell));

        m_eventBGuards.push(handleConditionCell(cell));

        collectEdgeGridValues();

        if (m_cellLayerNo <= m_refineLayerNo) {

            m_eventsXml += generateEventXml();//outputLeafCells
@@ -193,11 +190,16 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 


    private void collectEdgeGridValues() {

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

        m_collectedOutputValues.add(outputValue);

        String convertedValue = convertMatlabToEventB(outputValue, m_outputVariables.get(0).type());

        m_collectedOutputValues.add(convertedValue);

    }



    private String handleCell(Cell cell) {

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

    private String convertMatlabToEventB(String outputValue, VariableType variableType) {

        return MatlabParser.parseMatlabCode(m_variableDefinitions, outputValue).getCheckerOutput(m_eventBGenerator, variableType);

    }



    private String handleConditionCell(Cell cell) {

        return convertMatlabToEventB(cell.contents(), BooleanVariableType.Type);

    }



    public boolean isRefineRelationNecessary() {

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

+5 −5
Original line number Diff line number Diff line
@@ -110,7 +110,7 @@ public class ParameterizedEventBTableGeneratorTest { 
        cells.add(new HierarchicalCell("x < 0"));



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

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

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



        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 2);

        outputGrid.get(0,0).setContents("1");
@@ -135,11 +135,11 @@ public class ParameterizedEventBTableGeneratorTest { 
        nextGrid.add(new HierarchicalCell("z < 0"));



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

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

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



        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 5);

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

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

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

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

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

        outputGrid.get(0,4).setContents("5");
@@ -170,7 +170,7 @@ public class ParameterizedEventBTableGeneratorTest { 
        nextGrid.add(new HierarchicalCell("w < 1"));



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

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

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



        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 8);

        outputGrid.get(0,0).setContents("1");
@@ -199,7 +199,7 @@ public class ParameterizedEventBTableGeneratorTest { 
        //C_pwrConfirm is treated as enumerate here. It can choose values from

        //False:0 True:1

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

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

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



        TwoDimensionalGrid outputGrid = new TwoDimensionalGrid(1, 2);

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

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

+1 −1
Original line number Diff line number Diff line
@@ -18,7 +18,7 @@ 
<org.eventb.core.event name="Event2_1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2_1">

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

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

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

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

</org.eventb.core.event>

<org.eventb.core.event name="Event2_2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2_2">

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

src/test/resources/expected/WR/twoLayerTable/twoLayerTable_M0.bum

+1 −1
Original line number Diff line number Diff line
@@ -17,7 +17,7 @@ 
</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="output :∈ {2,3,4}" org.eventb.core.label="act1"/>

<org.eventb.core.action name="Action1" org.eventb.core.assignment="output :∈ {(1 + 1),3,4}" org.eventb.core.label="act1"/>

</org.eventb.core.event>

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

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

src/test/resources/expected/WR/twoLayerTable/twoLayerTable_M1.bum

+1 −1
Original line number Diff line number Diff line
@@ -19,7 +19,7 @@ 
<org.eventb.core.event name="Event2_1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2_1">

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

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

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

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

<org.eventb.core.refinesEvent name="evt2" org.eventb.core.target="evt2"/>

</org.eventb.core.event>

<org.eventb.core.event name="Event2_2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt2_2">