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

Rename EventBGenerator to EventBExpressionGenerator. 

This commit is used to keep the changes history clean so that the
modification is easy to see.
parent 544ce6ad

src/main/java/ca/mcscert/jtet/expression/EventBGenerator.java→src/main/java/ca/mcscert/jtet/eventbgenerator/EventBExpressionGenerator.java

+5 −4
Original line number Diff line number Diff line
@@ -27,8 +27,9 @@ 
 * POSSIBILITY OF SUCH DAMAGE.

 */



package ca.mcscert.jtet.expression;

package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.*;

import org.apache.commons.lang3.StringUtils;

import java.util.Map;
@@ -36,7 +37,7 @@ import java.util.Map; 
 *

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

 */

final public class EventBGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

final public class EventBExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {



    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {
@@ -78,12 +79,12 @@ final public class EventBGenerator implements VariablesDeclarationGenerator, Exp 


    @Override

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

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

          return "(" + lhsExp + " " + EventBExpressionGenerator.ConvertToOutputOp(op) + " " + rhsExp + ")";

    }



    @Override

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

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

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

    }

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

+2 −3
Original line number Diff line number Diff line
@@ -28,7 +28,6 @@ 
 */

package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.EventBGenerator;

import ca.mcscert.jtet.tablularexpression.*;



import java.io.IOException;
@@ -59,8 +58,8 @@ final public class EventBTableGenerator { 
            output += machineFileCfgPreXml;



            //Step 2: Generate the Variables & Invariants Xml

            EventBGenerator m_eventBGenerator = new EventBGenerator();

            output += m_eventBGenerator.GenerateVariablesDeclaration(m_table.getInputVariables());

            EventBExpressionGenerator eventBExpressionGenerator = new EventBExpressionGenerator();

            output += eventBExpressionGenerator.GenerateVariablesDeclaration(m_table.getInputVariables());



            //Step 3: Generate the Events Xml

            HierarchicalGridEventBGenerator hierarchicalGridEventBGenerator;

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

+2 −2
Original line number Diff line number Diff line
@@ -195,7 +195,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    }



    private String convertMatlabToEventB(String outputValue, VariableType variableType) {

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

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

    }



    private String handleConditionCell(Cell cell) {
@@ -223,7 +223,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe 
    TwoDimensionalGrid m_outputGrid;

    VariableCollection m_variableDefinitions;

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

    EventBGenerator m_eventBGenerator = new EventBGenerator();

    EventBExpressionGenerator m_eventBExpressionGenerator = new EventBExpressionGenerator();

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

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

    Stack<Integer> m_oldSubGridCellIndex = new Stack<Integer>();

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

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



import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;

import ca.mcscert.jtet.eventbgenerator.EventBExpressionGenerator;

import ca.mcscert.jtet.salgenerator.SALExpressionGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;

import ca.mcscert.jtet.parsers.PVSSimpleParser;
@@ -66,7 +67,7 @@ public class GenericOperationGeneratorTest { 
                        null,

                        null

                },

                {new EventBGenerator(),

                {new EventBExpressionGenerator(),

                        "((((x ∗ 5) = (1 ÷ (− 4))) ∨ (((x &gt; (8 + 3)) ∧ (9 &lt; (x − 2))) ∨ ((x ≥ 12) ∨ ((¬ (34 ≤ (− x))) ∨ (5 &gt; 4))))) ⇒ (x ≠ 5))",

                        null,

                        null

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

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



import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;

import ca.mcscert.jtet.eventbgenerator.EventBExpressionGenerator;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.salgenerator.SALVariablesDeclarationGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;
@@ -78,7 +79,7 @@ public class GenericVariablesDeclarationGeneratorTest { 
                        "new_x_name:MyEnum;\n",

                        "x:MyEnum;\ny:MyEnum;\n"

                },

                {new EventBGenerator(),

                {new EventBExpressionGenerator(),

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

                        "<org.eventb.core.invariant name=\"Invariant1\" org.eventb.core.label=\"inv1\" org.eventb.core.predicate=\"x ∈ ℤ\"/>\n" +

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