From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../viatrasolver/logic2viatra/Modality.java | 22 ++ .../ModelGenerationMethodProvider.xtend | 78 +++++++ .../MultiplicityGoalConstraintCalculator.xtend | 46 ++++ .../viatrasolver/logic2viatra/TypeAnalysis.xtend | 92 ++++++++ .../logic2viatra/patterns/ContainmentIndexer.xtend | 41 ++++ .../logic2viatra/patterns/GenericTypeIndexer.xtend | 194 ++++++++++++++++ .../patterns/GenericTypeRefinementGenerator.xtend | 102 +++++++++ .../logic2viatra/patterns/InvalidIndexer.xtend | 53 +++++ .../logic2viatra/patterns/PatternGenerator.xtend | 244 +++++++++++++++++++++ .../logic2viatra/patterns/PatternProvider.xtend | 96 ++++++++ .../patterns/RelationDeclarationIndexer.xtend | 154 +++++++++++++ .../patterns/RelationDefinitionIndexer.xtend | 185 ++++++++++++++++ .../patterns/RelationRefinementGenerator.xtend | 93 ++++++++ .../logic2viatra/patterns/RepairGenerator.xtend | 18 ++ .../logic2viatra/patterns/TypeIndexer.xtend | 16 ++ .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 97 ++++++++ .../patterns/TypeRefinementGenerator.xtend | 95 ++++++++ ...TypeRefinementWithPreliminaryTypeAnalysis.xtend | 105 +++++++++ .../logic2viatra/patterns/UnfinishedIndexer.xtend | 85 +++++++ .../rules/GoalConstraintProvider.xtend | 18 ++ .../rules/RefinementRuleProvider.xtend | 209 ++++++++++++++++++ .../viatrasolver/logic2viatra/util/ParseUtil.xtend | 89 ++++++++ 22 files changed, 2132 insertions(+) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeAnalysis.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/ContainmentIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/InvalidIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RepairGenerator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java new file mode 100644 index 00000000..d2132cea --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java @@ -0,0 +1,22 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra; + +public enum Modality { + MUST, MAY, CURRENT; + public boolean isMust() { + return this == MUST; + } + public boolean isMay() { + return this == MAY; + } + public boolean isCurrent() { + return this == CURRENT; + } + public boolean isMustOrCurrent() { + return isMust() || isCurrent(); + } + public Modality getDual() { + if(this.isCurrent()) return CURRENT; + else if(this.isMust())return MAY; + else return MUST; + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend new file mode 100644 index 00000000..1653226d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend @@ -0,0 +1,78 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +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.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Collection +import java.util.LinkedHashMap +import java.util.List +import org.eclipse.viatra.query.runtime.api.GenericPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.viatra.query.runtime.api.IPatternMatch + +class ModelGenerationStatistics { + public var long transformationExecutionTime = 0 + synchronized def addExecutionTime(long amount) { + transformationExecutionTime+=amount + } + public var long PreliminaryTypeAnalisisTime = 0 +} +@Data class ModelGenerationMethod { + ModelGenerationStatistics statistics + + Collection> objectRefinementRules + Collection> relationRefinementRules + + List unfinishedMultiplicities + Collection>> unfinishedWF + + Collection>> invalidWF +} +enum TypeInferenceMethod { + Generic, PreliminaryAnalysis +} + +class ModelGenerationMethodProvider { + private val PatternProvider patternProvider = new PatternProvider + private val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider + private val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider + + public def ModelGenerationMethod createModelGenerationMethod( + LogicProblem logicProblem, + PartialInterpretation emptySolution, + Iterable existingQueries, + ReasonerWorkspace workspace, + boolean nameNewElements, + TypeInferenceMethod typeInferenceMethod + ) { + val statistics = new ModelGenerationStatistics + val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod) + + val //LinkedHashMap, BatchTransformationRule>> + objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries,nameNewElements,statistics) + val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) + + val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) + val unfinishedWF = queries.getUnfinishedWFQueries.values + + val invalidWF = queries.getInvalidWFQueries.values + + return new ModelGenerationMethod( + statistics, + objectRefinementRules.values, + relationRefinementRules.values, + unfinishedMultiplicities, + unfinishedWF, + invalidWF + ) + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend new file mode 100644 index 00000000..e05160d0 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend @@ -0,0 +1,46 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +import org.eclipse.emf.common.notify.Notifier +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope + +class MultiplicityGoalConstraintCalculator { + val String targetRelationName; + val IQuerySpecification querySpecification; + var ViatraQueryMatcher matcher; + + public new(String targetRelationName, IQuerySpecification querySpecification) { + this.targetRelationName = targetRelationName + this.querySpecification = querySpecification + this.matcher = null + } + + public new(MultiplicityGoalConstraintCalculator other) { + this.targetRelationName = other.targetRelationName + this.querySpecification = other.querySpecification + this.matcher = null + } + + def public getName() { + targetRelationName + } + + def public init(Notifier notifier) { + val engine = ViatraQueryEngine.on(new EMFScope(notifier)) + matcher = querySpecification.getMatcher(engine) + } + + def public calculateValue() { + var res = 0 + val allMatches = this.matcher.allMatches + for(match : allMatches) { + //println(targetRelationName+ " missing multiplicity: "+match.get(3)) + val missingMultiplicity = match.get(4) as Integer + res += missingMultiplicity + } + //println(targetRelationName+ " all missing multiplicities: "+res) + return res + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeAnalysis.xtend new file mode 100644 index 00000000..395aba85 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeAnalysis.xtend @@ -0,0 +1,92 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra + +import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.List +import java.util.Map +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.emf.EMFScope +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.NewElementTypeConstructorMatcher +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.NewElementTypeRefinementTargetMatcher +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.NewElementTypeRefinementNegativeConstraintMatcher +import java.util.ArrayList +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.DontHaveDefinedSupertypeMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries.NewElementMayTypeNegativeConstraintMatcher + +@Data class TypeRefinementPrecondition { + Type targetType + List inhibitorTypes +} + +/** + * Collection of all possible element creation and type refinement rules for defined and undefined elements. + */ +@Data class TypeAnalysisResult { + ///////////////// + // New elements + ///////////////// + /** + * New elements can be created using with the following types. + */ + List possibleNewDynamicTypes + /** + * (A,B) in possibleNewTypeRefinements: a new element x can be refined to A <=> x has all types listed in B. + */ + List possibleNewTypeRefinements + /** + * A new element may have type A if it already has types + */ + Map mayNewTypePreconditions + + ///////////////// + // Old elements + ///////////////// + + /** + * (A,B) in possibleNewTypeRefinements: a new element x can be refined to A <=> x has all types listed in B. + */ + Map possibleOldTypeRefinements + /** + * A new element may have type A if it already has types + */ + Map> mayOldTypePreconditions +} + +class TypeAnalysis { + + def TypeAnalysisResult performTypeAnalysis(LogicProblem problem, PartialInterpretation interpretation) { + val viatraEngine = ViatraQueryEngine.on(new EMFScope(problem)) + val negativeMatcher = NewElementTypeRefinementNegativeConstraintMatcher.on(viatraEngine) + + val possibleNewDynamicTypes = NewElementTypeConstructorMatcher.on(viatraEngine).allValuesOftype + + val possibleNewTypeRefinementTargets = NewElementTypeRefinementTargetMatcher.on(viatraEngine).allValuesOfrefined + val possibleNewTypeRefinements = new ArrayList + for(possibleNewTypeRefinementTarget : possibleNewTypeRefinementTargets) { + val inhibitorTypes = negativeMatcher.getAllValuesOfinhibitor(possibleNewTypeRefinementTarget) + possibleNewTypeRefinements += new TypeRefinementPrecondition( + possibleNewTypeRefinementTarget, + inhibitorTypes.toList) + } + + val possibleTypes = DontHaveDefinedSupertypeMatcher.on(viatraEngine).allValuesOftype + val newElementMayTypeMatcher = NewElementMayTypeNegativeConstraintMatcher.on(viatraEngine) + + val mayNewTypePreconditions = possibleTypes.toInvertedMap[type | + val inhibitorTypes = newElementMayTypeMatcher.getAllValuesOfinhibitor(type as TypeDeclaration) + return new TypeRefinementPrecondition(type,inhibitorTypes.toList) + ] + + return new TypeAnalysisResult( + possibleNewDynamicTypes.toList, + possibleNewTypeRefinements, + mayNewTypePreconditions, + emptyMap, + emptyMap + ) + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/ContainmentIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/ContainmentIndexer.xtend new file mode 100644 index 00000000..02e58c9b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/ContainmentIndexer.xtend @@ -0,0 +1,41 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import java.util.Collection +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import java.util.Map +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality + +class ContainmentIndexer { + val PatternGenerator base; + + new(PatternGenerator base) { + this.base = base + } + + def isContainmentRelation(Relation relation, LogicProblem problem) { + problem.containmentHierarchies.exists[it.containmentRelations.contains(relation)] + } + + def transformContainment(LogicProblem problem, Collection relations,Map fqn2PQuery) + ''' + private pattern mustContains2(source: DefinedElement, target: DefinedElement) { + find mustContains4(_,_,source,target); + } + + private pattern mustContains4(problem:LogicProblem, interpretation:PartialInterpretation, + source: DefinedElement, target: DefinedElement) + «FOR reference : relations.filter[isContainmentRelation(problem)] SEPARATOR 'or\n'» + { «base.referRelation(reference,"source","target",Modality.MUST,fqn2PQuery)» } + «ENDFOR» + + private pattern mustTransitiveContains(source,target) { + find mustContains2+(source,target); + } + ''' + def referMustContaint(String source, String target) + '''find mustContains4(problem,interpretation,«source»,«target»);''' + def referTransitiveMustContains(String source, String target) + '''find mustTransitiveContains(source,target);''' +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend new file mode 100644 index 00000000..fbbd9fb5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend @@ -0,0 +1,194 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import org.eclipse.emf.ecore.EClass +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult + +class GenericTypeIndexer implements TypeIndexer { + val PatternGenerator base; + + new(PatternGenerator base) { + this.base = base + } + override requiresTypeAnalysis() { false } + + public override getRequiredQueries() ''' + private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) { + PartialInterpretation.newElements(interpretation,element); + } + + private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { + find interpretation(problem,interpetation); + LogicProblem.types(problem,type); + PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); + PartialTypeInterpratation.interpretationOf(typeInterpretation,type); + } + + private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { + find interpretation(problem,interpetation); + find mustExist(problem,interpetation,element); + LogicProblem.types(problem,type); + TypeDefinition.elements(type,element); + } or { + find mustExist(problem,interpetation,element); + find typeInterpretation(problem,interpetation,type,typeInterpretation); + PartialTypeInterpratation.elements(typeInterpretation,element); + } + + /** + * Direct supertypes of a type. + */ + private pattern supertypeDirect(subtype : Type, supertype : Type) { + Type.supertypes(subtype, supertype); + } + + /** + * All supertypes of a type. + */ + private pattern supertypeStar(subtype: Type, supertype: Type) { + subtype == supertype; + } or { + find supertypeDirect+(subtype,supertype); + } + + /// Complex type reasoning patterns /// + // + // In a valid type system, for each element e there is exactly one type T where + // 1: T(e) - but we dont know this for type declaration + // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. + // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: + // D(e) && D-->T && !T(e) + // 3: There is no T' that T'->T and T'(e) + // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: + // D(e) && ![T--->D] && T(e) + // 4: T is not abstract + // Such type T is called Dynamic type of e, while other types are called static types. + // + // The following patterns checks the possible dynamic types for an element + + private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { + // 1: T(e) + find directInstanceOf(problem,interpretation,element,dynamic); + // 2e is not true: D(e) && D-->T && !T(e) + neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); + // 4: T is not abstract + Type.isAbstract(dynamic,false); + } + + private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) + // case 1: element is defined at least once + { + LogicProblem.types(problem,dynamic); + // select a random definition 'randomType' + find directInstanceOf(problem,interpretation,element,randomType); + // dynamic is a subtype of 'randomType' + find supertypeStar(dynamic,randomType); + // 2e is not true: D(e) && D-->T && !T(e) + neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); + // 4: T is not abstract + Type.isAbstract(dynamic,false); + } or + // case 2: element is not defined anywhere + { + find mayExist(problem,interpretation,element); + // there is no definition + neg find directInstanceOf(problem,interpretation,element,_); + // 2e is not true: D(e) && D-->T && !T(e) + // because non of the definition contains element, the type cannot have defined supertype + LogicProblem.types(problem,dynamic); + PartialInterpretation.problem(interpretation,problem); + neg find typeWithDefinedSupertype(dynamic); + // 3e is not true: D(e) && ![T--->D] && T(e) + // because there is no definition, dynamic covers all definition + // 4: T is not abstract + Type.isAbstract(dynamic,false); + } + + /** + * supertype -------> element <------- otherSupertype + * A A + * | | + * wrongDynamic -----------------------------X + */ + private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { + find directInstanceOf(problem,interpretation,element,supertype); + find directInstanceOf(problem,interpretation,element,otherSupertype); + find supertypeStar(wrongDynamic,supertype); + neg find supertypeStar(wrongDynamic,otherSupertype); + } + + /** + * supertype -------> element <---X--- otherSupertype + * A A + * | | + * wrongDynamic -----------------------------+ + */ + private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { + find directInstanceOf(problem,interpretation,element,supertype); + neg find elementInTypeDefinition(element,otherSupertype); + TypeDefinition(otherSupertype); + find supertypeStar(wrongDynamic, supertype); + find supertypeStar(wrongDynamic, otherSupertype); + } + + private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { + TypeDefinition.elements(definition,element); + } + + private pattern typeWithDefinedSupertype(type:Type) { + find supertypeStar(type,definedSupertype); + TypeDefinition(definedSupertype); + } + ''' + + public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { + ''' + «FOR type:problem.types» + «problem.generateMustInstenceOf(type)» + «problem.generateMayInstanceOf(type)» + «ENDFOR» + ''' + } + + private def patternName(Type type, Modality modality) + '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' + + private def generateMustInstenceOf(LogicProblem problem, Type type) { + ''' + /** + * An element must be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + Type.name(type,"«type.name»"); + find directInstanceOf(problem,interpretation,element,type); + } + ''' + } + + private def generateMayInstanceOf(LogicProblem problem, Type type) { + ''' + /** + * An element may be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + Type.name(type,"«type.name»"); + find possibleDynamicType(problem,interpretation,dynamic,element); + find supertypeStar(dynamic,type); + } + ''' + } + + public override referInstanceOf(Type type, Modality modality, String variableName) { + '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' + } + public override referInstanceOf(EClass type, Modality modality, String variableName) { + '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''class «type.name»''')»(problem,interpretation,«variableName»);''' + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend new file mode 100644 index 00000000..4b7af959 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend @@ -0,0 +1,102 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.HashMap + +class GenericTypeRefinementGenerator extends TypeRefinementGenerator { + public new(PatternGenerator base) { + super(base) + } + override requiresTypeAnalysis() { false } + + override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val containment = p.containmentHierarchies.head + val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] + val inverseRelations = new HashMap + p.annotations.filter(InverseRelationAssertion).forEach[ + inverseRelations.put(it.inverseA,it.inverseB) + inverseRelations.put(it.inverseB,it.inverseA) + ] + return ''' + «FOR type:newObjectTypes» + «IF(containment.typesOrderedInHierarchy.contains(type))» + «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» + «IF inverseRelations.containsKey(containmentRelation)» + pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialTypeInterpratation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); + PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ELSE» + pattern «this.patternName(containmentRelation,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» + «ELSE» + pattern createObject_«this.patternName(null,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + typeInterpretation:PartialTypeInterpratation) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(type,"«type.name»"); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + find mayExist(problem, interpretation, newObject); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» + ''' + } + + override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + return ''' + «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» + pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { + find interpretation(problem,interpretation); + find mustExist(problem, interpretation, object); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» + neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» + } + «ENDFOR» + ''' + } + + override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/InvalidIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/InvalidIndexer.xtend new file mode 100644 index 00000000..d9ede2a8 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/InvalidIndexer.xtend @@ -0,0 +1,53 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.lookup +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import java.util.LinkedHashMap +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality + +class InvalidIndexer { + val PatternGenerator patternGenerator + + public new(PatternGenerator patternGenerator) { + this.patternGenerator = patternGenerator + } + + public def getWFQueryName(RelationDefinition query) '''invalidWFQuery_«patternGenerator.canonizeName(query.name)»''' + + public def generateInvalidatedByWfQueries(LogicProblem problem, Map fqn2PQuery) { + val wfQueries = problem.assertions.map[it.annotations] + .flatten + .filter(TransformedViatraWellformednessConstraint) + .map[it.query] + ''' + «FOR wfQuery: wfQueries» + pattern invalidatedBy_«patternGenerator.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, + «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») + { + «patternGenerator.relationDefinitionIndexer.referPattern( + wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), + wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], + Modality.MUST, + true,false)» + } + «ENDFOR» + ''' + } + + public def getInvalidateByWfQueryNames(LogicProblem problem) { + val wfQueries = problem.assertions.map[it.annotations] + .flatten + .filter(TransformedViatraWellformednessConstraint) + .map[it.query] + val map = new LinkedHashMap + for(wfQuery : wfQueries) { + map.put(wfQuery.target, '''invalidatedBy_«patternGenerator.canonizeName(wfQuery.target.name)»''') + } + return map + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend new file mode 100644 index 00000000..291b605b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -0,0 +1,244 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import java.util.Map +import org.eclipse.emf.ecore.EReference +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.xtend.lib.annotations.Accessors +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import org.eclipse.emf.ecore.EAttribute +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint +import java.util.HashMap +import java.util.HashSet +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.DefinedByDerivedFeature + +class PatternGenerator { + @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) + @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this) + @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this) + @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) + @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) + @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this) + @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) + @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) + + public new(TypeInferenceMethod typeInferenceMethod) { + if(typeInferenceMethod == TypeInferenceMethod.Generic) { + this.typeIndexer = new GenericTypeIndexer(this) + this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) + } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { + this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) + this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) + } else { + this.typeIndexer = null + this.typeRefinementGenerator = null + throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') + } + } + + public def requiresTypeAnalysis() { + typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis + } + + public dispatch def referRelation( + RelationDeclaration referred, + String sourceVariable, + String targetVariable, + Modality modality, + Map fqn2PQuery) + { + return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) + } + public dispatch def referRelation( + RelationDefinition referred, + String sourceVariable, + String targetVariable, + Modality modality, + Map fqn2PQuery) + { + val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) + return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false) + } + + def public referRelationByName(EReference reference, + String sourceVariable, + String targetVariable, + Modality modality) + { + '''find «modality.name.toLowerCase»InRelation«canonizeName('''inreference «reference.name» «reference.EContainingClass.name»''') + »(problem,interpretation,«sourceVariable»,«targetVariable»);''' + } + + def public CharSequence referAttributeByName(EAttribute attribute, + String sourceVariable, + String targetVariable, + Modality modality) + { + throw new UnsupportedOperationException + } + + public def canonizeName(String name) { + name.split(' ').join('_') + } + + public def lowerMultiplicities(LogicProblem problem) { + problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived] + } + public def wfQueries(LogicProblem problem) { + problem.assertions.map[it.annotations] + .flatten + .filter(TransformedViatraWellformednessConstraint) + .map[it.query] + } + public def getContainments(LogicProblem p) { + return p.containmentHierarchies.head.containmentRelations + } + public def getInverseRelations(LogicProblem p) { + val inverseRelations = new HashMap + p.annotations.filter(InverseRelationAssertion).forEach[ + inverseRelations.put(it.inverseA,it.inverseB) + inverseRelations.put(it.inverseB,it.inverseA) + ] + return inverseRelations + } + public def isRepresentative(Relation relation, Relation inverse) { + if(inverse == null) { + return true + } else { + relation.name.compareTo(inverse.name)<1 + } + } + + public def isDerived(Relation relation) { + relation.annotations.exists[it instanceof DefinedByDerivedFeature] + } + public def getDerivedDefinition(RelationDeclaration relation) { + relation.annotations.filter(DefinedByDerivedFeature).head.query + } + + public def transformBaseProperties( + LogicProblem problem, + PartialInterpretation emptySolution, + Map fqn2PQuery, + TypeAnalysisResult typeAnalysisResult + ) { + + return ''' + import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" + import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" + import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" + + ////////// + // 0. Util + ////////// + private pattern interpretation(problem:LogicProblem, interpetation:PartialInterpretation) { + PartialInterpretation.problem(interpetation,problem); + } + + ///////////////////////// + // 0.1 Existance + ///////////////////////// + private pattern mustExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { + find interpretation(problem,interpetation); + LogicProblem.elements(problem,element); + } or { + find interpretation(problem,interpetation); + PartialInterpretation.newElements(interpetation,element); + } + + private pattern mayExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { + find mustExist(problem,interpetation,element); + } or { + find interpretation(problem,interpetation); + neg find closeWorld(interpetation); + PartialInterpretation.openWorldElementPrototype(interpetation,element); + } + + private pattern closeWorld(interpetation:PartialInterpretation) { + PartialInterpretation.maxNewElements(interpetation,0); + } + + //////////////////////// + // 0.2 Equivalence + //////////////////////// + pattern mayEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { + find mayExist(problem,interpretation,a); + find mayExist(problem,interpretation,b); + a == b; + } + + //////////////////////// + // 0.3 Required Patterns by TypeIndexer + //////////////////////// + «typeIndexer.requiredQueries» + + ////////// + // 1. Problem-Specific Base Indexers + ////////// + // 1.1 Type Indexers + ////////// + «typeIndexer.generateInstanceOfQueries(problem,emptySolution,typeAnalysisResult)» + + ////////// + // 1.2 Relation Declaration Indexers + ////////// + «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)» + + ////////// + // 1.3 Relation Definition Indexers + ////////// + «relationDefinitionIndexer.generateRelationDefinitions(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)» + + ////////// + // 1.4 Containment Indexer + ////////// + «containmentIndexer.transformContainment(problem,problem.relations,fqn2PQuery)» + + ////////// + // 2. Invalidation Indexers + ////////// + // 2.1 Invalidated by WF Queries + ////////// + «invalidIndexer.generateInvalidatedByWfQueries(problem,fqn2PQuery)» + + ////////// + // 3. Unfinishedness Indexers + ////////// + // 3.1 Unfinishedness Measured by Multiplicity + ////////// + «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)» + + ////////// + // 3.2 Unfinishedness Measured by WF Queries + ////////// + «unfinishedIndexer.generateUnfinishedWfQueries(problem,fqn2PQuery)» + + ////////// + // 4. Refinement Indexers + ////////// + // 4.1 Object constructors + ////////// + «typeRefinementGenerator.generateRefineObjectQueries(problem,emptySolution,typeAnalysisResult)» + + ////////// + // 4.2 Type refinement + ////////// + «typeRefinementGenerator.generateRefineTypeQueries(problem,emptySolution,typeAnalysisResult)» + + ////////// + // 4.3 Relation refinement + ////////// + «relationRefinementGenerator.generateRefineReference(problem)» + ''' + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend new file mode 100644 index 00000000..dac5630b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend @@ -0,0 +1,96 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.Map +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery +import org.eclipse.xtend.lib.annotations.Data + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +@Data class GeneratedPatterns { + public Map>> invalidWFQueries + public Map>> unfinishedWFQueries + public Map>> unfinishedMulticiplicityQueries + public Map>> refineObjectQueries + public Map>> refineTypeQueries + public Map, IQuerySpecification>> refinerelationQueries +} + +class PatternProvider { + val ParseUtil parseUtil = new ParseUtil + val TypeAnalysis typeAnalysis = new TypeAnalysis + + public def generateQueries( + LogicProblem problem, + PartialInterpretation emptySolution, + ModelGenerationStatistics statistics, + Iterable existingQueries, + ReasonerWorkspace workspace, + TypeInferenceMethod typeInferenceMethod + ) { + val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] + val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) + val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { + val startTime = System.nanoTime + val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) + val typeAnalysisTime = System.nanoTime - startTime + statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime + result + } else { + null + } + val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) + writeQueries(baseIndexerFile,"GeneratedQueries",workspace) + val generatedQueries = parseUtil.parse(baseIndexerFile) + val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); + return runtimeQueries + } + + private def writeQueries(CharSequence content, String name,ReasonerWorkspace workspace) { + if(workspace!=null) { + workspace.writeText('''«name».vql_deactivated''',content) + } + } + + private def GeneratedPatterns calclulateRuntimeQueries( + PatternGenerator patternGenerator, + LogicProblem problem, + PartialInterpretation emptySolution, + TypeAnalysisResult typeAnalysisResult, + Map>> queries + ) { + val Map>> + invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] + val Map>> + unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] + val Map>> + unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] + val Map>> + refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] + val Map>> + refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] + val Map, IQuerySpecification>> + refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] + return new GeneratedPatterns( + invalidWFQueries, + unfinishedWFQueries, + unfinishedMultiplicityQueries, + refineObjectsQueries, + refineTypeQueries, + refineRelationQueries + ) + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend new file mode 100644 index 00000000..e6d92cc6 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend @@ -0,0 +1,154 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import java.util.HashMap +import java.util.List +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class RelationDeclarationIndexer { + val PatternGenerator base; + + new(PatternGenerator base) { + this.base = base + } + + public def generateRelationIndexers(LogicProblem problem, Iterable relations, Map fqn2PQuery) { + val upperMultiplicities = new HashMap + problem.annotations.filter(UpperMultiplicityAssertion).forEach[ + upperMultiplicities.put(it.relation,it.upper) + ] + + return ''' + «FOR relation : relations» + «IF base.isDerived(relation)» + «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» + «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» + «ELSE» + «generateMustRelation(problem,relation)» + «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)» + «ENDIF» + «ENDFOR» + ''' + } + + def private patternName(RelationDeclaration r, Modality modality) { + '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' + } + + public def referRelation( + RelationDeclaration referred, + String sourceVariable, + String targetVariable, + Modality modality) + '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' + + def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' + /** + * Matcher for detecting tuples t where []«relation.name»(source,target) + */ + private pattern «relation.patternName(Modality.MUST)»( + problem:LogicProblem, interpretation:PartialInterpretation, + source: DefinedElement, target:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); + PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relation.name»"); + PartialRelationInterpretation.relationlinks(relationIterpretation,link); + BinaryElementRelationLink.param1(link,source); + BinaryElementRelationLink.param2(link,target); + } + ''' + def generateMayRelation(LogicProblem problem, RelationDeclaration relation, + Map upperMultiplicities, + List containments, + HashMap inverseRelations, + Map fqn2PQuery) + { + return ''' + /** + * Matcher for detecting tuples t where <>«relation.name»(source,target) + */ + private pattern «relation.patternName(Modality.MAY)»( + problem:LogicProblem, interpretation:PartialInterpretation, + source: DefinedElement, target:DefinedElement) + { + find interpretation(problem,interpretation); + // The two endpoint of the link have to exist + find mayExist(problem, interpretation, source); + find mayExist(problem, interpretation, target); + // Type consistency + «transformTypeConsistency(relation.parameters.get(0),"source")» + «transformTypeConsistency(relation.parameters.get(1),"target")» + «IF upperMultiplicities.containsKey(relation)» + // There are "numberOfExistingReferences" currently existing instances of the reference from the source, + // the upper bound of the multiplicity should be considered. + numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» + check(numberOfExistingReferences < «upperMultiplicities.get(relation)»); + «ENDIF» + «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» + // There are "numberOfExistingReferences" currently existing instances of the reference to the target, + // the upper bound of the opposite reference multiplicity should be considered. + numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» + check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»); + «ENDIF» + «IF containments.contains(relation)» + // The reference is containment, then a new reference cannot be create if: + // 1. Multiple parents + neg «base.containmentIndexer.referMustContaint("_","target")» + // 2. Circle in the containment hierarchy + neg «base.containmentIndexer.referTransitiveMustContains("target","source")» + «ENDIF» + «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» + // The eOpposite of the reference is containment, then a referene cannot be created if + // 1. Multiple parents + neg «base.containmentIndexer.referMustContaint("source","_")» + // 2. Circle in the containment hierarchy + neg «base.containmentIndexer.referTransitiveMustContains("source","target")» + «ENDIF» + } or { + «relation.referRelation("source","target",Modality.MUST)» + } + ''' + } + + def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' + /** + * Matcher for detecting tuples t where []«relation.name»(source,target) + */ + private pattern «relation.patternName(Modality.MUST)»( + problem:LogicProblem, interpretation:PartialInterpretation, + source: DefinedElement, target:DefinedElement) + { + «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» + } + ''' + def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' + /** + * Matcher for detecting tuples t where []«relation.name»(source,target) + */ + private pattern «relation.patternName(Modality.MAY)»( + problem:LogicProblem, interpretation:PartialInterpretation, + source: DefinedElement, target:DefinedElement) + { + «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» + } + ''' + + protected def CharSequence transformTypeConsistency(TypeReference reference, String name) { + if(reference instanceof ComplexTypeReference) { + this.base.typeIndexer.referInstanceOf(reference.referred,Modality.MAY,name) + } else { + return '''// Primitive type of «name» is already enforced''' + } + + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend new file mode 100644 index 00000000..7792eccb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend @@ -0,0 +1,185 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import java.util.Map +import org.eclipse.emf.ecore.EAttribute +import org.eclipse.emf.ecore.EReference +import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey +import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Inequality +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.BinaryTransitiveClosure +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.ConstantValue +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality + +class RelationDefinitionIndexer { + val PatternGenerator base; + + new(PatternGenerator base) { + this.base = base + } + + public def generateRelationDefinitions( + LogicProblem problem, + Iterable relations, + Map fqn2PQuery) { + val relation2PQuery = relations.toInvertedMap[ + annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) + ] + + return ''' + «FOR relation : relations» + // Must, May and Current queries for «relation.name» + «relation.transformPattern(relation.lookup(relation2PQuery), Modality.MUST)» + «relation.transformPattern(relation.lookup(relation2PQuery), Modality.MAY)» + «relation.transformPattern(relation.lookup(relation2PQuery), Modality.CURRENT)» + «ENDFOR» + ''' + } + + private def relationDefinitionName(RelationDefinition relation, Modality modality) + '''«modality.name.toLowerCase»InRelation_«base.canonizeName(relation.name)»''' + + private def canonizeName(PVariable v) { + return '''«IF v.referringConstraints.size == 1»_«ENDIF»var_«v.name.replaceAll("\\W","")»''' + } + + private def transformPattern(RelationDefinition relation, PQuery p, Modality modality) { + try { + return ''' + private pattern «relationDefinitionName(relation,modality)»( + problem:LogicProblem, interpretation:PartialInterpretation, + «FOR param : p.parameters SEPARATOR ', '»var_«param.name»«ENDFOR») + «FOR body : p.disjunctBodies.bodies SEPARATOR "or"»{ + find interpretation(problem,interpretation); + «FOR constraint : body.constraints» + «constraint.transformConstraint(modality)» + «ENDFOR» + }«ENDFOR» + ''' + } catch(UnsupportedOperationException e) { + throw new UnsupportedOperationException('''Can not transform pattern "«p.fullyQualifiedName»"!''',e) + } + } + + private def toMustMay(Modality modality) { + if(modality == Modality::MAY) return Modality::MAY + else return Modality::MUST + } + + def public referPattern(PQuery p, String[] variables, Modality modality, boolean positive, boolean transitive) ''' + «IF !positive»neg «ENDIF»find «modality.name.toLowerCase»InRelation_pattern_«p.fullyQualifiedName.replace('.','_')»«IF transitive»+«ENDIF»(problem,interpretation,«variables.join(',')»); + ''' + + private dispatch def transformConstraint(TypeConstraint constraint, Modality modality) { + val touple = constraint.variablesTuple + if(touple.size == 1) { + val inputKey = constraint.equivalentJudgement.inputKey + if(inputKey instanceof EClassTransitiveInstancesKey) { + return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay, + constraint.getVariableInTuple(0).canonizeName) + } else if(inputKey instanceof EDataTypeInSlotsKey){ + return '''// type constraint is enforced by construction''' + } + + } else if(touple.size == 2){ + val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey + if(key instanceof EReference) { + return base.referRelationByName( + key, + constraint.getVariableInTuple(0).canonizeName, + constraint.getVariableInTuple(1).canonizeName, + modality.toMustMay) + } else if (key instanceof EAttribute) { + return '''// attribute reference omitted'''//base.referRelationByName() + } else throw new UnsupportedOperationException('''unknown key: «key.class»''') + } else { + throw new UnsupportedOperationException() + } + } + + private dispatch def transformConstraint(Equality equality, Modality modality) { + val a = equality.who + val b = equality.withWhom + transformEquality(modality.toMustMay, a, b) + } + + private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { + if(modality.isMustOrCurrent) '''«a.canonizeName» == «b.canonizeName»;''' + else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } + + private dispatch def transformConstraint(Inequality inequality, Modality modality) { + val a = inequality.who + val b = inequality.withWhom + if(modality.isCurrent) { + return '''«a.canonizeName» != «b.canonizeName»;''' + } else if(modality.isMust) { + return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' + } else { + return '''«a.canonizeName» != «b.canonizeName»;''' + } + } + + private dispatch def transformConstraint(NegativePatternCall pcall, Modality modality) { + val params = (0..) { + targetString = '''const_«target.name»_«target.declaringClass.simpleName»''' + additionalDefinition = '''DefinedElement.name(«targetString»,"«target.name» «target.declaringClass.simpleName»"); LogicProblem.elements(problem,«targetString»);''' + } else if(target instanceof Integer) { + targetString = target.toString + additionalDefinition = '''''' + } else throw new UnsupportedOperationException('''Unknown constant type: «target.class»''') + + val source = c.variablesTuple + var String sourceName + if(source.size == 1) + sourceName = (source.get(0) as PVariable).canonizeName + else throw new UnsupportedOperationException("unknown source") + return '''«sourceName» == «targetString»;«additionalDefinition»'''; + } + + private dispatch def transformConstraint(PConstraint c, Modality modality) { + throw new UnsupportedOperationException('''Unknown constraint type: "«c.class.name»"!''') + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend new file mode 100644 index 00000000..7b175227 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend @@ -0,0 +1,93 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import java.util.LinkedList +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference + +class RelationRefinementGenerator { + PatternGenerator base; + public new(PatternGenerator base) { + this.base = base + } + + def CharSequence generateRefineReference(LogicProblem p) { + return ''' + «FOR relationRefinement: this.getRelationRefinements(p)» + pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», + from: DefinedElement, to: DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); + PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); + «IF relationRefinement.value != null» + PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); + PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); + «ENDIF» + find mustExist(problem, interpretation, from); + find mustExist(problem, interpretation, to); + «base.typeIndexer.referInstanceOf((relationRefinement.key.parameters.get(0) as ComplexTypeReference).referred, Modality::MUST,"from")» + «base.typeIndexer.referInstanceOf((relationRefinement.key.parameters.get(1) as ComplexTypeReference).referred, Modality::MUST,"to")» + «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» + neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» + } + «ENDFOR» + ''' + } + + def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { + '''«IF inverseRelation != null + »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»« + ELSE + »refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' + } + + def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, + String inverseInterpretationName, String sourceName, String targetName) + '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation != null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' + + def getRefineRelationQueries(LogicProblem p) { +// val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet +// p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] + /* + val res = new LinkedHashMap + for(relation: getRelationRefinements(p)) { + if(inverseRelations.containsKey(relation)) { + val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' + res.put(relation -> inverseRelations.get(relation),name) + } else { + val name = '''refineRelation_«base.canonizeName(relation.name)»''' + res.put(relation -> null,name) + } + } + return res*/ + + getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)] + } + + + def getRelationRefinements(LogicProblem p) { + val inverses = base.getInverseRelations(p) + val containments = base.getContainments(p) + val list = new LinkedList + for(relation : p.relations.filter(RelationDeclaration)) { + if(!containments.contains(relation)) { + if(inverses.containsKey(relation)) { + val inverse = inverses.get(relation) + if(!containments.contains(inverse)) { + if(base.isRepresentative(relation,inverse)) { + list += (relation -> inverse) + } + } + } else { + list += (relation -> null) + } + } + } + return list + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RepairGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RepairGenerator.xtend new file mode 100644 index 00000000..30fe5878 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RepairGenerator.xtend @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem + +class RepairGenerator { + val PatternGenerator base; + new(PatternGenerator base) { + this.base = base + } + + def generateRepairUnfinishedMultiplicityPatterns(LogicProblem problem) { + //val refinements = base.relationRefinementGenerator.getRelationRefinements(problem) + //val unfinisedLowerMultiplicities = base.get + } + def getRepairUnfinishedMultiplicityPatterns() { + + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend new file mode 100644 index 00000000..6c450664 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend @@ -0,0 +1,16 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import org.eclipse.emf.ecore.EClass +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult + +interface TypeIndexer { + public def CharSequence getRequiredQueries() + public def boolean requiresTypeAnalysis() + public def CharSequence generateInstanceOfQueries(LogicProblem problem,PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) + public def CharSequence referInstanceOf(Type type, Modality modality, String variableName) + public def CharSequence referInstanceOf(EClass type, Modality modality, String variableName) +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend new file mode 100644 index 00000000..3c49c323 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend @@ -0,0 +1,97 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import org.eclipse.emf.ecore.EClass +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition +import java.util.Collections + +class TypeIndexerWithPreliminaryTypeAnalysis implements TypeIndexer{ + val PatternGenerator base; + + new(PatternGenerator base) { + this.base = base + } + override requiresTypeAnalysis() { true } + + override getRequiredQueries() ''' + private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { + find interpretation(problem,interpetation); + LogicProblem.types(problem,type); + PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); + PartialTypeInterpratation.interpretationOf(typeInterpretation,type); + } + + private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { + find interpretation(problem,interpetation); + LogicProblem.types(problem,type); + TypeDefinition.elements(type,element); + } or { + find interpretation(problem,interpetation); + find typeInterpretation(problem,interpetation,type,typeInterpretation); + PartialTypeInterpratation.elements(typeInterpretation,element); + } + ''' + + override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val mayNewTypePreconditions = typeAnalysisResult.mayNewTypePreconditions + + return ''' + «FOR type:problem.types» + «problem.generateMustInstenceOf(type)» + «problem.generateMayInstanceOf(type,mayNewTypePreconditions.get(type))» + «ENDFOR» + ''' + } + + private def patternName(Type type, Modality modality) + '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' + + private def generateMustInstenceOf(LogicProblem problem, Type type) { + ''' + /** + * An element must be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { + Type.name(type,"«type.name»"); + find directInstanceOf(problem,interpretation,element,type); + } + ''' + } + + private def generateMayInstanceOf(LogicProblem problem, Type type, TypeRefinementPrecondition precondition) { + val inhibitorTypes = if(precondition!=null) { + precondition.inhibitorTypes + } else { + null + } + ''' + /** + * An element may be an instance of type "«type.name»". + */ + private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) + «IF inhibitorTypes != null»{ + find interpretation(problem,interpretation); + PartialInterpretation.newElements(interpretation,element); + «FOR inhibitorType : inhibitorTypes» + neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» + «ENDFOR» + } or { + find interpretation(problem,interpretation); + PartialInterpretation.openWorldElementPrototype(interpetation,element); + } or + «ENDIF» + { «referInstanceOf(type,Modality.MUST,"element")» } + ''' + } + + public override referInstanceOf(Type type, Modality modality, String variableName) { + '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' + } + public override referInstanceOf(EClass type, Modality modality, String variableName) { + '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''class «type.name»''')»(problem,interpretation,«variableName»);''' + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend new file mode 100644 index 00000000..a9ce9d73 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend @@ -0,0 +1,95 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +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.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.Map +import org.eclipse.xtend.lib.annotations.Data +import java.util.HashMap +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import java.util.LinkedHashMap +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy + +@Data +class ObjectCreationPrecondition { + Relation containmentRelation + Relation inverseContainment + Type newType +} + +abstract class TypeRefinementGenerator { + val protected PatternGenerator base; + public new(PatternGenerator base) { + this.base = base + } + + public def boolean requiresTypeAnalysis() + public def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) + public def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) + public def Map getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) + + public def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val Map objectCreationQueries = new LinkedHashMap + val containment = p.containmentHierarchies.head + val inverseRelations = new HashMap + p.annotations.filter(InverseRelationAssertion).forEach[ + inverseRelations.put(it.inverseA,it.inverseB) + inverseRelations.put(it.inverseB,it.inverseA) + ] + for(type: p.types.filter(TypeDeclaration).filter[!it.isAbstract]) { + if(containment.typeInContainment(type)) { + for(containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]) { + if(inverseRelations.containsKey(containmentRelation)) { + objectCreationQueries.put( + new ObjectCreationPrecondition(containmentRelation,inverseRelations.get(containmentRelation),type), + this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)) + } else { + objectCreationQueries.put( + new ObjectCreationPrecondition(containmentRelation,null,type), + patternName(containmentRelation,null,type)) + } + } + } else { + objectCreationQueries.put( + new ObjectCreationPrecondition(null,null,type), + this.patternName(null,null,type)) + } + } + return objectCreationQueries + } + + protected def canBeContainedByRelation(Relation r, Type t) { + if(r.parameters.size==2) { + val param = r.parameters.get(1) + if(param instanceof ComplexTypeReference) { + val allSuperTypes = t.transitiveClosureStar[it.supertypes] + for(superType : allSuperTypes) { + if(param.referred == superType) return true + } + } + } + return false + } + + private def typeInContainment(ContainmentHierarchy hierarchy, Type type) { + val allSuperTypes = type.transitiveClosureStar[it.supertypes] + return allSuperTypes.exists[hierarchy.typesOrderedInHierarchy.contains(it)] + } + + protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) { + if(containmentRelation != null) { + if(inverseContainment != null) { + '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»''' + } else { + '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»''' + } + } else { + '''createObject_«base.canonizeName(newType.name)»''' + } + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend new file mode 100644 index 00000000..be54d63c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend @@ -0,0 +1,105 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import java.util.HashMap + +class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ + public new(PatternGenerator base) { + super(base) + } + override requiresTypeAnalysis() { true } + + + override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val possibleNewDynamicType = typeAnalysisResult.possibleNewDynamicTypes + val containment = p.containmentHierarchies.head + val inverseRelations = new HashMap + p.annotations.filter(InverseRelationAssertion).forEach[ + inverseRelations.put(it.inverseA,it.inverseB) + inverseRelations.put(it.inverseB,it.inverseA) + ] + return ''' + «FOR type:possibleNewDynamicType» + «IF(containment.typesOrderedInHierarchy.contains(type))» + «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» + «IF inverseRelations.containsKey(containmentRelation)» + pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); + PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ELSE» + pattern «this.patternName(containmentRelation,null,type)»( + problem:LogicProblem, interpretation:PartialInterpretation, + relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialTypeInterpratation, + container:DefinedElement) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); + PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); + «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» + find mustExist(problem, interpretation, container); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» + «ELSE» + pattern createObject_«base.canonizeName(type.name)»( + problem:LogicProblem, interpretation:PartialInterpretation, + typeInterpretation:PartialTypeInterpratation) + { + find interpretation(problem,interpretation); + PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); + PartialTypeInterpratation.interpretationOf.name(type,"«type.name»"); + «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» + find mayExist(problem, interpretation, newObject); + neg find mustExist(problem, interpretation, newObject); + } + «ENDIF» + «ENDFOR» + ''' + } + + override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val newTypeRefinements = typeAnalysisResult.possibleNewTypeRefinements + return ''' + «FOR newTypeRefinement : newTypeRefinements» + pattern refineTypeTo_«base.canonizeName(newTypeRefinement.targetType.name)»(problem:LogicProblem, interpretation:PartialInterpretation, element: DefinedElement) { + find interpretation(problem,interpretation); + PartialInterpretation.newElements(interpretation,element); + «FOR inhibitorType : newTypeRefinement.inhibitorTypes» + neg «base.typeIndexer.referInstanceOf(inhibitorType,Modality.MUST,"element")» + «ENDFOR» + } + «ENDFOR» + ''' + } + + override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { + val newTypeRefinements = typeAnalysisResult.possibleNewTypeRefinements + newTypeRefinements.map[targetType].toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend new file mode 100644 index 00000000..ad1c9033 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend @@ -0,0 +1,85 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns + +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint +import java.util.Map +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import java.util.LinkedHashMap +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference + +class UnfinishedIndexer { + val PatternGenerator base + + new(PatternGenerator patternGenerator) { + this.base = patternGenerator + } + + def generateUnfinishedWfQueries(LogicProblem problem, Map fqn2PQuery) { + val wfQueries = base.wfQueries(problem) + ''' + «FOR wfQuery: wfQueries» + pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, + «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») + { + «base.relationDefinitionIndexer.referPattern( + wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), + wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], + Modality.CURRENT, + true,false)» + } + «ENDFOR» + ''' + } + def getUnfinishedWFQueryNames(LogicProblem problem) { + val wfQueries = base.wfQueries(problem) + val map = new LinkedHashMap + for(wfQuery : wfQueries) { + map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') + } + return map + } + def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map fqn2PQuery) { + val lowerMultiplicities = base.lowerMultiplicities(problem) + return ''' + «FOR lowerMultiplicity : lowerMultiplicities» + pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { + find interpretation(problem,interpretation); + PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); + PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); + «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» + numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» + check(numberOfExistingReferences < «lowerMultiplicity.lower»); + missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); + } + «ENDFOR» + ''' + } + def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) + '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' + + def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) + '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' + + def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { + val parameters = lowerMultiplicityAssertion.relation.parameters + if(parameters.size == 2) { + val firstParam = parameters.get(0) + if(firstParam instanceof ComplexTypeReference) { + return firstParam.referred + } + } + } + + def getUnfinishedMultiplicityQueries(LogicProblem problem) { + val lowerMultiplicities = base.lowerMultiplicities(problem) + val map = new LinkedHashMap + for(lowerMultiplicity : lowerMultiplicities) { + map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) + } + return map + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend new file mode 100644 index 00000000..e1be2742 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns +import java.util.ArrayList + +class GoalConstraintProvider { + def public getUnfinishedMultiplicityQueries(GeneratedPatterns patterns) { + val multiplicityQueries = patterns.unfinishedMulticiplicityQueries + val res = new ArrayList(multiplicityQueries.size) + for(multiplicityQuery : multiplicityQueries.entrySet) { + val targetRelationName = multiplicityQuery.key.name + val query = multiplicityQuery.value + res += new MultiplicityGoalConstraintCalculator(targetRelationName,query); + } + return res + } +} \ No newline at end of file diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend new file mode 100644 index 00000000..8b0f8f85 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -0,0 +1,209 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition +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.PartialTypeInterpratation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory +import java.util.LinkedHashMap +import org.eclipse.viatra.query.runtime.api.GenericPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule +import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory + +class RefinementRuleProvider { + private extension BatchTransformationRuleFactory factory = new BatchTransformationRuleFactory + private extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE + private extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE + + def canonizeName(String name) { + return name.replace(' ','_') + } + + def LinkedHashMap>> + createObjectRefinementRules( + GeneratedPatterns patterns, + boolean nameNewElement, + ModelGenerationStatistics statistics + ) + { + val res = new LinkedHashMap + for(LHSEntry: patterns.refineObjectQueries.entrySet) { + val containmentRelation = LHSEntry.key.containmentRelation + val inverseRelation = LHSEntry.key.inverseContainment + val type = LHSEntry.key.newType + val lhs = LHSEntry.value as IQuerySpecification> + val rule = createObjectCreationRule(containmentRelation,inverseRelation,type,lhs,nameNewElement,statistics) + res.put(LHSEntry.key,rule) + } + return res + } + + def private createObjectCreationRule( + Relation containmentRelation, + Relation inverseRelation, + Type type, + IQuerySpecification> lhs, + boolean nameNewElement, + ModelGenerationStatistics statistics) + { + val name = '''addObject_«type.name.canonizeName»« + IF containmentRelation!=null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' + val ruleBuilder = factory.createRule + .name(name) + .precondition(lhs) + if(containmentRelation != null) { + if(inverseRelation!= null) { + ruleBuilder.action[match | + //println(name) + val startTime = System.nanoTime + //val problem = match.get(0) as LogicProblem + val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation + val typeInterpretation = match.get(4) as PartialTypeInterpratation + val container = match.get(5) as DefinedElement + + val newElement = createDefinedElement + if(nameNewElement) { + newElement.name = '''new «interpretation.newElements.size»''' + } + + // Existence + interpretation.newElements+=newElement + interpretation.maxNewElements=interpretation.maxNewElements-1 + if(interpretation.minNewElements > 0) { + interpretation.minNewElements=interpretation.minNewElements-1 + } + + // Types + typeInterpretation.elements += newElement + typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] + // ContainmentRelation + val newLink1 = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] + relationInterpretation.relationlinks+=newLink1 + // Inverse Containment + val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] + inverseRelationInterpretation.relationlinks+=newLink2 + statistics.addExecutionTime(System.nanoTime-startTime) + ] + } else { + ruleBuilder.action[match | + //println(name) + val startTime = System.nanoTime + //val problem = match.get(0) as LogicProblem + val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val typeInterpretation = match.get(3) as PartialTypeInterpratation + val container = match.get(4) as DefinedElement + + val newElement = createDefinedElement + if(nameNewElement) { + newElement.name = '''new «interpretation.newElements.size»''' + } + + // Existence + interpretation.newElements+=newElement + interpretation.maxNewElements=interpretation.maxNewElements-1 + if(interpretation.minNewElements > 0) { + interpretation.minNewElements=interpretation.minNewElements-1 + } + + // Types + typeInterpretation.elements += newElement + typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] + // ContainmentRelation + val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] + relationInterpretation.relationlinks+=newLink + statistics.addExecutionTime(System.nanoTime-startTime) + ] + } + } else { + ruleBuilder.action[match | + //println(name) + val startTime = System.nanoTime + //val problem = match.get(0) as LogicProblem + val interpretation = match.get(1) as PartialInterpretation + val typeInterpretation = match.get(2) as PartialTypeInterpratation + + val newElement = createDefinedElement //=> [it.name = null] + if(nameNewElement) { + newElement.name = '''new «interpretation.newElements.size»''' + } + // Existence + interpretation.newElements+=newElement + interpretation.maxNewElements=interpretation.maxNewElements-1 + if(interpretation.minNewElements > 0) { + interpretation.minNewElements=interpretation.minNewElements-1 + } + // Types + typeInterpretation.elements += newElement + typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] + statistics.addExecutionTime(System.nanoTime-startTime) + ] + } + return ruleBuilder.build + } + + def createRelationRefinementRules(GeneratedPatterns patterns, ModelGenerationStatistics statistics) { + val res = new LinkedHashMap + for(LHSEntry: patterns.refinerelationQueries.entrySet) { + val declaration = LHSEntry.key.key + val inverseReference = LHSEntry.key.value + val lhs = LHSEntry.value as IQuerySpecification> + val rule = createRelationRefinementRule(declaration,inverseReference,lhs,statistics) + res.put(LHSEntry.key,rule) + } + return res + } + + def private BatchTransformationRule> + createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification> lhs, ModelGenerationStatistics statistics) + { + val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' + val ruleBuilder = factory.createRule + .name(name) + .precondition(lhs) + if (inverseRelation == null) { + ruleBuilder.action [ match | + val startTime = System.nanoTime + //println(name) + // val problem = match.get(0) as LogicProblem + // val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val src = match.get(3) as DefinedElement + val trg = match.get(4) as DefinedElement + val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] + relationInterpretation.relationlinks += link + statistics.addExecutionTime(System.nanoTime-startTime) + ] + } else { + ruleBuilder.action [ match | + val startTime = System.nanoTime + //println(name) + // val problem = match.get(0) as LogicProblem + // val interpretation = match.get(1) as PartialInterpretation + val relationInterpretation = match.get(2) as PartialRelationInterpretation + val inverseInterpretation = match.get(3) as PartialRelationInterpretation + val src = match.get(4) as DefinedElement + val trg = match.get(5) as DefinedElement + val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] + relationInterpretation.relationlinks += link + val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] + inverseInterpretation.relationlinks += inverseLink + statistics.addExecutionTime(System.nanoTime-startTime) + ] + } + + return ruleBuilder.build + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend new file mode 100644 index 00000000..005304ea --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend @@ -0,0 +1,89 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util + +import com.google.inject.Guice +import com.google.inject.Injector +import com.google.inject.Module +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage +import java.io.ByteArrayInputStream +import java.io.InputStream +import java.util.LinkedHashMap +import org.eclipse.emf.common.util.URI +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.viatra.query.patternlanguage.PatternLanguageStandaloneSetup +import org.eclipse.viatra.query.patternlanguage.annotations.ExtensionBasedAnnotationValidatorLoader +import org.eclipse.viatra.query.patternlanguage.annotations.IAnnotationValidatorLoader +import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageRuntimeModule +import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup +import org.eclipse.viatra.query.patternlanguage.emf.GenmodelExtensionLoader +import org.eclipse.viatra.query.patternlanguage.emf.IGenmodelMappingLoader +import org.eclipse.viatra.query.patternlanguage.emf.eMFPatternLanguage.PatternModel +import org.eclipse.viatra.query.patternlanguage.emf.specification.SpecificationBuilder +import org.eclipse.xtext.resource.XtextResourceSet + +class MyModule extends EMFPatternLanguageRuntimeModule implements Module{ + def public Class bindAnnotationValidatorLoader() { + return typeof(ExtensionBasedAnnotationValidatorLoader); + } + def public Class bindGenmodelMappingLoader() { + return typeof(GenmodelExtensionLoader); + } +} + +class ParseUtil { + val Injector injector; + new() { + PatternLanguageStandaloneSetup.doSetup + EMFPatternLanguageStandaloneSetup.doSetup; + PartialinterpretationPackage.eINSTANCE.class; + LogicproblemPackage.eINSTANCE.class; + LogiclanguagePackage.eINSTANCE.class; + + injector = internalCreateInjector//(new EMFPatternLanguageStandaloneSetup()).createInjectorAndDoEMFRegistration(); + } + + def protected Injector internalCreateInjector() { + var newInjector = new EMFPatternLanguageStandaloneSetup().createInjectorAndDoEMFRegistration(); + //XXX the following line enforce the tests to be run in an Eclipse environment + val Module module = new MyModule + newInjector = Guice.createInjector(module) + //ViatraQueryLoggingUtil.setExternalLogger(newInjector.getInstance(Logger.class)); + //EMFPatternLanguagePlugin.getInstance().addCompoundInjector(newInjector,EMFPatternLanguagePlugin.TEST_INJECTOR_PRIORITY); + return newInjector; + } + +// @Inject +// var ParseHelper parseHelper; + val builder = new SpecificationBuilder + + public def parse(CharSequence vqlFileContent) { + //val patternModel = this.parseHelper.parse(vqlFileContent) + val XtextResourceSet resourceSet = injector.getInstance(XtextResourceSet); + val Resource resource = resourceSet.createResource(URI.createURI("dummy:/example.vql")); + val InputStream in = new ByteArrayInputStream(vqlFileContent.toString.getBytes()); + resource.load(in, resourceSet.getLoadOptions()); + val patternModel = resource.getContents().get(0) as PatternModel; + + EcoreUtil.resolveAll(resource) + resource.validate + val res = new LinkedHashMap + for(pattern : patternModel.patterns) { + val querySpecification = builder.getOrCreateSpecification(pattern) + res.put(querySpecification.fullyQualifiedName,querySpecification) + //println('''«querySpecification.fullyQualifiedName» -> «querySpecification»''') + } + resource.validate + return res + } + + def private validate(Resource resource) { + val errors = resource.errors + if(!errors.isEmpty) { + println('''-- Errors --''') + errors.forEach[println('''> «it»''')] + println('''------------''') + } + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf