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

Split the EventBVariablesDeclarationGenerator from EventBExpressionGenerator. 

This refactor is corresponding to split the VariablesDeclarationGenerator
interface from ExpressionGenerator interface commit.
parent cf686405

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

+2 −109
Original line number Diff line number Diff line
@@ -31,13 +31,13 @@ package ca.mcscert.jtet.eventbgenerator; 


import ca.mcscert.jtet.expression.*;

import org.apache.commons.lang3.StringUtils;

import java.util.Map;



/**

 *

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

 */

final public class EventBExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

final public class EventBExpressionGenerator implements ExpressionGenerator {

    public final static EventBExpressionGenerator Generator = new EventBExpressionGenerator();



    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {
@@ -98,25 +98,6 @@ final public class EventBExpressionGenerator implements VariablesDeclarationGene 
        throw new IllegalArgumentException("Unhandled operation: " + op);

    }



    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "ℤ";

        } else {

            throw new IllegalArgumentException("EventB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

    }



    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

        String variablesRelatedXml = "";



        variablesRelatedXml += generateVariablesXml(variableCollection);

        variablesRelatedXml += generateInvariantsXml(variableCollection);

        variablesRelatedXml += generateInitEventXml(variableCollection);



        return variablesRelatedXml;

    }



    @Override

    public String GenerateLiteralValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {
@@ -135,92 +116,4 @@ final public class EventBExpressionGenerator implements VariablesDeclarationGene 
            throw new IllegalArgumentException("Can't cast literal to that type!");

        }

    }



    private String generateVariablesXml(VariableCollection variableCollection) {

        final String variableXmlPost = "\"/>\n";

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the variables one by one.

        for(Variable var : vars.values()) {

            ret += generateVariableXmlPre(var.outputName());

            ret += var.outputName();

            ret += variableXmlPost;

        }



        return ret;

    }



    private String generateInvariantXmlPre(int invariantNum) {

        return "<org.eventb.core.invariant name=\""  + "Invariant" + invariantNum + "\" org.eventb.core.label=\""  + "inv" + invariantNum + "\" org.eventb.core.predicate=\"";

    }



    private String generateVariableXmlPre(String variableName) {

        return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\""  + variableName +"\" org.eventb.core.identifier=\"";

    }



    private String generateInvariantsXml(VariableCollection variableCollection) {

        String ret = "";

        int  invariantsNum = 1;

        final String invariantXmlPost = "\"/>\n";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Invariants one by one.

        for (Variable var : vars.values()) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.outputName();

            ret += " ∈ ";

            ret += GenerateVariableType(var.type());

            ret += invariantXmlPost;

            invariantsNum++;

        }



        return ret;

    }



    private String generateInitEventXmlPre() {

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

    }



    private String generateInitEventXmlPost() {

        return "</org.eventb.core.event>\n";

    }



    private String generateInitEventActionXmlPre(int actionNo) {



        return "<org.eventb.core.action name=\"InitAction" + actionNo  + "\" org.eventb.core.assignment=\"";

    }



    private String generateInitEventActionXmlPost(int actionNo) {



        return "\" org.eventb.core.label=\"act" + actionNo + "\"/>";

    }



    private String generateInitEventXml(VariableCollection variableCollection) {

        String ret = "";

        ret += generateInitEventXmlPre();

        ret += generateInitEventActionsXml(variableCollection);

        ret += generateInitEventXmlPost();



        return ret;

    }



    private String generateInitEventActionsXml(VariableCollection variableCollection) {

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Initialisation actions one by one.

        int actionNo = 0;

        for (Variable var : vars.values()) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.outputName();

            ret += " :∈ ";

            ret += GenerateVariableType(var.type());

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

        }



        return ret;

    }

}

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

+2 −2
Original line number Diff line number Diff line
@@ -58,8 +58,8 @@ final public class EventBTableGenerator { 
            output += machineFileCfgPreXml;



            //Step 2: Generate the Variables & Invariants Xml

            EventBExpressionGenerator eventBExpressionGenerator = new EventBExpressionGenerator();

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

            EventBVariablesDeclarationGenerator eventBVariablesDeclarationGenerator = new EventBVariablesDeclarationGenerator();

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



            //Step 3: Generate the Events Xml

            HierarchicalGridEventBGenerator hierarchicalGridEventBGenerator;

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

0 → 100644
+149 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.ca>

 *

 * Redistribution and use in source and binary forms, with or without

 * modification, are permitted provided that the following conditions are

 * met:

 *

 *     * Redistributions of source code must retain the above copyright

 *       notice, this list of conditions and the following disclaimer.

 *     * Redistributions in binary form must reproduce the above copyright

 *       notice, this list of conditions and the following disclaimer in

 *       the documentation and/or other materials provided with the distribution

 *     * Neither the name of the McMaster Centre for Software Certification nor the names

 *       of its contributors may be used to endorse or promote products derived

 *       from this software without specific prior written permission.

 *

 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"

 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE

 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE

 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE

 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR

 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF

 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS

 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN

 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)

 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

 * POSSIBILITY OF SUCH DAMAGE.

 */



package ca.mcscert.jtet.eventbgenerator;



import ca.mcscert.jtet.expression.*;



import java.util.Map;



/**

 *

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

 */

final public class EventBVariablesDeclarationGenerator implements VariablesDeclarationGenerator {

    public final static EventBVariablesDeclarationGenerator Generator = new EventBVariablesDeclarationGenerator();



    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "ℤ";

        } else {

            throw new IllegalArgumentException("EventB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

    }



    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

        String variablesRelatedXml = "";



        variablesRelatedXml += generateVariablesXml(variableCollection);

        variablesRelatedXml += generateInvariantsXml(variableCollection);

        variablesRelatedXml += generateInitEventXml(variableCollection);



        return variablesRelatedXml;

    }



    private String generateVariablesXml(VariableCollection variableCollection) {

        final String variableXmlPost = "\"/>\n";

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the variables one by one.

        for(Variable var : vars.values()) {

            ret += generateVariableXmlPre(var.outputName());

            ret += var.outputName();

            ret += variableXmlPost;

        }



        return ret;

    }



    private String generateInvariantXmlPre(int invariantNum) {

        return "<org.eventb.core.invariant name=\""  + "Invariant" + invariantNum + "\" org.eventb.core.label=\""  + "inv" + invariantNum + "\" org.eventb.core.predicate=\"";

    }



    private String generateVariableXmlPre(String variableName) {

        return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\""  + variableName +"\" org.eventb.core.identifier=\"";

    }



    private String generateInvariantsXml(VariableCollection variableCollection) {

        String ret = "";

        int  invariantsNum = 1;

        final String invariantXmlPost = "\"/>\n";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Invariants one by one.

        for (Variable var : vars.values()) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.outputName();

            ret += " ∈ ";

            ret += GenerateVariableType(var.type());

            ret += invariantXmlPost;

            invariantsNum++;

        }



        return ret;

    }



    private String generateInitEventXmlPre() {

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

    }



    private String generateInitEventXmlPost() {

        return "</org.eventb.core.event>\n";

    }



    private String generateInitEventActionXmlPre(int actionNo) {



        return "<org.eventb.core.action name=\"InitAction" + actionNo  + "\" org.eventb.core.assignment=\"";

    }



    private String generateInitEventActionXmlPost(int actionNo) {



        return "\" org.eventb.core.label=\"act" + actionNo + "\"/>";

    }



    private String generateInitEventXml(VariableCollection variableCollection) {

        String ret = "";

        ret += generateInitEventXmlPre();

        ret += generateInitEventActionsXml(variableCollection);

        ret += generateInitEventXmlPost();



        return ret;

    }



    private String generateInitEventActionsXml(VariableCollection variableCollection) {

        String ret = "";

        Map<String, Variable> vars = variableCollection.getVariables();



        //generate all the Initialisation actions one by one.

        int actionNo = 0;

        for (Variable var : vars.values()) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.outputName();

            ret += " :∈ ";

            ret += GenerateVariableType(var.type());

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

        }



        return ret;

    }

}

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

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



import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;

import ca.mcscert.jtet.eventbgenerator.EventBExpressionGenerator;

import ca.mcscert.jtet.eventbgenerator.EventBVariablesDeclarationGenerator;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.salgenerator.SALVariablesDeclarationGenerator;

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

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

                },

                {new EventBExpressionGenerator(),

                {new EventBVariablesDeclarationGenerator(),

                        "<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" +