diff --git a/subprojects/oxsts.lang/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/Oxsts.xtext b/subprojects/oxsts.lang/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/Oxsts.xtext index 6cfc578..1611060 100644 --- a/subprojects/oxsts.lang/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/Oxsts.xtext +++ b/subprojects/oxsts.lang/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/Oxsts.xtext @@ -193,7 +193,7 @@ InlineSeq: ; InlineCall: - 'inline' reference=ReferenceExpression '(' + (static ?= 'static')? 'inline' reference=ReferenceExpression '(' ( argumentBindings+=ArgumentBinding (',' argumentBindings+=ArgumentBinding)* (',')? diff --git a/subprojects/oxsts.model/model/oxsts.aird b/subprojects/oxsts.model/model/oxsts.aird index dd8e0ea..0c9c5cb 100644 --- a/subprojects/oxsts.model/model/oxsts.aird +++ b/subprojects/oxsts.model/model/oxsts.aird @@ -29,7 +29,7 @@ - + @@ -3073,7 +3073,7 @@ - + KEEP_LOCATION @@ -4093,6 +4093,10 @@ + + + + @@ -4359,6 +4363,12 @@ + + + bold + + + @@ -4379,7 +4389,7 @@ KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + @@ -4391,6 +4401,14 @@ + + + + + bold + + + @@ -4493,12 +4511,12 @@ - + - + italic - + diff --git a/subprojects/oxsts.model/model/oxsts.ecore b/subprojects/oxsts.model/model/oxsts.ecore index 903730d..9df81f2 100644 --- a/subprojects/oxsts.model/model/oxsts.ecore +++ b/subprojects/oxsts.model/model/oxsts.ecore @@ -66,6 +66,8 @@ containment="true"/> + diff --git a/subprojects/oxsts.model/model/oxsts.genmodel b/subprojects/oxsts.model/model/oxsts.genmodel index 9e52dd6..da9c729 100644 --- a/subprojects/oxsts.model/model/oxsts.genmodel +++ b/subprojects/oxsts.model/model/oxsts.genmodel @@ -59,6 +59,7 @@ + diff --git a/subprojects/semantifyr-vscode/syntaxes/oxsts.tmLanguage.json b/subprojects/semantifyr-vscode/syntaxes/oxsts.tmLanguage.json index 1a6abe2..c29cbf9 100644 --- a/subprojects/semantifyr-vscode/syntaxes/oxsts.tmLanguage.json +++ b/subprojects/semantifyr-vscode/syntaxes/oxsts.tmLanguage.json @@ -23,7 +23,7 @@ "patterns": [ { "name": "keyword.control.oxsts", - "match": "\\b(abstract|package|or|import|enum|inline|seq|ctrl|as|assume|var|type|target|feature|containment|reference|derived|instance|association|pattern|init|havoc|tran|choice|if|else|find|virtual|override|prop)\\b" + "match": "\\b(abstract|package|or|import|enum|static|inline|seq|ctrl|as|assume|var|type|target|feature|containment|reference|derived|instance|association|pattern|init|havoc|tran|choice|if|else|find|virtual|override|prop)\\b" } ] }, diff --git a/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/expected.xsts b/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/expected.xsts new file mode 100644 index 0000000..c96dc10 --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/expected.xsts @@ -0,0 +1,24 @@ +/* + * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + + +var __Mission__petriNet__p1__tokens : integer = 100 +var __Mission__petriNet__p2__tokens : integer = 0 + +trans { + assume ((__Mission__petriNet__p1__tokens >= 5)); + __Mission__petriNet__p1__tokens := (__Mission__petriNet__p1__tokens - 5); + __Mission__petriNet__p2__tokens := (__Mission__petriNet__p2__tokens + 5); +} + +init { +} + +env {} + +prop { + ! ((__Mission__petriNet__p2__tokens >= 20)) +} diff --git a/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/model.oxsts b/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/model.oxsts new file mode 100644 index 0000000..bbc91e0 --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Example/PetriNet/model.oxsts @@ -0,0 +1,158 @@ +package Example + +type Place { + reference defaultTokens : Integer = 0 + + var tokens : Integer = defaultTokens + + tran enoughTokens(weight: Integer) { + assume (tokens >= weight) + } + + tran takeTokens(weight: Integer) { + tokens := tokens - weight + } + + tran placeTokens(weight: Integer) { + tokens := tokens + weight + } +} + +type Edge { + reference weight : Integer = 1 + reference place : Place + + tran takeTokens { + inline place.enoughTokens(weight) + inline place.takeTokens(weight) + } + + tran placeTokens { + inline place.placeTokens(weight) + } +} + +type Transition { + feature sourceEdges : Edge[0..*] + feature targetEdges : Edge[0..*] + + tran fire { + inline seq sourceEdges -> takeTokens + inline seq targetEdges -> placeTokens + } +} + +type PetriNet { + feature places : Place[0..*] + feature transitions : Transition[0..*] + + tran { + inline choice transitions -> fire + } +} + +target Mission { + containment petriNet : PetriNet { + containment p1 :> places : Place { + reference ::> defaultTokens : Integer = 100 + } + containment p2 :> places : Place + + containment t1 :> transitions : Transition { + containment p1_t1 :> sourceEdges : Edge { + reference ::> weight : Integer = 5 + reference ::> place : Place = p1 + } + containment t1_p2 :> targetEdges : Edge { + reference ::> weight : Integer = 5 + reference ::> place : Place = p2 + } + } + } + + init { + + } + + tran asdf { + + } + + tran { + inline petriNet.main() + } + + prop { + ! (petriNet.p2.tokens >= 20) + } + +} + +target MissionWitness : Mission { + ctrl var state : Integer = 0 - 1 + + init { + assume (state == (0 - 1)) + + assume (petriNet.p1.tokens == 100) + assume (petriNet.p2.tokens == 0) + + static inline ExamplePetriNet::init() + + assume (petriNet.p1.tokens == 100) + assume (petriNet.p2.tokens == 0) + + choice { + state := 0 + } + } + + tran { + choice { + assume (state == 0) + + static inline ExamplePetriNet::main() + + assume (petriNet.p1.tokens == 95) + assume (petriNet.p2.tokens == 5) + + choice { + state := 1 + } + } or { + assume (state == 1) + + static inline ExamplePetriNet::main() + + assume (petriNet.p1.tokens == 90) + assume (petriNet.p2.tokens == 10) + + choice { + state := 2 + } + } or { + assume (state == 2) + + static inline ExamplePetriNet::main() + + assume (petriNet.p1.tokens == 85) + assume (petriNet.p2.tokens == 15) + + choice { + state := 3 + } + } or { + assume (state == 3) + + static inline ExamplePetriNet::main() + + assume (petriNet.p1.tokens == 80) + assume (petriNet.p2.tokens == 20) + + choice { + state := 4 + } + } + } + +} diff --git a/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/expected.xsts b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/expected.xsts new file mode 100644 index 0000000..afd035f --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/expected.xsts @@ -0,0 +1,24 @@ +/* + * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + + +var __Mission__b__x : integer = 0 +var __Mission__c__x : integer = 0 + +trans { + assume ((__Mission__b__x == 2)); + __Mission__c__x := 10; +} + +init { +} + +env {} + +prop { + true +} + \ No newline at end of file diff --git a/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/model.oxsts b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/model.oxsts new file mode 100644 index 0000000..f1aae4a --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/model.oxsts @@ -0,0 +1,45 @@ +/* + * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + +package Test + +type A { + var x : Integer = 0 + + tran { + assume (x == 2) + } +} + +type B : A { + tran { + static inline A::main() // without static would become a recursion + } +} + +type C : B { + tran { + x := 10 + } +} + +target Mission { + containment b : B + containment c : C + + init { + + } + + tran { + inline b.main() + inline c.main() + } + + prop { + true + } +} diff --git a/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/expected.xsts b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/expected.xsts new file mode 100644 index 0000000..1d33fd7 --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/expected.xsts @@ -0,0 +1,19 @@ +/* + * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + + +trans { + assume (false); +} + +init { +} + +env {} + +prop { + true +} diff --git a/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/model.oxsts b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/model.oxsts new file mode 100644 index 0000000..ac05856 --- /dev/null +++ b/subprojects/semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/model.oxsts @@ -0,0 +1,35 @@ +/* + * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ + +package Test + +type A { + tran { + assume (false) + } +} + +type B : A { + tran { + static inline A::main() // without static would become a recursion + } +} + +target Mission { + containment b : B + + init { + + } + + tran { + inline b.main() + } + + prop { + true + } +} diff --git a/subprojects/semantifyr/src/main/kotlin/transformation/rewrite/OperationInliner.kt b/subprojects/semantifyr/src/main/kotlin/transformation/rewrite/OperationInliner.kt index e7bedc7..ea68c65 100644 --- a/subprojects/semantifyr/src/main/kotlin/transformation/rewrite/OperationInliner.kt +++ b/subprojects/semantifyr/src/main/kotlin/transformation/rewrite/OperationInliner.kt @@ -29,6 +29,7 @@ import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.drop import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.dropLast import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.element import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.isStaticReference +import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.typedReferencedElement import org.eclipse.emf.ecore.EObject import org.eclipse.xtext.EcoreUtil2 @@ -40,14 +41,18 @@ class OperationInliner( is InlineCall -> { val containerInstance = context.contextualEvaluator.evaluateInstanceOrNull(operation.reference.asChainReferenceExpression().dropLast(1)) - @Suppress("FoldInitializerAndIfToElvis") // would be difficult to read + @Suppress("FoldInitializerAndIfToElvis") if (containerInstance == null) { // TODO: should we throw an exception here? // If the feature has no instances, then this is a violated reference return OxstsFactory.createEmptyOperation() } - val transition = context.contextualEvaluator.evaluateTransition(operation.reference) + val transition = if (operation.isStatic) { + operation.reference.typedReferencedElement() + } else { + context.contextualEvaluator.evaluateTransition(operation.reference) + } OxstsFactory.createChoiceOperation().apply { for (currentOperation in transition.operation) {