-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
#22 Implemented 'static inline' that disables dynamic transition reso…
…lving (#40)
- Loading branch information
Showing
14 changed files
with
381 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
32 changes: 32 additions & 0 deletions
32
...ng/src/main/java/hu/bme/mit/semantifyr/oxsts/lang/scoping/OxstsQualifiedNameProvider.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| package hu.bme.mit.semantifyr.oxsts.lang.scoping; | ||
|
|
||
| import hu.bme.mit.semantifyr.oxsts.model.oxsts.BaseType; | ||
| import hu.bme.mit.semantifyr.oxsts.model.oxsts.Transition; | ||
| import org.eclipse.xtext.EcoreUtil2; | ||
| import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider; | ||
| import org.eclipse.xtext.naming.QualifiedName; | ||
|
|
||
| public class OxstsQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider { | ||
|
|
||
| protected QualifiedName qualifiedName(Transition transition) { | ||
| var parentsName = getFullyQualifiedName(transition.eContainer()); | ||
| var name = elementName(transition); | ||
|
|
||
| return parentsName.append(name); | ||
| } | ||
|
|
||
| protected String elementName(Transition transition) { | ||
| var baseType = EcoreUtil2.getContainerOfType(transition, BaseType.class); | ||
|
|
||
| if (baseType.getMainTransition().contains(transition)) { | ||
| return "main"; | ||
| } else if (baseType.getInitTransition().contains(transition)) { | ||
| return "init"; | ||
| } else if (baseType.getHavocTransition().contains(transition)) { | ||
| return "havoc"; | ||
| } | ||
|
|
||
| return transition.getName(); | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
24 changes: 24 additions & 0 deletions
24
subprojects/semantifyr/TestModels/Automated/Example/PetriNet/expected.xsts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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)) | ||
| } |
158 changes: 158 additions & 0 deletions
158
subprojects/semantifyr/TestModels/Automated/Example/PetriNet/model.oxsts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
| } | ||
| } | ||
| } | ||
|
|
||
| } |
24 changes: 24 additions & 0 deletions
24
...TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/expected.xsts
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
| } | ||
|
|
Oops, something went wrong.