aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend13
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestAlloy.xtend190
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestViatra.xtend182
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/tester.xtend35
4 files changed, 413 insertions, 7 deletions
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 86c9092a..1559ee3f 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
@@ -4,11 +4,11 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import functionalarchitecture.Function 6import functionalarchitecture.Function
7import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
10import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor 11import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult 14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
@@ -30,8 +30,7 @@ import org.eclipse.emf.ecore.EReference
30import org.eclipse.emf.ecore.resource.Resource 30import org.eclipse.emf.ecore.resource.Resource
31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
32import org.eclipse.viatra.query.runtime.api.IQueryGroup 32import org.eclipse.viatra.query.runtime.api.IQueryGroup
33import org.eclipse.emf.ecore.EClassifier 33import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
34import functionalarchitecture.FunctionalOutput
35 34
36class GeneralTest { 35class GeneralTest {
37 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel, 36 def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List<EObject> partialModel,
@@ -67,7 +66,7 @@ class GeneralTest {
67 list2MapMin.get(Function.simpleName) 66 list2MapMin.get(Function.simpleName)
68 ), 1) 67 ), 1)
69 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, 68 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
70 list2MapMin.get(functionalarchitecture.FunctionalInterface.simpleName) 69 list2MapMin.get(FunctionalInterface.simpleName)
71 ), 2) 70 ), 2)
72 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace, 71 typeMapMin.put(ecore2Logic.TypeofEClass(modelGenerationProblem.trace,
73 list2MapMin.get(FunctionalOutput.simpleName) 72 list2MapMin.get(FunctionalOutput.simpleName)
@@ -80,7 +79,7 @@ class GeneralTest {
80 ), 5) 79 ), 5)
81 typeMapMax.put(ecore2Logic.TypeofEClass( 80 typeMapMax.put(ecore2Logic.TypeofEClass(
82 modelGenerationProblem.trace, 81 modelGenerationProblem.trace,
83 list2MapMax.get(functionalarchitecture.FunctionalInterface.simpleName) 82 list2MapMax.get(FunctionalInterface.simpleName)
84 ), 2) 83 ), 2)
85 typeMapMax.put(ecore2Logic.TypeofEClass( 84 typeMapMax.put(ecore2Logic.TypeofEClass(
86 modelGenerationProblem.trace, 85 modelGenerationProblem.trace,
@@ -92,7 +91,7 @@ class GeneralTest {
92 // add configuration things, in config file first 91 // add configuration things, in config file first
93 it.documentationLevel = DocumentationLevel::FULL 92 it.documentationLevel = DocumentationLevel::FULL
94 it.typeScopes.minNewElements = 6 93 it.typeScopes.minNewElements = 6
95 it.typeScopes.maxNewElements = 8 94 it.typeScopes.maxNewElements = 40
96 it.typeScopes.minNewElementsByType = typeMapMin 95 it.typeScopes.minNewElementsByType = typeMapMin
97 it.typeScopes.maxNewElementsByType = typeMapMax 96 it.typeScopes.maxNewElementsByType = typeMapMax
98 ] 97 ]
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestAlloy.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestAlloy.xtend
new file mode 100644
index 00000000..b0af3f64
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestAlloy.xtend
@@ -0,0 +1,190 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns
4import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage
5import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
6import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry
11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry
13import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
17import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
18import java.io.PrintWriter
19import java.text.SimpleDateFormat
20import java.util.Date
21import org.eclipse.emf.ecore.resource.Resource
22import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
23import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.impl.ModelResultImpl
24
25class YakinduTestAlloy {
26 def static void main(String[] args) {
27 val Ecore2Logic ecore2Logic = new Ecore2Logic
28 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
29 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
30 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
31
32 // Workspace setup
33 val Date date = new Date(System.currentTimeMillis)
34 val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");
35 val formattedDate = format.format(date)
36
37 val inputs = new FileSystemWorkspace('''initialModels/''', "")
38 val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "")
39 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")
40 workspace.initAndClear
41
42 // Logicproblem writing setup
43 val reg = Resource.Factory.Registry.INSTANCE
44 val map = reg.extensionToFactoryMap
45 map.put("logicproblem", new XMIResourceFactoryImpl)
46
47 println("Input and output workspaces are created")
48
49 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)
50 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")
51 val queries = GeneralTest.loadQueries(metamodel, Patterns.instance)
52// val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
53// val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")
54// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
55// val queries = null
56 println("DSL loaded")
57
58 var SZ_TOP = 100
59 var SZ_BOT = 100
60 var INC = 20
61 var REPS = 25
62
63 val RUNTIME = 300
64
65 var solverTimes = newArrayList
66 var transformationTimes = newArrayList
67 var LogicResult solution = null
68 var solver = "Alloy"
69
70 for (var k = 0; k < 1; k++) {
71
72 for (var i = SZ_BOT; i <= SZ_TOP; i += INC) {
73 var writer = new PrintWriter(
74 dataWorkspace.workspaceURI + "//_alloy" + i + "x" + REPS + "-" + formattedDate + ".csv")
75 writer.append("solver,size,TransformatonTime,sat?,kodkodTime,model?,modelTime\n")
76
77 val num = (i - SZ_BOT) / INC
78 println()
79 println("SOLVER: " + solver + ", SIZE=" + i)
80 println()
81
82 solverTimes.clear
83 transformationTimes.clear
84 for (var j = 0; j < REPS; j++) {
85 val Date date2 = new Date(System.currentTimeMillis)
86 val formattedDate2 = format.format(date2)
87 println(formattedDate2)
88 println("<<Run number " + j + ">> :")
89
90 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,
91 new Ecore2LogicConfiguration())
92 var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)
93 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,
94 new Viatra2LogicConfiguration)
95
96 var problem = modelGenerationProblem.output
97// workspace.writeModel(problem, "Yakindu.logicproblem")
98// println("Problem created")
99// Start Time
100 var startTime = System.currentTimeMillis
101
102 var AlloySolver reasoner
103 // *
104 reasoner = new AlloySolver
105
106 // /////////////////////////////////////////////////////
107 // Define Config File
108 val size = i
109 val inc = INC
110 val iter = j
111 val solverConfig = new AlloySolverConfiguration => [
112 // add configuration things, in config file first
113 it.documentationLevel = DocumentationLevel::FULL
114// it.iteration = iter
115 it.runtimeLimit = RUNTIME
116// it.typeScopes.maxNewElements = size
117 it.typeScopes.minNewElements = size
118 it.typeScopes.maxNewElements = size
119 ]
120 solution = reasoner.solve(problem, solverConfig, workspace)
121// print((solution as ModelResult).representation.get(0))
122// val soln = ((solution as ModelResult).representation.get(0) as VampireModel)
123// println(soln.confirmations)
124// println((solution as ModelResult).representation)
125// modelFound = !soln.confirmations.filter [
126// class == VLSFiniteModelImpl
127// ].isEmpty
128// ADD TO CSV
129 writer.append(solver + ",")
130 writer.append(size + ",")
131 writer.append(solution.statistics.transformationTime / 1000.0 + ",")
132
133// val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry).
134// value
135 val kodKodTime = (solution.statistics.entries.filter[name == "Alloy2KodKodTransformationTime"].
136 get(0) as IntStatisticEntry).value
137// print(solution.class)
138 val modOut = if(solution.class == ModelResultImpl) "FiniteModel" else "no"
139 val mod = solution.statistics.entries.filter[name == "Answer0Time"]
140 var modTime = 0.0
141 if (!mod.isEmpty) {
142 modTime = (mod.get(0) as IntStatisticEntry).value / 1000.0
143
144 }
145 writer.append("-,")
146 writer.append(kodKodTime.toString + ",")
147 writer.append(modOut + ",")
148 writer.append(modTime.toString + "")
149 writer.append("\n")
150
151 println("->" + modOut + " ... " + modTime)
152
153 // Run Garbage Collector
154 val Runtime r = Runtime.getRuntime();
155 r.gc();
156 r.gc();
157 r.gc();
158 Thread.sleep(3000)
159
160// print("(" + tTime + "/" + sTime + "s)..")
161// solverTimes.add(sTime)
162// transformationTimes.add(tTime)
163// } else {
164// writer.append("MNF" + ",")
165//// print("MNF")
166// }
167 // println("Problem solved")
168 // visualisation, see
169// var interpretations = reasoner.getInterpretations(solution as ModelResult)
170// for (interpretation : interpretations) {
171// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)
172// workspace.writeModel(model, "model.xmi")
173// }
174// var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
175// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
176// println("Problem solved")
177// println("Time was: " + totalTimeMin + ":" + totalTimeSec)
178 }
179// println()
180// var solverMed = solverTimes.sort.get(REPS / 2)
181// var transformationMed = transformationTimes.sort.get(REPS / 2)
182// writer.append(solverMed.toString + "," + transformationMed.toString)
183 writer.close
184 }
185
186 }
187
188 }
189
190}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestViatra.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestViatra.xtend
new file mode 100644
index 00000000..dbc90e97
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTestViatra.xtend
@@ -0,0 +1,182 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns
4import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage
5import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
6import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry
11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry
13import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
17import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
18import java.io.PrintWriter
19import java.text.SimpleDateFormat
20import java.util.Date
21import org.eclipse.emf.ecore.resource.Resource
22import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
23import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.impl.ModelResultImpl
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
26
27class YakinduTestViatra {
28 def static void main(String[] args) {
29 val Ecore2Logic ecore2Logic = new Ecore2Logic
30 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
31 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
32 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
33
34 // Workspace setup
35 val Date date = new Date(System.currentTimeMillis)
36 val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");
37 val formattedDate = format.format(date)
38
39 val inputs = new FileSystemWorkspace('''initialModels/''', "")
40 val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "")
41 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")
42 workspace.initAndClear
43
44 // Logicproblem writing setup
45 val reg = Resource.Factory.Registry.INSTANCE
46 val map = reg.extensionToFactoryMap
47 map.put("logicproblem", new XMIResourceFactoryImpl)
48
49 println("Input and output workspaces are created")
50
51 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)
52 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")
53 val queries = GeneralTest.loadQueries(metamodel, Patterns.instance)
54// val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
55// val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")
56// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
57// val queries = null
58 println("DSL loaded")
59
60 var SZ_TOP = 20
61 var SZ_BOT = 20
62 var INC = 20
63 var REPS = 5
64
65 val RUNTIME = 300
66
67 var solverTimes = newArrayList
68 var transformationTimes = newArrayList
69 var LogicResult solution = null
70 var solver = "Viatra"
71 var index = 2
72
73 for (var i = SZ_BOT; i <= SZ_TOP; i += INC*index) {
74 index*=2
75 var writer = new PrintWriter(
76 dataWorkspace.workspaceURI + "//_viatra" + i + "x" + REPS + "-" + formattedDate + ".csv")
77 writer.append("solver,size,TransformatonTime,sat?,kodkodTime,model?,modelTime\n")
78
79 val num = (i - SZ_BOT) / INC
80 println()
81 println("SOLVER: " + solver + ", SIZE=" + i)
82 println()
83
84 solverTimes.clear
85 transformationTimes.clear
86 for (var j = 0; j < REPS; j++) {
87
88 println("<<Run number " + j + ">> :")
89
90 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
91 var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)
92 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,
93 new Viatra2LogicConfiguration)
94
95 var problem = modelGenerationProblem.output
96 workspace.writeModel(problem, "Yakindu.logicproblem")
97// println("Problem created")
98// Start Time
99 var startTime = System.currentTimeMillis
100
101 var ViatraReasoner reasoner
102 // *
103 reasoner = new ViatraReasoner
104
105 // /////////////////////////////////////////////////////
106 // Define Config File
107 val size = i
108 val inc = INC
109 val iter = j
110 val solverConfig = new ViatraReasonerConfiguration => [
111 // add configuration things, in config file first
112// it.documentationLevel = DocumentationLevel::FULL
113// it.iteration = iter
114 it.runtimeLimit = RUNTIME
115 it.typeScopes.maxNewElements = size
116 it.typeScopes.minNewElements = size
117 ]
118
119 solution = reasoner.solve(problem, solverConfig, workspace)
120// print((solution as ModelResult).representation.get(0))
121// val soln = ((solution as ModelResult).representation.get(0) as VampireModel)
122// println(soln.confirmations)
123// println((solution as ModelResult).representation)
124// modelFound = !soln.confirmations.filter [
125// class == VLSFiniteModelImpl
126// ].isEmpty
127// ADD TO CSV
128 writer.append(solver + ",")
129 writer.append(size + ",")
130 writer.append(solution.statistics.transformationTime / 1000.0 + ",")
131
132// val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry).
133// value
134 val modOut = if(solution.class == ModelResultImpl) "FiniteModel" else "no"
135// val modTime = (solution.statistics.entries.filter[name.contains("Answer")].
136// get(0) as StringStatisticEntry).value
137 val modTime = solution.statistics.solverTime / 1000.0
138
139 writer.append("-,")
140 writer.append("-,")
141 writer.append(modOut + ",")
142 writer.append(modTime.toString + "")
143 writer.append("\n")
144
145 println("->" + modOut + " ... " + modTime)
146
147 // Run Garbage Collector
148 val Runtime r = Runtime.getRuntime();
149 r.gc();
150 r.gc();
151 r.gc();
152 Thread.sleep(3000)
153
154// print("(" + tTime + "/" + sTime + "s)..")
155// solverTimes.add(sTime)
156// transformationTimes.add(tTime)
157// } else {
158// writer.append("MNF" + ",")
159//// print("MNF")
160// }
161 // println("Problem solved")
162 // visualisation, see
163// var interpretations = reasoner.getInterpretations(solution as ModelResult)
164// for (interpretation : interpretations) {
165// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)
166// workspace.writeModel(model, "model.xmi")
167// }
168// var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
169// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
170// println("Problem solved")
171// println("Time was: " + totalTimeMin + ":" + totalTimeSec)
172 }
173// println()
174// var solverMed = solverTimes.sort.get(REPS / 2)
175// var transformationMed = transformationTimes.sort.get(REPS / 2)
176// writer.append(solverMed.toString + "," + transformationMed.toString)
177 writer.close
178 }
179
180 }
181
182}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/tester.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/tester.xtend
new file mode 100644
index 00000000..2bf0c4cc
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/tester.xtend
@@ -0,0 +1,35 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse
2
3import java.io.BufferedReader
4import java.io.FileInputStream
5import java.io.InputStream
6import java.io.InputStreamReader
7
8class tester {
9 def static void main(String[] args) {
10 val InputStream is = new FileInputStream("C://Users//Aren Babikian//git//VIATRA-Generator//Tests//ca.mcgill.ecse.dslreasoner.vampire.test//src//ca//mcgill//ecse//dslreasoner//vampire//icse//90-110Z3.txt");
11 val BufferedReader buf = new BufferedReader(new InputStreamReader(is));
12 var String line = buf.readLine();
13 val StringBuilder sb = new StringBuilder();
14 while (line != null) {
15 sb.append(line);
16 line = buf.readLine();
17 }
18 val String str = sb.toString();
19
20 val satArray = str.split("Model")
21
22 val satTimes = newArrayList
23
24 for(sat : satArray.subList(1, satArray.length)) {
25 satTimes.add(sat.substring(2, 8))
26 }
27
28 for(t : satTimes) {
29 println(t)
30 }
31
32
33
34 }
35}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-27 20:18:42 +0000