Commit 73ba00d8 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Move the walker interfaces over to accepting Expressions instead of Cells. 

All the walkers now use expressions internally, instead of Cells.  This allows
the parsing to be used into the Table class, avoiding having the walkers
needing the VariableCollection for a given table, simplifying their constructors
more.

Also clean up the imports, as they could be simplified due to this change.
Some imports may have not been necessary before this as well.
parent 2e852877

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+7 −13
Original line number Diff line number Diff line
@@ -29,10 +29,7 @@ 
package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.expression.ExpressionGeneratorSpy;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridBreadthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.Cell;





import java.util.ArrayList;
@@ -48,8 +45,7 @@ import org.apache.commons.lang3.StringUtils; 
 */

final public class HierarchicalGridCVC3Generator implements HierarchicalGridBreadthFirstCheckerGenerator {



    public HierarchicalGridCVC3Generator(VariableCollection variableDefinitions, int queryCountStart) {

        m_variableDefinitions = variableDefinitions;

    public HierarchicalGridCVC3Generator(int queryCountStart) {

        m_currentTCC = queryCountStart;

    }
@@ -106,11 +102,11 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

    public void descendIntoGridFromCell(Expression cellExpression) {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3ExpressionGenerator, BooleanVariableType.Type));

        m_parentCellsCVC3Code.addFirst(cellExpression.getCheckerOutput(m_CVC3ExpressionGenerator, BooleanVariableType.Type));

        m_currentlyRunning = true;

    }
@@ -123,15 +119,15 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
    }



    @Override

    public void handleEdgeCell(Cell inputCell) {

        handleLeafCell(inputCell);

    public void handleEdgeCell(Expression inputCellExpression) {

        handleLeafCell(inputCellExpression);

    }



    @Override

    public void handleLeafCell(Cell cell) {

    public void handleLeafCell(Expression inputCellExpression) {

        // First get the appropriate CVC3 code from matlab.  Capture generation for further processing.

        ExpressionGeneratorSpy spy = new ExpressionGeneratorSpy(m_CVC3ExpressionGenerator);

        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(spy, BooleanVariableType.Type);

        String newCellCode = inputCellExpression.getCheckerOutput(spy, BooleanVariableType.Type);



        // Next, find all the fixed point expressions and handle them.

        for(ExpressionGeneratorSpy.SpiedBinaryOp op : spy.getBinaryOps()) {
@@ -255,7 +251,5 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
    String m_output = "";

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



    // To fix properly.

    VariableCollection m_variableDefinitions;

    CVC3ExpressionGenerator m_CVC3ExpressionGenerator = new CVC3ExpressionGenerator();

}

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

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

package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.*;

import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.Expression;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableType;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridDepthFirstCheckerGenerator;

import org.apache.commons.lang3.StringUtils;

import ca.mcscert.jtet.tablularexpression.Table;
@@ -45,7 +47,6 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    public HierarchicalGridEventBGenerator(RefinementMode refineMode, int refineLayerNo, Table table) {

        m_refineMode = refineMode;

        m_refineLayerNo = refineLayerNo;

        m_variableDefinitions = table.getVariables();

        m_tableName = table.getTableName();

    }
@@ -143,14 +144,14 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

    public void descendIntoGridFromCell(Expression inputCellExpression) {

        m_oldParentEventNo.push(m_parentEventNo);

        m_oldSubGridCellIndex.push(m_subGridCellIndex);

        m_subGridCellIndex = 0;



        m_cellLayerNo++;

        m_parentEventNo = m_eventNo;

        m_eventBGuards.push(handleConditionCell(cell));

        m_eventBGuards.push(handleConditionCellExpression(inputCellExpression));

    }



    @Override
@@ -165,18 +166,18 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    }



    @Override

    public void handleEdgeCell(Cell cell) {

    public void handleEdgeCell(Expression inputCellExpression) {

        m_subGridCellIndex++;

        generatorGenerateEventNo();

    }



    @Override

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

    public void handleLeafCell(Expression inputCellExpression, Map<Variable, Expression> outputCellsExpression) {

        m_subGridCellIndex++;

        generatorGenerateEventNo();



        m_eventBGuards.push(handleConditionCell(cell));

        collectEdgeGridValues(outputCells);

        m_eventBGuards.push(handleConditionCellExpression(inputCellExpression));

        collectEdgeGridValues(outputCellsExpression);

        if (m_cellLayerNo <= m_refineLayerNo) {

            m_eventsXml += generateEventXml();//outputLeafCells

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

    }



    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());

    private void collectEdgeGridValues(Map<Variable, Expression> outputCellsExpression) {

        for(Map.Entry<Variable, Expression> outputCell : outputCellsExpression.entrySet()) {

            Expression outputExpression = outputCell.getValue();

            String convertedValue = convertExpressionToEventB(outputExpression, outputCell.getKey().type());

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

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

            }
@@ -200,12 +201,12 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
        }

    }



    private String convertMatlabToEventB(String outputValue, VariableType variableType) {

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

    private String convertExpressionToEventB(Expression expression, VariableType variableType) {

        return expression.getCheckerOutput(m_eventBExpressionGenerator, variableType);

    }



    private String handleConditionCell(Cell cell) {

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

    private String handleConditionCellExpression(Expression inputCellExpression) {

        return convertExpressionToEventB(inputCellExpression, BooleanVariableType.Type);

    }



    public boolean isRefineRelationNecessary() {
@@ -224,7 +225,6 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    String m_tableName = "";

    String m_eventNo = "";//like evt1_3_2

    String m_parentEventNo = "";//like evt1_3

    VariableCollection m_variableDefinitions;

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

    EventBExpressionGenerator m_eventBExpressionGenerator = new EventBExpressionGenerator();

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

src/main/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGenerator.java

+18 −23
Original line number Diff line number Diff line
@@ -29,13 +29,11 @@ 


package ca.mcscert.jtet.salgenerator;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.Expression;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridDepthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;



import java.util.List;

import java.util.Map;



/**
@@ -43,16 +41,15 @@ import java.util.Map; 
 */

public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstCheckerGenerator {



    public HierarchicalGridSALGenerator(VariableCollection variableDefinitions, Variable outputVariable)

    public HierarchicalGridSALGenerator(Variable outputVariable)

    {

        this.variableDefinitions = variableDefinitions;

        this.m_outputVariable = outputVariable;

    }



    @Override

    public void descendIntoGridFromCell(Cell cell)

    public void descendIntoGridFromCell(Expression inputCellExpression)

    {

        outputCellPrelude(cell);

        outputCellPrelude(inputCellExpression);

        m_firstCell = true;

    }
@@ -64,7 +61,7 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstC 
        m_firstCell = false;

    }



    private void outputCellPrelude(Cell cell)

    private void outputCellPrelude(Expression inputCellExpression)

    {

        m_currentlyRunning = true;

        if (m_firstCell) {
@@ -73,23 +70,23 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstC 
            result.append("ELSIF ");

        }

        m_firstCell = false;

        result.append(MatlabParser.parseMatlabCode(variableDefinitions, cell.contents()).getCheckerOutput(m_generator, BooleanVariableType.Type));

        result.append(inputCellExpression.getCheckerOutput(m_generator, BooleanVariableType.Type));

        result.append(" THEN ");

    }



    @Override

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

    public void handleLeafCell(Expression inputCellExpression, Map<Variable, Expression> outputCellsExpression)

    {

        if (m_firstOutputCell == null) {

            m_firstOutputCell = outputCells.get(m_outputVariable);

        if (m_firstOutputCellExpression == null) {

            m_firstOutputCellExpression = outputCellsExpression.get(m_outputVariable);

        }

        outputCellPrelude(cell);

        result.append(getOutputCellAsSALCode(outputCells.get(m_outputVariable)));

        outputCellPrelude(inputCellExpression);

        result.append(getOutputExpressionAsSALCode(outputCellsExpression.get(m_outputVariable)));

        result.append(" ");

    }



    @Override

    public void handleEdgeCell(Cell cell)

    public void handleEdgeCell(Expression inputCellExpression)

    {

    }
@@ -105,12 +102,12 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstC 


    private void handleEndIf() {

        result.append("ELSE ")

                .append(getOutputCellAsSALCode(m_firstOutputCell))

                .append(getOutputExpressionAsSALCode(m_firstOutputCellExpression))

                .append(" ENDIF");

    }



    private String getOutputCellAsSALCode(Cell outputCell) {

        return MatlabParser.parseMatlabCode(variableDefinitions, outputCell.contents()).getCheckerOutput(m_generator, m_outputVariable.type());

    private String getOutputExpressionAsSALCode(Expression expression) {

        return expression.getCheckerOutput(m_generator, m_outputVariable.type());

    }



    final private StringBuilder result = new StringBuilder();
@@ -118,9 +115,7 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstC 
    private boolean m_currentlyRunning = false;

    private boolean m_firstCell = true;

    private final Variable m_outputVariable;

    private Cell m_firstOutputCell;



    final private VariableCollection variableDefinitions;

    private Expression m_firstOutputCellExpression;



    final private SALExpressionGenerator m_generator = new SALExpressionGenerator();

}

src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunner.java

+1 −1
Original line number Diff line number Diff line
@@ -63,7 +63,7 @@ final public class CheckerRunner { 
        List<CheckerRunnerResult> ret = new ArrayList<CheckerRunnerResult>();



        // Get the queries

        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);

        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator();

        table.walk(queryGenerator);



        // Start Z3

src/main/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGenerator.java

+8 −13
Original line number Diff line number Diff line
@@ -29,10 +29,8 @@ 
package ca.mcscert.jtet.smtlibchecker;



import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.expression.Expression;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridBreadthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.Cell;

import org.apache.commons.lang3.StringUtils;



import java.util.ArrayDeque;
@@ -46,8 +44,7 @@ import java.util.List; 
 */

final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridBreadthFirstCheckerGenerator {



    public HierarchicalGridSMTLIBGenerator(VariableCollection variableDefinitions) {

        m_variableDefinitions = variableDefinitions;

    public HierarchicalGridSMTLIBGenerator() {

    }



    private String generateQueryPrefix() {
@@ -105,11 +102,11 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridBr 
    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

    public void descendIntoGridFromCell(Expression cellExpression) {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type));

        m_parentCellsCVC3Code.addFirst(cellExpression.getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type));

        m_currentlyRunning = true;

    }
@@ -122,14 +119,14 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridBr 
    }



    @Override

    public void handleEdgeCell(Cell inputCell) {

        handleLeafCell(inputCell);

    public void handleEdgeCell(Expression inputCellExpression) {

        handleLeafCell(inputCellExpression);

    }



    @Override

    public void handleLeafCell(Cell cell) {

    public void handleLeafCell(Expression cellExpression) {

        // First get the appropriate CVC3 code from matlab.

        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type);

        String newCellCode = cellExpression.getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type);



        // Next form the disjoint queries and add to the list.

        for(String otherCellCode : m_currentCompleteQueries) {
@@ -166,7 +163,5 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridBr 
    String m_output = "";

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



    // To fix properly.

    VariableCollection m_variableDefinitions;

    SMTLIBExpressionGenerator m_CVC3Generator = new SMTLIBExpressionGenerator();

}