Lead out message queue optimization to API

ftsrg · Sep 26, 2023 · 878b864 · 878b864
1 parent f981bde
commit 878b864
Show file tree

Hide file tree

Showing 8 changed files with 25 additions and 20 deletions.
diff --git a/.../gamma/composition/xsts/uppaal/transformation/Gamma2XstsUppaalTransformerSerializer.xtend b/.../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/....mit.gamma.ui/src/hu/bme/mit/gamma/ui/taskhandler/AnalysisModelTransformationHandler.java b/....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/...src/hu/bme/mit/gamma/xsts/nuxmv/transformation/Gamma2XstsNuxmvTransformerSerializer.xtend b/...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/...hu/bme/mit/gamma/xsts/promela/transformation/Gamma2XstsPromelaTransformerSerializer.xtend b/...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/...ator/src/hu/bme/mit/gamma/scenario/trace/generator/ScenarioStatechartTraceGenerator.xtend b/...ator/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/...sformation.util/src/hu/bme/mit/gamma/xsts/transformation/util/MessageQueueOptimizer.xtend b/...sformation.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/...xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/GammaToXstsTransformer.xtend b/...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/...mation/src/hu/bme/mit/gamma/xsts/transformation/api/Gamma2XstsTransformerSerializer.xtend b/...mation/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<Expression> 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)