diff options
author | 2019-10-07 00:35:42 -0400 | |
---|---|---|
committer | 2020-06-07 19:42:47 -0400 | |
commit | b503c81bee920c18806af25393d0a90b8f77dba6 (patch) | |
tree | 9b70f606bfa7fa450457c04714e045e5ac5f6199 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse | |
parent | VAMPIRE: fix model generation (diff) | |
download | VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.gz VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.zst VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.zip |
VAMPIRE: Implement Vampire measurement code
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse')
3 files changed, 173 insertions, 80 deletions
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 70ded02d..35b76350 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 | |||
@@ -50,7 +50,7 @@ class EcoreTest { | |||
50 | it.documentationLevel = DocumentationLevel::FULL | 50 | it.documentationLevel = DocumentationLevel::FULL |
51 | ] | 51 | ] |
52 | 52 | ||
53 | solution = reasoner.solve(logicProblem, vampireConfig, workspace, "ECO") | 53 | solution = reasoner.solve(logicProblem, vampireConfig, workspace) |
54 | 54 | ||
55 | println("Problem solved") | 55 | println("Problem solved") |
56 | 56 | ||
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 5143641b..a7da818c 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 | |||
@@ -2,12 +2,13 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
5 | import functionalarchitecture.FAMTerminator | ||
5 | import functionalarchitecture.Function | 6 | import functionalarchitecture.Function |
6 | import functionalarchitecture.FunctionalArchitectureModel | 7 | import functionalarchitecture.FunctionalArchitectureModel |
7 | import functionalarchitecture.FunctionalInterface | 8 | import functionalarchitecture.FunctionalInterface |
8 | import functionalarchitecture.FunctionalOutput | 9 | import functionalarchitecture.FunctionalOutput |
9 | import functionalarchitecture.FunctionalarchitecturePackage | 10 | import functionalarchitecture.FunctionalarchitecturePackage |
10 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | 11 | //import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
@@ -22,7 +23,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | |||
22 | import java.util.HashMap | 23 | import java.util.HashMap |
23 | import org.eclipse.emf.ecore.resource.Resource | 24 | import org.eclipse.emf.ecore.resource.Resource |
24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
25 | import functionalarchitecture.FAMTerminator | ||
26 | 26 | ||
27 | class FAMTest { | 27 | class FAMTest { |
28 | def static void main(String[] args) { | 28 | def static void main(String[] args) { |
@@ -47,15 +47,15 @@ class FAMTest { | |||
47 | // Load DSL | 47 | // Load DSL |
48 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | 48 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
49 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") | 49 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") |
50 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | 50 | // val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) |
51 | // val queries = null | 51 | val queries = null |
52 | 52 | ||
53 | println("DSL loaded") | 53 | println("DSL loaded") |
54 | 54 | ||
55 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 55 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
56 | var problem = modelGenerationProblem.output | 56 | var problem = modelGenerationProblem.output |
57 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | 57 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output |
58 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | 58 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output |
59 | workspace.writeModel(problem, "Fam.logicproblem") | 59 | workspace.writeModel(problem, "Fam.logicproblem") |
60 | 60 | ||
61 | println("Problem created") | 61 | println("Problem created") |
@@ -94,14 +94,15 @@ class FAMTest { | |||
94 | 94 | ||
95 | it.typeScopes.minNewElements = 8//24 | 95 | it.typeScopes.minNewElements = 8//24 |
96 | it.typeScopes.maxNewElements = 10//25 | 96 | it.typeScopes.maxNewElements = 10//25 |
97 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 97 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
98 | // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 98 | // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
99 | it.contCycleLevel = 5 | 99 | it.contCycleLevel = 5 |
100 | it.uniquenessDuplicates = false | 100 | it.uniquenessDuplicates = false |
101 | ] | 101 | ] |
102 | 102 | ||
103 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | 103 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
104 | 104 | ||
105 | println("Problem solved") | ||
105 | // visualisation, see | 106 | // visualisation, see |
106 | var interpretations = reasoner.getInterpretations(solution as ModelResult) | 107 | var interpretations = reasoner.getInterpretations(solution as ModelResult) |
107 | // interpretations.get(0) as VampireModelInterpretation | 108 | // interpretations.get(0) as VampireModelInterpretation |
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 fb1bdb59..057bcf12 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,25 +1,27 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage | 3 | import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
7 | import functionalarchitecture.FunctionalarchitecturePackage | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 10 | 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.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
13 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 16 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
14 | import java.util.HashMap | 17 | import java.io.PrintWriter |
15 | import org.eclipse.emf.ecore.resource.Resource | 18 | import org.eclipse.emf.ecore.resource.Resource |
16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
17 | 20 | ||
18 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.* | ||
19 | |||
20 | class YakinduTest { | 21 | class YakinduTest { |
21 | def static void main(String[] args) { | 22 | def static void main(String[] args) { |
22 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 23 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
24 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
23 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 25 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
24 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 26 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
25 | 27 | ||
@@ -35,76 +37,166 @@ class YakinduTest { | |||
35 | 37 | ||
36 | println("Input and output workspaces are created") | 38 | println("Input and output workspaces are created") |
37 | 39 | ||
38 | val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) | 40 | // val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) |
39 | val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") | 41 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
40 | // val queries = GeneralTest.loadQueries(metamodel, yakinduPatterns.instance) | 42 | // val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi") |
41 | val queries = null | 43 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") |
42 | 44 | // val queries = GeneralTest.loadQueries(metamodel, YakinduPatterns.instance) | |
45 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | ||
46 | // val queries = null | ||
43 | println("DSL loaded") | 47 | println("DSL loaded") |
44 | 48 | ||
45 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 49 | var MAX = 150 |
46 | var problem = modelGenerationProblem.output | 50 | var START = 10 |
47 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | 51 | var INC = 20 |
52 | var REPS = 1 | ||
53 | |||
54 | val EXACT = -1 | ||
55 | if (EXACT!= -1) { | ||
56 | MAX = EXACT | ||
57 | START = EXACT | ||
58 | INC = 1 | ||
59 | REPS = 5 | ||
60 | } | ||
61 | |||
62 | var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv") | ||
63 | writer.append("size,") | ||
64 | for (var x = 0; x < REPS; x++) { | ||
65 | writer.append("t" + x + ",") | ||
66 | } | ||
67 | writer.append("avg\n") | ||
68 | var totalTime = 0.0 | ||
69 | var totFound = 0.0 | ||
70 | var modelFound = true | ||
71 | var LogicResult solution = null | ||
72 | for (var i = START; i <= MAX; i += INC) { | ||
73 | val num = (i - START) / INC | ||
74 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | ||
75 | writer.append(i + ",") | ||
76 | totalTime = 0.0 | ||
77 | totFound = 0.0 | ||
78 | modelFound = true | ||
79 | for (var j = 0; j < REPS; j++) { | ||
80 | |||
81 | print(j) | ||
82 | |||
83 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | ||
84 | var problem = modelGenerationProblem.output | ||
85 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
48 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | 86 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output |
49 | workspace.writeModel(problem, "Yakindu.logicproblem") | 87 | workspace.writeModel(problem, "Yakindu.logicproblem") |
50 | 88 | ||
51 | println("Problem created") | 89 | // println("Problem created") |
52 | 90 | // Start Time | |
53 | // Start Time | 91 | var startTime = System.currentTimeMillis |
54 | var startTime = System.currentTimeMillis | 92 | |
55 | 93 | var VampireSolver reasoner | |
56 | var VampireSolver reasoner | 94 | // * |
57 | // * | 95 | reasoner = new VampireSolver |
58 | reasoner = new VampireSolver | 96 | |
59 | 97 | // ///////////////////////////////////////////////////// | |
60 | // ///////////////////////////////////////////////////// | 98 | // Minimum Scope |
61 | // Minimum Scope | 99 | // val classMapMin = new HashMap<Class, Integer> |
62 | val classMapMin = new HashMap<Class, Integer> | 100 | // classMapMin.put(Region, 1) |
63 | classMapMin.put(Region, 1) | 101 | // classMapMin.put(Transition, 2) |
64 | classMapMin.put(Transition, 2) | 102 | // classMapMin.put(CompositeElement, 3) |
65 | classMapMin.put(CompositeElement, 3) | 103 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
66 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 104 | // Maximum Scope |
67 | 105 | // val classMapMax = new HashMap<Class, Integer> | |
68 | // Maximum Scope | 106 | // classMapMax.put(Region, 5) |
69 | val classMapMax = new HashMap<Class, Integer> | 107 | // classMapMax.put(Transition, 2) |
70 | classMapMax.put(Region, 5) | 108 | // classMapMax.put(Synchronization, 4) |
71 | classMapMax.put(Transition, 2) | 109 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
72 | classMapMax.put(Synchronization, 4) | 110 | // Define Config File |
73 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | 111 | val size = i |
74 | 112 | val inc = INC | |
75 | // Define Config File | 113 | val vampireConfig = new VampireSolverConfiguration => [ |
76 | val vampireConfig = new VampireSolverConfiguration => [ | 114 | // add configuration things, in config file first |
77 | // add configuration things, in config file first | 115 | it.documentationLevel = DocumentationLevel::FULL |
78 | it.documentationLevel = DocumentationLevel::FULL | 116 | |
79 | 117 | it.typeScopes.minNewElements = size - inc | |
80 | it.typeScopes.minNewElements = 20 | 118 | it.typeScopes.maxNewElements = size |
81 | it.typeScopes.maxNewElements = 30 | 119 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
82 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 120 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
83 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 121 | it.contCycleLevel = 5 |
84 | it.contCycleLevel = 5 | 122 | it.uniquenessDuplicates = false |
85 | it.uniquenessDuplicates = false | 123 | ] |
86 | ] | 124 | |
87 | 125 | solution = reasoner.solve(problem, vampireConfig, workspace) | |
88 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "YAK") | 126 | // print((solution as ModelResult).representation.get(0)) |
89 | 127 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | |
90 | /*/ | 128 | // println(soln.confirmations) |
91 | * | 129 | // println((solution as ModelResult).representation) |
92 | * reasoner = new AlloySolver | 130 | // modelFound = !soln.confirmations.filter [ |
93 | * val alloyConfig = new AlloySolverConfiguration => [ | 131 | // class == VLSFiniteModelImpl |
94 | * it.typeScopes.maxNewElements = 7 | 132 | // ].isEmpty |
95 | * it.typeScopes.minNewElements = 3 | 133 | // |
96 | * it.solutionScope.numberOfRequiredSolution = 1 | 134 | // if (modelFound) { |
97 | * it.typeScopes.maxNewIntegers = 0 | 135 | val time = solution.statistics.transformationTime / 1000.0 |
98 | * it.documentationLevel = DocumentationLevel::NORMAL | 136 | writer.append(time + ",") |
99 | * ] | 137 | print("(" + time + ")..") |
100 | * solution = reasoner.solve(problem, alloyConfig, workspace) | 138 | totalTime += time |
101 | //*/ | 139 | totFound += 1 |
102 | // ///////////////////////////////////////////////////// | 140 | // } else { |
103 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | 141 | // writer.append("MNF" + ",") |
104 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | 142 | //// print("MNF") |
105 | 143 | // } | |
106 | println("Problem solved") | 144 | // println("Problem solved") |
107 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | 145 | // visualisation, see |
146 | // var interpretations = reasoner.getInterpretations(solution as ModelResult) | ||
147 | /* interpretations.get(0) as VampireModelInterpretation | ||
148 | * println(ecore2Logic.IsAttributeValue(modelGenerationProblem.trace, ) | ||
149 | * Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) ) | ||
150 | * ) | ||
151 | * println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType) | ||
152 | print(interpretations.class)*/ | ||
153 | // for (interpretation : interpretations) { | ||
154 | // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) | ||
155 | // workspace.writeModel(model, "model.xmi") | ||
156 | /* val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations | ||
157 | * if (representation instanceof PartialInterpretation) { | ||
158 | * val vis1 = new PartialInterpretation2Gml | ||
159 | * val gml = vis1.transform(representation) | ||
160 | * workspace.writeText("model.gml", gml) | ||
161 | |||
162 | * val vis2 = new GraphvizVisualiser | ||
163 | * val dot = vis2.visualiseConcretization(representation) | ||
164 | * dot.writeToFile(workspace, "model.png") | ||
165 | * } else { | ||
166 | * println("ERROR") | ||
167 | * } | ||
168 | look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor*/ | ||
169 | // } | ||
170 | /*/ | ||
171 | * | ||
172 | * reasoner = new AlloySolver | ||
173 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
174 | * it.typeScopes.maxNewElements = 7 | ||
175 | * it.typeScopes.minNewElements = 3 | ||
176 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
177 | * it.typeScopes.maxNewIntegers = 0 | ||
178 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
179 | * ] | ||
180 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
181 | //*/ | ||
182 | // ///////////////////////////////////////////////////// | ||
183 | // var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | ||
184 | // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | ||
185 | // println("Problem solved") | ||
186 | // println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
187 | } | ||
188 | println() | ||
189 | var avg = 0.0 | ||
190 | if (totFound == 0) { | ||
191 | avg = -1 | ||
192 | } else { | ||
193 | avg = totalTime / totFound | ||
194 | } | ||
195 | writer.append(avg.toString) | ||
196 | writer.append("\n") | ||
197 | } | ||
198 | writer.close | ||
199 | |||
108 | } | 200 | } |
109 | 201 | ||
110 | } | 202 | } |