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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
package modes3.queries
import "http://www.ece.mcgill.ca/wcet/modes3"
pattern connectedTo(S1 : Segment, S2 : Segment) {
Segment.connectedTo(S1, S2);
}
@Constraint(message = "connectedToNotSymmetric", severity = "error", key = { S1, S2 })
pattern connectedToNotSymmetric(S1 : Segment, S2 : Segment) {
Segment.connectedTo(S1, S2);
neg find connectedTo(S2, S1);
}
@Constraint(message = "connectedToReflexive", severity = "error", key = { S })
pattern connectedToReflexive(S : Segment) {
Segment.connectedTo(S, S);
}
pattern turnoutOutput(T : Turnout, S : Segment) {
Turnout.straight(T, S);
} or {
Turnout.divergent(T, S);
}
@Constraint(message = "outputReflexive", severity = "error", key = { T })
pattern outputReflexive(T : Turnout) {
find turnoutOutput(T, T);
}
@Constraint(message = "turnoutOutputsAreSame", severity = "error", key = { T })
pattern turnoutOutputsAreSame(T : Turnout) {
Turnout.straight(T, S);
Turnout.divergent(T, S);
}
pattern output(S1 : Segment, S2 : Segment) {
Segment.connectedTo(S1, S2);
} or {
find turnoutOutput(S1, S2);
}
//@Constraint(message = "noInputOfSegment", severity = "error", key = { S })
//pattern noInputOfSegment(S : Segment) {
// neg find turnout(S);
// neg find output(_, S);
//}
@Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S })
pattern tooManyInputsOfSegment(S : SimpleSegment) {
find output(I1, S);
find output(I2, S);
find output(I3, S);
I1 != I2;
I1 != I3;
I2 != I3;
}
@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
pattern turnoutConnectedToBothOutputs(T : Turnout) {
Turnout.straight(T, Straight);
Turnout.divergent(T, Divergent);
Segment.connectedTo(T, Straight);
Segment.connectedTo(T, Divergent);
}
pattern adjacent(S1 : Segment, S2 : Segment) {
find output(S1, S2);
} or {
find turnoutOutput(S2, S1);
}
@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
pattern tooManyInputsOfTurnout(T : Turnout) {
find adjacent(I1, T);
find adjacent(I2, T);
find adjacent(I3, T);
find adjacent(I4, T);
I1 != I2;
I1 != I3;
I1 != I4;
I2 != I3;
I2 != I4;
I3 != I4;
}
pattern inputsOfTurnout(T : Turnout) {
find adjacent(I1, T);
find adjacent(I2, T);
find adjacent(I3, T);
I1 != I2;
I1 != I3;
I2 != I3;
}
@Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T })
pattern tooFewInputsOfTurnout(T : Turnout) {
neg find inputsOfTurnout(T);
}
pattern reachable(S1 : Segment, S2 : Segment) {
S1 == S2;
} or {
find adjacent+(S1, S2);
}
@Constraint(message = "unreachable", severity = "error", key = { S1, S2 })
pattern unreachable(S1 : Segment, S2 : Segment) {
neg find reachable(S1, S2);
}
|
