diff options
author | 2021-02-16 09:01:25 +0100 | |
---|---|---|
committer | 2021-02-16 09:01:25 +0100 | |
commit | bc403272d867f82edd623179d82c080e57154c1a (patch) | |
tree | 3551ba142ed725595ee684981fc8973cade2ebf4 /Tests/MODELS2020-CaseStudies/case.study.pledge.run | |
parent | add dreal-timeout flag (diff) | |
download | VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.gz VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.zst VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.zip |
CrossingScenario case study is ready for serverdreal-integration
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.pledge.run')
14 files changed, 1887 insertions, 3 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar index 8d981fde..b97ebf5c 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar | |||
Binary files differ | |||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig new file mode 100644 index 00000000..290b8835 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig | |||
@@ -0,0 +1,51 @@ | |||
1 | import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" | ||
2 | import viatra "queries/csQueriesScale.vql" | ||
3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" | ||
4 | import viatra "queries/SatelliteQueries.vql" | ||
5 | |||
6 | generate { | ||
7 | metamodel = { package satellite } | ||
8 | constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } | ||
9 | partial-model = { "inputs/SatelliteInstance.xmi"} | ||
10 | solver = ViatraSolver | ||
11 | scope = { | ||
12 | #node += 10..* | ||
13 | } | ||
14 | |||
15 | config = { | ||
16 | runtime = 10000, | ||
17 | "numeric-solver" = "z3", | ||
18 | log-level = none | ||
19 | } | ||
20 | |||
21 | runs = 1 | ||
22 | |||
23 | output = "measurements/debug/warmup" | ||
24 | } | ||
25 | |||
26 | generate { | ||
27 | metamodel = { package crossingScenario } | ||
28 | constraints = { package queries} | ||
29 | partial-model = { "inputs/crossScen5.xmi"} | ||
30 | solver = ViatraSolver | ||
31 | scope = { | ||
32 | #node += 3..* | ||
33 | ,#<Lane> += 0 | ||
34 | ,#<Relation> += 0 | ||
35 | } | ||
36 | |||
37 | config = { | ||
38 | runtime = 10000, | ||
39 | "numeric-solver" = "z3", | ||
40 | "dreal-local-path" = "enterPathHere", | ||
41 | "dreal-timeout" = "10000", | ||
42 | log-level = none, | ||
43 | "scopePropagator" = "polyhedral"} | ||
44 | |||
45 | runs = 1 | ||
46 | number = 10 | ||
47 | debug = "outputs/debug" | ||
48 | log = "outputs/debug/log.txt" | ||
49 | output = "outputs/models" | ||
50 | statistics = "outputs/debug/statistics.csv" | ||
51 | } | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig new file mode 100644 index 00000000..836b6b76 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig | |||
@@ -0,0 +1,64 @@ | |||
1 | import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" | ||
2 | import viatra "queries/csQueriesStrategy.vql" | ||
3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" | ||
4 | import viatra "queries/SatelliteQueries.vql" | ||
5 | |||
6 | generate { | ||
7 | metamodel = { package satellite } | ||
8 | constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } | ||
9 | partial-model = { "inputs/SatelliteInstance.xmi"} | ||
10 | solver = ViatraSolver | ||
11 | scope = { | ||
12 | #node += 10..* | ||
13 | } | ||
14 | |||
15 | config = { | ||
16 | runtime = 10000, | ||
17 | "numeric-solver" = "z3", | ||
18 | log-level = none | ||
19 | } | ||
20 | |||
21 | runs = 1 | ||
22 | |||
23 | output = "measurements/debug/warmup" | ||
24 | } | ||
25 | |||
26 | generate { | ||
27 | metamodel = { package crossingScenario } | ||
28 | constraints = { package queries} | ||
29 | partial-model = { "inputs/crossScen4Strat.xmi"} | ||
30 | solver = ViatraSolver | ||
31 | scope = { | ||
32 | #node += 0..* | ||
33 | ,#<Lane> += 0 | ||
34 | ,#<Relation> += 0 | ||
35 | } | ||
36 | |||
37 | config = { | ||
38 | runtime = 10000, | ||
39 | "numeric-solver" = "z3", | ||
40 | "dreal-local-path" = "enterPathHere", | ||
41 | "dreal-timeout" = "10000", | ||
42 | log-level = none, | ||
43 | "ignored-attributes" = " | ||
44 | Pedestrian.xPos=*, | ||
45 | Pedestrian.yPos=*, | ||
46 | Pedestrian.length=*, | ||
47 | Pedestrian.width=*, | ||
48 | Pedestrian.xSpeed=*, | ||
49 | Pedestrian.ySpeed=*, | ||
50 | Vehicle.xPos=*, | ||
51 | Vehicle.yPos=*, | ||
52 | Vehicle.length=*, | ||
53 | Vehicle.width=*, | ||
54 | Vehicle.xSpeed=*, | ||
55 | Vehicle.ySpeed=*, | ||
56 | CollisionExists.collisionTime=*"} | ||
57 | |||
58 | runs = 1 | ||
59 | number = 10 | ||
60 | debug = "outputs/debug" | ||
61 | log = "outputs/debug/log.txt" | ||
62 | output = "outputs/models" | ||
63 | statistics = "outputs/debug/statistics.csv" | ||
64 | } | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig new file mode 100644 index 00000000..ebb2c4ca --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig | |||
@@ -0,0 +1,64 @@ | |||
1 | import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" | ||
2 | import viatra "queries/csQueriesStrategyHints.vql" | ||
3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" | ||
4 | import viatra "queries/SatelliteQueries.vql" | ||
5 | |||
6 | generate { | ||
7 | metamodel = { package satellite } | ||
8 | constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } | ||
9 | partial-model = { "inputs/SatelliteInstance.xmi"} | ||
10 | solver = ViatraSolver | ||
11 | scope = { | ||
12 | #node += 10..* | ||
13 | } | ||
14 | |||
15 | config = { | ||
16 | runtime = 10000, | ||
17 | "numeric-solver" = "z3", | ||
18 | log-level = none | ||
19 | } | ||
20 | |||
21 | runs = 1 | ||
22 | |||
23 | output = "measurements/debug/warmup" | ||
24 | } | ||
25 | |||
26 | generate { | ||
27 | metamodel = { package crossingScenario } | ||
28 | constraints = { package queries} | ||
29 | partial-model = { "inputs/crossScen4Strat.xmi"} | ||
30 | solver = ViatraSolver | ||
31 | scope = { | ||
32 | #node += 0..* | ||
33 | ,#<Lane> += 0 | ||
34 | ,#<Relation> += 0 | ||
35 | } | ||
36 | |||
37 | config = { | ||
38 | runtime = 10000, | ||
39 | "numeric-solver" = "z3", | ||
40 | "dreal-local-path" = "enterPathHere", | ||
41 | "dreal-timeout" = "10000", | ||
42 | log-level = none, | ||
43 | "ignored-attributes" = " | ||
44 | Pedestrian.xPos=*, | ||
45 | Pedestrian.yPos=*, | ||
46 | Pedestrian.length=*, | ||
47 | Pedestrian.width=*, | ||
48 | Pedestrian.xSpeed=*, | ||
49 | Pedestrian.ySpeed=*, | ||
50 | Vehicle.xPos=*, | ||
51 | Vehicle.yPos=*, | ||
52 | Vehicle.length=*, | ||
53 | Vehicle.width=*, | ||
54 | Vehicle.xSpeed=*, | ||
55 | Vehicle.ySpeed=*, | ||
56 | CollisionExists.collisionTime=*"} | ||
57 | |||
58 | runs = 1 | ||
59 | number = 10 | ||
60 | debug = "outputs/debug" | ||
61 | log = "outputs/debug/log.txt" | ||
62 | output = "outputs/models" | ||
63 | statistics = "outputs/debug/statistics.csv" | ||
64 | } | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig new file mode 100644 index 00000000..5c2077c2 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig | |||
@@ -0,0 +1,65 @@ | |||
1 | import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" | ||
2 | import viatra "queries/csQueriesStrategy.vql" | ||
3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" | ||
4 | import viatra "queries/SatelliteQueries.vql" | ||
5 | |||
6 | generate { | ||
7 | metamodel = { package satellite } | ||
8 | constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } | ||
9 | partial-model = { "inputs/SatelliteInstance.xmi"} | ||
10 | solver = ViatraSolver | ||
11 | scope = { | ||
12 | #node += 10..* | ||
13 | } | ||
14 | |||
15 | config = { | ||
16 | runtime = 10000, | ||
17 | "numeric-solver" = "z3", | ||
18 | log-level = none | ||
19 | } | ||
20 | |||
21 | runs = 1 | ||
22 | |||
23 | output = "measurements/debug/warmup" | ||
24 | } | ||
25 | |||
26 | generate { | ||
27 | metamodel = { package crossingScenario } | ||
28 | constraints = { package queries} | ||
29 | partial-model = { "inputs/crossScen4Strat.xmi"} | ||
30 | solver = ViatraSolver | ||
31 | scope = { | ||
32 | #node += 0..* | ||
33 | ,#<Lane> += 0 | ||
34 | ,#<Relation> += 0 | ||
35 | } | ||
36 | |||
37 | config = { | ||
38 | runtime = 10000, | ||
39 | "numeric-solver" = "z3", | ||
40 | "dreal-local-path" = "enterPathHere", | ||
41 | "dreal-timeout" = "10000", | ||
42 | log-level = none, | ||
43 | "strategy" = "crossingScenario", | ||
44 | "ignored-attributes" = " | ||
45 | Pedestrian.xPos=*, | ||
46 | Pedestrian.yPos=*, | ||
47 | Pedestrian.length=*, | ||
48 | Pedestrian.width=*, | ||
49 | Pedestrian.xSpeed=*, | ||
50 | Pedestrian.ySpeed=*, | ||
51 | Vehicle.xPos=*, | ||
52 | Vehicle.yPos=*, | ||
53 | Vehicle.length=*, | ||
54 | Vehicle.width=*, | ||
55 | Vehicle.xSpeed=*, | ||
56 | Vehicle.ySpeed=*, | ||
57 | CollisionExists.collisionTime=*"} | ||
58 | |||
59 | runs = 1 | ||
60 | number = 10 | ||
61 | debug = "outputs/debug" | ||
62 | log = "outputs/debug/log.txt" | ||
63 | output = "outputs/models" | ||
64 | statistics = "outputs/debug/statistics.csv" | ||
65 | } | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi new file mode 100644 index 00000000..08cde1e8 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi | |||
@@ -0,0 +1,38 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <crossingScenario:CrossingScenario | ||
3 | xmi:version="2.0" | ||
4 | xmlns:xmi="http://www.omg.org/XMI" | ||
5 | xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
6 | xmlns:crossingScenario="http://www.example.com/crossingScenario" | ||
7 | xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore" | ||
8 | xSize="30.0" | ||
9 | ySize="30.0" | ||
10 | maxTime="60.0" | ||
11 | maxXSpeed="100.0" | ||
12 | maxYSpeed="100.0"> | ||
13 | <actors xsi:type="crossingScenario:Pedestrian"/> | ||
14 | <actors xsi:type="crossingScenario:Vehicle"/> | ||
15 | <lanes xsi:type="crossingScenario:Lane_Horizontal"/> | ||
16 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
17 | referenceCoord="3.0"/> | ||
18 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
19 | referenceCoord="6.0"/> | ||
20 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
21 | referenceCoord="9.0"/> | ||
22 | <lanes xsi:type="crossingScenario:Lane_Vertical"/> | ||
23 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
24 | referenceCoord="3.0"/> | ||
25 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
26 | referenceCoord="6.0"/> | ||
27 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
28 | referenceCoord="9.0"/> | ||
29 | <relations | ||
30 | xsi:type="crossingScenario:CollisionExists" | ||
31 | target="//@actors.0" | ||
32 | source="//@actors.1" | ||
33 | collisionTime="-1.0"/> | ||
34 | <relations | ||
35 | xsi:type="crossingScenario:VisionBlocked" | ||
36 | target="//@actors.0" | ||
37 | source="//@actors.1"/> | ||
38 | </crossingScenario:CrossingScenario> | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi new file mode 100644 index 00000000..5eee1734 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi | |||
@@ -0,0 +1,31 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <crossingScenario:CrossingScenario | ||
3 | xmi:version="2.0" | ||
4 | xmlns:xmi="http://www.omg.org/XMI" | ||
5 | xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
6 | xmlns:crossingScenario="http://www.example.com/crossingScenario" | ||
7 | xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore" | ||
8 | xSize="30.0" | ||
9 | ySize="30.0" | ||
10 | maxTime="60.0" | ||
11 | maxXSpeed="10.0" | ||
12 | maxYSpeed="10.0"> | ||
13 | <lanes xsi:type="crossingScenario:Lane_Horizontal"/> | ||
14 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
15 | referenceCoord="3.0"/> | ||
16 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
17 | referenceCoord="6.0"/> | ||
18 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
19 | referenceCoord="9.0"/> | ||
20 | <lanes xsi:type="crossingScenario:Lane_Horizontal" | ||
21 | referenceCoord="12.0"/> | ||
22 | <lanes xsi:type="crossingScenario:Lane_Vertical"/> | ||
23 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
24 | referenceCoord="3.0"/> | ||
25 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
26 | referenceCoord="6.0"/> | ||
27 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
28 | referenceCoord="9.0"/> | ||
29 | <lanes xsi:type="crossingScenario:Lane_Vertical" | ||
30 | referenceCoord="12.0"/> | ||
31 | </crossingScenario:CrossingScenario> | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql new file mode 100644 index 00000000..d3afa775 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql | |||
@@ -0,0 +1,220 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "http://www.eclipse.org/emf/2002/Ecore" | ||
5 | |||
6 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
7 | //Lane+Actor | ||
8 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
9 | |||
10 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
11 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
12 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
13 | Actor.placedOn(a, vl); | ||
14 | Actor.xPos(a, x); | ||
15 | Lane.referenceCoord(vl, r); | ||
16 | check(x <= r); | ||
17 | } or { | ||
18 | Actor.placedOn(a, vl); | ||
19 | Actor.xPos(a, x); | ||
20 | Lane.referenceCoord(vl, r); | ||
21 | // //<<<<OLD>>>> | ||
22 | // Lane.numWidth(vl, w); | ||
23 | // check(x >= (r + w)); | ||
24 | |||
25 | //<<<<NEW>>>>: lanes all have width=3 | ||
26 | check(x >= (r + 3.0)); | ||
27 | } | ||
28 | |||
29 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
30 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | ||
31 | Actor.placedOn(a, hl); | ||
32 | Actor.yPos(a, y); | ||
33 | Lane.referenceCoord(hl, r); | ||
34 | check(y <= r); | ||
35 | } or { | ||
36 | Actor.placedOn(a, hl); | ||
37 | Actor.yPos(a, y); | ||
38 | Lane.referenceCoord(hl, r); | ||
39 | // //<<OLD>> | ||
40 | // Lane.numWidth(hl, w); | ||
41 | // check(y >= (r + w)); | ||
42 | |||
43 | //<<NEW>>: lanes all have width=3 | ||
44 | check(y >= (r + 3.0)); | ||
45 | |||
46 | } | ||
47 | |||
48 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
49 | //Actor | ||
50 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
51 | |||
52 | /////---------------- | ||
53 | //Xpos and Ypos Bounds | ||
54 | /////---------------- | ||
55 | |||
56 | private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, | ||
57 | xMax:java Double, xP:java Double) { | ||
58 | Actor.placedOn(a, hl); | ||
59 | Lane_Horizontal(hl); | ||
60 | CrossingScenario.actors(cs, a); | ||
61 | CrossingScenario.xSize(cs, xMax); | ||
62 | Actor.xPos(a, xP); | ||
63 | } | ||
64 | |||
65 | private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, | ||
66 | yMax:java Double, yP:java Double) { | ||
67 | Actor.placedOn(a, vl); | ||
68 | Lane_Vertical(vl); | ||
69 | CrossingScenario.actors(cs, a); | ||
70 | CrossingScenario.ySize(cs, yMax); | ||
71 | Actor.yPos(a, yP); | ||
72 | } | ||
73 | |||
74 | @Constraint(severity="error", key={cs}, message="x") | ||
75 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
76 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
77 | check(xP >= xMax);} | ||
78 | |||
79 | @Constraint(severity="error", key={cs}, message="x") | ||
80 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
81 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
82 | check(xP <= 0-xMax);} | ||
83 | |||
84 | @Constraint(severity="error", key={cs}, message="x") | ||
85 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | ||
86 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
87 | check(yP >= yMax);} | ||
88 | |||
89 | @Constraint(severity="error", key={cs}, message="x") | ||
90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | ||
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
92 | check(yP <= 0-yMax);} | ||
93 | |||
94 | //Minimum Distances | ||
95 | private pattern helper_getCoords(a1:Actor, | ||
96 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
97 | Actor.xPos(a1, x1); | ||
98 | Actor.yPos(a1, y1); | ||
99 | Actor.xPos(a2, x2); | ||
100 | Actor.yPos(a2, y2); | ||
101 | } | ||
102 | |||
103 | //INFO may remove? | ||
104 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
105 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | ||
106 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
107 | a1 != a2; | ||
108 | //check(dx^2 + dy^2 < 4^2) | ||
109 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 4*4); | ||
110 | } | ||
111 | |||
112 | /////---------------- | ||
113 | //Xspeed and Yspeed bounds | ||
114 | /////---------------- | ||
115 | /* | ||
116 | /////////VERTICAL LANE | ||
117 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
118 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | ||
119 | Actor.placedOn(a, vl); | ||
120 | Lane_Vertical(vl); | ||
121 | Actor.xSpeed(a, xSpeed); | ||
122 | check(xSpeed != 0.0); | ||
123 | } | ||
124 | |||
125 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
126 | ySpeedMax:java Double, ySpeed:java Double) { | ||
127 | Actor.placedOn(a, vl); | ||
128 | Lane_Vertical(vl); | ||
129 | CrossingScenario.actors(cs, a); | ||
130 | CrossingScenario.maxYSpeed(cs, ySpeedMax); | ||
131 | Actor.ySpeed(a, ySpeed); | ||
132 | } | ||
133 | |||
134 | @Constraint(severity="error", key={cs}, message="x") | ||
135 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | ||
136 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
137 | check(yS <= 0.0-ySMax); | ||
138 | } | ||
139 | |||
140 | @Constraint(severity="error", key={cs}, message="x") | ||
141 | pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { | ||
142 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
143 | check(yS >= ySMax); | ||
144 | } | ||
145 | |||
146 | /////////HORIZONTAL LANE | ||
147 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
148 | pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | ||
149 | Actor.placedOn(a, hl); | ||
150 | Lane_Horizontal(hl); | ||
151 | Actor.ySpeed(a, ySpeed); | ||
152 | check(ySpeed != 0.0); | ||
153 | } | ||
154 | |||
155 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
156 | xSpeedMax:java Double, xSpeed:java Double) { | ||
157 | Actor.placedOn(a, hl); | ||
158 | Lane_Horizontal(hl); | ||
159 | CrossingScenario.actors(cs, a); | ||
160 | CrossingScenario.maxXSpeed(cs, xSpeedMax); | ||
161 | Actor.xSpeed(a, xSpeed); | ||
162 | } | ||
163 | |||
164 | @Constraint(severity="error", key={cs}, message="x") | ||
165 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | ||
166 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
167 | check(xS <= 0.0-xSMax); | ||
168 | } | ||
169 | |||
170 | @Constraint(severity="error", key={cs}, message="x") | ||
171 | pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { | ||
172 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
173 | check(xS >= xSMax); | ||
174 | } | ||
175 | */ | ||
176 | /////---------------- | ||
177 | /////WIDTH and LENGTH | ||
178 | /////---------------- | ||
179 | |||
180 | ///////pedestrian-width (3) | ||
181 | @Constraint(severity="error", key={p}, message="3 Actor") | ||
182 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
183 | Pedestrian.width(p, w); | ||
184 | check(w != 1.0); | ||
185 | } | ||
186 | |||
187 | /////////pedestrian-width (4) | ||
188 | @Constraint(severity="error", key={p}, message="4 Actor") | ||
189 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
190 | Pedestrian.length(p, l); | ||
191 | check(l != 1.0); | ||
192 | } | ||
193 | |||
194 | /////////actor-width (5) | ||
195 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
196 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
197 | Vehicle.placedOn(v, lane); | ||
198 | Lane_Vertical(lane); | ||
199 | Vehicle.width(v, w); | ||
200 | check(w != 2.0); | ||
201 | } or { | ||
202 | Vehicle.placedOn(v, lane); | ||
203 | Lane_Horizontal(lane); | ||
204 | Vehicle.width(v, w); | ||
205 | check(w != 3.0); | ||
206 | } | ||
207 | |||
208 | /////////actor-width (6) | ||
209 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
210 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
211 | Vehicle.placedOn(v, lane); | ||
212 | Lane_Vertical(lane); | ||
213 | Vehicle.length(v, l); | ||
214 | check(l != 3.0); | ||
215 | } or { | ||
216 | Vehicle.placedOn(v, lane); | ||
217 | Lane_Horizontal(lane); | ||
218 | Vehicle.length(v, l); | ||
219 | check(l != 2.0); | ||
220 | } | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql new file mode 100644 index 00000000..5f35cd2b --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql | |||
@@ -0,0 +1,646 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "http://www.eclipse.org/emf/2002/Ecore" | ||
5 | |||
6 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
7 | //Lane+Actor | ||
8 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
9 | |||
10 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
11 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
12 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
13 | Actor.placedOn(a, vl); | ||
14 | Actor.xPos(a, x); | ||
15 | Lane.referenceCoord(vl, r); | ||
16 | check(x <= r); | ||
17 | } or { | ||
18 | Actor.placedOn(a, vl); | ||
19 | Actor.xPos(a, x); | ||
20 | Lane.referenceCoord(vl, r); | ||
21 | // //<<<<OLD>>>> | ||
22 | // Lane.numWidth(vl, w); | ||
23 | // check(x >= (r + w)); | ||
24 | |||
25 | //<<<<NEW>>>>: lanes all have width=3 | ||
26 | check(x >= (r + 3.0)); | ||
27 | } | ||
28 | |||
29 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
30 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | ||
31 | Actor.placedOn(a, hl); | ||
32 | Actor.yPos(a, y); | ||
33 | Lane.referenceCoord(hl, r); | ||
34 | check(y <= r); | ||
35 | } or { | ||
36 | Actor.placedOn(a, hl); | ||
37 | Actor.yPos(a, y); | ||
38 | Lane.referenceCoord(hl, r); | ||
39 | // //<<OLD>> | ||
40 | // Lane.numWidth(hl, w); | ||
41 | // check(y >= (r + w)); | ||
42 | |||
43 | //<<NEW>>: lanes all have width=3 | ||
44 | check(y >= (r + 3.0)); | ||
45 | |||
46 | } | ||
47 | |||
48 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
49 | //Actor | ||
50 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
51 | |||
52 | /////---------------- | ||
53 | //Xpos and Ypos Bounds | ||
54 | /////---------------- | ||
55 | |||
56 | private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, | ||
57 | xMax:java Double, xP:java Double) { | ||
58 | Actor.placedOn(a, hl); | ||
59 | Lane_Horizontal(hl); | ||
60 | CrossingScenario.actors(cs, a); | ||
61 | CrossingScenario.xSize(cs, xMax); | ||
62 | Actor.xPos(a, xP); | ||
63 | } | ||
64 | |||
65 | private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, | ||
66 | yMax:java Double, yP:java Double) { | ||
67 | Actor.placedOn(a, vl); | ||
68 | Lane_Vertical(vl); | ||
69 | CrossingScenario.actors(cs, a); | ||
70 | CrossingScenario.ySize(cs, yMax); | ||
71 | Actor.yPos(a, yP); | ||
72 | } | ||
73 | |||
74 | @Constraint(severity="error", key={cs}, message="x") | ||
75 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
76 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
77 | check(xP >= xMax);} | ||
78 | |||
79 | @Constraint(severity="error", key={cs}, message="x") | ||
80 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
81 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
82 | check(xP <= 0-xMax);} | ||
83 | |||
84 | @Constraint(severity="error", key={cs}, message="x") | ||
85 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | ||
86 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
87 | check(yP >= yMax);} | ||
88 | |||
89 | @Constraint(severity="error", key={cs}, message="x") | ||
90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | ||
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
92 | check(yP <= 0-yMax);} | ||
93 | |||
94 | ////////////ADDED | ||
95 | //to reduce overlap | ||
96 | //NEEDED | ||
97 | /* | ||
98 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
99 | pattern define_actor_wrtLane(a:Actor) { | ||
100 | Actor.placedOn(a, lane); | ||
101 | Lane_Vertical(lane); | ||
102 | Actor.yPos(a, yP); | ||
103 | check(yP > 0.0-1.0); | ||
104 | } or { | ||
105 | Actor.placedOn(a, lane); | ||
106 | Lane_Horizontal(lane); | ||
107 | Actor.xPos(a, xP); | ||
108 | check(xP > 0.0-1.0); | ||
109 | } | ||
110 | */ | ||
111 | ////////////ADDED | ||
112 | |||
113 | //Minimum Distances | ||
114 | private pattern helper_getCoords(a1:Actor, | ||
115 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
116 | Actor.xPos(a1, x1); | ||
117 | Actor.yPos(a1, y1); | ||
118 | Actor.xPos(a2, x2); | ||
119 | Actor.yPos(a2, y2); | ||
120 | } | ||
121 | |||
122 | //INFO may remove? | ||
123 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
124 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | ||
125 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
126 | a1 != a2; | ||
127 | //check(dx^2 + dy^2 < 3^2) | ||
128 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); | ||
129 | } | ||
130 | |||
131 | /////---------------- | ||
132 | //Xspeed and Yspeed bounds | ||
133 | /////---------------- | ||
134 | |||
135 | /////////VERTICAL LANE | ||
136 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
137 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | ||
138 | Actor.placedOn(a, vl); | ||
139 | Lane_Vertical(vl); | ||
140 | Actor.xSpeed(a, xSpeed); | ||
141 | check(xSpeed != 0.0); | ||
142 | } | ||
143 | |||
144 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
145 | ySpeedMax:java Double, ySpeed:java Double) { | ||
146 | Actor.placedOn(a, vl); | ||
147 | Lane_Vertical(vl); | ||
148 | CrossingScenario.actors(cs, a); | ||
149 | CrossingScenario.maxYSpeed(cs, ySpeedMax); | ||
150 | Actor.ySpeed(a, ySpeed); | ||
151 | } | ||
152 | |||
153 | @Constraint(severity="error", key={cs}, message="x") | ||
154 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | ||
155 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
156 | check(yS <= 0.0-ySMax); | ||
157 | } | ||
158 | |||
159 | @Constraint(severity="error", key={cs}, message="x") | ||
160 | pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { | ||
161 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
162 | check(yS >= ySMax); | ||
163 | } | ||
164 | |||
165 | /////////HORIZONTAL LANE | ||
166 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
167 | pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | ||
168 | Actor.placedOn(a, hl); | ||
169 | Lane_Horizontal(hl); | ||
170 | Actor.ySpeed(a, ySpeed); | ||
171 | check(ySpeed != 0.0); | ||
172 | } | ||
173 | |||
174 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
175 | xSpeedMax:java Double, xSpeed:java Double) { | ||
176 | Actor.placedOn(a, hl); | ||
177 | Lane_Horizontal(hl); | ||
178 | CrossingScenario.actors(cs, a); | ||
179 | CrossingScenario.maxXSpeed(cs, xSpeedMax); | ||
180 | Actor.xSpeed(a, xSpeed); | ||
181 | } | ||
182 | |||
183 | @Constraint(severity="error", key={cs}, message="x") | ||
184 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | ||
185 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
186 | check(xS <= 0.0-xSMax); | ||
187 | } | ||
188 | |||
189 | @Constraint(severity="error", key={cs}, message="x") | ||
190 | pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { | ||
191 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
192 | check(xS >= xSMax); | ||
193 | } | ||
194 | |||
195 | /////---------------- | ||
196 | /////WIDTH and LENGTH | ||
197 | /////---------------- | ||
198 | |||
199 | ///////pedestrian-width (3) | ||
200 | @Constraint(severity="error", key={p}, message="3 Actor") | ||
201 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
202 | Pedestrian.width(p, w); | ||
203 | check(w != 1.0); | ||
204 | } | ||
205 | |||
206 | /////////pedestrian-width (4) | ||
207 | @Constraint(severity="error", key={p}, message="4 Actor") | ||
208 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
209 | Pedestrian.length(p, l); | ||
210 | check(l != 1.0); | ||
211 | } | ||
212 | |||
213 | /////////actor-width (5) | ||
214 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
215 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
216 | Vehicle.placedOn(v, lane); | ||
217 | Lane_Vertical(lane); | ||
218 | Vehicle.width(v, w); | ||
219 | check(w != 2.0); | ||
220 | } or { | ||
221 | Vehicle.placedOn(v, lane); | ||
222 | Lane_Horizontal(lane); | ||
223 | Vehicle.width(v, w); | ||
224 | check(w != 3.0); | ||
225 | } | ||
226 | |||
227 | /////////actor-width (6) | ||
228 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
229 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
230 | Vehicle.placedOn(v, lane); | ||
231 | Lane_Vertical(lane); | ||
232 | Vehicle.length(v, l); | ||
233 | check(l != 3.0); | ||
234 | } or { | ||
235 | Vehicle.placedOn(v, lane); | ||
236 | Lane_Horizontal(lane); | ||
237 | Vehicle.length(v, l); | ||
238 | check(l != 2.0); | ||
239 | } | ||
240 | |||
241 | /////---------------- | ||
242 | /////DERIVED FEATURES | ||
243 | /////---------------- | ||
244 | /* | ||
245 | @QueryBasedFeature | ||
246 | pattern dist_near(a1: Actor, a2: Actor) { | ||
247 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
248 | |||
249 | //check(dx^2 + dy^2 < 10^2) | ||
250 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
251 | Actor.dist_near(a1, a2); | ||
252 | } | ||
253 | |||
254 | @QueryBasedFeature | ||
255 | pattern dist_med(a1: Actor, a2: Actor) { | ||
256 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
257 | |||
258 | //check(10^2 < dx^2 + dy^2 < 15^2) | ||
259 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
260 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
261 | Actor.dist_med(a1, a2); | ||
262 | } | ||
263 | |||
264 | @QueryBasedFeature | ||
265 | pattern dist_far(a1: Actor, a2: Actor) { | ||
266 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
267 | |||
268 | //check(dx^2 + dy^2 > 20^2) | ||
269 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
270 | Actor.dist_far(a1, a2); | ||
271 | } | ||
272 | */ | ||
273 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
274 | //Relation | ||
275 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
276 | |||
277 | //@Constraint(severity="error", key={a1, a2}, message="1 Relation") | ||
278 | //pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | ||
279 | // Relation.source(r, a1); | ||
280 | // Relation.target(r, a2); | ||
281 | // a1 == a2; | ||
282 | //} | ||
283 | |||
284 | //TODO do above but transitively?/ | ||
285 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
286 | //CollisionExists | ||
287 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
288 | |||
289 | |||
290 | //<<QUALTATIF ABSTRACTION>> | ||
291 | /* | ||
292 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
293 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | ||
294 | CollisionExists.source(ce, a1); | ||
295 | CollisionExists.target(ce, a2); | ||
296 | Actor.placedOn(a1, vl1); | ||
297 | Lane_Vertical(vl1); | ||
298 | Actor.placedOn(a2, vl2); | ||
299 | Lane_Vertical(vl2); | ||
300 | } or { | ||
301 | CollisionExists.source(ce, a1); | ||
302 | CollisionExists.target(ce, a2); | ||
303 | Actor.placedOn(a1, hl1); | ||
304 | Lane_Horizontal(hl1); | ||
305 | Actor.placedOn(a2, hl2); | ||
306 | Lane_Horizontal(hl2); | ||
307 | } | ||
308 | */ | ||
309 | //<<END TEMP QUALITATIF ABSTRACTION>> | ||
310 | |||
311 | |||
312 | //// | ||
313 | //CollisionExists - Time | ||
314 | //// | ||
315 | |||
316 | |||
317 | @Constraint(severity="error", key={c}, message="x") | ||
318 | pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | ||
319 | CrossingScenario.relations(ss, c); | ||
320 | CrossingScenario.maxTime(ss, maxTime); | ||
321 | CollisionExists.collisionTime(c, cTime); | ||
322 | check(cTime >= maxTime);} | ||
323 | |||
324 | @Constraint(severity="error", key={c}, message="x") | ||
325 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
326 | CollisionExists. collisionTime(c, cTime); | ||
327 | check(cTime <= 0.0);} | ||
328 | |||
329 | //// | ||
330 | //CollisionExists - Physical Positioniung | ||
331 | //// | ||
332 | |||
333 | private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | ||
334 | CollisionExists.source(c, a1); | ||
335 | CollisionExists.target(c, a2); | ||
336 | CollisionExists. collisionTime(c, cTime); | ||
337 | } | ||
338 | |||
339 | private pattern helper_getYCoords(a:Actor, l:java Double, | ||
340 | yPos:java Double, ySpeed:java Double) { | ||
341 | |||
342 | Actor.length(a, l); | ||
343 | Actor.yPos(a, yPos); | ||
344 | Actor.ySpeed(a, ySpeed); | ||
345 | } | ||
346 | |||
347 | private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | ||
348 | l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | ||
349 | ySpeed1:java Double, ySpeed2:java Double) { | ||
350 | |||
351 | CollisionExists.source(c, a1); | ||
352 | CollisionExists.target(c, a2); | ||
353 | find helper_getYCoords(a1, l1, yPos1, ySpeed1); | ||
354 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); | ||
355 | } | ||
356 | |||
357 | private pattern helper_getXCoords(a:Actor, w:java Double, | ||
358 | xPos:java Double, xSpeed:java Double) { | ||
359 | |||
360 | Actor.width(a, w); | ||
361 | Actor.xPos(a, xPos); | ||
362 | Actor.xSpeed(a, xSpeed); | ||
363 | } | ||
364 | |||
365 | private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | ||
366 | w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | ||
367 | xSpeed1:java Double, xSpeed2:java Double) { | ||
368 | |||
369 | CollisionExists.source(c, a1); | ||
370 | CollisionExists.target(c, a2); | ||
371 | find helper_getXCoords(a1, w1, xPos1, xSpeed1); | ||
372 | find helper_getXCoords(a2, w2, xPos2, xSpeed2); | ||
373 | } | ||
374 | |||
375 | @Constraint(severity="error", key={a1}, message="x") | ||
376 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | ||
377 | |||
378 | find helper_getCollExistsTime(a1, a2, cTime); | ||
379 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
380 | |||
381 | //check(y_1_bottom > y_2_top | ||
382 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
383 | } | ||
384 | |||
385 | @Constraint(severity="error", key={a1}, message="x") | ||
386 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | ||
387 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
388 | |||
389 | find helper_getCollExistsTime(a1, a2, cTime); | ||
390 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
391 | |||
392 | //check(y_1_top < y_2_bottom) | ||
393 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
394 | } | ||
395 | |||
396 | @Constraint(severity="error", key={a1}, message="x") | ||
397 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | ||
398 | |||
399 | find helper_getCollExistsTime(a1, a2, cTime); | ||
400 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
401 | |||
402 | //check(x_1_left > x_2_right) | ||
403 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
404 | } | ||
405 | |||
406 | @Constraint(severity="error", key={a1}, message="x") | ||
407 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | ||
408 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
409 | |||
410 | find helper_getCollExistsTime(a1, a2, cTime); | ||
411 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
412 | |||
413 | //check(x_1_right < x_2_left) | ||
414 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
415 | } | ||
416 | |||
417 | |||
418 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
419 | //VisionBlocked | ||
420 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
421 | |||
422 | //<<QUALTATIF ABSTRACTION>> | ||
423 | /* | ||
424 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") | ||
425 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | ||
426 | VisionBlocked.source(vb, a1); | ||
427 | VisionBlocked.target(vb, a2); | ||
428 | Actor.placedOn(a1, l); | ||
429 | Actor.placedOn(a2, l); | ||
430 | } or { | ||
431 | VisionBlocked.source(vb, a1); | ||
432 | VisionBlocked.blockedBy(vb, a2); | ||
433 | Actor.placedOn(a1, l); | ||
434 | Actor.placedOn(a2, l); | ||
435 | } or { | ||
436 | VisionBlocked.blockedBy(vb, a1); | ||
437 | VisionBlocked.target(vb, a2); | ||
438 | Actor.placedOn(a1, l); | ||
439 | Actor.placedOn(a2, l); | ||
440 | } | ||
441 | */ | ||
442 | /* | ||
443 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") | ||
444 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | ||
445 | VisionBlocked.source(ce, a1); | ||
446 | VisionBlocked.target(ce, a2); | ||
447 | Actor.placedOn(a1, vl1); | ||
448 | Lane_Vertical(vl1); | ||
449 | Actor.placedOn(a2, vl2); | ||
450 | Lane_Vertical(vl2); | ||
451 | } or { | ||
452 | VisionBlocked.source(ce, a1); | ||
453 | VisionBlocked.target(ce, a2); | ||
454 | Actor.placedOn(a1, hl1); | ||
455 | Lane_Horizontal(hl1); | ||
456 | Actor.placedOn(a2, hl2); | ||
457 | Lane_Horizontal(hl2); | ||
458 | } | ||
459 | */ | ||
460 | |||
461 | ////////////ADDED | ||
462 | //to make decision for ITE | ||
463 | //NOT NEEDED | ||
464 | /* | ||
465 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
466 | pattern define_vb_blvssrc(a:Actor) { | ||
467 | VisionBlocked.source(vb, a); | ||
468 | VisionBlocked.blockedBy(vb, b); | ||
469 | Actor.placedOn(a, lane); | ||
470 | Lane_Vertical(lane); | ||
471 | Actor.yPos(a, yPa); | ||
472 | Actor.yPos(b, yPb); | ||
473 | check(yPb <= yPa); | ||
474 | } or { | ||
475 | VisionBlocked.source(vb, a); | ||
476 | VisionBlocked.blockedBy(vb, b); | ||
477 | Actor.placedOn(a, lane); | ||
478 | Lane_Horizontal(lane); | ||
479 | Actor.xPos(a, xPa); | ||
480 | Actor.xPos(a, xPb); | ||
481 | check(xPb <= xPa); | ||
482 | } | ||
483 | */ | ||
484 | ////////////ADDED | ||
485 | //<<END QUALITATIF ABSTRACTION>> | ||
486 | |||
487 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
488 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | ||
489 | VisionBlocked.source(vb, a1); | ||
490 | VisionBlocked.target(vb, a2); | ||
491 | VisionBlocked.blockedBy(vb, a2); | ||
492 | } or { | ||
493 | VisionBlocked.source(vb, a1); | ||
494 | VisionBlocked.target(vb, a2); | ||
495 | VisionBlocked.blockedBy(vb, a1); | ||
496 | } | ||
497 | |||
498 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
499 | pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
500 | //REQUIRED to avoid division by 0 in next 2 queries | ||
501 | VisionBlocked.source(vb, a1); | ||
502 | VisionBlocked.target(vb, a2); | ||
503 | |||
504 | Actor.xPos(a1, x1); | ||
505 | Actor.xPos(a2, x2); | ||
506 | |||
507 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
508 | check(x1 == x2); | ||
509 | } | ||
510 | |||
511 | private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, | ||
512 | x1:java Double, y1:java Double, | ||
513 | x2:java Double, y2:java Double, | ||
514 | xBlocker:java Double, yBlocker:java Double, | ||
515 | lenBlocker:java Double, widBlocker:java Double) { | ||
516 | |||
517 | VisionBlocked.source(vb, a1); | ||
518 | VisionBlocked.target(vb, a2); | ||
519 | VisionBlocked.blockedBy(vb, aBlocker); | ||
520 | |||
521 | Actor.xPos(a1, x1); | ||
522 | Actor.yPos(a1, y1); | ||
523 | Actor.xPos(a2, x2); | ||
524 | Actor.yPos(a2, y2); | ||
525 | Actor.xPos(aBlocker, xBlocker); | ||
526 | Actor.yPos(aBlocker, yBlocker); | ||
527 | Actor.length(aBlocker, lenBlocker); | ||
528 | Actor.width(aBlocker, widBlocker); | ||
529 | } | ||
530 | |||
531 | @Constraint(severity="error", key={a1}, message="x") | ||
532 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { | ||
533 | |||
534 | find helper_VB_getAllCoords(a1, a2, | ||
535 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
536 | |||
537 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
538 | check( | ||
539 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | ||
540 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | ||
541 | < ((y1-y2)/(x1-x2))); | ||
542 | } | ||
543 | |||
544 | |||
545 | @Constraint(severity="error", key={a1}, message="x") | ||
546 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { | ||
547 | |||
548 | find helper_VB_getAllCoords(a1, a2, | ||
549 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
550 | |||
551 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
552 | check( | ||
553 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
554 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
555 | > ((y1-y2)/(x1-x2))); | ||
556 | } | ||
557 | |||
558 | /////// | ||
559 | //BLOCKER IN BETWEEN | ||
560 | /////// | ||
561 | |||
562 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, | ||
563 | x1:java Double, y1:java Double, | ||
564 | x2:java Double, y2:java Double, | ||
565 | xBlocker:java Double, yBlocker:java Double) { | ||
566 | |||
567 | VisionBlocked.source(vb, a1); | ||
568 | VisionBlocked.target(vb, a2); | ||
569 | VisionBlocked.blockedBy(vb, aBlocker); | ||
570 | |||
571 | Actor.xPos(a1, x1); | ||
572 | Actor.yPos(a1, y1); | ||
573 | Actor.xPos(a2, x2); | ||
574 | Actor.yPos(a2, y2); | ||
575 | Actor.xPos(aBlocker, xBlocker); | ||
576 | Actor.yPos(aBlocker, yBlocker); | ||
577 | } | ||
578 | |||
579 | /* | ||
580 | //INFO may use approximation instead | ||
581 | @Constraint(severity="error", key={a1}, message="x") | ||
582 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
583 | |||
584 | find helper_VB_getJustCoords(a1, a2, | ||
585 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
586 | |||
587 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
588 | check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); | ||
589 | } | ||
590 | |||
591 | //INFO may use approximation instead | ||
592 | @Constraint(severity="error", key={a1}, message="x") | ||
593 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
594 | |||
595 | find helper_VB_getJustCoords(a1, a2, | ||
596 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
597 | |||
598 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
599 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); | ||
600 | } | ||
601 | */ | ||
602 | |||
603 | //INFO may use approximation instead | ||
604 | @Constraint(severity="error", key={a1}, message="x") | ||
605 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
606 | |||
607 | find helper_VB_getJustCoords(a1, a2, | ||
608 | x1, _, x2, _, xBlocker, _); | ||
609 | |||
610 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
611 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
612 | } | ||
613 | |||
614 | //INFO may use approximation instead | ||
615 | @Constraint(severity="error", key={a1}, message="x") | ||
616 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
617 | |||
618 | find helper_VB_getJustCoords(a1, a2, | ||
619 | x1, _, x2, _, xBlocker, _); | ||
620 | |||
621 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
622 | check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); | ||
623 | } | ||
624 | |||
625 | //INFO may use approximation instead | ||
626 | @Constraint(severity="error", key={a1}, message="x") | ||
627 | pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { | ||
628 | |||
629 | find helper_VB_getJustCoords(a1, a2, | ||
630 | _, y1, _, y2, _, yBlocker); | ||
631 | |||
632 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
633 | check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); | ||
634 | } | ||
635 | |||
636 | //INFO may use approximation instead | ||
637 | @Constraint(severity="error", key={a1}, message="x") | ||
638 | pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { | ||
639 | |||
640 | find helper_VB_getJustCoords(a1, a2, | ||
641 | _, y1, _, y2, _, yBlocker); | ||
642 | |||
643 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
644 | check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); | ||
645 | } | ||
646 | |||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql new file mode 100644 index 00000000..6a9f106c --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql | |||
@@ -0,0 +1,646 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "http://www.eclipse.org/emf/2002/Ecore" | ||
5 | |||
6 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
7 | //Lane+Actor | ||
8 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
9 | |||
10 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
11 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
12 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
13 | Actor.placedOn(a, vl); | ||
14 | Actor.xPos(a, x); | ||
15 | Lane.referenceCoord(vl, r); | ||
16 | check(x <= r); | ||
17 | } or { | ||
18 | Actor.placedOn(a, vl); | ||
19 | Actor.xPos(a, x); | ||
20 | Lane.referenceCoord(vl, r); | ||
21 | // //<<<<OLD>>>> | ||
22 | // Lane.numWidth(vl, w); | ||
23 | // check(x >= (r + w)); | ||
24 | |||
25 | //<<<<NEW>>>>: lanes all have width=3 | ||
26 | check(x >= (r + 3.0)); | ||
27 | } | ||
28 | |||
29 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
30 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | ||
31 | Actor.placedOn(a, hl); | ||
32 | Actor.yPos(a, y); | ||
33 | Lane.referenceCoord(hl, r); | ||
34 | check(y <= r); | ||
35 | } or { | ||
36 | Actor.placedOn(a, hl); | ||
37 | Actor.yPos(a, y); | ||
38 | Lane.referenceCoord(hl, r); | ||
39 | // //<<OLD>> | ||
40 | // Lane.numWidth(hl, w); | ||
41 | // check(y >= (r + w)); | ||
42 | |||
43 | //<<NEW>>: lanes all have width=3 | ||
44 | check(y >= (r + 3.0)); | ||
45 | |||
46 | } | ||
47 | |||
48 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
49 | //Actor | ||
50 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
51 | |||
52 | /////---------------- | ||
53 | //Xpos and Ypos Bounds | ||
54 | /////---------------- | ||
55 | |||
56 | private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, | ||
57 | xMax:java Double, xP:java Double) { | ||
58 | Actor.placedOn(a, hl); | ||
59 | Lane_Horizontal(hl); | ||
60 | CrossingScenario.actors(cs, a); | ||
61 | CrossingScenario.xSize(cs, xMax); | ||
62 | Actor.xPos(a, xP); | ||
63 | } | ||
64 | |||
65 | private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, | ||
66 | yMax:java Double, yP:java Double) { | ||
67 | Actor.placedOn(a, vl); | ||
68 | Lane_Vertical(vl); | ||
69 | CrossingScenario.actors(cs, a); | ||
70 | CrossingScenario.ySize(cs, yMax); | ||
71 | Actor.yPos(a, yP); | ||
72 | } | ||
73 | |||
74 | @Constraint(severity="error", key={cs}, message="x") | ||
75 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
76 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
77 | check(xP >= xMax);} | ||
78 | |||
79 | @Constraint(severity="error", key={cs}, message="x") | ||
80 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
81 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
82 | check(xP <= 0-xMax);} | ||
83 | |||
84 | @Constraint(severity="error", key={cs}, message="x") | ||
85 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | ||
86 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
87 | check(yP >= yMax);} | ||
88 | |||
89 | @Constraint(severity="error", key={cs}, message="x") | ||
90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | ||
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
92 | check(yP <= 0-yMax);} | ||
93 | |||
94 | ////////////ADDED | ||
95 | //to reduce overlap | ||
96 | //NEEDED | ||
97 | |||
98 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
99 | pattern define_actor_wrtLane(a:Actor) { | ||
100 | Actor.placedOn(a, lane); | ||
101 | Lane_Vertical(lane); | ||
102 | Actor.yPos(a, yP); | ||
103 | check(yP > 0.0-1.0); | ||
104 | } or { | ||
105 | Actor.placedOn(a, lane); | ||
106 | Lane_Horizontal(lane); | ||
107 | Actor.xPos(a, xP); | ||
108 | check(xP > 0.0-1.0); | ||
109 | } | ||
110 | |||
111 | ////////////ADDED | ||
112 | |||
113 | //Minimum Distances | ||
114 | private pattern helper_getCoords(a1:Actor, | ||
115 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
116 | Actor.xPos(a1, x1); | ||
117 | Actor.yPos(a1, y1); | ||
118 | Actor.xPos(a2, x2); | ||
119 | Actor.yPos(a2, y2); | ||
120 | } | ||
121 | |||
122 | //INFO may remove? | ||
123 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
124 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | ||
125 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
126 | a1 != a2; | ||
127 | //check(dx^2 + dy^2 < 3^2) | ||
128 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); | ||
129 | } | ||
130 | |||
131 | /////---------------- | ||
132 | //Xspeed and Yspeed bounds | ||
133 | /////---------------- | ||
134 | |||
135 | /////////VERTICAL LANE | ||
136 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
137 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | ||
138 | Actor.placedOn(a, vl); | ||
139 | Lane_Vertical(vl); | ||
140 | Actor.xSpeed(a, xSpeed); | ||
141 | check(xSpeed != 0.0); | ||
142 | } | ||
143 | |||
144 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
145 | ySpeedMax:java Double, ySpeed:java Double) { | ||
146 | Actor.placedOn(a, vl); | ||
147 | Lane_Vertical(vl); | ||
148 | CrossingScenario.actors(cs, a); | ||
149 | CrossingScenario.maxYSpeed(cs, ySpeedMax); | ||
150 | Actor.ySpeed(a, ySpeed); | ||
151 | } | ||
152 | |||
153 | @Constraint(severity="error", key={cs}, message="x") | ||
154 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | ||
155 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
156 | check(yS <= 0.0-ySMax); | ||
157 | } | ||
158 | |||
159 | @Constraint(severity="error", key={cs}, message="x") | ||
160 | pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { | ||
161 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
162 | check(yS >= ySMax); | ||
163 | } | ||
164 | |||
165 | /////////HORIZONTAL LANE | ||
166 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
167 | pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | ||
168 | Actor.placedOn(a, hl); | ||
169 | Lane_Horizontal(hl); | ||
170 | Actor.ySpeed(a, ySpeed); | ||
171 | check(ySpeed != 0.0); | ||
172 | } | ||
173 | |||
174 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
175 | xSpeedMax:java Double, xSpeed:java Double) { | ||
176 | Actor.placedOn(a, hl); | ||
177 | Lane_Horizontal(hl); | ||
178 | CrossingScenario.actors(cs, a); | ||
179 | CrossingScenario.maxXSpeed(cs, xSpeedMax); | ||
180 | Actor.xSpeed(a, xSpeed); | ||
181 | } | ||
182 | |||
183 | @Constraint(severity="error", key={cs}, message="x") | ||
184 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | ||
185 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
186 | check(xS <= 0.0-xSMax); | ||
187 | } | ||
188 | |||
189 | @Constraint(severity="error", key={cs}, message="x") | ||
190 | pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { | ||
191 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
192 | check(xS >= xSMax); | ||
193 | } | ||
194 | |||
195 | /////---------------- | ||
196 | /////WIDTH and LENGTH | ||
197 | /////---------------- | ||
198 | |||
199 | ///////pedestrian-width (3) | ||
200 | @Constraint(severity="error", key={p}, message="3 Actor") | ||
201 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
202 | Pedestrian.width(p, w); | ||
203 | check(w != 1.0); | ||
204 | } | ||
205 | |||
206 | /////////pedestrian-width (4) | ||
207 | @Constraint(severity="error", key={p}, message="4 Actor") | ||
208 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
209 | Pedestrian.length(p, l); | ||
210 | check(l != 1.0); | ||
211 | } | ||
212 | |||
213 | /////////actor-width (5) | ||
214 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
215 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
216 | Vehicle.placedOn(v, lane); | ||
217 | Lane_Vertical(lane); | ||
218 | Vehicle.width(v, w); | ||
219 | check(w != 2.0); | ||
220 | } or { | ||
221 | Vehicle.placedOn(v, lane); | ||
222 | Lane_Horizontal(lane); | ||
223 | Vehicle.width(v, w); | ||
224 | check(w != 3.0); | ||
225 | } | ||
226 | |||
227 | /////////actor-width (6) | ||
228 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
229 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
230 | Vehicle.placedOn(v, lane); | ||
231 | Lane_Vertical(lane); | ||
232 | Vehicle.length(v, l); | ||
233 | check(l != 3.0); | ||
234 | } or { | ||
235 | Vehicle.placedOn(v, lane); | ||
236 | Lane_Horizontal(lane); | ||
237 | Vehicle.length(v, l); | ||
238 | check(l != 2.0); | ||
239 | } | ||
240 | |||
241 | /////---------------- | ||
242 | /////DERIVED FEATURES | ||
243 | /////---------------- | ||
244 | /* | ||
245 | @QueryBasedFeature | ||
246 | pattern dist_near(a1: Actor, a2: Actor) { | ||
247 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
248 | |||
249 | //check(dx^2 + dy^2 < 10^2) | ||
250 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
251 | Actor.dist_near(a1, a2); | ||
252 | } | ||
253 | |||
254 | @QueryBasedFeature | ||
255 | pattern dist_med(a1: Actor, a2: Actor) { | ||
256 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
257 | |||
258 | //check(10^2 < dx^2 + dy^2 < 15^2) | ||
259 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
260 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
261 | Actor.dist_med(a1, a2); | ||
262 | } | ||
263 | |||
264 | @QueryBasedFeature | ||
265 | pattern dist_far(a1: Actor, a2: Actor) { | ||
266 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
267 | |||
268 | //check(dx^2 + dy^2 > 20^2) | ||
269 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
270 | Actor.dist_far(a1, a2); | ||
271 | } | ||
272 | */ | ||
273 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
274 | //Relation | ||
275 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
276 | |||
277 | //@Constraint(severity="error", key={a1, a2}, message="1 Relation") | ||
278 | //pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | ||
279 | // Relation.source(r, a1); | ||
280 | // Relation.target(r, a2); | ||
281 | // a1 == a2; | ||
282 | //} | ||
283 | |||
284 | //TODO do above but transitively?/ | ||
285 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
286 | //CollisionExists | ||
287 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
288 | |||
289 | |||
290 | //<<QUALTATIF ABSTRACTION>> | ||
291 | |||
292 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
293 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | ||
294 | CollisionExists.source(ce, a1); | ||
295 | CollisionExists.target(ce, a2); | ||
296 | Actor.placedOn(a1, vl1); | ||
297 | Lane_Vertical(vl1); | ||
298 | Actor.placedOn(a2, vl2); | ||
299 | Lane_Vertical(vl2); | ||
300 | } or { | ||
301 | CollisionExists.source(ce, a1); | ||
302 | CollisionExists.target(ce, a2); | ||
303 | Actor.placedOn(a1, hl1); | ||
304 | Lane_Horizontal(hl1); | ||
305 | Actor.placedOn(a2, hl2); | ||
306 | Lane_Horizontal(hl2); | ||
307 | } | ||
308 | |||
309 | //<<END TEMP QUALITATIF ABSTRACTION>> | ||
310 | |||
311 | |||
312 | //// | ||
313 | //CollisionExists - Time | ||
314 | //// | ||
315 | |||
316 | |||
317 | @Constraint(severity="error", key={c}, message="x") | ||
318 | pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | ||
319 | CrossingScenario.relations(ss, c); | ||
320 | CrossingScenario.maxTime(ss, maxTime); | ||
321 | CollisionExists.collisionTime(c, cTime); | ||
322 | check(cTime >= maxTime);} | ||
323 | |||
324 | @Constraint(severity="error", key={c}, message="x") | ||
325 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
326 | CollisionExists. collisionTime(c, cTime); | ||
327 | check(cTime <= 0.0);} | ||
328 | |||
329 | //// | ||
330 | //CollisionExists - Physical Positioniung | ||
331 | //// | ||
332 | |||
333 | private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | ||
334 | CollisionExists.source(c, a1); | ||
335 | CollisionExists.target(c, a2); | ||
336 | CollisionExists. collisionTime(c, cTime); | ||
337 | } | ||
338 | |||
339 | private pattern helper_getYCoords(a:Actor, l:java Double, | ||
340 | yPos:java Double, ySpeed:java Double) { | ||
341 | |||
342 | Actor.length(a, l); | ||
343 | Actor.yPos(a, yPos); | ||
344 | Actor.ySpeed(a, ySpeed); | ||
345 | } | ||
346 | |||
347 | private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | ||
348 | l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | ||
349 | ySpeed1:java Double, ySpeed2:java Double) { | ||
350 | |||
351 | CollisionExists.source(c, a1); | ||
352 | CollisionExists.target(c, a2); | ||
353 | find helper_getYCoords(a1, l1, yPos1, ySpeed1); | ||
354 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); | ||
355 | } | ||
356 | |||
357 | private pattern helper_getXCoords(a:Actor, w:java Double, | ||
358 | xPos:java Double, xSpeed:java Double) { | ||
359 | |||
360 | Actor.width(a, w); | ||
361 | Actor.xPos(a, xPos); | ||
362 | Actor.xSpeed(a, xSpeed); | ||
363 | } | ||
364 | |||
365 | private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | ||
366 | w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | ||
367 | xSpeed1:java Double, xSpeed2:java Double) { | ||
368 | |||
369 | CollisionExists.source(c, a1); | ||
370 | CollisionExists.target(c, a2); | ||
371 | find helper_getXCoords(a1, w1, xPos1, xSpeed1); | ||
372 | find helper_getXCoords(a2, w2, xPos2, xSpeed2); | ||
373 | } | ||
374 | |||
375 | @Constraint(severity="error", key={a1}, message="x") | ||
376 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | ||
377 | |||
378 | find helper_getCollExistsTime(a1, a2, cTime); | ||
379 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
380 | |||
381 | //check(y_1_bottom > y_2_top | ||
382 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
383 | } | ||
384 | |||
385 | @Constraint(severity="error", key={a1}, message="x") | ||
386 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | ||
387 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
388 | |||
389 | find helper_getCollExistsTime(a1, a2, cTime); | ||
390 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
391 | |||
392 | //check(y_1_top < y_2_bottom) | ||
393 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
394 | } | ||
395 | |||
396 | @Constraint(severity="error", key={a1}, message="x") | ||
397 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | ||
398 | |||
399 | find helper_getCollExistsTime(a1, a2, cTime); | ||
400 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
401 | |||
402 | //check(x_1_left > x_2_right) | ||
403 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
404 | } | ||
405 | |||
406 | @Constraint(severity="error", key={a1}, message="x") | ||
407 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | ||
408 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
409 | |||
410 | find helper_getCollExistsTime(a1, a2, cTime); | ||
411 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
412 | |||
413 | //check(x_1_right < x_2_left) | ||
414 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
415 | } | ||
416 | |||
417 | |||
418 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
419 | //VisionBlocked | ||
420 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
421 | |||
422 | //<<QUALTATIF ABSTRACTION>> | ||
423 | /* | ||
424 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") | ||
425 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | ||
426 | VisionBlocked.source(vb, a1); | ||
427 | VisionBlocked.target(vb, a2); | ||
428 | Actor.placedOn(a1, l); | ||
429 | Actor.placedOn(a2, l); | ||
430 | } or { | ||
431 | VisionBlocked.source(vb, a1); | ||
432 | VisionBlocked.blockedBy(vb, a2); | ||
433 | Actor.placedOn(a1, l); | ||
434 | Actor.placedOn(a2, l); | ||
435 | } or { | ||
436 | VisionBlocked.blockedBy(vb, a1); | ||
437 | VisionBlocked.target(vb, a2); | ||
438 | Actor.placedOn(a1, l); | ||
439 | Actor.placedOn(a2, l); | ||
440 | } | ||
441 | */ | ||
442 | |||
443 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") | ||
444 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | ||
445 | VisionBlocked.source(ce, a1); | ||
446 | VisionBlocked.target(ce, a2); | ||
447 | Actor.placedOn(a1, vl1); | ||
448 | Lane_Vertical(vl1); | ||
449 | Actor.placedOn(a2, vl2); | ||
450 | Lane_Vertical(vl2); | ||
451 | } or { | ||
452 | VisionBlocked.source(ce, a1); | ||
453 | VisionBlocked.target(ce, a2); | ||
454 | Actor.placedOn(a1, hl1); | ||
455 | Lane_Horizontal(hl1); | ||
456 | Actor.placedOn(a2, hl2); | ||
457 | Lane_Horizontal(hl2); | ||
458 | } | ||
459 | |||
460 | |||
461 | ////////////ADDED | ||
462 | //to make decision for ITE | ||
463 | //NOT NEEDED | ||
464 | /* | ||
465 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
466 | pattern define_vb_blvssrc(a:Actor) { | ||
467 | VisionBlocked.source(vb, a); | ||
468 | VisionBlocked.blockedBy(vb, b); | ||
469 | Actor.placedOn(a, lane); | ||
470 | Lane_Vertical(lane); | ||
471 | Actor.yPos(a, yPa); | ||
472 | Actor.yPos(b, yPb); | ||
473 | check(yPb <= yPa); | ||
474 | } or { | ||
475 | VisionBlocked.source(vb, a); | ||
476 | VisionBlocked.blockedBy(vb, b); | ||
477 | Actor.placedOn(a, lane); | ||
478 | Lane_Horizontal(lane); | ||
479 | Actor.xPos(a, xPa); | ||
480 | Actor.xPos(a, xPb); | ||
481 | check(xPb <= xPa); | ||
482 | } | ||
483 | */ | ||
484 | ////////////ADDED | ||
485 | //<<END QUALITATIF ABSTRACTION>> | ||
486 | |||
487 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
488 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | ||
489 | VisionBlocked.source(vb, a1); | ||
490 | VisionBlocked.target(vb, a2); | ||
491 | VisionBlocked.blockedBy(vb, a2); | ||
492 | } or { | ||
493 | VisionBlocked.source(vb, a1); | ||
494 | VisionBlocked.target(vb, a2); | ||
495 | VisionBlocked.blockedBy(vb, a1); | ||
496 | } | ||
497 | |||
498 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
499 | pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
500 | //REQUIRED to avoid division by 0 in next 2 queries | ||
501 | VisionBlocked.source(vb, a1); | ||
502 | VisionBlocked.target(vb, a2); | ||
503 | |||
504 | Actor.xPos(a1, x1); | ||
505 | Actor.xPos(a2, x2); | ||
506 | |||
507 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
508 | check(x1 == x2); | ||
509 | } | ||
510 | |||
511 | private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, | ||
512 | x1:java Double, y1:java Double, | ||
513 | x2:java Double, y2:java Double, | ||
514 | xBlocker:java Double, yBlocker:java Double, | ||
515 | lenBlocker:java Double, widBlocker:java Double) { | ||
516 | |||
517 | VisionBlocked.source(vb, a1); | ||
518 | VisionBlocked.target(vb, a2); | ||
519 | VisionBlocked.blockedBy(vb, aBlocker); | ||
520 | |||
521 | Actor.xPos(a1, x1); | ||
522 | Actor.yPos(a1, y1); | ||
523 | Actor.xPos(a2, x2); | ||
524 | Actor.yPos(a2, y2); | ||
525 | Actor.xPos(aBlocker, xBlocker); | ||
526 | Actor.yPos(aBlocker, yBlocker); | ||
527 | Actor.length(aBlocker, lenBlocker); | ||
528 | Actor.width(aBlocker, widBlocker); | ||
529 | } | ||
530 | |||
531 | @Constraint(severity="error", key={a1}, message="x") | ||
532 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { | ||
533 | |||
534 | find helper_VB_getAllCoords(a1, a2, | ||
535 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
536 | |||
537 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
538 | check( | ||
539 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | ||
540 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | ||
541 | < ((y1-y2)/(x1-x2))); | ||
542 | } | ||
543 | |||
544 | |||
545 | @Constraint(severity="error", key={a1}, message="x") | ||
546 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { | ||
547 | |||
548 | find helper_VB_getAllCoords(a1, a2, | ||
549 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
550 | |||
551 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
552 | check( | ||
553 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
554 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
555 | > ((y1-y2)/(x1-x2))); | ||
556 | } | ||
557 | |||
558 | /////// | ||
559 | //BLOCKER IN BETWEEN | ||
560 | /////// | ||
561 | |||
562 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, | ||
563 | x1:java Double, y1:java Double, | ||
564 | x2:java Double, y2:java Double, | ||
565 | xBlocker:java Double, yBlocker:java Double) { | ||
566 | |||
567 | VisionBlocked.source(vb, a1); | ||
568 | VisionBlocked.target(vb, a2); | ||
569 | VisionBlocked.blockedBy(vb, aBlocker); | ||
570 | |||
571 | Actor.xPos(a1, x1); | ||
572 | Actor.yPos(a1, y1); | ||
573 | Actor.xPos(a2, x2); | ||
574 | Actor.yPos(a2, y2); | ||
575 | Actor.xPos(aBlocker, xBlocker); | ||
576 | Actor.yPos(aBlocker, yBlocker); | ||
577 | } | ||
578 | |||
579 | /* | ||
580 | //INFO may use approximation instead | ||
581 | @Constraint(severity="error", key={a1}, message="x") | ||
582 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
583 | |||
584 | find helper_VB_getJustCoords(a1, a2, | ||
585 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
586 | |||
587 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
588 | check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); | ||
589 | } | ||
590 | |||
591 | //INFO may use approximation instead | ||
592 | @Constraint(severity="error", key={a1}, message="x") | ||
593 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
594 | |||
595 | find helper_VB_getJustCoords(a1, a2, | ||
596 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
597 | |||
598 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
599 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); | ||
600 | } | ||
601 | */ | ||
602 | |||
603 | //INFO may use approximation instead | ||
604 | @Constraint(severity="error", key={a1}, message="x") | ||
605 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
606 | |||
607 | find helper_VB_getJustCoords(a1, a2, | ||
608 | x1, _, x2, _, xBlocker, _); | ||
609 | |||
610 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
611 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
612 | } | ||
613 | |||
614 | //INFO may use approximation instead | ||
615 | @Constraint(severity="error", key={a1}, message="x") | ||
616 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
617 | |||
618 | find helper_VB_getJustCoords(a1, a2, | ||
619 | x1, _, x2, _, xBlocker, _); | ||
620 | |||
621 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
622 | check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); | ||
623 | } | ||
624 | |||
625 | //INFO may use approximation instead | ||
626 | @Constraint(severity="error", key={a1}, message="x") | ||
627 | pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { | ||
628 | |||
629 | find helper_VB_getJustCoords(a1, a2, | ||
630 | _, y1, _, y2, _, yBlocker); | ||
631 | |||
632 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
633 | check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); | ||
634 | } | ||
635 | |||
636 | //INFO may use approximation instead | ||
637 | @Constraint(severity="error", key={a1}, message="x") | ||
638 | pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { | ||
639 | |||
640 | find helper_VB_getJustCoords(a1, a2, | ||
641 | _, y1, _, y2, _, yBlocker); | ||
642 | |||
643 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
644 | check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); | ||
645 | } | ||
646 | |||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh new file mode 100755 index 00000000..8a6a30be --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh | |||
@@ -0,0 +1,21 @@ | |||
1 | #!/usr/bin/bash | ||
2 | NODE="$1" | ||
3 | ./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 | ||
4 | ./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
5 | ./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 | ||
6 | ./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
7 | ./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 | ||
8 | ./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
9 | ./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
10 | ./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
11 | ./run.sh "${NODE}" -d CrossScenario -lb 12 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
12 | ./run.sh "${NODE}" -d CrossScenario -lb 15 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
13 | ./run.sh "${NODE}" -d CrossScenario -lb 16 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
14 | ./run.sh "${NODE}" -d CrossScenario -lb 18 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
15 | |||
16 | ./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
17 | ./run.sh "${NODE}" -d CrossScenario -lb 20 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
18 | |||
19 | ./run.sh "${NODE}" -d CrossScenario -lb 21 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
20 | ./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
21 | |||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh new file mode 100755 index 00000000..5ceda582 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh | |||
@@ -0,0 +1,15 @@ | |||
1 | #!/usr/bin/bash | ||
2 | NODE="$1" | ||
3 | ./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
4 | |||
5 | ./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
6 | ./run.sh "${NODE}" -d StrategyNo -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
7 | |||
8 | ./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
9 | ./run.sh "${NODE}" -d StrategyNo -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
10 | |||
11 | ./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
12 | ./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 | ||
13 | |||
14 | ./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
15 | ./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh new file mode 100755 index 00000000..64a72200 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh | |||
@@ -0,0 +1,11 @@ | |||
1 | #!/usr/bin/bash | ||
2 | NODE="$1" | ||
3 | |||
4 | ./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns z3 -drto 300000 | ||
5 | ./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
6 | |||
7 | ./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns z3 -drto 2000 | ||
8 | ./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 2000 | ||
9 | |||
10 | ./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 | ||
11 | ./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 \ No newline at end of file | ||
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend index eddb8bb5..78d86504 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend | |||
@@ -39,6 +39,7 @@ class RunGeneratorConfig { | |||
39 | static var RUNTIME = 1500 | 39 | static var RUNTIME = 1500 |
40 | static var NUM_SOLVER = "z3" | 40 | static var NUM_SOLVER = "z3" |
41 | static var DREAL_PATH = "" | 41 | static var DREAL_PATH = "" |
42 | static var DREAL_TIMEOUT = "-2" | ||
42 | // static var SCOPE_PROPAGATOR = "typeHierarchy" | 43 | // static var SCOPE_PROPAGATOR = "typeHierarchy" |
43 | 44 | ||
44 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" | 45 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" |
@@ -75,6 +76,9 @@ class RunGeneratorConfig { | |||
75 | val drp = new Option("drp", "drealPath", true, "path to dreal executeable") | 76 | val drp = new Option("drp", "drealPath", true, "path to dreal executeable") |
76 | options.addOption(drp) | 77 | options.addOption(drp) |
77 | 78 | ||
79 | val drto = new Option("drto", "drealTimeout", true, "drealTimeout") | ||
80 | options.addOption(drto) | ||
81 | |||
78 | // val sp = new Option("sp", "scopePropagator", true, "scope Propagator") | 82 | // val sp = new Option("sp", "scopePropagator", true, "scope Propagator") |
79 | // options.addOption(sp) | 83 | // options.addOption(sp) |
80 | // | 84 | // |
@@ -82,7 +86,7 @@ class RunGeneratorConfig { | |||
82 | options.addOption(d) | 86 | options.addOption(d) |
83 | 87 | ||
84 | val hh = new Option("hh", "household", true, "number of households") | 88 | val hh = new Option("hh", "household", true, "number of households") |
85 | options.addOption(hh) | 89 | options.addOption(hh) |
86 | 90 | ||
87 | val CommandLineParser parser = new BasicParser | 91 | val CommandLineParser parser = new BasicParser |
88 | val formatter = new HelpFormatter() | 92 | val formatter = new HelpFormatter() |
@@ -110,6 +114,8 @@ class RunGeneratorConfig { | |||
110 | if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local" | 114 | if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local" |
111 | val drpIn = cmd.getOptionValue("drealPath") | 115 | val drpIn = cmd.getOptionValue("drealPath") |
112 | if(drpIn !== null) DREAL_PATH = drpIn | 116 | if(drpIn !== null) DREAL_PATH = drpIn |
117 | val drtoIn = cmd.getOptionValue("drealTimeout") | ||
118 | if(drtoIn !== null) DREAL_TIMEOUT = drtoIn | ||
113 | // val spIn = cmd.getOptionValue("scopePropagator") | 119 | // val spIn = cmd.getOptionValue("scopePropagator") |
114 | // if(spIn !== null ) SCOPE_PROPAGATOR = spIn | 120 | // if(spIn !== null ) SCOPE_PROPAGATOR = spIn |
115 | val dIn = cmd.getOptionValue("domain") | 121 | val dIn = cmd.getOptionValue("domain") |
@@ -136,14 +142,16 @@ class RunGeneratorConfig { | |||
136 | ", SIZE=" + SIZE_LB + "to" + SIZE_UB + | 142 | ", SIZE=" + SIZE_LB + "to" + SIZE_UB + |
137 | ", Runs=" + RUNS + | 143 | ", Runs=" + RUNS + |
138 | ", ModelsPerRun=" + MODELS + | 144 | ", ModelsPerRun=" + MODELS + |
139 | ", Runtime=" + RUNTIME + ">>") | 145 | ", Runtime=" + RUNTIME + |
146 | ", dreal-timeout=" + DREAL_TIMEOUT + ">>") | ||
140 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") | 147 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") |
141 | 148 | ||
142 | var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + | 149 | var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + |
143 | "r" + RUNS + | 150 | "r" + RUNS + |
144 | "n" + MODELS + | 151 | "n" + MODELS + |
145 | "rt" + RUNTIME + | 152 | "rt" + RUNTIME + |
146 | "ns" + NUM_SOLVER | 153 | "ns" + NUM_SOLVER + |
154 | "drto" + DREAL_TIMEOUT | ||
147 | if (isTaxation) naming = naming + "hh" + HOUSEHOLD | 155 | if (isTaxation) naming = naming + "hh" + HOUSEHOLD |
148 | val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate | 156 | val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate |
149 | val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate | 157 | val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate |
@@ -211,6 +219,10 @@ class RunGeneratorConfig { | |||
211 | numSolverEntry.value = NUM_SOLVER | 219 | numSolverEntry.value = NUM_SOLVER |
212 | val drealPathEntry = configScope.entries.get(2) as CustomEntry | 220 | val drealPathEntry = configScope.entries.get(2) as CustomEntry |
213 | drealPathEntry.value = DREAL_PATH | 221 | drealPathEntry.value = DREAL_PATH |
222 | if (DREAL_TIMEOUT != "-2") { | ||
223 | val drealTimeoutEntry = configScope.entries.get(3) as CustomEntry | ||
224 | drealTimeoutEntry.value = DREAL_TIMEOUT | ||
225 | } | ||
214 | // val scopePropEntry = configScope.entries.get(3) as CustomEntry | 226 | // val scopePropEntry = configScope.entries.get(3) as CustomEntry |
215 | // scopePropEntry.value = SCOPE_PROPAGATOR | 227 | // scopePropEntry.value = SCOPE_PROPAGATOR |
216 | 228 | ||