Commit 88d1e624 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Move EventB event action generation to use a single helper function. 

Moving from the previous function, move the single event generation work to
a single function, reducing duplication.  Also move some other duplicated
lines to single places, reuse common variables, and start actionNo at 1,
avoiding an unnecessary addition on each loop iteration.

This was just a cleanup, building on the previous commit.
parent 224b9eb0

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

+22 −25
Original line number Diff line number Diff line
@@ -52,41 +52,38 @@ 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 void generateOneEventActionXml(StringBuilder ret, int actionNo, String outputVariableName, String outputValue, String assignmentOperator) {

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

                .append(actionNo)

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

                .append(outputVariableName)

                .append(" ")

                .append(assignmentOperator)

                .append(" ")

                .append(outputValue)

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

                .append(actionNo)

                .append("\"/>\n");

    }



    private String generateEventActionsXml() {

        final StringBuilder ret = new StringBuilder();

        String outputVariableName;

        String outputValue;

        int actionNo = 0;

        int actionNo = 1;



        for (Map.Entry<Variable, List<String>> variableOutputs : m_collectedOutputValues.entrySet()) {

            List<String> collectedOutputValues = variableOutputs.getValue();

            Variable outputVariable = variableOutputs.getKey();

            if (collectedOutputValues.size() == 1) { // leaf action

                outputValue = collectedOutputValues.get(0);

            outputVariableName = outputVariable.name();

                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");

            if (collectedOutputValues.size() == 1) {

                outputValue = collectedOutputValues.get(0);

                generateOneEventActionXml(ret, actionNo, outputVariableName, outputValue, "≔");

            } else {

                outputVariableName = outputVariable.name();

                String columnVector = "{";

                columnVector += StringUtils.join(collectedOutputValues, ',');

                columnVector += "}";

                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");

                outputValue = "{";

                outputValue += StringUtils.join(collectedOutputValues, ',');

                outputValue += "}";

                generateOneEventActionXml(ret, actionNo, outputVariableName, outputValue, ":∈");

            }

            actionNo++;

        }