From 16970bfa029b11680df1179722bd9dfd5a4dcf95 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 13 Jun 2018 15:52:11 +0200 Subject: Support for updated partial model representation during generation --- .../logic2viatra/patterns/GenericTypeIndexer.xtend | 6 +- .../patterns/GenericTypeRefinementGenerator.xtend | 8 +- .../logic2viatra/patterns/PatternGenerator.xtend | 101 +++++++-------------- .../TypeIndexerWithPreliminaryTypeAnalysis.xtend | 8 +- ...TypeRefinementWithPreliminaryTypeAnalysis.xtend | 6 +- 5 files changed, 47 insertions(+), 82 deletions(-) (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns') 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 index a703ba4b..2dae95be 100644 --- 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 @@ -20,11 +20,11 @@ class GenericTypeIndexer extends TypeIndexer { PartialInterpretation.newElements(interpretation,element); } - private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { + private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpetation); LogicProblem.types(problem,type); PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); - PartialTypeInterpratation.interpretationOf(typeInterpretation,type); + PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); } private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { @@ -35,7 +35,7 @@ class GenericTypeIndexer extends TypeIndexer { } or { find mustExist(problem,interpetation,element); find typeInterpretation(problem,interpetation,type,typeInterpretation); - PartialTypeInterpratation.elements(typeInterpretation,element); + PartialComplexTypeInterpretation.elements(typeInterpretation,element); } /** 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 index c9e183ab..1aa3b955 100644 --- 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 @@ -42,7 +42,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); @@ -61,7 +61,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.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")» @@ -79,7 +79,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { find interpretation(problem,interpretation); neg find hasElementInContainment(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(type,"«type.name»"); + PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» find mayExist(problem, interpretation, newObject); neg find mustExist(problem, interpretation, newObject); @@ -91,7 +91,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» find mayExist(problem, interpretation, newObject); neg find mustExist(problem, interpretation, newObject); 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 index 34094cac..001ff13f 100644 --- 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 @@ -177,58 +177,23 @@ class PatternGenerator { find interpretation(problem,interpetation); PartialInterpretation.newElements(interpetation,element); } - «IF problem.hasBoolean»or { - find interpretation(problem,interpetation); - PartialInterpretation.booleanelements(interpetation,element); - }«ENDIF» - «IF problem.hasInteger»or { - find interpretation(problem,interpetation); - PartialInterpretation.integerelements(interpetation,element); - }«ENDIF» - «IF problem.hasReal»or { - find interpretation(problem,interpetation); - PartialInterpretation.realelements(interpetation,element); - }«ENDIF» - «IF problem.hasString»or { - find interpretation(problem,interpetation); - PartialInterpretation.stringelements(interpetation,element); - }«ENDIF» private pattern mayExist(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement) { find mustExist(problem,interpetation,element); } or { find interpretation(problem,interpetation); neg find elementCloseWorld(interpetation); - PartialInterpretation.openWorldElementPrototypes(interpetation,element); + PartialInterpretation.openWorldElements(interpetation,element); } - «IF problem.hasInteger»or { - find interpretation(problem,interpetation); - neg find integerCloseWorld(interpetation); - PartialInterpretation.newIntegers(interpetation,element); - }«ENDIF» - «IF problem.hasReal»or { - find interpretation(problem,interpetation); - neg find realCloseWorld(interpetation); - PartialInterpretation.newReals(interpetation,element); - }«ENDIF» - «IF problem.hasString»or { - find interpretation(problem,interpetation); - neg find stringCloseWorld(interpetation); - PartialInterpretation.newStrings(interpetation,element); - }«ENDIF» - private pattern elementCloseWorld(interpetation:PartialInterpretation) { - PartialInterpretation.maxNewElements(interpetation,0); + private pattern elementCloseWorld(element:DefinedElement) { + PartialInterpretation.newElements(i,element); + PartialInterpretation.maxNewElements(i,0); + } or { + Scope.targetTypeInterpretation(scope,interpetation); + PartialTypeInterpratation.elements(interpetation,element); + Scope.maxNewElements(scope,0); } - «IF problem.hasInteger»private pattern integerCloseWorld(interpetation:PartialInterpretation) { - PartialInterpretation.maxNewIntegers(interpetation,0); - }«ENDIF» - «IF problem.hasReal»private pattern realCloseWorld(interpetation:PartialInterpretation) { - PartialInterpretation.maxNewReals(interpetation,0); - }«ENDIF» - «IF problem.hasString»private pattern stringCloseWorld(interpetation:PartialInterpretation) { - PartialInterpretation.maxNewStrings(interpetation,0); - }«ENDIF» //////////////////////// // 0.2 Equivalence @@ -251,31 +216,31 @@ class PatternGenerator { ////////// // 1.1.1 primitive Type Indexers ////////// - pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - find interpretation(problem,interpretation); - PartialInterpretation.booleanelements(interpretation,element); - } - pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - find interpretation(problem,interpretation); - PartialInterpretation.integerelements(interpretation,element); - } or { - find interpretation(problem,interpretation); - PartialInterpretation.newIntegers(interpetation,element); - } - pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - find interpretation(problem,interpretation); - PartialInterpretation.realelements(interpretation,element); - } or { - find interpretation(problem,interpretation); - PartialInterpretation.newReals(interpetation,element); - } - pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { - find interpretation(problem,interpretation); - PartialInterpretation.stringelements(interpretation,element); - } or { - find interpretation(problem,interpretation); - PartialInterpretation.newStrings(interpetation,element); - } +««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.booleanelements(interpretation,element); +««« } +««« pattern instanceofInteger(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.integerelements(interpretation,element); +««« } or { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.newIntegers(interpetation,element); +««« } +««« pattern instanceofReal(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.realelements(interpretation,element); +««« } or { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.newReals(interpetation,element); +««« } +««« pattern instanceofString(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.stringelements(interpretation,element); +««« } or { +««« find interpretation(problem,interpretation); +««« PartialInterpretation.newStrings(interpetation,element); +««« } ////////// // 1.1.2 domain-specific Type Indexers 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 index fd0b7c18..7bdb9a5b 100644 --- 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 @@ -18,11 +18,11 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ override requiresTypeAnalysis() { true } override getRequiredQueries() ''' - private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { + private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { find interpretation(problem,interpetation); LogicProblem.types(problem,type); PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); - PartialTypeInterpratation.interpretationOf(typeInterpretation,type); + PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); } private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { @@ -32,7 +32,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ } or { find interpretation(problem,interpetation); find typeInterpretation(problem,interpetation,type,typeInterpretation); - PartialTypeInterpratation.elements(typeInterpretation,element); + PartialComplexTypeInterpretation.elements(typeInterpretation,element); } ''' @@ -81,7 +81,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ «ENDFOR» } or { find interpretation(problem,interpretation); - PartialInterpretation.openWorldElementPrototypes(interpetation,element); + PartialInterpretation.openWorldElements(interpetation,element); } or «ENDIF» { «referInstanceOf(type,Modality.MUST,"element")» } 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 index 8a6efeeb..7c5f507b 100644 --- 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 @@ -41,7 +41,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); @@ -60,7 +60,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ { find interpretation(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.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")» @@ -78,7 +78,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{ find interpretation(problem,interpretation); neg find hasElementInContainment(problem,interpretation); PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); - PartialTypeInterpratation.interpretationOf.name(typeInterpretation,"«type.name»"); + PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» find mayExist(problem, interpretation, newObject); neg find mustExist(problem, interpretation, newObject); -- cgit v1.2.3-70-g09d2