Skip to content
Open
Show file tree
Hide file tree
Changes from all 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 @@ -67,7 +67,7 @@ class CompletenessTrapStateInjector {
}
else {
val defaultGuard = outgoingTransitions.createDefaultGuard
trapTransition.trigger = createOnCycleTrigger
trapTransition.trigger = statechartFactory.createOnCycleTrigger
trapTransition.guard = defaultGuard
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -692,6 +692,16 @@ public Set<ValueDeclaration> getReferredValues(Expression expression) {
return referred;
}

public EnumerationLiteralDefinition getEnumerationLiteralDefinitionByName(EnumerationTypeDefinition typeDefinition, String name) {
for (EnumerationLiteralDefinition literal : typeDefinition.getLiterals()) {
String enumLiteralName = literal.getName();
if (enumLiteralName.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 @@ -1719,6 +1729,12 @@ public EnumerationLiteralExpression createEnumerationLiteralExpression(
return literalExpression;
}

public EnumerationLiteralExpression createEnumerationLiteralExpression(
EnumerationTypeDefinition typeDefinition, String name) {
EnumerationLiteralDefinition enumLiteralDefinition = getEnumerationLiteralDefinitionByName(typeDefinition, name);
return createEnumerationLiteralExpression(enumLiteralDefinition);
}

public SubtractExpression createSubtractExpression(Expression lhs, Expression rhs) {
SubtractExpression subtractExpression = factory.createSubtractExpression();
subtractExpression.setLeftOperand(lhs);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -441,8 +441,9 @@ DeepHistoryState returns DeepHistoryState:

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

SynchronousComponent returns CompositeModel::SynchronousComponent:
Expand Down Expand Up @@ -748,7 +749,7 @@ ComponentInstanceReflectiveElementReferenceExpression returns CompositeModel::Co

//

CoordinationStatechartDefinition returns CoordinationStatechartDefinition:
SynchronousCoordinationStatechartDefinition returns SynchronousCoordinationStatechartDefinition:
'@Coordination'
(
('@RegionSchedule' '=' schedulingOrder=SchedulingOrder)? &
Expand All @@ -759,20 +760,91 @@ 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
;

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 @@ -377,7 +377,7 @@ public IScope getScope(final EObject context, final EReference reference) {
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 @@ -166,6 +166,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 @@ -402,7 +402,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 @@ -50,6 +50,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 @@ -108,11 +109,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 @@ -132,6 +136,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 @@ -142,6 +147,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 @@ -825,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;
Expand Down Expand Up @@ -2290,6 +2298,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 @@ -2386,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);
}

Expand Down Expand Up @@ -2461,6 +2480,11 @@ public static List<Transition> getSiblingTransitions(Transition transition) {

public static List<Transition> getOutgoingTransitions(StateNode node) {
StatechartDefinition statechart = getContainingStatechart(node);
if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) {
// TODO CoordinationStatechart Validation
return coordinationStatechart.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 @@ -2508,6 +2532,12 @@ public static List<Transition> getOutgoingTransitionsUntilState(StateNode node)

public static List<Transition> getIncomingTransitions(StateNode node) {
StatechartDefinition statechart = getContainingStatechart(node);
if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) {
// TODO CoordinationStatechart Validation
return coordinationStatechart.getCoordinationTransitions().stream()
.filter(it -> it.getTargetState() == node).collect(Collectors.toList());
}

return statechart.getTransitions().stream().filter(it -> it.getTargetState() == node)
.collect(Collectors.toList());
}
Expand All @@ -2516,6 +2546,12 @@ public static List<Transition> getAllIncomingTransitions(StateNode node) {
List<StateNode> allStateNodes = ecoreUtil
.getSelfAndAllContentsOfType(node, StateNode.class);
StatechartDefinition statechart = getContainingStatechart(node);
if (statechart instanceof CoordinationStatechartDefinition coordinationStatechart) {
// TODO CoordinationStatechart Validation
return coordinationStatechart.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 @@ -4012,4 +4048,15 @@ public static List<Expression> mapInterfaceInvariantsToPort(Port port) {
return interfaceInvariants;
}

// Coordination

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

public static boolean isCoordinationStatechart(StatechartDefinition statechart) {
return statechart instanceof CoordinationStatechartDefinition;
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,9 @@ public String serialize(Expression expression) {
if (expression instanceof ComponentInstanceEventParameterReferenceExpression reference) {
return _serialize(reference);
}
if (expression instanceof TimeoutReferenceExpression reference) {
return _serialize(reference);
}
String string = super.serialize(expression);
return javaUtil.deparenthesize(string);
}
Expand Down
Loading