Commit b33e364c authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Make the Table class use an arbitrary expression parser. 

The Table class now accepts an ExpressionParser interface for its constructor,
allowing for cell's expression to be written in any (single) language.

Update tests to continue to use the Matlab parser.
parent 36df2034

src/main/java/ca/mcscert/jtet/tabularexpression/Table.java

+20 −18
Original line number Diff line number Diff line
@@ -31,7 +31,7 @@ package ca.mcscert.jtet.tabularexpression; 
import ca.mcscert.jtet.expression.Expression;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.parsers.ExpressionParser;



import java.util.HashMap;

import java.util.LinkedHashMap;
@@ -42,9 +42,10 @@ import java.util.Map; 
 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

public class Table {

    public Table(String name, VariableCollection variables) {

    public Table(String name, VariableCollection variables, ExpressionParser expressionParser) {

        this.name = name;

        this.m_variables = variables;

        this.m_expressionParser = expressionParser;

    }



    public void verifyTable() throws IllegalTableSetup {
@@ -82,8 +83,8 @@ public class Table { 
        return m_variables;

    }



    private Expression parseMatlabCode(Cell cell) {

        return MatlabParser.Parser.parseExpressionString(m_variables, cell.contents());

    private Expression parseExpressionInCell(Cell cell) {

        return m_expressionParser.parseExpressionString(m_variables, cell.contents());

    }



    private int HandleLeftGrid(SubHierarchyFetcher grid, HierarchicalGridDepthFirstCheckerGenerator generator, int outputCellXIndex, int outputCellYIndex) {
@@ -93,21 +94,21 @@ public class Table { 


            if (cell.getSubHierarchy().isEmpty()) {

                if (!topGrid.getSubHierarchy().isEmpty()) {

                    generator.handleEdgeCell(parseMatlabCode(cell));

                    generator.descendIntoGridFromCell(parseMatlabCode(cell));

                    generator.handleEdgeCell(parseExpressionInCell(cell));

                    generator.descendIntoGridFromCell(parseExpressionInCell(cell));

                    HandleTopGrid(topGrid, generator, outputCellXIndex, outputCellYIndex);

                    generator.ascendFromGrid();

                } else {

                    Map<Variable, Expression> outputCells = new LinkedHashMap<Variable, Expression>();

                    for (Variable outputVariable : m_variables.getOutputVariables().values()) {

                        outputCells.put(outputVariable, parseMatlabCode(variableOutputs.get(outputVariable).get(outputCellXIndex, outputCellYIndex)));

                        outputCells.put(outputVariable, parseExpressionInCell(variableOutputs.get(outputVariable).get(outputCellXIndex, outputCellYIndex)));

                    }

                    generator.handleLeafCell(parseMatlabCode(cell), outputCells);

                    generator.handleLeafCell(parseExpressionInCell(cell), outputCells);

                }

                outputCellYIndex++;

            } else {

                generator.handleEdgeCell(parseMatlabCode(cell));

                generator.descendIntoGridFromCell(parseMatlabCode(cell));

                generator.handleEdgeCell(parseExpressionInCell(cell));

                generator.descendIntoGridFromCell(parseExpressionInCell(cell));

                outputCellYIndex = HandleLeftGrid(cell, generator, outputCellXIndex, outputCellYIndex);

                generator.ascendFromGrid();

            }
@@ -123,13 +124,13 @@ public class Table { 
            if (cell.getSubHierarchy().isEmpty()) {

                Map<Variable, Expression> outputCells = new LinkedHashMap<Variable, Expression>();

                for(Variable outputVariable : m_variables.getOutputVariables().values()) {

                    outputCells.put(outputVariable, parseMatlabCode(variableOutputs.get(outputVariable).get(outputCellXIndex, outputCellYIndex)));

                    outputCells.put(outputVariable, parseExpressionInCell(variableOutputs.get(outputVariable).get(outputCellXIndex, outputCellYIndex)));

                }

                generator.handleLeafCell(parseMatlabCode(cell), outputCells);

                generator.handleLeafCell(parseExpressionInCell(cell), outputCells);

                outputCellXIndex++;

            } else {

                generator.handleEdgeCell(parseMatlabCode(cell));

                generator.descendIntoGridFromCell(parseMatlabCode(cell));

                generator.handleEdgeCell(parseExpressionInCell(cell));

                generator.descendIntoGridFromCell(parseExpressionInCell(cell));

                outputCellXIndex = HandleTopGrid(cell, generator, outputCellXIndex, outputCellYIndex);

                generator.ascendFromGrid();

            }
@@ -152,9 +153,9 @@ public class Table { 
            HierarchicalCell cell = cells.get(i);



            if (cell.getSubHierarchy().isEmpty() && !(checkTopGrid && !topGrid.getSubHierarchy().isEmpty())) {

                generator.handleLeafCell(parseMatlabCode(cell));

                generator.handleLeafCell(parseExpressionInCell(cell));

            } else {

                generator.handleEdgeCell(parseMatlabCode(cell));

                generator.handleEdgeCell(parseExpressionInCell(cell));

            }

        }
@@ -162,11 +163,11 @@ public class Table { 
            HierarchicalCell cell = cells.get(i);



            if (!cell.getSubHierarchy().isEmpty()) {

                generator.descendIntoGridFromCell(parseMatlabCode(cell));

                generator.descendIntoGridFromCell(parseExpressionInCell(cell));

                HandleGrid(cell, generator, checkTopGrid);

                generator.ascendFromGrid();

            } else if (checkTopGrid && !topGrid.getSubHierarchy().isEmpty()) {

                generator.descendIntoGridFromCell(parseMatlabCode(cell));

                generator.descendIntoGridFromCell(parseExpressionInCell(cell));

                HandleGrid(topGrid, generator, false);

                generator.ascendFromGrid();

            }
@@ -184,6 +185,7 @@ public class Table { 


    private String name;

    private VariableCollection m_variables;

    private final ExpressionParser m_expressionParser;

    private final HierarchicalGrid leftGrid = new HierarchicalGrid();

    private final HierarchicalGrid topGrid = new HierarchicalGrid();

    private final Map<Variable, TwoDimensionalGrid> variableOutputs = new HashMap<Variable, TwoDimensionalGrid>();

src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java

+4 −3
Original line number Diff line number Diff line
@@ -29,6 +29,7 @@ 
package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tabularexpression.HierarchicalCell;

import ca.mcscert.jtet.tabularexpression.Table;
@@ -50,7 +51,7 @@ public class HierarchicalGridCVC3GeneratorTest { 
    // Exercise the cvc3 generator using a table designed in matlab.

    @Test

    public void exerciseCVC3Generator() {

        Table table = new Table(null, variableCollection);

        Table table = new Table(null, variableCollection, MatlabParser.Parser);



        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();
@@ -102,7 +103,7 @@ public class HierarchicalGridCVC3GeneratorTest { 
    // Exercise the cvc3 generator's overflow protection

    @Test

    public void testCVC3GeneratorUnsignedOverflow() {

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x:fixedt(0,8,0),y:fixedt(0,8,0)")));

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x:fixedt(0,8,0),y:fixedt(0,8,0)")), MatlabParser.Parser);



        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();
@@ -152,7 +153,7 @@ public class HierarchicalGridCVC3GeneratorTest { 


    @Test

    public void testCVC3GeneratorSignedOverflow() {

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x:fixedt(1,8,0),y:fixedt(1,8,0)")));

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x:fixedt(1,8,0),y:fixedt(1,8,0)")), MatlabParser.Parser);



        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();

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

+2 −1
Original line number Diff line number Diff line
@@ -29,6 +29,7 @@ 
package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tabularexpression.*;

import ca.mcscert.jtet.parsers.VariableParser;
@@ -258,7 +259,7 @@ public class ParameterizedEventBTableGeneratorTest { 


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

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

        return new Table(tableName, variableCollection);

        return new Table(tableName, variableCollection, MatlabParser.Parser);

    }



    public void doTest(RefinementMode refineMode) throws IOException {

src/test/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGeneratorTest.java

+3 −4
Original line number Diff line number Diff line
@@ -32,15 +32,14 @@ import ca.mcscert.jtet.expression.PartialVariableCollection; 
import ca.mcscert.jtet.expression.RealType;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tabularexpression.*;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.HashMap;

import java.util.List;

import java.util.Map;



import static org.junit.Assert.assertEquals;
@@ -55,7 +54,7 @@ public class HierarchicalGridSALGeneratorTest { 
    @Test

    public void exerciseCVC3Generator() {

        Variable outputVar = new Variable("output", new RealType());

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z"), new PartialVariableCollection(outputVar)));

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z"), new PartialVariableCollection(outputVar)), MatlabParser.Parser);

        List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();



        topCells.add(new HierarchicalCell("x > 0"));
@@ -85,7 +84,7 @@ public class HierarchicalGridSALGeneratorTest { 
    // Test the smtlib generator using an empty table

    @Test

    public void testEmptyTable() {

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("")));

        Table table = new Table(null, new VariableCollection(variableParser.parseVariables("")), MatlabParser.Parser);



        String out = table.walk(new HierarchicalGridSALGenerator(null));

src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerTest.java

+5 −4
Original line number Diff line number Diff line
@@ -29,6 +29,7 @@ 
package ca.mcscert.jtet.smtlibchecker;



import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.tabularexpression.HierarchicalCell;

import ca.mcscert.jtet.tabularexpression.Table;
@@ -48,7 +49,7 @@ import static org.junit.Assert.*; 
public class CheckerRunnerTest {

    @Test

    public void TestRunningZ3() {

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z")));

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z")), MatlabParser.Parser);

        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();



        topCells.add(new HierarchicalCell("x > 0"));
@@ -76,7 +77,7 @@ public class CheckerRunnerTest { 
    }

    @Test

    public void TestRunningZ3WithNegative() {

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z")));

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x,z")), MatlabParser.Parser);

        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();



        topCells.add(new HierarchicalCell("x > 0"));
@@ -99,7 +100,7 @@ public class CheckerRunnerTest { 
    }

    @Test

    public void TestRunningZ3WithFractionalReturn() {

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x")));

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x")), MatlabParser.Parser);

        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();



        topCells.add(new HierarchicalCell("x > 0"));
@@ -114,7 +115,7 @@ public class CheckerRunnerTest { 
    }

    @Test

    public void TestRunningZ3WithNegativeFractionalReturn() {

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x")));

        final Table table = new Table(null, new VariableCollection(variableParser.parseVariables("x")), MatlabParser.Parser);

        final List<HierarchicalCell> topCells = table.getLeftGrid().getSubHierarchy();



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