From f019f3ec81976f8e05d0c7458aba2f29b18461d0 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 5 Mar 2019 13:37:02 -0500 Subject: Implement type scope handling --- .../ecse/dslreasoner/vampire/icse/EcoreTest.xtend | 6 +-- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 8 ++-- .../dslreasoner/vampire/icse/GeneralTest.xtend | 52 +++++++++++++++------- .../dslreasoner/vampire/icse/YakinduTest.xtend | 6 +-- .../dslreasoner/vampire/queries/FamPatterns.vql | 2 +- .../dslreasoner/vampire/test/MedicalSystem.xtend | 10 ++--- .../dslreasoner/vampire/test/VampireTest.xtend | 13 +++--- 7 files changed, 55 insertions(+), 42 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend index 54114189..18b3badd 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend @@ -6,6 +6,7 @@ import functionalarchitecture.FunctionalarchitecturePackage import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore @@ -22,9 +23,6 @@ import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.EReference import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns -import java.util.LinkedHashMap -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor class EcoreTest { def static void main(String[] args) { @@ -62,7 +60,7 @@ class EcoreTest { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL ] solution = reasoner.solve(logicProblem, vampireConfig, workspace) diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend index 9ae00f8d..95bfd87a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend @@ -1,8 +1,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse +import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.LinkedList +import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl @@ -21,12 +23,12 @@ class FAMTest { println("Input and output workspaces are created") val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") + val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi") val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) println("DSL loaded") - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) + GeneralTest.createAndSolveProblem(metamodel, new LinkedList, queries, workspace) } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 2c53d181..8a60f486 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -26,56 +26,74 @@ import org.eclipse.emf.ecore.EReference import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.eclipse.viatra.query.runtime.api.IQueryGroup +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel class GeneralTest { - def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List partialModel, ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { + def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List partialModel, + ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { val Ecore2Logic ecore2Logic = new Ecore2Logic val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic - - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) - var problem = instanceModel2Logic.transform(modelGenerationProblem,partialModel).output - problem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration).output - + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output + problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + workspace.writeModel(problem, "Fam.logicproblem") - + println("Problem created") - + var LogicResult solution var LogicReasoner reasoner + //* reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ - //add configuration things, in config file first - it.writeToFile = true + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + it.typeScopes.minNewElements = 5 ] + solution = reasoner.solve(problem, vampireConfig, workspace) - solution = reasoner.solve(problem, vampireConfig, workspace) + /*/ + reasoner = new AlloySolver + val alloyConfig = new AlloySolverConfiguration => [ + it.typeScopes.maxNewElements = 7 + it.typeScopes.minNewElements = 3 + it.solutionScope.numberOfRequiredSolution = 1 + it.typeScopes.maxNewIntegers = 0 + it.documentationLevel = DocumentationLevel::NORMAL + ] + solution = reasoner.solve(problem, alloyConfig, workspace) + //*/ + println("Problem solved") } - + def static loadMetamodel(EPackage pckg) { val List classes = pckg.getEClassifiers.filter(EClass).toList val List enums = pckg.getEClassifiers.filter(EEnum).toList val List literals = enums.map[getELiterals].flatten.toList val List references = classes.map[getEReferences].flatten.toList val List attributes = classes.map[getEAttributes].flatten.toList - return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) + return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) } def static loadPartialModel(ReasonerWorkspace inputs, String path) { Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); - inputs.readModel(EObject,path).eResource.contents + inputs.readModel(EObject, path).eResource.contents // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList } def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) { val patterns = i.specifications.toList - val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet val derivedFeatures = emptyMap - //NO DERIVED FEATURES + // NO DERIVED FEATURES // val derivedFeatures = new LinkedHashMap // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) @@ -86,4 +104,4 @@ class GeneralTest { ) return res } -} \ No newline at end of file +} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index e4f6f87a..eb3f4b14 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend @@ -1,11 +1,11 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.y import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage +import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns class YakinduTest { def static void main(String[] args) { @@ -23,11 +23,11 @@ class YakinduTest { val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") - val queries = GeneralTest.loadQueries(metamodel, +// val queries = GeneralTest.loadQueries(metamodel, FamPa println("DSL loaded") - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) +// GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql index 013d0419..60679874 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql @@ -1,4 +1,4 @@ -package hu.bme.mit.inf.dslreasoner.domains.fam +package ca.mcgill.ecse.dslreasoner.vampire.queries import epackage "http://www.inf.mit.bme.hu/viatrasolver/example/fam" diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend index 15f9e1fe..40cb70a7 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend @@ -1,19 +1,17 @@ package ca.mcgill.ecse.dslreasoner.vampire.test import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.Collections import org.eclipse.emf.common.util.URI import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl @@ -41,7 +39,7 @@ class MedicalSystem { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL ] solution = reasoner.solve(root, vampireConfig, workspace) diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend index 4fc81ad8..bbb14f1f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend @@ -1,23 +1,19 @@ package ca.mcgill.ecse.dslreasoner.vampire.test - import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.Collections -import org.eclipse.emf.common.util.URI import org.eclipse.emf.ecore.resource.Resource -import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import java.io.File class VampireTest { @@ -65,7 +61,8 @@ class VampireTest { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL + it.typeScopes.minNewElements = 4 ] solution = reasoner.solve(problem, vampireConfig, workspace) -- cgit v1.2.3-54-g00ecf