From b4d44b4c8002e84fb593c37fba832b5746931106 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 29 Apr 2025 13:22:26 +0200 Subject: [PATCH 01/27] First version of the coordination-automata --- .../language/StatechartLanguage.xtext | 65 +++++++++++++++---- .../StatechartLanguageScopeProvider.java | 17 ++++- .../StatechartLanguageValidator.java | 2 +- .../model/statechart.ecore | 32 ++++++++- .../model/statechart.genmodel | 19 +++++- .../StatechartModelDerivedFeatures.java | 12 ++++ .../util/StatechartModelValidator.java | 5 ++ 7 files changed, 133 insertions(+), 19 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext index fc7ef1cdf..dc76f3a1f 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext @@ -436,7 +436,7 @@ DeepHistoryState returns DeepHistoryState: Component returns InterfaceModel::Component: SynchronousComponent | - AsynchronousComponent | + AsynchronousComponent | CoordinationStatechartDefinition ; @@ -749,20 +749,59 @@ CoordinationStatechartDefinition returns CoordinationStatechartDefinition: annotations+=StatechartContractAnnotation )* ) - 'statechart' name=ID + 'coordination-statechart' name=ID ('(' ((parameterDeclarations+=ParameterDeclaration)(',' parameterDeclarations+=ParameterDeclaration)*)? ')')? - ('[' ((ports+=Port)((',')? ports+=Port)*)? ']')? '{' - ( - variableDeclarations+=VariableDeclaration | - timeoutDeclarations+=TimeoutDeclaration | - ('invariant' invariants+=Expression) - )* - ( - regions+=Region | - transitions+=Transition - )* - functionDeclarations+=FunctionDeclaration* + ('[' ((ports+=Port)((',')? ports+=Port)*)? ']')? + 'composition' '{' + ( + components+=ComponentInstance | + portBindings+=PortBinding | + channels+=Channel + )* '}' + 'coordination' '{' + ( + variableDeclarations+=VariableDeclaration | + timeoutDeclarations+=TimeoutDeclaration | + ('invariant' invariants+=Expression) + )* + ( + regions+=Region | + coordinationTransitions+=CoordinationTransition + )* + functionDeclarations+=FunctionDeclaration* + '}' +; + +AbstractCoordinationReferenceExpression returns AbstractCoordinationReferenceExpression: + ComponentCoordinationReferenceExpression + | SequentialCoordinationReferenceExpression + | UnorderedCoordinationReferenceExpression +; + +ComponentCoordinationReferenceExpression returns ComponentCoordinationReferenceExpression: + instance=ComponentInstanceReferenceExpression +; + +SequentialCoordinationReferenceExpression returns SequentialCoordinationReferenceExpression: + 'seq' '{' instances+=ComponentInstanceReferenceExpression((',') instances+=ComponentInstanceReferenceExpression)* '}' | instances+=ComponentInstanceReferenceExpression +; + +UnorderedCoordinationReferenceExpression returns UnorderedCoordinationReferenceExpression: + 'unord' '{' instances+=ComponentInstanceReferenceExpression ((',') instances+=ComponentInstanceReferenceExpression)* '}' +; + +CoordinationTransition returns CoordinationTransition: + + (annotations+=TransitionAnnotation)* + 'transition' ('(' priority=INTEGER ')')? + 'from' sourceState=[StateNode] 'to' targetState=[StateNode] + + ('when' trigger=Trigger)? + ('[' guard=Expression ']')? + ('execute' coordinatedComponent=AbstractCoordinationReferenceExpression)? + ('/' ( => effects+=Action)* )? + ; // \ No newline at end of file diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java index c207aa831..98c94139d 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java @@ -74,6 +74,7 @@ import hu.bme.mit.gamma.statechart.phase.PhaseModelPackage; import hu.bme.mit.gamma.statechart.statechart.AnyPortEventReference; import hu.bme.mit.gamma.statechart.statechart.CompositeElement; +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.PortEventReference; import hu.bme.mit.gamma.statechart.statechart.RaiseEventAction; import hu.bme.mit.gamma.statechart.statechart.Region; @@ -367,13 +368,27 @@ public IScope getScope(final EObject context, final EReference reference) { } return scope; } +// if (ecoreUtil.hasContainerOfType(context, CoordinationStatechartDefinition.class)) { +// CoordinationStatechartDefinition parent = ecoreUtil.getSelfOrContainerOfType(context, CoordinationStatechartDefinition.class); +// ComponentInstance component = parent.getCoordinatedComponent(); +// if (component instanceof AsynchronousComponentInstance) { +// return handleTypeDeclarationAndComponentInstanceElementReferences(context, reference, null, ((AsynchronousComponentInstance)component).getType()); +// } +// if (component instanceof SynchronousComponentInstance) { +// return handleTypeDeclarationAndComponentInstanceElementReferences(context, reference, null, ((SynchronousComponentInstance)component).getType()); +// } +// return null; +// } + // } catch (NullPointerException e) { // Nullptr exception is thrown if the scope turns out to be empty // This can be due to modeling error of the user, e.g., there are no in events on the specified ports return super.getScope(context, reference); } catch (Exception e) { e.printStackTrace(); - } + } + System.out.println(context); + System.out.println(reference); return super.getScope(context, reference); } diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/validation/StatechartLanguageValidator.java b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/validation/StatechartLanguageValidator.java index 8a198b22f..62a7da0ce 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/validation/StatechartLanguageValidator.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/validation/StatechartLanguageValidator.java @@ -1,5 +1,5 @@ /******************************************************************************** - * Copyright (c) 2018-2024 Contributors to the Gamma project + * Copyright (c) 2018-2025 Contributors to the Gamma project * * All rights reserved. This program and the accompanying materials * are made available under the terms of the Eclipse Public License v1.0 diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore index d57006310..d61b25f58 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore @@ -164,6 +164,34 @@ - - + + + + + + + + + + + + + + + + + diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel index c0cbf519d..652791d07 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel @@ -397,7 +397,22 @@ - - + + + + + + + + + + + + + + + + + diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java index 8d68bebe1..48fa8b2f1 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java @@ -111,6 +111,7 @@ import hu.bme.mit.gamma.statechart.statechart.ChoiceState; import hu.bme.mit.gamma.statechart.statechart.ClockTickReference; import hu.bme.mit.gamma.statechart.statechart.CompositeElement; +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.DeepHistoryState; import hu.bme.mit.gamma.statechart.statechart.EntryState; import hu.bme.mit.gamma.statechart.statechart.ForkState; @@ -2299,6 +2300,11 @@ public static List getNonTrappingOutgoingTransitions(StateNode node) public static List getOutgoingTransitions(StateNode node) { StatechartDefinition statechart = getContainingStatechart(node); + if (statechart instanceof CoordinationStatechartDefinition) { + // TODO CoordinationStatechart Validation + return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream().filter(it -> it.getSourceState() == node) + .collect(Collectors.toList()); + } return statechart.getTransitions().stream().filter(it -> it.getSourceState() == node) .collect(Collectors.toList()); } @@ -2346,6 +2352,12 @@ public static List getOutgoingTransitionsUntilState(StateNode node) public static List getIncomingTransitions(StateNode node) { StatechartDefinition statechart = getContainingStatechart(node); + if (statechart instanceof CoordinationStatechartDefinition) { + // TODO CoordinationStatechart Validation + return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream().filter(it -> it.getTargetState() == node) + .collect(Collectors.toList()); + } + return statechart.getTransitions().stream().filter(it -> it.getTargetState() == node) .collect(Collectors.toList()); } diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java index 946fded5f..1b2c98697 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java @@ -107,6 +107,7 @@ import hu.bme.mit.gamma.statechart.statechart.ChoiceState; import hu.bme.mit.gamma.statechart.statechart.ClockTickReference; import hu.bme.mit.gamma.statechart.statechart.ComplexTrigger; +import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition; import hu.bme.mit.gamma.statechart.statechart.EntryState; import hu.bme.mit.gamma.statechart.statechart.ForkState; import hu.bme.mit.gamma.statechart.statechart.InitialState; @@ -706,6 +707,10 @@ public Collection checkElseTransitionPriority(Transitio public Collection checkTransitionTriggers(Transition transition) { Collection validationResultMessages = new ArrayList(); + if (transition instanceof CoordinationTransition) { + // TODO + return validationResultMessages; + } if (!StatechartModelDerivedFeatures.needsTrigger(transition)) { return validationResultMessages; } From b5cd716ae320ecaa7364ae5284f5bb42268b8b0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Mon, 12 May 2025 19:33:21 +0200 Subject: [PATCH 02/27] Simplified coordination automata --- .../language/StatechartLanguage.xtext | 54 +++++++++++++++---- .../model/statechart.ecore | 30 +++++------ 2 files changed, 57 insertions(+), 27 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext index dc76f3a1f..d7566e0fd 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext @@ -437,7 +437,8 @@ DeepHistoryState returns DeepHistoryState: Component returns InterfaceModel::Component: SynchronousComponent | AsynchronousComponent | - CoordinationStatechartDefinition + SynchronousCoordinationStatechartDefinition | + AsynchronousCoordinationStatechartDefinition ; SynchronousComponent returns CompositeModel::SynchronousComponent: @@ -738,7 +739,7 @@ ComponentInstanceReflectiveElementReferenceExpression returns CompositeModel::Co // -CoordinationStatechartDefinition returns CoordinationStatechartDefinition: +SynchronousCoordinationStatechartDefinition returns SynchronousCoordinationStatechartDefinition: '@Coordination' ( ('@RegionSchedule' '=' schedulingOrder=SchedulingOrder)? & @@ -752,14 +753,14 @@ CoordinationStatechartDefinition returns CoordinationStatechartDefinition: 'coordination-statechart' name=ID ('(' ((parameterDeclarations+=ParameterDeclaration)(',' parameterDeclarations+=ParameterDeclaration)*)? ')')? ('[' ((ports+=Port)((',')? ports+=Port)*)? ']')? - 'composition' '{' + '{' ( - components+=ComponentInstance | + components+=SynchronousComponentInstance | portBindings+=PortBinding | channels+=Channel )* '}' - 'coordination' '{' + '<' ( variableDeclarations+=VariableDeclaration | timeoutDeclarations+=TimeoutDeclaration | @@ -770,19 +771,50 @@ CoordinationStatechartDefinition returns CoordinationStatechartDefinition: coordinationTransitions+=CoordinationTransition )* functionDeclarations+=FunctionDeclaration* + '>' +; + +AsynchronousCoordinationStatechartDefinition returns AsynchronousCoordinationStatechartDefinition: + '@Coordination' + '@Asynchronous' + ( + ('@RegionSchedule' '=' schedulingOrder=SchedulingOrder)? & + ('@OrthogonalRegionSchedule' '=' orthogonalRegionSchedulingOrder=OrthogonalRegionSchedulingOrder)? & + ('@TransitionPriority' '=' transitionPriority=TransitionPriority)? & + ('@GuardEvaluation' '=' guardEvaluation=GuardEvaluation)? & + ( annotations+=ComponentAnnotation | + annotations+=StatechartContractAnnotation + )* + ) + 'coordination-statechart' name=ID + ('(' ((parameterDeclarations+=ParameterDeclaration)(',' parameterDeclarations+=ParameterDeclaration)*)? ')')? + ('[' ((ports+=Port)((',')? ports+=Port)*)? ']')? + '{' + ( + components+=AsynchronousComponentInstance | + portBindings+=PortBinding | + channels+=Channel + )* '}' + '<' + ( + variableDeclarations+=VariableDeclaration | + timeoutDeclarations+=TimeoutDeclaration | + ('invariant' invariants+=Expression) + )* + ( + regions+=Region | + coordinationTransitions+=CoordinationTransition + )* + functionDeclarations+=FunctionDeclaration* + '>' ; AbstractCoordinationReferenceExpression returns AbstractCoordinationReferenceExpression: - ComponentCoordinationReferenceExpression - | SequentialCoordinationReferenceExpression + SequentialCoordinationReferenceExpression | UnorderedCoordinationReferenceExpression ; -ComponentCoordinationReferenceExpression returns ComponentCoordinationReferenceExpression: - instance=ComponentInstanceReferenceExpression -; - SequentialCoordinationReferenceExpression returns SequentialCoordinationReferenceExpression: 'seq' '{' instances+=ComponentInstanceReferenceExpression((',') instances+=ComponentInstanceReferenceExpression)* '}' | instances+=ComponentInstanceReferenceExpression ; diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore index d61b25f58..5aee53314 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore @@ -165,33 +165,31 @@ eType="#//TimeoutDeclaration"/> - + + + + + + - - - - + abstract="true" eSuperTypes="../../hu.bme.mit.gamma.expression.model/model/expression.ecore#//ReferenceExpression"> + - - + eSuperTypes="#//AbstractCoordinationReferenceExpression"/> From 379b053eb695cba52df72ce5950d84290a3a26e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 17 Jun 2025 16:30:29 +0200 Subject: [PATCH 03/27] Coordination automata transformation WIP --- .../StatechartModelDerivedFeatures.java | 14 ++ .../util/reducer/SystemReducer.xtend | 7 +- .../GammaToLowlevelTransformer.xtend | 5 + .../StatechartToLowlevelTransformer.xtend | 184 ++++++++++++++++++ .../transformation/ComponentTransformer.xtend | 175 +++++++++++++++++ 5 files changed, 384 insertions(+), 1 deletion(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java index 48fa8b2f1..e8f90df4c 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java @@ -106,6 +106,7 @@ import hu.bme.mit.gamma.statechart.phase.MissionPhaseAnnotation; import hu.bme.mit.gamma.statechart.phase.MissionPhaseStateAnnotation; import hu.bme.mit.gamma.statechart.statechart.AnyPortEventReference; +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.AsynchronousStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.BinaryTrigger; import hu.bme.mit.gamma.statechart.statechart.ChoiceState; @@ -131,6 +132,7 @@ import hu.bme.mit.gamma.statechart.statechart.StateNode; import hu.bme.mit.gamma.statechart.statechart.StatechartAnnotation; import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition; +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.SynchronousStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.TimeoutDeclaration; import hu.bme.mit.gamma.statechart.statechart.TimeoutEventReference; @@ -2146,6 +2148,12 @@ public static List getDerivedComponents(CompositeCo if (composite instanceof AbstractAsynchronousCompositeComponent asynchronousCompositeComponent) { return asynchronousCompositeComponent.getComponents(); } + if (composite instanceof SynchronousCoordinationStatechartDefinition synchronousCoordinationStatechart) { + return synchronousCoordinationStatechart.getComponents(); + } + if (composite instanceof AsynchronousCoordinationStatechartDefinition asynchronousCoordinationStatechart) { + return asynchronousCoordinationStatechart.getComponents(); + } throw new IllegalArgumentException("Not known type: " + composite); } @@ -2366,6 +2374,12 @@ public static List getAllIncomingTransitions(StateNode node) { List allStateNodes = ecoreUtil .getSelfAndAllContentsOfType(node, StateNode.class); StatechartDefinition statechart = getContainingStatechart(node); + if (statechart instanceof CoordinationStatechartDefinition) { + // TODO CoordinationStatechart Validation + return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream() + .filter(it -> allStateNodes.contains(it.getTargetState())) + .collect(Collectors.toList()); + } return statechart.getTransitions().stream() .filter(it -> allStateNodes.contains(it.getTargetState())) .collect(Collectors.toList()); diff --git a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend index 7e90b6ba7..ac2192f16 100644 --- a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend +++ b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend @@ -48,6 +48,7 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import static extension hu.bme.mit.gamma.action.derivedfeatures.ActionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition class SystemReducer implements Reducer { @@ -101,7 +102,8 @@ class SystemReducer implements Reducer { } // Statechart optimizing for (statechart : statecharts) { - if (statechart.regions.empty || !simpleInstancesMatcher.hasMatch(null, statechart)) { + // TODO note: a coordination automaton is not a simple instance we have to handle this somewhere! + if ((statechart.regions.empty || !simpleInstancesMatcher.hasMatch(null, statechart)) && !(statechart instanceof CoordinationStatechartDefinition)) { statechart.regions.clear statechart.variableDeclarations.clear statechart.timeoutDeclarations.clear @@ -172,12 +174,15 @@ class SystemReducer implements Reducer { } private def void removeUnnecessaryStateNodes(Region region) { + info("Removing states of region " + region.name + " of " + + region.containingStatechart.name) val consideredStateNodes = region.stateNodes.reject(EntryState).toSet // To avoid concurrent mod exception for (stateNode : consideredStateNodes) { if (stateNode.allIncomingTransitions.empty) { for (outgoingTransitions : stateNode.outgoingTransitions) { outgoingTransitions.removeTransition } + info("|- Removing state " + stateNode.name) stateNode.remove } } diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend index 6c3303bc1..b812cfdc2 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend @@ -17,6 +17,7 @@ import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition class GammaToLowlevelTransformer { @@ -54,6 +55,10 @@ class GammaToLowlevelTransformer { return statechart.execute } + def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition transform(SynchronousCoordinationStatechartDefinition statechart) { + return statechart.execute + } + def Package transformAndWrap(StatechartDefinition statechart) { val gammaPackage = statechart.containingPackage diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index 6204439b7..5c4cde10a 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -50,6 +50,14 @@ import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.transformation.util.LowlevelNamings.* +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression +import hu.bme.mit.gamma.expression.model.EnumerableTypeDefinition +import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition class StatechartToLowlevelTransformer { // Auxiliary objects @@ -98,6 +106,14 @@ class StatechartToLowlevelTransformer { // return statechart.transformComponent as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition } + + def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition execute(SynchronousCoordinationStatechartDefinition statechart) { + // Eliminating merge states + val mergeStateEliminator = new MergeStateEliminator(statechart) + mergeStateEliminator.execute + // + return statechart.transformCoordinationAutomaton as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition + } protected def hu.bme.mit.gamma.statechart.lowlevel.model.Package transform(Package _package) { if (trace.isMapped(_package)) { @@ -461,4 +477,172 @@ class StatechartToLowlevelTransformer { return trace } + // Coordination automaton + + protected def dispatch Component transformCoordinationAutomaton(CoordinationStatechartDefinition statechart) { + if (trace.isMapped(statechart)) { + // It is already transformed + return trace.get(statechart) + } + val lowlevelStatechart = createStatechartDefinition => [ + it.name = getName(statechart) + it.schedulingOrder = statechart.schedulingOrder.transform + it.guardEvaluation = statechart.guardEvaluation.transform + it.orthogonalRegionSchedulingOrder = statechart.orthogonalRegionSchedulingOrder.transform + ] + if (!statechart.hasOrthogonalRegions) { + // If there are no orthogonal regions, then the guard evaluation policy is irrelevant; + // on the fly is the faster option, though + lowlevelStatechart.guardEvaluation = + hu.bme.mit.gamma.statechart.lowlevel.model.GuardEvaluation.ON_THE_FLY + } + if (statechart.hasAnnotation(RunUponExternalEventAnnotation)) { + lowlevelStatechart.addRunUponExternalEventAnnotation + } + if (statechart.hasAnnotation(RunUponExternalEventOrInternalTimeoutAnnotation)) { + lowlevelStatechart.addRunUponExternalEventOrInternalTimeoutAnnotation + } + trace.put(statechart, lowlevelStatechart) // Saving in trace + + // create scheduled control variable for each subcomponent + val scheduledComponentEnum = createEnumerationTypeDefinition + + // create default value, when no component is scheduled + val noComponentLiteral = createEnumerationLiteralDefinition + noComponentLiteral.name = "__nothing__" + scheduledComponentEnum.literals += noComponentLiteral + + // TODO is differentiation between SynchronousCoordinationStatechartDefinition and AsynchronousCoordinationStatechartDefinition necessary? + if (statechart.synchronous) { + for (subcomponent : (statechart as SynchronousCoordinationStatechartDefinition).components) { + val componentLiteral = createEnumerationLiteralDefinition + componentLiteral.name = subcomponent.name + scheduledComponentEnum.literals += componentLiteral + } + } else if (statechart.asynchronous) { + for (subcomponent : (statechart as AsynchronousCoordinationStatechartDefinition).components) { + val componentLiteral = createEnumerationLiteralDefinition + componentLiteral.name = subcomponent.name + scheduledComponentEnum.literals += componentLiteral + } + } else { + throw new IllegalArgumentException("CoordinationStateChart: " + statechart.name + " is neither synchronous nor asynchronous!") + } + val schedulableComponentsTypeDeclaration = scheduledComponentEnum.createTypeDeclaration("schedulableComponents") + statechart.typeDeclarations += schedulableComponentsTypeDeclaration + + val schedulableComponentsTypeReference = createTypeReference(schedulableComponentsTypeDeclaration) + + val scheduledCtrlVar = createVariableDeclaration(schedulableComponentsTypeReference, "scheduledComponent") + statechart.variableDeclarations += scheduledCtrlVar + + + // Constants + val gammaPackage = statechart.containingPackage + for (constantDeclaration : gammaPackage.selfAndImports // During code generation, imported constants can be referenced + .map[it.constantDeclarations].flatten) { + lowlevelStatechart.variableDeclarations += constantDeclaration.transform + } + // No parameter declarations mapping + for (parameterDeclaration : statechart.parameterDeclarations) { + val lowlevelParameterDeclaration = parameterDeclaration.transformComponentParameter + lowlevelStatechart.variableDeclarations += lowlevelParameterDeclaration + lowlevelStatechart.parameterDeclarations += lowlevelParameterDeclaration + } + for (variableDeclaration : statechart.variableDeclarations) { + lowlevelStatechart.variableDeclarations += variableDeclaration.transform + } + for (timeoutDeclaration : statechart.timeoutDeclarations) { + // Timeout declarations are transformed to integer variable declarations + val lowlevelTimeoutDeclaration = timeoutDeclaration.transform + lowlevelStatechart.variableDeclarations += lowlevelTimeoutDeclaration + lowlevelStatechart.timeoutDeclarations += lowlevelTimeoutDeclaration + } + for (port : statechart.ports) { + // Both in and out events are transformed to a boolean VarDecl with additional parameters + for (eventDeclaration : port.allEventDeclarations) { + val lowlevelEventDeclarations = eventDeclaration.transform(port) + lowlevelStatechart.eventDeclarations += lowlevelEventDeclarations + if (eventDeclaration.direction == EventDirection.INTERNAL) { + // Tracing + lowlevelStatechart.internalEventDeclarations += lowlevelEventDeclarations + } + } + } + for (region : statechart.regions) { + lowlevelStatechart.regions += region.transform + } + + + for (transition : statechart.coordinationTransitions) { + // Prioritizing transitions is done here + val lowlevelTransition = transition.transform(scheduledCtrlVar, scheduledComponentEnum) + lowlevelStatechart.transitions += lowlevelTransition + } + + + // Mapping port and interface invariants (now, not before, because we want to refer to e.g., state nodes and variables) + // First the interface invariants must be mapped to the ports realizing the interface + for (port : statechart.ports) { + val mappedInvariants = port.mapInterfaceInvariantsToPort + if (!mappedInvariants.empty) { + lowlevelStatechart.environmentalInvariants += mappedInvariants.map[it.transformSimpleExpression] + } + val invariants = port.invariants + if (!invariants.empty) { + lowlevelStatechart.environmentalInvariants += invariants.map[it.transformSimpleExpression] + } + } + + // Mapping statechart invariants + val statechartInvariants = statechart.invariants + if (!statechartInvariants.empty) { + lowlevelStatechart.invariants += statechartInvariants.map[it.transformSimpleExpression] + } + + return lowlevelStatechart + } + + protected def hu.bme.mit.gamma.statechart.lowlevel.model.Transition transform( + CoordinationTransition coordinationTransition, VariableDeclaration scheduledCtrlVar, + EnumerationTypeDefinition scheduledComponentEnum + ) { + // Trivial simple transitions + val gammaSource = coordinationTransition.sourceState + val gammaTarget = coordinationTransition.targetState + val lowlevelSource = if (gammaSource instanceof State) { + trace.get(gammaSource) + } else if (gammaSource instanceof PseudoState) { + trace.get(gammaSource) + } + val lowlevelTarget = if (gammaTarget instanceof State) { + trace.get(gammaTarget) + } else if (gammaTarget instanceof PseudoState) { + trace.get(gammaTarget) + } + val lowlevelTransition = createTransition => [ + it.source = lowlevelSource + it.target = lowlevelTarget + it.priority = coordinationTransition.calculatePriority.intValue // Priority is handled later + ] + trace.put(coordinationTransition, lowlevelTransition) // Saving in trace + // Important to trace the Gamma transition as the trigger transformer depends on it + lowlevelTransition.guard = coordinationTransition.transformTriggerAndGuard + val componentLiteral = createEnumerationLiteralDefinition + + if (coordinationTransition.coordinatedComponent instanceof SequentialCoordinationReferenceExpression) { + componentLiteral.name = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name + coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum.literals.get(0))) + } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression) { + componentLiteral.name = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name + coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum.literals.get(0))) + } else { + // transition without coordinated component + } + + lowlevelTransition.action = coordinationTransition.effects.transformActions + + return lowlevelTransition + } + } \ No newline at end of file diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index 62b644283..5c9c833e1 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -36,7 +36,9 @@ import hu.bme.mit.gamma.statechart.lowlevel.model.Package import hu.bme.mit.gamma.statechart.lowlevel.transformation.GammaToLowlevelTransformer import hu.bme.mit.gamma.statechart.lowlevel.transformation.Trace import hu.bme.mit.gamma.statechart.lowlevel.transformation.ValueDeclarationTransformer +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.util.GammaEcoreUtil import hu.bme.mit.gamma.util.JavaUtil import hu.bme.mit.gamma.xsts.model.AbstractAssignmentAction @@ -64,6 +66,7 @@ import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeature import static extension hu.bme.mit.gamma.xsts.transformation.util.Namings.* import static extension hu.bme.mit.gamma.xsts.transformation.util.QueueNamings.* import static extension java.lang.Math.* +import hu.bme.mit.gamma.statechart.util.StatechartUtil class ComponentTransformer { // This gammaToLowlevelTransformer must be the same during this transformation cycle due to tracing @@ -88,6 +91,7 @@ class ComponentTransformer { protected final extension EventConnector eventConnector = EventConnector.INSTANCE protected final extension InternalEventHandler internalEventHandler = InternalEventHandler.INSTANCE protected final extension SystemReducer systemReducer = SystemReducer.INSTANCE + protected final StatechartUtil statechartUtil = StatechartUtil.INSTANCE protected final extension ExpressionModelFactory expressionModelFactory = ExpressionModelFactory.eINSTANCE protected final extension XSTSModelFactory xStsModelFactory = XSTSModelFactory.eINSTANCE @@ -1339,6 +1343,177 @@ class ComponentTransformer { return xSts } + def dispatch XSTS transform(SynchronousCoordinationStatechartDefinition component, Package lowlevelPackage) { + val name = component.name + logger.info( "Transforming Synchronous Coordination Statechart " + name) + // TODO + val xSts = name.createXsts + val componentMergedActions = newHashMap // To handle multiple schedulings in CascadeCompositeComponents + val components = component.components + + if (components.empty) { + logger.warning("No components in Synchronous Coordination Statechart " + name) + return xSts + } + + val coordinationInstance = this.statechartUtil.instantiateSynchronousComponent(component) + + val lowlevelStatechart = gammaToLowlevelTransformer.transform(component) + lowlevelPackage.components += lowlevelStatechart + val lowlevelToXSTSTransformer = new LowlevelToXstsTransformer( + lowlevelPackage, optimize, transitionMerging) + val xStsEntry = lowlevelToXSTSTransformer.execute + lowlevelPackage.components -= lowlevelStatechart // So that next time the matches do not return elements from this statechart + val coordinationXSts = xStsEntry.key + + // Adding new elements + xSts.merge(coordinationXSts) + + component.components.add(coordinationInstance) + + val coordinationActualComponentMergedAction = createSequentialAction => [ + it.actions += coordinationXSts.mergedAction + ] + // In and Out actions - using sequential actions to make sure they are composite actions + // Methods reset... and delete... require this + val newCoordinationInEventAction = createSequentialAction => [ it.actions += coordinationXSts.inEventTransition.action ] + coordinationXSts.inEventTransition = newCoordinationInEventAction.wrap + val newCoordinationOutEventAction = createSequentialAction => [ it.actions += coordinationXSts.outEventTransition.action ] + coordinationXSts.outEventTransition = newCoordinationOutEventAction.wrap + // Resetting channel events + // 1) the Sync ort semantics: Resetting channel IN events AFTER schedule would result in a deadlock + // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components + // Note, System in and out events are reset in the env action + + // Resetting OUT events BEFORE schedule +// val clonedNewOutEventAction = newOutEventAction.clone // Clone is important +// .resetEverythingExceptPersistentParameters(subcomponentType) +// actualComponentMergedAction.actions.add(0, clonedNewOutEventAction) // Putting the new action BEFORE + // Tracing merged action + componentMergedActions += component -> coordinationActualComponentMergedAction.clone + + // In event + newCoordinationInEventAction.deleteEverythingExceptSystemEventsAndParameters(component) + + // Out event + newCoordinationOutEventAction.deleteEverythingExceptSystemEventsAndParameters(component) + + + + for (subcomponent : components.reject[it == coordinationInstance]) { + val subcomponentType = subcomponent.type + + // Normal transformation + subcomponentType.extractParameters(subcomponent.arguments) // Change the reference from parameters to constants + val newXSts = subcomponentType.transform(lowlevelPackage) + newXSts.customizeDeclarationNames(subcomponent) + + // Internal event handling here as EventReferenceHandler cannot be used without customizeDeclarationNames + if (subcomponentType.statechart) { + newXSts.addInternalEventHandlingActions(subcomponentType) + } + // + + // Adding new elements + xSts.merge(newXSts) + + // Merged action + val actualComponentMergedAction = createSequentialAction => [ + it.actions += newXSts.mergedAction + ] + // In and Out actions - using sequential actions to make sure they are composite actions + // Methods reset... and delete... require this + val newInEventAction = createSequentialAction => [ it.actions += newXSts.inEventTransition.action ] + newXSts.inEventTransition = newInEventAction.wrap + val newOutEventAction = createSequentialAction => [ it.actions += newXSts.outEventTransition.action ] + newXSts.outEventTransition = newOutEventAction.wrap + // Resetting channel events + // 1) the Sync ort semantics: Resetting channel IN events AFTER schedule would result in a deadlock + // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components + // Note, System in and out events are reset in the env action + + // Resetting OUT events BEFORE schedule +// val clonedNewOutEventAction = newOutEventAction.clone // Clone is important +// .resetEverythingExceptPersistentParameters(subcomponentType) +// actualComponentMergedAction.actions.add(0, clonedNewOutEventAction) // Putting the new action BEFORE + // Tracing merged action + componentMergedActions += subcomponentType -> actualComponentMergedAction.clone + + // In event + newInEventAction.deleteEverythingExceptSystemEventsAndParameters(component) + if (xSts !== newXSts) { // Only if this is not the first component + val inEventAction = createSequentialAction + inEventAction.actions += xSts.inEventTransition.action + inEventAction.actions += newInEventAction + xSts.inEventTransition = inEventAction.wrap + } + // Out event + newOutEventAction.deleteEverythingExceptSystemEventsAndParameters(component) + if (xSts !== newXSts) { // Only if this is not the first component + val outEventAction = createSequentialAction + outEventAction.actions += xSts.outEventTransition.action + outEventAction.actions += newOutEventAction + xSts.outEventTransition = outEventAction.wrap + } + } + // Merged action based on scheduling instances + val mergedAction = createSequentialAction + for (subcomponent : components.reject[it == coordinationInstance]) { + val subcomponentType = subcomponent.type + logger.info( "Checking subcomponent type " + subcomponentType + " in merged actions") + checkState(componentMergedActions.containsKey(subcomponentType)) + val componentMergedAction = componentMergedActions.get(subcomponentType).clone + mergedAction.actions += componentMergedAction + } + xSts.changeTransitions(mergedAction.wrap) + +// logger.info( "Deleting unused instance ports in " + name) +// xSts.deleteUnusedPorts(component) // Deleting variable assignments for unused ports +// +// // Connect only after "xSts.mergedTransition.action = mergedAction" / "xSts.changeTransitions" +// logger.info( "Connecting events through channels in " + name) +// xSts.connectEventsThroughChannels(component) // Event (variable setting) connecting across channels +// +// logger.info( "Binding event to system port events in " + name) +// val oldInEventAction = xSts.inEventTransition.action +// val bindingAssignments = xSts.createEventAndParameterAssignmentsBoundToTheSameSystemPort(component) +// // Optimization: removing old NonDeterministicActions +// bindingAssignments.removeNonDeterministicActionsReferencingAssignedVariables(oldInEventAction) +// +// val newInEventAction = createSequentialAction => [ +// it.actions += oldInEventAction +// // Bind together ports connected to the same system port +// it.actions += bindingAssignments +// ] +// +// xSts.inEventTransition = newInEventAction.wrap +// +// if (transformOrthogonalActions) { +// // After connectEventsThroughChannels +// logger.info( "Transforming orthogonal actions in XSTS " + name) +// xSts.mergedAction.transform(xSts) +// // Before optimize actions +// } +// +// if (optimize) { +// // Optimization: system in events (but not PERSISTENT parameters) can be reset after the merged transition +// // E.g., synchronous components do not reset system events +// xSts.resetInEventsAfterMergedAction(component) +// } +// +// // After in event optimization +// logger.info( "Adding internal event handlings in " + name) +// xSts.addInternalEventHandlingActions(component) + + return xSts + } + + def dispatch XSTS transform(AsynchronousCoordinationStatechartDefinition component, Package lowlevelPackage) { + logger.info( "Transforming Asynchronous Coordination Statechart " + component.name) + // TODO + return null + } + // Utils private def void extractAllParameters(AbstractAsynchronousCompositeComponent component) { From b61d1af9d6eaa81d3dacba6f5953e03e935a6636 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Thu, 19 Jun 2025 09:31:00 +0200 Subject: [PATCH 04/27] Coord automata is now generated to env --- .../transformation/ComponentTransformer.xtend | 32 ++++++++++--------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index 5c9c833e1..275fcfecc 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -1377,6 +1377,7 @@ class ComponentTransformer { // In and Out actions - using sequential actions to make sure they are composite actions // Methods reset... and delete... require this val newCoordinationInEventAction = createSequentialAction => [ it.actions += coordinationXSts.inEventTransition.action ] + coordinationActualComponentMergedAction.actions.forEach[ newCoordinationInEventAction.actions += it.clone] coordinationXSts.inEventTransition = newCoordinationInEventAction.wrap val newCoordinationOutEventAction = createSequentialAction => [ it.actions += coordinationXSts.outEventTransition.action ] coordinationXSts.outEventTransition = newCoordinationOutEventAction.wrap @@ -1393,10 +1394,10 @@ class ComponentTransformer { componentMergedActions += component -> coordinationActualComponentMergedAction.clone // In event - newCoordinationInEventAction.deleteEverythingExceptSystemEventsAndParameters(component) +// newCoordinationInEventAction.deleteEverythingExceptSystemEventsAndParameters(component) // Out event - newCoordinationOutEventAction.deleteEverythingExceptSystemEventsAndParameters(component) +// newCoordinationOutEventAction.deleteEverythingExceptSystemEventsAndParameters(component) @@ -1474,19 +1475,20 @@ class ComponentTransformer { // logger.info( "Connecting events through channels in " + name) // xSts.connectEventsThroughChannels(component) // Event (variable setting) connecting across channels // -// logger.info( "Binding event to system port events in " + name) -// val oldInEventAction = xSts.inEventTransition.action -// val bindingAssignments = xSts.createEventAndParameterAssignmentsBoundToTheSameSystemPort(component) -// // Optimization: removing old NonDeterministicActions -// bindingAssignments.removeNonDeterministicActionsReferencingAssignedVariables(oldInEventAction) -// -// val newInEventAction = createSequentialAction => [ -// it.actions += oldInEventAction -// // Bind together ports connected to the same system port -// it.actions += bindingAssignments -// ] -// -// xSts.inEventTransition = newInEventAction.wrap + logger.info( "Binding event to system port events in " + name) + val oldInEventAction = xSts.inEventTransition.action + val bindingAssignments = xSts.createEventAndParameterAssignmentsBoundToTheSameSystemPort(component) + // Optimization: removing old NonDeterministicActions + bindingAssignments.removeNonDeterministicActionsReferencingAssignedVariables(oldInEventAction) + + val newInEventAction = createSequentialAction => [ + it.actions += newCoordinationInEventAction + it.actions += oldInEventAction + // Bind together ports connected to the same system port + it.actions += bindingAssignments + ] + + xSts.inEventTransition = newInEventAction.wrap // // if (transformOrthogonalActions) { // // After connectEventsThroughChannels From 0368b78524312de91d1d554a8c9d045884e1e0e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 20 Jun 2025 16:51:47 +0200 Subject: [PATCH 05/27] Added util functions for EnumerationExpressions --- .../mit/gamma/expression/util/ExpressionUtil.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java b/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java index df51075a7..ea2ecc507 100644 --- a/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java +++ b/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java @@ -567,6 +567,15 @@ public Set getReferredValues(Expression expression) { return referred; } + public EnumerationLiteralDefinition getEnumerationLiteralDefinitionByName(EnumerationTypeDefinition typeDefinition, String name) { + for (EnumerationLiteralDefinition literal : typeDefinition.getLiterals()) { + if (literal.getName().equals(name)) { + return literal; + } + } + throw new IllegalArgumentException("No EnumerationLiteralDefinition found in: " + typeDefinition + " for name: " + name); + } + // Extract parameters public List extractParameters(ParametricElement parametricElement, @@ -1271,6 +1280,12 @@ public EnumerationLiteralExpression createEnumerationLiteralExpression( return literalExpression; } + + public EnumerationLiteralExpression createEnumerationLiteralExpression( + EnumerationTypeDefinition typeDefinition, String name) { + return createEnumerationLiteralExpression(getEnumerationLiteralDefinitionByName(typeDefinition, name)); + } + public Expression createDefaultExpression(Collection expressions) { Expression orExpression = wrapIntoOrExpression(expressions); NotExpression notExpression = createNotExpression( From 3e009a32cd210152248a0702c225eab8626233c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 20 Jun 2025 16:53:07 +0200 Subject: [PATCH 06/27] More work on coordination automata --- .../GammaToLowlevelTransformer.xtend | 3 +- .../StatechartToLowlevelTransformer.xtend | 30 +++++++++---------- .../transformation/ComponentTransformer.xtend | 14 +++++++-- 3 files changed, 29 insertions(+), 18 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend index b812cfdc2..f4cc65c4d 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend @@ -18,6 +18,7 @@ import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.expression.model.VariableDeclaration class GammaToLowlevelTransformer { @@ -55,7 +56,7 @@ class GammaToLowlevelTransformer { return statechart.execute } - def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition transform(SynchronousCoordinationStatechartDefinition statechart) { + def Pair transform(SynchronousCoordinationStatechartDefinition statechart) { return statechart.execute } diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index 5c4cde10a..66ad5fdf1 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -56,8 +56,8 @@ import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression -import hu.bme.mit.gamma.expression.model.EnumerableTypeDefinition import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition +import hu.bme.mit.gamma.expression.model.EqualityExpression class StatechartToLowlevelTransformer { // Auxiliary objects @@ -76,6 +76,8 @@ class StatechartToLowlevelTransformer { protected final extension ActionModelFactory actionFactory = ActionModelFactory.eINSTANCE // Trace object for storing the mappings protected final Trace trace + //Coordination Automata + protected VariableDeclaration scheduledCtrlVar new() { this(null) @@ -107,12 +109,12 @@ class StatechartToLowlevelTransformer { return statechart.transformComponent as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition } - def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition execute(SynchronousCoordinationStatechartDefinition statechart) { + def Pair execute(SynchronousCoordinationStatechartDefinition statechart) { // Eliminating merge states val mergeStateEliminator = new MergeStateEliminator(statechart) mergeStateEliminator.execute // - return statechart.transformCoordinationAutomaton as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition + return statechart.transformCoordinationAutomaton } protected def hu.bme.mit.gamma.statechart.lowlevel.model.Package transform(Package _package) { @@ -479,10 +481,10 @@ class StatechartToLowlevelTransformer { // Coordination automaton - protected def dispatch Component transformCoordinationAutomaton(CoordinationStatechartDefinition statechart) { + protected def Pair transformCoordinationAutomaton(CoordinationStatechartDefinition statechart) { if (trace.isMapped(statechart)) { // It is already transformed - return trace.get(statechart) + return new Pair(trace.get(statechart), scheduledCtrlVar) } val lowlevelStatechart = createStatechartDefinition => [ it.name = getName(statechart) @@ -533,7 +535,7 @@ class StatechartToLowlevelTransformer { val schedulableComponentsTypeReference = createTypeReference(schedulableComponentsTypeDeclaration) - val scheduledCtrlVar = createVariableDeclaration(schedulableComponentsTypeReference, "scheduledComponent") + scheduledCtrlVar = createVariableDeclaration(schedulableComponentsTypeReference, "scheduledComponent") statechart.variableDeclarations += scheduledCtrlVar @@ -576,7 +578,7 @@ class StatechartToLowlevelTransformer { for (transition : statechart.coordinationTransitions) { // Prioritizing transitions is done here - val lowlevelTransition = transition.transform(scheduledCtrlVar, scheduledComponentEnum) + val lowlevelTransition = transition.transform(scheduledComponentEnum) lowlevelStatechart.transitions += lowlevelTransition } @@ -600,12 +602,11 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.invariants += statechartInvariants.map[it.transformSimpleExpression] } - return lowlevelStatechart + return new Pair(lowlevelStatechart, scheduledCtrlVar) } protected def hu.bme.mit.gamma.statechart.lowlevel.model.Transition transform( - CoordinationTransition coordinationTransition, VariableDeclaration scheduledCtrlVar, - EnumerationTypeDefinition scheduledComponentEnum + CoordinationTransition coordinationTransition, EnumerationTypeDefinition scheduledComponentEnum ) { // Trivial simple transitions val gammaSource = coordinationTransition.sourceState @@ -628,14 +629,13 @@ class StatechartToLowlevelTransformer { trace.put(coordinationTransition, lowlevelTransition) // Saving in trace // Important to trace the Gamma transition as the trigger transformer depends on it lowlevelTransition.guard = coordinationTransition.transformTriggerAndGuard - val componentLiteral = createEnumerationLiteralDefinition if (coordinationTransition.coordinatedComponent instanceof SequentialCoordinationReferenceExpression) { - componentLiteral.name = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name - coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum.literals.get(0))) + val componentName = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name + coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression) { - componentLiteral.name = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name - coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum.literals.get(0))) + val componentName = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name + coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) } else { // transition without coordinated component } diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index ec0297e0d..ccdd69356 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -67,6 +67,8 @@ import static extension hu.bme.mit.gamma.xsts.transformation.util.Namings.* import static extension hu.bme.mit.gamma.xsts.transformation.util.QueueNamings.* import static extension java.lang.Math.* import hu.bme.mit.gamma.statechart.util.StatechartUtil +import hu.bme.mit.gamma.expression.model.VariableDeclaration +import hu.bme.mit.gamma.expression.model.EqualityExpression class ComponentTransformer { // This gammaToLowlevelTransformer must be the same during this transformation cycle due to tracing @@ -1393,7 +1395,9 @@ class ComponentTransformer { val coordinationInstance = this.statechartUtil.instantiateSynchronousComponent(component) - val lowlevelStatechart = gammaToLowlevelTransformer.transform(component) + val transformedCoordinationStatechart = gammaToLowlevelTransformer.transform(component) + val lowlevelStatechart = transformedCoordinationStatechart.key + val scheduledCtrlVar = transformedCoordinationStatechart.value lowlevelPackage.components += lowlevelStatechart val lowlevelToXSTSTransformer = new LowlevelToXstsTransformer( lowlevelPackage, optimize, transitionMerging) @@ -1499,7 +1503,8 @@ class ComponentTransformer { logger.info( "Checking subcomponent type " + subcomponentType + " in merged actions") checkState(componentMergedActions.containsKey(subcomponentType)) val componentMergedAction = componentMergedActions.get(subcomponentType).clone - mergedAction.actions += componentMergedAction +// mergedAction.actions += componentMergedAction + mergedAction.actions += createIfAction(createComponentScheduledEqualityExpression(scheduledCtrlVar, subcomponent.name) , componentMergedAction) } xSts.changeTransitions(mergedAction.wrap) @@ -1691,4 +1696,9 @@ class ComponentTransformer { } } + protected def EqualityExpression createComponentScheduledEqualityExpression(VariableDeclaration scheduledCtrlVar, String name) { + val enumTypeDefinition = scheduledCtrlVar.typeDefinition as EnumerationTypeDefinition + return createEqualityExpression(scheduledCtrlVar, createEnumerationLiteralExpression(enumTypeDefinition, name)) + } + } \ No newline at end of file From cefb8957de23d19361a517b851bf337f2a751f06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 5 Aug 2025 12:32:42 +0200 Subject: [PATCH 07/27] Added additional logging to SystemReducer --- .../src/hu/bme/mit/gamma/xsts/transformation/SystemReducer.xtend | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/SystemReducer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/SystemReducer.xtend index 2eeca5b72..5e87fe06d 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/SystemReducer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/SystemReducer.xtend @@ -80,6 +80,7 @@ class SystemReducer { val xStsDeletableAssignmentActions = newHashSet for (instance : component.derivedComponents) { for (instancePort : instance.unusedPorts) { + logger.info("Unused port: " + component.name + "." + instancePort.name) // In events on required port for (inputEvent : instancePort.inputEvents) { val inEventName = inputEvent.customizeInputName(instancePort, instance) From f01a48c52f88493239c2e3b0748dbd59be2d7fee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 5 Aug 2025 12:48:36 +0200 Subject: [PATCH 08/27] Added Imply serialization to XstsExprSerializer, see Theta XstsDsl Imply operator --- .../xsts/transformation/serializer/ExpressionSerializer.xtend | 3 +++ 1 file changed, 3 insertions(+) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ExpressionSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ExpressionSerializer.xtend index 3b5bfd8e8..14c70d5ff 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ExpressionSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ExpressionSerializer.xtend @@ -18,6 +18,7 @@ import hu.bme.mit.gamma.expression.model.ElseExpression import hu.bme.mit.gamma.expression.model.EnumerationLiteralExpression import hu.bme.mit.gamma.expression.model.Expression import hu.bme.mit.gamma.expression.model.IfThenElseExpression +import hu.bme.mit.gamma.expression.model.ImplyExpression import hu.bme.mit.gamma.expression.model.ModExpression import hu.bme.mit.gamma.expression.model.NotExpression import hu.bme.mit.gamma.expression.util.ExpressionTypeDeterminator2 @@ -47,6 +48,8 @@ class ExpressionSerializer extends hu.bme.mit.gamma.expression.util.ExpressionSe override String _serialize(NotExpression expression) '''(«super._serialize(expression)»)''' + override String _serialize(ImplyExpression expression) '''(«expression.leftOperand.serialize» => «expression.rightOperand.serialize»)''' + override String _serialize(ArrayAccessExpression expression) '''«expression.operand.serialize»[«expression.index.serialize»]''' // The default branch has to contain the default value of the type: crucial for back-annotation override String _serialize(ArrayLiteralExpression expression) '''[«FOR i : 0 ..< expression.operands.size SEPARATOR ', '»«i» <- «expression.operands.get(i).serialize»«ENDFOR», default <- «expression.operands.head.type.defaultExpression.serialize»]''' From e6261cf507d602f939ee8364e46a52007042b561 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 5 Aug 2025 12:54:20 +0200 Subject: [PATCH 09/27] Added CoordinationVariableAnnotation to mark variable used for coordination --- .../model/statechart.ecore | 12 +- .../model/statechart.genmodel | 17 +- .../StatechartModelDerivedFeatures.java | 18 +- .../gamma/statechart/util/StatechartUtil.java | 5 + .../StatechartToLowlevelTransformer.xtend | 220 ++++++++++++++---- .../derivedfeatures/XstsDerivedFeatures.java | 8 + 6 files changed, 219 insertions(+), 61 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore index 5aee53314..a1f3b343c 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.ecore @@ -169,15 +169,9 @@ upperBound="-1" eType="#//CoordinationTransition" containment="true"/> - - + eSuperTypes="#//CoordinationStatechartDefinition composite.ecore#//SynchronousComponent composite.ecore#//SynchronousCompositeComponent"/> - - + eSuperTypes="#//CoordinationStatechartDefinition composite.ecore#//AsynchronousComponent composite.ecore#//AsynchronousCompositeComponent"/> @@ -192,4 +186,6 @@ eSuperTypes="#//AbstractCoordinationReferenceExpression"/> + diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel index 652791d07..1dd289881 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/model/statechart.genmodel @@ -398,21 +398,18 @@ - + + - - - - - - - - - + + + + + diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java index 460836e44..fadb76d70 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java @@ -48,6 +48,7 @@ import hu.bme.mit.gamma.expression.model.TypeDeclaration; import hu.bme.mit.gamma.expression.model.TypeDefinition; import hu.bme.mit.gamma.expression.model.TypeReference; +import hu.bme.mit.gamma.expression.model.VariableDeclaration; import hu.bme.mit.gamma.statechart.composite.AbstractAsynchronousCompositeComponent; import hu.bme.mit.gamma.statechart.composite.AbstractSynchronousCompositeComponent; import hu.bme.mit.gamma.statechart.composite.AsynchronousAdapter; @@ -113,6 +114,7 @@ import hu.bme.mit.gamma.statechart.statechart.ClockTickReference; import hu.bme.mit.gamma.statechart.statechart.CompositeElement; import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; +import hu.bme.mit.gamma.statechart.statechart.CoordinationVariableDeclarationAnnotation; import hu.bme.mit.gamma.statechart.statechart.DeepHistoryState; import hu.bme.mit.gamma.statechart.statechart.EntryState; import hu.bme.mit.gamma.statechart.statechart.ForkState; @@ -143,6 +145,7 @@ import hu.bme.mit.gamma.statechart.statechart.UnaryTrigger; import hu.bme.mit.gamma.statechart.util.StatechartUtil; + public class StatechartModelDerivedFeatures extends ActionModelDerivedFeatures { protected static final StatechartUtil statechartUtil = StatechartUtil.INSTANCE; @@ -1879,10 +1882,7 @@ public static List getAllBoundSimplePorts(Component component) { public static List getAllBoundSimplePorts(Port port) { List simplePorts = new ArrayList(); Component component = getContainingComponent(port); - if (component instanceof StatechartDefinition) { - simplePorts.add(port); - } - else if (component instanceof CompositeComponent composite) { + if (component instanceof CompositeComponent composite) { for (PortBinding portBinding : composite.getPortBindings()) { if (portBinding.getCompositeSystemPort() == port) { // Makes sense only if the containment hierarchy is a tree structure @@ -1893,6 +1893,9 @@ else if (component instanceof CompositeComponent composite) { } } } + else if (component instanceof StatechartDefinition) { + simplePorts.add(port); + } // Note that one port can be in the list multiple times iff the component is NOT unfolded return simplePorts; } @@ -3814,4 +3817,11 @@ public static List mapInterfaceInvariantsToPort(Port port) { return interfaceInvariants; } + // Coordination + + public static List getCoordinationVariables(StatechartDefinition statechart) { + return filterVariablesByAnnotation(statechart.getVariableDeclarations(), + CoordinationVariableDeclarationAnnotation.class); + } + } \ No newline at end of file diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java index 4310af166..52e3758d4 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java @@ -1246,4 +1246,9 @@ public void removeRegions(CompositeElement element) { ecoreUtil.removeAll(element.getRegions()); } + // Coordination + + public void addCoordinationVariableAnnotation(VariableDeclaration variable) { + addAnnotation(variable, statechartFactory.createCoordinationVariableDeclarationAnnotation()); + } } \ No newline at end of file diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index 66ad5fdf1..1f5c1ec7d 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -57,7 +57,7 @@ import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechart import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition -import hu.bme.mit.gamma.expression.model.EqualityExpression +import hu.bme.mit.gamma.statechart.util.StatechartUtil class StatechartToLowlevelTransformer { // Auxiliary objects @@ -70,6 +70,7 @@ class StatechartToLowlevelTransformer { protected final extension GammaEcoreUtil gammaEcoreUtil = GammaEcoreUtil.INSTANCE protected final extension LowlevelStatechartUtil lowlevelUtil = LowlevelStatechartUtil.INSTANCE protected final extension EventAttributeTransformer eventAttributeTransformer = EventAttributeTransformer.INSTANCE + protected final StatechartUtil statechartUtil = StatechartUtil.INSTANCE // Low-level statechart model factory protected final extension StatechartModelFactory factory = StatechartModelFactory.eINSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE @@ -109,7 +110,7 @@ class StatechartToLowlevelTransformer { return statechart.transformComponent as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition } - def Pair execute(SynchronousCoordinationStatechartDefinition statechart) { + def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition execute(SynchronousCoordinationStatechartDefinition statechart) { // Eliminating merge states val mergeStateEliminator = new MergeStateEliminator(statechart) mergeStateEliminator.execute @@ -481,10 +482,10 @@ class StatechartToLowlevelTransformer { // Coordination automaton - protected def Pair transformCoordinationAutomaton(CoordinationStatechartDefinition statechart) { + protected def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition transformCoordinationAutomaton(CoordinationStatechartDefinition statechart) { if (trace.isMapped(statechart)) { // It is already transformed - return new Pair(trace.get(statechart), scheduledCtrlVar) + return trace.get(statechart) as hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition } val lowlevelStatechart = createStatechartDefinition => [ it.name = getName(statechart) @@ -535,9 +536,16 @@ class StatechartToLowlevelTransformer { val schedulableComponentsTypeReference = createTypeReference(schedulableComponentsTypeDeclaration) + // TODO add ctrl var annotation scheduledCtrlVar = createVariableDeclaration(schedulableComponentsTypeReference, "scheduledComponent") + statechartUtil.addCoordinationVariableAnnotation(scheduledCtrlVar) statechart.variableDeclarations += scheduledCtrlVar + // Transforming CoordinationTransitions to regular transitions, possibly creating VariableDeclarations and States + for (transition : statechart.coordinationTransitions) { + transition.transformCoordinationTransition(scheduledComponentEnum) + } + // Constants val gammaPackage = statechart.containingPackage @@ -575,10 +583,9 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.regions += region.transform } - - for (transition : statechart.coordinationTransitions) { + for (transition : statechart.transitions) { // Prioritizing transitions is done here - val lowlevelTransition = transition.transform(scheduledComponentEnum) + val lowlevelTransition = transition.transform lowlevelStatechart.transitions += lowlevelTransition } @@ -602,47 +609,182 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.invariants += statechartInvariants.map[it.transformSimpleExpression] } - return new Pair(lowlevelStatechart, scheduledCtrlVar) + // TODO remove + return lowlevelStatechart } - protected def hu.bme.mit.gamma.statechart.lowlevel.model.Transition transform( + protected def transformCoordinationTransition( CoordinationTransition coordinationTransition, EnumerationTypeDefinition scheduledComponentEnum ) { - // Trivial simple transitions - val gammaSource = coordinationTransition.sourceState + var gammaSource = coordinationTransition.sourceState + val sourceName = gammaSource.name + val containingStatechart = gammaSource.containingStatechart + val region = gammaSource.getParentRegion + val gammaTarget = coordinationTransition.targetState - val lowlevelSource = if (gammaSource instanceof State) { - trace.get(gammaSource) - } else if (gammaSource instanceof PseudoState) { - trace.get(gammaSource) - } - val lowlevelTarget = if (gammaTarget instanceof State) { - trace.get(gammaTarget) - } else if (gammaTarget instanceof PseudoState) { - trace.get(gammaTarget) - } - val lowlevelTransition = createTransition => [ - it.source = lowlevelSource - it.target = lowlevelTarget - it.priority = coordinationTransition.calculatePriority.intValue // Priority is handled later - ] - trace.put(coordinationTransition, lowlevelTransition) // Saving in trace - // Important to trace the Gamma transition as the trigger transformer depends on it - lowlevelTransition.guard = coordinationTransition.transformTriggerAndGuard - + if (coordinationTransition.coordinatedComponent instanceof SequentialCoordinationReferenceExpression) { - val componentName = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name - coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) + if (!coordinationTransition.coordinatedComponent.instances.empty) { + for (var i = 0; i < coordinationTransition.coordinatedComponent.instances.size; i++) { + val componentInstanceReference = coordinationTransition.coordinatedComponent.instances.get(i) + val componentName = componentInstanceReference.componentInstance.name + + if (i == coordinationTransition.coordinatedComponent.instances.size - 1) { + + val internalTransition = statechartUtil.createTransition(gammaSource, gammaTarget) + internalTransition.trigger = coordinationTransition.trigger.clone + internalTransition.guard = coordinationTransition.guard.clone + internalTransition.effects += + createAssignment(scheduledCtrlVar, + createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) + internalTransition.effects += coordinationTransition.effects.clone + + containingStatechart.transitions += internalTransition + } else { + val internalState = statechartUtil.createState(region, sourceName + "_" + i++) + if (gammaTarget instanceof State) { + internalState.invariants += gammaTarget.invariants.clone + internalState.entryActions += gammaTarget.entryActions.clone + internalState.exitActions += gammaTarget.exitActions.clone + internalState.annotations += gammaTarget.annotations.clone + } + + val internalTransition = statechartUtil.createTransition(gammaSource, internalState) + internalTransition.trigger = coordinationTransition.trigger.clone + internalTransition.guard = coordinationTransition.guard.clone + internalTransition.effects += + createAssignment(scheduledCtrlVar, + createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) + + gammaSource = internalState + containingStatechart.transitions += internalTransition + } + } + } } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression) { - val componentName = coordinationTransition.coordinatedComponent.instances.get(0).componentInstance.name - coordinationTransition.effects += createAssignment(scheduledCtrlVar, createEnumerationLiteralExpression(scheduledComponentEnum, componentName)) +// val unordComponentEnum = createEnumerationTypeDefinition + val unordName = "unord_" + gammaSource.name + gammaTarget.name + val unordBoolVariables = newHashMap + + /* XSTS: + * + * ctrl var unord_q0q3 : enum{Sensor1, Sensor2, Sensor3, Sensor4} + * ctrl var unord_q0q3_Sensor1 : boolean = false + * ctrl var unord_q0q3_Sensor2 : boolean = false + * ctrl var unord_q0q3_Sensor3 : boolean = false + * ctrl var unord_q0q3_Sensor4 : boolean = false + */ + + for (componentInstanceReference : coordinationTransition.coordinatedComponent.instances) { +// val componentLiteral = createEnumerationLiteralDefinition +// componentLiteral.name = componentInstanceReference.componentInstance.name +// unordComponentEnum.literals += componentLiteral + + unordBoolVariables += + componentInstanceReference.componentInstance -> + createVariableDeclarationWithDefaultInitialValue(createBooleanTypeDefinition, + unordName + "_" + componentInstanceReference.componentInstance.name) + } + +// val unordComponentsTypeDeclaration = unordComponentEnum.createTypeDeclaration(unordName) +// containingStatechart.typeDeclarations += unordComponentsTypeDeclaration +// +// val unordComponentsTypeReference = createTypeReference(unordComponentsTypeDeclaration) + + // TODO add ctrl var annotation +// val unordComponentsVariableDecl = createVariableDeclaration(unordComponentsTypeReference, unordName) +// containingStatechart.variableDeclarations += unordComponentsVariableDecl + containingStatechart.variableDeclarations += unordBoolVariables.values + + /* XSTS: + * if (coordState == q0) { + * assume c1 > 1 && c1 <= 2; + * havoc unord_q0q3; TODO initializing! + * choice { + * assume unord_q0q3 == Sensor1 && !unord_q0q3_Sensor1; + * unord_q0q3_Sensor1 := true; + * scheduled := Sensor1; + * } or { + * assume unord_q0q3 == Sensor2 && !unord_q0q3_Sensor2; + * unord_q0q3_Sensor2 := true; + * scheduled := Sensor2; + * } or { + * ... // Sensor3 + * } or { + * ... // Sensor4 + * } + * if (unord_q0q3_Sensor1 && unord_q0q3_Sensor2 && unord_q0q3_Sensor3 && unord_q0q3_Sensor4) { + * c1 := 0; + * coordState := q3; + * unord_q0q3_Sensor1 := false; + * unord_q0q3_Sensor2 := false; + * ... // Sensor3, Sensor4 + * } + * } + */ + + // creating new transition sourceState->sourceState for every componentInstance + +// if (gammaSource instanceof State) { +// gammaSource.entryActions += createHavocStatement => [ +// it.lhs = unordComponentsVariableDecl.createReferenceExpression +// ] +// } + for (componentInstanceReference : coordinationTransition.coordinatedComponent.instances) { + val componentName = componentInstanceReference.componentInstance.name + + val internalTransition = statechartUtil.createTransition(gammaSource, gammaSource) + internalTransition.trigger = coordinationTransition.trigger.clone + internalTransition.guard = createAndExpression => [ + if (coordinationTransition.guard !== null) { + it.operands += coordinationTransition.guard.clone + } +// it.operands += +// createEqualityExpression(unordComponentsVariableDecl, +// createEnumerationLiteralExpression(unordComponentEnum, componentName)) + it.operands += + createEqualityExpression(unordBoolVariables.get(componentInstanceReference.componentInstance), + createFalseExpression) + ] + internalTransition.effects += + createAssignment(scheduledCtrlVar, + createEnumerationLiteralExpression(scheduledCtrlVar.typeDefinition as EnumerationTypeDefinition, componentName)) + internalTransition.effects += + createAssignment(unordBoolVariables.get(componentInstanceReference.componentInstance), + createTrueExpression) + containingStatechart.transitions += internalTransition + } + + // creating new transition sourceState->targetState if every component was executed, reset action for each bool + + val finalTransition = statechartUtil.createTransition(gammaSource, gammaTarget) + finalTransition.trigger = coordinationTransition.trigger.clone + + val guardExpression = createAndExpression => [ + if (coordinationTransition.guard !== null) { + it.operands += coordinationTransition.guard.clone + } + ] + finalTransition.guard = guardExpression + + for (componentInstanceReference : coordinationTransition.coordinatedComponent.instances) { + guardExpression.operands += + createEqualityExpression(unordBoolVariables.get(componentInstanceReference.componentInstance), + createTrueExpression) + finalTransition.effects += + createAssignment(unordBoolVariables.get(componentInstanceReference.componentInstance), + createFalseExpression) + } + containingStatechart.transitions += finalTransition + } else { - // transition without coordinated component + val transition = statechartUtil.createTransition(gammaSource, gammaTarget) + transition.trigger = coordinationTransition.trigger.clone + transition.guard = coordinationTransition.guard.clone + transition.effects += coordinationTransition.effects.clone + transition.annotations += coordinationTransition.annotations.clone + containingStatechart.transitions += transition } - - lowlevelTransition.action = coordinationTransition.effects.transformActions - - return lowlevelTransition } } \ No newline at end of file diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java b/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java index f7f91b18d..4cf96209a 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java @@ -35,6 +35,7 @@ import hu.bme.mit.gamma.expression.model.LiteralExpression; import hu.bme.mit.gamma.expression.model.ReferenceExpression; import hu.bme.mit.gamma.expression.model.VariableDeclaration; +import hu.bme.mit.gamma.statechart.statechart.CoordinationVariableDeclarationAnnotation; import hu.bme.mit.gamma.util.Triple; import hu.bme.mit.gamma.xsts.model.AbstractAssignmentAction; import hu.bme.mit.gamma.xsts.model.Action; @@ -1203,4 +1204,11 @@ else if (secondExpr instanceof DirectReferenceExpression rhsIdentifierExpression literalVariableAssignments, variableVariableAssignments, notLiteralVariables); } + // Coordination + + public static List getCoordinationVariables(XSTS xSts) { + return filterVariablesByAnnotation(xSts.getVariableDeclarations(), + CoordinationVariableDeclarationAnnotation.class); + } + } From af28c8895e86c02c73f1d6cf09d85ea9e7ee6d7c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 5 Aug 2025 12:55:48 +0200 Subject: [PATCH 10/27] Simplified coordination transformation using CoordinationVariableAnnotation, further work on coordination transformation --- .../util/preprocessor/ModelUnfolder.xtend | 56 ++++++++ .../GammaToLowlevelTransformer.xtend | 2 +- .../serializer/ActionSerializer.xtend | 2 + .../transformation/ComponentTransformer.xtend | 128 +++++++++++------- 4 files changed, 140 insertions(+), 48 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend index 347478d18..baa4ec2aa 100644 --- a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend +++ b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend @@ -44,6 +44,8 @@ import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.transformation.util.Namings.* +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition class ModelUnfolder { @@ -204,6 +206,60 @@ class ModelUnfolder { // No tracing as it handles only instances } + private dispatch def void copyComponents(SynchronousCoordinationStatechartDefinition component, + Package gammaPackage, Trace trace) { + for (instance : component.components) { + val type = instance.type + val clonedPackage = type.containingPackage.clone + val clonedComponent = clonedPackage.components + .findFirst[it.helperEquals(type)] as SynchronousComponent // Sync composite or Statechart + clonedComponent.removeAnnotations // To prevent importing unnecessary resources into the resource set + gammaPackage.components += clonedComponent // Adding it to the "Instance container" + instance.type = clonedComponent // Setting the type to the new declaration + // Declarations must be copied AFTER moving component instances to enable reference changes + gammaPackage.addDeclarations(clonedPackage) + + // Changing the port binding + fixPortBindings(component, instance) + // Changing the providedPort references of Channels + fixChannelProvidedPorts(component, instance) + // Changing the requiredPort references of Channels + fixChannelRequiredPorts(component, instance) + if (clonedComponent instanceof AbstractSynchronousCompositeComponent) { + clonedComponent.copyComponents(gammaPackage, trace) // Cloning the contained CompositeSystems recursively + } + // Tracing + type.traceComponentInstances(clonedComponent, trace) + } + } + + private dispatch def void copyComponents(AsynchronousCoordinationStatechartDefinition component, + Package gammaPackage, Trace trace) { + for (instance : component.components) { + val type = instance.type + + val clonedPackage = type.containingPackage.clone + val clonedComponent = clonedPackage.components + .findFirst[it.helperEquals(type)] as AsynchronousComponent + gammaPackage.components += clonedComponent + + instance.type = clonedComponent + // Declarations must be copied AFTER moving component instances to enable reference changes + gammaPackage.addDeclarations(clonedPackage) + + clonedComponent.copyComponents(gammaPackage, trace) // Cloning the contained CompositeSystems recursively + + // Tracing + type.traceComponentInstances(clonedComponent, trace) + // Changing the port binding + fixPortBindings(component, instance) + // Changing the providedPort references of Channels + fixChannelProvidedPorts(component, instance) + // Changing the requiredPort references of Channels + fixChannelRequiredPorts(component, instance) + } + } + protected def void removeAnnotations(Component component) { if (component instanceof StatechartDefinition) { val keepableAnnotations = #[ RunUponExternalEventAnnotation, RunUponExternalEventOrInternalTimeoutAnnotation ] diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend index f4cc65c4d..dce938af6 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend @@ -56,7 +56,7 @@ class GammaToLowlevelTransformer { return statechart.execute } - def Pair transform(SynchronousCoordinationStatechartDefinition statechart) { + def hu.bme.mit.gamma.statechart.lowlevel.model.StatechartDefinition transform(SynchronousCoordinationStatechartDefinition statechart) { return statechart.execute } diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend index 913ab8d2c..7f7a0a0f8 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend @@ -38,6 +38,7 @@ class ActionSerializer { return xSts.serializeXsts(false) } + // TODO how to handle the env in non timed case? def String serializeXsts(XSTS xSts, boolean serializePrimedVariables) ''' «xSts.serializeDeclarations(serializePrimedVariables)» @@ -49,6 +50,7 @@ class ActionSerializer { «xSts.initializingAction.serialize» } env { + «IF xSts.timed && !xSts.coordinationVariables.empty»__delay;«ENDIF» «xSts.environmentalAction.serialize» } ''' diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index ccdd69356..a101af778 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -12,10 +12,12 @@ package hu.bme.mit.gamma.xsts.transformation import hu.bme.mit.gamma.expression.model.ArrayTypeDefinition import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition +import hu.bme.mit.gamma.expression.model.EqualityExpression import hu.bme.mit.gamma.expression.model.Expression import hu.bme.mit.gamma.expression.model.ExpressionModelFactory import hu.bme.mit.gamma.expression.model.TypeDeclaration import hu.bme.mit.gamma.expression.model.TypeReference +import hu.bme.mit.gamma.expression.model.VariableDeclaration import hu.bme.mit.gamma.expression.util.ExpressionEvaluator import hu.bme.mit.gamma.lowlevel.xsts.transformation.LowlevelToXstsTransformer import hu.bme.mit.gamma.lowlevel.xsts.transformation.TransitionMerging @@ -39,6 +41,7 @@ import hu.bme.mit.gamma.statechart.lowlevel.transformation.ValueDeclarationTrans import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.util.StatechartUtil import hu.bme.mit.gamma.util.GammaEcoreUtil import hu.bme.mit.gamma.util.JavaUtil import hu.bme.mit.gamma.xsts.model.AbstractAssignmentAction @@ -66,9 +69,6 @@ import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeature import static extension hu.bme.mit.gamma.xsts.transformation.util.Namings.* import static extension hu.bme.mit.gamma.xsts.transformation.util.QueueNamings.* import static extension java.lang.Math.* -import hu.bme.mit.gamma.statechart.util.StatechartUtil -import hu.bme.mit.gamma.expression.model.VariableDeclaration -import hu.bme.mit.gamma.expression.model.EqualityExpression class ComponentTransformer { // This gammaToLowlevelTransformer must be the same during this transformation cycle due to tracing @@ -1395,28 +1395,52 @@ class ComponentTransformer { val coordinationInstance = this.statechartUtil.instantiateSynchronousComponent(component) - val transformedCoordinationStatechart = gammaToLowlevelTransformer.transform(component) - val lowlevelStatechart = transformedCoordinationStatechart.key - val scheduledCtrlVar = transformedCoordinationStatechart.value + val lowlevelStatechart = gammaToLowlevelTransformer.transform(component) lowlevelPackage.components += lowlevelStatechart val lowlevelToXSTSTransformer = new LowlevelToXstsTransformer( lowlevelPackage, optimize, transitionMerging) val xStsEntry = lowlevelToXSTSTransformer.execute lowlevelPackage.components -= lowlevelStatechart // So that next time the matches do not return elements from this statechart val coordinationXSts = xStsEntry.key - + val coordinationXStsTrace = xStsEntry.value + // getting the xsts variable of the scheduled component + + var VariableDeclaration xstsScheduledCtrlVar = null + val coordinationVariables = coordinationXSts.coordinationVariables + if (!coordinationVariables.empty) { + // There must be only one + xstsScheduledCtrlVar = coordinationVariables.get(0) + } + coordinationXSts.customizeDeclarationNames(coordinationInstance) + // Adding new elements xSts.merge(coordinationXSts) + + // Initializing action + val coordinationVariableInitAction = createSequentialAction + coordinationVariableInitAction.actions += coordinationXSts.variableInitializingTransition.action + xSts.variableInitializingTransition = coordinationVariableInitAction.wrap + val coordinationConfigInitAction = createSequentialAction + coordinationConfigInitAction.actions += coordinationXSts.configurationInitializingTransition.action + xSts.configurationInitializingTransition = coordinationConfigInitAction.wrap + val coordinationEntryAction = createSequentialAction + coordinationEntryAction.actions += coordinationXSts.entryEventTransition.action + xSts.entryEventTransition = coordinationEntryAction.wrap component.components.add(coordinationInstance) - val coordinationActualComponentMergedAction = createSequentialAction => [ - it.actions += coordinationXSts.mergedAction - ] +// val coordinationActualComponentMergedAction = createSequentialAction => [ +// it.actions += coordinationXSts.mergedAction +// ] // In and Out actions - using sequential actions to make sure they are composite actions // Methods reset... and delete... require this - val newCoordinationInEventAction = createSequentialAction => [ it.actions += coordinationXSts.inEventTransition.action ] - coordinationActualComponentMergedAction.actions.forEach[ newCoordinationInEventAction.actions += it.clone] + + // The coordination automata needs to be executed in the env step + val newCoordinationInEventAction = createSequentialAction => [ + it.actions += coordinationXSts.inEventTransition.action + it.actions += coordinationXSts.mergedAction + ] + coordinationXSts.inEventTransition = newCoordinationInEventAction.wrap val newCoordinationOutEventAction = createSequentialAction => [ it.actions += coordinationXSts.outEventTransition.action ] coordinationXSts.outEventTransition = newCoordinationOutEventAction.wrap @@ -1425,20 +1449,12 @@ class ComponentTransformer { // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components // Note, System in and out events are reset in the env action + // TODO // Resetting OUT events BEFORE schedule // val clonedNewOutEventAction = newOutEventAction.clone // Clone is important // .resetEverythingExceptPersistentParameters(subcomponentType) // actualComponentMergedAction.actions.add(0, clonedNewOutEventAction) // Putting the new action BEFORE - // Tracing merged action - componentMergedActions += component -> coordinationActualComponentMergedAction.clone - - // In event -// newCoordinationInEventAction.deleteEverythingExceptSystemEventsAndParameters(component) - // Out event -// newCoordinationOutEventAction.deleteEverythingExceptSystemEventsAndParameters(component) - - for (subcomponent : components.reject[it == coordinationInstance]) { val subcomponentType = subcomponent.type @@ -1455,7 +1471,21 @@ class ComponentTransformer { // // Adding new elements - xSts.merge(newXSts) + xSts.merge(newXSts) + + // Initializing action + val variableInitAction = createSequentialAction + variableInitAction.actions += xSts.variableInitializingTransition.action + variableInitAction.actions += newXSts.variableInitializingTransition.action + xSts.variableInitializingTransition = variableInitAction.wrap + val configInitAction = createSequentialAction + configInitAction.actions += xSts.configurationInitializingTransition.action + configInitAction.actions += newXSts.configurationInitializingTransition.action + xSts.configurationInitializingTransition = configInitAction.wrap + val entryAction = createSequentialAction + entryAction.actions += xSts.entryEventTransition.action + entryAction.actions += newXSts.entryEventTransition.action + xSts.entryEventTransition = entryAction.wrap // Merged action val actualComponentMergedAction = createSequentialAction => [ @@ -1463,7 +1493,8 @@ class ComponentTransformer { ] // In and Out actions - using sequential actions to make sure they are composite actions // Methods reset... and delete... require this - val newInEventAction = createSequentialAction => [ it.actions += newXSts.inEventTransition.action ] + val newSeqAction = createSequentialAction => [ it.actions += newXSts.inEventTransition.action ] + val newInEventAction = createIfAction(createComponentScheduledEqualityExpression(xstsScheduledCtrlVar, subcomponent.name), newSeqAction) newXSts.inEventTransition = newInEventAction.wrap val newOutEventAction = createSequentialAction => [ it.actions += newXSts.outEventTransition.action ] newXSts.outEventTransition = newOutEventAction.wrap @@ -1472,6 +1503,7 @@ class ComponentTransformer { // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components // Note, System in and out events are reset in the env action + // TODO // Resetting OUT events BEFORE schedule // val clonedNewOutEventAction = newOutEventAction.clone // Clone is important // .resetEverythingExceptPersistentParameters(subcomponentType) @@ -1496,25 +1528,25 @@ class ComponentTransformer { xSts.outEventTransition = outEventAction.wrap } } - // Merged action based on scheduling instances - val mergedAction = createSequentialAction + + val nondetAction = createNonDeterministicAction + for (subcomponent : components.reject[it == coordinationInstance]) { val subcomponentType = subcomponent.type logger.info( "Checking subcomponent type " + subcomponentType + " in merged actions") checkState(componentMergedActions.containsKey(subcomponentType)) val componentMergedAction = componentMergedActions.get(subcomponentType).clone -// mergedAction.actions += componentMergedAction - mergedAction.actions += createIfAction(createComponentScheduledEqualityExpression(scheduledCtrlVar, subcomponent.name) , componentMergedAction) + nondetAction.extendChoiceWithBranch(createComponentScheduledEqualityExpression(xstsScheduledCtrlVar, subcomponent.name), componentMergedAction) } - xSts.changeTransitions(mergedAction.wrap) + xSts.changeTransitions(nondetAction.wrap) + + logger.info( "Deleting unused instance ports in " + name) + xSts.deleteUnusedPorts(component) // Deleting variable assignments for unused ports + + // Connect only after "xSts.mergedTransition.action = mergedAction" / "xSts.changeTransitions" + logger.info( "Connecting events through channels in " + name) + xSts.connectEventsThroughChannels(component) // Event (variable setting) connecting across channels -// logger.info( "Deleting unused instance ports in " + name) -// xSts.deleteUnusedPorts(component) // Deleting variable assignments for unused ports -// -// // Connect only after "xSts.mergedTransition.action = mergedAction" / "xSts.changeTransitions" -// logger.info( "Connecting events through channels in " + name) -// xSts.connectEventsThroughChannels(component) // Event (variable setting) connecting across channels -// logger.info( "Binding event to system port events in " + name) val oldInEventAction = xSts.inEventTransition.action val bindingAssignments = xSts.createEventAndParameterAssignmentsBoundToTheSameSystemPort(component) @@ -1522,6 +1554,8 @@ class ComponentTransformer { bindingAssignments.removeNonDeterministicActionsReferencingAssignedVariables(oldInEventAction) val newInEventAction = createSequentialAction => [ + // TODO Add delay + it.actions += newCoordinationInEventAction it.actions += oldInEventAction // Bind together ports connected to the same system port @@ -1529,23 +1563,23 @@ class ComponentTransformer { ] xSts.inEventTransition = newInEventAction.wrap -// -// if (transformOrthogonalActions) { -// // After connectEventsThroughChannels -// logger.info( "Transforming orthogonal actions in XSTS " + name) -// xSts.mergedAction.transform(xSts) -// // Before optimize actions -// } -// + + if (transformOrthogonalActions) { + // After connectEventsThroughChannels + logger.info( "Transforming orthogonal actions in XSTS " + name) + xSts.mergedAction.transform(xSts) + // Before optimize actions + } + // if (optimize) { // // Optimization: system in events (but not PERSISTENT parameters) can be reset after the merged transition // // E.g., synchronous components do not reset system events // xSts.resetInEventsAfterMergedAction(component) // } -// -// // After in event optimization -// logger.info( "Adding internal event handlings in " + name) -// xSts.addInternalEventHandlingActions(component) + + // After in event optimization + logger.info( "Adding internal event handlings in " + name) + xSts.addInternalEventHandlingActions(component) return xSts } From 666c1279abb7cc70e33196a1b1ad68f3b3e84615 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 5 Aug 2025 12:56:22 +0200 Subject: [PATCH 11/27] Removed unnecessary printout --- .../language/scoping/StatechartLanguageScopeProvider.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java index 98c94139d..f34d86c22 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java @@ -387,8 +387,6 @@ public IScope getScope(final EObject context, final EReference reference) { } catch (Exception e) { e.printStackTrace(); } - System.out.println(context); - System.out.println(reference); return super.getScope(context, reference); } From 6b2070e9baab21e1219658653917f1aac6b6274a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 27 Jan 2026 15:36:06 +0100 Subject: [PATCH 12/27] Added PlantUML visualization for CoordinationAutomata --- .../META-INF/MANIFEST.MF | 1 + .../plugin.xml | 129 ++++++++++- .../CoordinationLayoutHandler.java | 24 +++ .../plantuml/commandhandler/TextProvider.java | 17 +- .../CoordinationToPlantUmlTransformer.xtend | 201 ++++++++++++++++++ 5 files changed, 370 insertions(+), 2 deletions(-) create mode 100644 plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/CoordinationLayoutHandler.java create mode 100644 plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/META-INF/MANIFEST.MF b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/META-INF/MANIFEST.MF index 98d2ed84f..fb1d103e2 100644 --- a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/META-INF/MANIFEST.MF +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/META-INF/MANIFEST.MF @@ -8,6 +8,7 @@ Automatic-Module-Name: hu.bme.mit.gamma.statechart.plantuml.commandhandler Bundle-RequiredExecutionEnvironment: JavaSE-17 Require-Bundle: org.eclipse.emf.ecore, org.eclipse.jface, + org.eclipse.ui, org.eclipse.ui.ide, org.eclipse.equinox.registry, net.sourceforge.plantuml.eclipse, diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/plugin.xml b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/plugin.xml index df7d8716f..4211dcf92 100644 --- a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/plugin.xml +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/plugin.xml @@ -1,5 +1,5 @@ - + @@ -9,4 +9,131 @@ providerClass="hu.bme.mit.gamma.plantuml.commandhandler.TextProvider"> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/CoordinationLayoutHandler.java b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/CoordinationLayoutHandler.java new file mode 100644 index 000000000..0f6cda7af --- /dev/null +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/CoordinationLayoutHandler.java @@ -0,0 +1,24 @@ +package hu.bme.mit.gamma.plantuml.commandhandler; + +import org.eclipse.core.commands.AbstractHandler; +import org.eclipse.core.commands.ExecutionEvent; +import org.eclipse.core.commands.ExecutionException; +import org.eclipse.ui.handlers.HandlerUtil; +import org.eclipse.ui.handlers.RadioState; + +public class CoordinationLayoutHandler extends AbstractHandler { + + @Override + public Object execute(ExecutionEvent event) throws ExecutionException { + + if (HandlerUtil.matchesRadioState(event)) + return null; // we are already in the updated state - do nothing + + String currentState = event.getParameter(RadioState.PARAMETER_ID); + // update the current state + HandlerUtil.updateRadioState(event.getCommand(), currentState); + + return null; + } + +} \ No newline at end of file diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java index 69c0c239e..8ef06fb61 100644 --- a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java @@ -15,6 +15,7 @@ import java.util.List; import java.util.stream.Collectors; +import org.eclipse.core.commands.Command; import org.eclipse.core.resources.IFile; import org.eclipse.core.runtime.IPath; import org.eclipse.emf.common.util.URI; @@ -23,12 +24,16 @@ import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; import org.eclipse.jface.viewers.ISelection; import org.eclipse.jface.viewers.IStructuredSelection; +import org.eclipse.ui.PlatformUI; +import org.eclipse.ui.commands.ICommandService; +import org.eclipse.ui.handlers.RadioState; import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition; import hu.bme.mit.gamma.expression.model.FunctionDeclaration; import hu.bme.mit.gamma.expression.model.RecordTypeDefinition; import hu.bme.mit.gamma.plantuml.transformation.AdapterToPlantUmlTransformer; import hu.bme.mit.gamma.plantuml.transformation.CompositeToPlantUmlTransformer; +import hu.bme.mit.gamma.plantuml.transformation.CoordinationToPlantUmlTransformer; import hu.bme.mit.gamma.plantuml.transformation.InterfaceToPlantUmlTransformer; import hu.bme.mit.gamma.plantuml.transformation.StatechartToPlantUmlTransformer; import hu.bme.mit.gamma.plantuml.transformation.TraceToPlantUmlTransformer; @@ -36,6 +41,7 @@ import hu.bme.mit.gamma.statechart.composite.CompositeComponent; import hu.bme.mit.gamma.statechart.interface_.Component; import hu.bme.mit.gamma.statechart.interface_.Package; +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition; import hu.bme.mit.gamma.trace.model.ExecutionTrace; import net.sourceforge.plantuml.eclipse.utils.WorkbenchPartDiagramIntentProviderContext; @@ -116,7 +122,16 @@ private String getComponentPlantUmlCode(Resource resource) { List components = _package.getComponents(); if (!components.isEmpty()) { Component component = components.get(0); - if (component instanceof StatechartDefinition) { + if (component instanceof CoordinationStatechartDefinition) { + ICommandService commandService = + PlatformUI.getWorkbench().getService(ICommandService.class); + Command command = commandService.getCommand("hu.bme.mit.gamma.plantuml.coordinationLayoutCommand"); + String state = (String)command.getState(RadioState.STATE_ID).getValue(); + CoordinationStatechartDefinition statechartDefinition = (CoordinationStatechartDefinition) component; + CoordinationToPlantUmlTransformer transformer = new CoordinationToPlantUmlTransformer( + statechartDefinition, state); + return transformer.execute(); + } else if (component instanceof StatechartDefinition) { StatechartDefinition statechartDefinition = (StatechartDefinition) component; StatechartToPlantUmlTransformer transformer = new StatechartToPlantUmlTransformer( statechartDefinition); diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend b/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend new file mode 100644 index 000000000..17c800f8c --- /dev/null +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend @@ -0,0 +1,201 @@ +package hu.bme.mit.gamma.plantuml.transformation + +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.PseudoState +import hu.bme.mit.gamma.statechart.statechart.State +import hu.bme.mit.gamma.statechart.composite.CompositeComponent +import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition +import hu.bme.mit.gamma.statechart.statechart.EntryState + +import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* +import hu.bme.mit.gamma.statechart.statechart.AbstractCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression + +class CoordinationToPlantUmlTransformer extends StatechartToPlantUmlTransformer { + protected final CoordinationStatechartDefinition statechart + + protected final CompositeToPlantUmlTransformer compositeTransformer + + enum CoordinationLayoutType { + COORDINATION, + COMPOSITION, + COORDINATION_COMPOSITION + } + + protected CoordinationLayoutType layoutType + + new(CoordinationStatechartDefinition statechart) { + super(statechart) + this.statechart = statechart + this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart as CompositeComponent) + this.layoutType = CoordinationLayoutType.COORDINATION + } + + new(CoordinationStatechartDefinition statechart, String layoutType) { + super(statechart) + this.statechart = statechart + this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart as CompositeComponent) + this.layoutType = CoordinationLayoutType.valueOf(layoutType) + } + + /** + * execute() + * + * This method combines the functionality of the StatechartToPlantUmlTransformer and the functionality of the + * CompositeToPlantUmlTransformer + * + */ + override String execute() { + switch (layoutType) { + case COORDINATION: { + return executeCoordinationLayout + } + case COMPOSITION: { + return executeCompositionLayout + } + case COORDINATION_COMPOSITION: { + return executeCoordinationCompositionLayout + } + default: { + return executeCoordinationLayout + } + } + } + + def String executeCoordinationLayout() ''' + @startuml + + skin rose + skinparam backgroundcolor transparent + skinparam legend { + BackgroundColor lightgrey + } + + skinparam nodesep 30 + skinparam ranksep 30 + skinparam padding 5 + «statechart.listVariablesInNote()» + «statechart.mainRegionSearch» + + @enduml + ''' + + def String executeCompositionLayout() ''' + «compositeTransformer.execute()» + ''' + + // TODO Better solution for replacing the @startuml and @enduml tags + def String executeCoordinationCompositionLayout() ''' + @startuml + left to right direction + + package Components [ + {{ + «compositeTransformer.execute().replace("@startuml","").replace("@enduml","")» + }} + ] + + package Coordination [ + {{ + skin rose + skinparam backgroundcolor transparent + skinparam legend { + BackgroundColor lightgrey + } + + skinparam nodesep 30 + skinparam ranksep 30 + skinparam padding 5 + «statechart.listVariablesInNote()» + «statechart.mainRegionSearch» + }} + ] + + @enduml + ''' + + /** + * mainRegionSearch(CoordinationStatechartDefinition) + * + * This method has the same functionality as the mainRegionSearch function of the StatechartToPlantUmlTransformer, but using + * CoordinationTransitions + * + */ + protected def mainRegionSearch(CoordinationStatechartDefinition statechart) { + val mainString = ''' + «IF statechart.regions.size > 1»state «statechart.name» {«ENDIF» + «FOR main : statechart.regions» + «FOR pseudo: main.stateNodes» + «IF pseudo instanceof PseudoState» + «pseudo.transformPseudoState» + «ENDIF» + «ENDFOR» + «FOR mainstate: main.stateNodes.filter(State)» + «regionSearch(mainstate, statechart)» + «IF !(mainstate instanceof PseudoState)» + «IF stateActionsSearch(mainstate) !== null» + «stateActionsSearch(mainstate)» + «ENDIF» + «ENDIF» + «ENDFOR» + «FOR transition : statechart.coordinationTransitions» + «FOR mainstate: main.stateNodes» + «IF transition.sourceState == mainstate» + «stateSearch(transition)» + «ENDIF» + «ENDFOR» + «ENDFOR» + + «IF !(isLastRegion(statechart.regions, main))» + -- + «ENDIF» + + «ENDFOR» + «IF statechart.regions.size > 1» + } + [*] -> «statechart.name» + «ENDIF» + ''' + return mainString + } + + /** + * stateSearch(CoordinationTransition) + * + * This method searches the source and target state of the transition received as parameter. + * This is where the visualization of the initial and history states is handled, as well as + * the obtaining of the guards and triggers of transitions. + * The end result will look like this: + * + * State1 -> State2 : trigger [guard] / action + * + */ + protected def stateSearch(CoordinationTransition transition) { + val source = transition.sourceState + val trigger = transition.trigger + val guard = transition.guard + val effects = transition.effects + val target = transition.targetState + var arrow = "" + if (source instanceof EntryState || (source.parentRegion.orthogonal && target.state)) { + arrow = "->" + } else { + arrow = "-->" + } + return ''' + «transition.sourceText» «arrow» «target.name»«IF !transition.empty» : «ENDIF»«IF trigger !== null»«trigger.transformTrigger»«ENDIF» «IF guard !== null»\n[«guard.serialize + .replaceAll("\\|\\|", "||\\\\n").replaceAll("\\&\\&", "&&\\\\n")»]«ENDIF»«FOR effect : effects BEFORE ' /\\n' SEPARATOR '\\n'»«effect.transformAction»«ENDFOR»«transition.coordinatedComponent.serializeCoordinatedComponent» + ''' + } + + protected def serializeCoordinatedComponent (AbstractCoordinationReferenceExpression expression) { + if (expression instanceof SequentialCoordinationReferenceExpression) { + return ''' \n / execute: «IF expression.instances.length > 1»SEQ{«ENDIF»«FOR instance : expression.instances SEPARATOR ','»«instance.componentInstance.name»«ENDFOR»«IF expression.instances.length > 1»}«ENDIF»''' + } else if (expression instanceof UnorderedCoordinationReferenceExpression) { + return ''' \n / execute: UNORD{«FOR instance : expression.instances SEPARATOR ','»«instance.componentInstance.name»«ENDFOR»}''' + } + + return '''''' + } +} \ No newline at end of file From 57aff9f1d250ec59131d8af13180c924fb85e872 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 27 Jan 2026 15:43:58 +0100 Subject: [PATCH 13/27] Added separate warnings for unconnected ports --- .../hu/bme/mit/gamma/statechart/util/ExpressionSerializer.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/ExpressionSerializer.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/ExpressionSerializer.java index 450306dba..68bc4660b 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/ExpressionSerializer.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/ExpressionSerializer.java @@ -201,6 +201,9 @@ public String serialize(Expression expression) { if (expression instanceof ComponentInstanceEventParameterReferenceExpression reference) { return _serialize(reference); } + if (expression instanceof TimeoutReferenceExpression reference) { + return _serialize(reference); + } return super.serialize(expression); } From 4990c716486d71665241fc9fe7e0f7378e900640 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 27 Jan 2026 15:49:02 +0100 Subject: [PATCH 14/27] Added util function for oncycle trigger to StatechartUtil --- .../mit/gamma/statechart/util/StatechartUtil.java | 15 +++++++++++++++ .../OriginalEnvironmentBehaviorCreator.xtend | 4 ++-- .../transformation/TriggerTransformer.xtend | 2 +- .../mit/gamma/mutation/ModelElementMutator.xtend | 2 +- 4 files changed, 19 insertions(+), 4 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java index 52e3758d4..3f5b48b9d 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java @@ -98,6 +98,8 @@ import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.StatechartModelFactory; import hu.bme.mit.gamma.statechart.statechart.SynchronousStatechartDefinition; +import hu.bme.mit.gamma.statechart.statechart.TimeoutDeclaration; +import hu.bme.mit.gamma.statechart.statechart.TimeoutReferenceExpression; import hu.bme.mit.gamma.statechart.statechart.Transition; import hu.bme.mit.gamma.statechart.statechart.TransitionPriority; import hu.bme.mit.gamma.statechart.statechart.UnaryTrigger; @@ -438,6 +440,10 @@ public UnaryTrigger createUnaryTrigger(Trigger trigger, UnaryType type) { return unaryTrigger; } + public Trigger createOnCycleTrigger() { + return statechartFactory.createOnCycleTrigger(); + } + public void extendGuard(Transition transition, Expression guard) { extendGuard(transition, guard, factory.createAndExpression()); } @@ -1251,4 +1257,13 @@ public void removeRegions(CompositeElement element) { public void addCoordinationVariableAnnotation(VariableDeclaration variable) { addAnnotation(variable, statechartFactory.createCoordinationVariableDeclarationAnnotation()); } + + // TimeoutReferenceExpression + + public TimeoutReferenceExpression createTimeoutReferenceExpression(TimeoutDeclaration timeout) { + TimeoutReferenceExpression expression = statechartFactory.createTimeoutReferenceExpression(); + expression.setTimeout(timeout); + + return expression; + } } \ No newline at end of file diff --git a/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/OriginalEnvironmentBehaviorCreator.xtend b/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/OriginalEnvironmentBehaviorCreator.xtend index 0141a73e1..d079fd791 100644 --- a/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/OriginalEnvironmentBehaviorCreator.xtend +++ b/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/OriginalEnvironmentBehaviorCreator.xtend @@ -85,7 +85,7 @@ class OriginalEnvironmentBehaviorCreator { val inOutCycleState = environmentModel.createRegionWithState(inOutCycleRegionName, inOutCycleInitialStateName, inOutCycleStateName) val inOutCycleTransition = inOutCycleState.createTransition(inOutCycleState) - inOutCycleTransition.trigger = createOnCycleTrigger + inOutCycleTransition.trigger = statechartModelFactory.createOnCycleTrigger inOutCycleTransition.effects += inOutCycleVariable.createAssignment( inOutCycleVariable.createReferenceExpression.createNotExpression) } @@ -136,7 +136,7 @@ class OriginalEnvironmentBehaviorCreator { region.stateNodes += lastTargetState val firstTransition = createTransition => [ - it.trigger = createOnCycleTrigger + it.trigger = statechartModelFactory.createOnCycleTrigger ] firstTransition.sourceState = internalLastState firstTransition.targetState = lastTargetState diff --git a/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/TriggerTransformer.xtend b/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/TriggerTransformer.xtend index 8f996ecfb..66123746f 100644 --- a/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/TriggerTransformer.xtend +++ b/plugins/core/hu.bme.mit.gamma.trace.environment.transformation/src/hu/bme/mit/gamma/trace/environment/transformation/TriggerTransformer.xtend @@ -128,7 +128,7 @@ class TriggerTransformer { } else if (transition.trigger === null) { // The old transition has to have a trigger - transition.trigger = createOnCycleTrigger + transition.trigger = statechartModelFactory.createOnCycleTrigger } } diff --git a/plugins/mutation/hu.bme.mit.gamma.mutation/src/hu/bme/mit/gamma/mutation/ModelElementMutator.xtend b/plugins/mutation/hu.bme.mit.gamma.mutation/src/hu/bme/mit/gamma/mutation/ModelElementMutator.xtend index 2422b1d8f..a173289c3 100644 --- a/plugins/mutation/hu.bme.mit.gamma.mutation/src/hu/bme/mit/gamma/mutation/ModelElementMutator.xtend +++ b/plugins/mutation/hu.bme.mit.gamma.mutation/src/hu/bme/mit/gamma/mutation/ModelElementMutator.xtend @@ -115,7 +115,7 @@ class ModelElementMutator { def removeTransitionTrigger(Transition transition) { val trigger = transition.trigger - val onCycleTrigger = createOnCycleTrigger + val onCycleTrigger = statechartFactory.createOnCycleTrigger onCycleTrigger.replace(trigger) From 082ade4647c472220c6b2ae81b6ddd9188673214 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 11:58:08 +0100 Subject: [PATCH 15/27] Added util functions for CoordinationTransitions --- .../util/StatechartModelValidator.java | 15 ++++++-- .../gamma/statechart/util/StatechartUtil.java | 38 +++++++++++++++++++ 2 files changed, 49 insertions(+), 4 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java index 9b2e94994..7254a4b22 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartModelValidator.java @@ -1499,10 +1499,17 @@ public Collection checkComponentInstances(ComponentInst } Collection unusedPorts = StatechartModelDerivedFeatures.getUnusedPorts(instance); if (!unusedPorts.isEmpty()) { - validationResultMessages.add(new ValidationResultMessage(ValidationResult.WARNING, - "The following ports are used neither in a system port binding nor a channel: " + - unusedPorts.stream().map(it -> it.getName()).collect(Collectors.toSet()), - new ReferenceInfo(ExpressionModelPackage.Literals.NAMED_ELEMENT__NAME))); + for (Port port : unusedPorts) { + var msg = new ValidationResultMessage(ValidationResult.WARNING, + "The following port are used neither in a system port binding nor a channel: " + instance.getName() + "." + port.getName(), + new ReferenceInfo(ExpressionModelPackage.Literals.NAMED_ELEMENT__NAME)); + validationResultMessages.add(msg); + } + +// validationResultMessages.add(new ValidationResultMessage(ValidationResult.WARNING, +// "The following ports are used neither in a system port binding nor a channel: " + +// unusedPorts.stream().map(it -> it.getName()).collect(Collectors.toSet()), +// new ReferenceInfo(ExpressionModelPackage.Literals.NAMED_ELEMENT__NAME))); } return validationResultMessages; } diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java index 3f5b48b9d..6d849485f 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java @@ -14,6 +14,7 @@ import java.util.ArrayList; import java.util.Collection; import java.util.HashSet; +import java.util.Iterator; import java.util.LinkedList; import java.util.List; import java.util.Map.Entry; @@ -88,11 +89,14 @@ import hu.bme.mit.gamma.statechart.statechart.BinaryType; import hu.bme.mit.gamma.statechart.statechart.ChoiceState; import hu.bme.mit.gamma.statechart.statechart.CompositeElement; +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; +import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition; import hu.bme.mit.gamma.statechart.statechart.EntryState; import hu.bme.mit.gamma.statechart.statechart.InitialState; import hu.bme.mit.gamma.statechart.statechart.PortEventReference; import hu.bme.mit.gamma.statechart.statechart.RaiseEventAction; import hu.bme.mit.gamma.statechart.statechart.Region; +import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression; import hu.bme.mit.gamma.statechart.statechart.State; import hu.bme.mit.gamma.statechart.statechart.StateNode; import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition; @@ -104,6 +108,7 @@ import hu.bme.mit.gamma.statechart.statechart.TransitionPriority; import hu.bme.mit.gamma.statechart.statechart.UnaryTrigger; import hu.bme.mit.gamma.statechart.statechart.UnaryType; +import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression; public class StatechartUtil extends ActionUtil { // Singleton @@ -1258,6 +1263,39 @@ public void addCoordinationVariableAnnotation(VariableDeclaration variable) { addAnnotation(variable, statechartFactory.createCoordinationVariableDeclarationAnnotation()); } + public CoordinationTransition createSequentialCoordinationTransition(StateNode source, StateNode target, List coordinatedComponents) { + CoordinationTransition transition = statechartFactory.createCoordinationTransition(); + transition.setSourceState(source); + transition.setTargetState(target); + SequentialCoordinationReferenceExpression expression = statechartFactory.createSequentialCoordinationReferenceExpression(); + expression.getInstances().addAll(ecoreUtil.clone(coordinatedComponents)); + + transition.setCoordinatedComponent(expression); + + CoordinationStatechartDefinition statechart = + (CoordinationStatechartDefinition) StatechartModelDerivedFeatures.getContainingStatechart(source); + if (statechart != null) { + statechart.getCoordinationTransitions().add(transition); + } + return transition; + } + + public CoordinationTransition createUnorderedCoordinationTransition(StateNode source, StateNode target, List coordinatedComponents) { + CoordinationTransition transition = statechartFactory.createCoordinationTransition(); + transition.setSourceState(source); + transition.setTargetState(target); + UnorderedCoordinationReferenceExpression expression = statechartFactory.createUnorderedCoordinationReferenceExpression(); + expression.getInstances().addAll(coordinatedComponents); + transition.setCoordinatedComponent(expression); + + CoordinationStatechartDefinition statechart = + (CoordinationStatechartDefinition) StatechartModelDerivedFeatures.getContainingStatechart(source); + if (statechart != null) { + statechart.getCoordinationTransitions().add(transition); + } + return transition; + } + // TimeoutReferenceExpression public TimeoutReferenceExpression createTimeoutReferenceExpression(TimeoutDeclaration timeout) { From a8b4df3af7ec66e8cf28edce1458241de21b6d9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 12:02:21 +0100 Subject: [PATCH 16/27] Added util function to generate all possible permutations of a list --- .../src/hu/bme/mit/gamma/util/JavaUtil.xtend | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend b/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend index 44c862f1c..0d65e8b4d 100644 --- a/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend +++ b/plugins/core/hu.bme.mit.gamma.util/src/hu/bme/mit/gamma/util/JavaUtil.xtend @@ -11,6 +11,7 @@ package hu.bme.mit.gamma.util import java.util.AbstractMap.SimpleEntry +import java.util.ArrayList import java.util.Collection import java.util.List import java.util.Map @@ -407,4 +408,28 @@ class JavaUtil { causeMessage.startsWith("CreateProcess error=") // CreateProcess error=2, but not sure about the literal in other OS } + def List> getAllPermutations(List original) { + val workingCopy = original.clone + val List> result = new ArrayList> + + if (workingCopy.size == 1) { + val List innerResult = newArrayList + innerResult.add(workingCopy.get(0)) + result += innerResult + return result + } + + val firstElement = workingCopy.get(0) + val permutations = getAllPermutations(workingCopy.subList(1, workingCopy.size)) + for (permutation : permutations) { + val permutationSize = permutation.size + for (var i = 0; i <= permutationSize; i++) { + val permutationCopy = newArrayList(permutation.clone) + permutationCopy.add(i, firstElement) + result += permutationCopy + } + } + + return result + } } \ No newline at end of file From dbfa0a080eecb5bcc87eaf7e98ee92393d14d0d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 12:05:30 +0100 Subject: [PATCH 17/27] Modified unordered coordination transformation --- .../ExpressionTransformer.xtend | 2 +- .../StatechartToLowlevelTransformer.xtend | 95 +++++++++++-------- 2 files changed, 56 insertions(+), 41 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/ExpressionTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/ExpressionTransformer.xtend index 7e711e56a..c1052517e 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/ExpressionTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/ExpressionTransformer.xtend @@ -410,7 +410,7 @@ class ExpressionTransformer { // - private def Expression getValueOfTimeout(TimeoutDeclaration timeoutDeclaration) { + protected def Expression getValueOfTimeout(TimeoutDeclaration timeoutDeclaration) { val gammaStatechart = timeoutDeclaration.containingStatechart val timeoutSettings = gammaStatechart.getAllContentsOfType(SetTimeoutAction) val correctTimeoutSetting = timeoutSettings.filter[it.timeoutDeclaration == timeoutDeclaration] diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index 1f5c1ec7d..292441b66 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -11,6 +11,7 @@ package hu.bme.mit.gamma.statechart.lowlevel.transformation import hu.bme.mit.gamma.action.model.ActionModelFactory +import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition import hu.bme.mit.gamma.expression.model.Expression import hu.bme.mit.gamma.expression.model.ExpressionModelFactory import hu.bme.mit.gamma.expression.model.TrueExpression @@ -26,6 +27,9 @@ import hu.bme.mit.gamma.statechart.lowlevel.model.EventDeclaration import hu.bme.mit.gamma.statechart.lowlevel.model.StateNode import hu.bme.mit.gamma.statechart.lowlevel.model.StatechartModelFactory import hu.bme.mit.gamma.statechart.lowlevel.util.LowlevelStatechartUtil +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition import hu.bme.mit.gamma.statechart.statechart.DeepHistoryState import hu.bme.mit.gamma.statechart.statechart.GuardEvaluation import hu.bme.mit.gamma.statechart.statechart.InitialState @@ -35,14 +39,19 @@ import hu.bme.mit.gamma.statechart.statechart.Region import hu.bme.mit.gamma.statechart.statechart.RunUponExternalEventAnnotation import hu.bme.mit.gamma.statechart.statechart.RunUponExternalEventOrInternalTimeoutAnnotation import hu.bme.mit.gamma.statechart.statechart.SchedulingOrder +import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression import hu.bme.mit.gamma.statechart.statechart.ShallowHistoryState import hu.bme.mit.gamma.statechart.statechart.State import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.TimeoutAction import hu.bme.mit.gamma.statechart.statechart.TimeoutDeclaration import hu.bme.mit.gamma.statechart.statechart.TimeoutEventReference import hu.bme.mit.gamma.statechart.statechart.Transition +import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.util.StatechartUtil import hu.bme.mit.gamma.util.GammaEcoreUtil +import hu.bme.mit.gamma.util.JavaUtil import java.util.List import static com.google.common.base.Preconditions.checkState @@ -50,14 +59,6 @@ import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.transformation.util.LowlevelNamings.* -import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition -import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition -import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition -import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition -import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression -import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression -import hu.bme.mit.gamma.expression.model.EnumerationTypeDefinition -import hu.bme.mit.gamma.statechart.util.StatechartUtil class StatechartToLowlevelTransformer { // Auxiliary objects @@ -71,6 +72,7 @@ class StatechartToLowlevelTransformer { protected final extension LowlevelStatechartUtil lowlevelUtil = LowlevelStatechartUtil.INSTANCE protected final extension EventAttributeTransformer eventAttributeTransformer = EventAttributeTransformer.INSTANCE protected final StatechartUtil statechartUtil = StatechartUtil.INSTANCE + protected final extension JavaUtil javaUtil = JavaUtil.INSTANCE // Low-level statechart model factory protected final extension StatechartModelFactory factory = StatechartModelFactory.eINSTANCE protected final extension ExpressionModelFactory constraintFactory = ExpressionModelFactory.eINSTANCE @@ -541,12 +543,16 @@ class StatechartToLowlevelTransformer { statechartUtil.addCoordinationVariableAnnotation(scheduledCtrlVar) statechart.variableDeclarations += scheduledCtrlVar + // Transforming UnorderedCoordinationTransitions to SequentialCoordinationTransitions, + // Generating all possible permutations + for (transition : statechart.coordinationTransitions.clone.filter[it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression ]) { + transition.transformCoordinationTransition(scheduledComponentEnum) + } // Transforming CoordinationTransitions to regular transitions, possibly creating VariableDeclarations and States - for (transition : statechart.coordinationTransitions) { + for (transition : statechart.coordinationTransitions.filter[!(it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression)]) { transition.transformCoordinationTransition(scheduledComponentEnum) } - // Constants val gammaPackage = statechart.containingPackage for (constantDeclaration : gammaPackage.selfAndImports // During code generation, imported constants can be referenced @@ -567,7 +573,8 @@ class StatechartToLowlevelTransformer { val lowlevelTimeoutDeclaration = timeoutDeclaration.transform lowlevelStatechart.variableDeclarations += lowlevelTimeoutDeclaration lowlevelStatechart.timeoutDeclarations += lowlevelTimeoutDeclaration - } + } + for (port : statechart.ports) { // Both in and out events are transformed to a boolean VarDecl with additional parameters for (eventDeclaration : port.allEventDeclarations) { @@ -609,16 +616,16 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.invariants += statechartInvariants.map[it.transformSimpleExpression] } - // TODO remove return lowlevelStatechart } - protected def transformCoordinationTransition( - CoordinationTransition coordinationTransition, EnumerationTypeDefinition scheduledComponentEnum - ) { + protected def void transformCoordinationTransition(CoordinationTransition coordinationTransition, + EnumerationTypeDefinition scheduledComponentEnum) { + var gammaSource = coordinationTransition.sourceState val sourceName = gammaSource.name val containingStatechart = gammaSource.containingStatechart + val containingCoordinationStatechart = gammaSource.containingStatechart as CoordinationStatechartDefinition val region = gammaSource.getParentRegion val gammaTarget = coordinationTransition.targetState @@ -641,7 +648,9 @@ class StatechartToLowlevelTransformer { containingStatechart.transitions += internalTransition } else { - val internalState = statechartUtil.createState(region, sourceName + "_" + i++) + val internalState = statechartUtil.createState(region, + sourceName + "_" + i++ + "_" + containingCoordinationStatechart.coordinationTransitions.indexOf(coordinationTransition) + ) if (gammaTarget instanceof State) { internalState.invariants += gammaTarget.invariants.clone internalState.entryActions += gammaTarget.entryActions.clone @@ -661,8 +670,19 @@ class StatechartToLowlevelTransformer { } } } - } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression) { -// val unordComponentEnum = createEnumerationTypeDefinition + } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression && true) { + + val permutations = coordinationTransition.coordinatedComponent.instances.allPermutations + + for (permutation : permutations) { + val sequentialTransition = statechartUtil.createSequentialCoordinationTransition(gammaSource, gammaTarget, permutation); + sequentialTransition.trigger = coordinationTransition.trigger.clone + sequentialTransition.guard = coordinationTransition.guard.clone + sequentialTransition.effects += coordinationTransition.effects.clone + } + + } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression && false) { + val unordName = "unord_" + gammaSource.name + gammaTarget.name val unordBoolVariables = newHashMap @@ -676,24 +696,13 @@ class StatechartToLowlevelTransformer { */ for (componentInstanceReference : coordinationTransition.coordinatedComponent.instances) { -// val componentLiteral = createEnumerationLiteralDefinition -// componentLiteral.name = componentInstanceReference.componentInstance.name -// unordComponentEnum.literals += componentLiteral - unordBoolVariables += componentInstanceReference.componentInstance -> createVariableDeclarationWithDefaultInitialValue(createBooleanTypeDefinition, unordName + "_" + componentInstanceReference.componentInstance.name) } -// val unordComponentsTypeDeclaration = unordComponentEnum.createTypeDeclaration(unordName) -// containingStatechart.typeDeclarations += unordComponentsTypeDeclaration -// -// val unordComponentsTypeReference = createTypeReference(unordComponentsTypeDeclaration) - // TODO add ctrl var annotation -// val unordComponentsVariableDecl = createVariableDeclaration(unordComponentsTypeReference, unordName) -// containingStatechart.variableDeclarations += unordComponentsVariableDecl containingStatechart.variableDeclarations += unordBoolVariables.values /* XSTS: @@ -722,26 +731,31 @@ class StatechartToLowlevelTransformer { * } * } */ - + // creating new transition sourceState->sourceState for every componentInstance - -// if (gammaSource instanceof State) { -// gammaSource.entryActions += createHavocStatement => [ -// it.lhs = unordComponentsVariableDecl.createReferenceExpression -// ] -// } for (componentInstanceReference : coordinationTransition.coordinatedComponent.instances) { val componentName = componentInstanceReference.componentInstance.name val internalTransition = statechartUtil.createTransition(gammaSource, gammaSource) - internalTransition.trigger = coordinationTransition.trigger.clone + + // if the trigger is a timeout event, then create an invariant and on onCycleTrigger + if (coordinationTransition.trigger.containsType(TimeoutEventReference)) { + val timeout = coordinationTransition.trigger.getFirstOfAllContentsOfType(TimeoutEventReference).timeout + if (gammaSource instanceof State) { + gammaSource.invariants += createGreaterEqualExpression( + statechartUtil.createTimeoutReferenceExpression(timeout), + timeout.valueOfTimeout + ) + } + internalTransition.trigger = statechartUtil.createOnCycleTrigger + } else { + internalTransition.trigger = coordinationTransition.trigger.clone + } + internalTransition.guard = createAndExpression => [ if (coordinationTransition.guard !== null) { it.operands += coordinationTransition.guard.clone } -// it.operands += -// createEqualityExpression(unordComponentsVariableDecl, -// createEnumerationLiteralExpression(unordComponentEnum, componentName)) it.operands += createEqualityExpression(unordBoolVariables.get(componentInstanceReference.componentInstance), createFalseExpression) @@ -787,4 +801,5 @@ class StatechartToLowlevelTransformer { } } + } \ No newline at end of file From 129cd680af23279a5afb20e5e89a1fcd4995aae3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 17:17:19 +0100 Subject: [PATCH 18/27] Introduced delay action to xsts model --- plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore | 1 + .../xsts/hu.bme.mit.gamma.xsts.model/model/model.genmodel | 1 + .../xsts/transformation/serializer/ActionSerializer.xtend | 6 +++++- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore index 66ca856a5..1d4b9e220 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore @@ -147,4 +147,5 @@ eSuperTypes="../../hu.bme.mit.gamma.expression.model/model/expression.ecore#//VariableDeclarationAnnotation"/> + diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.genmodel b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.genmodel index 54b508b28..ef6942315 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.genmodel +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.genmodel @@ -107,5 +107,6 @@ + diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend index 7f7a0a0f8..56e644676 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend @@ -25,6 +25,7 @@ import hu.bme.mit.gamma.xsts.model.XSTS import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* +import hu.bme.mit.gamma.xsts.model.DelayAction class ActionSerializer { // Singleton @@ -50,7 +51,6 @@ class ActionSerializer { «xSts.initializingAction.serialize» } env { - «IF xSts.timed && !xSts.coordinationVariables.empty»__delay;«ENDIF» «xSts.environmentalAction.serialize» } ''' @@ -120,4 +120,8 @@ class ActionSerializer { ««« } ''' + def dispatch String serialize(DelayAction action) ''' + __delay; + ''' + } \ No newline at end of file From d5a5ba290ee09649b393b2fda407060d8cee7e4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 17:18:13 +0100 Subject: [PATCH 19/27] Added delay actions to coordination automata env --- .../gamma/xsts/transformation/ComponentTransformer.xtend | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index a101af778..cf6ff2710 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -1554,9 +1554,12 @@ class ComponentTransformer { bindingAssignments.removeNonDeterministicActionsReferencingAssignedVariables(oldInEventAction) val newInEventAction = createSequentialAction => [ - // TODO Add delay - + // Add delay -> new DelayAction -> transformed in GammaToXstsTransformer.setClockVariables + val delayAction = xStsModelFactory.createDelayAction + delayAction.lhs = xSts.clockVariables.get(0).createReferenceExpression + it.actions += delayAction it.actions += newCoordinationInEventAction + it.actions += delayAction.clone it.actions += oldInEventAction // Bind together ports connected to the same system port it.actions += bindingAssignments From 1cc291413a7a48d94d8c86a4a9958fac8c816176 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Fri, 30 Jan 2026 17:19:25 +0100 Subject: [PATCH 20/27] Added handling of delay actions to the clock handling of GammaToXstsTransformer --- .../xsts/transformation/GammaToXstsTransformer.xtend | 9 +++++++++ 1 file changed, 9 insertions(+) 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 22ca5b63a..b3e02b54c 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 @@ -52,6 +52,8 @@ import static hu.bme.mit.gamma.xsts.transformation.util.Namings.* import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* +import hu.bme.mit.gamma.xsts.model.DelayAction +import hu.bme.mit.gamma.xsts.model.SequentialAction class GammaToXstsTransformer { // This gammaToLowlevelTransformer must be the same during this transformation cycle due to tracing @@ -239,6 +241,13 @@ class GammaToXstsTransformer { // Denoting variable as scheduled clock variable xStsClockVariable.addScheduledClockAnnotation } + + if (xSts.inEventTransition.action instanceof SequentialAction) { + for (delayAction : (xSts.inEventTransition.action as SequentialAction).actions.filter[it instanceof DelayAction]) { + xStsClockSettingAction.clone.replace(delayAction) + } + } + // Putting it in merged transition as it does not work in environment action xStsClockSettingAction.actions += xSts.mergedAction From 2a12fefc3ec378e4b485e988bad03b98a8d42e62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Mon, 2 Feb 2026 12:25:50 +0100 Subject: [PATCH 21/27] Commit changes --- plugins/xsts/hu.bme.mit.gamma.xsts.model/META-INF/MANIFEST.MF | 3 ++- .../xsts/transformation/serializer/ActionSerializer.xtend | 1 - 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/META-INF/MANIFEST.MF b/plugins/xsts/hu.bme.mit.gamma.xsts.model/META-INF/MANIFEST.MF index f05222b02..3595adc08 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/META-INF/MANIFEST.MF +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/META-INF/MANIFEST.MF @@ -6,7 +6,8 @@ Bundle-Version: 2.11.0.qualifier Bundle-ClassPath: . Require-Bundle: org.eclipse.core.runtime, org.eclipse.emf.ecore;visibility:=reexport, - hu.bme.mit.gamma.expression.model;visibility:=reexport + hu.bme.mit.gamma.expression.model;visibility:=reexport, + hu.bme.mit.gamma.statechart.model Bundle-ActivationPolicy: lazy Bundle-Vendor: BME-FTSRG Bundle-Localization: plugin diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend index 56e644676..4d4b94fec 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend @@ -39,7 +39,6 @@ class ActionSerializer { return xSts.serializeXsts(false) } - // TODO how to handle the env in non timed case? def String serializeXsts(XSTS xSts, boolean serializePrimedVariables) ''' «xSts.serializeDeclarations(serializePrimedVariables)» From def3db88f5e54aadba2101002785918ddd306afb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Wed, 4 Feb 2026 16:54:02 +0100 Subject: [PATCH 22/27] Fixed minor mistake --- .../transformation/StatechartToLowlevelTransformer.xtend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index efa7d702d..99f2b0319 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -649,7 +649,7 @@ class StatechartToLowlevelTransformer { containingStatechart.transitions += internalTransition } else { val internalState = statechartUtil.createState(region, - sourceName + "_" + i++ + "_" + containingCoordinationStatechart.coordinationTransitions.indexOf(coordinationTransition) + sourceName + "_" + i + "_" + containingCoordinationStatechart.coordinationTransitions.indexOf(coordinationTransition) ) if (gammaTarget instanceof State) { internalState.invariants += gammaTarget.invariants.clone From 069493202118752b07e7acf89ad9856afec26737 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Wed, 4 Feb 2026 16:54:43 +0100 Subject: [PATCH 23/27] Added test models for coordination automaton --- .../Coordination/Interfaces/Interfaces.gcd | 5 ++ .../Coordination/Statechart/Statechart.gcd | 26 ++++++++ .../System/Coordination-nondet.gcd | 43 +++++++++++++ .../Coordination/System/Coordination-seq.gcd | 42 +++++++++++++ .../System/Coordination-unord.gcd | 42 +++++++++++++ .../model/Coordination/System/Generation.ggen | 63 +++++++++++++++++++ 6 files changed, 221 insertions(+) create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/Interfaces/Interfaces.gcd create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/Statechart/Statechart.gcd create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-nondet.gcd create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-seq.gcd create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-unord.gcd create mode 100644 tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/Interfaces/Interfaces.gcd b/tests/hu.bme.mit.gamma.tests/model/Coordination/Interfaces/Interfaces.gcd new file mode 100644 index 000000000..7e1024f6c --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/Interfaces/Interfaces.gcd @@ -0,0 +1,5 @@ +package coordination_tests + +interface SimpleInterface { + out event simpleEvent +} diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/Statechart/Statechart.gcd b/tests/hu.bme.mit.gamma.tests/model/Coordination/Statechart/Statechart.gcd new file mode 100644 index 000000000..cecfea75a --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/Statechart/Statechart.gcd @@ -0,0 +1,26 @@ +package coordination_tests +// import interfaces_package + +import "Interfaces/Interfaces.gcd" + +statechart SimpleStatechart ( + // Declaration of parameters +) [ + // Declaration of ports + port inPort : requires SimpleInterface + port outPort : provides SimpleInterface +] { + // Definition of states, regions and transitions + timeout c1 + + + region main_region_1 { + initial init_1 + state state_1 { + entry / set c1 := 5 s; + } + } + transition from init_1 to state_1 + transition from state_1 to state_1 when inPort.simpleEvent + transition from state_1 to state_1 when timeout c1 / raise outPort.simpleEvent; +} diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-nondet.gcd b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-nondet.gcd new file mode 100644 index 000000000..3c062a1fd --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-nondet.gcd @@ -0,0 +1,43 @@ +package coordination_tests + +import "Interfaces/Interfaces.gcd" +import "Statechart/Statechart.gcd" + +@Coordination +coordination-statechart CoordinationNondet ( + // parameters +) [ + // system ports + port SystemIn1 : requires SimpleInterface + port SystemIn2 : requires SimpleInterface + port SystemOut1 : provides SimpleInterface + port SystemOut2 : provides SimpleInterface +] { + // system composition + component Component1 : SimpleStatechart + component Component2 : SimpleStatechart + + bind SystemIn1 -> Component1.inPort + bind SystemIn2 -> Component2.inPort + bind SystemOut1 -> Component1.outPort + bind SystemOut2 -> Component2.outPort +} < + // system coordination + timeout c1 + + region main { + initial init + state q0 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + state q1 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + } + + transition from init to q0 + transition from q0 to q1 when timeout c1 execute Component1 + transition from q0 to q1 when timeout c1 execute Component2 +> \ No newline at end of file diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-seq.gcd b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-seq.gcd new file mode 100644 index 000000000..a4e1b504f --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-seq.gcd @@ -0,0 +1,42 @@ +package coordination_tests + +import "Interfaces/Interfaces.gcd" +import "Statechart/Statechart.gcd" + +@Coordination +coordination-statechart CoordinationSeq ( + // parameters +) [ + // system ports + port SystemIn1 : requires SimpleInterface + port SystemIn2 : requires SimpleInterface + port SystemOut1 : provides SimpleInterface + port SystemOut2 : provides SimpleInterface +] { + // system composition + component Component1 : SimpleStatechart + component Component2 : SimpleStatechart + + bind SystemIn1 -> Component1.inPort + bind SystemIn2 -> Component2.inPort + bind SystemOut1 -> Component1.outPort + bind SystemOut2 -> Component2.outPort +} < + // system coordination + timeout c1 + + region main { + initial init + state q0 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + state q1 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + } + + transition from init to q0 + transition from q0 to q1 when timeout c1 execute seq{Component1, Component2} +> \ No newline at end of file diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-unord.gcd b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-unord.gcd new file mode 100644 index 000000000..47224bdd2 --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Coordination-unord.gcd @@ -0,0 +1,42 @@ +package coordination_tests + +import "Interfaces/Interfaces.gcd" +import "Statechart/Statechart.gcd" + +@Coordination +coordination-statechart CoordinationUnord ( + // parameters +) [ + // system ports + port SystemIn1 : requires SimpleInterface + port SystemIn2 : requires SimpleInterface + port SystemOut1 : provides SimpleInterface + port SystemOut2 : provides SimpleInterface +] { + // system composition + component Component1 : SimpleStatechart + component Component2 : SimpleStatechart + + bind SystemIn1 -> Component1.inPort + bind SystemIn2 -> Component2.inPort + bind SystemOut1 -> Component1.outPort + bind SystemOut2 -> Component2.outPort +} < + // system coordination + timeout c1 + + region main { + initial init + state q0 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + state q1 { + invariant (time-elapsed(c1) < 4) + entry / set c1 := 1 s; + } + } + + transition from init to q0 + transition from q0 to q1 when timeout c1 execute unord{Component1, Component2} +> \ No newline at end of file diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen new file mode 100644 index 000000000..cf68816fd --- /dev/null +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen @@ -0,0 +1,63 @@ +import "Coordination-nondet.gcd" +import "Coordination-seq.gcd" +import "Coordination-unord.gcd" + +//analysis { +// component : CoordinationNondet +// language : XSTS +// folder : "model-gen-coordination-timed" +// optimize : false +// state-coverage +//} +// +//analysis { +// component : CoordinationNondet +// language : XSTS +// folder : "model-gen-coordination" +// optimize : false +// state-coverage +// constraint : { +// minimum-orchestrating-period : 0 s +// maximum-orchestrating-period : 4 s +// } +//} + +analysis { + component : CoordinationSeq + language : XSTS + folder : "model-gen-coordination-timed" + optimize : false + state-coverage +} + +analysis { + component : CoordinationSeq + language : XSTS + folder : "model-gen-coordination" + optimize : false + state-coverage + constraint : { + minimum-orchestrating-period : 0 s + maximum-orchestrating-period : 4 s + } +} + +analysis { + component : CoordinationUnord + language : XSTS + folder : "model-gen-coordination-timed" + optimize : false + state-coverage +} + +analysis { + component : CoordinationUnord + language : XSTS + folder : "model-gen-coordination" + optimize : false + state-coverage + constraint : { + minimum-orchestrating-period : 0 s + maximum-orchestrating-period : 4 s + } +} \ No newline at end of file From 59e2e51f82c88d224e3f78faf156d45524c8c81b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 10 Feb 2026 19:51:56 +0100 Subject: [PATCH 24/27] Addressed several comments --- .../gamma/expression/util/ExpressionUtil.java | 6 ++- .../language/StatechartLanguage.xtext | 3 +- .../StatechartLanguageScopeProvider.java | 13 ----- .../StatechartModelDerivedFeatures.java | 28 ++++++----- .../gamma/statechart/util/StatechartUtil.java | 32 +++++++------ .../util/preprocessor/ModelUnfolder.xtend | 4 +- .../util/reducer/SystemReducer.xtend | 4 +- .../plantuml/commandhandler/TextProvider.java | 6 +-- .../CoordinationToPlantUmlTransformer.xtend | 15 +++--- .../GammaToLowlevelTransformer.xtend | 3 +- .../StatechartToLowlevelTransformer.xtend | 48 ++++++++++--------- .../serializer/ActionSerializer.xtend | 2 +- .../GammaToXstsTransformer.xtend | 9 ++-- .../model/Coordination/System/Generation.ggen | 38 +++++++-------- 14 files changed, 104 insertions(+), 107 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java b/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java index b6e89bfc6..e4a41c000 100644 --- a/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java +++ b/plugins/core/hu.bme.mit.gamma.expression.model/src/hu/bme/mit/gamma/expression/util/ExpressionUtil.java @@ -689,7 +689,8 @@ public Set getReferredValues(Expression expression) { public EnumerationLiteralDefinition getEnumerationLiteralDefinitionByName(EnumerationTypeDefinition typeDefinition, String name) { for (EnumerationLiteralDefinition literal : typeDefinition.getLiterals()) { - if (literal.getName().equals(name)) { + String enumLiteralName = literal.getName(); + if (enumLiteralName.equals(name)) { return literal; } } @@ -1710,7 +1711,8 @@ public EnumerationLiteralExpression createEnumerationLiteralExpression( public EnumerationLiteralExpression createEnumerationLiteralExpression( EnumerationTypeDefinition typeDefinition, String name) { - return createEnumerationLiteralExpression(getEnumerationLiteralDefinitionByName(typeDefinition, name)); + EnumerationLiteralDefinition enumLiteralDefinition = getEnumerationLiteralDefinitionByName(typeDefinition, name); + return createEnumerationLiteralExpression(enumLiteralDefinition); } public SubtractExpression createSubtractExpression(Expression lhs, Expression rhs) { diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext index c4ebbd5bc..ef51a8de2 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/StatechartLanguage.xtext @@ -826,7 +826,8 @@ AbstractCoordinationReferenceExpression returns AbstractCoordinationReferenceExp ; SequentialCoordinationReferenceExpression returns SequentialCoordinationReferenceExpression: - 'seq' '{' instances+=ComponentInstanceReferenceExpression((',') instances+=ComponentInstanceReferenceExpression)* '}' | instances+=ComponentInstanceReferenceExpression + 'seq' '{' instances+=ComponentInstanceReferenceExpression ((',') instances+=ComponentInstanceReferenceExpression)* '}' + | instances+=ComponentInstanceReferenceExpression ; UnorderedCoordinationReferenceExpression returns UnorderedCoordinationReferenceExpression: diff --git a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java index d8c473a32..409778081 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.language/src/hu/bme/mit/gamma/statechart/language/scoping/StatechartLanguageScopeProvider.java @@ -74,7 +74,6 @@ import hu.bme.mit.gamma.statechart.phase.PhaseModelPackage; import hu.bme.mit.gamma.statechart.statechart.AnyPortEventReference; import hu.bme.mit.gamma.statechart.statechart.CompositeElement; -import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition; import hu.bme.mit.gamma.statechart.statechart.PortEventReference; import hu.bme.mit.gamma.statechart.statechart.RaiseEventAction; import hu.bme.mit.gamma.statechart.statechart.Region; @@ -372,18 +371,6 @@ public IScope getScope(final EObject context, final EReference reference) { } return scope; } -// if (ecoreUtil.hasContainerOfType(context, CoordinationStatechartDefinition.class)) { -// CoordinationStatechartDefinition parent = ecoreUtil.getSelfOrContainerOfType(context, CoordinationStatechartDefinition.class); -// ComponentInstance component = parent.getCoordinatedComponent(); -// if (component instanceof AsynchronousComponentInstance) { -// return handleTypeDeclarationAndComponentInstanceElementReferences(context, reference, null, ((AsynchronousComponentInstance)component).getType()); -// } -// if (component instanceof SynchronousComponentInstance) { -// return handleTypeDeclarationAndComponentInstanceElementReferences(context, reference, null, ((SynchronousComponentInstance)component).getType()); -// } -// return null; -// } - // } catch (NullPointerException e) { // Nullptr exception is thrown if the scope turns out to be empty // This can be due to modeling error of the user, e.g., there are no in events on the specified ports diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java index 353cc2ef0..b2b48fdaa 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java @@ -1960,7 +1960,10 @@ public static List getAllBoundSimplePorts(Component component) { public static List getAllBoundSimplePorts(Port port) { List simplePorts = new ArrayList(); Component component = getContainingComponent(port); - if (component instanceof CompositeComponent composite) { + if (component instanceof StatechartDefinition) { + simplePorts.add(port); + } + else if (component instanceof CompositeComponent composite) { for (PortBinding portBinding : composite.getPortBindings()) { if (portBinding.getCompositeSystemPort() == port) { // Makes sense only if the containment hierarchy is a tree structure @@ -1971,9 +1974,6 @@ public static List getAllBoundSimplePorts(Port port) { } } } - else if (component instanceof StatechartDefinition) { - simplePorts.add(port); - } // Note that one port can be in the list multiple times iff the component is NOT unfolded return simplePorts; } @@ -2473,10 +2473,10 @@ public static List getSiblingTransitions(Transition transition) { public static List getOutgoingTransitions(StateNode node) { StatechartDefinition statechart = getContainingStatechart(node); - if (statechart instanceof CoordinationStatechartDefinition) { + if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) { // TODO CoordinationStatechart Validation - return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream().filter(it -> it.getSourceState() == node) - .collect(Collectors.toList()); + return coordinationStatechart.getCoordinationTransitions().stream() + .filter(it -> it.getSourceState() == node).collect(Collectors.toList()); } return statechart.getTransitions().stream().filter(it -> it.getSourceState() == node) .collect(Collectors.toList()); @@ -2525,10 +2525,10 @@ public static List getOutgoingTransitionsUntilState(StateNode node) public static List getIncomingTransitions(StateNode node) { StatechartDefinition statechart = getContainingStatechart(node); - if (statechart instanceof CoordinationStatechartDefinition) { + if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) { // TODO CoordinationStatechart Validation - return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream().filter(it -> it.getTargetState() == node) - .collect(Collectors.toList()); + return coordinationStatechart.getCoordinationTransitions().stream() + .filter(it -> it.getTargetState() == node).collect(Collectors.toList()); } return statechart.getTransitions().stream().filter(it -> it.getTargetState() == node) @@ -2539,9 +2539,9 @@ public static List getAllIncomingTransitions(StateNode node) { List allStateNodes = ecoreUtil .getSelfAndAllContentsOfType(node, StateNode.class); StatechartDefinition statechart = getContainingStatechart(node); - if (statechart instanceof CoordinationStatechartDefinition) { + if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) { // TODO CoordinationStatechart Validation - return ((CoordinationStatechartDefinition) statechart).getCoordinationTransitions().stream() + return coordinationStatechart.getCoordinationTransitions().stream() .filter(it -> allStateNodes.contains(it.getTargetState())) .collect(Collectors.toList()); } @@ -4048,4 +4048,8 @@ public static List getCoordinationVariables(StatechartDefin CoordinationVariableDeclarationAnnotation.class); } + public static boolean isCoordinationStatechart(StatechartDefinition statechart) { + return statechart instanceof CoordinationStatechartDefinition; + } + } \ No newline at end of file diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java index 39e2f0077..5bb4a84c9 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/util/StatechartUtil.java @@ -14,7 +14,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.HashSet; -import java.util.Iterator; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -96,6 +95,7 @@ import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition; import hu.bme.mit.gamma.statechart.statechart.EntryState; import hu.bme.mit.gamma.statechart.statechart.InitialState; +import hu.bme.mit.gamma.statechart.statechart.OnCycleTrigger; import hu.bme.mit.gamma.statechart.statechart.PortEventReference; import hu.bme.mit.gamma.statechart.statechart.RaiseEventAction; import hu.bme.mit.gamma.statechart.statechart.Region; @@ -448,7 +448,7 @@ public UnaryTrigger createUnaryTrigger(Trigger trigger, UnaryType type) { return unaryTrigger; } - public Trigger createOnCycleTrigger() { + public OnCycleTrigger createOnCycleTrigger() { return statechartFactory.createOnCycleTrigger(); } @@ -1349,33 +1349,37 @@ public void addCoordinationVariableAnnotation(VariableDeclaration variable) { addAnnotation(variable, statechartFactory.createCoordinationVariableDeclarationAnnotation()); } - public CoordinationTransition createSequentialCoordinationTransition(StateNode source, StateNode target, List coordinatedComponents) { + public CoordinationTransition createSequentialCoordinationTransition(StateNode source, StateNode target, + List coordinatedComponents) { CoordinationTransition transition = statechartFactory.createCoordinationTransition(); transition.setSourceState(source); transition.setTargetState(target); - SequentialCoordinationReferenceExpression expression = statechartFactory.createSequentialCoordinationReferenceExpression(); + SequentialCoordinationReferenceExpression expression = statechartFactory + .createSequentialCoordinationReferenceExpression(); expression.getInstances().addAll(ecoreUtil.clone(coordinatedComponents)); - + transition.setCoordinatedComponent(expression); - - CoordinationStatechartDefinition statechart = - (CoordinationStatechartDefinition) StatechartModelDerivedFeatures.getContainingStatechart(source); + + CoordinationStatechartDefinition statechart = (CoordinationStatechartDefinition) StatechartModelDerivedFeatures + .getContainingStatechart(source); if (statechart != null) { statechart.getCoordinationTransitions().add(transition); } return transition; } - - public CoordinationTransition createUnorderedCoordinationTransition(StateNode source, StateNode target, List coordinatedComponents) { + + public CoordinationTransition createUnorderedCoordinationTransition(StateNode source, StateNode target, + List coordinatedComponents) { CoordinationTransition transition = statechartFactory.createCoordinationTransition(); transition.setSourceState(source); transition.setTargetState(target); - UnorderedCoordinationReferenceExpression expression = statechartFactory.createUnorderedCoordinationReferenceExpression(); + UnorderedCoordinationReferenceExpression expression = statechartFactory + .createUnorderedCoordinationReferenceExpression(); expression.getInstances().addAll(coordinatedComponents); transition.setCoordinatedComponent(expression); - - CoordinationStatechartDefinition statechart = - (CoordinationStatechartDefinition) StatechartModelDerivedFeatures.getContainingStatechart(source); + + CoordinationStatechartDefinition statechart = (CoordinationStatechartDefinition) StatechartModelDerivedFeatures + .getContainingStatechart(source); if (statechart != null) { statechart.getCoordinationTransitions().add(transition); } diff --git a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend index baa4ec2aa..cba29c746 100644 --- a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend +++ b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/preprocessor/ModelUnfolder.xtend @@ -25,6 +25,7 @@ import hu.bme.mit.gamma.statechart.interface_.EventTrigger import hu.bme.mit.gamma.statechart.interface_.InterfaceModelFactory import hu.bme.mit.gamma.statechart.interface_.Package import hu.bme.mit.gamma.statechart.statechart.AnyPortEventReference +import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.AsynchronousStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.ClockTickReference import hu.bme.mit.gamma.statechart.statechart.PortEventReference @@ -32,6 +33,7 @@ import hu.bme.mit.gamma.statechart.statechart.RunUponExternalEventAnnotation import hu.bme.mit.gamma.statechart.statechart.RunUponExternalEventOrInternalTimeoutAnnotation import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition import hu.bme.mit.gamma.statechart.statechart.StatechartModelFactory +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.util.StatechartUtil import hu.bme.mit.gamma.util.GammaEcoreUtil import hu.bme.mit.gamma.util.JavaUtil @@ -44,8 +46,6 @@ import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.transformation.util.Namings.* -import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition -import hu.bme.mit.gamma.statechart.statechart.AsynchronousCoordinationStatechartDefinition class ModelUnfolder { diff --git a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend index ac2192f16..f89cee7b5 100644 --- a/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend +++ b/plugins/core/hu.bme.mit.gamma.transformation.util/src/hu/bme/mit/gamma/transformation/util/reducer/SystemReducer.xtend @@ -20,6 +20,7 @@ import hu.bme.mit.gamma.statechart.composite.SimpleChannel import hu.bme.mit.gamma.statechart.composite.SynchronousComponentInstance import hu.bme.mit.gamma.statechart.composite.SynchronousCompositeComponent import hu.bme.mit.gamma.statechart.interface_.Package +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition import hu.bme.mit.gamma.statechart.statechart.EntryState import hu.bme.mit.gamma.statechart.statechart.GuardEvaluation import hu.bme.mit.gamma.statechart.statechart.OrthogonalRegionSchedulingOrder @@ -48,7 +49,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import static extension hu.bme.mit.gamma.action.derivedfeatures.ActionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* -import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition class SystemReducer implements Reducer { @@ -103,7 +103,7 @@ class SystemReducer implements Reducer { // Statechart optimizing for (statechart : statecharts) { // TODO note: a coordination automaton is not a simple instance we have to handle this somewhere! - if ((statechart.regions.empty || !simpleInstancesMatcher.hasMatch(null, statechart)) && !(statechart instanceof CoordinationStatechartDefinition)) { + if ((statechart.regions.empty || !simpleInstancesMatcher.hasMatch(null, statechart)) && !(statechart.isCoordinationStatechart)) { statechart.regions.clear statechart.variableDeclarations.clear statechart.timeoutDeclarations.clear diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java index 6bfdbcf4b..6c620f273 100644 --- a/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.textprovider/src/hu/bme/mit/gamma/plantuml/commandhandler/TextProvider.java @@ -127,17 +127,15 @@ private String getComponentPlantUmlCode(Resource resource) { List interfaces = _package.getInterfaces(); if (!components.isEmpty()) { Component component = components.get(0); - if (component instanceof CoordinationStatechartDefinition) { + if (component instanceof CoordinationStatechartDefinition statechartDefinition) { ICommandService commandService = PlatformUI.getWorkbench().getService(ICommandService.class); Command command = commandService.getCommand("hu.bme.mit.gamma.plantuml.coordinationLayoutCommand"); String state = (String)command.getState(RadioState.STATE_ID).getValue(); - CoordinationStatechartDefinition statechartDefinition = (CoordinationStatechartDefinition) component; CoordinationToPlantUmlTransformer transformer = new CoordinationToPlantUmlTransformer( statechartDefinition, state); return transformer.execute(); - } else if (component instanceof StatechartDefinition) { - StatechartDefinition statechartDefinition = (StatechartDefinition) component; + } else if (component instanceof StatechartDefinition statechartDefinition) { StatechartToPlantUmlTransformer transformer = new StatechartToPlantUmlTransformer( statechartDefinition); return transformer.execute(); diff --git a/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend b/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend index 17c800f8c..25ff2e950 100644 --- a/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend +++ b/plugins/vis/hu.bme.mit.gamma.plantuml.transformation/src/hu/bme/mit/gamma/plantuml/transformation/CoordinationToPlantUmlTransformer.xtend @@ -1,17 +1,16 @@ package hu.bme.mit.gamma.plantuml.transformation +import hu.bme.mit.gamma.statechart.statechart.AbstractCoordinationReferenceExpression import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition -import hu.bme.mit.gamma.statechart.statechart.PseudoState -import hu.bme.mit.gamma.statechart.statechart.State -import hu.bme.mit.gamma.statechart.composite.CompositeComponent import hu.bme.mit.gamma.statechart.statechart.CoordinationTransition import hu.bme.mit.gamma.statechart.statechart.EntryState - -import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* -import hu.bme.mit.gamma.statechart.statechart.AbstractCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.statechart.PseudoState import hu.bme.mit.gamma.statechart.statechart.SequentialCoordinationReferenceExpression +import hu.bme.mit.gamma.statechart.statechart.State import hu.bme.mit.gamma.statechart.statechart.UnorderedCoordinationReferenceExpression +import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* + class CoordinationToPlantUmlTransformer extends StatechartToPlantUmlTransformer { protected final CoordinationStatechartDefinition statechart @@ -28,14 +27,14 @@ class CoordinationToPlantUmlTransformer extends StatechartToPlantUmlTransformer new(CoordinationStatechartDefinition statechart) { super(statechart) this.statechart = statechart - this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart as CompositeComponent) + this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart) this.layoutType = CoordinationLayoutType.COORDINATION } new(CoordinationStatechartDefinition statechart, String layoutType) { super(statechart) this.statechart = statechart - this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart as CompositeComponent) + this.compositeTransformer = new CompositeToPlantUmlTransformer(statechart) this.layoutType = CoordinationLayoutType.valueOf(layoutType) } diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend index 876b8c962..e26e47bba 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/GammaToLowlevelTransformer.xtend @@ -13,12 +13,11 @@ package hu.bme.mit.gamma.statechart.lowlevel.transformation import hu.bme.mit.gamma.statechart.interface_.TimeUnit import hu.bme.mit.gamma.statechart.lowlevel.model.Package import hu.bme.mit.gamma.statechart.statechart.StatechartDefinition +import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition import static com.google.common.base.Preconditions.checkState import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* -import hu.bme.mit.gamma.statechart.statechart.SynchronousCoordinationStatechartDefinition -import hu.bme.mit.gamma.expression.model.VariableDeclaration class GammaToLowlevelTransformer { diff --git a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend index 99f2b0319..fe6c5f98c 100644 --- a/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.statechart.lowlevel.transformation/src/hu/bme/mit/gamma/statechart/lowlevel/transformation/StatechartToLowlevelTransformer.xtend @@ -79,7 +79,7 @@ class StatechartToLowlevelTransformer { protected final extension ActionModelFactory actionFactory = ActionModelFactory.eINSTANCE // Trace object for storing the mappings protected final Trace trace - //Coordination Automata + // Coordination automata protected VariableDeclaration scheduledCtrlVar new() { @@ -495,11 +495,10 @@ class StatechartToLowlevelTransformer { it.guardEvaluation = statechart.guardEvaluation.transform it.orthogonalRegionSchedulingOrder = statechart.orthogonalRegionSchedulingOrder.transform ] - if (!statechart.hasOrthogonalRegions) { + if (!statechart.hasOrthogonalRegions) { // If there are no orthogonal regions, then the guard evaluation policy is irrelevant; // on the fly is the faster option, though - lowlevelStatechart.guardEvaluation = - hu.bme.mit.gamma.statechart.lowlevel.model.GuardEvaluation.ON_THE_FLY + lowlevelStatechart.guardEvaluation = hu.bme.mit.gamma.statechart.lowlevel.model.GuardEvaluation.ON_THE_FLY } if (statechart.hasAnnotation(RunUponExternalEventAnnotation)) { lowlevelStatechart.addRunUponExternalEventAnnotation @@ -508,15 +507,14 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.addRunUponExternalEventOrInternalTimeoutAnnotation } trace.put(statechart, lowlevelStatechart) // Saving in trace - // create scheduled control variable for each subcomponent val scheduledComponentEnum = createEnumerationTypeDefinition - + // create default value, when no component is scheduled val noComponentLiteral = createEnumerationLiteralDefinition noComponentLiteral.name = "__nothing__" scheduledComponentEnum.literals += noComponentLiteral - + // TODO is differentiation between SynchronousCoordinationStatechartDefinition and AsynchronousCoordinationStatechartDefinition necessary? if (statechart.synchronous) { for (subcomponent : (statechart as SynchronousCoordinationStatechartDefinition).components) { @@ -531,32 +529,37 @@ class StatechartToLowlevelTransformer { scheduledComponentEnum.literals += componentLiteral } } else { - throw new IllegalArgumentException("CoordinationStateChart: " + statechart.name + " is neither synchronous nor asynchronous!") + throw new IllegalArgumentException("CoordinationStateChart: " + statechart.name + + " is neither synchronous nor asynchronous!") } val schedulableComponentsTypeDeclaration = scheduledComponentEnum.createTypeDeclaration("schedulableComponents") statechart.typeDeclarations += schedulableComponentsTypeDeclaration - + val schedulableComponentsTypeReference = createTypeReference(schedulableComponentsTypeDeclaration) - + // TODO add ctrl var annotation scheduledCtrlVar = createVariableDeclaration(schedulableComponentsTypeReference, "scheduledComponent") statechartUtil.addCoordinationVariableAnnotation(scheduledCtrlVar) statechart.variableDeclarations += scheduledCtrlVar - + // Transforming UnorderedCoordinationTransitions to SequentialCoordinationTransitions, // Generating all possible permutations - for (transition : statechart.coordinationTransitions.clone.filter[it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression ]) { + for (transition : statechart.coordinationTransitions.clone.filter [ + it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression + ]) { transition.transformCoordinationTransition(scheduledComponentEnum) } // Transforming CoordinationTransitions to regular transitions, possibly creating VariableDeclarations and States - for (transition : statechart.coordinationTransitions.filter[!(it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression)]) { + for (transition : statechart.coordinationTransitions.filter [ + !(it.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression) + ]) { transition.transformCoordinationTransition(scheduledComponentEnum) } - + // Constants val gammaPackage = statechart.containingPackage for (constantDeclaration : gammaPackage.selfAndImports // During code generation, imported constants can be referenced - .map[it.constantDeclarations].flatten) { + .map[it.constantDeclarations].flatten) { lowlevelStatechart.variableDeclarations += constantDeclaration.transform } // No parameter declarations mapping @@ -573,8 +576,8 @@ class StatechartToLowlevelTransformer { val lowlevelTimeoutDeclaration = timeoutDeclaration.transform lowlevelStatechart.variableDeclarations += lowlevelTimeoutDeclaration lowlevelStatechart.timeoutDeclarations += lowlevelTimeoutDeclaration - } - + } + for (port : statechart.ports) { // Both in and out events are transformed to a boolean VarDecl with additional parameters for (eventDeclaration : port.allEventDeclarations) { @@ -589,14 +592,13 @@ class StatechartToLowlevelTransformer { for (region : statechart.regions) { lowlevelStatechart.regions += region.transform } - + for (transition : statechart.transitions) { // Prioritizing transitions is done here val lowlevelTransition = transition.transform lowlevelStatechart.transitions += lowlevelTransition } - - + // Mapping port and interface invariants (now, not before, because we want to refer to e.g., state nodes and variables) // First the interface invariants must be mapped to the ports realizing the interface for (port : statechart.ports) { @@ -609,13 +611,13 @@ class StatechartToLowlevelTransformer { lowlevelStatechart.environmentalInvariants += invariants.map[it.transformSimpleExpression] } } - + // Mapping statechart invariants val statechartInvariants = statechart.invariants if (!statechartInvariants.empty) { lowlevelStatechart.invariants += statechartInvariants.map[it.transformSimpleExpression] } - + return lowlevelStatechart } @@ -682,7 +684,7 @@ class StatechartToLowlevelTransformer { } } else if (coordinationTransition.coordinatedComponent instanceof UnorderedCoordinationReferenceExpression && false) { - + // TODO need some measurements which case is better val unordName = "unord_" + gammaSource.name + gammaTarget.name val unordBoolVariables = newHashMap diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend index 8f962210d..8991e91e3 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation.util/src/hu/bme/mit/gamma/xsts/transformation/serializer/ActionSerializer.xtend @@ -13,6 +13,7 @@ package hu.bme.mit.gamma.xsts.transformation.serializer import hu.bme.mit.gamma.expression.model.DirectReferenceExpression import hu.bme.mit.gamma.xsts.model.AssignmentAction import hu.bme.mit.gamma.xsts.model.AssumeAction +import hu.bme.mit.gamma.xsts.model.DelayAction import hu.bme.mit.gamma.xsts.model.EmptyAction import hu.bme.mit.gamma.xsts.model.FunctionCallAction import hu.bme.mit.gamma.xsts.model.HavocAction @@ -29,7 +30,6 @@ import hu.bme.mit.gamma.xsts.model.XSTS import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* -import hu.bme.mit.gamma.xsts.model.DelayAction class ActionSerializer { // Singleton 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 43bce1806..a218411de 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 @@ -31,6 +31,8 @@ import hu.bme.mit.gamma.statechart.interface_.SchedulingConstraintAnnotation import hu.bme.mit.gamma.statechart.lowlevel.transformation.GammaToLowlevelTransformer import hu.bme.mit.gamma.transformation.util.preprocessor.AnalysisModelPreprocessor import hu.bme.mit.gamma.util.GammaEcoreUtil +import hu.bme.mit.gamma.xsts.model.DelayAction +import hu.bme.mit.gamma.xsts.model.SequentialAction import hu.bme.mit.gamma.xsts.model.SystemInEventGroup import hu.bme.mit.gamma.xsts.model.SystemInEventParameterGroup import hu.bme.mit.gamma.xsts.model.SystemOutEventGroup @@ -52,8 +54,6 @@ import static hu.bme.mit.gamma.xsts.transformation.util.Namings.* import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* import static extension hu.bme.mit.gamma.xsts.derivedfeatures.XstsDerivedFeatures.* -import hu.bme.mit.gamma.xsts.model.DelayAction -import hu.bme.mit.gamma.xsts.model.SequentialAction class GammaToXstsTransformer { // This gammaToLowlevelTransformer must be the same during this transformation cycle due to tracing @@ -243,8 +243,9 @@ class GammaToXstsTransformer { xStsClockVariable.addScheduledClockAnnotation } - if (xSts.inEventTransition.action instanceof SequentialAction) { - for (delayAction : (xSts.inEventTransition.action as SequentialAction).actions.filter[it instanceof DelayAction]) { + val inAction = xSts.inEventTransition.action + if (inAction instanceof SequentialAction) { + for (delayAction : inAction.actions.filter[it instanceof DelayAction]) { xStsClockSettingAction.clone.replace(delayAction) } } diff --git a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen index cf68816fd..2bbaf3b58 100644 --- a/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen +++ b/tests/hu.bme.mit.gamma.tests/model/Coordination/System/Generation.ggen @@ -2,25 +2,25 @@ import "Coordination-nondet.gcd" import "Coordination-seq.gcd" import "Coordination-unord.gcd" -//analysis { -// component : CoordinationNondet -// language : XSTS -// folder : "model-gen-coordination-timed" -// optimize : false -// state-coverage -//} -// -//analysis { -// component : CoordinationNondet -// language : XSTS -// folder : "model-gen-coordination" -// optimize : false -// state-coverage -// constraint : { -// minimum-orchestrating-period : 0 s -// maximum-orchestrating-period : 4 s -// } -//} +analysis { + component : CoordinationNondet + language : XSTS + folder : "model-gen-coordination-timed" + optimize : false + state-coverage +} + +analysis { + component : CoordinationNondet + language : XSTS + folder : "model-gen-coordination" + optimize : false + state-coverage + constraint : { + minimum-orchestrating-period : 0 s + maximum-orchestrating-period : 4 s + } +} analysis { component : CoordinationSeq From e842b5c4103ec67115351f1bf5507e0f571326a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Tue, 10 Feb 2026 20:04:12 +0100 Subject: [PATCH 25/27] Changed superclass of DelayAction to AbstractUpdateAction --- plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore | 2 +- .../mit/gamma/xsts/transformation/ComponentTransformer.xtend | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore index ea5e25b8a..da3c8129c 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/model/model.ecore @@ -170,5 +170,5 @@ eSuperTypes="../../hu.bme.mit.gamma.expression.model/model/expression.ecore#//VariableDeclarationAnnotation"/> - + diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index 443c387b8..d840309f3 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -1560,7 +1560,6 @@ class ComponentTransformer { val newInEventAction = createSequentialAction => [ // Add delay -> new DelayAction -> transformed in GammaToXstsTransformer.setClockVariables val delayAction = xStsModelFactory.createDelayAction - delayAction.lhs = xSts.clockVariables.get(0).createReferenceExpression it.actions += delayAction it.actions += newCoordinationInEventAction it.actions += delayAction.clone From e25c819d48164dc05a6539efccdfe58db1b0c50e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Wed, 25 Feb 2026 11:49:30 +0100 Subject: [PATCH 26/27] Added resettig channel events to coordination automaton --- .../transformation/ComponentTransformer.xtend | 25 ++++++------------- 1 file changed, 8 insertions(+), 17 deletions(-) diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend index d840309f3..4b5ee176e 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.transformation/src/hu/bme/mit/gamma/xsts/transformation/ComponentTransformer.xtend @@ -1387,7 +1387,7 @@ class ComponentTransformer { def dispatch XSTS transform(SynchronousCoordinationStatechartDefinition component, Package lowlevelPackage) { val name = component.name logger.info( "Transforming Synchronous Coordination Statechart " + name) - // TODO + val xSts = name.createXsts val componentMergedActions = newHashMap // To handle multiple schedulings in CascadeCompositeComponents val components = component.components @@ -1432,10 +1432,7 @@ class ComponentTransformer { xSts.entryEventTransition = coordinationEntryAction.wrap component.components.add(coordinationInstance) - -// val coordinationActualComponentMergedAction = createSequentialAction => [ -// it.actions += coordinationXSts.mergedAction -// ] + // In and Out actions - using sequential actions to make sure they are composite actions // Methods reset... and delete... require this @@ -1452,13 +1449,7 @@ class ComponentTransformer { // 1) the Sync ort semantics: Resetting channel IN events AFTER schedule would result in a deadlock // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components // Note, System in and out events are reset in the env action - - // TODO - // Resetting OUT events BEFORE schedule -// val clonedNewOutEventAction = newOutEventAction.clone // Clone is important -// .resetEverythingExceptPersistentParameters(subcomponentType) -// actualComponentMergedAction.actions.add(0, clonedNewOutEventAction) // Putting the new action BEFORE - + // 3) Coordination automata semantics: following the the Casc semantics resetting IN events AFTER schedule for (subcomponent : components.reject[it == coordinationInstance]) { val subcomponentType = subcomponent.type @@ -1506,12 +1497,12 @@ class ComponentTransformer { // 1) the Sync ort semantics: Resetting channel IN events AFTER schedule would result in a deadlock // 2) the Casc semantics: Resetting channel OUT events BEFORE schedule would delete in events of subsequent components // Note, System in and out events are reset in the env action + // 3) Coordination automata semantics: following the the Casc semantics resetting IN events AFTER schedule + - // TODO - // Resetting OUT events BEFORE schedule -// val clonedNewOutEventAction = newOutEventAction.clone // Clone is important -// .resetEverythingExceptPersistentParameters(subcomponentType) -// actualComponentMergedAction.actions.add(0, clonedNewOutEventAction) // Putting the new action BEFORE + val clonedNewInEventAction = newInEventAction.clone. + resetEverythingExceptPersistentParameters(subcomponentType) // Clone is important + actualComponentMergedAction.actions += clonedNewInEventAction // Putting the new action AFTER // Tracing merged action componentMergedActions += subcomponentType -> actualComponentMergedAction.clone From c71a964c1639bc4a024fbecffc139cf2c54025d8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rich=C3=A1rd=20Szab=C3=B3?= Date: Thu, 5 Mar 2026 15:42:46 +0100 Subject: [PATCH 27/27] Coordination automata states now shows in gpl and trace --- .../StatechartModelDerivedFeatures.java | 11 +++++++++-- .../serializer/ExpressionSerializer.xtend | 9 ++++++++- .../derivedfeatures/XstsDerivedFeatures.java | 19 +++++++++++++++++++ .../api/Gamma2XstsTransformerSerializer.xtend | 12 ++++++++++++ 4 files changed, 48 insertions(+), 3 deletions(-) diff --git a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java index b2b48fdaa..2973cc9b6 100644 --- a/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java +++ b/plugins/core/hu.bme.mit.gamma.statechart.model/src/hu/bme/mit/gamma/statechart/derivedfeatures/StatechartModelDerivedFeatures.java @@ -831,8 +831,10 @@ else if (component instanceof AbstractSynchronousCompositeComponent synchronousC for (SynchronousComponentInstance instance : synchronousCompositeComponent.getComponents()) { instances.add(instance); SynchronousComponent type = instance.getType(); - instances.addAll( - getAllInstances(type)); + if (!(type instanceof CoordinationStatechartDefinition)) { + // The instances of the components of a CoordinationStatechart are already visited + instances.addAll(getAllInstances(type)); + } } } return instances; @@ -2398,6 +2400,11 @@ public static boolean needsWrapping(Component component) { if (component instanceof AsynchronousAdapter adapter) { return !isSimplifiable(adapter); } + else if (component instanceof SynchronousCoordinationStatechartDefinition) { + // CoordinationStatechartDefinitions are composite components as well + return false; + } + // TODO check again when implementing AsynchronousCoordinationStatechartDefinition return isStatechart(component); } diff --git a/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/serializer/ExpressionSerializer.xtend b/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/serializer/ExpressionSerializer.xtend index 8edf7f0f4..3accf12a4 100644 --- a/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/serializer/ExpressionSerializer.xtend +++ b/plugins/nuxmv/hu.bme.mit.gamma.xsts.nuxmv.transformation/src/hu/bme/mit/gamma/xsts/nuxmv/transformation/serializer/ExpressionSerializer.xtend @@ -28,6 +28,7 @@ import hu.bme.mit.gamma.statechart.util.ExpressionTypeDeterminator import hu.bme.mit.gamma.util.GammaEcoreUtil import static extension hu.bme.mit.gamma.expression.derivedfeatures.ExpressionModelDerivedFeatures.* +import hu.bme.mit.gamma.statechart.statechart.TimeoutReferenceExpression class ExpressionSerializer extends hu.bme.mit.gamma.expression.util.ExpressionSerializer { // Singleton @@ -43,7 +44,11 @@ class ExpressionSerializer extends hu.bme.mit.gamma.expression.util.ExpressionSe override String _serialize(EnumerationLiteralExpression expression) '''«expression.reference.name»''' override String serialize(Expression expression) { - return super.serialize(expression) + if (expression instanceof TimeoutReferenceExpression) { + return expression.serialize + } else { + return super.serialize(expression) + } } override String _serialize(TrueExpression expression) '''TRUE''' @@ -89,4 +94,6 @@ class ExpressionSerializer extends hu.bme.mit.gamma.expression.util.ExpressionSe return smvArrayLiteral.toString } + def String serialize(TimeoutReferenceExpression expression) '''«expression.timeout.name»''' + } \ No newline at end of file diff --git a/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java b/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java index 11d81046d..82ab6e0af 100644 --- a/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java +++ b/plugins/xsts/hu.bme.mit.gamma.xsts.model/src/hu/bme/mit/gamma/xsts/derivedfeatures/XstsDerivedFeatures.java @@ -49,6 +49,7 @@ import hu.bme.mit.gamma.xsts.model.AssumeAction; import hu.bme.mit.gamma.xsts.model.AsynchronousSystemAnnotation; import hu.bme.mit.gamma.xsts.model.AtomicAction; +import hu.bme.mit.gamma.xsts.model.DelayAction; import hu.bme.mit.gamma.xsts.model.EmptyAction; import hu.bme.mit.gamma.xsts.model.EnvironmentalInvariantAnnotation; import hu.bme.mit.gamma.xsts.model.FunctionCallAction; @@ -661,6 +662,10 @@ private static Set _getReadVariables(MultiaryAction action) return variableList; } + private static Set _getReadVariables(DelayAction action) { + return Collections.emptySet(); + } + private static Set _getExternallyReadVariables(AssignmentAction action) { Set readVariables = new HashSet(); @@ -795,6 +800,10 @@ private static Set _getWrittenVariables(MultiaryAction acti return variableList; } + + private static Set _getWrittenVariables(DelayAction action) { + return Collections.emptySet(); // Empty, as this is a declaration, not a "writing" + } public static Set getReadVariables(Action action) { if (action instanceof AssignmentAction _action) { @@ -830,6 +839,10 @@ else if (action instanceof FunctionCallAction _action) { else if (action instanceof OpaqueAction) { return Set.of(); } + else if (action instanceof DelayAction _action) { + return _getReadVariables(_action); + } + else { throw new IllegalArgumentException("Unhandled action type: " + action); } @@ -869,6 +882,9 @@ else if (action instanceof FunctionCallAction _action) { else if (action instanceof OpaqueAction) { return Set.of(); } + else if (action instanceof DelayAction _action) { + return _getReadVariables(_action); + } else { throw new IllegalArgumentException("Unhandled action type: " + action); } @@ -905,6 +921,9 @@ else if (action instanceof FunctionCallAction _action) { else if (action instanceof OpaqueAction) { return Set.of(); } + else if (action instanceof DelayAction _action) { + return _getWrittenVariables(_action); + } else { throw new IllegalArgumentException("Unhandled action type: " + action); } 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 bba870f75..4a35492e7 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 @@ -30,6 +30,7 @@ import java.io.File import java.util.List import static extension hu.bme.mit.gamma.statechart.derivedfeatures.StatechartModelDerivedFeatures.* +import hu.bme.mit.gamma.statechart.statechart.CoordinationStatechartDefinition class Gamma2XstsTransformerSerializer { @@ -153,6 +154,17 @@ class Gamma2XstsTransformerSerializer { val xSts = gammaToXSTSTransformer.execute(newGammaPackage) // EMF xSts.normalSave(targetFolderUri, fileName.emfXStsFileName) + + if (newTopComponent instanceof CoordinationStatechartDefinition) { + /* This is needed because during the transformation new ComponentInstances, States and Transitions are created, + * and the updated .gsm is needed for the trace and the property language + * + * note: might be worth to makes this generic, e.g. create a definition which means that the model changed during the + * transformation as is needed to be saved again + */ + + newGammaPackage.eResource.save + } // String xSts.serializeAndSaveXSts }