diff options
Diffstat (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries')
-rw-r--r-- | Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | 197 |
1 files changed, 191 insertions, 6 deletions
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql index b8841928..d22bdd8b 100644 --- a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | |||
@@ -40,12 +40,6 @@ pattern output(S1 : Segment, S2 : Segment) { | |||
40 | find turnoutOutput(S1, S2); | 40 | find turnoutOutput(S1, S2); |
41 | } | 41 | } |
42 | 42 | ||
43 | //@Constraint(message = "noInputOfSegment", severity = "error", key = { S }) | ||
44 | //pattern noInputOfSegment(S : Segment) { | ||
45 | // neg find turnout(S); | ||
46 | // neg find output(_, S); | ||
47 | //} | ||
48 | |||
49 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) | 43 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) |
50 | pattern tooManyInputsOfSegment(S : SimpleSegment) { | 44 | pattern tooManyInputsOfSegment(S : SimpleSegment) { |
51 | find output(I1, S); | 45 | find output(I1, S); |
@@ -108,3 +102,194 @@ pattern reachable(S1 : Segment, S2 : Segment) { | |||
108 | pattern unreachable(S1 : Segment, S2 : Segment) { | 102 | pattern unreachable(S1 : Segment, S2 : Segment) { |
109 | neg find reachable(S1, S2); | 103 | neg find reachable(S1, S2); |
110 | } | 104 | } |
105 | |||
106 | // | ||
107 | // closeTrains | ||
108 | // | ||
109 | |||
110 | pattern closeTrains_step_2(in train : Train) { | ||
111 | // frame->t1 = model->trains[i0]; | ||
112 | // frame->start = frame->t1->location; | ||
113 | // if(frame->start != 0){ | ||
114 | // ... | ||
115 | // } | ||
116 | // + OUTER FOR LOOP COUNTER INCREMENT | ||
117 | Train(train); | ||
118 | } | ||
119 | |||
120 | pattern closeTrains_step_3(in train : Train, in start : Segment) { | ||
121 | // int loop_bound1 = frame->start->connected_to_count; | ||
122 | // for (int i1 = 0; i1 < loop_bound1; i1++) { LOOP COUNTER INCREMENT IS NOT INCLUDED HERE | ||
123 | // ... | ||
124 | // } | ||
125 | Train.location(train, start); | ||
126 | } | ||
127 | |||
128 | pattern closeTrains_step_4(in train : Train, in start : Segment, in middle : Segment) { | ||
129 | // frame->middle = frame->start->connected_to[i1]; | ||
130 | // int loop_bound2 = frame->middle->connected_to_count; | ||
131 | |||
132 | // for (int i2 = 0; i2 < loop_bound2; i2++) { LOOP COUNTER INCREMENT IS NOT INCLUDED HERE | ||
133 | // ... | ||
134 | // } | ||
135 | // + OUTER FOR LOOP COUNTER INCREMENT | ||
136 | Train.location(train, start); | ||
137 | Segment.connectedTo(start, middle); | ||
138 | } | ||
139 | |||
140 | pattern closeTrains_step_5(in train : Train, in start : Segment, in middle : Segment, in end : Segment) { | ||
141 | // frame->end = frame->middle->connected_to[i2]; | ||
142 | // if (frame->start != frame->end) { | ||
143 | // ... | ||
144 | // } | ||
145 | // + OUTER FOR LOOP COUNTER INCREMENT | ||
146 | Train.location(train, start); | ||
147 | Segment.connectedTo(start, middle); | ||
148 | Segment.connectedTo(middle, end); | ||
149 | } | ||
150 | |||
151 | pattern closeTrains_step_6(in train : Train, in start : Segment, in middle : Segment, in end : Segment) { | ||
152 | // frame->t2 = frame->end->train; | ||
153 | // if (frame->t2 != 0) { | ||
154 | // ... | ||
155 | // } | ||
156 | Train.location(train, start); | ||
157 | Segment.connectedTo(start, middle); | ||
158 | Segment.connectedTo(middle, end); | ||
159 | start != end; | ||
160 | } | ||
161 | |||
162 | pattern closeTrains_step_7(in train : Train, in start : Segment, in middle : Segment, in end : Segment, in otherTrain : Train) { | ||
163 | // results->matches[match_cntr].start = frame->start; | ||
164 | // results->matches[match_cntr++].end = frame->end; | ||
165 | Train.location(train, start); | ||
166 | Segment.connectedTo(start, middle); | ||
167 | Segment.connectedTo(middle, end); | ||
168 | start != end; | ||
169 | Segment.occupiedBy(end, otherTrain); | ||
170 | } | ||
171 | |||
172 | // | ||
173 | // trainLocations | ||
174 | // | ||
175 | |||
176 | pattern trainLocations_step_2(in train : Train) { | ||
177 | // frame->train = model->trains[i0]; | ||
178 | // frame->location = frame->train->location; | ||
179 | // if (frame->location != NULL) { | ||
180 | // ... | ||
181 | // } | ||
182 | |||
183 | Train(train); | ||
184 | } | ||
185 | |||
186 | pattern trainLocations_step_3(in train : Train, in location : Segment) { | ||
187 | // results->matches[match_cntr].location = frame->location; | ||
188 | // results->matches[match_cntr++].train = frame->train; | ||
189 | Train(train); | ||
190 | Train.location(train, location); | ||
191 | } | ||
192 | |||
193 | // | ||
194 | // misalignedTurnout | ||
195 | // | ||
196 | |||
197 | pattern misalignedTurnout_step_2(in turnout : Turnout) { | ||
198 | // frame->turnout = model->turnouts[i0]; | ||
199 | // frame->location = frame->turnout->straight; | ||
200 | // if (frame->location != NULL) { | ||
201 | // ... | ||
202 | // } | ||
203 | Turnout(turnout); | ||
204 | } | ||
205 | |||
206 | pattern misalignedTurnout_step_3(in turnout : Turnout, in location : Segment) { | ||
207 | // Segment *disconnected = ((Segment *)frame->turnout); | ||
208 | // if (disconnected->connected_to[0] != frame->location && | ||
209 | // disconnected->connected_to[1] != frame->location) { | ||
210 | // ... | ||
211 | // } | ||
212 | Turnout(turnout); | ||
213 | Turnout.straight(turnout, location); | ||
214 | } | ||
215 | |||
216 | pattern misalignedTurnout_step_4(in turnout : Turnout, in location : Segment) { | ||
217 | // frame->train = frame->location->train; | ||
218 | // if (frame->train != NULL) { | ||
219 | // ... | ||
220 | // } | ||
221 | Turnout(turnout); | ||
222 | Turnout.straight(turnout, location); | ||
223 | neg find connectedSegmentsDirected(turnout, location); | ||
224 | } | ||
225 | |||
226 | pattern misalignedTurnout_step_5(in turnout : Turnout, in location : Segment, in train : Train) { | ||
227 | // results->matches[match_cntr].start = frame->start; | ||
228 | // results->matches[match_cntr++].end = frame->end; | ||
229 | Turnout(turnout); | ||
230 | Turnout.straight(turnout, location); | ||
231 | neg find connectedSegmentsDirected(turnout, location); | ||
232 | Segment.occupiedBy(location, train); | ||
233 | } | ||
234 | |||
235 | pattern connectedSegmentsDirected(s1 : Segment, s2 : Segment) { | ||
236 | Segment.connectedTo(s1, s2); | ||
237 | } | ||
238 | |||
239 | // | ||
240 | // endOfSiding | ||
241 | // | ||
242 | |||
243 | pattern endOfSiding_step_2(in train : Train) { | ||
244 | // frame->train = model->trains[i0]; | ||
245 | // frame->location = frame->train->location; | ||
246 | // if (frame->location != NULL) { | ||
247 | // ... | ||
248 | // } | ||
249 | |||
250 | Train(train); | ||
251 | } | ||
252 | |||
253 | pattern endOfSiding_step_3(in train : Train, in location : Segment) { | ||
254 | // int loop_bound1 = frame->location->connected_to_count; | ||
255 | // for (int i1 = 0; i1 < loop_bound1; i1++) { | ||
256 | // ... | ||
257 | // } | ||
258 | Train(train); | ||
259 | Train.location(train, location); | ||
260 | } | ||
261 | |||
262 | pattern endOfSiding_step_4(in train : Train, in location : Segment, in end : Segment) { | ||
263 | // frame->end = frame->location->connected_to[i1]; | ||
264 | // if (frame->end != NULL && | ||
265 | // frame->end->connected_to[1] == frame->location && | ||
266 | // frame->end->connected_to[0] == NULL) { | ||
267 | // ... | ||
268 | // } | ||
269 | // if (frame->end != NULL && | ||
270 | // frame->end->connected_to[0] == frame->location && | ||
271 | // frame->end->connected_to[1] == NULL) { | ||
272 | // ... | ||
273 | // } | ||
274 | Train(train); | ||
275 | Train.location(train, location); | ||
276 | Segment.connectedTo(location, end); | ||
277 | } | ||
278 | |||
279 | pattern endOfSiding_step_5(in train : Train, in location : Segment, in end : Segment) { | ||
280 | // results->matches[match_cntr].location = frame->location; | ||
281 | // results->matches[match_cntr++].train = frame->train; | ||
282 | // ...OR... | ||
283 | // results->matches[match_cntr].location = frame->location; | ||
284 | // results->matches[match_cntr++].train = frame->train; | ||
285 | Train(train); | ||
286 | Train.location(train, location); | ||
287 | Segment.connectedTo(location, end); | ||
288 | neg find multipleConnectedTo(end); | ||
289 | } | ||
290 | |||
291 | pattern multipleConnectedTo(s : Segment) { | ||
292 | Segment.connectedTo(s, n1); | ||
293 | Segment.connectedTo(s, n2); | ||
294 | n1 != n2; | ||
295 | } | ||