aboutsummaryrefslogtreecommitdiffstats
path: root/Domains/ca.mcgill.rtgmrt.example.modes3/src
diff options
context:
space:
mode:
Diffstat (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src')
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql295
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/CloseTrainsObjectiveHint.xtend201
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/EndOfSidingObjectiveHint.xtend139
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/MisalignedTurnoutObjectiveHint.xtend140
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend357
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3TypeScopeHint.xtend79
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend417
-rw-r--r--Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/TrainLocationsObjectiveHint.xtend85
8 files changed, 1713 insertions, 0 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
new file mode 100644
index 00000000..d22bdd8b
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql
@@ -0,0 +1,295 @@
1package modes3.queries
2
3import "http://www.ece.mcgill.ca/wcet/modes3"
4
5pattern connectedTo(S1 : Segment, S2 : Segment) {
6 Segment.connectedTo(S1, S2);
7}
8
9@Constraint(message = "connectedToNotSymmetric", severity = "error", key = { S1, S2 })
10pattern connectedToNotSymmetric(S1 : Segment, S2 : Segment) {
11 Segment.connectedTo(S1, S2);
12 neg find connectedTo(S2, S1);
13}
14
15@Constraint(message = "connectedToReflexive", severity = "error", key = { S })
16pattern connectedToReflexive(S : Segment) {
17 Segment.connectedTo(S, S);
18}
19
20pattern turnoutOutput(T : Turnout, S : Segment) {
21 Turnout.straight(T, S);
22} or {
23 Turnout.divergent(T, S);
24}
25
26@Constraint(message = "outputReflexive", severity = "error", key = { T })
27pattern outputReflexive(T : Turnout) {
28 find turnoutOutput(T, T);
29}
30
31@Constraint(message = "turnoutOutputsAreSame", severity = "error", key = { T })
32pattern turnoutOutputsAreSame(T : Turnout) {
33 Turnout.straight(T, S);
34 Turnout.divergent(T, S);
35}
36
37pattern output(S1 : Segment, S2 : Segment) {
38 Segment.connectedTo(S1, S2);
39} or {
40 find turnoutOutput(S1, S2);
41}
42
43@Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S })
44pattern tooManyInputsOfSegment(S : SimpleSegment) {
45 find output(I1, S);
46 find output(I2, S);
47 find output(I3, S);
48 I1 != I2;
49 I1 != I3;
50 I2 != I3;
51}
52
53@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
54pattern turnoutConnectedToBothOutputs(T : Turnout) {
55 Turnout.straight(T, Straight);
56 Turnout.divergent(T, Divergent);
57 Segment.connectedTo(T, Straight);
58 Segment.connectedTo(T, Divergent);
59}
60
61pattern adjacent(S1 : Segment, S2 : Segment) {
62 find output(S1, S2);
63} or {
64 find turnoutOutput(S2, S1);
65}
66
67@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
68pattern tooManyInputsOfTurnout(T : Turnout) {
69 find adjacent(I1, T);
70 find adjacent(I2, T);
71 find adjacent(I3, T);
72 find adjacent(I4, T);
73 I1 != I2;
74 I1 != I3;
75 I1 != I4;
76 I2 != I3;
77 I2 != I4;
78 I3 != I4;
79}
80
81pattern inputsOfTurnout(T : Turnout) {
82 find adjacent(I1, T);
83 find adjacent(I2, T);
84 find adjacent(I3, T);
85 I1 != I2;
86 I1 != I3;
87 I2 != I3;
88}
89
90@Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T })
91pattern tooFewInputsOfTurnout(T : Turnout) {
92 neg find inputsOfTurnout(T);
93}
94
95pattern reachable(S1 : Segment, S2 : Segment) {
96 S1 == S2;
97} or {
98 find adjacent+(S1, S2);
99}
100
101@Constraint(message = "unreachable", severity = "error", key = { S1, S2 })
102pattern unreachable(S1 : Segment, S2 : Segment) {
103 neg find reachable(S1, S2);
104}
105
106//
107// closeTrains
108//
109
110pattern 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
120pattern 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
128pattern 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
140pattern 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
151pattern 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
162pattern 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
176pattern 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
186pattern 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
197pattern 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
206pattern 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
216pattern 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
226pattern 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
235pattern connectedSegmentsDirected(s1 : Segment, s2 : Segment) {
236 Segment.connectedTo(s1, s2);
237}
238
239//
240// endOfSiding
241//
242
243pattern 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
253pattern 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
262pattern 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
279pattern 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
291pattern multipleConnectedTo(s : Segment) {
292 Segment.connectedTo(s, n1);
293 Segment.connectedTo(s, n2);
294 n1 != n2;
295}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/CloseTrainsObjectiveHint.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/CloseTrainsObjectiveHint.xtend
new file mode 100644
index 00000000..519a228a
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/CloseTrainsObjectiveHint.xtend
@@ -0,0 +1,201 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatch
8import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatchers
9import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint
10import java.util.Collection
11import java.util.Map
12import modes3.Modes3Package
13import modes3.queries.CloseTrains_step_2
14import modes3.queries.CloseTrains_step_3
15import modes3.queries.CloseTrains_step_4
16import modes3.queries.CloseTrains_step_5
17import modes3.queries.CloseTrains_step_6
18import modes3.queries.CloseTrains_step_7
19
20class CloseTrainsObjectiveHint extends CostObjectiveHint {
21 val Type segmentType
22 val Type trainType
23
24 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
25 extension val Modes3Package = Modes3Package.eINSTANCE
26 segmentType = ecore2LogicTrace.TypeofEClass(segment)
27 trainType = ecore2LogicTrace.TypeofEClass(train)
28 }
29
30 override isExact() {
31 true
32 }
33
34 override createPolyhedronExtensionOperator(Map<String, CostElementMatchers> costElementMatchers) {
35 val step2 = costElementMatchers.get(CloseTrains_step_2.instance.fullyQualifiedName)
36 val step3 = costElementMatchers.get(CloseTrains_step_3.instance.fullyQualifiedName)
37 val step4 = costElementMatchers.get(CloseTrains_step_4.instance.fullyQualifiedName)
38 val step5 = costElementMatchers.get(CloseTrains_step_5.instance.fullyQualifiedName)
39 val step6 = costElementMatchers.get(CloseTrains_step_6.instance.fullyQualifiedName)
40 val step7 = costElementMatchers.get(CloseTrains_step_7.instance.fullyQualifiedName);
41
42 [
43 val objectiveBuilder = createBuilder
44
45 for (m : step2.matches) {
46 val dimension = getDimension(m.match)
47 objectiveBuilder.add(step2.weight, dimension)
48 dimension.tightenLowerBound(0)
49 if (m.multi) {
50 createBuilder.add(1, dimension).add(-1, trainType).build.assertEqualsTo(0)
51 } else {
52 dimension.tightenUpperBound(1)
53 if (m.must) {
54 dimension.tightenLowerBound(1)
55 }
56 }
57 }
58
59 val step3Matches = step3.matches
60 for (m : step3Matches) {
61 val dimension = getDimension(m.match)
62 objectiveBuilder.add(step3.weight, dimension)
63 dimension.tightenLowerBound(0)
64 if (!m.multi) {
65 dimension.tightenUpperBound(1)
66 if (m.must) {
67 dimension.tightenLowerBound(1)
68 }
69 }
70 }
71 for (pair : step3Matches.groupBy[step2.projectMayMatch(match, 2)].entrySet) {
72 val multiplicityBuilder = createBuilder
73 for (m : pair.value) {
74 multiplicityBuilder.add(1, m.match)
75 }
76 multiplicityBuilder.add(-1, pair.key)
77 multiplicityBuilder.build.assertEqualsTo(0)
78 }
79 boundLimit(step3Matches, 2, trainType, 1)
80 boundLimit(step3Matches, 3, segmentType, 1)
81
82 val step4Matches = step4.matches
83 for (m : step4Matches) {
84 val dimension = getDimension(m.match)
85 objectiveBuilder.add(step4.weight, dimension)
86 dimension.tightenLowerBound(0)
87 if (!m.multi) {
88 dimension.tightenUpperBound(1)
89 if (m.must) {
90 dimension.tightenLowerBound(1)
91 }
92 }
93 }
94 for (pair : step4Matches.groupBy[step3.projectMayMatch(match, 2, 3)].entrySet) {
95 val multiplicityBuilder = createBuilder
96 for (m : pair.value) {
97 multiplicityBuilder.add(1, m.match)
98 }
99 multiplicityBuilder.add(-2, pair.key)
100 multiplicityBuilder.build.tightenUpperBound(0)
101 }
102 boundLimit(step4Matches, 2, trainType, 2)
103 boundLimit(step4Matches, 3, segmentType, 2)
104 boundLimit(step4Matches, 4, segmentType, 2)
105
106 val step5Matches = step5.matches
107 for (m : step5Matches) {
108 val dimension = getDimension(m.match)
109 objectiveBuilder.add(step5.weight, dimension)
110 dimension.tightenLowerBound(0)
111 if (!m.multi) {
112 dimension.tightenUpperBound(1)
113 if (m.must) {
114 dimension.tightenLowerBound(1)
115 }
116 }
117 }
118 for (pair : step5Matches.groupBy[step4.projectMayMatch(match, 2, 3, 4)].entrySet) {
119 val multiplicityBuilder = createBuilder
120 for (m : pair.value) {
121 multiplicityBuilder.add(1, m.match)
122 }
123 multiplicityBuilder.add(-2, pair.key)
124 multiplicityBuilder.build.tightenUpperBound(0)
125 }
126 boundLimit(step5Matches, 2, trainType, 4)
127 boundLimit(step5Matches, 3, segmentType, 4)
128 boundLimit(step5Matches, 4, segmentType, 4)
129 boundLimit(step5Matches, 5, segmentType, 4)
130
131 val step6Matches = step6.matches
132 for (m : step6Matches) {
133 val dimension = getDimension(m.match)
134 objectiveBuilder.add(step6.weight, dimension)
135 dimension.tightenLowerBound(0)
136 if (m.multi) {
137 if (m.match.get(3) == m.match.get(5)) {
138 createBuilder.add(2, m.match).add(-1, step5.projectMayMatch(m.match, 2, 3, 4, 5)).build.
139 assertEqualsTo(0)
140 } else {
141 createBuilder.add(1, m.match).add(-1, step5.projectMayMatch(m.match, 2, 3, 4, 5)).build.
142 assertEqualsTo(0)
143 }
144 } else {
145 dimension.tightenUpperBound(1)
146 if (m.must) {
147 dimension.tightenLowerBound(1)
148 }
149 }
150 }
151 boundLimit(step6Matches, 2, trainType, 2)
152 boundLimit(step6Matches, 3, segmentType, 2)
153 boundLimit(step6Matches, 4, segmentType, 2)
154 boundLimit(step6Matches, 5, segmentType, 2)
155
156 val step7Matches = step7.matches
157 for (m : step7Matches) {
158 val dimension = getDimension(m.match)
159 objectiveBuilder.add(step7.weight, dimension)
160 dimension.tightenLowerBound(0)
161 if (!m.multi) {
162 dimension.tightenUpperBound(1)
163 if (m.must) {
164 dimension.tightenLowerBound(1)
165 }
166 }
167 }
168 for (pair : step7Matches.groupBy[step6.projectMayMatch(match, 2, 3, 4, 5)].entrySet) {
169 val multiplicityBuilder = createBuilder
170 for (m : pair.value) {
171 multiplicityBuilder.add(1, m.match)
172 }
173 multiplicityBuilder.add(-1, pair.key)
174 multiplicityBuilder.build.tightenUpperBound(0)
175 }
176 boundLimit(step7Matches, 2, trainType, 2)
177 boundLimit(step7Matches, 3, segmentType, 2)
178 boundLimit(step7Matches, 4, segmentType, 2)
179 boundLimit(step7Matches, 5, segmentType, 2)
180 boundLimit(step7Matches, 6, trainType, 2)
181
182 objectiveBuilder.buildWithBounds
183 ]
184 }
185
186 private static def boundLimit(extension ExtendedLinearExpressionBuilderFactory factory,
187 Collection<CostElementMatch> matches, int index, Type type, int count) {
188 for (pair : matches.groupBy[match.get(index)].entrySet) {
189 val multiplicityBuilder = createBuilder
190 for (m : pair.value) {
191 multiplicityBuilder.add(1, m.match)
192 }
193 if (CostElementMatchers.isMulti(pair.key)) {
194 multiplicityBuilder.add(-count, type)
195 multiplicityBuilder.build.tightenUpperBound(0)
196 } else {
197 multiplicityBuilder.build.tightenUpperBound(count)
198 }
199 }
200 }
201}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/EndOfSidingObjectiveHint.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/EndOfSidingObjectiveHint.xtend
new file mode 100644
index 00000000..f7e23a57
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/EndOfSidingObjectiveHint.xtend
@@ -0,0 +1,139 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatch
8import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatchers
9import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint
10import java.util.Collection
11import java.util.Map
12import modes3.Modes3Package
13import modes3.queries.EndOfSiding_step_2
14import modes3.queries.EndOfSiding_step_3
15import modes3.queries.EndOfSiding_step_4
16import modes3.queries.EndOfSiding_step_5
17
18class EndOfSidingObjectiveHint extends CostObjectiveHint {
19 val Type segmentType
20 val Type trainType
21
22 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
23 extension val Modes3Package = Modes3Package.eINSTANCE
24 segmentType = ecore2LogicTrace.TypeofEClass(segment)
25 trainType = ecore2LogicTrace.TypeofEClass(train)
26 }
27
28 override isExact() {
29 true
30// false
31 }
32
33 override createPolyhedronExtensionOperator(Map<String, CostElementMatchers> costElementMatchers) {
34 val step2 = costElementMatchers.get(EndOfSiding_step_2.instance.fullyQualifiedName)
35 val step3 = costElementMatchers.get(EndOfSiding_step_3.instance.fullyQualifiedName)
36 val step4 = costElementMatchers.get(EndOfSiding_step_4.instance.fullyQualifiedName)
37 val step5 = costElementMatchers.get(EndOfSiding_step_5.instance.fullyQualifiedName);
38
39 [
40 val objectiveBuilder = createBuilder
41
42 for (m : step2.matches) {
43 val dimension = getDimension(m.match)
44 objectiveBuilder.add(step2.weight, dimension)
45 dimension.tightenLowerBound(0)
46 if (m.multi) {
47 createBuilder.add(1, dimension).add(-1, trainType).build.assertEqualsTo(0)
48 } else {
49 dimension.tightenUpperBound(1)
50 if (m.must) {
51 dimension.tightenLowerBound(1)
52 }
53 }
54 }
55
56 val step3Matches = step3.matches
57 for (m : step3Matches) {
58 val dimension = getDimension(m.match)
59 objectiveBuilder.add(step3.weight, dimension)
60 dimension.tightenLowerBound(0)
61 if (!m.multi) {
62 dimension.tightenUpperBound(1)
63 if (m.must) {
64 dimension.tightenLowerBound(1)
65 }
66 }
67 }
68 for (pair : step3Matches.groupBy[step2.projectMayMatch(match, 2)].entrySet) {
69 val multiplicityBuilder = createBuilder
70 for (m : pair.value) {
71 multiplicityBuilder.add(1, m.match)
72 }
73 multiplicityBuilder.add(-1, pair.key)
74 multiplicityBuilder.build.assertEqualsTo(0)
75 }
76 boundLimit(step3Matches, 2, trainType, 1)
77 boundLimit(step3Matches, 3, segmentType, 1)
78
79 val step4Matches = step4.matches
80 for (m : step4Matches) {
81 val dimension = getDimension(m.match)
82 objectiveBuilder.add(step4.weight, dimension)
83 dimension.tightenLowerBound(0)
84 if (!m.multi) {
85 dimension.tightenUpperBound(1)
86 if (m.must) {
87 dimension.tightenLowerBound(1)
88 }
89 }
90 }
91 for (pair : step4Matches.groupBy[step3.projectMayMatch(match, 2, 3)].entrySet) {
92 val multiplicityBuilder = createBuilder
93 for (m : pair.value) {
94 multiplicityBuilder.add(1, m.match)
95 }
96 multiplicityBuilder.add(-2, pair.key)
97 multiplicityBuilder.build.tightenUpperBound(0)
98 }
99 boundLimit(step4Matches, 2, trainType, 2)
100 boundLimit(step4Matches, 3, segmentType, 2)
101 boundLimit(step4Matches, 4, segmentType, 2)
102
103 val step5Matches = step5.matches
104 for (m : step5Matches) {
105 val dimension = getDimension(m.match)
106 objectiveBuilder.add(step5.weight, dimension)
107 dimension.tightenLowerBound(0)
108 if (!m.multi) {
109 dimension.tightenUpperBound(1)
110 if (m.must) {
111 dimension.tightenLowerBound(1)
112 }
113 }
114 createBuilder.add(1, m.match).add(-1, step4.projectMayMatch(m.match, 2, 3, 4)).build.tightenUpperBound(0)
115 }
116 boundLimit(step5Matches, 2, trainType, 1)
117 boundLimit(step5Matches, 3, segmentType, 2)
118 boundLimit(step5Matches, 4, segmentType, 1)
119
120 objectiveBuilder.buildWithBounds
121 ]
122 }
123
124 private static def boundLimit(extension ExtendedLinearExpressionBuilderFactory factory,
125 Collection<CostElementMatch> matches, int index, Type type, int count) {
126 for (pair : matches.groupBy[match.get(index)].entrySet) {
127 val multiplicityBuilder = createBuilder
128 for (m : pair.value) {
129 multiplicityBuilder.add(1, m.match)
130 }
131 if (CostElementMatchers.isMulti(pair.key)) {
132 multiplicityBuilder.add(-count, type)
133 multiplicityBuilder.build.tightenUpperBound(0)
134 } else {
135 multiplicityBuilder.build.tightenUpperBound(count)
136 }
137 }
138 }
139} \ No newline at end of file
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/MisalignedTurnoutObjectiveHint.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/MisalignedTurnoutObjectiveHint.xtend
new file mode 100644
index 00000000..cb014dea
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/MisalignedTurnoutObjectiveHint.xtend
@@ -0,0 +1,140 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatch
8import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatchers
9import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint
10import java.util.Collection
11import java.util.Map
12import modes3.Modes3Package
13import modes3.queries.MisalignedTurnout_step_2
14import modes3.queries.MisalignedTurnout_step_3
15import modes3.queries.MisalignedTurnout_step_4
16import modes3.queries.MisalignedTurnout_step_5
17
18class MisalignedTurnoutObjectiveHint extends CostObjectiveHint {
19 val Type segmentType
20 val Type turnoutType
21 val Type trainType
22
23 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
24 extension val Modes3Package = Modes3Package.eINSTANCE
25 segmentType = ecore2LogicTrace.TypeofEClass(segment)
26 turnoutType = ecore2LogicTrace.TypeofEClass(turnout)
27 trainType = ecore2LogicTrace.TypeofEClass(train)
28 }
29
30 override isExact() {
31 true
32// false
33 }
34
35 override createPolyhedronExtensionOperator(Map<String, CostElementMatchers> costElementMatchers) {
36 val step2 = costElementMatchers.get(MisalignedTurnout_step_2.instance.fullyQualifiedName)
37 val step3 = costElementMatchers.get(MisalignedTurnout_step_3.instance.fullyQualifiedName)
38 val step4 = costElementMatchers.get(MisalignedTurnout_step_4.instance.fullyQualifiedName)
39 val step5 = costElementMatchers.get(MisalignedTurnout_step_5.instance.fullyQualifiedName);
40
41 [
42 val objectiveBuilder = createBuilder
43
44 for (m : step2.matches) {
45 val dimension = getDimension(m.match)
46 objectiveBuilder.add(step2.weight, dimension)
47 dimension.tightenLowerBound(0)
48 if (m.multi) {
49 createBuilder.add(1, dimension).add(-1, turnoutType).build.assertEqualsTo(0)
50 } else {
51 dimension.tightenUpperBound(1)
52 if (m.must) {
53 dimension.tightenLowerBound(1)
54 }
55 }
56 }
57
58 val step3Matches = step3.matches
59 for (m : step3Matches) {
60 val dimension = getDimension(m.match)
61 objectiveBuilder.add(step3.weight, dimension)
62 dimension.tightenLowerBound(0)
63 if (!m.multi) {
64 dimension.tightenUpperBound(1)
65 if (m.must) {
66 dimension.tightenLowerBound(1)
67 }
68 }
69 }
70 for (pair : step3Matches.groupBy[step2.projectMayMatch(match, 2)].entrySet) {
71 val multiplicityBuilder = createBuilder
72 for (m : pair.value) {
73 multiplicityBuilder.add(1, m.match)
74 }
75 multiplicityBuilder.add(-1, pair.key)
76 multiplicityBuilder.build.tightenUpperBound(0)
77 }
78 boundLimit(step3Matches, 2, turnoutType, 1)
79 boundLimit(step3Matches, 3, segmentType, 2)
80
81 val step4Matches = step4.matches
82 for (m : step4Matches) {
83 val dimension = getDimension(m.match)
84 objectiveBuilder.add(step4.weight, dimension)
85 dimension.tightenLowerBound(0)
86 if (!m.multi) {
87 dimension.tightenUpperBound(1)
88 if (m.must) {
89 dimension.tightenLowerBound(1)
90 }
91 }
92 createBuilder.add(1, m.match).add(-1, step3.projectMayMatch(m.match, 2, 3)).build.tightenUpperBound(0)
93 }
94 boundLimit(step4Matches, 2, turnoutType, 1)
95 boundLimit(step4Matches, 3, segmentType, 2)
96
97 val step5Matches = step5.matches
98 for (m : step5Matches) {
99 val dimension = getDimension(m.match)
100 objectiveBuilder.add(step5.weight, dimension)
101 dimension.tightenLowerBound(0)
102 if (!m.multi) {
103 dimension.tightenUpperBound(1)
104 if (m.must) {
105 dimension.tightenLowerBound(1)
106 }
107 }
108 }
109 for (pair : step5Matches.groupBy[step4.projectMayMatch(match, 2, 3)].entrySet) {
110 val multiplicityBuilder = createBuilder
111 for (m : pair.value) {
112 multiplicityBuilder.add(1, m.match)
113 }
114 multiplicityBuilder.add(-1, pair.key)
115 multiplicityBuilder.build.tightenUpperBound(0)
116 }
117 boundLimit(step5Matches, 2, turnoutType, 1)
118 boundLimit(step5Matches, 3, segmentType, 2)
119 boundLimit(step5Matches, 4, trainType, 2)
120
121 objectiveBuilder.buildWithBounds
122 ]
123 }
124
125 private static def boundLimit(extension ExtendedLinearExpressionBuilderFactory factory,
126 Collection<CostElementMatch> matches, int index, Type type, int count) {
127 for (pair : matches.groupBy[match.get(index)].entrySet) {
128 val multiplicityBuilder = createBuilder
129 for (m : pair.value) {
130 multiplicityBuilder.add(1, m.match)
131 }
132 if (CostElementMatchers.isMulti(pair.key)) {
133 multiplicityBuilder.add(-count, type)
134 multiplicityBuilder.build.tightenUpperBound(0)
135 } else {
136 multiplicityBuilder.build.tightenUpperBound(count)
137 }
138 }
139 }
140}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend
new file mode 100644
index 00000000..288a7692
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend
@@ -0,0 +1,357 @@
1package modes3.run
2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.ImmutableSet
5import hu.bme.mit.inf.dslreasoner.ecore2logic.EReferenceMapper_RelationsOverTypes_Trace
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
9import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
10import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsFactory
11import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
16import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
17import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
18import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
19import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
21import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
22import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
23import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
24import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints
25import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver
26import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink
29import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
30import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
31import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration
33import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
35import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
36import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
37import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
38import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
39import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
40import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
41import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
42import java.util.List
43import modes3.Modes3Factory
44import modes3.Modes3Package
45import modes3.queries.CloseTrains_step_2
46import modes3.queries.CloseTrains_step_3
47import modes3.queries.CloseTrains_step_4
48import modes3.queries.CloseTrains_step_5
49import modes3.queries.CloseTrains_step_6
50import modes3.queries.CloseTrains_step_7
51import modes3.queries.EndOfSiding_step_2
52import modes3.queries.EndOfSiding_step_3
53import modes3.queries.EndOfSiding_step_4
54import modes3.queries.EndOfSiding_step_5
55import modes3.queries.MisalignedTurnout_step_2
56import modes3.queries.MisalignedTurnout_step_3
57import modes3.queries.MisalignedTurnout_step_4
58import modes3.queries.MisalignedTurnout_step_5
59import modes3.queries.Modes3Queries
60import modes3.queries.TrainLocations_step_2
61import modes3.queries.TrainLocations_step_3
62import org.eclipse.emf.ecore.EClass
63import org.eclipse.emf.ecore.EObject
64import org.eclipse.emf.ecore.resource.Resource
65import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
66import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
67import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions
68import org.eclipse.viatra.query.runtime.localsearch.matcher.integration.LocalSearchEMFBackendFactory
69import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
70import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
71
72@FinalFieldsConstructor
73class Modes3ModelGenerator {
74 val MonitoringQuery monitoringQuery
75 val int modelSize
76
77 val ecore2Logic = new Ecore2Logic
78 val instanceModel2Logic = new InstanceModel2Logic
79 val viatra2Logic = new Viatra2Logic(ecore2Logic)
80 val solver = new ViatraReasoner
81 extension val LogicProblemBuilder = new LogicProblemBuilder
82
83 def generate() {
84 val metamodel = createMetamodelDescriptor()
85 val metamodelLogic = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration)
86 val segment = ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.segment)
87 val connectedTo = ecore2Logic.relationOfReference(metamodelLogic.trace,
88 Modes3Package.eINSTANCE.segment_ConnectedTo)
89 val connectedToIndicator = (metamodelLogic.trace.
90 referenceMapperTrace as EReferenceMapper_RelationsOverTypes_Trace).indicators.get(
91 Modes3Package.eINSTANCE.segment_ConnectedTo)
92 val inverseAssertion = Assertion(
93 '''oppositeReference «connectedTo.name» «connectedTo.name»''',
94 Forall[
95 val src = addVar('''src''', segment)
96 val trg = addVar('''trg''', segment)
97 connectedToIndicator.call(src, trg) <=> connectedToIndicator.call(trg, src)
98 ]
99 )
100 metamodelLogic.output.assertions += inverseAssertion
101 val inverseAnnotation = Ecore2logicannotationsFactory.eINSTANCE.createInverseRelationAssertion => [
102 target = inverseAssertion
103 inverseA = connectedTo
104 inverseB = connectedTo
105 ]
106 metamodelLogic.output.annotations += inverseAnnotation
107 val initialModel = loadInitialModel()
108 val initialModelLogic = instanceModel2Logic.transform(metamodelLogic, initialModel)
109 val queries = loadQueries
110 val logic = viatra2Logic.transformQueries(queries, initialModelLogic, new Viatra2LogicConfiguration)
111 val config = new ViatraReasonerConfiguration => [
112 runtimeLimit = 3600
113 typeScopes => [
114 minNewElements = modelSize
115 maxNewElements = modelSize
116 minNewElementsByType => [
117// put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), modelSize / 5)
118// put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), modelSize / 5)
119// put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.simpleSegment), 3 * modelSize / 5)
120 ]
121 maxNewElementsByType => [
122 put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), modelSize / 5)
123 put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), modelSize / 5)
124// put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.simpleSegment), 3 * modelSize / 5)
125 ]
126 ]
127 solutionScope => [
128 numberOfRequiredSolutions = 1
129 ]
130 costObjectives += getObjective(ecore2Logic, metamodelLogic.trace)
131 scopeWeight = 6
132 nameNewElements = false
133 typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
134 stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood
135 scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(
136 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)
137 hints += new Modes3TypeScopeHint(ecore2Logic, metamodelLogic.trace)
138 unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace)
139 debugConfiguration => [
140 partialInterpretatioVisualiser = new GraphvizVisualiser
141// partalInterpretationVisualisationFrequency = 50
142 ]
143 documentationLevel = DocumentationLevel.NORMAL
144 ]
145 val workspace = new FileSystemWorkspace("output/", "")
146 workspace.writeModel(logic.output, "problem.logicproblem")
147 val solution = solver.solve(logic.output, config, workspace)
148 if (solution instanceof ModelResult) {
149 println("Saving generated solutions")
150 val logic2Ecore = new Logic2Ecore(ecore2Logic)
151 val interpretations = solver.getInterpretations(solution)
152 for (representationIndex : 0 ..< interpretations.size) {
153 val interpretation = interpretations.get(representationIndex)
154 val representationNumber = representationIndex + 1
155 if (interpretation instanceof PartialModelAsLogicInterpretation) {
156 val representation = interpretation.partialInterpretation
157 workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
158 val partialInterpretation2GML = new PartialInterpretation2Gml
159 val gml = partialInterpretation2GML.transform(representation)
160 workspace.writeText('''solution«representationNumber».gml''', gml)
161 val model = logic2Ecore.transformInterpretation(interpretation, metamodelLogic.trace)
162 val iterator = model.eAllContents
163 var int id = 0
164 while (iterator.hasNext) {
165 val obj = iterator.next
166 val idFeature = obj.eClass.EAllAttributes.findFirst[name == 'id']
167 if (idFeature !== null) {
168 obj.eSet(idFeature, id)
169 id++
170 }
171 }
172 workspace.writeModel(model, '''solution«representationNumber».modes3''')
173 if (representation.newElements.size < 160) {
174 val rootType = (representation.problem.types.findFirst [
175 name == "Modes3ModelRoot class DefinedPart"
176 ] as TypeDefinition)
177 val rootIntepretation = representation.partialtypeinterpratation.filter(
178 PartialComplexTypeInterpretation).findFirst [
179 interpretationOf.name == "Modes3ModelRoot class"
180 ]
181 rootIntepretation.elements.removeAll(rootType.elements)
182 representation.problem.elements.removeAll(rootType.elements)
183 for (relationInterpretation : representation.partialrelationinterpretation) {
184 relationInterpretation.relationlinks.removeIf [ link |
185 if (link instanceof BinaryElementRelationLink) {
186 rootType.elements.contains(link.param1) ||
187 rootType.elements.contains(link.param2)
188 } else {
189 false
190 }
191 ]
192 }
193 rootType.elements.clear
194 val visualiser = new GraphvizVisualiser
195 val visualisation = visualiser.visualiseConcretization(representation)
196 visualisation.writeToFile(workspace, '''solution«representationNumber».png''')
197 }
198 } else {
199 workspace.writeText('''solution«representationNumber».txt''', interpretation.toString)
200 }
201 }
202 } else {
203 println("Failed to solve problem")
204 val partial = logic.output
205 workspace.writeModel(partial, "solution.partialinterpretation")
206 }
207 }
208
209 static def createMetamodelDescriptor() {
210 val eClasses = ImmutableList.copyOf(Modes3Package.eINSTANCE.EClassifiers.filter(EClass))
211 new EcoreMetamodelDescriptor(
212 eClasses,
213 emptySet,
214 false,
215 emptyList,
216 emptyList,
217 ImmutableList.copyOf(eClasses.flatMap[EReferences]),
218 emptyList
219 )
220 }
221
222 static def List<EObject> loadInitialModel() {
223 #[Modes3Factory.eINSTANCE.createModes3ModelRoot]
224 }
225
226 def loadQueries() {
227 val patternsBuilder = ImmutableList.builder
228 patternsBuilder.addAll(Modes3Queries.instance.specifications)
229 val patterns = patternsBuilder.build
230 val validationPatterns = ImmutableSet.copyOf(patterns.filter [ pattern |
231 pattern.allAnnotations.exists[name == "Constraint"]
232 ])
233 new ViatraQuerySetDescriptor(
234 patterns,
235 validationPatterns,
236 emptyMap
237 )
238 }
239
240 def getObjective(Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
241 new CostObjectiveConfiguration => [
242 switch (monitoringQuery) {
243 case closeTrains: {
244 elements += new CostObjectiveElementConfiguration => [
245 patternQualifiedName = CloseTrains_step_2.instance.fullyQualifiedName
246 weight = 14 + 53 + 11
247 ]
248 elements += new CostObjectiveElementConfiguration => [
249 patternQualifiedName = CloseTrains_step_3.instance.fullyQualifiedName
250 weight = 21 + 14
251 ]
252 elements += new CostObjectiveElementConfiguration => [
253 patternQualifiedName = CloseTrains_step_4.instance.fullyQualifiedName
254 weight = 14 + 44 + 14 + 9
255 ]
256 elements += new CostObjectiveElementConfiguration => [
257 patternQualifiedName = CloseTrains_step_5.instance.fullyQualifiedName
258 weight = 14 + 41 + 11
259 ]
260 elements += new CostObjectiveElementConfiguration => [
261 patternQualifiedName = CloseTrains_step_6.instance.fullyQualifiedName
262 weight = 27
263 ]
264 elements += new CostObjectiveElementConfiguration => [
265 patternQualifiedName = CloseTrains_step_7.instance.fullyQualifiedName
266 weight = 48
267 ]
268 hint = new CloseTrainsObjectiveHint(ecore2Logic, ecore2LogicTrace)
269 }
270 case trainLocations: {
271 elements += new CostObjectiveElementConfiguration => [
272 patternQualifiedName = TrainLocations_step_2.instance.fullyQualifiedName
273 weight = 14 + 53 + 11
274 ]
275 elements += new CostObjectiveElementConfiguration => [
276 patternQualifiedName = TrainLocations_step_3.instance.fullyQualifiedName
277 weight = 48
278 ]
279 hint = new TrainLocationsObjectiveHint(ecore2Logic, ecore2LogicTrace)
280 }
281 case misalignedTurnout: {
282 elements += new CostObjectiveElementConfiguration => [
283 patternQualifiedName = MisalignedTurnout_step_2.instance.fullyQualifiedName
284 weight = 14 + 53 + 11
285 ]
286 elements += new CostObjectiveElementConfiguration => [
287 patternQualifiedName = MisalignedTurnout_step_3.instance.fullyQualifiedName
288 weight = 108
289 ]
290 elements += new CostObjectiveElementConfiguration => [
291 patternQualifiedName = MisalignedTurnout_step_4.instance.fullyQualifiedName
292 weight = 27
293 ]
294 elements += new CostObjectiveElementConfiguration => [
295 patternQualifiedName = MisalignedTurnout_step_5.instance.fullyQualifiedName
296 weight = 48
297 ]
298 hint = new MisalignedTurnoutObjectiveHint(ecore2Logic, ecore2LogicTrace)
299 }
300 case endOfSiding: {
301 elements += new CostObjectiveElementConfiguration => [
302 patternQualifiedName = EndOfSiding_step_2.instance.fullyQualifiedName
303 weight = 14 + 53 + 11
304 ]
305 elements += new CostObjectiveElementConfiguration => [
306 patternQualifiedName = EndOfSiding_step_3.instance.fullyQualifiedName
307 weight = 21 + 14
308 ]
309 elements += new CostObjectiveElementConfiguration => [
310 patternQualifiedName = EndOfSiding_step_4.instance.fullyQualifiedName
311 weight = 14 + 35 + 21 + 15 + 14 + 21 + 15 + 11
312 ]
313 elements += new CostObjectiveElementConfiguration => [
314 patternQualifiedName = EndOfSiding_step_5.instance.fullyQualifiedName
315 weight = 48
316 ]
317 hint = new EndOfSidingObjectiveHint(ecore2Logic, ecore2LogicTrace)
318 }
319 default:
320 throw new IllegalArgumentException("Unknown monitoring query: " + monitoringQuery)
321 }
322 kind = ObjectiveKind.HIGHER_IS_BETTER
323 threshold = ObjectiveThreshold.NO_THRESHOLD
324 findExtremum = true
325 ]
326 }
327
328 def static init() {
329 EMFPatternLanguageStandaloneSetup.doSetup
330 ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE,
331 LocalSearchEMFBackendFactory.INSTANCE)
332 LogiclanguagePackage.eINSTANCE.class
333 LogicproblemPackage.eINSTANCE.class
334 PartialinterpretationPackage.eINSTANCE.class
335 Ecore2logicannotationsPackage.eINSTANCE.class
336 Viatra2LogicAnnotationsPackage.eINSTANCE.class
337 Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*", new XMIResourceFactoryImpl)
338 }
339
340 def static void main(String[] args) {
341 if (args.length != 2) {
342 System.err.println("Usage: <query> <model size>")
343 }
344 val monitoringQuery = MonitoringQuery.valueOf(args.get(0))
345 val modelSize = Integer.parseInt(args.get(1))
346 init()
347 val generator = new Modes3ModelGenerator(monitoringQuery, modelSize)
348 generator.generate()
349 }
350
351 private static enum MonitoringQuery {
352 closeTrains,
353 trainLocations,
354 endOfSiding,
355 misalignedTurnout
356 }
357}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3TypeScopeHint.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3TypeScopeHint.xtend
new file mode 100644
index 00000000..94e5eb08
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3TypeScopeHint.xtend
@@ -0,0 +1,79 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
10import java.util.Map
11import modes3.Modes3Package
12import modes3.queries.Adjacent
13import org.eclipse.viatra.query.runtime.api.IPatternMatch
14import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
15import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
17
18class Modes3TypeScopeHint implements LinearTypeConstraintHint {
19 static val TURNOUT_NEIGHBOR_COUNT = "turnoutNeighborCount"
20
21 val Type segmentType
22 val Type turnoutType
23
24 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
25 extension val Modes3Package = Modes3Package.eINSTANCE
26 segmentType = ecore2LogicTrace.TypeofEClass(segment)
27 turnoutType = ecore2LogicTrace.TypeofEClass(turnout)
28 }
29
30 override getAdditionalPatterns(extension PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) {
31 '''
32 pattern «TURNOUT_NEIGHBOR_COUNT»_helper(problem: LogicProblem, interpretation: PartialInterpretation, source: DefinedElement, target: DefinedElement) {
33 find interpretation(problem, interpretation);
34 find mustExist(problem, interpretation, source);
35 find mustExist(problem, interpretation, target);
36 «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")»
37 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")»
38 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["source", "target"], Modality.MUST, true, false)»
39 }
40
41 pattern «TURNOUT_NEIGHBOR_COUNT»(problem: LogicProblem, interpretation: PartialInterpretation, element: DefinedElement, N) {
42 find interpretation(problem, interpretation);
43 find mustExist(problem, interpretation, element);
44 «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "element")»
45 N == count find «TURNOUT_NEIGHBOR_COUNT»_helper(problem, interpretation, element, _);
46 }
47 '''
48 }
49
50 override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) {
51 val turnoutNeighborCountMatcher = builderFactory.createMatcher(TURNOUT_NEIGHBOR_COUNT)
52 val newNeighbors = builderFactory.createBuilder.add(1, segmentType).build
53
54 return [ partialInterpretation |
55 val requiredNeighbbors = turnoutNeighborCountMatcher.getRemainingCount(partialInterpretation, 3)
56 newNeighbors.tightenLowerBound(requiredNeighbbors)
57 ]
58 }
59
60 private static def <T extends IPatternMatch> getRemainingCount(ViatraQueryMatcher<T> matcher,
61 PartialInterpretation partialInterpretation, int capacity) {
62 val partialMatch = matcher.newEmptyMatch
63 partialMatch.set(0, partialInterpretation.problem)
64 partialMatch.set(1, partialInterpretation)
65 val iterator = matcher.streamAllMatches(partialMatch).iterator
66 var int max = 0
67 while (iterator.hasNext) {
68 val match = iterator.next
69 val n = (match.get(3) as Integer).intValue
70 if (n < capacity) {
71 val required = capacity - n
72 if (max < required) {
73 max = required
74 }
75 }
76 }
77 max
78 }
79}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend
new file mode 100644
index 00000000..953a21d4
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend
@@ -0,0 +1,417 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator
10import java.util.Map
11import modes3.Modes3Package
12import modes3.queries.Adjacent
13import modes3.queries.Output
14import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
15import org.eclipse.xtend2.lib.StringConcatenationClient
16
17class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator {
18 static val MUST_NOT_CONNECTED_TO = "mustNotConnectedTo"
19 static val MUST_NOT_STRAIGHT = "mustNotStraight"
20 static val MUST_NOT_DIVERGENT = "mustNotDivergent"
21 static val MUST_CONNECTED_TO = "mustConnectedTo"
22 static val MUST_STRAIGHT = "mustStraight"
23 static val MUST_DIVERGENT = "mustDivergent"
24
25 val Type segmentType
26 val Type simpleSegmentType
27 val Type turnoutType
28 val Relation connectedToRelation
29 val Relation straightRelation
30 val Relation divergentRelation
31
32 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
33 extension val Modes3Package = Modes3Package.eINSTANCE
34 segmentType = ecore2LogicTrace.TypeofEClass(segment)
35 simpleSegmentType = ecore2LogicTrace.TypeofEClass(simpleSegment)
36 turnoutType = ecore2LogicTrace.TypeofEClass(turnout)
37 connectedToRelation = ecore2LogicTrace.relationOfReference(segment_ConnectedTo)
38 straightRelation = ecore2LogicTrace.relationOfReference(turnout_Straight)
39 divergentRelation = ecore2LogicTrace.relationOfReference(turnout_Divergent)
40 }
41
42 override getMustPatterns() {
43 #{
44 connectedToRelation -> MUST_CONNECTED_TO,
45 straightRelation -> MUST_STRAIGHT,
46 divergentRelation -> MUST_DIVERGENT
47 }
48 }
49
50 override getMustNotPatterns() {
51 #{
52 connectedToRelation -> MUST_NOT_CONNECTED_TO,
53 straightRelation -> MUST_NOT_STRAIGHT,
54 divergentRelation -> MUST_NOT_DIVERGENT
55 }
56 }
57
58 override getAdditionalPatterns(extension PatternGenerator generator, Map<String, PQuery> fqnToPQuery) {
59 val StringConcatenationClient parameters = '''
60 problem: LogicProblem, interpretation: PartialInterpretation,
61 source: DefinedElement, target: DefinedElement
62 '''
63
64 val StringConcatenationClient commonMustParameterConstraints = '''
65 find interpretation(problem, interpretation);
66 find mustExist(problem, interpretation, source);
67 find mustExist(problem, interpretation, target);
68 '''
69
70 val StringConcatenationClient commonMayParameterConstraints = '''
71 find interpretation(problem, interpretation);
72 find mayExist(problem, interpretation, source);
73 find mayExist(problem, interpretation, target);
74 '''
75
76 '''
77 pattern mayInput(«parameters») {
78 «commonMayParameterConstraints»
79 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
80 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["target", "source"], Modality.MAY, true, false)»
81 neg «referRelation(straightRelation, "target", "source", Modality.MUST, fqnToPQuery)»
82 neg «referRelation(straightRelation, "target", "source", Modality.MUST, fqnToPQuery)»
83 }
84
85 pattern multipleMayInput(problem: LogicProblem, interpretation: PartialInterpretation,
86 target: DefinedElement) {
87 find interpretation(problem, interpretation);
88 find mustExist(problem, interpretation, target);
89 find mayInput(problem, interpretaton, source1, target);
90 find mayInput(problem, interpretaton, source2, target);
91 neg find mustEquivalent(problem, interpretation, source1, source2);
92 }
93
94 pattern multipleMayStraight(problem: LogicProblem, interpretation: PartialInterpretation,
95 source: DefinedElement) {
96 find interpretation(problem, interpretation);
97 find mustExist(problem, interpretation, source);
98 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
99 «referRelation(straightRelation, "source", "target1", Modality.MAY, fqnToPQuery)»
100 «referRelation(straightRelation, "source", "target2", Modality.MAY, fqnToPQuery)»
101 neg find mustEquivalent(problem, interpretation, target1, target2);
102 }
103
104 pattern multipleMayDivergent(problem: LogicProblem, interpretation: PartialInterpretation,
105 source: DefinedElement) {
106 find interpretation(problem, interpretation);
107 find mustExist(problem, interpretation, source);
108 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
109 «referRelation(divergentRelation, "source", "target1", Modality.MAY, fqnToPQuery)»
110 «referRelation(divergentRelation, "source", "target2", Modality.MAY, fqnToPQuery)»
111 neg find mustEquivalent(problem, interpretation, target1, target2);
112 }
113
114 pattern «MUST_CONNECTED_TO»(«parameters») {
115 «commonMustParameterConstraints»
116 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
117 find mayInput(problem, interpretaton, source, target);
118 neg find multipleMayInput(problem, interpretaton, target);
119 «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)»
120 neg «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)»
121 neg «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)»
122 neg «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)»
123 }
124
125 pattern «MUST_STRAIGHT»(«parameters») {
126 «commonMustParameterConstraints»
127 neg «referRelation(straightRelation, "source", "_", Modality.MUST, fqnToPQuery)»
128 neg find multipleMayStraight(problem, interpretation, source);
129 «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)»
130 neg «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)»
131 } or {
132 «commonMustParameterConstraints»
133 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
134 find mayInput(problem, interpretaton, source, target);
135 neg find multipleMayInput(problem, interpretaton, target);
136 neg «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)»
137 «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)»
138 neg «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)»
139 neg «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)»
140 }
141
142 pattern «MUST_DIVERGENT»(«parameters») {
143 «commonMustParameterConstraints»
144 neg «referRelation(divergentRelation, "source", "_", Modality.MUST, fqnToPQuery)»
145 neg find multipleMayDivergent(problem, interpretation, source);
146 «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)»
147 neg «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)»
148 } or {
149 «commonMustParameterConstraints»
150 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
151 find mayInput(problem, interpretaton, source, target);
152 neg find multipleMayInput(problem, interpretaton, target);
153 neg «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)»
154 neg «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)»
155 «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)»
156 neg «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)»
157 }
158
159 pattern turnoutOutput_must_to_true_by_straight(«parameters», T : DefinedElement, S : DefinedElement) {
160 «commonMayParameterConstraints»
161 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
162 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
163 T == source;
164 S == target;
165 }
166
167 pattern turnoutOutput_must_to_true_by_divergent(«parameters», T : DefinedElement, S : DefinedElement) {
168 «commonMayParameterConstraints»
169 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
170 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
171 T == source;
172 S == target;
173 }
174
175 pattern output_must_to_true_by_connectedTo(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
176 «commonMayParameterConstraints»
177 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "source")»
178 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
179 S1 == source;
180 S2 == target;
181 }
182
183 pattern output_must_to_true_by_straight(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
184 find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, S1, S2);
185 }
186
187 pattern output_must_to_true_by_divergent(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
188 find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, S1, S2);
189 }
190
191 pattern adjacent_must_to_true_by_connectedTo(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
192 find output_must_to_true_by_connectedTo(problem, interpretation, source, target, S1, S2);
193 }
194
195 pattern adjacent_must_to_true_by_straight(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
196 find output_must_to_true_by_straight(problem, interpretation, source, target, S1, S2);
197 } or {
198 find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, S2, S1);
199 }
200
201 pattern adjacent_must_to_true_by_divergent(«parameters», S1 : DefinedElement, S2 : DefinedElement) {
202 find output_must_to_true_by_divergent(problem, interpretation, source, target, S1, S2);
203 } or {
204 find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, S2, S1);
205 }
206
207 pattern connectedToReflexive_must_to_true_by_connectedTo(«parameters», S : DefinedElement) {
208 find mustExist(problem, interpretation, source);
209 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")»
210 S == source;
211 S == target;
212 }
213
214 pattern outputReflexive_must_to_true_by_straight(«parameters», T : DefinedElement) {
215 find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, T, T);
216 }
217
218 pattern outputReflexive_must_to_true_by_divergent(«parameters», T : DefinedElement) {
219 find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, T, T);
220 }
221
222 pattern turnoutOutputsAreSame_must_to_true_by_straight(«parameters», T : DefinedElement) {
223 «commonMayParameterConstraints»
224 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
225 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
226 T == source;
227 S == target;
228 «referRelation(divergentRelation, "T", "S", Modality.MUST, fqnToPQuery)»
229 }
230
231 pattern turnoutOutputsAreSame_must_to_true_by_divergent(«parameters», T : DefinedElement) {
232 «commonMayParameterConstraints»
233 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
234 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
235 T == source;
236 S == target;
237 «referRelation(straightRelation, "T", "S", Modality.MUST, fqnToPQuery)»
238 }
239
240 pattern tooManyInputsOfSegment_must_to_true_by_connectedTo(«parameters», S : DefinedElement) {
241 find mustExist(problem, interpretation, S);
242 «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")»
243 find output_must_to_true_by_connectedTo(problem, interpretation, source, target, I1, S);
244 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
245 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
246 I1 != I2;
247 I1 != I3;
248 I2 != I3;
249 }
250
251 pattern tooManyInputsOfSegment_must_to_true_by_straight(«parameters», S : DefinedElement) {
252 find mustExist(problem, interpretation, S);
253 «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")»
254 find output_must_to_true_by_straight(problem, interpretation, source, target, I1, S);
255 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
256 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
257 I1 != I2;
258 I1 != I3;
259 I2 != I3;
260 }
261
262 pattern tooManyInputsOfSegment_must_to_true_by_divergent(«parameters», S : DefinedElement) {
263 find mustExist(problem, interpretation, S);
264 «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")»
265 find output_must_to_true_by_divergent(problem, interpretation, source, target, I1, S);
266 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
267 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
268 I1 != I2;
269 I1 != I3;
270 I2 != I3;
271 }
272
273 pattern turnoutConnectedToBothOutputs_must_to_true_by_connectedTo(«parameters», T : DefinedElement) {
274 «commonMayParameterConstraints»
275 find mustExist(problem, interpretation, Straight);
276 find mustExist(problem, interpretation, Divergent);
277 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
278 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
279 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")»
280 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")»
281 «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
282 «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
283 T == source;
284 Straight == target;
285 «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
286 } or {
287 «commonMayParameterConstraints»
288 find mustExist(problem, interpretation, Straight);
289 find mustExist(problem, interpretation, Divergent);
290 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
291 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
292 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")»
293 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")»
294 «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
295 «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
296 «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
297 T == source;
298 Straight == target;
299 }
300
301 pattern turnoutConnectedToBothOutputs_must_to_true_by_straight(«parameters», T : DefinedElement) {
302 «commonMayParameterConstraints»
303 find mustExist(problem, interpretation, Straight);
304 find mustExist(problem, interpretation, Divergent);
305 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
306 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
307 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")»
308 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")»
309 T == source;
310 Straight == target;
311 «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
312 «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
313 «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
314 }
315
316 pattern turnoutConnectedToBothOutputs_must_to_true_by_divergent(«parameters», T : DefinedElement) {
317 «commonMayParameterConstraints»
318 find mustExist(problem, interpretation, Straight);
319 find mustExist(problem, interpretation, Divergent);
320 «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")»
321 «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")»
322 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")»
323 «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")»
324 «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
325 T == source;
326 Divergent == target;
327 «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)»
328 «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)»
329 }
330
331 pattern tooManyInputsOfTurnout_must_to_true_by_connectedTo(«parameters», T : DefinedElement) {
332 find mustExist(problem, interpretation, S);
333 «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")»
334 find adjacent_must_to_true_by_connectedTo(problem, interpretation, source, target, I1, S);
335 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
336 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
337 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)»
338 I1 != I2;
339 I1 != I3;
340 I1 != I4;
341 I2 != I3;
342 I2 != I4;
343 I3 != I4;
344 }
345
346 pattern tooManyInputsOfTurnout_must_to_true_by_straight(«parameters», T : DefinedElement) {
347 find mustExist(problem, interpretation, S);
348 «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")»
349 find adjacent_must_to_true_by_straight(problem, interpretation, source, target, I1, S);
350 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
351 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
352 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)»
353 I1 != I2;
354 I1 != I3;
355 I1 != I4;
356 I2 != I3;
357 I2 != I4;
358 I3 != I4;
359 }
360
361 pattern tooManyInputsOfTurnout_must_to_true_by_divergent(«parameters», T : DefinedElement) {
362 find mustExist(problem, interpretation, S);
363 «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")»
364 find adjacent_must_to_true_by_divergent(problem, interpretation, source, target, I1, S);
365 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)»
366 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)»
367 «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)»
368 I1 != I2;
369 I1 != I3;
370 I1 != I4;
371 I2 != I3;
372 I2 != I4;
373 I3 != I4;
374 }
375
376 pattern «MUST_NOT_CONNECTED_TO»_helper(«parameters») {
377 find connectedToReflexive_must_to_true_by_connectedTo(problem, interpretation, source, target, _);
378 } or {
379 find tooManyInputsOfSegment_must_to_true_by_connectedTo(problem, interpretation, source, target, _);
380 } or {
381 find turnoutConnectedToBothOutputs_must_to_true_by_connectedTo(problem, interpretation, source, target, _);
382 } or {
383 find tooManyInputsOfTurnout_must_to_true_by_connectedTo(problem, interpretation, source, target, _);
384 }
385
386 pattern «MUST_NOT_CONNECTED_TO»(«parameters») {
387 find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, source, target);
388 } or {
389 find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, target, source);
390 }
391
392 pattern «MUST_NOT_STRAIGHT»(«parameters») {
393 find outputReflexive_must_to_true_by_straight(problem, interpretation, source, target, _);
394 } or {
395 find turnoutOutputsAreSame_must_to_true_by_straight(problem, interpretation, source, target, _);
396 } or {
397 find tooManyInputsOfSegment_must_to_true_by_straight(problem, interpretation, source, target, _);
398 } or {
399 find turnoutConnectedToBothOutputs_must_to_true_by_straight(problem, interpretation, source, target, _);
400 } or {
401 find tooManyInputsOfTurnout_must_to_true_by_straight(problem, interpretation, source, target, _);
402 }
403
404 pattern «MUST_NOT_DIVERGENT»(«parameters») {
405 find outputReflexive_must_to_true_by_divergent(problem, interpretation, source, target, _);
406 } or {
407 find turnoutOutputsAreSame_must_to_true_by_divergent(problem, interpretation, source, target, _);
408 } or {
409 find tooManyInputsOfSegment_must_to_true_by_divergent(problem, interpretation, source, target, _);
410 } or {
411 find turnoutConnectedToBothOutputs_must_to_true_by_divergent(problem, interpretation, source, target, _);
412 } or {
413 find tooManyInputsOfTurnout_must_to_true_by_divergent(problem, interpretation, source, target, _);
414 }
415 '''
416 }
417}
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/TrainLocationsObjectiveHint.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/TrainLocationsObjectiveHint.xtend
new file mode 100644
index 00000000..cc2d7925
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/TrainLocationsObjectiveHint.xtend
@@ -0,0 +1,85 @@
1package modes3.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatch
8import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostElementMatchers
9import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint
10import java.util.Collection
11import java.util.Map
12import modes3.Modes3Package
13import modes3.queries.TrainLocations_step_2
14import modes3.queries.TrainLocations_step_3
15
16class TrainLocationsObjectiveHint extends CostObjectiveHint {
17 val Type segmentType
18 val Type trainType
19
20 new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) {
21 extension val Modes3Package = Modes3Package.eINSTANCE
22 segmentType = ecore2LogicTrace.TypeofEClass(segment)
23 trainType = ecore2LogicTrace.TypeofEClass(train)
24 }
25
26 override isExact() {
27 true
28 }
29
30 override createPolyhedronExtensionOperator(Map<String, CostElementMatchers> costElementMatchers) {
31 val step2 = costElementMatchers.get(TrainLocations_step_2.instance.fullyQualifiedName)
32 val step3 = costElementMatchers.get(TrainLocations_step_3.instance.fullyQualifiedName);
33
34 [
35 val objectiveBuilder = createBuilder
36
37 for (m : step2.matches) {
38 val dimension = getDimension(m.match)
39 objectiveBuilder.add(step2.weight, dimension)
40 dimension.tightenLowerBound(0)
41 if (m.multi) {
42 createBuilder.add(1, dimension).add(-1, trainType).build.assertEqualsTo(0)
43 } else {
44 dimension.tightenUpperBound(1)
45 if (m.must) {
46 dimension.tightenLowerBound(1)
47 }
48 }
49 }
50
51 val step3Matches = step3.matches
52 for (m : step3Matches) {
53 val dimension = getDimension(m.match)
54 objectiveBuilder.add(step3.weight, dimension)
55 dimension.tightenLowerBound(0)
56 if (!m.multi) {
57 dimension.tightenUpperBound(1)
58 if (m.must) {
59 dimension.tightenLowerBound(1)
60 }
61 }
62 }
63 boundLimit(step3Matches, 2, trainType, 1)
64 boundLimit(step3Matches, 3, segmentType, 1)
65
66 objectiveBuilder.buildWithBounds
67 ]
68 }
69
70 private static def boundLimit(extension ExtendedLinearExpressionBuilderFactory factory,
71 Collection<CostElementMatch> matches, int index, Type type, int count) {
72 for (pair : matches.groupBy[match.get(index)].entrySet) {
73 val multiplicityBuilder = createBuilder
74 for (m : pair.value) {
75 multiplicityBuilder.add(1, m.match)
76 }
77 if (CostElementMatchers.isMulti(pair.key)) {
78 multiplicityBuilder.add(-count, type)
79 multiplicityBuilder.build.tightenUpperBound(0)
80 } else {
81 multiplicityBuilder.build.tightenUpperBound(count)
82 }
83 }
84 }
85} \ No newline at end of file
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-30 17:17:45 +0000