Commit 53b299b7 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Move EventB's variable generator over to a single StringBuilder. 

Avoid concating several strings together in the EventB variable generator.
While a complete optimization, the number of concatenations required makes
it worth it.
parent a3858ef6

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

+45 −49
Original line number Diff line number Diff line
@@ -50,97 +50,93 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla 


    @Override

    public String GenerateVariablesDeclaration(Collection<Variable> variables) {

        String variablesRelatedXml = "";

        final StringBuilder variablesRelatedXml = new StringBuilder();



        variablesRelatedXml += generateVariablesXml(variables);

        variablesRelatedXml += generateInvariantsXml(variables);

        variablesRelatedXml += generateInitEventXml(variables);

        generateVariablesXml(variablesRelatedXml, variables);

        generateInvariantsXml(variablesRelatedXml, variables);

        generateInitEventXml(variablesRelatedXml, variables);



        return variablesRelatedXml;

        return variablesRelatedXml.toString();

    }



    private String generateVariablesXml(Collection<Variable> variables) {

    private void generateVariablesXml(StringBuilder ret, Collection<Variable> variables) {

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

        String ret = "";



        //generate all the variables one by one.

        for(Variable var : variables) {

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

            ret += var.outputName();

            ret += variableXmlPost;

            generateVariableXmlPre(ret, var.outputName());

            ret.append(var.outputName());

            ret.append(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 void generateInvariantXmlPre(StringBuilder ret, int invariantNum) {

        ret.append("<org.eventb.core.invariant name=\"Invariant")

                .append(invariantNum)

                .append("\" org.eventb.core.label=\"inv")

                .append(invariantNum)

                .append("\" 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 void generateVariableXmlPre(StringBuilder ret, String variableName) {

        ret.append("<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"")

                .append(variableName)

                .append("\" org.eventb.core.identifier=\"");

    }



    private String generateInvariantsXml(Collection<Variable> variables) {

        String ret = "";

    private void generateInvariantsXml(StringBuilder ret, Collection<Variable> variables) {

        int  invariantsNum = 1;

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



        //generate all the Invariants one by one.

        for (Variable var : variables) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.outputName();

            ret += " ∈ ";

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

            ret += invariantXmlPost;

            generateInvariantXmlPre(ret, invariantsNum);

            ret.append(var.outputName());

            ret.append(" ∈ ");

            ret.append(GenerateVariableType(var.type()));

            ret.append(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";

        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 void generateInitEventActionXmlPre(StringBuilder ret, int actionNo) {

        ret.append("<org.eventb.core.action name=\"InitAction")

                .append(actionNo)

                .append("\" org.eventb.core.assignment=\"");

    }



    private String generateInitEventActionXmlPost(int actionNo) {



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

    private void generateInitEventActionXmlPost(StringBuilder ret, int actionNo) {

        ret.append("\" org.eventb.core.label=\"act")

                .append(actionNo)

                .append("\"/>");

    }



    private String generateInitEventXml(Collection<Variable> variables) {

        String ret = "";

        ret += generateInitEventXmlPre();

        ret += generateInitEventActionsXml(variables);

        ret += generateInitEventXmlPost();



        return ret;

    private void generateInitEventXml(StringBuilder ret, Collection<Variable> variables) {

        ret.append(generateInitEventXmlPre());

        generateInitEventActionsXml(ret, variables);

        ret.append(generateInitEventXmlPost());

    }



    private String generateInitEventActionsXml(Collection<Variable> variables) {

        String ret = "";

    private void generateInitEventActionsXml(StringBuilder ret, Collection<Variable> variables) {



        //generate all the Initialisation actions one by one.

        int actionNo = 0;

        for (Variable var : variables) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.outputName();

            ret += " :∈ ";

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

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

            generateInitEventActionXmlPre(ret, actionNo);

            ret.append(var.outputName());

            ret.append(" :∈ ");

            ret.append(GenerateVariableType(var.type()));

            generateInitEventActionXmlPost(ret, actionNo);

            ret.append("\n");

        }



        return ret;

    }

}