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 --- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6358 -> 6358 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 4068 -> 6825 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 4115 -> 6088 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 8623 -> 6456 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 4054 -> 6042 bytes .../ecse/dslreasoner/vampire/icse/FAMTest.java | 107 +++++++++++++++++---- .../dslreasoner/vampire/icse/FileSystemTest.java | 102 ++++++++++++++++---- .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 107 +++------------------ .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 99 ++++++++++++++++--- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 12 files changed, 266 insertions(+), 149 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 7f92eba4..55d90ac7 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin index 67bf34bd..8eeb2d28 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin index 093855d8..ab6aaf6e 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index 2df2ba62..cd75a66c 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin index 0c97e8d1..1b920064 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java index 7b4bb578..5fc2a391 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java @@ -2,37 +2,110 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 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.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.ecore2logic.Ecore2Logic_Trace; 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.builder.TracedOutput; +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.logic.model.logicresult.LogicResult; +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 java.util.HashMap; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class FAMTest { public static void main(final String[] args) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("initialModels/"); - final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FAMTest/"); - final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); - workspace.initAndClear(); - final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; - final Map map = reg.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - map.put("logicproblem", _xMIResourceFactoryImpl); - InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi"); - final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); - InputOutput.println("DSL loaded"); - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace); + try { + final Ecore2Logic ecore2Logic = new Ecore2Logic(); + final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); + final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/FAMTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi"); + final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); + InputOutput.println("DSL loaded"); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + workspace.writeModel(problem, "Fam.logicproblem"); + InputOutput.println("Problem created"); + long startTime = System.currentTimeMillis(); + LogicReasoner reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + classMapMin.put(Function.class, Integer.valueOf(1)); + classMapMin.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2)); + classMapMin.put(FunctionalOutput.class, Integer.valueOf(3)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(Function.class, Integer.valueOf(5)); + classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2)); + classMapMax.put(FunctionalOutput.class, Integer.valueOf(4)); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 4; + it.typeScopes.maxNewElements = 5; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } + int _size_1 = typeMapMin.size(); + boolean _notEquals_1 = (_size_1 != 0); + if (_notEquals_1) { + it.typeScopes.maxNewElementsByType = typeMapMax; + } + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); + long _currentTimeMillis = System.currentTimeMillis(); + long _minus = (_currentTimeMillis - startTime); + long totalTimeMin = (_minus / 60000); + long _currentTimeMillis_1 = System.currentTimeMillis(); + long _minus_1 = (_currentTimeMillis_1 - startTime); + long _divide = (_minus_1 / 1000); + long totalTimeSec = (_divide % 60); + InputOutput.println("Problem solved"); + InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java index 5994b4b4..eedec995 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java @@ -1,38 +1,100 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; +import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; -import functionalarchitecture.FunctionalarchitecturePackage; -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns; +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.ecore2logic.Ecore2Logic_Trace; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; +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.builder.TracedOutput; +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.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 java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class FileSystemTest { public static void main(final String[] args) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("initialModels/"); - final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FAMTest/"); - final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); - workspace.initAndClear(); - final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; - final Map map = reg.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - map.put("logicproblem", _xMIResourceFactoryImpl); - InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi"); - final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); - InputOutput.println("DSL loaded"); - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace); + try { + final Ecore2Logic ecore2Logic = new Ecore2Logic(); + final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); + final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/FAMTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); + InputOutput.println("DSL loaded"); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + workspace.writeModel(problem, "Fam.logicproblem"); + InputOutput.println("Problem created"); + long startTime = System.currentTimeMillis(); + LogicReasoner reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 4; + it.typeScopes.maxNewElements = 5; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } + int _size_1 = typeMapMin.size(); + boolean _notEquals_1 = (_size_1 != 0); + if (_notEquals_1) { + it.typeScopes.maxNewElementsByType = typeMapMax; + } + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); + long _currentTimeMillis = System.currentTimeMillis(); + long _minus = (_currentTimeMillis - startTime); + long totalTimeMin = (_minus / 60000); + long _currentTimeMillis_1 = System.currentTimeMillis(); + long _minus_1 = (_currentTimeMillis_1 - startTime); + long _divide = (_minus_1 / 1000); + long totalTimeSec = (_divide % 60); + InputOutput.println("Problem solved"); + InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 0150ef1d..0bb8f76e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -1,27 +1,12 @@ 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 com.google.common.base.Objects; import com.google.common.collect.Iterables; -import functionalarchitecture.Function; -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.DocumentationLevel; -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; -import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; 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.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.Collections; import java.util.HashMap; @@ -43,94 +28,24 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; import org.eclipse.viatra.query.runtime.api.IQuerySpecification; import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Exceptions; -import org.eclipse.xtext.xbase.lib.Extension; import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class GeneralTest { - public static String createAndSolveProblem(final EcoreMetamodelDescriptor metamodel, final List partialModel, final ViatraQuerySetDescriptor queries, final FileSystemWorkspace workspace) { - try { - String _xblockexpression = null; - { - @Extension - final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - final Ecore2Logic ecore2Logic = new Ecore2Logic(); - final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); - final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); - final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); - Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); - final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - LogicProblem problem = modelGenerationProblem.getOutput(); - workspace.writeModel(problem, "Fam.logicproblem"); - InputOutput.println("Problem created"); - long startTime = System.currentTimeMillis(); - LogicResult solution = null; - LogicReasoner reasoner = null; - VampireSolver _vampireSolver = new VampireSolver(); - reasoner = _vampireSolver; - final HashMap typeMapMin = new HashMap(); - final HashMap typeMapMax = new HashMap(); - final Function1 _function = (EClass s) -> { - return s.getName(); - }; - final Map list2MapMin = IterableExtensions.toMap(metamodel.getClasses(), _function); - final Function1 _function_1 = (EClass s) -> { - return s.getName(); - }; - final Map list2MapMax = IterableExtensions.toMap(metamodel.getClasses(), _function_1); - typeMapMin.put( - ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), - list2MapMin.get(Function.class.getSimpleName())), Integer.valueOf(1)); - typeMapMin.put( - ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), - list2MapMin.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2)); - typeMapMin.put( - ecore2Logic.TypeofEClass(modelGenerationProblem.getTrace(), - list2MapMin.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(3)); - typeMapMax.put( - ecore2Logic.TypeofEClass( - modelGenerationProblem.getTrace(), - list2MapMax.get(Function.class.getSimpleName())), Integer.valueOf(5)); - typeMapMax.put( - ecore2Logic.TypeofEClass( - modelGenerationProblem.getTrace(), - list2MapMax.get(functionalarchitecture.FunctionalInterface.class.getSimpleName())), Integer.valueOf(2)); - typeMapMax.put( - ecore2Logic.TypeofEClass( - modelGenerationProblem.getTrace(), - list2MapMax.get(FunctionalOutput.class.getSimpleName())), Integer.valueOf(4)); - VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); - final Procedure1 _function_2 = (VampireSolverConfiguration it) -> { - 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; - }; - final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function_2); - solution = reasoner.solve(problem, vampireConfig, workspace); - long _currentTimeMillis = System.currentTimeMillis(); - long _minus = (_currentTimeMillis - startTime); - long totalTimeMin = (_minus / 60000); - long _currentTimeMillis_1 = System.currentTimeMillis(); - long _minus_1 = (_currentTimeMillis_1 - startTime); - long _divide = (_minus_1 / 1000); - long totalTimeSec = (_divide % 60); - InputOutput.println("Problem solved"); - _xblockexpression = InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); - } - return _xblockexpression; - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); + public static Map getTypeMap(final Map classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { + final HashMap typeMap = new HashMap(); + final Function1 _function = (EClass s) -> { + return s.getName(); + }; + final Map listMap = IterableExtensions.toMap(metamodel.getClasses(), _function); + Set _keySet = classMap.keySet(); + for (final Class elem : _keySet) { + typeMap.put( + e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem)); } + return typeMap; } public static EcoreMetamodelDescriptor loadMetamodel(final EPackage pckg) { diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index bea4e8a6..81079764 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java @@ -1,34 +1,101 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; +import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; -import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage; +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.ecore2logic.Ecore2Logic_Trace; 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.builder.TracedOutput; +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.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 java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class YakinduTest { public static void main(final String[] args) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("initialModels/"); - final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/YakinduTest/"); - final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); - workspace.initAndClear(); - final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; - final Map map = reg.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - map.put("logicproblem", _xMIResourceFactoryImpl); - InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi"); - InputOutput.println("DSL loaded"); + try { + final Ecore2Logic ecore2Logic = new Ecore2Logic(); + final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); + final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/YakinduTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi"); + final Object queries = null; + InputOutput.println("DSL loaded"); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + workspace.writeModel(problem, "Yakindu.logicproblem"); + InputOutput.println("Problem created"); + long startTime = System.currentTimeMillis(); + LogicReasoner reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 20; + it.typeScopes.maxNewElements = 30; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } + int _size_1 = typeMapMin.size(); + boolean _notEquals_1 = (_size_1 != 0); + if (_notEquals_1) { + it.typeScopes.maxNewElementsByType = typeMapMax; + } + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); + long _currentTimeMillis = System.currentTimeMillis(); + long _minus = (_currentTimeMillis - startTime); + long totalTimeMin = (_minus / 60000); + long _currentTimeMillis_1 = System.currentTimeMillis(); + long _minus_1 = (_currentTimeMillis_1 - startTime); + long _divide = (_minus_1 / 1000); + long totalTimeSec = (_divide % 60); + InputOutput.println("Problem solved"); + InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index c0481fd8..29f8df00 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin index 53dc2a03..72d33e5d 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index 6c84f917..e9c4c0a4 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf