Skip to content

Commit

Permalink
test: add fischer-6 test
Browse files Browse the repository at this point in the history
  • Loading branch information
@sillydan1
sillydan1 committed Apr 15, 2023
1 parent 6e9d914 commit 5548c8d
Show file tree
Hide file tree
Showing 5 changed files with 388 additions and 11 deletions.
17 changes: 6 additions & 11 deletions test/verification/fischer-suite/fischer-2/Queries.json
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,17 @@
[
{
"query": "E F ctr == 1",
"comment": "Should be reachable",
"is_periodic": false
},
{
"query": "A G ctr < 0 ",
"comment": "No counter-example should be found",
"query": "E F ctr > 1",
"comment": "Can the counter be larger than one? Should be unreachable",
"is_periodic": false
},
{
"query": "E F ctr < 0",
"comment": "Should be unreachable",
"comment": "Can the counter be less than zero? Should be unreachable",
"is_periodic": false
},
{
"query": "E F pid == 2 && ctr == 1",
"comment": "Should be reachable",
"query": "E F ctr == 1",
"comment": "Can the counter reach excactly 1? Should be reachable",
"is_periodic": false
}
]
]
262 changes: 262 additions & 0 deletions test/verification/fischer-suite/fischer-6/Fischer(id).json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,262 @@
{
"name": "Fischer(id)",
"declarations": "public int pid := 0;\npublic int ctr := 0;\npublic int k := 1;\n",
"locations": [
{
"id": "L4",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 20.0,
"y": 90.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
{
"id": "L5",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 330.0,
"y": 90.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
{
"id": "L6",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 330.0,
"y": 260.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
{
"id": "L7",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 20.0,
"y": 260.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
}
],
"initial_location": {
"id": "L2",
"nickname": "",
"invariant": "",
"type": "INITIAL",
"urgency": "NORMAL",
"x": 20.0,
"y": 20.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
"final_location": {
"id": "L3",
"nickname": "",
"invariant": "",
"type": "FINAl",
"urgency": "NORMAL",
"x": 440.0,
"y": 310.0,
"color": "7",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
"jorks": [],
"sub_components": [],
"edges": [
{
"uuid": "0344699d-baf8-4cd5-9a14-9f4368eb1ef1",
"source_location": "L2",
"target_location": "L4",
"select": "",
"guard": "",
"update": "",
"sync": "",
"nails": []
},
{
"uuid": "15b1e1e5-d689-4130-b99f-9514fbd4f6f8",
"source_location": "L4",
"target_location": "L5",
"select": "",
"guard": "pid == 0",
"update": "x := 0_ms",
"sync": "",
"nails": [
{
"x": 90.0,
"y": 90.0,
"property_type": "GUARD",
"property_x": 10.0,
"property_y": -10.0
},
{
"x": 200.0,
"y": 90.0,
"property_type": "UPDATE",
"property_x": 10.0,
"property_y": -10.0
}
]
},
{
"uuid": "60745b5c-d576-4766-a146-dae608c1d671",
"source_location": "L5",
"target_location": "L4",
"select": "",
"guard": "x > k",
"update": "",
"sync": "",
"nails": [
{
"x": 260.0,
"y": 40.0,
"property_type": "NONE",
"property_x": 0.0,
"property_y": 0.0
},
{
"x": 170.0,
"y": 40.0,
"property_type": "GUARD",
"property_x": 10.0,
"property_y": -10.0
},
{
"x": 80.0,
"y": 40.0,
"property_type": "NONE",
"property_x": 0.0,
"property_y": 0.0
}
]
},
{
"uuid": "e55252c5-9e23-4a24-9ee7-c307052f71ed",
"source_location": "L6",
"target_location": "L5",
"select": "",
"guard": "x > k && pid != id",
"update": "x := 0_ms",
"sync": "",
"nails": [
{
"x": 340.0,
"y": 190.0,
"property_type": "GUARD",
"property_x": 10.0,
"property_y": -10.0
},
{
"x": 340.0,
"y": 150.0,
"property_type": "UPDATE",
"property_x": 10.0,
"property_y": -10.0
}
]
},
{
"uuid": "e2897759-4156-467c-8b85-b82ff8d94348",
"source_location": "L5",
"target_location": "L6",
"select": "",
"guard": "x <= k",
"update": "pid := id",
"sync": "",
"nails": [
{
"x": 320.0,
"y": 150.0,
"property_type": "GUARD",
"property_x": -50.0,
"property_y": -10.0
},
{
"x": 320.0,
"y": 190.0,
"property_type": "UPDATE",
"property_x": -70.0,
"property_y": -10.0
}
]
},
{
"uuid": "a06a9e8d-bf75-4fa0-933e-f39fc5c5e47f",
"source_location": "L6",
"target_location": "L7",
"select": "",
"guard": "pid == id &&\nctr == 0",
"update": "ctr := ctr + 1;\nx := 0_ms",
"sync": "",
"nails": [
{
"x": 230.0,
"y": 260.0,
"property_type": "GUARD",
"property_x": -40.0,
"property_y": 10.0
},
{
"x": 120.0,
"y": 260.0,
"property_type": "UPDATE",
"property_x": -40.0,
"property_y": 10.0
}
]
},
{
"uuid": "76cd33fc-c5d8-48a8-a01c-9410fcc91e7e",
"source_location": "L7",
"target_location": "L4",
"select": "",
"guard": "",
"update": "pid := 0;\nctr := ctr - 1",
"sync": "",
"nails": [
{
"x": 20.0,
"y": 140.0,
"property_type": "UPDATE",
"property_x": 10.0,
"property_y": -10.0
}
]
}
],
"main": false,
"description": "",
"x": 5.0,
"y": 5.0,
"width": 460.0,
"height": 330.0,
"color": "7",
"include_in_periodic_check": true
}
93 changes: 93 additions & 0 deletions test/verification/fischer-suite/fischer-6/Main.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
{
"name": "Main",
"declarations": "",
"locations": [],
"initial_location": {
"id": "L0",
"nickname": "",
"invariant": "",
"type": "INITIAL",
"urgency": "NORMAL",
"x": 20.0,
"y": 20.0,
"color": "8",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
"final_location": {
"id": "L1",
"nickname": "",
"invariant": "",
"type": "FINAl",
"urgency": "NORMAL",
"x": 240.0,
"y": 260.0,
"color": "8",
"nickname_x": 30.0,
"nickname_y": -10.0,
"invariant_x": 30.0,
"invariant_y": 10.0
},
"jorks": [],
"sub_components": [
{
"component": "Fischer(id)",
"identifier": "F(1)",
"x": 10.0,
"y": 30.0,
"width": 240.0,
"height": 120.0
},
{
"component": "Fischer(id)",
"identifier": "F(2)",
"x": 10.0,
"y": 60.0,
"width": 240.0,
"height": 120.0
},
{
"component": "Fischer(id)",
"identifier": "F(3)",
"x": 10.0,
"y": 90.0,
"width": 240.0,
"height": 120.0
},
{
"component": "Fischer(id)",
"identifier": "F(4)",
"x": 10.0,
"y": 120.0,
"width": 240.0,
"height": 120.0
},
{
"component": "Fischer(id)",
"identifier": "F(5)",
"x": 10.0,
"y": 150.0,
"width": 240.0,
"height": 120.0
},
{
"component": "Fischer(id)",
"identifier": "F(6)",
"x": 10.0,
"y": 180.0,
"width": 240.0,
"height": 120.0
}
],
"edges": [],
"main": true,
"description": "",
"x": 5.0,
"y": 5.0,
"width": 260.0,
"height": 280.0,
"color": "8",
"include_in_periodic_check": true
}
Loading

0 comments on commit 5548c8d

Please sign in to comment.