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 | |
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')
4 files changed, 464 insertions, 169 deletions
diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql index 982e6cec..b8841928 100644 --- a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | |||
@@ -2,11 +2,6 @@ package modes3.queries | |||
2 | 2 | ||
3 | import "http://www.ece.mcgill.ca/wcet/modes3" | 3 | import "http://www.ece.mcgill.ca/wcet/modes3" |
4 | 4 | ||
5 | @Constraint(message = "turnoutInSegments", severity = "error", key = { T }) | ||
6 | pattern turnoutInSegments(T : Turnout) { | ||
7 | Modes3ModelRoot.segments(_, T); | ||
8 | } | ||
9 | |||
10 | pattern connectedTo(S1 : Segment, S2 : Segment) { | 5 | pattern connectedTo(S1 : Segment, S2 : Segment) { |
11 | Segment.connectedTo(S1, S2); | 6 | Segment.connectedTo(S1, S2); |
12 | } | 7 | } |
@@ -39,10 +34,6 @@ pattern turnoutOutputsAreSame(T : Turnout) { | |||
39 | Turnout.divergent(T, S); | 34 | Turnout.divergent(T, S); |
40 | } | 35 | } |
41 | 36 | ||
42 | pattern turnout(T : Turnout) { | ||
43 | Turnout(T); | ||
44 | } | ||
45 | |||
46 | pattern output(S1 : Segment, S2 : Segment) { | 37 | pattern output(S1 : Segment, S2 : Segment) { |
47 | Segment.connectedTo(S1, S2); | 38 | Segment.connectedTo(S1, S2); |
48 | } or { | 39 | } or { |
@@ -56,8 +47,7 @@ pattern output(S1 : Segment, S2 : Segment) { | |||
56 | //} | 47 | //} |
57 | 48 | ||
58 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) | 49 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) |
59 | pattern tooManyInputsOfSegment(S : Segment) { | 50 | pattern tooManyInputsOfSegment(S : SimpleSegment) { |
60 | neg find turnout(S); | ||
61 | find output(I1, S); | 51 | find output(I1, S); |
62 | find output(I2, S); | 52 | find output(I2, S); |
63 | find output(I3, S); | 53 | find output(I3, S); |
@@ -74,30 +64,38 @@ pattern turnoutConnectedToBothOutputs(T : Turnout) { | |||
74 | Segment.connectedTo(T, Divergent); | 64 | Segment.connectedTo(T, Divergent); |
75 | } | 65 | } |
76 | 66 | ||
77 | pattern extraInputOfTurnout(T : Turnout, S : Segment) { | 67 | pattern adjacent(S1 : Segment, S2 : Segment) { |
78 | Turnout.straight(T, Straight); | 68 | find output(S1, S2); |
79 | Turnout.divergent(T, Divergent); | 69 | } or { |
80 | find output(S, T); | 70 | find turnoutOutput(S2, S1); |
81 | S != Straight; | ||
82 | S != Divergent; | ||
83 | } | 71 | } |
84 | 72 | ||
85 | @Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T }) | 73 | @Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T }) |
86 | pattern noExtraInputOfTurnout(T : Turnout) { | 74 | pattern tooManyInputsOfTurnout(T : Turnout) { |
87 | neg find extraInputOfTurnout(T, _); | 75 | find adjacent(I1, T); |
76 | find adjacent(I2, T); | ||
77 | find adjacent(I3, T); | ||
78 | find adjacent(I4, T); | ||
79 | I1 != I2; | ||
80 | I1 != I3; | ||
81 | I1 != I4; | ||
82 | I2 != I3; | ||
83 | I2 != I4; | ||
84 | I3 != I4; | ||
88 | } | 85 | } |
89 | 86 | ||
90 | @Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T }) | 87 | pattern inputsOfTurnout(T : Turnout) { |
91 | pattern tooManyExtraInputsOfTurnout(T : Turnout) { | 88 | find adjacent(I1, T); |
92 | find extraInputOfTurnout(T, I1); | 89 | find adjacent(I2, T); |
93 | find extraInputOfTurnout(T, I2); | 90 | find adjacent(I3, T); |
94 | I1 != I2; | 91 | I1 != I2; |
92 | I1 != I3; | ||
93 | I2 != I3; | ||
95 | } | 94 | } |
96 | 95 | ||
97 | pattern adjacent(S1 : Segment, S2 : Segment) { | 96 | @Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T }) |
98 | find output(S1, S2); | 97 | pattern tooFewInputsOfTurnout(T : Turnout) { |
99 | } or { | 98 | neg find inputsOfTurnout(T); |
100 | find turnoutOutput(S2, S1); | ||
101 | } | 99 | } |
102 | 100 | ||
103 | pattern reachable(S1 : Segment, S2 : Segment) { | 101 | pattern reachable(S1 : Segment, S2 : Segment) { |
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 index 71d1798f..fac7c496 100644 --- a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend | |||
@@ -8,6 +8,7 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | |||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | 8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsFactory | 9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsFactory |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
@@ -22,6 +23,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr | |||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
@@ -44,8 +46,6 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions | |||
44 | import org.eclipse.viatra.query.runtime.localsearch.matcher.integration.LocalSearchEMFBackendFactory | 46 | import org.eclipse.viatra.query.runtime.localsearch.matcher.integration.LocalSearchEMFBackendFactory |
45 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | 47 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory |
46 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 48 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
48 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
49 | 49 | ||
50 | @FinalFieldsConstructor | 50 | @FinalFieldsConstructor |
51 | class Modes3ModelGenerator { | 51 | class Modes3ModelGenerator { |
@@ -92,22 +92,32 @@ class Modes3ModelGenerator { | |||
92 | minNewElements = modelSize | 92 | minNewElements = modelSize |
93 | maxNewElements = modelSize | 93 | maxNewElements = modelSize |
94 | minNewElementsByType => [ | 94 | minNewElementsByType => [ |
95 | put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 1) | 95 | // put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 5) |
96 | ] | 96 | ] |
97 | maxNewElementsByType => [ | 97 | maxNewElementsByType => [ |
98 | put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), 5) | 98 | put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), 5) |
99 | put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 5) | ||
99 | ] | 100 | ] |
100 | ] | 101 | ] |
101 | solutionScope.numberOfRequiredSolutions = 1 | 102 | solutionScope => [ |
103 | numberOfRequiredSolutions = 1 | ||
104 | ] | ||
105 | scopeWeight = 5 | ||
102 | nameNewElements = false | 106 | nameNewElements = false |
103 | typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | 107 | typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis |
104 | stateCoderStrategy = StateCoderStrategy::Neighbourhood | 108 | stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood |
105 | scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | 109 | scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( |
106 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 110 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) |
107 | // unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace) | 111 | hints += new Modes3TypeScopeHint(ecore2Logic, metamodelLogic.trace) |
108 | debugConfiguration.partialInterpretatioVisualiser = null | 112 | unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace) |
113 | debugConfiguration => [ | ||
114 | partialInterpretatioVisualiser = new GraphvizVisualiser | ||
115 | // partalInterpretationVisualisationFrequency = 50 | ||
116 | ] | ||
117 | documentationLevel = DocumentationLevel.NORMAL | ||
109 | ] | 118 | ] |
110 | val workspace = new FileSystemWorkspace("output/", "") | 119 | val workspace = new FileSystemWorkspace("output/", "") |
120 | workspace.writeModel(logic.output, "problem.logicproblem") | ||
111 | val solution = solver.solve(logic.output, config, workspace) | 121 | val solution = solver.solve(logic.output, config, workspace) |
112 | if (solution instanceof ModelResult) { | 122 | if (solution instanceof ModelResult) { |
113 | println("Saving generated solutions") | 123 | println("Saving generated solutions") |
@@ -122,7 +132,6 @@ class Modes3ModelGenerator { | |||
122 | workspace.writeText('''solution«representationNumber».gml''', gml) | 132 | workspace.writeText('''solution«representationNumber».gml''', gml) |
123 | if (representation.newElements.size < 160) { | 133 | if (representation.newElements.size < 160) { |
124 | if (representation instanceof PartialInterpretation) { | 134 | if (representation instanceof PartialInterpretation) { |
125 | representation.problem.types.forEach[println(name)] | ||
126 | val rootType = (representation.problem.types.findFirst [ | 135 | val rootType = (representation.problem.types.findFirst [ |
127 | name == "Modes3ModelRoot class DefinedPart" | 136 | name == "Modes3ModelRoot class DefinedPart" |
128 | ] as TypeDefinition) | 137 | ] as TypeDefinition) |
@@ -198,10 +207,7 @@ class Modes3ModelGenerator { | |||
198 | PartialinterpretationPackage.eINSTANCE.class | 207 | PartialinterpretationPackage.eINSTANCE.class |
199 | Ecore2logicannotationsPackage.eINSTANCE.class | 208 | Ecore2logicannotationsPackage.eINSTANCE.class |
200 | Viatra2LogicAnnotationsPackage.eINSTANCE.class | 209 | Viatra2LogicAnnotationsPackage.eINSTANCE.class |
201 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("ecore", new XMIResourceFactoryImpl) | 210 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*", new XMIResourceFactoryImpl) |
202 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("logicproblem", new XMIResourceFactoryImpl) | ||
203 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("partialinterpretation", | ||
204 | new XMIResourceFactoryImpl) | ||
205 | } | 211 | } |
206 | 212 | ||
207 | def static void main(String[] args) { | 213 | def static void main(String[] args) { |
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 @@ | |||
1 | package modes3.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
10 | import java.util.Map | ||
11 | import modes3.Modes3Package | ||
12 | import modes3.queries.Adjacent | ||
13 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
14 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
15 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
17 | |||
18 | class 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 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 | } |