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 --- .../modes3/run/.Modes3ModelGenerator.xtendbin | Bin 0 -> 14631 bytes .../run/.Modes3UnitPropagationGenerator.xtendbin | Bin 0 -> 9899 bytes .../xtend-gen/modes3/run/.gitignore | 2 + .../xtend-gen/modes3/run/Modes3ModelGenerator.java | 381 ++++++++++++++ .../modes3/run/Modes3UnitPropagationGenerator.java | 585 +++++++++++++++++++++ 5 files changed, 968 insertions(+) create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3ModelGenerator.xtendbin create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3UnitPropagationGenerator.xtendbin create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.gitignore create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3ModelGenerator.java create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3UnitPropagationGenerator.java (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3') diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3ModelGenerator.xtendbin b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3ModelGenerator.xtendbin new file mode 100644 index 00000000..4f542a67 Binary files /dev/null and b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3ModelGenerator.xtendbin differ diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3UnitPropagationGenerator.xtendbin b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3UnitPropagationGenerator.xtendbin new file mode 100644 index 00000000..28e763b9 Binary files /dev/null and b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.Modes3UnitPropagationGenerator.xtendbin differ diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.gitignore b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.gitignore new file mode 100644 index 00000000..53dcf60f --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/.gitignore @@ -0,0 +1,2 @@ +/.Modes3ModelGenerator.java._trace +/.Modes3UnitPropagationGenerator.java._trace diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3ModelGenerator.java b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3ModelGenerator.java new file mode 100644 index 00000000..c7364257 --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3ModelGenerator.java @@ -0,0 +1,381 @@ +package modes3.run; + +import com.google.common.base.Objects; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Iterables; +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.Ecore2Logic_Trace; +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.ecore2logic.ecore2logicannotations.InverseRelationAssertion; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +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.Viatra2LogicTrace; +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.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.PartialRelationInterpretation; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; +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.Collections; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.function.Consumer; +import java.util.function.Predicate; +import modes3.Modes3Factory; +import modes3.Modes3ModelRoot; +import modes3.Modes3Package; +import modes3.queries.Modes3Queries; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.EAttribute; +import org.eclipse.emf.ecore.EClass; +import org.eclipse.emf.ecore.EEnum; +import org.eclipse.emf.ecore.EEnumLiteral; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.EReference; +import org.eclipse.emf.ecore.EStructuralFeature; +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.IQuerySpecification; +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions; +import org.eclipse.viatra.query.runtime.localsearch.matcher.integration.LocalSearchEMFBackendFactory; +import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; +import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory; +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.ExclusiveRange; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@FinalFieldsConstructor +@SuppressWarnings("all") +public class Modes3ModelGenerator { + private enum MonitoringQuery { + closeTrains, + + misalignedTurnout; + } + + private final Modes3ModelGenerator.MonitoringQuery monitoringQuery; + + private final int modelSize; + + private final Ecore2Logic ecore2Logic = new Ecore2Logic(); + + private final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + + private final Viatra2Logic viatra2Logic = new Viatra2Logic(this.ecore2Logic); + + private final ViatraReasoner solver = new ViatraReasoner(); + + @Extension + private final LogicProblemBuilder _logicProblemBuilder = new LogicProblemBuilder(); + + public URI generate() { + try { + URI _xblockexpression = null; + { + final EcoreMetamodelDescriptor metamodel = Modes3ModelGenerator.createMetamodelDescriptor(); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput metamodelLogic = this.ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + final Type segment = this.ecore2Logic.TypeofEClass(metamodelLogic.getTrace(), Modes3Package.eINSTANCE.getSegment()); + final RelationDeclaration connectedTo = this.ecore2Logic.relationOfReference(metamodelLogic.getTrace(), + Modes3Package.eINSTANCE.getSegment_ConnectedTo()); + final RelationDeclaration connectedToIndicator = ((EReferenceMapper_RelationsOverTypes_Trace) metamodelLogic.getTrace().referenceMapperTrace).indicators.get( + Modes3Package.eINSTANCE.getSegment_ConnectedTo()); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("oppositeReference "); + String _name = connectedTo.getName(); + _builder.append(_name); + _builder.append(" "); + String _name_1 = connectedTo.getName(); + _builder.append(_name_1); + final Function1 _function = (VariableContext it) -> { + Iff _xblockexpression_1 = null; + { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("src"); + final Variable src = it.addVar(_builder_1, segment); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("trg"); + final Variable trg = it.addVar(_builder_2, segment); + SymbolicValue _call = this._logicProblemBuilder.call(connectedToIndicator, src, trg); + SymbolicValue _call_1 = this._logicProblemBuilder.call(connectedToIndicator, trg, src); + _xblockexpression_1 = this._logicProblemBuilder.operator_spaceship(_call, _call_1); + } + return _xblockexpression_1; + }; + final Assertion inverseAssertion = this._logicProblemBuilder.Assertion(_builder, + this._logicProblemBuilder.Forall(_function)); + EList _assertions = metamodelLogic.getOutput().getAssertions(); + _assertions.add(inverseAssertion); + InverseRelationAssertion _createInverseRelationAssertion = Ecore2logicannotationsFactory.eINSTANCE.createInverseRelationAssertion(); + final Procedure1 _function_1 = (InverseRelationAssertion it) -> { + it.setTarget(inverseAssertion); + it.setInverseA(connectedTo); + it.setInverseB(connectedTo); + }; + final InverseRelationAssertion inverseAnnotation = ObjectExtensions.operator_doubleArrow(_createInverseRelationAssertion, _function_1); + EList _annotations = metamodelLogic.getOutput().getAnnotations(); + _annotations.add(inverseAnnotation); + final List initialModel = Modes3ModelGenerator.loadInitialModel(); + final TracedOutput initialModelLogic = this.instanceModel2Logic.transform(metamodelLogic, initialModel); + final ViatraQuerySetDescriptor queries = this.loadQueries(); + Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); + final TracedOutput logic = this.viatra2Logic.transformQueries(queries, initialModelLogic, _viatra2LogicConfiguration); + ViatraReasonerConfiguration _viatraReasonerConfiguration = new ViatraReasonerConfiguration(); + final Procedure1 _function_2 = (ViatraReasonerConfiguration it) -> { + it.runtimeLimit = 3600; + final Procedure1 _function_3 = (TypeScopes it_1) -> { + it_1.minNewElements = this.modelSize; + it_1.maxNewElements = this.modelSize; + final Procedure1> _function_4 = (Map it_2) -> { + it_2.put(this.ecore2Logic.TypeofEClass(metamodelLogic.getTrace(), Modes3Package.eINSTANCE.getTurnout()), Integer.valueOf(1)); + }; + ObjectExtensions.>operator_doubleArrow( + it_1.minNewElementsByType, _function_4); + final Procedure1> _function_5 = (Map it_2) -> { + it_2.put(this.ecore2Logic.TypeofEClass(metamodelLogic.getTrace(), Modes3Package.eINSTANCE.getTrain()), Integer.valueOf(5)); + }; + ObjectExtensions.>operator_doubleArrow( + it_1.maxNewElementsByType, _function_5); + }; + ObjectExtensions.operator_doubleArrow( + it.typeScopes, _function_3); + it.solutionScope.numberOfRequiredSolutions = 1; + it.nameNewElements = false; + it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis; + it.stateCoderStrategy = StateCoderStrategy.Neighbourhood; + ScopePropagatorStrategy.Polyhedral _polyhedral = new ScopePropagatorStrategy.Polyhedral( + PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp); + it.scopePropagatorStrategy = _polyhedral; + it.debugConfiguration.partialInterpretatioVisualiser = null; + }; + final ViatraReasonerConfiguration config = ObjectExtensions.operator_doubleArrow(_viatraReasonerConfiguration, _function_2); + final FileSystemWorkspace workspace = new FileSystemWorkspace("output/", ""); + final LogicResult solution = this.solver.solve(logic.getOutput(), config, workspace); + URI _xifexpression = null; + if ((solution instanceof ModelResult)) { + InputOutput.println("Saving generated solutions"); + final EList representations = ((ModelResult)solution).getRepresentation(); + int _size = representations.size(); + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size, true); + for (final Integer representationIndex : _doubleDotLessThan) { + { + final Object representation = representations.get((representationIndex).intValue()); + final int representationNumber = ((representationIndex).intValue() + 1); + if ((representation instanceof PartialInterpretation)) { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("solution"); + _builder_1.append(representationNumber); + _builder_1.append(".partialinterpretation"); + workspace.writeModel(((EObject)representation), _builder_1.toString()); + final PartialInterpretation2Gml partialInterpretation2GML = new PartialInterpretation2Gml(); + final String gml = partialInterpretation2GML.transform(((PartialInterpretation)representation)); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("solution"); + _builder_2.append(representationNumber); + _builder_2.append(".gml"); + workspace.writeText(_builder_2.toString(), gml); + int _size_1 = ((PartialInterpretation)representation).getNewElements().size(); + boolean _lessThan = (_size_1 < 160); + if (_lessThan) { + if ((representation instanceof PartialInterpretation)) { + final Consumer _function_3 = (Type it) -> { + InputOutput.println(it.getName()); + }; + ((PartialInterpretation)representation).getProblem().getTypes().forEach(_function_3); + final Function1 _function_4 = (Type it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "Modes3ModelRoot class DefinedPart")); + }; + Type _findFirst = IterableExtensions.findFirst(((PartialInterpretation)representation).getProblem().getTypes(), _function_4); + final TypeDefinition rootType = ((TypeDefinition) _findFirst); + final Function1 _function_5 = (PartialComplexTypeInterpretation it) -> { + String _name_2 = it.getInterpretationOf().getName(); + return Boolean.valueOf(Objects.equal(_name_2, "Modes3ModelRoot class")); + }; + final PartialComplexTypeInterpretation rootIntepretation = IterableExtensions.findFirst(Iterables.filter(((PartialInterpretation)representation).getPartialtypeinterpratation(), + PartialComplexTypeInterpretation.class), _function_5); + rootIntepretation.getElements().removeAll(rootType.getElements()); + ((PartialInterpretation)representation).getProblem().getElements().removeAll(rootType.getElements()); + EList _partialrelationinterpretation = ((PartialInterpretation)representation).getPartialrelationinterpretation(); + for (final PartialRelationInterpretation relationInterpretation : _partialrelationinterpretation) { + final Predicate _function_6 = (RelationLink link) -> { + boolean _xifexpression_1 = false; + if ((link instanceof BinaryElementRelationLink)) { + _xifexpression_1 = (rootType.getElements().contains(((BinaryElementRelationLink)link).getParam1()) || rootType.getElements().contains(((BinaryElementRelationLink)link).getParam2())); + } else { + _xifexpression_1 = false; + } + return _xifexpression_1; + }; + relationInterpretation.getRelationlinks().removeIf(_function_6); + } + rootType.getElements().clear(); + } + final GraphvizVisualiser visualiser = new GraphvizVisualiser(); + final PartialInterpretationVisualisation visualisation = visualiser.visualiseConcretization(((PartialInterpretation)representation)); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("solution"); + _builder_3.append(representationNumber); + _builder_3.append(".png"); + visualisation.writeToFile(workspace, _builder_3.toString()); + } + } else { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("solution"); + _builder_4.append(representationNumber); + _builder_4.append(".txt"); + workspace.writeText(_builder_4.toString(), representation.toString()); + } + } + } + } else { + URI _xblockexpression_1 = null; + { + InputOutput.println("Failed to solver problem"); + final LogicProblem partial = logic.getOutput(); + _xblockexpression_1 = workspace.writeModel(partial, "solution.partialinterpretation"); + } + _xifexpression = _xblockexpression_1; + } + _xblockexpression = _xifexpression; + } + return _xblockexpression; + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } + } + + public static EcoreMetamodelDescriptor createMetamodelDescriptor() { + EcoreMetamodelDescriptor _xblockexpression = null; + { + final ImmutableList eClasses = ImmutableList.copyOf(Iterables.filter(Modes3Package.eINSTANCE.getEClassifiers(), EClass.class)); + Set _emptySet = CollectionLiterals.emptySet(); + List _emptyList = CollectionLiterals.emptyList(); + List _emptyList_1 = CollectionLiterals.emptyList(); + final Function1> _function = (EClass it) -> { + return it.getEReferences(); + }; + ImmutableList _copyOf = ImmutableList.copyOf(IterableExtensions.flatMap(eClasses, _function)); + List _emptyList_2 = CollectionLiterals.emptyList(); + _xblockexpression = new EcoreMetamodelDescriptor(eClasses, _emptySet, + false, _emptyList, _emptyList_1, _copyOf, _emptyList_2); + } + return _xblockexpression; + } + + public static List loadInitialModel() { + Modes3ModelRoot _createModes3ModelRoot = Modes3Factory.eINSTANCE.createModes3ModelRoot(); + return Collections.unmodifiableList(CollectionLiterals.newArrayList(_createModes3ModelRoot)); + } + + public ViatraQuerySetDescriptor loadQueries() { + ViatraQuerySetDescriptor _xblockexpression = null; + { + final ImmutableList.Builder> patternsBuilder = ImmutableList.>builder(); + patternsBuilder.addAll(Modes3Queries.instance().getSpecifications()); + final ImmutableList> patterns = patternsBuilder.build(); + final Function1, Boolean> _function = (IQuerySpecification pattern) -> { + final Function1 _function_1 = (PAnnotation it) -> { + String _name = it.getName(); + return Boolean.valueOf(Objects.equal(_name, "Constraint")); + }; + return Boolean.valueOf(IterableExtensions.exists(pattern.getAllAnnotations(), _function_1)); + }; + final ImmutableSet> validationPatterns = ImmutableSet.>copyOf(IterableExtensions.>filter(patterns, _function)); + Map, EStructuralFeature> _emptyMap = CollectionLiterals., EStructuralFeature>emptyMap(); + _xblockexpression = new ViatraQuerySetDescriptor(patterns, validationPatterns, _emptyMap); + } + return _xblockexpression; + } + + public static Object init() { + Object _xblockexpression = null; + { + EMFPatternLanguageStandaloneSetup.doSetup(); + ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE, + LocalSearchEMFBackendFactory.INSTANCE); + LogiclanguagePackage.eINSTANCE.getClass(); + LogicproblemPackage.eINSTANCE.getClass(); + PartialinterpretationPackage.eINSTANCE.getClass(); + Ecore2logicannotationsPackage.eINSTANCE.getClass(); + Viatra2LogicAnnotationsPackage.eINSTANCE.getClass(); + Map _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + _extensionToFactoryMap.put("ecore", _xMIResourceFactoryImpl); + Map _extensionToFactoryMap_1 = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl_1 = new XMIResourceFactoryImpl(); + _extensionToFactoryMap_1.put("logicproblem", _xMIResourceFactoryImpl_1); + Map _extensionToFactoryMap_2 = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl_2 = new XMIResourceFactoryImpl(); + _xblockexpression = _extensionToFactoryMap_2.put("partialinterpretation", _xMIResourceFactoryImpl_2); + } + return _xblockexpression; + } + + public static void main(final String[] args) { + int _length = args.length; + boolean _notEquals = (_length != 2); + if (_notEquals) { + System.err.println("Usage: "); + } + final Modes3ModelGenerator.MonitoringQuery monitoringQuery = Modes3ModelGenerator.MonitoringQuery.valueOf(args[0]); + final int modelSize = Integer.parseInt(args[1]); + Modes3ModelGenerator.init(); + final Modes3ModelGenerator generator = new Modes3ModelGenerator(monitoringQuery, modelSize); + generator.generate(); + } + + public Modes3ModelGenerator(final Modes3ModelGenerator.MonitoringQuery monitoringQuery, final int modelSize) { + super(); + this.monitoringQuery = monitoringQuery; + this.modelSize = modelSize; + } +} diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3UnitPropagationGenerator.java b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3UnitPropagationGenerator.java new file mode 100644 index 00000000..91adaaaa --- /dev/null +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/xtend-gen/modes3/run/Modes3UnitPropagationGenerator.java @@ -0,0 +1,585 @@ +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.Collections; +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; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Pair; + +@SuppressWarnings("all") +public class Modes3UnitPropagationGenerator implements UnitPropagationPatternGenerator { + private static final String MUST_NOT_CONNECTED_TO = "mustNotConnectedTo"; + + private static final String MUST_NOT_CONNECTED_TO_HELPER = "mustNotConnectedTo_helper"; + + private static final String MUST_NOT_TURNOUT_OUTPUT = "mustNotTurnoutOutput"; + + private static final String MUST_NOT_STRAIGHT = "mustNotStraight"; + + private static final String MUST_NOT_DIVERGENT = "mustNotDivergent"; + + private final Type segmentType; + + private final Type turnoutType; + + private final Relation connectedToRelation; + + private final Relation straightRelation; + + private final Relation divergentRelation; + + public Modes3UnitPropagationGenerator(@Extension final Ecore2Logic ecore2Logic, final Ecore2Logic_Trace ecore2LogicTrace) { + @Extension + final Modes3Package Modes3Package = modes3.Modes3Package.eINSTANCE; + this.segmentType = ecore2Logic.TypeofEClass(ecore2LogicTrace, Modes3Package.getSegment()); + this.turnoutType = ecore2Logic.TypeofEClass(ecore2LogicTrace, Modes3Package.getTurnout()); + this.connectedToRelation = ecore2Logic.relationOfReference(ecore2LogicTrace, Modes3Package.getSegment_ConnectedTo()); + this.straightRelation = ecore2Logic.relationOfReference(ecore2LogicTrace, Modes3Package.getTurnout_Straight()); + this.divergentRelation = ecore2Logic.relationOfReference(ecore2LogicTrace, Modes3Package.getTurnout_Divergent()); + } + + @Override + public Map getMustPatterns() { + return CollectionLiterals.emptyMap(); + } + + @Override + public Map getMustNotPatterns() { + Pair _mappedTo = Pair.of(this.connectedToRelation, Modes3UnitPropagationGenerator.MUST_NOT_CONNECTED_TO); + Pair _mappedTo_1 = Pair.of(this.straightRelation, Modes3UnitPropagationGenerator.MUST_NOT_STRAIGHT); + Pair _mappedTo_2 = Pair.of(this.divergentRelation, Modes3UnitPropagationGenerator.MUST_NOT_DIVERGENT); + return Collections.unmodifiableMap(CollectionLiterals.newHashMap(_mappedTo, _mappedTo_1, _mappedTo_2)); + } + + @Override + public StringConcatenationClient getAdditionalPatterns(@Extension final PatternGenerator generator, final Map fqnToPQuery) { + StringConcatenationClient _xblockexpression = null; + { + StringConcatenationClient _client = new StringConcatenationClient() { + @Override + protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) { + _builder.append("problem: LogicProblem, interpretation: PartialInterpretation,"); + _builder.newLine(); + _builder.append("source: DefinedElement, target: DefinedElement"); + _builder.newLine(); + } + }; + final StringConcatenationClient parameters = _client; + StringConcatenationClient _client_1 = new StringConcatenationClient() { + @Override + protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) { + _builder.append("find interpretation(problem, interpretation);"); + _builder.newLine(); + _builder.append("find mustExist(problem, interpretation, source);"); + _builder.newLine(); + _builder.append("find mustExist(problem, interpretation, target);"); + _builder.newLine(); + } + }; + final StringConcatenationClient commonParameterConstraints = _client_1; + StringConcatenationClient _client_2 = new StringConcatenationClient() { + @Override + protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) { + _builder.append("pattern "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_CONNECTED_TO_HELPER); + _builder.append("("); + _builder.append(parameters); + _builder.append(") {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("// connectedToReflexive unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "source"); + _builder.append(_referInstanceOf, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_1 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_1, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("source == target;"); + _builder.newLine(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// tooManyInputsOfSegment unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_2 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_2, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_3 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_3, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_4 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "input1"); + _builder.append(_referInstanceOf_4, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_5 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "input2"); + _builder.append(_referInstanceOf_5, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("neg "); + CharSequence _referInstanceOf_6 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MAY, "source"); + _builder.append(_referInstanceOf_6, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(Output.instance().getFullyQualifiedName()), new String[] { "input1", "source" }, Modality.MUST, true, false); + _builder.append(_referPattern, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_1 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(Output.instance().getFullyQualifiedName()), new String[] { "input2", "source" }, Modality.MUST, true, false); + _builder.append(_referPattern_1, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("input1 != input2;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("input1 != target;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("input2 != target;"); + _builder.newLine(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutConnectedToBothOutputs unit propagation 1"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_7 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_7, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_8 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_8, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_9 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "divergent"); + _builder.append(_referInstanceOf_9, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation = generator.referRelation(Modes3UnitPropagationGenerator.this.straightRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_1 = generator.referRelation(Modes3UnitPropagationGenerator.this.divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_1, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_2 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_2, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutConnectedToBothOutputs unit propagation 2"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_10 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_10, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_11 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_11, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_12 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "straight"); + _builder.append(_referInstanceOf_12, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_3 = generator.referRelation(Modes3UnitPropagationGenerator.this.straightRelation, "source", "straight", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_3, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_4 = generator.referRelation(Modes3UnitPropagationGenerator.this.divergentRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_4, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_5 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_5, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// tooManyExtraInputsOfTurnout unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_13 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_13, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_14 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_14, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_15 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "extraInput"); + _builder.append(_referInstanceOf_15, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_2 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(TurnoutOutput.instance().getFullyQualifiedName()), new String[] { "source", "target" }, Modality.MAY, false, false); + _builder.append(_referPattern_2, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_3 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance().getFullyQualifiedName()), new String[] { "source", "extraInput" }, Modality.MUST, true, false); + _builder.append(_referPattern_3, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("target != extraInput;"); + _builder.newLine(); + _builder.append("}"); + _builder.newLine(); + _builder.newLine(); + _builder.append("pattern "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_CONNECTED_TO); + _builder.append("("); + _builder.append(parameters); + _builder.append(") {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("find "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_CONNECTED_TO_HELPER, "\t"); + _builder.append("(problem, interpretation, source, target);"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("find "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_CONNECTED_TO_HELPER, "\t"); + _builder.append("(problem, interpretation, target, source);"); + _builder.newLineIfNotEmpty(); + _builder.append("}"); + _builder.newLine(); + _builder.newLine(); + _builder.append("pattern "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_TURNOUT_OUTPUT); + _builder.append("("); + _builder.append(parameters); + _builder.append(") {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("// outputReflexive unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_16 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_16, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_17 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_17, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("source == target;"); + _builder.newLine(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// tooManyInputsOfSegment unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_18 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_18, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_19 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_19, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_20 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "input1"); + _builder.append(_referInstanceOf_20, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_21 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "input2"); + _builder.append(_referInstanceOf_21, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("neg "); + CharSequence _referInstanceOf_22 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MAY, "target"); + _builder.append(_referInstanceOf_22, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_4 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(Output.instance().getFullyQualifiedName()), new String[] { "input1", "target" }, Modality.MUST, true, false); + _builder.append(_referPattern_4, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_5 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(Output.instance().getFullyQualifiedName()), new String[] { "input2", "target" }, Modality.MUST, true, false); + _builder.append(_referPattern_5, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("input1 != input2;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("input1 != source;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("input2 != source;"); + _builder.newLine(); + _builder.append("}"); + _builder.newLine(); + _builder.newLine(); + _builder.append("pattern "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_STRAIGHT); + _builder.append("("); + _builder.append(parameters); + _builder.append(") {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("find "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_TURNOUT_OUTPUT, "\t"); + _builder.append("(problem, interpretation, source, target);"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutOutputsAreSame unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_23 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_23, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_24 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_24, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_6 = generator.referRelation(Modes3UnitPropagationGenerator.this.divergentRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_6, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutConnectedToBothOutputs unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_25 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_25, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_26 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_26, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_27 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "divergent"); + _builder.append(_referInstanceOf_27, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_7 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_7, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_8 = generator.referRelation(Modes3UnitPropagationGenerator.this.divergentRelation, "source", "divergent", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_8, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_9 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "divergent", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_9, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// tooManyExtraInputsOfTurnout unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_28 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_28, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_29 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_29, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_30 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "extraInput"); + _builder.append(_referInstanceOf_30, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_31 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "potentialExtraInput"); + _builder.append(_referInstanceOf_31, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_6 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance().getFullyQualifiedName()), new String[] { "source", "extraInput" }, Modality.MUST, true, false); + _builder.append(_referPattern_6, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_10 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_10, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("neg "); + CharSequence _referRelation_11 = generator.referRelation(Modes3UnitPropagationGenerator.this.divergentRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery); + _builder.append(_referRelation_11, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("extraInput != potentialExtraInput;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("extraInput != target;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("potentialExtraInput != target;"); + _builder.newLine(); + _builder.append("}"); + _builder.newLine(); + _builder.newLine(); + _builder.append("pattern "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_DIVERGENT); + _builder.append("("); + _builder.append(parameters); + _builder.append(") {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("find "); + _builder.append(Modes3UnitPropagationGenerator.MUST_NOT_TURNOUT_OUTPUT, "\t"); + _builder.append("(problem, interpretation, source, target);"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutOutputsAreSame unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_32 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_32, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_33 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_33, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_12 = generator.referRelation(Modes3UnitPropagationGenerator.this.straightRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_12, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// turnoutConnectedToBothOutputs unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_34 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_34, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_35 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_35, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_36 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "straight"); + _builder.append(_referInstanceOf_36, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_13 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "target", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_13, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_14 = generator.referRelation(Modes3UnitPropagationGenerator.this.straightRelation, "source", "straight", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_14, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_15 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "straight", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_15, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("} or {"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("// tooManyExtraInputsOfTurnout unit propagation"); + _builder.newLine(); + _builder.append("\t"); + _builder.append(commonParameterConstraints, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_37 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.turnoutType, Modality.MUST, "source"); + _builder.append(_referInstanceOf_37, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_38 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "target"); + _builder.append(_referInstanceOf_38, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_39 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "extraInput"); + _builder.append(_referInstanceOf_39, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referInstanceOf_40 = generator.getTypeIndexer().referInstanceOf(Modes3UnitPropagationGenerator.this.segmentType, Modality.MUST, "potentialExtraInput"); + _builder.append(_referInstanceOf_40, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referPattern_7 = generator.getRelationDefinitionIndexer().referPattern(fqnToPQuery.get(ExtraInputOfTurnout.instance().getFullyQualifiedName()), new String[] { "source", "extraInput" }, Modality.MUST, true, false); + _builder.append(_referPattern_7, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + CharSequence _referRelation_16 = generator.referRelation(Modes3UnitPropagationGenerator.this.connectedToRelation, "source", "potentialExtraInput", Modality.MUST, fqnToPQuery); + _builder.append(_referRelation_16, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("neg "); + CharSequence _referRelation_17 = generator.referRelation(Modes3UnitPropagationGenerator.this.straightRelation, "source", "potentialExtraInput", Modality.MAY, fqnToPQuery); + _builder.append(_referRelation_17, "\t"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("extraInput != potentialExtraInput;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("extraInput != target;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("potentialExtraInput != target;"); + _builder.newLine(); + _builder.append("}"); + _builder.newLine(); + } + }; + _xblockexpression = _client_2; + } + return _xblockexpression; + } +} -- cgit v1.2.3-54-g00ecf