From 4fe7fce97aedbd516109ef81afc33e00112b7b68 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 28 Aug 2020 18:58:37 +0200 Subject: Must unit propagation --- .../src/modes3/queries/Modes3Queries.vql | 54 ++- .../src/modes3/run/Modes3ModelGenerator.xtend | 30 +- .../src/modes3/run/Modes3TypeScopeHint.xtend | 79 ++++ .../run/Modes3UnitPropagationGenerator.xtend | 470 +++++++++++++++------ 4 files changed, 464 insertions(+), 169 deletions(-) create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3TypeScopeHint.xtend (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3') 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 import "http://www.ece.mcgill.ca/wcet/modes3" -@Constraint(message = "turnoutInSegments", severity = "error", key = { T }) -pattern turnoutInSegments(T : Turnout) { - Modes3ModelRoot.segments(_, T); -} - pattern connectedTo(S1 : Segment, S2 : Segment) { Segment.connectedTo(S1, S2); } @@ -39,10 +34,6 @@ pattern turnoutOutputsAreSame(T : Turnout) { Turnout.divergent(T, S); } -pattern turnout(T : Turnout) { - Turnout(T); -} - pattern output(S1 : Segment, S2 : Segment) { Segment.connectedTo(S1, S2); } or { @@ -56,8 +47,7 @@ pattern output(S1 : Segment, S2 : Segment) { //} @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) -pattern tooManyInputsOfSegment(S : Segment) { - neg find turnout(S); +pattern tooManyInputsOfSegment(S : SimpleSegment) { find output(I1, S); find output(I2, S); find output(I3, S); @@ -74,30 +64,38 @@ pattern turnoutConnectedToBothOutputs(T : Turnout) { Segment.connectedTo(T, Divergent); } -pattern extraInputOfTurnout(T : Turnout, S : Segment) { - Turnout.straight(T, Straight); - Turnout.divergent(T, Divergent); - find output(S, T); - S != Straight; - S != Divergent; +pattern adjacent(S1 : Segment, S2 : Segment) { + find output(S1, S2); +} or { + find turnoutOutput(S2, S1); } -@Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T }) -pattern noExtraInputOfTurnout(T : Turnout) { - neg find extraInputOfTurnout(T, _); +@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T }) +pattern tooManyInputsOfTurnout(T : Turnout) { + find adjacent(I1, T); + find adjacent(I2, T); + find adjacent(I3, T); + find adjacent(I4, T); + I1 != I2; + I1 != I3; + I1 != I4; + I2 != I3; + I2 != I4; + I3 != I4; } -@Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T }) -pattern tooManyExtraInputsOfTurnout(T : Turnout) { - find extraInputOfTurnout(T, I1); - find extraInputOfTurnout(T, I2); +pattern inputsOfTurnout(T : Turnout) { + find adjacent(I1, T); + find adjacent(I2, T); + find adjacent(I3, T); I1 != I2; + I1 != I3; + I2 != I3; } -pattern adjacent(S1 : Segment, S2 : Segment) { - find output(S1, S2); -} or { - find turnoutOutput(S2, S1); +@Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T }) +pattern tooFewInputsOfTurnout(T : Turnout) { + neg find inputsOfTurnout(T); } 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 import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsFactory import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition @@ -22,6 +23,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage @@ -44,8 +46,6 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions import org.eclipse.viatra.query.runtime.localsearch.matcher.integration.LocalSearchEMFBackendFactory import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink @FinalFieldsConstructor class Modes3ModelGenerator { @@ -92,22 +92,32 @@ class Modes3ModelGenerator { minNewElements = modelSize maxNewElements = modelSize minNewElementsByType => [ - put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 1) +// put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 5) ] maxNewElementsByType => [ put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), 5) + put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 5) ] ] - solutionScope.numberOfRequiredSolutions = 1 + solutionScope => [ + numberOfRequiredSolutions = 1 + ] + scopeWeight = 5 nameNewElements = false typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis - stateCoderStrategy = StateCoderStrategy::Neighbourhood + stateCoderStrategy = StateCoderStrategy.PairwiseNeighbourhood scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) -// unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace) - debugConfiguration.partialInterpretatioVisualiser = null + hints += new Modes3TypeScopeHint(ecore2Logic, metamodelLogic.trace) + unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace) + debugConfiguration => [ + partialInterpretatioVisualiser = new GraphvizVisualiser +// partalInterpretationVisualisationFrequency = 50 + ] + documentationLevel = DocumentationLevel.NORMAL ] val workspace = new FileSystemWorkspace("output/", "") + workspace.writeModel(logic.output, "problem.logicproblem") val solution = solver.solve(logic.output, config, workspace) if (solution instanceof ModelResult) { println("Saving generated solutions") @@ -122,7 +132,6 @@ class Modes3ModelGenerator { workspace.writeText('''solution«representationNumber».gml''', gml) if (representation.newElements.size < 160) { if (representation instanceof PartialInterpretation) { - representation.problem.types.forEach[println(name)] val rootType = (representation.problem.types.findFirst [ name == "Modes3ModelRoot class DefinedPart" ] as TypeDefinition) @@ -198,10 +207,7 @@ class Modes3ModelGenerator { PartialinterpretationPackage.eINSTANCE.class Ecore2logicannotationsPackage.eINSTANCE.class Viatra2LogicAnnotationsPackage.eINSTANCE.class - Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("ecore", new XMIResourceFactoryImpl) - Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("logicproblem", new XMIResourceFactoryImpl) - Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("partialinterpretation", - new XMIResourceFactoryImpl) + Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*", new XMIResourceFactoryImpl) } 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 @@ +package modes3.run + +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator +import java.util.Map +import modes3.Modes3Package +import modes3.queries.Adjacent +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation + +class Modes3TypeScopeHint implements LinearTypeConstraintHint { + static val TURNOUT_NEIGHBOR_COUNT = "turnoutNeighborCount" + + val Type segmentType + val Type turnoutType + + new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) { + extension val Modes3Package = Modes3Package.eINSTANCE + segmentType = ecore2LogicTrace.TypeofEClass(segment) + turnoutType = ecore2LogicTrace.TypeofEClass(turnout) + } + + override getAdditionalPatterns(extension PatternGenerator patternGenerator, Map fqnToPQuery) { + ''' + pattern «TURNOUT_NEIGHBOR_COUNT»_helper(problem: LogicProblem, interpretation: PartialInterpretation, source: DefinedElement, target: DefinedElement) { + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, source); + find mustExist(problem, interpretation, target); + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["source", "target"], Modality.MUST, true, false)» + } + + pattern «TURNOUT_NEIGHBOR_COUNT»(problem: LogicProblem, interpretation: PartialInterpretation, element: DefinedElement, N) { + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, element); + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "element")» + N == count find «TURNOUT_NEIGHBOR_COUNT»_helper(problem, interpretation, element, _); + } + ''' + } + + override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) { + val turnoutNeighborCountMatcher = builderFactory.createMatcher(TURNOUT_NEIGHBOR_COUNT) + val newNeighbors = builderFactory.createBuilder.add(1, segmentType).build + + return [ partialInterpretation | + val requiredNeighbbors = turnoutNeighborCountMatcher.getRemainingCount(partialInterpretation, 3) + newNeighbors.tightenLowerBound(requiredNeighbbors) + ] + } + + private static def getRemainingCount(ViatraQueryMatcher matcher, + PartialInterpretation partialInterpretation, int capacity) { + val partialMatch = matcher.newEmptyMatch + partialMatch.set(0, partialInterpretation.problem) + partialMatch.set(1, partialInterpretation) + val iterator = matcher.streamAllMatches(partialMatch).iterator + var int max = 0 + while (iterator.hasNext) { + val match = iterator.next + val n = (match.get(3) as Integer).intValue + if (n < capacity) { + val required = capacity - n + if (max < required) { + max = required + } + } + } + max + } +} 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 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator import java.util.Map import modes3.Modes3Package -import modes3.queries.ExtraInputOfTurnout +import modes3.queries.Adjacent import modes3.queries.Output -import modes3.queries.TurnoutOutput import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery import org.eclipse.xtend2.lib.StringConcatenationClient class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator { static val MUST_NOT_CONNECTED_TO = "mustNotConnectedTo" - static val MUST_NOT_CONNECTED_TO_HELPER = "mustNotConnectedTo_helper" - static val MUST_NOT_TURNOUT_OUTPUT = "mustNotTurnoutOutput" static val MUST_NOT_STRAIGHT = "mustNotStraight" static val MUST_NOT_DIVERGENT = "mustNotDivergent" + static val MUST_CONNECTED_TO = "mustConnectedTo" + static val MUST_STRAIGHT = "mustStraight" + static val MUST_DIVERGENT = "mustDivergent" val Type segmentType + val Type simpleSegmentType val Type turnoutType val Relation connectedToRelation val Relation straightRelation @@ -31,6 +32,7 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) { extension val Modes3Package = Modes3Package.eINSTANCE segmentType = ecore2LogicTrace.TypeofEClass(segment) + simpleSegmentType = ecore2LogicTrace.TypeofEClass(simpleSegment) turnoutType = ecore2LogicTrace.TypeofEClass(turnout) connectedToRelation = ecore2LogicTrace.relationOfReference(segment_ConnectedTo) straightRelation = ecore2LogicTrace.relationOfReference(turnout_Straight) @@ -38,7 +40,11 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator } override getMustPatterns() { - emptyMap + #{ + connectedToRelation -> MUST_CONNECTED_TO, + straightRelation -> MUST_STRAIGHT, + divergentRelation -> MUST_DIVERGENT + } } override getMustNotPatterns() { @@ -55,150 +61,356 @@ class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator source: DefinedElement, target: DefinedElement ''' - val StringConcatenationClient commonParameterConstraints = ''' + val StringConcatenationClient commonMustParameterConstraints = ''' find interpretation(problem, interpretation); find mustExist(problem, interpretation, source); find mustExist(problem, interpretation, target); ''' + + val StringConcatenationClient commonMayParameterConstraints = ''' + find interpretation(problem, interpretation); + find mayExist(problem, interpretation, source); + find mayExist(problem, interpretation, target); + ''' ''' - pattern «MUST_NOT_CONNECTED_TO_HELPER»(«parameters») { - // connectedToReflexive unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - source == target; + pattern mayInput(«parameters») { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["target", "source"], Modality.MAY, true, false)» + neg «referRelation(straightRelation, "target", "source", Modality.MUST, fqnToPQuery)» + neg «referRelation(straightRelation, "target", "source", Modality.MUST, fqnToPQuery)» + } + + pattern multipleMayInput(problem: LogicProblem, interpretation: PartialInterpretation, + target: DefinedElement) { + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, target); + find mayInput(problem, interpretaton, source1, target); + find mayInput(problem, interpretaton, source2, target); + neg find mustEquivalent(problem, interpretation, source1, source2); + } + + pattern multipleMayStraight(problem: LogicProblem, interpretation: PartialInterpretation, + source: DefinedElement) { + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, source); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «referRelation(straightRelation, "source", "target1", Modality.MAY, fqnToPQuery)» + «referRelation(straightRelation, "source", "target2", Modality.MAY, fqnToPQuery)» + neg find mustEquivalent(problem, interpretation, target1, target2); + } + + pattern multipleMayDivergent(problem: LogicProblem, interpretation: PartialInterpretation, + source: DefinedElement) { + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, source); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «referRelation(divergentRelation, "source", "target1", Modality.MAY, fqnToPQuery)» + «referRelation(divergentRelation, "source", "target2", Modality.MAY, fqnToPQuery)» + neg find mustEquivalent(problem, interpretation, target1, target2); + } + + pattern «MUST_CONNECTED_TO»(«parameters») { + «commonMustParameterConstraints» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + find mayInput(problem, interpretaton, source, target); + neg find multipleMayInput(problem, interpretaton, target); + «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)» + neg «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)» + } + + pattern «MUST_STRAIGHT»(«parameters») { + «commonMustParameterConstraints» + neg «referRelation(straightRelation, "source", "_", Modality.MUST, fqnToPQuery)» + neg find multipleMayStraight(problem, interpretation, source); + «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» } or { - // tooManyInputsOfSegment unit propagation - «commonParameterConstraints» + «commonMustParameterConstraints» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + find mayInput(problem, interpretaton, source, target); + neg find multipleMayInput(problem, interpretaton, target); + neg «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)» + «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» + neg «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)» + } + + pattern «MUST_DIVERGENT»(«parameters») { + «commonMustParameterConstraints» + neg «referRelation(divergentRelation, "source", "_", Modality.MUST, fqnToPQuery)» + neg find multipleMayDivergent(problem, interpretation, source); + «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» + } or { + «commonMustParameterConstraints» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + find mayInput(problem, interpretaton, source, target); + neg find multipleMayInput(problem, interpretaton, target); + neg «referRelation(connectedToRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(straightRelation, "source", "target", Modality.MAY, fqnToPQuery)» + «referRelation(divergentRelation, "source", "target", Modality.MAY, fqnToPQuery)» + neg «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» + } + + pattern turnoutOutput_must_to_true_by_straight(«parameters», T : DefinedElement, S : DefinedElement) { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + T == source; + S == target; + } + + pattern turnoutOutput_must_to_true_by_divergent(«parameters», T : DefinedElement, S : DefinedElement) { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + T == source; + S == target; + } + + pattern output_must_to_true_by_connectedTo(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + S1 == source; + S2 == target; + } + + pattern output_must_to_true_by_straight(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, S1, S2); + } + + pattern output_must_to_true_by_divergent(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, S1, S2); + } + + pattern adjacent_must_to_true_by_connectedTo(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + find output_must_to_true_by_connectedTo(problem, interpretation, source, target, S1, S2); + } + + pattern adjacent_must_to_true_by_straight(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + find output_must_to_true_by_straight(problem, interpretation, source, target, S1, S2); + } or { + find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, S2, S1); + } + + pattern adjacent_must_to_true_by_divergent(«parameters», S1 : DefinedElement, S2 : DefinedElement) { + find output_must_to_true_by_divergent(problem, interpretation, source, target, S1, S2); + } or { + find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, S2, S1); + } + + pattern connectedToReflexive_must_to_true_by_connectedTo(«parameters», S : DefinedElement) { + find mustExist(problem, interpretation, source); «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input1")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input2")» - neg «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input1", "source"], Modality.MUST, true, false)» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input2", "source"], Modality.MUST, true, false)» - input1 != input2; - input1 != target; - input2 != target; - } or { - // turnoutConnectedToBothOutputs unit propagation 1 - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "divergent")» - «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» - «referRelation(divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» - «referRelation(connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» - } or { - // turnoutConnectedToBothOutputs unit propagation 2 - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "straight")» - «referRelation(straightRelation, "source", "straight", Modality.MUST, fqnToPQuery)» - «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» - «referRelation(connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery)» - } or { - // tooManyExtraInputsOfTurnout unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(TurnoutOutput.instance.fullyQualifiedName), #["source", "target"], Modality.MAY, false, false)» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» - target != extraInput; + S == source; + S == target; } - pattern «MUST_NOT_CONNECTED_TO»(«parameters») { - find «MUST_NOT_CONNECTED_TO_HELPER»(problem, interpretation, source, target); + pattern outputReflexive_must_to_true_by_straight(«parameters», T : DefinedElement) { + find turnoutOutput_must_to_true_by_straight(problem, interpretation, source, target, T, T); + } + + pattern outputReflexive_must_to_true_by_divergent(«parameters», T : DefinedElement) { + find turnoutOutput_must_to_true_by_divergent(problem, interpretation, source, target, T, T); + } + + pattern turnoutOutputsAreSame_must_to_true_by_straight(«parameters», T : DefinedElement) { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + T == source; + S == target; + «referRelation(divergentRelation, "T", "S", Modality.MUST, fqnToPQuery)» + } + + pattern turnoutOutputsAreSame_must_to_true_by_divergent(«parameters», T : DefinedElement) { + «commonMayParameterConstraints» + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + T == source; + S == target; + «referRelation(straightRelation, "T", "S", Modality.MUST, fqnToPQuery)» + } + + pattern tooManyInputsOfSegment_must_to_true_by_connectedTo(«parameters», S : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")» + find output_must_to_true_by_connectedTo(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I2 != I3; + } + + pattern tooManyInputsOfSegment_must_to_true_by_straight(«parameters», S : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")» + find output_must_to_true_by_straight(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I2 != I3; + } + + pattern tooManyInputsOfSegment_must_to_true_by_divergent(«parameters», S : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(simpleSegmentType, Modality.MUST, "S")» + find output_must_to_true_by_divergent(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I2 != I3; + } + + pattern turnoutConnectedToBothOutputs_must_to_true_by_connectedTo(«parameters», T : DefinedElement) { + «commonMayParameterConstraints» + find mustExist(problem, interpretation, Straight); + find mustExist(problem, interpretation, Divergent); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")» + «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» + T == source; + Straight == target; + «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» } or { - find «MUST_NOT_CONNECTED_TO_HELPER»(problem, interpretation, target, source); + «commonMayParameterConstraints» + find mustExist(problem, interpretation, Straight); + find mustExist(problem, interpretation, Divergent); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")» + «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» + «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + T == source; + Straight == target; } - pattern «MUST_NOT_TURNOUT_OUTPUT»(«parameters») { - // outputReflexive unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "target")» - source == target; + pattern turnoutConnectedToBothOutputs_must_to_true_by_straight(«parameters», T : DefinedElement) { + «commonMayParameterConstraints» + find mustExist(problem, interpretation, Straight); + find mustExist(problem, interpretation, Divergent); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")» + T == source; + Straight == target; + «referRelation(divergentRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» + «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» + } + + pattern turnoutConnectedToBothOutputs_must_to_true_by_divergent(«parameters», T : DefinedElement) { + «commonMayParameterConstraints» + find mustExist(problem, interpretation, Straight); + find mustExist(problem, interpretation, Divergent); + «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "source")» + «typeIndexer.referInstanceOf(segmentType, Modality.MAY, "target")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Straight")» + «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "Divergent")» + «referRelation(straightRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + T == source; + Divergent == target; + «referRelation(connectedToRelation, "T", "Straight", Modality.MUST, fqnToPQuery)» + «referRelation(connectedToRelation, "T", "Divergent", Modality.MUST, fqnToPQuery)» + } + + pattern tooManyInputsOfTurnout_must_to_true_by_connectedTo(«parameters», T : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")» + find adjacent_must_to_true_by_connectedTo(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I1 != I4; + I2 != I3; + I2 != I4; + I3 != I4; + } + + pattern tooManyInputsOfTurnout_must_to_true_by_straight(«parameters», T : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")» + find adjacent_must_to_true_by_straight(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I1 != I4; + I2 != I3; + I2 != I4; + I3 != I4; + } + + pattern tooManyInputsOfTurnout_must_to_true_by_divergent(«parameters», T : DefinedElement) { + find mustExist(problem, interpretation, S); + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "S")» + find adjacent_must_to_true_by_divergent(problem, interpretation, source, target, I1, S); + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I2", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I3", "S"], Modality.MUST, true, false)» + «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Adjacent.instance.fullyQualifiedName), #["I4", "S"], Modality.MUST, true, false)» + I1 != I2; + I1 != I3; + I1 != I4; + I2 != I3; + I2 != I4; + I3 != I4; + } + + pattern «MUST_NOT_CONNECTED_TO»_helper(«parameters») { + find connectedToReflexive_must_to_true_by_connectedTo(problem, interpretation, source, target, _); } or { - // tooManyInputsOfSegment unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input1")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "input2")» - neg «typeIndexer.referInstanceOf(turnoutType, Modality.MAY, "target")» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input1", "target"], Modality.MUST, true, false)» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(Output.instance.fullyQualifiedName), #["input2", "target"], Modality.MUST, true, false)» - input1 != input2; - input1 != source; - input2 != source; + find tooManyInputsOfSegment_must_to_true_by_connectedTo(problem, interpretation, source, target, _); + } or { + find turnoutConnectedToBothOutputs_must_to_true_by_connectedTo(problem, interpretation, source, target, _); + } or { + find tooManyInputsOfTurnout_must_to_true_by_connectedTo(problem, interpretation, source, target, _); + } + + pattern «MUST_NOT_CONNECTED_TO»(«parameters») { + find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, source, target); + } or { + find «MUST_NOT_CONNECTED_TO»_helper(problem, interpretation, target, source); } pattern «MUST_NOT_STRAIGHT»(«parameters») { - find «MUST_NOT_TURNOUT_OUTPUT»(problem, interpretation, source, target); - } or { - // turnoutOutputsAreSame unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «referRelation(divergentRelation, "source", "target", Modality.MUST, fqnToPQuery)» - } or { - // turnoutConnectedToBothOutputs unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "divergent")» - «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)» - «referRelation(divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» - «referRelation(connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery)» - } or { - // tooManyExtraInputsOfTurnout unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "potentialExtraInput")» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» - «referRelation(connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery)» - neg «referRelation(divergentRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery)» - extraInput != potentialExtraInput; - extraInput != target; - potentialExtraInput != target; + find outputReflexive_must_to_true_by_straight(problem, interpretation, source, target, _); + } or { + find turnoutOutputsAreSame_must_to_true_by_straight(problem, interpretation, source, target, _); + } or { + find tooManyInputsOfSegment_must_to_true_by_straight(problem, interpretation, source, target, _); + } or { + find turnoutConnectedToBothOutputs_must_to_true_by_straight(problem, interpretation, source, target, _); + } or { + find tooManyInputsOfTurnout_must_to_true_by_straight(problem, interpretation, source, target, _); } pattern «MUST_NOT_DIVERGENT»(«parameters») { - find «MUST_NOT_TURNOUT_OUTPUT»(problem, interpretation, source, target); - } or { - // turnoutOutputsAreSame unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «referRelation(straightRelation, "source", "target", Modality.MUST, fqnToPQuery)» - } or { - // turnoutConnectedToBothOutputs unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "straight")» - «referRelation(connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery)» - «referRelation(straightRelation, "source", "straight", Modality.MUST, fqnToPQuery)» - «referRelation(connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery)» - } or { - // tooManyExtraInputsOfTurnout unit propagation - «commonParameterConstraints» - «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "target")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "extraInput")» - «typeIndexer.referInstanceOf(segmentType, Modality.MUST, "potentialExtraInput")» - «relationDefinitionIndexer.referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance.fullyQualifiedName), #["source", "extraInput"], Modality.MUST, true, false)» - «referRelation(connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery)» - neg «referRelation(straightRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery)» - extraInput != potentialExtraInput; - extraInput != target; - potentialExtraInput != target; + find outputReflexive_must_to_true_by_divergent(problem, interpretation, source, target, _); + } or { + find turnoutOutputsAreSame_must_to_true_by_divergent(problem, interpretation, source, target, _); + } or { + find tooManyInputsOfSegment_must_to_true_by_divergent(problem, interpretation, source, target, _); + } or { + find turnoutConnectedToBothOutputs_must_to_true_by_divergent(problem, interpretation, source, target, _); + } or { + find tooManyInputsOfTurnout_must_to_true_by_divergent(problem, interpretation, source, target, _); } ''' } -- cgit v1.2.3-54-g00ecf