diff --git a/plugins/core/hu.bme.mit.gamma.composition.xsts.uppaal.transformation/src/hu/bme/mit/gamma/composition/xsts/uppaal/transformation/Gamma2XstsUppaalTransformerSerializer.xtend b/plugins/core/hu.bme.mit.gamma.composition.xsts.uppaal.transformation/src/hu/bme/mit/gamma/composition/xsts/uppaal/transformation/Gamma2XstsUppaalTransformerSerializer.xtend index f2f05a9e9..fc529e576 100644 --- a/plugins/core/hu.bme.mit.gamma.composition.xsts.uppaal.transformation/src/hu/bme/mit/gamma/composition/xsts/uppaal/transformation/Gamma2XstsUppaalTransformerSerializer.xtend +++ b/plugins/core/hu.bme.mit.gamma.composition.xsts.uppaal.transformation/src/hu/bme/mit/gamma/composition/xsts/uppaal/transformation/Gamma2XstsUppaalTransformerSerializer.xtend @@ -101,7 +101,7 @@ class Gamma2XstsUppaalTransformerSerializer { val xStsTransformer = new Gamma2XstsTransformerSerializer(component, arguments, targetFolderUri, fileName, minSchedulingConstraint, maxSchedulingConstraint, - optimize, false, + optimize, false, false, transitionMerging, slicingProperties, annotatableElements, initialState, initialStateSetting) diff --git a/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/AnalysisModelTransformationHandler.java b/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/AnalysisModelTransformationHandler.java index 3d32a8751..8d82eb513 100644 --- a/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/AnalysisModelTransformationHandler.java +++ b/plugins/core/hu.bme.mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/AnalysisModelTransformationHandler.java @@ -519,7 +519,7 @@ public void execute(AnalysisModelTransformation transformation) throws IOExcepti component, reference.getArguments(), targetFolderUri, fileName, minSchedulingConstraint, maxSchedulingConstraint, - transformation.isOptimize(), true, + transformation.isOptimize(), true, true, TransitionMerging.HIERARCHICAL, transformation.getPropertyPackage(), new AnnotatablePreprocessableElements( testedComponentsForStates, testedComponentsForTransitions, diff --git a/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/Gamma2XstsNuxmvTransformerSerializer.xtend b/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/Gamma2XstsNuxmvTransformerSerializer.xtend index 8199ec150..a3d7135d8 100644 --- a/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/Gamma2XstsNuxmvTransformerSerializer.xtend +++ b/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/Gamma2XstsNuxmvTransformerSerializer.xtend @@ -103,7 +103,7 @@ class Gamma2XstsNuxmvTransformerSerializer { val xStsTransformer = new Gamma2XstsTransformerSerializer(component, arguments, targetFolderUri, fileName, minSchedulingConstraint, maxSchedulingConstraint, - optimize, true, // Optimize arrays? + optimize, true, /* Optimize arrays? */ true, /* Optimize message queues */ transitionMerging, slicingProperties, annotatableElements, initialState, initialStateSetting) diff --git a/plugins/promela/hu.bme.mit.gamma.xsts.promela.transformation/src/hu/bme/mit/gamma/xsts/promela/transformation/Gamma2XstsPromelaTransformerSerializer.xtend b/plugins/promela/hu.bme.mit.gamma.xsts.promela.transformation/src/hu/bme/mit/gamma/xsts/promela/transformation/Gamma2XstsPromelaTransformerSerializer.xtend index 0c5642eb7..c2b84daff 100644 --- a/plugins/promela/hu.bme.mit.gamma.xsts.promela.transformation/src/hu/bme/mit/gamma/xsts/promela/transformation/Gamma2XstsPromelaTransformerSerializer.xtend +++ b/plugins/promela/hu.bme.mit.gamma.xsts.promela.transformation/src/hu/bme/mit/gamma/xsts/promela/transformation/Gamma2XstsPromelaTransformerSerializer.xtend @@ -99,7 +99,7 @@ class Gamma2XstsPromelaTransformerSerializer { val xStsTransformer = new Gamma2XstsTransformerSerializer(component, arguments, targetFolderUri, fileName, minSchedulingConstraint, maxSchedulingConstraint, - optimize, true, // Optimize arrays? + optimize, true, /* Optimize arrays? */ false, /* Optimize message queues? */ transitionMerging, slicingProperties, annotatableElements, initialState, initialStateSetting) diff --git a/plugins/scenario/hu.bme.mit.gamma.scenario.trace.generator/src/hu/bme/mit/gamma/scenario/trace/generator/ScenarioStatechartTraceGenerator.xtend b/plugins/scenario/hu.bme.mit.gamma.scenario.trace.generator/src/hu/bme/mit/gamma/scenario/trace/generator/ScenarioStatechartTraceGenerator.xtend index de41fef83..55ff279c0 100644 --- a/plugins/scenario/hu.bme.mit.gamma.scenario.trace.generator/src/hu/bme/mit/gamma/scenario/trace/generator/ScenarioStatechartTraceGenerator.xtend +++ b/plugins/scenario/hu.bme.mit.gamma.scenario.trace.generator/src/hu/bme/mit/gamma/scenario/trace/generator/ScenarioStatechartTraceGenerator.xtend @@ -87,7 +87,7 @@ class ScenarioStatechartTraceGenerator { val name = statechart.name val compInstanceRef = new ComponentInstanceReferences(newArrayList,newArrayList) val transformator = new Gamma2XstsTransformerSerializer(statechart, arguments, absoluteParentFolder, name, schedulingConstraint, schedulingConstraint, - true, false, TransitionMerging.HIERARCHICAL, null, + true, false, false, TransitionMerging.HIERARCHICAL, null, new AnnotatablePreprocessableElements(null, compInstanceRef, null, null, null, InteractionCoverageCriterion.EVERY_INTERACTION, InteractionCoverageCriterion.EVERY_INTERACTION, null, DataflowCoverageCriterion.ALL_USE, null, DataflowCoverageCriterion.ALL_USE), null, null) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/util/MessageQueueOptimizer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/util/MessageQueueOptimizer.xtend index eab5ddd07..51131fd7c 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/util/MessageQueueOptimizer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/util/MessageQueueOptimizer.xtend @@ -211,7 +211,6 @@ class MessageQueueOptimizer { val addAction = flattenedQueueVariable.createAssignmentAction(clonedRhs) addAction.replace(action) - return } else { // q[size] := x; val sizeVariable = index.declaration @@ -230,8 +229,8 @@ class MessageQueueOptimizer { val newAddAction = ifActions.weave newAddAction.replace(action) - return } + return } } throw new IllegalArgumentException("Not known action: " + action) @@ -304,8 +303,8 @@ class MessageQueueOptimizer { val notEmptyAssumption = notEmptyExpression.createAssumeAction action.appendToAction(notEmptyAssumption) - return } + return } throw new IllegalArgumentException("Not known action: " + action) } diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/GammaToXstsTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/GammaToXstsTransformer.xtend index 80678d959..a98f6497b 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/GammaToXstsTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/GammaToXstsTransformer.xtend @@ -65,7 +65,7 @@ class GammaToXstsTransformer { protected final InitialStateSetting initialStateSetting protected final boolean optimize protected final boolean optimizeArrays - protected final boolean optimizeMessageQueues = false + protected final boolean optimizeMessageQueues // Auxiliary objects protected final extension GammaEcoreUtil ecoreUtil = GammaEcoreUtil.INSTANCE protected final extension ActionSerializer actionSerializer = ActionSerializer.INSTANCE @@ -82,26 +82,28 @@ class GammaToXstsTransformer { protected final Logger logger = Logger.getLogger("GammaLogger") new() { - this(null, true, true, false, TransitionMerging.HIERARCHICAL) + this(null, true, true, false, false, TransitionMerging.HIERARCHICAL) } new(Integer schedulingConstraint, boolean transformOrthogonalActions, - boolean optimize, boolean optimizeArrays, TransitionMerging transitionMerging) { + boolean optimize, boolean optimizeArrays, boolean optimizeMessageQueues, + TransitionMerging transitionMerging) { this(schedulingConstraint, transformOrthogonalActions, - optimize, optimizeArrays, transitionMerging, - null, null) + optimize, optimizeArrays, optimizeMessageQueues, + transitionMerging, null, null) } new(Integer schedulingConstraint, boolean transformOrthogonalActions, - boolean optimize, boolean optimizeArrays, TransitionMerging transitionMerging, + boolean optimize, boolean optimizeArrays, boolean optimizeMessageQueues, + TransitionMerging transitionMerging, PropertyPackage initialState, InitialStateSetting initialStateSetting) { this(schedulingConstraint, schedulingConstraint, - transformOrthogonalActions, optimize, optimizeArrays, transitionMerging, - initialState, initialStateSetting) + transformOrthogonalActions, optimize, optimizeArrays, optimizeMessageQueues, + transitionMerging, initialState, initialStateSetting) } new(Integer minSchedulingConstraint, Integer maxSchedulingConstraint, - boolean transformOrthogonalActions, boolean optimize, boolean optimizeArrays, + boolean transformOrthogonalActions, boolean optimize, boolean optimizeArrays, boolean optimizeMessageQueues, TransitionMerging transitionMerging, PropertyPackage initialState, InitialStateSetting initialStateSetting) { this.gammaToLowlevelTransformer = new GammaToLowlevelTransformer @@ -113,6 +115,7 @@ class GammaToXstsTransformer { this.initialStateSetting = initialStateSetting this.optimize = optimize this.optimizeArrays = optimizeArrays + this.optimizeMessageQueues = optimizeMessageQueues } def preprocessAndExecuteAndSerialize(Package _package, diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/api/Gamma2XstsTransformerSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/api/Gamma2XstsTransformerSerializer.xtend index 61ba24f0b..2dab1c5d2 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/api/Gamma2XstsTransformerSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/api/Gamma2XstsTransformerSerializer.xtend @@ -42,6 +42,7 @@ class Gamma2XstsTransformerSerializer { // Configuration protected final boolean optimize protected final boolean optimizeArray + protected final boolean optimizeMessageQueues protected final TransitionMerging transitionMerging // Slicing protected final PropertyPackage slicingProperties @@ -70,7 +71,7 @@ class Gamma2XstsTransformerSerializer { String targetFolderUri, String fileName, Integer schedulingConstraint) { this(component, arguments, targetFolderUri, fileName, schedulingConstraint, schedulingConstraint, - true, false, TransitionMerging.HIERARCHICAL, + true, false, false, TransitionMerging.HIERARCHICAL, null, new AnnotatablePreprocessableElements(null, null, null, null, null, InteractionCoverageCriterion.EVERY_INTERACTION, InteractionCoverageCriterion.EVERY_INTERACTION, null, DataflowCoverageCriterion.ALL_USE, @@ -81,7 +82,7 @@ class Gamma2XstsTransformerSerializer { new(Component component, List arguments, String targetFolderUri, String fileName, Integer minSchedulingConstraint, Integer maxSchedulingConstraint, - boolean optimize, boolean optimizeArray, + boolean optimize, boolean optimizeArray, boolean optimizeMessageQueues, TransitionMerging transitionMerging, PropertyPackage slicingProperties, AnnotatablePreprocessableElements annotatableElements, @@ -95,6 +96,7 @@ class Gamma2XstsTransformerSerializer { // this.optimize = optimize this.optimizeArray = optimizeArray + this.optimizeMessageQueues = optimizeMessageQueues this.transitionMerging = transitionMerging // this.slicingProperties = slicingProperties @@ -119,7 +121,8 @@ class Gamma2XstsTransformerSerializer { targetFolderUri, fileName) slicerAnnotatorAndPropertyGenerator.execute val gammaToXSTSTransformer = new GammaToXstsTransformer( - minSchedulingConstraint, maxSchedulingConstraint, true, true, optimizeArray, + minSchedulingConstraint, maxSchedulingConstraint, + true, true, optimizeArray, optimizeMessageQueues, transitionMerging, initialState, initialStateSetting) // Normal transformation val xSts = gammaToXSTSTransformer.execute(newGammaPackage)