From a620f07468780778bd55dcffc30245def37ece69 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 6 Aug 2020 16:07:16 +0200 Subject: MoDeS3 unit propagation WIP --- .../src/modes3/queries/Modes3Queries.vql | 112 +++++++++++ .../src/modes3/run/Modes3ModelGenerator.xtend | 222 +++++++++++++++++++++ .../run/Modes3UnitPropagationGenerator.xtend | 205 +++++++++++++++++++ 3 files changed, 539 insertions(+) create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src') diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql new file mode 100644 index 00000000..982e6cec --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql @@ -0,0 +1,112 @@ +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); +} + +@Constraint(message = "connectedToNotSymmetric", severity = "error", key = { S1, S2 }) +pattern connectedToNotSymmetric(S1 : Segment, S2 : Segment) { + Segment.connectedTo(S1, S2); + neg find connectedTo(S2, S1); +} + +@Constraint(message = "connectedToReflexive", severity = "error", key = { S }) +pattern connectedToReflexive(S : Segment) { + Segment.connectedTo(S, S); +} + +pattern turnoutOutput(T : Turnout, S : Segment) { + Turnout.straight(T, S); +} or { + Turnout.divergent(T, S); +} + +@Constraint(message = "outputReflexive", severity = "error", key = { T }) +pattern outputReflexive(T : Turnout) { + find turnoutOutput(T, T); +} + +@Constraint(message = "turnoutOutputsAreSame", severity = "error", key = { T }) +pattern turnoutOutputsAreSame(T : Turnout) { + Turnout.straight(T, S); + Turnout.divergent(T, S); +} + +pattern turnout(T : Turnout) { + Turnout(T); +} + +pattern output(S1 : Segment, S2 : Segment) { + Segment.connectedTo(S1, S2); +} or { + find turnoutOutput(S1, S2); +} + +//@Constraint(message = "noInputOfSegment", severity = "error", key = { S }) +//pattern noInputOfSegment(S : Segment) { +// neg find turnout(S); +// neg find output(_, S); +//} + +@Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) +pattern tooManyInputsOfSegment(S : Segment) { + neg find turnout(S); + find output(I1, S); + find output(I2, S); + find output(I3, S); + I1 != I2; + I1 != I3; + I2 != I3; +} + +@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T }) +pattern turnoutConnectedToBothOutputs(T : Turnout) { + Turnout.straight(T, Straight); + Turnout.divergent(T, Divergent); + Segment.connectedTo(T, Straight); + 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; +} + +@Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T }) +pattern noExtraInputOfTurnout(T : Turnout) { + neg find extraInputOfTurnout(T, _); +} + +@Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T }) +pattern tooManyExtraInputsOfTurnout(T : Turnout) { + find extraInputOfTurnout(T, I1); + find extraInputOfTurnout(T, I2); + I1 != I2; +} + +pattern adjacent(S1 : Segment, S2 : Segment) { + find output(S1, S2); +} or { + find turnoutOutput(S2, S1); +} + +pattern reachable(S1 : Segment, S2 : Segment) { + S1 == S2; +} or { + find adjacent+(S1, S2); +} + +@Constraint(message = "unreachable", severity = "error", key = { S1, S2 }) +pattern unreachable(S1 : Segment, S2 : Segment) { + neg find reachable(S1, S2); +} diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend new file mode 100644 index 00000000..71d1798f --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3ModelGenerator.xtend @@ -0,0 +1,222 @@ +package modes3.run + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableSet +import hu.bme.mit.inf.dslreasoner.ecore2logic.EReferenceMapper_RelationsOverTypes_Trace +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +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.LogicProblemBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints +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.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration +import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.List +import modes3.Modes3Factory +import modes3.Modes3Package +import modes3.queries.Modes3Queries +import org.eclipse.emf.ecore.EClass +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl +import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup +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 { + val MonitoringQuery monitoringQuery + val int modelSize + + val ecore2Logic = new Ecore2Logic + val instanceModel2Logic = new InstanceModel2Logic + val viatra2Logic = new Viatra2Logic(ecore2Logic) + val solver = new ViatraReasoner + extension val LogicProblemBuilder = new LogicProblemBuilder + + def generate() { + val metamodel = createMetamodelDescriptor() + val metamodelLogic = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration) + val segment = ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.segment) + val connectedTo = ecore2Logic.relationOfReference(metamodelLogic.trace, + Modes3Package.eINSTANCE.segment_ConnectedTo) + val connectedToIndicator = (metamodelLogic.trace. + referenceMapperTrace as EReferenceMapper_RelationsOverTypes_Trace).indicators.get( + Modes3Package.eINSTANCE.segment_ConnectedTo) + val inverseAssertion = Assertion( + '''oppositeReference «connectedTo.name» «connectedTo.name»''', + Forall[ + val src = addVar('''src''', segment) + val trg = addVar('''trg''', segment) + connectedToIndicator.call(src, trg) <=> connectedToIndicator.call(trg, src) + ] + ) + metamodelLogic.output.assertions += inverseAssertion + val inverseAnnotation = Ecore2logicannotationsFactory.eINSTANCE.createInverseRelationAssertion => [ + target = inverseAssertion + inverseA = connectedTo + inverseB = connectedTo + ] + metamodelLogic.output.annotations += inverseAnnotation + val initialModel = loadInitialModel() + val initialModelLogic = instanceModel2Logic.transform(metamodelLogic, initialModel) + val queries = loadQueries + val logic = viatra2Logic.transformQueries(queries, initialModelLogic, new Viatra2LogicConfiguration) + val config = new ViatraReasonerConfiguration => [ + runtimeLimit = 3600 + typeScopes => [ + minNewElements = modelSize + maxNewElements = modelSize + minNewElementsByType => [ + put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.turnout), 1) + ] + maxNewElementsByType => [ + put(ecore2Logic.TypeofEClass(metamodelLogic.trace, Modes3Package.eINSTANCE.train), 5) + ] + ] + solutionScope.numberOfRequiredSolutions = 1 + nameNewElements = false + typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis + stateCoderStrategy = StateCoderStrategy::Neighbourhood + scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( + PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) +// unitPropagationPatternGenerators += new Modes3UnitPropagationGenerator(ecore2Logic, metamodelLogic.trace) + debugConfiguration.partialInterpretatioVisualiser = null + ] + val workspace = new FileSystemWorkspace("output/", "") + val solution = solver.solve(logic.output, config, workspace) + if (solution instanceof ModelResult) { + println("Saving generated solutions") + val representations = solution.representation + for (representationIndex : 0 ..< representations.size) { + val representation = representations.get(representationIndex) + val representationNumber = representationIndex + 1 + if (representation instanceof PartialInterpretation) { + workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') + val partialInterpretation2GML = new PartialInterpretation2Gml + val gml = partialInterpretation2GML.transform(representation) + 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) + val rootIntepretation = representation.partialtypeinterpratation.filter( + PartialComplexTypeInterpretation).findFirst [ + interpretationOf.name == "Modes3ModelRoot class" + ] + rootIntepretation.elements.removeAll(rootType.elements) + representation.problem.elements.removeAll(rootType.elements) + for (relationInterpretation : representation.partialrelationinterpretation) { + relationInterpretation.relationlinks.removeIf [ link | + if (link instanceof BinaryElementRelationLink) { + rootType.elements.contains(link.param1) || rootType.elements.contains(link.param2) + } else { + false + } + ] + } + rootType.elements.clear + } + val visualiser = new GraphvizVisualiser + val visualisation = visualiser.visualiseConcretization(representation) + visualisation.writeToFile(workspace, '''solution«representationNumber».png''') + } + } else { + workspace.writeText('''solution«representationNumber».txt''', representation.toString) + } + } + } else { + println("Failed to solver problem") + val partial = logic.output + workspace.writeModel(partial, "solution.partialinterpretation") + } + } + + static def createMetamodelDescriptor() { + val eClasses = ImmutableList.copyOf(Modes3Package.eINSTANCE.EClassifiers.filter(EClass)) + new EcoreMetamodelDescriptor( + eClasses, + emptySet, + false, + emptyList, + emptyList, + ImmutableList.copyOf(eClasses.flatMap[EReferences]), + emptyList + ) + } + + static def List loadInitialModel() { + #[Modes3Factory.eINSTANCE.createModes3ModelRoot] + } + + def loadQueries() { + val patternsBuilder = ImmutableList.builder + patternsBuilder.addAll(Modes3Queries.instance.specifications) + val patterns = patternsBuilder.build + val validationPatterns = ImmutableSet.copyOf(patterns.filter [ pattern | + pattern.allAnnotations.exists[name == "Constraint"] + ]) + new ViatraQuerySetDescriptor( + patterns, + validationPatterns, + emptyMap + ) + } + + def static init() { + EMFPatternLanguageStandaloneSetup.doSetup + ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE, + LocalSearchEMFBackendFactory.INSTANCE) + LogiclanguagePackage.eINSTANCE.class + LogicproblemPackage.eINSTANCE.class + 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) + } + + def static void main(String[] args) { + if (args.length != 2) { + System.err.println("Usage: ") + } + val monitoringQuery = MonitoringQuery.valueOf(args.get(0)) + val modelSize = Integer.parseInt(args.get(1)) + init() + val generator = new Modes3ModelGenerator(monitoringQuery, modelSize) + generator.generate() + } + + private static enum MonitoringQuery { + closeTrains, + misalignedTurnout + } +} diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend new file mode 100644 index 00000000..61bd2814 --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/run/Modes3UnitPropagationGenerator.xtend @@ -0,0 +1,205 @@ +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.Relation +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.patterns.PatternGenerator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator +import java.util.Map +import modes3.Modes3Package +import modes3.queries.ExtraInputOfTurnout +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" + + val Type segmentType + val Type turnoutType + val Relation connectedToRelation + val Relation straightRelation + val Relation divergentRelation + + new(extension Ecore2Logic ecore2Logic, Ecore2Logic_Trace ecore2LogicTrace) { + extension val Modes3Package = Modes3Package.eINSTANCE + segmentType = ecore2LogicTrace.TypeofEClass(segment) + turnoutType = ecore2LogicTrace.TypeofEClass(turnout) + connectedToRelation = ecore2LogicTrace.relationOfReference(segment_ConnectedTo) + straightRelation = ecore2LogicTrace.relationOfReference(turnout_Straight) + divergentRelation = ecore2LogicTrace.relationOfReference(turnout_Divergent) + } + + override getMustPatterns() { + emptyMap + } + + override getMustNotPatterns() { + #{ + connectedToRelation -> MUST_NOT_CONNECTED_TO, + straightRelation -> MUST_NOT_STRAIGHT, + divergentRelation -> MUST_NOT_DIVERGENT + } + } + + override getAdditionalPatterns(extension PatternGenerator generator, Map fqnToPQuery) { + val StringConcatenationClient parameters = ''' + problem: LogicProblem, interpretation: PartialInterpretation, + source: DefinedElement, target: DefinedElement + ''' + + val StringConcatenationClient commonParameterConstraints = ''' + find interpretation(problem, interpretation); + find mustExist(problem, interpretation, source); + find mustExist(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; + } or { + // tooManyInputsOfSegment unit propagation + «commonParameterConstraints» + «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; + } + + 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_TURNOUT_OUTPUT»(«parameters») { + // outputReflexive unit propagation + «commonParameterConstraints» + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "source")» + «typeIndexer.referInstanceOf(turnoutType, Modality.MUST, "target")» + 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; + } + + 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; + } + + 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; + } + ''' + } +} -- cgit v1.2.3-70-g09d2