diff options
author | 2020-08-28 18:58:37 +0200 | |
---|---|---|
committer | 2020-08-28 18:58:37 +0200 | |
commit | 4fe7fce97aedbd516109ef81afc33e00112b7b68 (patch) | |
tree | 7eaa7c4e9b31b2a1488e49de48721b4dbad31fae /Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend | |
parent | MoDeS3 unit propagation WIP (diff) | |
download | VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.tar.gz VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.tar.zst VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.zip |
Must unit propagation
Diffstat (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend')
-rw-r--r-- | Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend | 470 |
1 files changed, 341 insertions, 129 deletions
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 index 61bd2814..953a21d4 100644 --- a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend | |||
@@ -9,20 +9,21 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGene | |||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator |
10 | import java.util.Map | 10 | import java.util.Map |
11 | import modes3.Modes3Package | 11 | import modes3.Modes3Package |
12 | import modes3.queries.ExtraInputOfTurnout | 12 | import modes3.queries.Adjacent |
13 | import modes3.queries.Output | 13 | import modes3.queries.Output |
14 | import modes3.queries.TurnoutOutput | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 14 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
16 | import org.eclipse.xtend2.lib.StringConcatenationClient | 15 | import org.eclipse.xtend2.lib.StringConcatenationClient |
17 | 16 | ||
18 | class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator { | 17 | class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator { |
19 | static val MUST_NOT_CONNECTED_TO = "mustNotConnectedTo" | 18 | static val MUST_NOT_CONNECTED_TO = "mustNotConnectedTo" |
20 | static val MUST_NOT_CONNECTED_TO_HELPER = "mustNotConnectedTo_helper" | ||
21 | static val MUST_NOT_TURNOUT_OUTPUT = "mustNotTurnoutOutput" | ||
22 | static val MUST_NOT_STRAIGHT = "mustNotStraight" | 19 | static val MUST_NOT_STRAIGHT = "mustNotStraight" |
23 | static val MUST_NOT_DIVERGENT = "mustNotDivergent" | 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 | 24 | ||
25 | val Type segmentType | 25 | val Type segmentType |
26 | val Type simpleSegmentType | ||
26 | val Type turnoutType | 27 | val Type turnoutType |
27 | val Relation connectedToRelation | 28 | val Relation connectedToRelation |
28 | val Relation straightRelation | 29 | val Relation straightRelation |
@@ -31,6 +32,7 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator | |||
31 | new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) { | 32 | new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) { |
32 | extension val Modes3Package = Modes3Package.eINSTANCE | 33 | extension val Modes3Package = Modes3Package.eINSTANCE |
33 | segmentType = ecore2LogicTrace.TypeofEClass(segment) | 34 | segmentType = ecore2LogicTrace.TypeofEClass(segment) |
35 | simpleSegmentType = ecore2LogicTrace.TypeofEClass(simpleSegment) | ||
34 | turnoutType = ecore2LogicTrace.TypeofEClass(turnout) | 36 | turnoutType = ecore2LogicTrace.TypeofEClass(turnout) |
35 | connectedToRelation = ecore2LogicTrace.relationOfReference(segment_ConnectedTo) | 37 | connectedToRelation = ecore2LogicTrace.relationOfReference(segment_ConnectedTo) |
36 | straightRelation = ecore2LogicTrace.relationOfReference(turnout_Straight) | 38 | straightRelation = ecore2LogicTrace.relationOfReference(turnout_Straight) |
@@ -38,7 +40,11 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator | |||
38 | } | 40 | } |
39 | 41 | ||
40 | override getMustPatterns() { | 42 | override getMustPatterns() { |
41 | emptyMap | 43 | #{ |
44 | connectedToRelation -> MUST_CONNECTED_TO, | ||
45 | straightRelation -> MUST_STRAIGHT, | ||
46 | divergentRelation -> MUST_DIVERGENT | ||
47 | } | ||
42 | } | 48 | } |
43 | 49 | ||
44 | override getMustNotPatterns() { | 50 | override getMustNotPatterns() { |
@@ -55,150 +61,356 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator | |||
55 | source: DefinedElement, target: DefinedElement | 61 | source: DefinedElement, target: DefinedElement |
56 | ''' | 62 | ''' |
57 | 63 | ||
58 | val StringConcatenationClient commonParameterConstraints = ''' | 64 | val StringConcatenationClient commonMustParameterConstraints = ''' |
59 | find interpretation(problem, interpretation); | 65 | find interpretation(problem, interpretation); |
60 | find mustExist(problem, interpretation, source); | 66 | find mustExist(problem, interpretation, source); |
61 | find mustExist(problem, interpretation, target); | 67 | find mustExist(problem, interpretation, target); |
62 | ''' | 68 | ''' |
69 | |||
70 | val StringConcatenationClient commonMayParameterConstraints = ''' | ||
71 | find interpretation(problem, interpretation); | ||
72 | find mayExist(problem, interpretation, source); | ||
73 | find mayExist(problem, interpretation, target); | ||
74 | ''' | ||
63 | 75 | ||
64 | ''' | 76 | ''' |
65 | pattern «MUST_NOT_CONNECTED_TO_HELPER»(«parameters») { | 77 | pattern mayInput(«parameters») { |
66 | // connectedToReflexive unit propagation | 78 | «commonMayParameterConstraints» |
67 | «commonParameterConstraints» | 79 | «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» |
68 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")» | 80 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["target", "source"], Modality.MAY, true, false)» |
69 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | 81 | neg «referRelation(straightRelation, "target", "source", Modality.MUST, fqnToPQuery)» |
70 | source == target; | 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)» | ||
71 | } or { | 131 | } or { |
72 | // tooManyInputsOfSegment unit propagation | 132 | «commonMustParameterConstraints» |
73 | «commonParameterConstraints» | 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); | ||
74 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")» | 209 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")» |
75 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | 210 | S == source; |
76 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input1")» | 211 | S == target; |
77 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input2")» | ||
78 | neg «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» | ||
79 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input1", "source"], Modality.MUST, true, false)» | ||
80 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input2", "source"], Modality.MUST, true, false)» | ||
81 | input1 != input2; | ||
82 | input1 != target; | ||
83 | input2 != target; | ||
84 | } or { | ||
85 | // turnoutConnectedToBothOutputs unit propagation 1 | ||
86 | «commonParameterConstraints» | ||
87 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
88 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
89 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "divergent")» | ||
90 | «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» | ||
91 | «referRelation(divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» | ||
92 | «referRelation(connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» | ||
93 | } or { | ||
94 | // turnoutConnectedToBothOutputs unit propagation 2 | ||
95 | «commonParameterConstraints» | ||
96 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
97 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
98 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "straight")» | ||
99 | «referRelation(straightRelation, "source", "straight", Modality.MUST, fqnToPQuery)» | ||
100 | «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» | ||
101 | «referRelation(connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery)» | ||
102 | } or { | ||
103 | // tooManyExtraInputsOfTurnout unit propagation | ||
104 | «commonParameterConstraints» | ||
105 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
106 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
107 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» | ||
108 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(TurnoutOutput.instance.fullyQualifiedName), #["source", "target"], Modality.MAY, false, false)» | ||
109 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» | ||
110 | target != extraInput; | ||
111 | } | 212 | } |
112 | 213 | ||
113 | pattern «MUST_NOT_CONNECTED_TO»(«parameters») { | 214 | pattern outputReflexive_must_to_true_by_straight(«parameters», T : DefinedElement) { |
114 | find «MUST_NOT_CONNECTED_TO_HELPER»(problem, interpretation, source, target); | 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)» | ||
115 | } or { | 286 | } or { |
116 | find «MUST_NOT_CONNECTED_TO_HELPER»(problem, interpretation, target, source); | 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; | ||
117 | } | 299 | } |
118 | 300 | ||
119 | pattern «MUST_NOT_TURNOUT_OUTPUT»(«parameters») { | 301 | pattern turnoutConnectedToBothOutputs_must_to_true_by_straight(«parameters», T : DefinedElement) { |
120 | // outputReflexive unit propagation | 302 | «commonMayParameterConstraints» |
121 | «commonParameterConstraints» | 303 | find mustExist(problem, interpretation, Straight); |
122 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | 304 | find mustExist(problem, interpretation, Divergent); |
123 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "target")» | 305 | «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» |
124 | source == target; | 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, _); | ||
125 | } or { | 378 | } or { |
126 | // tooManyInputsOfSegment unit propagation | 379 | find tooManyInputsOfSegment_must_to_true_by_connectedTo(problem, interpretation, source, target, _); |
127 | «commonParameterConstraints» | 380 | } or { |
128 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | 381 | find turnoutConnectedToBothOutputs_must_to_true_by_connectedTo(problem, interpretation, source, target, _); |
129 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | 382 | } or { |
130 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input1")» | 383 | find tooManyInputsOfTurnout_must_to_true_by_connectedTo(problem, interpretation, source, target, _); |
131 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input2")» | 384 | } |
132 | neg «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "target")» | 385 | |
133 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input1", "target"], Modality.MUST, true, false)» | 386 | pattern «MUST_NOT_CONNECTED_TO»(«parameters») { |
134 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input2", "target"], Modality.MUST, true, false)» | 387 | find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, source, target); |
135 | input1 != input2; | 388 | } or { |
136 | input1 != source; | 389 | find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, target, source); |
137 | input2 != source; | ||
138 | } | 390 | } |
139 | 391 | ||
140 | pattern «MUST_NOT_STRAIGHT»(«parameters») { | 392 | pattern «MUST_NOT_STRAIGHT»(«parameters») { |
141 | find «MUST_NOT_TURNOUT_OUTPUT»(problem, interpretation, source, target); | 393 | find outputReflexive_must_to_true_by_straight(problem, interpretation, source, target, _); |
142 | } or { | 394 | } or { |
143 | // turnoutOutputsAreSame unit propagation | 395 | find turnoutOutputsAreSame_must_to_true_by_straight(problem, interpretation, source, target, _); |
144 | «commonParameterConstraints» | 396 | } or { |
145 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | 397 | find tooManyInputsOfSegment_must_to_true_by_straight(problem, interpretation, source, target, _); |
146 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | 398 | } or { |
147 | «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» | 399 | find turnoutConnectedToBothOutputs_must_to_true_by_straight(problem, interpretation, source, target, _); |
148 | } or { | 400 | } or { |
149 | // turnoutConnectedToBothOutputs unit propagation | 401 | find tooManyInputsOfTurnout_must_to_true_by_straight(problem, interpretation, source, target, _); |
150 | «commonParameterConstraints» | ||
151 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
152 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
153 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "divergent")» | ||
154 | «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)» | ||
155 | «referRelation(divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» | ||
156 | «referRelation(connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» | ||
157 | } or { | ||
158 | // tooManyExtraInputsOfTurnout unit propagation | ||
159 | «commonParameterConstraints» | ||
160 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
161 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
162 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» | ||
163 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "potentialExtraInput")» | ||
164 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» | ||
165 | «referRelation(connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery)» | ||
166 | neg «referRelation(divergentRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery)» | ||
167 | extraInput != potentialExtraInput; | ||
168 | extraInput != target; | ||
169 | potentialExtraInput != target; | ||
170 | } | 402 | } |
171 | 403 | ||
172 | pattern «MUST_NOT_DIVERGENT»(«parameters») { | 404 | pattern «MUST_NOT_DIVERGENT»(«parameters») { |
173 | find «MUST_NOT_TURNOUT_OUTPUT»(problem, interpretation, source, target); | 405 | find outputReflexive_must_to_true_by_divergent(problem, interpretation, source, target, _); |
174 | } or { | 406 | } or { |
175 | // turnoutOutputsAreSame unit propagation | 407 | find turnoutOutputsAreSame_must_to_true_by_divergent(problem, interpretation, source, target, _); |
176 | «commonParameterConstraints» | 408 | } or { |
177 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | 409 | find tooManyInputsOfSegment_must_to_true_by_divergent(problem, interpretation, source, target, _); |
178 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | 410 | } or { |
179 | «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» | 411 | find turnoutConnectedToBothOutputs_must_to_true_by_divergent(problem, interpretation, source, target, _); |
180 | } or { | 412 | } or { |
181 | // turnoutConnectedToBothOutputs unit propagation | 413 | find tooManyInputsOfTurnout_must_to_true_by_divergent(problem, interpretation, source, target, _); |
182 | «commonParameterConstraints» | ||
183 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
184 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
185 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "straight")» | ||
186 | «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)» | ||
187 | «referRelation(straightRelation, "source", "straight", Modality.MUST, fqnToPQuery)» | ||
188 | «referRelation(connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery)» | ||
189 | } or { | ||
190 | // tooManyExtraInputsOfTurnout unit propagation | ||
191 | «commonParameterConstraints» | ||
192 | «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» | ||
193 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» | ||
194 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» | ||
195 | «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "potentialExtraInput")» | ||
196 | «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» | ||
197 | «referRelation(connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery)» | ||
198 | neg «referRelation(straightRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery)» | ||
199 | extraInput != potentialExtraInput; | ||
200 | extraInput != target; | ||
201 | potentialExtraInput != target; | ||
202 | } | 414 | } |
203 | ''' | 415 | ''' |
204 | } | 416 | } |