From 77f583cd433f3ed0fed3a1f240c0677e41cb4d31 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 11 Apr 2019 16:59:48 -0400 Subject: VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging --- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 97 +++++++++++++++-- .../dslreasoner/vampire/icse/FileSystemTest.xtend | 99 ++++++++++++++--- .../dslreasoner/vampire/icse/GeneralTest.xtend | 117 +++------------------ .../dslreasoner/vampire/icse/YakinduTest.xtend | 98 ++++++++++++++--- 4 files changed, 273 insertions(+), 138 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca') 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 ef2e0c2f..f66ad93c 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,36 +1,115 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import functionalarchitecture.Function +import functionalarchitecture.FunctionalInterface +import functionalarchitecture.FunctionalOutput 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.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.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.LinkedList -import org.eclipse.emf.ecore.EObject +import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl class FAMTest { def static void main(String[] args) { - //Workspace setup + val Ecore2Logic ecore2Logic = new Ecore2Logic + val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + + // Workspace setup val inputs = new FileSystemWorkspace('''initialModels/''', "") val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") workspace.initAndClear - - //Logicproblem writing setup + + // Logicproblem writing setup val reg = Resource.Factory.Registry.INSTANCE val map = reg.extensionToFactoryMap map.put("logicproblem", new XMIResourceFactoryImpl) - println("Input and output workspaces are created") + // Load DSL val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) println("DSL loaded") + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + var problem = modelGenerationProblem.output +// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output +// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + workspace.writeModel(problem, "Fam.logicproblem") + + println("Problem created") + + //Start Time + var startTime = System.currentTimeMillis + + var LogicReasoner reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope + val classMapMin = new HashMap + classMapMin.put(Function, 1) + classMapMin.put(FunctionalInterface, 2) + classMapMin.put(FunctionalOutput, 3) - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Maximum Scope + val classMapMax = new HashMap + classMapMax.put(Function, 5) + classMapMax.put(FunctionalInterface, 2) + classMapMax.put(FunctionalOutput, 4) + + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Define Config File + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + + it.typeScopes.minNewElements = 4 + it.typeScopes.maxNewElements = 5 + if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin + if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + var LogicResult 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) + //*/ + // ///////////////////////////////////////////////////// + + var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 + var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 + + println("Problem solved") + println("Time was: " + totalTimeMin + ":" + totalTimeSec) } - - + } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend index 363b9356..50639577 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend @@ -1,33 +1,108 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns +import ca.mcgill.ecse.dslreasoner.vampire.queries +import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +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.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl class FileSystemTest { def static void main(String[] args) { - //Workspace setup + val Ecore2Logic ecore2Logic = new Ecore2Logic + val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + + // Workspace setup val inputs = new FileSystemWorkspace('''initialModels/''', "") val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") workspace.initAndClear - - //Logicproblem writing setup + + // Logicproblem writing setup val reg = Resource.Factory.Registry.INSTANCE val map = reg.extensionToFactoryMap map.put("logicproblem", new XMIResourceFactoryImpl) println("Input and output workspaces are created") - val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") - val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) + val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE) + val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi") + //val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance) println("DSL loaded") - - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + var problem = modelGenerationProblem.output +// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output +// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + workspace.writeModel(problem, "Fam.logicproblem") + + println("Problem created") + + // Start Time + var startTime = System.currentTimeMillis + + var LogicReasoner reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope + val classMapMin = new HashMap +// classMapMin.put(Function, 1) +// classMapMin.put(FunctionalInterface, 2) +// classMapMin.put(FunctionalOutput, 3) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Maximum Scope + val classMapMax = new HashMap +// classMapMax.put(Function, 5) +// classMapMax.put(FunctionalInterface, 2) +// classMapMax.put(FunctionalOutput, 4) + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Define Config File + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + + it.typeScopes.minNewElements = 4 + it.typeScopes.maxNewElements = 5 + if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin + if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + var LogicResult 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) + //*/ + // ///////////////////////////////////////////////////// + var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 + var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 + + println("Problem solved") + println("Time was: " + totalTimeMin + ":" + totalTimeSec) } - - + } 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 949abe87..89375801 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 @@ -1,25 +1,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import functionalarchitecture.Function -import functionalarchitecture.FunctionalInterface -import functionalarchitecture.FunctionalOutput import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic -import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore -import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic -import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.HashMap import java.util.List +import java.util.Map import org.eclipse.emf.ecore.EAttribute import org.eclipse.emf.ecore.EClass import org.eclipse.emf.ecore.EEnum @@ -30,100 +19,18 @@ 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.dslreasoner.logic.model.builder.DocumentationLevel -class GeneralTest { - def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List partialModel, - ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { - val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE - 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 = modelGenerationProblem.output -// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output -// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output - workspace.writeModel(problem, "Fam.logicproblem") - - println("Problem created") - - var startTime = System.currentTimeMillis - - var LogicResult solution - var LogicReasoner reasoner - - // * - reasoner = new VampireSolver - - // Setting up scope - val typeMapMin = new HashMap - val typeMapMax = new HashMap - val list2MapMin = metamodel.classes.toMap[s|s.name] - val list2MapMax = metamodel.classes.toMap[s|s.name] - - // Minimum Scope - typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, - list2MapMin.get(Function.simpleName) - ), 1) - typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, - list2MapMin.get(FunctionalInterface.simpleName) - ), 2) - typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, - list2MapMin.get(FunctionalOutput.simpleName) - ), 3) - - // Maximum Scope - typeMapMax.put(ecore2Logic.TypeofEClass( - modelGenerationProblem.trace, - list2MapMax.get(Function.simpleName) - ), 5) - typeMapMax.put(ecore2Logic.TypeofEClass( - modelGenerationProblem.trace, - list2MapMax.get(FunctionalInterface.simpleName) - ), 2) - typeMapMax.put(ecore2Logic.TypeofEClass( - modelGenerationProblem.trace, - list2MapMax.get(FunctionalOutput.simpleName) - ), 4) - - // Configuration - val vampireConfig = new VampireSolverConfiguration => [ - // add configuration things, in config file first - it.documentationLevel = DocumentationLevel::FULL - it.typeScopes.minNewElements = 4 - it.typeScopes.maxNewElements = 25 - it.typeScopes.minNewElementsByType = typeMapMin - it.typeScopes.maxNewElementsByType = typeMapMax - it.contCycleLevel = 5 - it.uniquenessDuplicates = false - ] - 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) - //*/ - - - var totalTimeMin = (System.currentTimeMillis - startTime)/60000 - var totalTimeSec = ((System.currentTimeMillis - startTime)/1000)% 60 - - println("Problem solved") - println("Time was: " + totalTimeMin + ":" + totalTimeSec) - - - +class GeneralTest { + def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { + val typeMap = new HashMap + val listMap = metamodel.classes.toMap[s|s.name] + for (Class elem : classMap.keySet) { + typeMap.put(e2l.TypeofEClass( + trace, listMap.get(elem.simpleName) + ), classMap.get(elem)) + } + return typeMap } def static loadMetamodel(EPackage pckg) { 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 eb3f4b14..1fac968b 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,34 +1,108 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import functionalarchitecture.FunctionalarchitecturePackage +import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic +import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration +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.viatra2logic.Viatra2Logic +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.HashMap 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) { - //Workspace setup + val Ecore2Logic ecore2Logic = new Ecore2Logic + val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) + val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic + + // Workspace setup val inputs = new FileSystemWorkspace('''initialModels/''', "") val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") workspace.initAndClear - - //Logicproblem writing setup + + // Logicproblem writing setup val reg = Resource.Factory.Registry.INSTANCE val map = reg.extensionToFactoryMap map.put("logicproblem", new XMIResourceFactoryImpl) println("Input and output workspaces are created") - val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") + val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) + val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") // val queries = GeneralTest.loadQueries(metamodel, FamPa + val queries = null println("DSL loaded") - -// GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + var problem = modelGenerationProblem.output +// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output +// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + workspace.writeModel(problem, "Yakindu.logicproblem") + + println("Problem created") + + // Start Time + var startTime = System.currentTimeMillis + + var LogicReasoner reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope + val classMapMin = new HashMap +// classMapMin.put(Function, 1) +// classMapMin.put(FunctionalInterface, 2) +// classMapMin.put(FunctionalOutput, 3) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Maximum Scope + val classMapMax = new HashMap +// classMapMax.put(Function, 5) +// classMapMax.put(FunctionalInterface, 2) +// classMapMax.put(FunctionalOutput, 4) + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + + // Define Config File + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + + it.typeScopes.minNewElements = 20 + it.typeScopes.maxNewElements = 30 + if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin + if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + var LogicResult 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) + //*/ + // ///////////////////////////////////////////////////// + var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 + var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 + + println("Problem solved") + println("Time was: " + totalTimeMin + ":" + totalTimeSec) } - - + } -- cgit v1.2.3-54-g00ecf