Skip to content
Open
Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
b4d44b4
First version of the coordination-automata
Rorck Apr 29, 2025
b5cd716
Simplified coordination automata
Rorck May 12, 2025
379b053
Coordination automata transformation WIP
Rorck Jun 17, 2025
b61d1af
Coord automata is now generated to env
Rorck Jun 19, 2025
9bdcd67
Merge branch 'dev' into coordination-automata
Rorck Jun 19, 2025
0368b78
Added util functions for EnumerationExpressions
Rorck Jun 20, 2025
3e009a3
More work on coordination automata
Rorck Jun 20, 2025
cefb895
Added additional logging to SystemReducer
Rorck Aug 5, 2025
f01a48c
Added Imply serialization to XstsExprSerializer, see Theta XstsDsl Im…
Rorck Aug 5, 2025
e6261cf
Added CoordinationVariableAnnotation to mark variable used for coordi…
Rorck Aug 5, 2025
af28c88
Simplified coordination transformation using CoordinationVariableAnno…
Rorck Aug 5, 2025
666c127
Removed unnecessary printout
Rorck Aug 5, 2025
a1a8644
Merge branch 'dev' into coordination-automata
Rorck Aug 5, 2025
6b2070e
Added PlantUML visualization for CoordinationAutomata
Rorck Jan 27, 2026
57aff9f
Added separate warnings for unconnected ports
Rorck Jan 27, 2026
4990c71
Added util function for oncycle trigger to StatechartUtil
Rorck Jan 27, 2026
082ade4
Added util functions for CoordinationTransitions
Rorck Jan 30, 2026
a8b4df3
Added util function to generate all possible permutations of a list
Rorck Jan 30, 2026
dbfa0a0
Modified unordered coordination transformation
Rorck Jan 30, 2026
129cd68
Introduced delay action to xsts model
Rorck Jan 30, 2026
d5a5ba2
Added delay actions to coordination automata env
Rorck Jan 30, 2026
1cc2914
Added handling of delay actions to the clock handling of GammaToXstsT…
Rorck Jan 30, 2026
2a12fef
Commit changes
Rorck Feb 2, 2026
2bbc76a
Merged newest dev
Rorck Feb 2, 2026
def3db8
Fixed minor mistake
Rorck Feb 4, 2026
0694932
Added test models for coordination automaton
Rorck Feb 4, 2026
59e2e51
Addressed several comments
Rorck Feb 10, 2026
dbd715f
Merged dev
Rorck Feb 10, 2026
e842b5c
Changed superclass of DelayAction to AbstractUpdateAction
Rorck Feb 10, 2026
e25c819
Added resettig channel events to coordination automaton
Rorck Feb 25, 2026
c71a964
Coordination automata states now shows in gpl and trace
Rorck Mar 5, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -567,6 +567,15 @@ public Set<ValueDeclaration> 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<ConstantDeclaration> extractParameters(ParametricElement parametricElement,
Expand Down Expand Up @@ -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<? extends Expression> expressions) {
Expression orExpression = wrapIntoOrExpression(expressions);
NotExpression notExpression = createNotExpression(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -436,8 +436,9 @@ DeepHistoryState returns DeepHistoryState:

Component returns InterfaceModel::Component:
SynchronousComponent |
AsynchronousComponent |
CoordinationStatechartDefinition
AsynchronousComponent |
SynchronousCoordinationStatechartDefinition |
AsynchronousCoordinationStatechartDefinition
;

SynchronousComponent returns CompositeModel::SynchronousComponent:
Expand Down Expand Up @@ -738,7 +739,7 @@ ComponentInstanceReflectiveElementReferenceExpression returns CompositeModel::Co

//

CoordinationStatechartDefinition returns CoordinationStatechartDefinition:
SynchronousCoordinationStatechartDefinition returns SynchronousCoordinationStatechartDefinition:
'@Coordination'
(
('@RegionSchedule' '=' schedulingOrder=SchedulingOrder)? &
Expand All @@ -749,20 +750,90 @@ 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)*)? ']')?
'{'
(
components+=SynchronousComponentInstance |
portBindings+=PortBinding |
channels+=Channel
)*
'}'
'<'
(
variableDeclarations+=VariableDeclaration |
timeoutDeclarations+=TimeoutDeclaration |
('invariant' invariants+=Expression)
)*
(
regions+=Region |
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:
SequentialCoordinationReferenceExpression
| UnorderedCoordinationReferenceExpression
;

SequentialCoordinationReferenceExpression returns SequentialCoordinationReferenceExpression:
'seq' '{' instances+=ComponentInstanceReferenceExpression((',') instances+=ComponentInstanceReferenceExpression)* '}' | instances+=ComponentInstanceReferenceExpression
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the sake of unity, we may (or may not) want to revamp these keywords, e.g., seq -> sequential; we tend to use complete words like transition, state, integer...

;

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)* )?

;

//
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -367,13 +368,25 @@ 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();
}
}
return super.getScope(context, reference);
}

Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,28 @@
<eStructuralFeatures xsi:type="ecore:EReference" name="timeout" lowerBound="1"
eType="#//TimeoutDeclaration"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="CoordinationStatechartDefinition" eSuperTypes="#//StatechartDefinition"/>
<eClassifiers xsi:type="ecore:EClass" name="CoordinationTransition" eSuperTypes="#//Transition"/>
<eClassifiers xsi:type="ecore:EClass" name="CoordinationStatechartDefinition" eSuperTypes="#//StatechartDefinition composite.ecore#//CompositeComponent">
<eStructuralFeatures xsi:type="ecore:EReference" name="coordinationTransitions"
upperBound="-1" eType="#//CoordinationTransition" containment="true"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="SynchronousCoordinationStatechartDefinition"
eSuperTypes="#//CoordinationStatechartDefinition composite.ecore#//SynchronousComponent composite.ecore#//SynchronousCompositeComponent"/>
<eClassifiers xsi:type="ecore:EClass" name="AsynchronousCoordinationStatechartDefinition"
eSuperTypes="#//CoordinationStatechartDefinition composite.ecore#//AsynchronousComponent composite.ecore#//AsynchronousCompositeComponent"/>
<eClassifiers xsi:type="ecore:EClass" name="CoordinationTransition" eSuperTypes="#//Transition">
<eStructuralFeatures xsi:type="ecore:EReference" name="coordinatedComponent" eType="#//AbstractCoordinationReferenceExpression"
containment="true"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="AbstractCoordinationReferenceExpression"
abstract="true" eSuperTypes="../../hu.bme.mit.gamma.expression.model/model/expression.ecore#//ReferenceExpression">
<eStructuralFeatures xsi:type="ecore:EReference" name="instances" lowerBound="1"
upperBound="-1" eType="ecore:EClass composite.ecore#//ComponentInstanceReferenceExpression"
containment="true"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="SequentialCoordinationReferenceExpression"
eSuperTypes="#//AbstractCoordinationReferenceExpression"/>
<eClassifiers xsi:type="ecore:EClass" name="UnorderedCoordinationReferenceExpression"
eSuperTypes="#//AbstractCoordinationReferenceExpression"/>
<eClassifiers xsi:type="ecore:EClass" name="CoordinationVariableDeclarationAnnotation"
eSuperTypes="../../hu.bme.mit.gamma.expression.model/model/expression.ecore#//VariableDeclarationAnnotation"/>
</ecore:EPackage>
Original file line number Diff line number Diff line change
Expand Up @@ -397,7 +397,19 @@
<genClasses ecoreClass="statechart.ecore#//TimeoutReferenceExpression">
<genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference statechart.ecore#//TimeoutReferenceExpression/timeout"/>
</genClasses>
<genClasses ecoreClass="statechart.ecore#//CoordinationStatechartDefinition"/>
<genClasses ecoreClass="statechart.ecore#//CoordinationTransition"/>
<genClasses ecoreClass="statechart.ecore#//CoordinationStatechartDefinition">
<genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference statechart.ecore#//CoordinationStatechartDefinition/coordinationTransitions"/>
</genClasses>
<genClasses ecoreClass="statechart.ecore#//SynchronousCoordinationStatechartDefinition"/>
<genClasses ecoreClass="statechart.ecore#//AsynchronousCoordinationStatechartDefinition"/>
<genClasses ecoreClass="statechart.ecore#//CoordinationTransition">
<genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference statechart.ecore#//CoordinationTransition/coordinatedComponent"/>
</genClasses>
<genClasses image="false" ecoreClass="statechart.ecore#//AbstractCoordinationReferenceExpression">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference statechart.ecore#//AbstractCoordinationReferenceExpression/instances"/>
</genClasses>
<genClasses ecoreClass="statechart.ecore#//SequentialCoordinationReferenceExpression"/>
<genClasses ecoreClass="statechart.ecore#//UnorderedCoordinationReferenceExpression"/>
<genClasses ecoreClass="statechart.ecore#//CoordinationVariableDeclarationAnnotation"/>
</genPackages>
</genmodel:GenModel>
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -106,11 +107,14 @@
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;
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;
Expand All @@ -130,6 +134,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;
Expand All @@ -140,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;
Expand Down Expand Up @@ -1876,10 +1882,7 @@ public static List<Port> getAllBoundSimplePorts(Component component) {
public static List<Port> getAllBoundSimplePorts(Port port) {
List<Port> simplePorts = new ArrayList<Port>();
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
Expand All @@ -1890,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;
}
Expand Down Expand Up @@ -2150,6 +2156,12 @@ public static List<? extends ComponentInstance> 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);
}

Expand Down Expand Up @@ -2304,6 +2316,11 @@ public static List<Transition> getNonTrappingOutgoingTransitions(StateNode node)

public static List<Transition> 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());
}
Expand Down Expand Up @@ -2351,6 +2368,12 @@ public static List<Transition> getOutgoingTransitionsUntilState(StateNode node)

public static List<Transition> 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());
}
Expand All @@ -2359,6 +2382,12 @@ public static List<Transition> getAllIncomingTransitions(StateNode node) {
List<StateNode> 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());
Expand Down Expand Up @@ -3788,4 +3817,11 @@ public static List<Expression> mapInterfaceInvariantsToPort(Port port) {
return interfaceInvariants;
}

// Coordination

public static List<VariableDeclaration> getCoordinationVariables(StatechartDefinition statechart) {
return filterVariablesByAnnotation(statechart.getVariableDeclarations(),
CoordinationVariableDeclarationAnnotation.class);
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -706,6 +707,10 @@ public Collection<ValidationResultMessage> checkElseTransitionPriority(Transitio

public Collection<ValidationResultMessage> checkTransitionTriggers(Transition transition) {
Collection<ValidationResultMessage> validationResultMessages = new ArrayList<ValidationResultMessage>();
if (transition instanceof CoordinationTransition) {
// TODO
return validationResultMessages;
}
if (!StatechartModelDerivedFeatures.needsTrigger(transition)) {
return validationResultMessages;
}
Expand Down
Loading