diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..9b670f4 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,10 @@ +[*] +charset = utf-8 +end_of_line = lf +indent_style = tab +tab_width = 4 +insert_final_newline = true + +[*.yml] +indent_style = space +indent_size = 2 diff --git a/.github/workflows/validate-project-examples.yml b/.github/workflows/validate-project-examples.yml new file mode 100644 index 0000000..c2e9c45 --- /dev/null +++ b/.github/workflows/validate-project-examples.yml @@ -0,0 +1,26 @@ +name: Validate project examples + +on: + push: + branches: [main] + pull_request: + branches: [main] + +permissions: + contents: read + +jobs: + validate: + runs-on: ubuntu-latest + + steps: + - name: Checkout code + uses: actions/checkout@v3 + + - name: Set up Deno stable + uses: denoland/setup-deno@v1 + with: + deno-version: vx.x.x + + - name: Run validation + run: cd Project-Examples && deno run --allow-read=. validate.mjs diff --git a/Project-Examples/README.md b/Project-Examples/README.md new file mode 100644 index 0000000..a25cee3 --- /dev/null +++ b/Project-Examples/README.md @@ -0,0 +1,19 @@ +# Ecdar project examples + +This repository contains a few example projects to use with Ecdar. + +The projects are intended to be used by: + +- newcomers to Ecdar that want to understand how it works +- developers who need a quick project to test their work with + +The projects can also be useful for: + +- seasoned users that need a quick template to build from +- test suites that are testing support for real-world projects + +This repository is NOT intended to be: + +- an exhaustive list of all features and project types that Ecdar supports +- a long list of unit tests for use in test suites +- a long list of broken projects for use in test suites diff --git a/Project-Examples/examples/AG test/Components/A_Good.json b/Project-Examples/examples/AG test/Components/A_Good.json new file mode 100644 index 0000000..f2dcdea --- /dev/null +++ b/Project-Examples/examples/AG test/Components/A_Good.json @@ -0,0 +1,113 @@ +{ + "name": "A_Good", + "declarations": "", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 210, + "y": 190, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 150, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 10 + }, + { + "x": 150, + "y": 160, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "bad", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 140, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 240, + "y": 140, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 180, + "y": 240, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "9", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/AG test/Components/G.json b/Project-Examples/examples/AG test/Components/G.json new file mode 100644 index 0000000..fdb7e8c --- /dev/null +++ b/Project-Examples/examples/AG test/Components/G.json @@ -0,0 +1,113 @@ +{ + "name": "G", + "declarations": "", + "locations": [ + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E4", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 180, + "y": 270, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 360, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 200, + "y": 360, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E6", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 270, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 280, + "y": 330, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "5", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/AG test/Components/Imp.json b/Project-Examples/examples/AG test/Components/Imp.json new file mode 100644 index 0000000..230830a --- /dev/null +++ b/Project-Examples/examples/AG test/Components/Imp.json @@ -0,0 +1,190 @@ +{ + "name": "Imp", + "declarations": "", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 210, + "y": 150, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "U1", + "nickname": "", + "invariant": "", + "type": "UNIVERSAL", + "urgency": "NORMAL", + "x": 210, + "y": 250, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E7", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 160, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 160, + "y": 190, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E8", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 260, + "y": 190, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E9", + "group": "", + "sourceLocation": "U1", + "targetLocation": "U1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": false, + "nails": [ + { + "x": 160, + "y": 240, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 140, + "y": 250, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 160, + "y": 260, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E10", + "group": "", + "sourceLocation": "U1", + "targetLocation": "U1", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 240, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 260, + "y": 250, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 240, + "y": 260, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E11", + "group": "", + "sourceLocation": "L0", + "targetLocation": "U1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/AG test/GlobalDeclarations.json b/Project-Examples/examples/AG test/GlobalDeclarations.json new file mode 100644 index 0000000..1a4a958 --- /dev/null +++ b/Project-Examples/examples/AG test/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan good, bad, button1, button2;" +} diff --git a/Project-Examples/examples/AG test/Queries.json b/Project-Examples/examples/AG test/Queries.json new file mode 100644 index 0000000..cac57f8 --- /dev/null +++ b/Project-Examples/examples/AG test/Queries.json @@ -0,0 +1,17 @@ +[ + { + "query": "refinement: G1 <= ((A1 || G2) \\ A2)", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: ((A1 || G2) \\ A2) <= G1", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: ((A1 || G1) \\ A2) <= Imp", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/AG test/SystemDeclarations.json b/Project-Examples/examples/AG test/SystemDeclarations.json new file mode 100644 index 0000000..f1eded6 --- /dev/null +++ b/Project-Examples/examples/AG test/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "A1 = A_Good();\nA2 = A_Good();\nG1 = G();\nG2 = G();\n\nsystem Imp, A1, A2, G1, G2;\n\nIO A1 {button1!, button2!, good?, bad?}\nIO A2 {button1!, button2!, good?, bad?}\n\nIO G1 {button1?, button2?, good!, bad!}\nIO G2 {button1?, button2?, good!, bad!}\nIO Imp {button1?, button2?, good!, bad!}" +} diff --git a/Project-Examples/examples/AG/Components/A.json b/Project-Examples/examples/AG/Components/A.json new file mode 100644 index 0000000..6791599 --- /dev/null +++ b/Project-Examples/examples/AG/Components/A.json @@ -0,0 +1,113 @@ +{ + "name": "A", + "declarations": "// comment\nclock a;\n// comment\nclock b, z;\n// comment\nclock m;", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 240, + "y": 350, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E41", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "bad", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 280, + "y": 330, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E42", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 190, + "y": 340, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E43", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + }, + { + "x": 270, + "y": 400, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "3", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/AG/Components/AA.json b/Project-Examples/examples/AG/Components/AA.json new file mode 100644 index 0000000..6f6fbba --- /dev/null +++ b/Project-Examples/examples/AG/Components/AA.json @@ -0,0 +1,113 @@ +{ + "name": "AA", + "declarations": "", + "locations": [ + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E31", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 170, + "y": 320, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "bad", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 250, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 160, + "y": 280, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E33", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "meh", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/AG/Components/G.json b/Project-Examples/examples/AG/Components/G.json new file mode 100644 index 0000000..639c3d3 --- /dev/null +++ b/Project-Examples/examples/AG/Components/G.json @@ -0,0 +1,113 @@ +{ + "name": "G", + "declarations": "", + "locations": [ + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E21", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E22", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -30 + }, + { + "x": 170, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E23", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 20 + }, + { + "x": 240, + "y": 360, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "1", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/AG/Components/Imp.json b/Project-Examples/examples/AG/Components/Imp.json new file mode 100644 index 0000000..aa63311 --- /dev/null +++ b/Project-Examples/examples/AG/Components/Imp.json @@ -0,0 +1,232 @@ +{ + "name": "Imp", + "declarations": "", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 300, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 430, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E11", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 300, + "y": 270, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 150, + "y": 270, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": -70, + "propertyY": 10 + }, + { + "x": 140, + "y": 440, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E14", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 480, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 10 + }, + { + "x": 180, + "y": 480, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E15", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 390, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 300, + "y": 410, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E16", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "bad", + "isLocked": false, + "nails": [ + { + "x": 300, + "y": 440, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 300, + "y": 470, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E17", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 370, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -30 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "2", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/AG/Components/Q.json b/Project-Examples/examples/AG/Components/Q.json new file mode 100644 index 0000000..ec9bff6 --- /dev/null +++ b/Project-Examples/examples/AG/Components/Q.json @@ -0,0 +1,190 @@ +{ + "name": "Q", + "declarations": "", + "locations": [ + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 180, + "y": 180, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "U10", + "nickname": "", + "invariant": "", + "type": "UNIVERSAL", + "urgency": "NORMAL", + "x": 180, + "y": 300, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "U10", + "targetLocation": "U10", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": true, + "nails": [ + { + "x": 140, + "y": 290, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 120, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 140, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "U10", + "targetLocation": "U10", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": true, + "nails": [ + { + "x": 220, + "y": 290, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 240, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L5", + "targetLocation": "U10", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button2", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "good", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 170, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 190, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "button1", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 150, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 110, + "y": 190, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "8", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/AG/GlobalDeclarations.json b/Project-Examples/examples/AG/GlobalDeclarations.json new file mode 100644 index 0000000..ab3d9a9 --- /dev/null +++ b/Project-Examples/examples/AG/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan button1, button2, good, bad, meh;" +} diff --git a/Project-Examples/examples/AG/Queries.json b/Project-Examples/examples/AG/Queries.json new file mode 100644 index 0000000..367832b --- /dev/null +++ b/Project-Examples/examples/AG/Queries.json @@ -0,0 +1,47 @@ +[ + { + "query": "refinement: (A || G) <= (A || Imp)", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: (A || Imp) <= (A || G)", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: G <= Imp", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: Imp <= G", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: G <= Q", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: Q <= G", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: Q <= Imp", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: Imp <= Q", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: A <= AA", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/AG/SystemDeclarations.json b/Project-Examples/examples/AG/SystemDeclarations.json new file mode 100644 index 0000000..d2cb94a --- /dev/null +++ b/Project-Examples/examples/AG/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Imp, A, G, Q, AA;\n\nIO A {button1!, button2!, good?, bad? }\nIO AA { good?, bad?, meh?}\nIO Imp { button1?, button2?, good!, bad! }\nIO G { button1?, button2?, good!}\nIO Q { button1?, button2?, good! }" +} diff --git a/Project-Examples/examples/Big Refinement/Components/Comp1.json b/Project-Examples/examples/Big Refinement/Components/Comp1.json new file mode 100644 index 0000000..f279287 --- /dev/null +++ b/Project-Examples/examples/Big Refinement/Components/Comp1.json @@ -0,0 +1,435 @@ +{ + "name": "Comp1", + "declarations": "clock x, y, z, k, l;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 20, + "y": 260, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 140, + "y": 260, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 140, + "y": 50, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 280, + "y": 110, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 320, + "y": 150, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 340, + "y": 200, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 250, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L7", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 310, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L8", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 350, + "y": 360, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L9", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 320, + "y": 400, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L10", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 280, + "y": 440, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L11", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 230, + "y": 460, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E11", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "x < 5", + "update": "", + "sync": "i1", + "isLocked": false, + "nails": [ + { + "x": 60, + "y": 260, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 20 + }, + { + "x": 90, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -40 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "x < 5 && y <10 && z < 14 && k <12 && l >= 8", + "update": "x = 0, y = 0, z = 0, k = 0, l = 0", + "sync": "o1", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 220, + "propertyType": "GUARD", + "propertyX": -130, + "propertyY": -40 + }, + { + "x": 140, + "y": 170, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 140, + "y": 130, + "propertyType": "UPDATE", + "propertyX": -110, + "propertyY": -30 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o2", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E14", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o3", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E15", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o4", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E16", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o5", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E17", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L7", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o6", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E18", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o7", + "isLocked": false, + "nails": [ + { + "x": 250, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E19", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L9", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 340, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E20", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L10", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o9", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": 10 + } + ] + }, + { + "id": "E21", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L11", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o10", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 360, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 390, + "height": 490, + "color": "7", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Big Refinement/Components/Ref1.json b/Project-Examples/examples/Big Refinement/Components/Ref1.json new file mode 100644 index 0000000..38ea105 --- /dev/null +++ b/Project-Examples/examples/Big Refinement/Components/Ref1.json @@ -0,0 +1,456 @@ +{ + "name": "Ref1", + "declarations": "clock x, y;", + "locations": [ + { + "id": "L12", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 20, + "y": 240, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L13", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 200, + "y": 240, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L14", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 200, + "y": 150, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L15", + "nickname": "", + "invariant": "x <= 20", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 200, + "y": 320, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -30, + "invariantY": 20 + }, + { + "id": "L16", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 200, + "y": 410, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L17", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 200, + "y": 70, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L18", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 240, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L14", + "status": "INPUT", + "select": "", + "guard": "x <20", + "update": "", + "sync": "i2", + "isLocked": false, + "nails": [ + { + "x": 80, + "y": 180, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 110, + "y": 150, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -30 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L17", + "status": "INPUT", + "select": "", + "guard": "x <= 15", + "update": "", + "sync": "i3", + "isLocked": false, + "nails": [ + { + "x": 20, + "y": 170, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -30 + }, + { + "x": 20, + "y": 70, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -20 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L15", + "status": "INPUT", + "select": "", + "guard": "x <= 8", + "update": "x = 0", + "sync": "i4", + "isLocked": false, + "nails": [ + { + "x": 50, + "y": 280, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -20 + }, + { + "x": 80, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 140, + "y": 320, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -30 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L16", + "status": "INPUT", + "select": "", + "guard": "x < 55", + "update": "", + "sync": "i5", + "isLocked": false, + "nails": [ + { + "x": 20, + "y": 330, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 20, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "x = 0", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 360, + "y": 70, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -20 + }, + { + "x": 360, + "y": 150, + "propertyType": "UPDATE", + "propertyX": -50, + "propertyY": -20 + } + ] + }, + { + "id": "E6", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 360, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -30 + } + ] + }, + { + "id": "E7", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "x > 15", + "update": "", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 320, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 300, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E8", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 150, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E9", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o8", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E30", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L17", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o3", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 50, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -10 + }, + { + "x": 180, + "y": 30, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E31", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L17", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o5", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 30, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 260, + "y": 60, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L14", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i6", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 110, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E33", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "x < 5", + "update": "", + "sync": "i1", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 240, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 140, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -30 + } + ] + } + ], + "description": "", + "x": 287, + "y": 120, + "width": 390, + "height": 440, + "color": "8", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Big Refinement/GlobalDeclarations.json b/Project-Examples/examples/Big Refinement/GlobalDeclarations.json new file mode 100644 index 0000000..d9614f3 --- /dev/null +++ b/Project-Examples/examples/Big Refinement/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan i1, i2, i3, i4, i5, i6, o1, o2, o3, o4, o5, o6, o7, o8, o9, o10;" +} diff --git a/Project-Examples/examples/Big Refinement/Queries.json b/Project-Examples/examples/Big Refinement/Queries.json new file mode 100644 index 0000000..bf736a3 --- /dev/null +++ b/Project-Examples/examples/Big Refinement/Queries.json @@ -0,0 +1,7 @@ +[ + { + "query": "refinement: Ref1 <= Comp1", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Big Refinement/SystemDeclarations.json b/Project-Examples/examples/Big Refinement/SystemDeclarations.json new file mode 100644 index 0000000..58b6c84 --- /dev/null +++ b/Project-Examples/examples/Big Refinement/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Comp1, Ref1;\n\nIO Comp1 {i1?, o1!, o2!, o3!, o4!, o5!, o6!, o7!, o8!, o9!, o10!}\nIO Ref1 {i1?, i2?, i3?, i4?, i5?, i6?, o3!, o5!, o8!}" +} diff --git a/Project-Examples/examples/Car alarm/Components/Alarm.json b/Project-Examples/examples/Car alarm/Components/Alarm.json new file mode 100644 index 0000000..d15c344 --- /dev/null +++ b/Project-Examples/examples/Car alarm/Components/Alarm.json @@ -0,0 +1,953 @@ +{ + "name": "Alarm", + "declarations": "clock x;\non_off_t shutdown;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 330, + "y": 560, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 240, + "y": 470, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 420, + "y": 470, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "x<=25", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 330, + "y": 380, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -50, + "invariantY": -30 + }, + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 330, + "y": 260, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -30, + "invariantY": -40 + }, + { + "id": "L5", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 80, + "y": 260, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": -40 + }, + { + "id": "L6", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 490, + "y": 180, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 20, + "invariantY": -10 + }, + { + "id": "L7", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 330, + "y": 180, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 20 + }, + { + "id": "L8", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 170, + "y": 180, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -60, + "invariantY": -10 + }, + { + "id": "L9", + "nickname": "", + "invariant": "x<=35", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 330, + "y": 100, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 20, + "invariantY": -20 + }, + { + "id": "L10", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 30, + "y": 100, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": -40 + }, + { + "id": "L11", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 30, + "y": 190, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 20, + "invariantY": -10 + }, + { + "id": "L12", + "nickname": "", + "invariant": "x<=305", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 590, + "y": 60, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -60, + "invariantY": -30 + }, + { + "id": "L13", + "nickname": "", + "invariant": "x<=305", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 590, + "y": 210, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -80, + "invariantY": -10 + }, + { + "id": "L14", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 590, + "y": 370, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L15", + "nickname": "", + "invariant": "x<=5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 490, + "y": 310, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 20, + "invariantY": -10 + } + ], + "edges": [ + { + "id": "E0", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "close", + "isLocked": false, + "nails": [ + { + "x": 390, + "y": 440, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -10 + }, + { + "x": 370, + "y": 420, + "propertyType": "UPDATE", + "propertyX": -10, + "propertyY": -30 + } + ] + }, + { + "id": "E1", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "lock", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 440, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 290, + "y": 420, + "propertyType": "UPDATE", + "propertyX": -30, + "propertyY": -30 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "x<=15", + "update": "", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 380, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 240, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -10 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "x<=15", + "update": "", + "sync": "open", + "isLocked": false, + "nails": [ + { + "x": 420, + "y": 380, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 420, + "y": 410, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L7", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "armedOff", + "isLocked": false, + "nails": [ + { + "x": 420, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -30 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "flashOn", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 10 + } + ] + }, + { + "id": "E6", + "group": "", + "sourceLocation": "L8", + "targetLocation": "L9", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "soundOn", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 150, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E7", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L12", + "status": "OUTPUT", + "select": "", + "guard": "x>25", + "update": "", + "sync": "soundOff", + "isLocked": false, + "nails": [ + { + "x": 440, + "y": 100, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 470, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 10 + }, + { + "x": 550, + "y": 100, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E8", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "lock", + "isLocked": false, + "nails": [ + { + "x": 390, + "y": 500, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -10 + } + ] + }, + { + "id": "E9", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L0", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 420, + "y": 560, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E10", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "close", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 500, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E11", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L0", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "open", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 560, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -10 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L0", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 590, + "y": 590, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -30 + }, + { + "x": 350, + "y": 590, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L15", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "close", + "isLocked": false, + "nails": [ + { + "x": 550, + "y": 370, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 490, + "y": 370, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": 10 + } + ] + }, + { + "id": "E14", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "shutdown==0", + "update": "", + "sync": "armedOff", + "isLocked": false, + "nails": [ + { + "x": 80, + "y": 470, + "propertyType": "GUARD", + "propertyX": -40, + "propertyY": 10 + }, + { + "x": 120, + "y": 470, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -30 + } + ] + }, + { + "id": "E15", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L10", + "status": "INPUT", + "select": "", + "guard": "x<=25", + "update": "x=0", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 100, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 200, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 170, + "y": 100, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -30 + } + ] + }, + { + "id": "E16", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L10", + "status": "INPUT", + "select": "", + "guard": "x<=295", + "update": "x=0", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 390, + "y": 60, + "propertyType": "GUARD", + "propertyX": -30, + "propertyY": -30 + }, + { + "x": 330, + "y": 60, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 280, + "y": 60, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 70, + "y": 60, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E17", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "x>15", + "update": "shutdown=0", + "sync": "armedOn", + "isLocked": false, + "nails": [ + { + "x": 330, + "y": 350, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 330, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 330, + "y": 310, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E18", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L6", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "open", + "isLocked": false, + "nails": [ + { + "x": 370, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 220, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E19", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "shutdown=1", + "sync": "armedOn", + "isLocked": false, + "nails": [ + { + "x": 460, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 440, + "y": 260, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E20", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "shutdown==0", + "update": "x=0", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 260, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -30 + }, + { + "x": 200, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 150, + "y": 260, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -30 + } + ] + }, + { + "id": "E21", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "shutdown==1 && x>=395", + "update": "", + "sync": "armedOff", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 320, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 140, + "y": 320, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -30 + }, + { + "x": 140, + "y": 390, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -20 + } + ] + }, + { + "id": "E22", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L11", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "soundOff", + "isLocked": false, + "nails": [ + { + "x": 30, + "y": 140, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E23", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "flashOff", + "isLocked": false, + "nails": [ + { + "x": 30, + "y": 590, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -30 + }, + { + "x": 300, + "y": 590, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E24", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L13", + "status": "OUTPUT", + "select": "", + "guard": "x>295", + "update": "", + "sync": "soundOff", + "isLocked": false, + "nails": [ + { + "x": 590, + "y": 120, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -10 + }, + { + "x": 590, + "y": 140, + "propertyType": "SYNCHRONIZATION", + "propertyX": -70, + "propertyY": -10 + } + ] + }, + { + "id": "E25", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "flashOff", + "isLocked": false, + "nails": [ + { + "x": 590, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": -70, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 620, + "height": 610, + "color": "8", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Car alarm/Components/Env.json b/Project-Examples/examples/Car alarm/Components/Env.json new file mode 100644 index 0000000..0cf71b5 --- /dev/null +++ b/Project-Examples/examples/Car alarm/Components/Env.json @@ -0,0 +1,141 @@ +{ + "name": "Env", + "declarations": "", + "locations": [ + { + "id": "L16", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 110, + "y": 120, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E30", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "open", + "isLocked": false, + "nails": [ + { + "x": 120, + "y": 40, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 100, + "y": 40, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E31", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "close", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 130, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 190, + "y": 110, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "lock", + "isLocked": false, + "nails": [ + { + "x": 100, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -10 + }, + { + "x": 120, + "y": 200, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E33", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "unlock", + "isLocked": false, + "nails": [ + { + "x": 30, + "y": 110, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 30, + "y": 130, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 220, + "height": 220, + "color": "2", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Car alarm/GlobalDeclarations.json b/Project-Examples/examples/Car alarm/GlobalDeclarations.json new file mode 100644 index 0000000..d183886 --- /dev/null +++ b/Project-Examples/examples/Car alarm/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan close, open, lock, unlock, armedOn, armedOff, flashOn, flashOff, soundOn, soundOff;\n\ntypedef int[0,1] on_off_t;" +} diff --git a/Project-Examples/examples/Car alarm/Queries.json b/Project-Examples/examples/Car alarm/Queries.json new file mode 100644 index 0000000..e17f296 --- /dev/null +++ b/Project-Examples/examples/Car alarm/Queries.json @@ -0,0 +1,32 @@ +[ + { + "query": "consistency: Alarm", + "comment": "", + "isPeriodic": false + }, + { + "query": "specification: Alarm", + "comment": "", + "isPeriodic": false + }, + { + "query": "E<> Alarm.L11", + "comment": "", + "isPeriodic": false + }, + { + "query": "E<> Alarm.L12", + "comment": "", + "isPeriodic": false + }, + { + "query": "E<> Alarm.L9", + "comment": "", + "isPeriodic": false + }, + { + "query": "specification: (Alarm : A[] not Alarm.L7 || Alarm.x<=30)", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Car alarm/SystemDeclarations.json b/Project-Examples/examples/Car alarm/SystemDeclarations.json new file mode 100644 index 0000000..a3691fb --- /dev/null +++ b/Project-Examples/examples/Car alarm/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Alarm, Env;\n\nIO Alarm {close?, lock?, open?, unlock?, armedOff!, armedOn!, flashOff!, flashOn!, soundOff!, soundOn!}\nIO Env {open!, close!, lock!, unlock!}" +} diff --git a/Project-Examples/examples/Conjunction/Components/Test1.json b/Project-Examples/examples/Conjunction/Components/Test1.json new file mode 100644 index 0000000..2d32906 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test1.json @@ -0,0 +1,141 @@ +{ + "name": "Test1", + "declarations": "clock x;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 140, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 230, + "y": 330, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E111", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E112", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E113", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 340, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E114", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 130, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 150, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "5", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test10.json b/Project-Examples/examples/Conjunction/Components/Test10.json new file mode 100644 index 0000000..85f091a --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test10.json @@ -0,0 +1,71 @@ +{ + "name": "Test10", + "declarations": "clock y;", + "locations": [ + { + "id": "L26", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 130, + "y": 220, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L28", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 280, + "y": 220, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E101", + "group": "", + "sourceLocation": "L26", + "targetLocation": "L28", + "status": "OUTPUT", + "select": "", + "guard": "y > 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 170, + "y": 220, + "propertyType": "GUARD", + "propertyX": -10, + "propertyY": 10 + }, + { + "x": 220, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "6", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test11.json b/Project-Examples/examples/Conjunction/Components/Test11.json new file mode 100644 index 0000000..173a578 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test11.json @@ -0,0 +1,71 @@ +{ + "name": "Test11", + "declarations": "clock z;", + "locations": [ + { + "id": "L30", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 120, + "y": 200, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L31", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 200, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E91", + "group": "", + "sourceLocation": "L30", + "targetLocation": "L31", + "status": "OUTPUT", + "select": "", + "guard": "z > 5 && z <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 200, + "propertyType": "GUARD", + "propertyX": -40, + "propertyY": 10 + }, + { + "x": 260, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "3", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test12.json b/Project-Examples/examples/Conjunction/Components/Test12.json new file mode 100644 index 0000000..442251e --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test12.json @@ -0,0 +1,64 @@ +{ + "name": "Test12", + "declarations": "", + "locations": [ + { + "id": "L27", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 120, + "y": 210, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L29", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 260, + "y": 210, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E81", + "group": "", + "sourceLocation": "L27", + "targetLocation": "L29", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "5", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test2.json b/Project-Examples/examples/Conjunction/Components/Test2.json new file mode 100644 index 0000000..04de32d --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test2.json @@ -0,0 +1,141 @@ +{ + "name": "Test2", + "declarations": "clock y;", + "locations": [ + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 190, + "y": 140, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 190, + "y": 290, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E71", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E72", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E73", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 130, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 230, + "y": 150, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E74", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 230, + "y": 300, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "1", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test3.json b/Project-Examples/examples/Conjunction/Components/Test3.json new file mode 100644 index 0000000..56fe6fb --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test3.json @@ -0,0 +1,197 @@ +{ + "name": "Test3", + "declarations": "clock z;", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 240, + "y": 160, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 120, + "y": 320, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 320, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E61", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E62", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 240, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E63", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 70, + "y": 310, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 70, + "y": 330, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E64", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 10 + } + ] + }, + { + "id": "E65", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 10 + } + ] + }, + { + "id": "E66", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 350, + "y": 310, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 350, + "y": 330, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "3", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test4.json b/Project-Examples/examples/Conjunction/Components/Test4.json new file mode 100644 index 0000000..4d99583 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test4.json @@ -0,0 +1,239 @@ +{ + "name": "Test4", + "declarations": "clock x;", + "locations": [ + { + "id": "L7", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 160, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L8", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 130, + "y": 310, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L9", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 310, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E51", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L8", + "status": "INPUT", + "select": "", + "guard": "x <= 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 220, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -10 + }, + { + "x": 160, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E52", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L9", + "status": "INPUT", + "select": "", + "guard": "x > 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 220, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 280, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E53", + "group": "", + "sourceLocation": "L8", + "targetLocation": "L9", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -30 + } + ] + }, + { + "id": "E54", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L8", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 0 + } + ] + }, + { + "id": "E55", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L7", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 150, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 260, + "y": 170, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E56", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L9", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 350, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 350, + "y": 320, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E57", + "group": "", + "sourceLocation": "L8", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 90, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test5.json b/Project-Examples/examples/Conjunction/Components/Test5.json new file mode 100644 index 0000000..e98a57a --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test5.json @@ -0,0 +1,456 @@ +{ + "name": "Test5", + "declarations": "clock y;", + "locations": [ + { + "id": "L10", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 90, + "y": 160, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L11", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 290, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L12", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 90, + "y": 290, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L13", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 380, + "y": 280, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L14", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 240, + "y": 420, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L15", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 380, + "y": 150, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E41", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L12", + "status": "INPUT", + "select": "", + "guard": "y <= 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 310, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 140, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": -30 + } + ] + }, + { + "id": "E42", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "y > 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 300, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 320, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": 10 + } + ] + }, + { + "id": "E43", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 340, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E44", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 450, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 250, + "y": 470, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E45", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L12", + "status": "INPUT", + "select": "", + "guard": "y <= 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 150, + "y": 390, + "propertyType": "GUARD", + "propertyX": -10, + "propertyY": 10 + }, + { + "x": 110, + "y": 360, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E46", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "y > 5", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 310, + "y": 380, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 340, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E47", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E48", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L12", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 230, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E49", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L15", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 380, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E410", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L10", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -10 + } + ] + }, + { + "id": "E411", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L12", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 300, + "y": 130, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 180, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E412", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 120, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 290, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E413", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L10", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 70, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -10 + }, + { + "x": 100, + "y": 110, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E414", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L15", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 370, + "y": 110, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 120, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "7", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/Components/Test6.json b/Project-Examples/examples/Conjunction/Components/Test6.json new file mode 100644 index 0000000..a498bf7 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test6.json @@ -0,0 +1,134 @@ +{ + "name": "Test6", + "declarations": "clock x;", + "locations": [ + { + "id": "L16", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 130, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L17", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 260, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E31", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "x <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 110, + "propertyType": "GUARD", + "propertyX": -10, + "propertyY": -30 + }, + { + "x": 280, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 140, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L17", + "status": "OUTPUT", + "select": "", + "guard": "x > 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 170, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E33", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L17", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 250, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 260, + "y": 270, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "9", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Conjunction/Components/Test7.json b/Project-Examples/examples/Conjunction/Components/Test7.json new file mode 100644 index 0000000..92b79c7 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test7.json @@ -0,0 +1,134 @@ +{ + "name": "Test7", + "declarations": "clock y;", + "locations": [ + { + "id": "L18", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 150, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L19", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 290, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E21", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L19", + "status": "OUTPUT", + "select": "", + "guard": "y <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 200, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E22", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "y > 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 130, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 290, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 160, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E23", + "group": "", + "sourceLocation": "L19", + "targetLocation": "L19", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 260, + "y": 300, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "8", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Conjunction/Components/Test8.json b/Project-Examples/examples/Conjunction/Components/Test8.json new file mode 100644 index 0000000..a7f8496 --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test8.json @@ -0,0 +1,281 @@ +{ + "name": "Test8", + "declarations": "clock z;", + "locations": [ + { + "id": "L20", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 110, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L21", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 130, + "y": 220, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L22", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 220, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L23", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 230, + "y": 310, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E11", + "group": "", + "sourceLocation": "L20", + "targetLocation": "L21", + "status": "OUTPUT", + "select": "", + "guard": "z > 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 150, + "propertyType": "GUARD", + "propertyX": -60, + "propertyY": -10 + }, + { + "x": 160, + "y": 190, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L20", + "targetLocation": "L22", + "status": "OUTPUT", + "select": "", + "guard": "z <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 150, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 280, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L21", + "targetLocation": "L23", + "status": "OUTPUT", + "select": "", + "guard": "z <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 160, + "y": 250, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 200, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + } + ] + }, + { + "id": "E14", + "group": "", + "sourceLocation": "L22", + "targetLocation": "L23", + "status": "OUTPUT", + "select": "", + "guard": "z >10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 250, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": 0 + }, + { + "x": 260, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": 0 + } + ] + }, + { + "id": "E15", + "group": "", + "sourceLocation": "L22", + "targetLocation": "L22", + "status": "OUTPUT", + "select": "", + "guard": "z <= 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 350, + "y": 210, + "propertyType": "GUARD", + "propertyX": -30, + "propertyY": -30 + }, + { + "x": 370, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 350, + "y": 230, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E16", + "group": "", + "sourceLocation": "L21", + "targetLocation": "L21", + "status": "OUTPUT", + "select": "", + "guard": "z > 10", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 210, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 70, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": 0 + }, + { + "x": 80, + "y": 230, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E17", + "group": "", + "sourceLocation": "L23", + "targetLocation": "L23", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 260, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 320, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "2", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Conjunction/Components/Test9.json b/Project-Examples/examples/Conjunction/Components/Test9.json new file mode 100644 index 0000000..b93f9ed --- /dev/null +++ b/Project-Examples/examples/Conjunction/Components/Test9.json @@ -0,0 +1,71 @@ +{ + "name": "Test9", + "declarations": "clock x;", + "locations": [ + { + "id": "L24", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 140, + "y": 230, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L25", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 300, + "y": 230, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L24", + "targetLocation": "L25", + "status": "OUTPUT", + "select": "", + "guard": "x <= 5", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 230, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 250, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "4", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Conjunction/GlobalDeclarations.json b/Project-Examples/examples/Conjunction/GlobalDeclarations.json new file mode 100644 index 0000000..6f35cbd --- /dev/null +++ b/Project-Examples/examples/Conjunction/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan a, b;" +} diff --git a/Project-Examples/examples/Conjunction/SystemDeclarations.json b/Project-Examples/examples/Conjunction/SystemDeclarations.json new file mode 100644 index 0000000..1c009e0 --- /dev/null +++ b/Project-Examples/examples/Conjunction/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Test1, Test2, Test3, Test4, Test5, Test6, Test7, Test8, Test9, Test10, Test11, Test12;\n\nIO Test1 { a?, b!}\nIO Test2 { a?, b!}\nIO Test3 { a?, b!}\nIO Test4 { a?, b!}\nIO Test5 { a?, b!}\nIO Test6 { b!}\nIO Test7 { b!}\nIO Test8 { b!}\nIO Test9 { b!}\nIO Test10 { b!}\nIO Test11 { b!}\nIO Test12 { b!}" +} diff --git a/Project-Examples/examples/Delay add/Components/A1.json b/Project-Examples/examples/Delay add/Components/A1.json new file mode 100644 index 0000000..fc8a598 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/A1.json @@ -0,0 +1,204 @@ +{ + "name": "A1", + "declarations": "clock x;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 220, + "y": 110, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 250, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L2", + "nickname": "", + "invariant": "x <= 0", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 390, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 520, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L9", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 90, + "y": 360, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E111", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "x <= 200", + "update": "x = 0", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 150, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 180, + "propertyType": "SYNCHRONIZATION", + "propertyX": 20, + "propertyY": -10 + }, + { + "x": 220, + "y": 210, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E112", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "x <= 100", + "update": "x = 0", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 280, + "propertyType": "GUARD", + "propertyX": 20, + "propertyY": -10 + }, + { + "x": 220, + "y": 310, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 220, + "y": 340, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E113", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 460, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E114", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L9", + "status": "OUTPUT", + "select": "", + "guard": "x == 0", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 160, + "y": 290, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 130, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "1", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/A2.json b/Project-Examples/examples/Delay add/Components/A2.json new file mode 100644 index 0000000..a8dd7cd --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/A2.json @@ -0,0 +1,99 @@ +{ + "name": "A2", + "declarations": "", + "locations": [ + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 210, + "y": 130, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 210, + "y": 260, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L7", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 210, + "y": 370, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E101", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L6", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E102", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L7", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "6", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/B.json b/Project-Examples/examples/Delay add/Components/B.json new file mode 100644 index 0000000..18bebf0 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/B.json @@ -0,0 +1,71 @@ +{ + "name": "B", + "declarations": "clock x;", + "locations": [ + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 60, + "y": 280, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L8", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 270, + "y": 280, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E91", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "x <= 250", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 280, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 20 + }, + { + "x": 170, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "8", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/C1.json b/Project-Examples/examples/Delay add/Components/C1.json new file mode 100644 index 0000000..9a769c0 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/C1.json @@ -0,0 +1,71 @@ +{ + "name": "C1", + "declarations": "clock x;", + "locations": [ + { + "id": "L10", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 110, + "y": 260, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L11", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 270, + "y": 260, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E81", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L11", + "status": "OUTPUT", + "select": "", + "guard": "x <= 5", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 260, + "propertyType": "GUARD", + "propertyX": -10, + "propertyY": 10 + }, + { + "x": 170, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "4", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/C2.json b/Project-Examples/examples/Delay add/Components/C2.json new file mode 100644 index 0000000..2b723b1 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/C2.json @@ -0,0 +1,71 @@ +{ + "name": "C2", + "declarations": "clock x;", + "locations": [ + { + "id": "L12", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 110, + "y": 230, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L13", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 280, + "y": 230, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E71", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L13", + "status": "OUTPUT", + "select": "", + "guard": "x <= 4", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 230, + "propertyType": "GUARD", + "propertyX": 0, + "propertyY": 20 + }, + { + "x": 160, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "2", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/D1.json b/Project-Examples/examples/Delay add/Components/D1.json new file mode 100644 index 0000000..9e1c7c6 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/D1.json @@ -0,0 +1,92 @@ +{ + "name": "D1", + "declarations": "clock x;", + "locations": [ + { + "id": "L14", + "nickname": "", + "invariant": "x <= 6", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 340, + "y": 260, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 30 + }, + { + "id": "L16", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 90, + "y": 260, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E61", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 340, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 180, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E62", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L14", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "7", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/D2.json b/Project-Examples/examples/Delay add/Components/D2.json new file mode 100644 index 0000000..b47e2c6 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/D2.json @@ -0,0 +1,92 @@ +{ + "name": "D2", + "declarations": "clock x;", + "locations": [ + { + "id": "L15", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 140, + "y": 230, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L17", + "nickname": "", + "invariant": "x <= 5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 270, + "y": 230, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 20 + } + ], + "edges": [ + { + "id": "E51", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L17", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o2", + "isLocked": false, + "nails": [ + { + "x": 370, + "y": 190, + "propertyType": "SYNCHRONIZATION", + "propertyX": 0, + "propertyY": -30 + }, + { + "x": 250, + "y": 180, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E52", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L17", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "3", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/E1.json b/Project-Examples/examples/Delay add/Components/E1.json new file mode 100644 index 0000000..8e91f73 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/E1.json @@ -0,0 +1,99 @@ +{ + "name": "E1", + "declarations": "clock x;", + "locations": [ + { + "id": "L18", + "nickname": "", + "invariant": "x <= 3", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 140, + "y": 280, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -30, + "invariantY": 30 + }, + { + "id": "L20", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 280, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L22", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 210, + "y": 160, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E41", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L20", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 220, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + } + ] + }, + { + "id": "E42", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L22", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 170, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "9", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Delay add/Components/E2.json b/Project-Examples/examples/Delay add/Components/E2.json new file mode 100644 index 0000000..e2849c4 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/E2.json @@ -0,0 +1,99 @@ +{ + "name": "E2", + "declarations": "clock x;", + "locations": [ + { + "id": "L19", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 130, + "y": 280, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L21", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 320, + "y": 280, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L23", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 190, + "y": 170, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E31", + "group": "", + "sourceLocation": "L19", + "targetLocation": "L21", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L19", + "targetLocation": "L23", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 160, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "5", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Delay add/Components/T1.json b/Project-Examples/examples/Delay add/Components/T1.json new file mode 100644 index 0000000..665604d --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/T1.json @@ -0,0 +1,141 @@ +{ + "name": "T1", + "declarations": "clock x;", + "locations": [ + { + "id": "L24", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 50, + "y": 210, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L25", + "nickname": "", + "invariant": "x <= 3", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 150, + "y": 210, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 20 + }, + { + "id": "L26", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 260, + "y": 210, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L32", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 380, + "y": 210, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E21", + "group": "", + "sourceLocation": "L24", + "targetLocation": "L25", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "ro", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 10 + } + ] + }, + { + "id": "E22", + "group": "", + "sourceLocation": "L25", + "targetLocation": "L26", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + } + ] + }, + { + "id": "E23", + "group": "", + "sourceLocation": "L26", + "targetLocation": "L32", + "status": "INPUT", + "select": "", + "guard": "x <= 5", + "update": "", + "sync": "ri", + "isLocked": false, + "nails": [ + { + "x": 300, + "y": 210, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 340, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/T2.json b/Project-Examples/examples/Delay add/Components/T2.json new file mode 100644 index 0000000..72ad206 --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/T2.json @@ -0,0 +1,64 @@ +{ + "name": "T2", + "declarations": "clock x;", + "locations": [ + { + "id": "L27", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 140, + "y": 230, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -60, + "invariantY": 30 + }, + { + "id": "L30", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 260, + "y": 230, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E11", + "group": "", + "sourceLocation": "L27", + "targetLocation": "L30", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i", + "isLocked": false, + "nails": [ + { + "x": 200, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "7", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/Components/T3.json b/Project-Examples/examples/Delay add/Components/T3.json new file mode 100644 index 0000000..4ce816a --- /dev/null +++ b/Project-Examples/examples/Delay add/Components/T3.json @@ -0,0 +1,106 @@ +{ + "name": "T3", + "declarations": "clock x;", + "locations": [ + { + "id": "L28", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 120, + "y": 260, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L29", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 240, + "y": 260, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L31", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 390, + "y": 260, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L28", + "targetLocation": "L29", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "ro", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L29", + "targetLocation": "L31", + "status": "INPUT", + "select": "", + "guard": "x <= 5", + "update": "", + "sync": "ri", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 260, + "propertyType": "GUARD", + "propertyX": -30, + "propertyY": 20 + }, + { + "x": 340, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "5", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Delay add/GlobalDeclarations.json b/Project-Examples/examples/Delay add/GlobalDeclarations.json new file mode 100644 index 0000000..7a56bb0 --- /dev/null +++ b/Project-Examples/examples/Delay add/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan a, b, o, p, i, ri, o2, ro;" +} diff --git a/Project-Examples/examples/Delay add/Queries.json b/Project-Examples/examples/Delay add/Queries.json new file mode 100644 index 0000000..2d3d7ba --- /dev/null +++ b/Project-Examples/examples/Delay add/Queries.json @@ -0,0 +1,47 @@ +[ + { + "query": "refinement: (A1 || A2) <= B", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: C1 <= C2", + "comment": "", + "isPeriodic": false + }, + { + "query": "consistency: D1", + "comment": "", + "isPeriodic": false + }, + { + "query": "consistency: C2", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: D1 <= D2", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: E1 <= E2", + "comment": "", + "isPeriodic": false + }, + { + "query": "consistency: T1", + "comment": "", + "isPeriodic": false + }, + { + "query": "refinement: (T1 || T2) <= T3", + "comment": "", + "isPeriodic": false + }, + { + "query": "consistency: T2", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Delay add/SystemDeclarations.json b/Project-Examples/examples/Delay add/SystemDeclarations.json new file mode 100644 index 0000000..78bbba9 --- /dev/null +++ b/Project-Examples/examples/Delay add/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system A1, A2, B, C1, C2, D1, D2, E1, E2, T1, T2, T3, S1, S2;\n\nIO A1 {a!, b!, o!}\nIO A2 {a?, b?}\nIO B {o!}\nIO C1 {o!}\nIO C2 {o!}\nIO D1 {i?, o!}\nIO D2 {i?, o2!}\nIO E1 {i?, o!}\nIO E2 {i?}\nIO T1 {ri?, i?, ro!}\nIO T2 {i!}\nIO T3 {ri?, ro!}\nIO S1 {i?}\nIO S2 {i!}" +} diff --git a/Project-Examples/examples/Ecdar university/Components/Administration 1.json b/Project-Examples/examples/Ecdar university/Components/Administration 1.json new file mode 100644 index 0000000..329d5ce --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Administration 1.json @@ -0,0 +1,309 @@ +{ + "name": "Administration 1", + "declarations": "clock z;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 130, + "y": 100, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "z <= 2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 100, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 50, + "invariantY": -40 + }, + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 310, + "y": 300, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "z<=2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 130, + "y": 300, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 20, + "invariantY": 20 + } + ], + "edges": [ + { + "id": "E44", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "z=0", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 230, + "y": 100, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -30 + } + ] + }, + { + "id": "E45", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 310, + "y": 190, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E46", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "z=0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 250, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -40 + }, + { + "x": 200, + "y": 300, + "propertyType": "UPDATE", + "propertyX": -20, + "propertyY": -40 + } + ] + }, + { + "id": "E47", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 130, + "y": 200, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E48", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 310, + "y": 60, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -20 + }, + { + "x": 290, + "y": 60, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E49", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 350, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 350, + "y": 120, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E50", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 350, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": -40 + }, + { + "x": 350, + "y": 320, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E51", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 130, + "y": 340, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 110, + "y": 340, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E52", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 280, + "propertyType": "SYNCHRONIZATION", + "propertyX": -50, + "propertyY": -20 + }, + { + "x": 90, + "y": 300, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 569, + "y": 407, + "width": 450, + "height": 400, + "color": "5", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Administration 2.json b/Project-Examples/examples/Ecdar university/Components/Administration 2.json new file mode 100644 index 0000000..5801b3b --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Administration 2.json @@ -0,0 +1,379 @@ +{ + "name": "Administration 2", + "declarations": "clock x, y;", + "locations": [ + { + "id": "L20", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 91, + "y": 91, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L21", + "nickname": "", + "invariant": "y <= 2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 321, + "y": 91, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -17, + "invariantY": -39 + }, + { + "id": "L22", + "nickname": "", + "invariant": "x <= 2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 91, + "y": 281, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -15, + "invariantY": 19 + }, + { + "id": "L23", + "nickname": "", + "invariant": "x <= 2 && y <= 2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 331, + "y": 281, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 23, + "invariantY": -7 + } + ], + "edges": [ + { + "id": "E53", + "group": "", + "sourceLocation": "L20", + "targetLocation": "L21", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y = 0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 172, + "y": 70, + "propertyType": "SYNCHRONIZATION", + "propertyX": -12, + "propertyY": -28 + }, + { + "x": 241, + "y": 70, + "propertyType": "UPDATE", + "propertyX": -14.659394792399718, + "propertyY": -25 + } + ] + }, + { + "id": "E54", + "group": "", + "sourceLocation": "L21", + "targetLocation": "L20", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 209, + "y": 124, + "propertyType": "SYNCHRONIZATION", + "propertyX": -19.010907811400422, + "propertyY": 8.335151301900071 + } + ] + }, + { + "id": "E55", + "group": "", + "sourceLocation": "L21", + "targetLocation": "L21", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 363, + "y": 67, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 370, + "y": 86, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E56", + "group": "", + "sourceLocation": "L21", + "targetLocation": "L23", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x = 0", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 367, + "y": 136, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 367, + "y": 208, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E57", + "group": "", + "sourceLocation": "L23", + "targetLocation": "L21", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 272, + "y": 184, + "propertyType": "SYNCHRONIZATION", + "propertyX": -38, + "propertyY": -7 + } + ] + }, + { + "id": "E58", + "group": "", + "sourceLocation": "L23", + "targetLocation": "L23", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 370, + "y": 310, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 354, + "y": 325.33515130190005, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E59", + "group": "", + "sourceLocation": "L23", + "targetLocation": "L23", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 316.692118226601, + "y": 324.98909218859956, + "propertyType": "SYNCHRONIZATION", + "propertyX": -15, + "propertyY": 10 + }, + { + "x": 297.692118226601, + "y": 311.98909218859956, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E60", + "group": "", + "sourceLocation": "L23", + "targetLocation": "L22", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 213, + "y": 255, + "propertyType": "SYNCHRONIZATION", + "propertyX": -18, + "propertyY": -26 + } + ] + }, + { + "id": "E61", + "group": "", + "sourceLocation": "L22", + "targetLocation": "L23", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y = 0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 173, + "y": 305, + "propertyType": "SYNCHRONIZATION", + "propertyX": -11, + "propertyY": 9 + }, + { + "x": 240, + "y": 305, + "propertyType": "UPDATE", + "propertyX": -13, + "propertyY": 10 + } + ] + }, + { + "id": "E62", + "group": "", + "sourceLocation": "L22", + "targetLocation": "L22", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 47, + "y": 270, + "propertyType": "SYNCHRONIZATION", + "propertyX": -16, + "propertyY": -24 + }, + { + "x": 47, + "y": 301, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E63", + "group": "", + "sourceLocation": "L22", + "targetLocation": "L20", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 158, + "y": 186, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E64", + "group": "", + "sourceLocation": "L20", + "targetLocation": "L22", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x = 0", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 44, + "y": 135, + "propertyType": "SYNCHRONIZATION", + "propertyX": 11, + "propertyY": -3 + }, + { + "x": 44, + "y": 204, + "propertyType": "UPDATE", + "propertyX": 11, + "propertyY": -8 + } + ] + } + ], + "description": "", + "x": 635, + "y": 416, + "width": 450, + "height": 381, + "color": "0", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Ecdar university/Components/Coffee Machine 1.json b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 1.json new file mode 100644 index 0000000..b573c7c --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 1.json @@ -0,0 +1,141 @@ +{ + "name": "Coffee Machine 1", + "declarations": "", + "locations": [ + { + "id": "L10", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 110, + "y": 150, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L11", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 110, + "y": 100, + "color": "3", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E21", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L10", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 150, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": 20, + "propertyY": -7.5 + } + ] + }, + { + "id": "E22", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L10", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 205, + "propertyType": "SYNCHRONIZATION", + "propertyX": -45, + "propertyY": -7.5 + }, + { + "x": 130, + "y": 205, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E23", + "group": "", + "sourceLocation": "L11", + "targetLocation": "L11", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 130, + "y": 55, + "propertyType": "SYNCHRONIZATION", + "propertyX": 20, + "propertyY": -7.5 + }, + { + "x": 85, + "y": 55, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E24", + "group": "", + "sourceLocation": "L10", + "targetLocation": "L11", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 61, + "y": 101, + "propertyType": "SYNCHRONIZATION", + "propertyX": -45, + "propertyY": -7.5 + } + ] + } + ], + "description": "", + "x": 438, + "y": 487, + "width": 230, + "height": 240, + "color": "3", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Coffee Machine 2.json b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 2.json new file mode 100644 index 0000000..c453226 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 2.json @@ -0,0 +1,162 @@ +{ + "name": "Coffee Machine 2", + "declarations": "clock y;", + "locations": [ + { + "id": "L8", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 125, + "y": 77, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L19", + "nickname": "", + "invariant": "y <= 5", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 125, + "y": 220, + "color": "4", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 1, + "invariantY": 30 + } + ], + "edges": [ + { + "id": "E17", + "group": "", + "sourceLocation": "L8", + "targetLocation": "L19", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y = 0", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 165, + "y": 127, + "propertyType": "SYNCHRONIZATION", + "propertyX": 18, + "propertyY": -7.5 + }, + { + "x": 165, + "y": 178, + "propertyType": "UPDATE", + "propertyX": 20, + "propertyY": -9 + } + ] + }, + { + "id": "E18", + "group": "", + "sourceLocation": "L19", + "targetLocation": "L19", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 204, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 204, + "y": 255, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E19", + "group": "", + "sourceLocation": "L8", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "y >= 2", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 209, + "y": 77, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 209, + "y": 42, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 168, + "y": 42, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E20", + "group": "", + "sourceLocation": "L19", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "y >= 4", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 75, + "y": 176, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -8 + }, + { + "x": 75, + "y": 127, + "propertyType": "SYNCHRONIZATION", + "propertyX": -44, + "propertyY": -8 + } + ] + } + ], + "description": "", + "x": 407, + "y": 456, + "width": 292, + "height": 301, + "color": "4", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Coffee Machine 3.json b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 3.json new file mode 100644 index 0000000..c4e71d4 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 3.json @@ -0,0 +1,190 @@ +{ + "name": "Coffee Machine 3", + "declarations": "clock y;", + "locations": [ + { + "id": "L4", + "nickname": "", + "invariant": "y<=6", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 111.5, + "y": 286.5, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 29.5, + "invariantY": -7.5 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 111.5, + "y": 86.5, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "y>=4", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 67.5, + "y": 214.5, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -7.5 + }, + { + "x": 67.5, + "y": 164.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": -44, + "propertyY": -7.5 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 155.5, + "y": 241.5, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 168.5, + "y": 190.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": 14.5, + "propertyY": -7.5 + }, + { + "x": 155.5, + "y": 137.5, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y=0", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 111.5, + "y": 206.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": 12, + "propertyY": -7 + }, + { + "x": 111.5, + "y": 176, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 96.5, + "y": 331, + "propertyType": "SYNCHRONIZATION", + "propertyX": -45, + "propertyY": -7.5 + }, + { + "x": 127, + "y": 331, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "y<0", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 133, + "y": 43.5, + "propertyType": "GUARD", + "propertyX": 17, + "propertyY": -8 + }, + { + "x": 93, + "y": 43.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": -38, + "propertyY": -8 + } + ] + } + ], + "description": "", + "x": 443, + "y": 429, + "width": 220, + "height": 356, + "color": "7", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Coffee Machine 4.json b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 4.json new file mode 100644 index 0000000..2b668bf --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Coffee Machine 4.json @@ -0,0 +1,190 @@ +{ + "name": "Coffee Machine 4", + "declarations": "clock y;", + "locations": [ + { + "id": "L24", + "nickname": "", + "invariant": "y<=6", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 111.5, + "y": 286.5, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 29.5, + "invariantY": -7.5 + }, + { + "id": "L25", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 111.5, + "y": 86.5, + "color": "7", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E71", + "group": "", + "sourceLocation": "L24", + "targetLocation": "L25", + "status": "OUTPUT", + "select": "", + "guard": "y>=4", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 67.5, + "y": 214.5, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": -7.5 + }, + { + "x": 67.5, + "y": 164.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": -44, + "propertyY": -7.5 + } + ] + }, + { + "id": "E72", + "group": "", + "sourceLocation": "L24", + "targetLocation": "L25", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 155.5, + "y": 241.5, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 168.5, + "y": 190.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": 14.5, + "propertyY": -7.5 + }, + { + "x": 155.5, + "y": 137.5, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E73", + "group": "", + "sourceLocation": "L25", + "targetLocation": "L24", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y=0", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 111.5, + "y": 206.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": 12, + "propertyY": -7 + }, + { + "x": 111.5, + "y": 176, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E74", + "group": "", + "sourceLocation": "L24", + "targetLocation": "L24", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 96.5, + "y": 331, + "propertyType": "SYNCHRONIZATION", + "propertyX": -45, + "propertyY": -7.5 + }, + { + "x": 127, + "y": 331, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E75", + "group": "", + "sourceLocation": "L25", + "targetLocation": "L25", + "status": "OUTPUT", + "select": "", + "guard": "y>=2", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 133, + "y": 43.5, + "propertyType": "GUARD", + "propertyX": 17, + "propertyY": -8 + }, + { + "x": 93, + "y": 43.5, + "propertyType": "SYNCHRONIZATION", + "propertyX": -38, + "propertyY": -8 + } + ] + } + ], + "description": "", + "x": 443, + "y": 429, + "width": 220, + "height": 356, + "color": "7", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Half Administration 1.json b/Project-Examples/examples/Ecdar university/Components/Half Administration 1.json new file mode 100644 index 0000000..0386166 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Half Administration 1.json @@ -0,0 +1,239 @@ +{ + "name": "Half Administration 1", + "declarations": "clock x;", + "locations": [ + { + "id": "L12", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 70, + "y": 118, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L13", + "nickname": "", + "invariant": "x<=2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 243, + "y": 119, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -37, + "invariantY": -33 + } + ], + "edges": [ + { + "id": "E37", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 134, + "y": 141, + "propertyType": "SYNCHRONIZATION", + "propertyX": -14, + "propertyY": 9 + }, + { + "x": 179, + "y": 141, + "propertyType": "UPDATE", + "propertyX": -12, + "propertyY": 9 + } + ] + }, + { + "id": "E38", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L12", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 180, + "y": 100, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 136, + "y": 98, + "propertyType": "SYNCHRONIZATION", + "propertyX": -14, + "propertyY": -24 + } + ] + }, + { + "id": "E39", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L13", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 253, + "y": 56, + "propertyType": "SYNCHRONIZATION", + "propertyX": -18, + "propertyY": -24 + }, + { + "x": 279, + "y": 71, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E40", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 301, + "y": 105, + "propertyType": "SYNCHRONIZATION", + "propertyX": -11, + "propertyY": -25 + }, + { + "x": 301, + "y": 135, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E41", + "group": "", + "sourceLocation": "L13", + "targetLocation": "L13", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 247.89868147120055, + "y": 176.73421235253295, + "propertyType": "SYNCHRONIZATION", + "propertyX": -13, + "propertyY": 9 + }, + { + "x": 277, + "y": 160, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E42", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L12", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 60, + "y": 58, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -27 + }, + { + "x": 27, + "y": 78, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E43", + "group": "", + "sourceLocation": "L12", + "targetLocation": "L12", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 61.36710617626648, + "y": 177.06315058986814, + "propertyType": "SYNCHRONIZATION", + "propertyX": -17, + "propertyY": 9 + }, + { + "x": 26, + "y": 155, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 556, + "y": 497, + "width": 329, + "height": 220, + "color": "2", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Half Administration 2.json b/Project-Examples/examples/Ecdar university/Components/Half Administration 2.json new file mode 100644 index 0000000..60da38f --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Half Administration 2.json @@ -0,0 +1,239 @@ +{ + "name": "Half Administration 2", + "declarations": "clock y;", + "locations": [ + { + "id": "L14", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 76.89114489105513, + "y": 119.0376235539684, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L15", + "nickname": "", + "invariant": "y<=2", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 261.8374549289125, + "y": 119.90830522533889, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -40.190012356271055, + "invariantY": -34.49605273874029 + } + ], + "edges": [ + { + "id": "E30", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L15", + "status": "INPUT", + "select": "", + "guard": "", + "update": "y=0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 142.66233599965273, + "y": 141.40845647420008, + "propertyType": "SYNCHRONIZATION", + "propertyX": -8.372039554055217, + "propertyY": 10.042224968060236 + }, + { + "x": 189.4275275917933, + "y": 142.45857596477973, + "propertyType": "UPDATE", + "propertyX": -11.712410382065254, + "propertyY": 7.815311082720207 + } + ] + }, + { + "id": "E31", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 190.9893984400012, + "y": 96.26909353541649, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 144.97369982111329, + "y": 95.73560934069943, + "propertyType": "SYNCHRONIZATION", + "propertyX": -17.153020191234617, + "propertyY": -27.2585826113852 + } + ] + }, + { + "id": "E32", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L15", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 274.74777218976817, + "y": 175.58115235883952, + "propertyType": "SYNCHRONIZATION", + "propertyX": -14.348265350529463, + "propertyY": 11.155681910730248 + }, + { + "x": 298.1092555018084, + "y": 158.83707325072905, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E33", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L15", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 318.1092555018084, + "y": 109.45270297499508, + "propertyType": "SYNCHRONIZATION", + "propertyX": -11.813536603056452, + "propertyY": -29.54883394881558 + }, + { + "x": 318.4381828479714, + "y": 135.13388825093105, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E34", + "group": "", + "sourceLocation": "L15", + "targetLocation": "L15", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 274.48608423897133, + "y": 63.68706776293859, + "propertyType": "SYNCHRONIZATION", + "propertyX": -16.124013184685072, + "propertyY": -27.697180385037715 + }, + { + "x": 299.98169335779573, + "y": 75.7917429432573, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E35", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L14", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 66.4508256860921, + "y": 176.24719226370794, + "propertyType": "SYNCHRONIZATION", + "propertyX": -16.51439543828484, + "propertyY": 10.263631624674183 + }, + { + "x": 34.507844945498945, + "y": 156.0804241865535, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E36", + "group": "", + "sourceLocation": "L14", + "targetLocation": "L14", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 70.9349255784252, + "y": 62.04308398261528, + "propertyType": "SYNCHRONIZATION", + "propertyX": -12.676625902434262, + "propertyY": -26.05200707028724 + }, + { + "x": 35.32953248148583, + "y": 81.1907352204371, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 682, + "y": 487, + "width": 355.0582859210015, + "height": 239.44828437149366, + "color": "1", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Researcher.json b/Project-Examples/examples/Ecdar university/Components/Researcher.json new file mode 100644 index 0000000..c368fb0 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Researcher.json @@ -0,0 +1,414 @@ +{ + "name": "Researcher", + "declarations": "clock x;", + "locations": [ + { + "id": "L6", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 296, + "y": 97, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L7", + "nickname": "", + "invariant": "x <= 8", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 297, + "y": 233, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -15, + "invariantY": 17 + }, + { + "id": "L9", + "nickname": "", + "invariant": "x<=4", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 89, + "y": 96, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 13, + "invariantY": 15 + }, + { + "id": "U80", + "nickname": "", + "invariant": "", + "type": "UNIVERSAL", + "urgency": "NORMAL", + "x": 429, + "y": 97, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E6", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L9", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 49, + "y": 76, + "propertyType": "SYNCHRONIZATION", + "propertyX": -35, + "propertyY": -9 + }, + { + "x": 49, + "y": 96, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E7", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L9", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 69, + "y": 136, + "propertyType": "SYNCHRONIZATION", + "propertyX": -12, + "propertyY": 10 + }, + { + "x": 89, + "y": 136, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E8", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L7", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 255, + "y": 255, + "propertyType": "SYNCHRONIZATION", + "propertyX": -33, + "propertyY": -8 + }, + { + "x": 256, + "y": 233, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E9", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L7", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 337, + "y": 253, + "propertyType": "SYNCHRONIZATION", + "propertyX": 12, + "propertyY": -7 + }, + { + "x": 337, + "y": 233, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E10", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L9", + "status": "INPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "cof", + "isLocked": false, + "nails": [ + { + "x": 226, + "y": 108, + "propertyType": "SYNCHRONIZATION", + "propertyX": -21, + "propertyY": 10 + }, + { + "x": 157, + "y": 108, + "propertyType": "UPDATE", + "propertyX": 0, + "propertyY": 9 + } + ] + }, + { + "id": "E11", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L7", + "status": "INPUT", + "select": "", + "guard": "x<=15", + "update": "x=0", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 276, + "y": 147, + "propertyType": "GUARD", + "propertyX": -47, + "propertyY": -7 + }, + { + "x": 276, + "y": 167, + "propertyType": "SYNCHRONIZATION", + "propertyX": -33, + "propertyY": -7 + }, + { + "x": 276, + "y": 187, + "propertyType": "UPDATE", + "propertyX": -35, + "propertyY": -8 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L9", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "x>=2", + "update": "x=0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 156, + "y": 77, + "propertyType": "GUARD", + "propertyX": -15, + "propertyY": -26 + }, + { + "x": 191, + "y": 77, + "propertyType": "SYNCHRONIZATION", + "propertyX": -11, + "propertyY": -25 + }, + { + "x": 226, + "y": 77, + "propertyType": "UPDATE", + "propertyX": -12, + "propertyY": -25 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L7", + "targetLocation": "L6", + "status": "OUTPUT", + "select": "", + "guard": "x>=4", + "update": "x=0", + "sync": "pub", + "isLocked": false, + "nails": [ + { + "x": 315, + "y": 188, + "propertyType": "GUARD", + "propertyX": 13, + "propertyY": -8 + }, + { + "x": 316, + "y": 168, + "propertyType": "SYNCHRONIZATION", + "propertyX": 14, + "propertyY": -8 + }, + { + "x": 316, + "y": 146, + "propertyType": "UPDATE", + "propertyX": 13, + "propertyY": -8 + } + ] + }, + { + "id": "E14", + "group": "", + "sourceLocation": "U80", + "targetLocation": "U80", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": true, + "nails": [ + { + "x": 389, + "y": 87, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 369, + "y": 97, + "propertyType": "SYNCHRONIZATION", + "propertyX": -32, + "propertyY": -7 + }, + { + "x": 389, + "y": 107, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E15", + "group": "", + "sourceLocation": "U80", + "targetLocation": "U80", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "*", + "isLocked": true, + "nails": [ + { + "x": 469, + "y": 87, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 489, + "y": 97, + "propertyType": "SYNCHRONIZATION", + "propertyX": 11, + "propertyY": -8 + }, + { + "x": 469, + "y": 107, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E16", + "group": "", + "sourceLocation": "L6", + "targetLocation": "U80", + "status": "INPUT", + "select": "", + "guard": "x>15", + "update": "", + "sync": "tea", + "isLocked": false, + "nails": [ + { + "x": 329, + "y": 57, + "propertyType": "GUARD", + "propertyX": -16, + "propertyY": -25 + }, + { + "x": 379, + "y": 57, + "propertyType": "SYNCHRONIZATION", + "propertyX": -11, + "propertyY": -27 + } + ] + } + ], + "description": "", + "x": 451, + "y": 467, + "width": 538, + "height": 278, + "color": "8", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/Components/Specification.json b/Project-Examples/examples/Ecdar university/Components/Specification.json new file mode 100644 index 0000000..9af83ee --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Components/Specification.json @@ -0,0 +1,246 @@ +{ + "name": "Specification", + "declarations": "clock u;", + "locations": [ + { + "id": "L16", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 203.91394864677306, + "y": 127.21721027064538, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L17", + "nickname": "", + "invariant": "u<=20", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 333.91394864677306, + "y": 127.21721027064538, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -56.39139486467731, + "invariantY": -8.195697432338653 + }, + { + "id": "L18", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 53.91394864677307, + "y": 127.21721027064538, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E80", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L17", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 373.3707002245025, + "y": 115.26574498069328, + "propertyType": "SYNCHRONIZATION", + "propertyX": -15.940319222761971, + "propertyY": -26.391394864677306 + }, + { + "x": 373.3707002245025, + "y": 140.69822920339877, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E81", + "group": "", + "sourceLocation": "L17", + "targetLocation": "L16", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "u=0", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 333.91394864677306, + "y": 197.21721027064538, + "propertyType": "SYNCHRONIZATION", + "propertyX": -18.195697432338655, + "propertyY": 8.64677307425399 + }, + { + "x": 270.07633587786256, + "y": 198.11936155447606, + "propertyType": "UPDATE", + "propertyX": -10.97848716169327, + "propertyY": 10.527411519777932 + }, + { + "x": 203.91394864677306, + "y": 197.21721027064538, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E82", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L18", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "patent", + "isLocked": false, + "nails": [ + { + "x": 53.91394864677307, + "y": 87.21721027064538, + "propertyType": "SYNCHRONIZATION", + "propertyX": -19.097848716169327, + "propertyY": -26.391394864677306 + }, + { + "x": 33.91394864677307, + "y": 87.21721027064538, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E83", + "group": "", + "sourceLocation": "L18", + "targetLocation": "L18", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 53.31020124913254, + "y": 167.66828591256072, + "propertyType": "SYNCHRONIZATION", + "propertyX": -15.489243580846631, + "propertyY": 12.706453851492022 + }, + { + "x": 32.71339347675225, + "y": 167.21721027064538, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E84", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L17", + "status": "INPUT", + "select": "", + "guard": "u<=2", + "update": "u=0", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 203.91394864677306, + "y": 87.21721027064538, + "propertyType": "GUARD", + "propertyX": 13.157529493407356, + "propertyY": -8.195697432338653 + }, + { + "x": 203.91394864677306, + "y": 57.21721027064538, + "propertyType": "SYNCHRONIZATION", + "propertyX": -14.809160305343514, + "propertyY": -25.66828591256072 + }, + { + "x": 268.5773768216516, + "y": 57.21721027064538, + "propertyType": "UPDATE", + "propertyX": -13.23386537126995, + "propertyY": -25.66828591256072 + }, + { + "x": 333.91394864677306, + "y": 57.21721027064538, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E85", + "group": "", + "sourceLocation": "L16", + "targetLocation": "L18", + "status": "INPUT", + "select": "", + "guard": "u>2", + "update": "", + "sync": "grant", + "isLocked": false, + "nails": [ + { + "x": 163.91394864677306, + "y": 127.21721027064538, + "propertyType": "GUARD", + "propertyX": -12.782789729354615, + "propertyY": -26.391394864677306 + }, + { + "x": 113.91394864677306, + "y": 127.21721027064538, + "propertyType": "SYNCHRONIZATION", + "propertyX": -15.940319222761971, + "propertyY": -25.489243580846633 + } + ] + } + ], + "description": "", + "x": 353, + "y": 487, + "width": 400.8327550312283, + "height": 238.88757807078417, + "color": "6", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Ecdar university/GlobalDeclarations.json b/Project-Examples/examples/Ecdar university/GlobalDeclarations.json new file mode 100644 index 0000000..69aa085 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan pub, grant, patent, coin, tea, cof;" +} diff --git a/Project-Examples/examples/Ecdar university/Queries.json b/Project-Examples/examples/Ecdar university/Queries.json new file mode 100644 index 0000000..be12da2 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Queries.json @@ -0,0 +1,50 @@ +[ + { + "query": "specification: (Administration 1 || Coffee Machine 1 || Researcher)", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "specification: Specification", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "consistency: (Administration 1 || Coffee Machine 1 || Researcher)", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "consistency: (Administration 1 || Coffee Machine 1 || Researcher)", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "refinement: (Administration 1 || Coffee Machine 2 || Researcher) <= Specification", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "refinement: Coffee Machine 3 <= Coffee Machine 3", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "refinement: (Half Administration 1 && Half Administration 2) <= Administration 2", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + }, + { + "query": "refinement: Administration 2 <= (Half Administration 1 && Half Administration 2)", + "comment": "", + "isPeriodic": false, + "engine": "Reveaal" + } +] diff --git a/Project-Examples/examples/Ecdar university/Systems/University Example.json b/Project-Examples/examples/Ecdar university/Systems/University Example.json new file mode 100644 index 0000000..4cadb20 --- /dev/null +++ b/Project-Examples/examples/Ecdar university/Systems/University Example.json @@ -0,0 +1,76 @@ +{ + "name": "University Example", + "description": "", + "x": 590, + "y": 402, + "width": 540, + "height": 410, + "color": "5", + "systemRootX": 240, + "componentInstances": [ + { + "id": 1, + "componentName": "Coffee Machine 4", + "x": 10, + "y": 110 + }, + { + "id": 3, + "componentName": "Researcher", + "x": 310, + "y": 110 + }, + { + "id": 5, + "componentName": "Half Administration 1", + "x": 10, + "y": 280 + }, + { + "id": 6, + "componentName": "Half Administration 2", + "x": 310, + "y": 280 + } + ], + "operators": [ + { + "id": 2, + "type": "composition", + "x": 250, + "y": 60 + }, + { + "id": 4, + "type": "conjunction", + "x": 250, + "y": 230 + } + ], + "edges": [ + { + "child": 2, + "parent": 0 + }, + { + "child": 1, + "parent": 2 + }, + { + "child": 3, + "parent": 2 + }, + { + "child": 4, + "parent": 2 + }, + { + "child": 5, + "parent": 4 + }, + { + "child": 6, + "parent": 4 + } + ] +} diff --git a/Project-Examples/examples/Fish retailer/Components/Retailer.json b/Project-Examples/examples/Fish retailer/Components/Retailer.json new file mode 100644 index 0000000..30ab4f6 --- /dev/null +++ b/Project-Examples/examples/Fish retailer/Components/Retailer.json @@ -0,0 +1,169 @@ +{ + "name": "Retailer", + "declarations": "clock x;\n\nbool_t free;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 150, + "y": 80, + "color": "6", + "nicknameX": 50, + "nicknameY": -60, + "invariantX": 60, + "invariantY": -30 + }, + { + "id": "L1", + "nickname": "", + "invariant": "x<=4", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 370, + "y": 80, + "color": "6", + "nicknameX": 60, + "nicknameY": -50, + "invariantX": -20, + "invariantY": -40 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "x>4", + "update": "x=0, free=1", + "sync": "coin", + "isLocked": false, + "nails": [ + { + "x": 250, + "y": 80, + "propertyType": "GUARD", + "propertyX": -30, + "propertyY": -30 + }, + { + "x": 280, + "y": 80, + "propertyType": "SYNCHRONIZATION", + "propertyX": -20, + "propertyY": 10 + }, + { + "x": 310, + "y": 80, + "propertyType": "UPDATE", + "propertyX": -40, + "propertyY": -30 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "x<3 && free==1", + "update": "free=0", + "sync": "garnish", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 40, + "propertyType": "GUARD", + "propertyX": -90, + "propertyY": -10 + }, + { + "x": 110, + "y": 80, + "propertyType": "SYNCHRONIZATION", + "propertyX": -70, + "propertyY": -10 + }, + { + "x": 110, + "y": 120, + "propertyType": "UPDATE", + "propertyX": -50, + "propertyY": -10 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "garnish", + "isLocked": false, + "nails": [ + { + "x": 310, + "y": 40, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + }, + { + "x": 250, + "y": 40, + "propertyType": "SYNCHRONIZATION", + "propertyX": -80, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "x>1", + "update": "", + "sync": "tuna", + "isLocked": false, + "nails": [ + { + "x": 310, + "y": 120, + "propertyType": "GUARD", + "propertyX": 20, + "propertyY": -10 + }, + { + "x": 250, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": -60, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 400, + "height": 140, + "color": "6", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Fish retailer/GlobalDeclarations.json b/Project-Examples/examples/Fish retailer/GlobalDeclarations.json new file mode 100644 index 0000000..597f9d8 --- /dev/null +++ b/Project-Examples/examples/Fish retailer/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan coin, tuna, garnish;\n\ntypedef int[0,1] bool_t;" +} diff --git a/Project-Examples/examples/Fish retailer/Queries.json b/Project-Examples/examples/Fish retailer/Queries.json new file mode 100644 index 0000000..972568a --- /dev/null +++ b/Project-Examples/examples/Fish retailer/Queries.json @@ -0,0 +1,7 @@ +[ + { + "query": "consistency: Retailer", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Fish retailer/SystemDeclarations.json b/Project-Examples/examples/Fish retailer/SystemDeclarations.json new file mode 100644 index 0000000..ee5f01c --- /dev/null +++ b/Project-Examples/examples/Fish retailer/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Retailer;\n\nIO Retailer {coin?, tuna!, garnish!}" +} diff --git a/Project-Examples/examples/Input enabled/Components/Automaton.json b/Project-Examples/examples/Input enabled/Components/Automaton.json new file mode 100644 index 0000000..3dbb4d7 --- /dev/null +++ b/Project-Examples/examples/Input enabled/Components/Automaton.json @@ -0,0 +1,183 @@ +{ + "name": "Automaton", + "declarations": "clock x, y;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 80, + "y": 250, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "x <= 10", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 220, + "y": 120, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 30 + }, + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 320, + "y": 260, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 280, + "y": 380, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 380, + "y": 120, + "color": "2", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i1", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 190, + "propertyType": "SYNCHRONIZATION", + "propertyX": -30, + "propertyY": -20 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "x >= 3 && x <= 5 && y >= 4", + "update": "", + "sync": "i2", + "isLocked": false, + "nails": [ + { + "x": 130, + "y": 250, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 30 + }, + { + "x": 220, + "y": 250, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": 0 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "x <= 2 && y <= 3", + "update": "", + "sync": "i2", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 310, + "propertyType": "GUARD", + "propertyX": -60, + "propertyY": 20 + }, + { + "x": 210, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": 20 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L4", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "o", + "isLocked": false, + "nails": [ + { + "x": 300, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "2", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Input enabled/GlobalDeclarations.json b/Project-Examples/examples/Input enabled/GlobalDeclarations.json new file mode 100644 index 0000000..476befc --- /dev/null +++ b/Project-Examples/examples/Input enabled/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan i1, i2, o;" +} diff --git a/Project-Examples/examples/Input enabled/Queries.json b/Project-Examples/examples/Input enabled/Queries.json new file mode 100644 index 0000000..ca14ab7 --- /dev/null +++ b/Project-Examples/examples/Input enabled/Queries.json @@ -0,0 +1,7 @@ +[ + { + "query": "consistency: Automaton", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Input enabled/SystemDeclarations.json b/Project-Examples/examples/Input enabled/SystemDeclarations.json new file mode 100644 index 0000000..b565635 --- /dev/null +++ b/Project-Examples/examples/Input enabled/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Automaton;\n\nIO Automaton {i1?, i2?, o!}" +} diff --git a/Project-Examples/examples/Sender receiver/Components/Receiver.json b/Project-Examples/examples/Sender receiver/Components/Receiver.json new file mode 100644 index 0000000..8817624 --- /dev/null +++ b/Project-Examples/examples/Sender receiver/Components/Receiver.json @@ -0,0 +1,120 @@ +{ + "name": "Receiver", + "declarations": "", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 20, + "y": 50, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 20, + "y": 160, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 170, + "y": 50, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 90, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": 10 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 50, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 20, + "y": 100, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 190, + "height": 180, + "color": "5", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Sender receiver/Components/Sender.json b/Project-Examples/examples/Sender receiver/Components/Sender.json new file mode 100644 index 0000000..53447a7 --- /dev/null +++ b/Project-Examples/examples/Sender receiver/Components/Sender.json @@ -0,0 +1,141 @@ +{ + "name": "Sender", + "declarations": "", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 190, + "y": 50, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 20, + "y": 170, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 20, + "y": 50, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E10", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 190, + "y": 170, + "propertyType": "SYNCHRONIZATION", + "propertyX": -40, + "propertyY": -30 + } + ] + }, + { + "id": "E11", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 50, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -20 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 70, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L5", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 20, + "y": 120, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 210, + "height": 190, + "color": "9", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Sender receiver/GlobalDeclarations.json b/Project-Examples/examples/Sender receiver/GlobalDeclarations.json new file mode 100644 index 0000000..15fd7a7 --- /dev/null +++ b/Project-Examples/examples/Sender receiver/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan c, b;" +} diff --git a/Project-Examples/examples/Sender receiver/Queries.json b/Project-Examples/examples/Sender receiver/Queries.json new file mode 100644 index 0000000..16a9106 --- /dev/null +++ b/Project-Examples/examples/Sender receiver/Queries.json @@ -0,0 +1,27 @@ +[ + { + "query": "E<> Receiver.L4", + "comment": "", + "isPeriodic": false + }, + { + "query": "specification: Sender", + "comment": "", + "isPeriodic": false + }, + { + "query": "implementation: Sender", + "comment": "", + "isPeriodic": false + }, + { + "query": "specification: Receiver", + "comment": "", + "isPeriodic": false + }, + { + "query": "implementation: Receiver", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Sender receiver/SystemDeclarations.json b/Project-Examples/examples/Sender receiver/SystemDeclarations.json new file mode 100644 index 0000000..2844f27 --- /dev/null +++ b/Project-Examples/examples/Sender receiver/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Sender, Receiver;\n\nIO Sender {c!}\nIO Receiver {c?}" +} diff --git a/Project-Examples/examples/Simple mutation/Components/Component 1.json b/Project-Examples/examples/Simple mutation/Components/Component 1.json new file mode 100644 index 0000000..528f47a --- /dev/null +++ b/Project-Examples/examples/Simple mutation/Components/Component 1.json @@ -0,0 +1,183 @@ +{ + "name": "Component1", + "declarations": "clock x;", + "locations": [ + { + "id": "L0", + "type": "INITIAL", + "urgency": "NORMAL", + "color": "2", + "x": 250, + "y": 280, + "nickname": "", + "nicknameX": 30, + "nicknameY": -10, + "invariant": "", + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "type": "NORMAL", + "urgency": "NORMAL", + "color": "2", + "x": 130, + "y": 400, + "nickname": "", + "nicknameX": 30, + "nicknameY": -10, + "invariant": "", + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L2", + "type": "NORMAL", + "urgency": "NORMAL", + "color": "2", + "x": 370, + "y": 400, + "nickname": "", + "nicknameX": 30, + "nicknameY": -10, + "invariant": "x<=7", + "invariantX": 20, + "invariantY": -40 + }, + { + "id": "L3", + "type": "NORMAL", + "urgency": "NORMAL", + "color": "2", + "x": 250, + "y": 520, + "nickname": "", + "nicknameX": 30, + "nicknameY": -10, + "invariant": "", + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 170, + "y": 360, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L2", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "x=0", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 290, + "y": 320, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 330, + "y": 360, + "propertyType": "UPDATE", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "x>=4 && x<=5", + "update": "", + "sync": "c", + "isLocked": false, + "nails": [ + { + "x": 210, + "y": 400, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -30 + }, + { + "x": 290, + "y": 400, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "x>=2", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 330, + "y": 440, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 290, + "y": 480, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "2", + "includeInPeriodicCheck": false +} diff --git a/Project-Examples/examples/Simple mutation/GlobalDeclarations.json b/Project-Examples/examples/Simple mutation/GlobalDeclarations.json new file mode 100644 index 0000000..891f4c9 --- /dev/null +++ b/Project-Examples/examples/Simple mutation/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan a, b, c;" +} diff --git a/Project-Examples/examples/Simple mutation/SystemDeclarations.json b/Project-Examples/examples/Simple mutation/SystemDeclarations.json new file mode 100644 index 0000000..a1e0eee --- /dev/null +++ b/Project-Examples/examples/Simple mutation/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Component1;\n\nIO Component1 {a!, b!, c?}" +} diff --git a/Project-Examples/examples/Simple refinement/Components/Component1.json b/Project-Examples/examples/Simple refinement/Components/Component1.json new file mode 100644 index 0000000..f3cb698 --- /dev/null +++ b/Project-Examples/examples/Simple refinement/Components/Component1.json @@ -0,0 +1,71 @@ +{ + "name": "Component1", + "declarations": "clock x;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 180, + "y": 300, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 300, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "OUTPUT", + "select": "", + "guard": "x<=4", + "update": "", + "sync": "o!", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 300, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 300, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "8", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Simple refinement/Components/Component2.json b/Project-Examples/examples/Simple refinement/Components/Component2.json new file mode 100644 index 0000000..9b22b05 --- /dev/null +++ b/Project-Examples/examples/Simple refinement/Components/Component2.json @@ -0,0 +1,71 @@ +{ + "name": "Component2", + "declarations": "clock y;", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 210, + "y": 300, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 380, + "y": 300, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E2", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "y<=2", + "update": "", + "sync": "o!", + "isLocked": false, + "nails": [ + { + "x": 250, + "y": 300, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": 20 + }, + { + "x": 310, + "y": 300, + "propertyType": "SYNCHRONIZATION", + "propertyX": -10, + "propertyY": -30 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "9", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Simple refinement/Queries.json b/Project-Examples/examples/Simple refinement/Queries.json new file mode 100644 index 0000000..7cd98a8 --- /dev/null +++ b/Project-Examples/examples/Simple refinement/Queries.json @@ -0,0 +1,7 @@ +[ + { + "query": "refinement: Component1 <= Component1", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Unspec/Components/A.json b/Project-Examples/examples/Unspec/Components/A.json new file mode 100644 index 0000000..e727b27 --- /dev/null +++ b/Project-Examples/examples/Unspec/Components/A.json @@ -0,0 +1,57 @@ +{ + "name": "A", + "declarations": "", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "6", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L0", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "6", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Unspec/Components/AA.json b/Project-Examples/examples/Unspec/Components/AA.json new file mode 100644 index 0000000..8f26006 --- /dev/null +++ b/Project-Examples/examples/Unspec/Components/AA.json @@ -0,0 +1,57 @@ +{ + "name": "AA", + "declarations": "", + "locations": [ + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "a", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Unspec/Components/B.json b/Project-Examples/examples/Unspec/Components/B.json new file mode 100644 index 0000000..c7d3846 --- /dev/null +++ b/Project-Examples/examples/Unspec/Components/B.json @@ -0,0 +1,57 @@ +{ + "name": "B", + "declarations": "", + "locations": [ + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "9", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E0", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "b", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 290, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 270, + "y": 310, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 257, + "y": 40, + "width": 450, + "height": 600, + "color": "9", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/Unspec/GlobalDeclarations.json b/Project-Examples/examples/Unspec/GlobalDeclarations.json new file mode 100644 index 0000000..6f35cbd --- /dev/null +++ b/Project-Examples/examples/Unspec/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan a, b;" +} diff --git a/Project-Examples/examples/Unspec/Queries.json b/Project-Examples/examples/Unspec/Queries.json new file mode 100644 index 0000000..9ee2141 --- /dev/null +++ b/Project-Examples/examples/Unspec/Queries.json @@ -0,0 +1,7 @@ +[ + { + "query": "refinement: (A || AA) <= B", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/Unspec/SystemDeclarations.json b/Project-Examples/examples/Unspec/SystemDeclarations.json new file mode 100644 index 0000000..f4fcbc4 --- /dev/null +++ b/Project-Examples/examples/Unspec/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system A, B, AA;\n\nIO A { a! }\nIO B { b? }\nIO AA { a? }" +} diff --git a/Project-Examples/examples/input_enablednes/Components/Component1.json b/Project-Examples/examples/input_enablednes/Components/Component1.json new file mode 100644 index 0000000..2eaab5f --- /dev/null +++ b/Project-Examples/examples/input_enablednes/Components/Component1.json @@ -0,0 +1,106 @@ +{ + "name": "Component1", + "declarations": "clock x;\nclock y;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "x <= 10", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 390, + "y": 150, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 30 + }, + { + "id": "L2", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 390, + "y": 420, + "color": "0", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "y >= 3", + "update": "", + "sync": "i2?", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 330, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 320, + "y": 370, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i1?", + "isLocked": false, + "nails": [ + { + "x": 320, + "y": 210, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "0", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/input_enablednes/Components/Component2.json b/Project-Examples/examples/input_enablednes/Components/Component2.json new file mode 100644 index 0000000..2925de1 --- /dev/null +++ b/Project-Examples/examples/input_enablednes/Components/Component2.json @@ -0,0 +1,288 @@ +{ + "name": "Component2", + "declarations": "clock x;\nclock y;", + "locations": [ + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 120, + "y": 290, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L4", + "nickname": "", + "invariant": "x <= 10", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 140, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": -20, + "invariantY": 40 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 360, + "y": 410, + "color": "1", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E3", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i1?", + "isLocked": false, + "nails": [ + { + "x": 380, + "y": 70, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 300, + "y": 100, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i2?", + "isLocked": false, + "nails": [ + { + "x": 430, + "y": 140, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 430, + "y": 190, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "x > 10", + "update": "", + "sync": "i1?", + "isLocked": false, + "nails": [ + { + "x": 100, + "y": 200, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -30 + }, + { + "x": 40, + "y": 230, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 30, + "y": 260, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E6", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L3", + "status": "INPUT", + "select": "", + "guard": "y < 3", + "update": "", + "sync": "i2?", + "isLocked": false, + "nails": [ + { + "x": 140, + "y": 350, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 70, + "y": 360, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 60, + "y": 340, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E7", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "y >= 3", + "update": "", + "sync": "i2?", + "isLocked": false, + "nails": [ + { + "x": 170, + "y": 320, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 240, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 20, + "propertyY": -10 + } + ] + }, + { + "id": "E8", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i1?", + "isLocked": false, + "nails": [ + { + "x": 360, + "y": 350, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 380, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E9", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i2?", + "isLocked": false, + "nails": [ + { + "x": 360, + "y": 470, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 420, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + }, + { + "id": "E10", + "group": "", + "sourceLocation": "L3", + "targetLocation": "L4", + "status": "INPUT", + "select": "", + "guard": "", + "update": "", + "sync": "i1?", + "isLocked": false, + "nails": [ + { + "x": 240, + "y": 220, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 450, + "height": 600, + "color": "1", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/input_enablednes/GlobalDeclarations.json b/Project-Examples/examples/input_enablednes/GlobalDeclarations.json new file mode 100644 index 0000000..0dbf8b9 --- /dev/null +++ b/Project-Examples/examples/input_enablednes/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan i1, i2;" +} diff --git a/Project-Examples/examples/input_enablednes/SystemDeclarations.json b/Project-Examples/examples/input_enablednes/SystemDeclarations.json new file mode 100644 index 0000000..0aa3ccc --- /dev/null +++ b/Project-Examples/examples/input_enablednes/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Component1, Component2;\n\nIO Component1 {i1?, i2?}\nIO Component2 {i1?, i2?}\n" +} diff --git a/Project-Examples/examples/spec test/Components/comp.json b/Project-Examples/examples/spec test/Components/comp.json new file mode 100644 index 0000000..54130ce --- /dev/null +++ b/Project-Examples/examples/spec test/Components/comp.json @@ -0,0 +1,253 @@ +{ + "name": "comp", + "declarations": "clock x;", + "locations": [ + { + "id": "L0", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 230, + "y": 300, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L1", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 410, + "y": 230, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L2", + "nickname": "", + "invariant": "x>10", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 410, + "y": 360, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L3", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 550, + "y": 290, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L8", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 570, + "y": 490, + "color": "5", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E1", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "x>5", + "update": "", + "sync": "input", + "isLocked": false, + "nails": [ + { + "x": 290, + "y": 280, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 320, + "y": 270, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E2", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L2", + "status": "INPUT", + "select": "", + "guard": "x<2", + "update": "", + "sync": "input", + "isLocked": false, + "nails": [ + { + "x": 280, + "y": 320, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 320, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E3", + "group": "", + "sourceLocation": "L1", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "output", + "isLocked": false, + "nails": [ + { + "x": 480, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E4", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L3", + "status": "OUTPUT", + "select": "", + "guard": "x>7", + "update": "", + "sync": "output", + "isLocked": false, + "nails": [ + { + "x": 470, + "y": 340, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 480, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E5", + "group": "", + "sourceLocation": "L0", + "targetLocation": "L1", + "status": "INPUT", + "select": "", + "guard": "x>2 && x<5", + "update": "", + "sync": "input", + "isLocked": false, + "nails": [ + { + "x": 270, + "y": 180, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 290, + "y": 140, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E6", + "group": "", + "sourceLocation": "L2", + "targetLocation": "L8", + "status": "OUTPUT", + "select": "", + "guard": "x <5", + "update": "", + "sync": "output", + "isLocked": false, + "nails": [ + { + "x": 410, + "y": 430, + "propertyType": "GUARD", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 410, + "y": 490, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + }, + { + "x": 590, + "y": 440, + "propertyType": "NONE", + "propertyX": 0, + "propertyY": 0 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 680, + "height": 600, + "color": "5", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/spec test/Components/comp1.json b/Project-Examples/examples/spec test/Components/comp1.json new file mode 100644 index 0000000..02454d7 --- /dev/null +++ b/Project-Examples/examples/spec test/Components/comp1.json @@ -0,0 +1,169 @@ +{ + "name": "comp1", + "declarations": "clock x;", + "locations": [ + { + "id": "L4", + "nickname": "", + "invariant": "", + "type": "INITIAL", + "urgency": "NORMAL", + "x": 40, + "y": 300, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L5", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 320, + "y": 220, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L6", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 290, + "y": 370, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + }, + { + "id": "L7", + "nickname": "", + "invariant": "", + "type": "NORMAL", + "urgency": "NORMAL", + "x": 440, + "y": 290, + "color": "8", + "nicknameX": 30, + "nicknameY": -10, + "invariantX": 30, + "invariantY": 10 + } + ], + "edges": [ + { + "id": "E10", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L5", + "status": "INPUT", + "select": "", + "guard": "x>5", + "update": "", + "sync": "input", + "isLocked": false, + "nails": [ + { + "x": 110, + "y": 280, + "propertyType": "GUARD", + "propertyX": -20, + "propertyY": -110 + }, + { + "x": 180, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E11", + "group": "", + "sourceLocation": "L4", + "targetLocation": "L6", + "status": "INPUT", + "select": "", + "guard": "x<7", + "update": "", + "sync": "input", + "isLocked": false, + "nails": [ + { + "x": 130, + "y": 330, + "propertyType": "GUARD", + "propertyX": -50, + "propertyY": 20 + }, + { + "x": 170, + "y": 340, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E12", + "group": "", + "sourceLocation": "L5", + "targetLocation": "L7", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "output", + "isLocked": false, + "nails": [ + { + "x": 380, + "y": 260, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + }, + { + "id": "E13", + "group": "", + "sourceLocation": "L6", + "targetLocation": "L7", + "status": "OUTPUT", + "select": "", + "guard": "", + "update": "", + "sync": "output", + "isLocked": false, + "nails": [ + { + "x": 370, + "y": 330, + "propertyType": "SYNCHRONIZATION", + "propertyX": 10, + "propertyY": -10 + } + ] + } + ], + "description": "", + "x": 5, + "y": 5, + "width": 550, + "height": 600, + "color": "8", + "includeInPeriodicCheck": true +} diff --git a/Project-Examples/examples/spec test/GlobalDeclarations.json b/Project-Examples/examples/spec test/GlobalDeclarations.json new file mode 100644 index 0000000..d563032 --- /dev/null +++ b/Project-Examples/examples/spec test/GlobalDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "Global Declarations", + "declarations": "broadcast chan input, output;" +} diff --git a/Project-Examples/examples/spec test/Queries.json b/Project-Examples/examples/spec test/Queries.json new file mode 100644 index 0000000..80accb7 --- /dev/null +++ b/Project-Examples/examples/spec test/Queries.json @@ -0,0 +1,12 @@ +[ + { + "query": "specification: comp", + "comment": "", + "isPeriodic": false + }, + { + "query": "specification: comp1", + "comment": "", + "isPeriodic": false + } +] diff --git a/Project-Examples/examples/spec test/SystemDeclarations.json b/Project-Examples/examples/spec test/SystemDeclarations.json new file mode 100644 index 0000000..406245a --- /dev/null +++ b/Project-Examples/examples/spec test/SystemDeclarations.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system comp, comp1;\n\nIO comp{input?, output!}\nIO comp1{input?, output!}" +} diff --git a/Project-Examples/format.mjs b/Project-Examples/format.mjs new file mode 100644 index 0000000..3f1205a --- /dev/null +++ b/Project-Examples/format.mjs @@ -0,0 +1,100 @@ +/** + * @file + * This is a simple formatter that ensures consistent formatting of all json files. + * + * You can run this file with: + * `deno run --allow-read=. --allow-write=. format.mjs` + * or + * `node format.mjs` + * or + * `bun run format.mjs`. + */ + +import { readFile, writeFile, readdir } from "node:fs/promises"; +import { join } from "node:path"; + +let foundFiles = 0; +let unreadDirs = 0; +let unreadFiles = 0; +let invalidFiles = 0; +let unwrittenFiles = 0; +let unformattedFiles = 0; + +await format("."); +async function format(path) { + let dirents; + try { + dirents = await readdir(path, { withFileTypes: true }); + } catch (error) { + console.warn(`Could not read directory: ${path}: ${error.message}`); + unreadDirs++; + return; + } + for (const dirent of dirents) { + if (dirent.isFile() && dirent.name.endsWith(".json")) { + foundFiles++; + let json; + try { + json = await readFile(fullPath(dirent), "utf8"); + } catch (error) { + console.warn(`Could not read file: ${fullPath(dirent)}: ${error.message}`); + unreadFiles++; + continue; + } + let object; + try { + object = JSON.parse(json); + } catch (error) { + console.warn(`Skipping invalid JSON: ${fullPath(dirent)}: ${error.message}`); + invalidFiles++; + continue; + } + const formatted = stringify(object); + if (formatted !== json) { + console.log(`Formatting ${fullPath(dirent)}`); + unformattedFiles++; + try { + await writeFile(fullPath(dirent), formatted); + } catch (error) { + console.warn(`Could not write to file: ${fullPath(dirent)}: ${error.message}`); + unwrittenFiles++; + continue; + } + } + } else if (dirent.isDirectory()) { + await format(fullPath(dirent)); + } + } + function fullPath(dirent) { + return join(path, dirent.name); + } +} + +function stringify(object) { + return `${JSON.stringify(object, undefined, "\t")}\n`; +} + +if (foundFiles === 0) { + console.warn("Did not find any files to format. Are you sure you are running this in the correct directory?"); +} else { + const foundFormatted = `Found ${foundFiles} files, ${unformattedFiles === 0 ? "all of them were already formatted" : `${unformattedFiles} needed formatting`}.`; + const warnings = []; + if (unreadDirs > 0) { + warnings.push(`Could not read ${unreadDirs === 1 ? "one of the directories" : `${unreadDirs} directories`}`); + } + if (unreadFiles > 0) { + warnings.push(`Could not read ${unreadFiles === 1 ? "one of the files" : `${unreadFiles} files`}`); + } + if (invalidFiles > 0) { + warnings.push(`Had to skip ${invalidFiles === 1 ? "an invalid file because it" : `${invalidFiles} files because they`} contained invalid JSON`); + } + if (unwrittenFiles > 0) { + warnings.push(`Could not write to ${unwrittenFiles === 1 ? "one of the files" : `${unwrittenFiles} files`}`); + } + if (warnings.length === 0) { + console.log(` ✔️ ${foundFormatted}`); + } else { + warnings.push(foundFormatted); + console.warn(warnings.join(". ")); + } +} diff --git a/Project-Examples/validate.mjs b/Project-Examples/validate.mjs new file mode 100644 index 0000000..399df02 --- /dev/null +++ b/Project-Examples/validate.mjs @@ -0,0 +1,83 @@ +/** + * @file + * This is a simple validator to check that the examples directory is somewhat standardized. + * This does not do any advanced validation of the structure of the projects. + * + * You can run this file with: + * `deno run --allow-read=. validate.mjs` + * or + * `node validate.mjs` + * or + * `bun run validate.mjs`. + */ + +import { readFile, readdir } from "node:fs/promises"; +import { join } from "node:path"; + +const dirPath = "./examples"; + +let directoryExamples; +try { + directoryExamples = await readdir(dirPath, { withFileTypes: true }); +} catch (error) { + throw new Error(`Could not find the examples directory. It should be located at "${dirPath}". Are you sure you are running this script in the correct directory?`); +} + +log("Validating structure of examples directory"); +for (const example of directoryExamples) { + if (!example.isDirectory()) fail(`Found a non-directory in the examples directory: ${example.name}. Please remove it.`); +} + +log("Validating file formatting in examples directory"); +await validateFileFormatting(dirPath); +async function validateFileFormatting(path) { + let dirents; + try { + dirents = await readdir(path, { withFileTypes: true }); + } catch (error) { + throw new Error(`Could not read directory: ${path}: ${error.message}`); + } + for (const dirent of dirents) { + if (dirent.isFile()) { + if (!dirent.name.endsWith(".json")) fail(`${fullPath(dirent)} should use the .json file extension. All project files must be json encoded.`); + let json; + try { + json = await readFile(fullPath(dirent), "utf8"); + } catch (error) { + throw new Error(`Could not read ${fullPath(dirent)}: ${error.message}`); + } + let object; + try { + object = JSON.parse(json); + } catch (error) { + fail(`${fullPath(dirent)} does not contain valid JSON`, error); + } + if (stringify(object) !== json) { + fail(`${fullPath(dirent)} is not formatted. Please run the formatter and try again.`); + } + } else if (dirent.isDirectory()) { + await validateFileFormatting(fullPath(dirent)); + } + } + function fullPath(dirent) { + return join(path, dirent.name); + } +} + +function stringify(object) { + return `${JSON.stringify(object, undefined, "\t")}\n`; +} + +function log(message) { + console.log(` - ${message}`); +} +function fail(message, error) { + console.error(`\n ❌ ${message}\n`); + if (error) { + throw error; + } else { + throw new TypeError(message); + } +} + +console.log(" ✔️ Yay, everything is valid!");