Commit 224b9eb0 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Make HierarchicialGridEventBGenerator use StringBuilder in loops.

When preforming a loop with direct string concatenations, use a StringBuilder
instead.  Note function calls inside those loops may still use concatenations.
The whole class is not converted to avoid huge changes.
parent 53b299b7
Loading
Loading
Loading
Loading
+27 −15
Original line number Diff line number Diff line
@@ -52,12 +52,8 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe
        return "<org.eventb.core.guard name=\"Guard" + guardNo + "\" org.eventb.core.label=\"grd" + + guardNo + "\" org.eventb.core.predicate=\"" + guard +"\"/>\n";
    }

     private String generateOneEventActionXml(int actionNo, String variable, String value) {
        return  "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + variable +  " ≔ " + value + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";
    }

    private String generateEventActionsXml() {
        String ret = "";
        final StringBuilder ret = new StringBuilder();
        String outputVariableName;
        String outputValue;
        int actionNo = 0;
@@ -68,18 +64,34 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe
            if (collectedOutputValues.size() == 1) { // leaf action
                outputValue = collectedOutputValues.get(0);
                outputVariableName = outputVariable.name();
                ret += generateOneEventActionXml(actionNo, outputVariableName, outputValue);
                ret.append("<org.eventb.core.action name=\"Action")
                        .append(actionNo + 1)
                        .append("\" org.eventb.core.assignment=\"")
                        .append(outputVariableName)
                        .append(" ≔ ")
                        .append(outputValue)
                        .append("\" org.eventb.core.label=\"act")
                        .append(actionNo + 1)
                        .append("\"/>\n");
            } else {
                outputVariableName = outputVariable.name();
                String columnVector = "{";
                columnVector += StringUtils.join(collectedOutputValues, ',');
                columnVector += "}";
                ret += "<org.eventb.core.action name=\"Action" + (actionNo + 1) + "\" org.eventb.core.assignment=\"" + outputVariableName + " :∈ " + columnVector + "\" org.eventb.core.label=\"act" + (actionNo + 1) + "\"/>\n";
                ret.append("<org.eventb.core.action name=\"Action")
                        .append(actionNo + 1)
                        .append("\" org.eventb.core.assignment=\"")
                        .append(outputVariableName)
                        .append(" :∈ ")
                        .append(columnVector)
                        .append("\" org.eventb.core.label=\"act")
                        .append(actionNo + 1)
                        .append("\"/>\n");
            }
            actionNo++;
        }

        return ret;
        return ret.toString();
    }

    private String getEventName(){
@@ -107,26 +119,26 @@ final public class HierarchicalGridEventBGenerator implements HierarchicalGridDe

    private String generateEventXml() {
        int guardNo = 1;
        String ret = "";
        final StringBuilder ret = new StringBuilder();
        final String eventXmlPost = "</org.eventb.core.event>\n";

        ret += generateEventLabelXml();
        ret.append(generateEventLabelXml());

        for (String parentCellContent: m_eventBGuards){
            ret += generateEventGuardXml(guardNo++, parentCellContent);
            ret.append(generateEventGuardXml(guardNo++, parentCellContent));
        }

        ret += generateEventActionsXml();
        ret.append(generateEventActionsXml());

        if (isRefineRelationNecessary()) {
            ret += generateEventRefineRelationXml();
            ret.append(generateEventRefineRelationXml());
        }

        ret += eventXmlPost;
        ret.append(eventXmlPost);

        m_collectedOutputValues.clear();

        return ret;
        return ret.toString();
    }

    public void generateEventNo() {