diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-11 16:59:48 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:36:36 -0400 |
commit | ab556f8705c70a3376bcadf73698c95fd4df5bf9 (patch) | |
tree | 0c34ae58ee74f4f154659ad303775cee3e5eb206 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src | |
parent | Implement containment circularity avoidance #20 (diff) | |
download | VIATRA-Generator-ab556f8705c70a3376bcadf73698c95fd4df5bf9.tar.gz VIATRA-Generator-ab556f8705c70a3376bcadf73698c95fd4df5bf9.tar.zst VIATRA-Generator-ab556f8705c70a3376bcadf73698c95fd4df5bf9.zip |
VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
4 files changed, 273 insertions, 138 deletions
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
6 | import functionalarchitecture.Function | ||
7 | import functionalarchitecture.FunctionalInterface | ||
8 | import functionalarchitecture.FunctionalOutput | ||
4 | import functionalarchitecture.FunctionalarchitecturePackage | 9 | import functionalarchitecture.FunctionalarchitecturePackage |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
6 | import java.util.LinkedList | 18 | import java.util.HashMap |
7 | import org.eclipse.emf.ecore.EObject | ||
8 | import org.eclipse.emf.ecore.resource.Resource | 19 | import org.eclipse.emf.ecore.resource.Resource |
9 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
10 | 21 | ||
11 | class FAMTest { | 22 | class FAMTest { |
12 | def static void main(String[] args) { | 23 | def static void main(String[] args) { |
13 | //Workspace setup | 24 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
25 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
26 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
27 | |||
28 | // Workspace setup | ||
14 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | 29 | val inputs = new FileSystemWorkspace('''initialModels/''', "") |
15 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") | 30 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") |
16 | workspace.initAndClear | 31 | workspace.initAndClear |
17 | 32 | ||
18 | //Logicproblem writing setup | 33 | // Logicproblem writing setup |
19 | val reg = Resource.Factory.Registry.INSTANCE | 34 | val reg = Resource.Factory.Registry.INSTANCE |
20 | val map = reg.extensionToFactoryMap | 35 | val map = reg.extensionToFactoryMap |
21 | map.put("logicproblem", new XMIResourceFactoryImpl) | 36 | map.put("logicproblem", new XMIResourceFactoryImpl) |
22 | |||
23 | 37 | ||
24 | println("Input and output workspaces are created") | 38 | println("Input and output workspaces are created") |
25 | 39 | ||
40 | // Load DSL | ||
26 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | 41 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
27 | val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") | 42 | val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") |
28 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | 43 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) |
29 | 44 | ||
30 | println("DSL loaded") | 45 | println("DSL loaded") |
46 | |||
47 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | ||
48 | var problem = modelGenerationProblem.output | ||
49 | // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
50 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | ||
51 | workspace.writeModel(problem, "Fam.logicproblem") | ||
52 | |||
53 | println("Problem created") | ||
54 | |||
55 | //Start Time | ||
56 | var startTime = System.currentTimeMillis | ||
57 | |||
58 | var LogicReasoner reasoner | ||
59 | // * | ||
60 | reasoner = new VampireSolver | ||
61 | |||
62 | // ///////////////////////////////////////////////////// | ||
63 | // Minimum Scope | ||
64 | val classMapMin = new HashMap<Class, Integer> | ||
65 | classMapMin.put(Function, 1) | ||
66 | classMapMin.put(FunctionalInterface, 2) | ||
67 | classMapMin.put(FunctionalOutput, 3) | ||
31 | 68 | ||
32 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | 69 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
70 | |||
71 | // Maximum Scope | ||
72 | val classMapMax = new HashMap<Class, Integer> | ||
73 | classMapMax.put(Function, 5) | ||
74 | classMapMax.put(FunctionalInterface, 2) | ||
75 | classMapMax.put(FunctionalOutput, 4) | ||
76 | |||
77 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
78 | |||
79 | // Define Config File | ||
80 | val vampireConfig = new VampireSolverConfiguration => [ | ||
81 | // add configuration things, in config file first | ||
82 | it.documentationLevel = DocumentationLevel::FULL | ||
83 | |||
84 | it.typeScopes.minNewElements = 4 | ||
85 | it.typeScopes.maxNewElements = 5 | ||
86 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | ||
87 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | ||
88 | it.contCycleLevel = 5 | ||
89 | it.uniquenessDuplicates = false | ||
90 | ] | ||
91 | |||
92 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | ||
93 | |||
94 | /*/ | ||
95 | * | ||
96 | * reasoner = new AlloySolver | ||
97 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
98 | * it.typeScopes.maxNewElements = 7 | ||
99 | * it.typeScopes.minNewElements = 3 | ||
100 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
101 | * it.typeScopes.maxNewIntegers = 0 | ||
102 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
103 | * ] | ||
104 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
105 | //*/ | ||
106 | // ///////////////////////////////////////////////////// | ||
107 | |||
108 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | ||
109 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | ||
110 | |||
111 | println("Problem solved") | ||
112 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
33 | } | 113 | } |
34 | 114 | ||
35 | |||
36 | } | 115 | } |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import functionalarchitecture.FunctionalarchitecturePackage | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries |
4 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | 4 | import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
15 | import java.util.HashMap | ||
6 | import org.eclipse.emf.ecore.resource.Resource | 16 | import org.eclipse.emf.ecore.resource.Resource |
7 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 17 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
8 | 18 | ||
9 | class FileSystemTest { | 19 | class FileSystemTest { |
10 | def static void main(String[] args) { | 20 | def static void main(String[] args) { |
11 | //Workspace setup | 21 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
22 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
23 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
24 | |||
25 | // Workspace setup | ||
12 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | 26 | val inputs = new FileSystemWorkspace('''initialModels/''', "") |
13 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") | 27 | val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") |
14 | workspace.initAndClear | 28 | workspace.initAndClear |
15 | 29 | ||
16 | //Logicproblem writing setup | 30 | // Logicproblem writing setup |
17 | val reg = Resource.Factory.Registry.INSTANCE | 31 | val reg = Resource.Factory.Registry.INSTANCE |
18 | val map = reg.extensionToFactoryMap | 32 | val map = reg.extensionToFactoryMap |
19 | map.put("logicproblem", new XMIResourceFactoryImpl) | 33 | map.put("logicproblem", new XMIResourceFactoryImpl) |
20 | 34 | ||
21 | println("Input and output workspaces are created") | 35 | println("Input and output workspaces are created") |
22 | 36 | ||
23 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | 37 | val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE) |
24 | val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") | 38 | val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi") |
25 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | 39 | //val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance) |
26 | 40 | ||
27 | println("DSL loaded") | 41 | println("DSL loaded") |
28 | 42 | ||
29 | GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | 43 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
44 | var problem = modelGenerationProblem.output | ||
45 | // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
46 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | ||
47 | workspace.writeModel(problem, "Fam.logicproblem") | ||
48 | |||
49 | println("Problem created") | ||
50 | |||
51 | // Start Time | ||
52 | var startTime = System.currentTimeMillis | ||
53 | |||
54 | var LogicReasoner reasoner | ||
55 | // * | ||
56 | reasoner = new VampireSolver | ||
57 | |||
58 | // ///////////////////////////////////////////////////// | ||
59 | // Minimum Scope | ||
60 | val classMapMin = new HashMap<Class, Integer> | ||
61 | // classMapMin.put(Function, 1) | ||
62 | // classMapMin.put(FunctionalInterface, 2) | ||
63 | // classMapMin.put(FunctionalOutput, 3) | ||
64 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
65 | |||
66 | // Maximum Scope | ||
67 | val classMapMax = new HashMap<Class, Integer> | ||
68 | // classMapMax.put(Function, 5) | ||
69 | // classMapMax.put(FunctionalInterface, 2) | ||
70 | // classMapMax.put(FunctionalOutput, 4) | ||
71 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
72 | |||
73 | // Define Config File | ||
74 | val vampireConfig = new VampireSolverConfiguration => [ | ||
75 | // add configuration things, in config file first | ||
76 | it.documentationLevel = DocumentationLevel::FULL | ||
77 | |||
78 | it.typeScopes.minNewElements = 4 | ||
79 | it.typeScopes.maxNewElements = 5 | ||
80 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | ||
81 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | ||
82 | it.contCycleLevel = 5 | ||
83 | it.uniquenessDuplicates = false | ||
84 | ] | ||
85 | |||
86 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | ||
87 | |||
88 | /*/ | ||
89 | * | ||
90 | * reasoner = new AlloySolver | ||
91 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
92 | * it.typeScopes.maxNewElements = 7 | ||
93 | * it.typeScopes.minNewElements = 3 | ||
94 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
95 | * it.typeScopes.maxNewIntegers = 0 | ||
96 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
97 | * ] | ||
98 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
99 | //*/ | ||
100 | // ///////////////////////////////////////////////////// | ||
101 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | ||
102 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | ||
103 | |||
104 | println("Problem solved") | ||
105 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
30 | } | 106 | } |
31 | 107 | ||
32 | |||
33 | } | 108 | } |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
6 | import functionalarchitecture.Function | ||
7 | import functionalarchitecture.FunctionalInterface | ||
8 | import functionalarchitecture.FunctionalOutput | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
15 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | 7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
19 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
20 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
21 | import java.util.HashMap | 9 | import java.util.HashMap |
22 | import java.util.List | 10 | import java.util.List |
11 | import java.util.Map | ||
23 | import org.eclipse.emf.ecore.EAttribute | 12 | import org.eclipse.emf.ecore.EAttribute |
24 | import org.eclipse.emf.ecore.EClass | 13 | import org.eclipse.emf.ecore.EClass |
25 | import org.eclipse.emf.ecore.EEnum | 14 | import org.eclipse.emf.ecore.EEnum |
@@ -30,100 +19,18 @@ import org.eclipse.emf.ecore.EReference | |||
30 | import org.eclipse.emf.ecore.resource.Resource | 19 | import org.eclipse.emf.ecore.resource.Resource |
31 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
32 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 21 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
33 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
34 | 22 | ||
35 | class GeneralTest { | 23 | class GeneralTest { |
36 | def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, | 24 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { |
37 | ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { | 25 | val typeMap = new HashMap<Type, Integer> |
38 | val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 26 | val listMap = metamodel.classes.toMap[s|s.name] |
39 | val Ecore2Logic ecore2Logic = new Ecore2Logic | ||
40 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
41 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
42 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
43 | |||
44 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | ||
45 | var problem = modelGenerationProblem.output | ||
46 | // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
47 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | ||
48 | workspace.writeModel(problem, "Fam.logicproblem") | ||
49 | |||
50 | println("Problem created") | ||
51 | |||
52 | var startTime = System.currentTimeMillis | ||
53 | |||
54 | var LogicResult solution | ||
55 | var LogicReasoner reasoner | ||
56 | |||
57 | // * | ||
58 | reasoner = new VampireSolver | ||
59 | |||
60 | // Setting up scope | ||
61 | val typeMapMin = new HashMap<Type, Integer> | ||
62 | val typeMapMax = new HashMap<Type, Integer> | ||
63 | val list2MapMin = metamodel.classes.toMap[s|s.name] | ||
64 | val list2MapMax = metamodel.classes.toMap[s|s.name] | ||
65 | |||
66 | // Minimum Scope | ||
67 | typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, | ||
68 | list2MapMin.get(Function.simpleName) | ||
69 | ), 1) | ||
70 | typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, | ||
71 | list2MapMin.get(FunctionalInterface.simpleName) | ||
72 | ), 2) | ||
73 | typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, | ||
74 | list2MapMin.get(FunctionalOutput.simpleName) | ||
75 | ), 3) | ||
76 | |||
77 | // Maximum Scope | ||
78 | typeMapMax.put(ecore2Logic.TypeofEClass( | ||
79 | modelGenerationProblem.trace, | ||
80 | list2MapMax.get(Function.simpleName) | ||
81 | ), 5) | ||
82 | typeMapMax.put(ecore2Logic.TypeofEClass( | ||
83 | modelGenerationProblem.trace, | ||
84 | list2MapMax.get(FunctionalInterface.simpleName) | ||
85 | ), 2) | ||
86 | typeMapMax.put(ecore2Logic.TypeofEClass( | ||
87 | modelGenerationProblem.trace, | ||
88 | list2MapMax.get(FunctionalOutput.simpleName) | ||
89 | ), 4) | ||
90 | |||
91 | // Configuration | ||
92 | val vampireConfig = new VampireSolverConfiguration => [ | ||
93 | // add configuration things, in config file first | ||
94 | it.documentationLevel = DocumentationLevel::FULL | ||
95 | it.typeScopes.minNewElements = 4 | ||
96 | it.typeScopes.maxNewElements = 25 | ||
97 | it.typeScopes.minNewElementsByType = typeMapMin | ||
98 | it.typeScopes.maxNewElementsByType = typeMapMax | ||
99 | it.contCycleLevel = 5 | ||
100 | it.uniquenessDuplicates = false | ||
101 | ] | ||
102 | solution = reasoner.solve(problem, vampireConfig, workspace) | ||
103 | |||
104 | /*/ | ||
105 | * | ||
106 | * reasoner = new AlloySolver | ||
107 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
108 | * it.typeScopes.maxNewElements = 7 | ||
109 | * it.typeScopes.minNewElements = 3 | ||
110 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
111 | * it.typeScopes.maxNewIntegers = 0 | ||
112 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
113 | * ] | ||
114 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
115 | //*/ | ||
116 | |||
117 | |||
118 | var totalTimeMin = (System.currentTimeMillis - startTime)/60000 | ||
119 | var totalTimeSec = ((System.currentTimeMillis - startTime)/1000)% 60 | ||
120 | |||
121 | println("Problem solved") | ||
122 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
123 | |||
124 | |||
125 | |||
126 | 27 | ||
28 | for (Class elem : classMap.keySet) { | ||
29 | typeMap.put(e2l.TypeofEClass( | ||
30 | trace, listMap.get(elem.simpleName) | ||
31 | ), classMap.get(elem)) | ||
32 | } | ||
33 | return typeMap | ||
127 | } | 34 | } |
128 | 35 | ||
129 | def static loadMetamodel(EPackage pckg) { | 36 | 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import functionalarchitecture.FunctionalarchitecturePackage | 3 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 13 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
14 | import java.util.HashMap | ||
5 | import org.eclipse.emf.ecore.resource.Resource | 15 | import org.eclipse.emf.ecore.resource.Resource |
6 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
7 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | ||
8 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns | ||
9 | 17 | ||
10 | class YakinduTest { | 18 | class YakinduTest { |
11 | def static void main(String[] args) { | 19 | def static void main(String[] args) { |
12 | //Workspace setup | 20 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
21 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
22 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
23 | |||
24 | // Workspace setup | ||
13 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | 25 | val inputs = new FileSystemWorkspace('''initialModels/''', "") |
14 | val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") | 26 | val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") |
15 | workspace.initAndClear | 27 | workspace.initAndClear |
16 | 28 | ||
17 | //Logicproblem writing setup | 29 | // Logicproblem writing setup |
18 | val reg = Resource.Factory.Registry.INSTANCE | 30 | val reg = Resource.Factory.Registry.INSTANCE |
19 | val map = reg.extensionToFactoryMap | 31 | val map = reg.extensionToFactoryMap |
20 | map.put("logicproblem", new XMIResourceFactoryImpl) | 32 | map.put("logicproblem", new XMIResourceFactoryImpl) |
21 | 33 | ||
22 | println("Input and output workspaces are created") | 34 | println("Input and output workspaces are created") |
23 | 35 | ||
24 | val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) | 36 | val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) |
25 | val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") | 37 | val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") |
26 | // val queries = GeneralTest.loadQueries(metamodel, FamPa | 38 | // val queries = GeneralTest.loadQueries(metamodel, FamPa |
39 | val queries = null | ||
27 | 40 | ||
28 | println("DSL loaded") | 41 | println("DSL loaded") |
29 | 42 | ||
30 | // GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) | 43 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
44 | var problem = modelGenerationProblem.output | ||
45 | // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
46 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | ||
47 | workspace.writeModel(problem, "Yakindu.logicproblem") | ||
48 | |||
49 | println("Problem created") | ||
50 | |||
51 | // Start Time | ||
52 | var startTime = System.currentTimeMillis | ||
53 | |||
54 | var LogicReasoner reasoner | ||
55 | // * | ||
56 | reasoner = new VampireSolver | ||
57 | |||
58 | // ///////////////////////////////////////////////////// | ||
59 | // Minimum Scope | ||
60 | val classMapMin = new HashMap<Class, Integer> | ||
61 | // classMapMin.put(Function, 1) | ||
62 | // classMapMin.put(FunctionalInterface, 2) | ||
63 | // classMapMin.put(FunctionalOutput, 3) | ||
64 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
65 | |||
66 | // Maximum Scope | ||
67 | val classMapMax = new HashMap<Class, Integer> | ||
68 | // classMapMax.put(Function, 5) | ||
69 | // classMapMax.put(FunctionalInterface, 2) | ||
70 | // classMapMax.put(FunctionalOutput, 4) | ||
71 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
72 | |||
73 | // Define Config File | ||
74 | val vampireConfig = new VampireSolverConfiguration => [ | ||
75 | // add configuration things, in config file first | ||
76 | it.documentationLevel = DocumentationLevel::FULL | ||
77 | |||
78 | it.typeScopes.minNewElements = 20 | ||
79 | it.typeScopes.maxNewElements = 30 | ||
80 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | ||
81 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | ||
82 | it.contCycleLevel = 5 | ||
83 | it.uniquenessDuplicates = false | ||
84 | ] | ||
85 | |||
86 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | ||
87 | |||
88 | /*/ | ||
89 | * | ||
90 | * reasoner = new AlloySolver | ||
91 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
92 | * it.typeScopes.maxNewElements = 7 | ||
93 | * it.typeScopes.minNewElements = 3 | ||
94 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
95 | * it.typeScopes.maxNewIntegers = 0 | ||
96 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
97 | * ] | ||
98 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
99 | //*/ | ||
100 | // ///////////////////////////////////////////////////// | ||
101 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | ||
102 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | ||
103 | |||
104 | println("Problem solved") | ||
105 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
31 | } | 106 | } |
32 | 107 | ||
33 | |||
34 | } | 108 | } |