-
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 Added 'static inline' to disable dynamic resolving
- Loading branch information
1 parent
1515287
commit 5fb0c71
Showing
12 changed files
with
341 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
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 | ||
| } | ||
|
|
45 changes: 45 additions & 0 deletions
45
...r/TestModels/Automated/Simple/InlineTransition/StaticInline/MultiHierarchical/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,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 | ||
| } | ||
| } |
19 changes: 19 additions & 0 deletions
19
...semantifyr/TestModels/Automated/Simple/InlineTransition/StaticInline/Simple/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,19 @@ | ||
| /* | ||
| * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors | ||
| * | ||
| * SPDX-License-Identifier: EPL-2.0 | ||
| */ | ||
|
|
||
|
|
||
| trans { | ||
| assume (false); | ||
| } | ||
|
|
||
| init { | ||
| } | ||
|
|
||
| env {} | ||
|
|
||
| prop { | ||
| true | ||
| } |
Oops, something went wrong.