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

Move VariableDeclarationGenerator to use a Collection instead of VariableCollection. 

By making the interface of VariableDeclarationGenerator use VariableCollection,
it becomes very hard to figure out of a particular language needs all variables
(both input and output) generated.  This makes testing all these classes less
practical (the point of the interface).  By moving this logic out of a
generator, higher level logic for the language can decide how to use the
generator, without impacting the tests.
parent e6d518dd

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

+5 −5
Original line number Diff line number Diff line
@@ -30,7 +30,8 @@ 
package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.*;

import java.util.Map;



import java.util.Collection;



/**

 *
@@ -41,12 +42,11 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara 
    public final static CVC3VariablesDeclarationGenerator Generator = new CVC3VariablesDeclarationGenerator();



    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

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

    public String GenerateVariablesDeclaration(Collection<Variable> variables) {

        StringBuilder ret = new StringBuilder();



        // First generate all the variables.

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

        for(Variable var : variables) {

            ret.append(var.outputName())

               .append(":")

               .append(GenerateVariableType(var.type()))
@@ -54,7 +54,7 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara 
        }



        // Then generate the variable predicates.  This ensures any dependent variables are declared.

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

        for(Variable var : variables) {

            if (var.type().subtypePredicate() != null) {

                ret.append("ASSERT ")

                   .append(var.type().subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanVariableType.Type))

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

+1 −1
Original line number Diff line number Diff line
@@ -59,7 +59,7 @@ final public class EventBTableGenerator { 


            //Step 2: Generate the Variables & Invariants Xml

            EventBVariablesDeclarationGenerator eventBVariablesDeclarationGenerator = new EventBVariablesDeclarationGenerator();

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

            output += eventBVariablesDeclarationGenerator.GenerateVariablesDeclaration(m_table.getVariables().getAllVariablesList());



            //Step 3: Generate the Events Xml

            HierarchicalGridEventBGenerator hierarchicalGridEventBGenerator;

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

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


import ca.mcscert.jtet.expression.*;



import java.util.Map;

import java.util.Collection;



/**

 *
@@ -49,23 +49,22 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla 
    }



    @Override

    public String GenerateVariablesDeclaration(VariableCollection variableCollection) {

    public String GenerateVariablesDeclaration(Collection<Variable> variables) {

        String variablesRelatedXml = "";



        variablesRelatedXml += generateVariablesXml(variableCollection);

        variablesRelatedXml += generateInvariantsXml(variableCollection);

        variablesRelatedXml += generateInitEventXml(variableCollection);

        variablesRelatedXml += generateVariablesXml(variables);

        variablesRelatedXml += generateInvariantsXml(variables);

        variablesRelatedXml += generateInitEventXml(variables);



        return variablesRelatedXml;

    }



    private String generateVariablesXml(VariableCollection variableCollection) {

    private String generateVariablesXml(Collection<Variable> variables) {

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

        String ret = "";

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



        //generate all the variables one by one.

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

        for(Variable var : variables) {

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

            ret += var.outputName();

            ret += variableXmlPost;
@@ -82,14 +81,13 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla 
        return "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\""  + variableName +"\" org.eventb.core.identifier=\"";

    }



    private String generateInvariantsXml(VariableCollection variableCollection) {

    private String generateInvariantsXml(Collection<Variable> variables) {

        String ret = "";

        int  invariantsNum = 1;

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

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



        //generate all the Invariants one by one.

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

        for (Variable var : variables) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.outputName();

            ret += " ∈ ";
@@ -119,22 +117,21 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla 
        return "\" org.eventb.core.label=\"act" + actionNo + "\"/>";

    }



    private String generateInitEventXml(VariableCollection variableCollection) {

    private String generateInitEventXml(Collection<Variable> variables) {

        String ret = "";

        ret += generateInitEventXmlPre();

        ret += generateInitEventActionsXml(variableCollection);

        ret += generateInitEventActionsXml(variables);

        ret += generateInitEventXmlPost();



        return ret;

    }



    private String generateInitEventActionsXml(VariableCollection variableCollection) {

    private String generateInitEventActionsXml(Collection<Variable> variables) {

        String ret = "";

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



        //generate all the Initialisation actions one by one.

        int actionNo = 0;

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

        for (Variable var : variables) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.outputName();

src/main/java/ca/mcscert/jtet/expression/VariableCollection.java

+30 −0
Original line number Diff line number Diff line
@@ -133,6 +133,36 @@ final public class VariableCollection { 
        return Collections.unmodifiableMap(variables);

    }



    /**

     * Returns a collection containing only input the variables.

     * <p>

     * This ignores all the enumeration constants present.

     * @return A collection of input variables.

     */

    public Collection<Variable> getInputVariablesList() {

        return getInputVariables().values();

    }



    /**

     * Returns a collection containing only output the variables.

     * <p>

     * This ignores all the enumeration constants present.

     * @return A collection of output variables.

     */

    public Collection<Variable> getOutputVariablesList() {

        return getOutputVariables().values();

    }



    /**

     * Returns a collection containing all the variables.

     * <p>

     * This combines the input and output variables, ignoring all the enumeration constants present.

     * @return A collection of output variables.

     */

    public Collection<Variable> getAllVariablesList() {

        return getAllVariables().values();

    }



    private final Map<String,Variable> m_inputVariables = new LinkedHashMap<String, Variable>();

    private final Map<String,Variable> m_outputVariables = new LinkedHashMap<String, Variable>();

    private final Map<String,Variable> m_variablesAndEnumeratedValues = new HashMap<String, Variable>();

src/main/java/ca/mcscert/jtet/expression/VariablesDeclarationGenerator.java

+3 −1
Original line number Diff line number Diff line
@@ -28,6 +28,8 @@ 
 */

package ca.mcscert.jtet.expression;



import java.util.Collection;



/**

 * Generates variable declarations for a language.

 * <p>
@@ -46,5 +48,5 @@ public interface VariablesDeclarationGenerator { 
     * @param variables  The variables to generate declarations for.

     * @return           The generated variable declaration string.

     */

    public String GenerateVariablesDeclaration(VariableCollection variables);

    public String GenerateVariablesDeclaration(Collection<Variable> variables);

}