1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
package queries
import "http://www.example.com/simpleScenario"
//lanes and lane+widths are in simpleScenarioBoundingBox
// actor coords within simpleScenarioBoundingBox
//@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
//pattern actorOnVerticalLane(a : Actor) {
// Actor.placedOn(a, l);
// Lane.orientation(l, Orientation::Vertical);
// Actor.xPos(a, x);
// Lane.referenceCoord(l, r);
// check(x <= r);
//} or {
// Actor.placedOn(a, l);
// Lane.orientation(l, Orientation::Vertical);
// Actor.xPos(a, x);
// Lane.referenceCoord(l, r);
// Lane.widthNum(l, w);
// check(x >= (r + w));
//}
//
//@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for horizontal lanes")
//pattern actorOnHorizontalLane(a : Actor) {
// Actor.placedOn(a, l);
// Lane.orientation(l, Orientation::Horizontal);
// Actor.yPos(a, y);
// Lane.referenceCoord(l, r);
// check(y <= r);
//} or {
// Actor.placedOn(a, l);
// Lane.orientation(l, Orientation::Horizontal);
// Actor.yPos(a, y);
// Lane.referenceCoord(l, r);
// Lane.widthNum(l, w);
// check(y >= (r + w));
//}
@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation")
pattern actorOnLane(a : Actor) {
find actorOnVerticalLane(a);
// neg find actorOnHorizontalLane(a);
}
private pattern actorOnVerticalLane(a : Actor) {
Actor.placedOn(a, l);
Lane.orientation(l, Orientation::Vertical);
Actor.xPos(a, x);
Lane.referenceCoord(l, r);
Lane.widthNum(l, w);
check(x >= r);
check(x <= (r + w));
}
@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
pattern widthSpec(l : Lane) {
Lane.widthNum(l, w);
check(w != 5);
}
@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
pattern refSpec(l : Lane) {
Lane.referenceCoord(l, w);
check(w != 2);
}
private pattern actorOnHorizontalLane(a : Actor) {
Actor.placedOn(a, l);
Lane.orientation(l, Orientation::Vertical);
Actor.yPos(a, y);
Lane.referenceCoord(l, r);
Lane.widthNum(l, w);
check(y >= r);
check(y <= (r + w));
}
|
