aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend103
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend76
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend275
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend2
4 files changed, 295 insertions, 161 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend
new file mode 100644
index 00000000..a8b4dcfb
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.xtend
@@ -0,0 +1,103 @@
1package ca.mcgill.ecse.dslreasoner.vampire.test
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import functionalarchitecture.FunctionalarchitecturePackage
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
11import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
12import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
14import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
16import java.util.List
17import org.eclipse.emf.ecore.EAttribute
18import org.eclipse.emf.ecore.EClass
19import org.eclipse.emf.ecore.EEnum
20import org.eclipse.emf.ecore.EEnumLiteral
21import org.eclipse.emf.ecore.EObject
22import org.eclipse.emf.ecore.EReference
23import org.eclipse.emf.ecore.resource.Resource
24import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
25
26class DslTest {
27 def static void main(String[] args) {
28 val inputs = new FileSystemWorkspace('''initialModels/''', "")
29 val workspace = new FileSystemWorkspace('''outputDslModels/''', "")
30 workspace.initAndClear
31
32 println("Input and output workspaces are created")
33
34 val metamodel = loadMetamodel()
35 val partialModel = loadPartialModel(inputs)
36// val queries = loadQueries(metamodel)
37
38 println("DSL loaded")
39
40 val Ecore2Logic ecore2Logic = new Ecore2Logic
41 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
42 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
43 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
44
45 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())
46// val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel)
47// val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration)
48
49 val logicProblem = modelGenerationProblem.output
50// val logicProblem = modelExtensionProblem.output
51// val logicProblem = validModelExtensionProblem.output
52
53
54 println("Problem created")
55
56 var LogicResult solution
57 var LogicReasoner reasoner
58 //*
59 reasoner = new VampireSolver
60 val vampireConfig = new VampireSolverConfiguration => [
61 //add configuration things, in config file first
62 it.writeToFile = false
63 ]
64
65 solution = reasoner.solve(logicProblem, vampireConfig, workspace)
66
67 println("Problem solved")
68
69
70 }
71
72 def private static loadMetamodel() {
73 //FAM
74 val pckg = FunctionalarchitecturePackage.eINSTANCE
75 val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList
76 val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList
77 val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList
78 val List<EReference> references = classes.map[getEReferences].flatten.toList
79 val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList
80 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)
81 }
82
83 def private static loadPartialModel(ReasonerWorkspace inputs) {
84 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());
85 inputs.readModel(EObject,"FunctionalArchitectureModel.xmi").eResource.allContents.toList
86// inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList
87 }
88
89// def private static loadQueries(EcoreMetamodelDescriptor metamodel) {
90// val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance
91// val patterns = i.specifications.toList
92// val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
93// val derivedFeatures = new LinkedHashMap
94// derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head)
95// derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head)
96// val res = new ViatraQuerySetDescriptor(
97// patterns,
98// wfPatterns,
99// derivedFeatures
100// )
101// return res
102// }
103}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend
new file mode 100644
index 00000000..ccc17617
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend
@@ -0,0 +1,76 @@
1package ca.mcgill.ecse.dslreasoner.vampire.test
2
3import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
4import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
7import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
9import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
10import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
11import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
14import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
15import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
16import java.util.Collections
17import org.eclipse.emf.common.util.URI
18import org.eclipse.emf.ecore.resource.Resource
19import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
20import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
21
22class MedicalSystem {
23 def static void main(String[] args) {
24 init()
25 val workspace = new FileSystemWorkspace('''outputModels/''',"")
26 workspace.initAndClear
27 val root = load()
28 println("Problem Loaded")
29
30// val rs = new ResourceSetImpl
31// val logRes = rs.createResource(URI.createFileURI("vampireMidel.tptp"))
32//
33// var vampireModel = VampireLanguageFactory.eINSTANCE.createVampireModel()
34
35
36
37 var LogicResult solution
38 var LogicReasoner reasoner
39
40 reasoner = new VampireSolver
41 val vampireConfig = new VampireSolverConfiguration => [
42 //add configuration things, in config file first
43 it.writeToFile = false
44 ]
45
46 solution = reasoner.solve(root, vampireConfig, workspace)
47
48// vampireModel = solution
49//
50// logRes.contents.add(vampireModel)
51// logRes.save(Collections.EMPTY_MAP)
52
53
54 println("Problem Solved")
55
56 }
57
58 protected def static LogicProblem load() {
59 val resourceSet = new ResourceSetImpl
60 val resource = resourceSet.getResource(URI.createURI("inputLPs/newMedicalSystem.logicproblem"),true)
61 val root = resource.contents.get(0) as LogicProblem
62 root
63 }
64
65 protected def static void init() {
66 LogiclanguagePackage.eINSTANCE.eClass
67 LogicproblemPackage.eINSTANCE.eClass()
68 Ecore2logicannotationsPackage.eINSTANCE.eClass()
69 Viatra2LogicAnnotationsPackage.eINSTANCE.eClass()
70 val reg = Resource.Factory.Registry.INSTANCE
71 val map = reg.extensionToFactoryMap
72 map.put("logicproblem", new XMIResourceFactoryImpl)
73 map.put("tptp", new XMIResourceFactoryImpl)
74 VampireLanguageStandaloneSetup.doSetup
75 }
76}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend
index feb28dd5..9d2235f0 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend
@@ -1,176 +1,130 @@
1//package ca.mcgill.ecse.dslreasoner.vampire.test 1//package ca.mcgill.ecse.dslreasoner.vampire.test
2// 2//
3//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
4//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
5//import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage
6//import hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern
7//import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
8//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
9//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
10//import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
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.viatra2logic.ViatraQuerySetDescriptor
14//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
15//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
16//import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 3//import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
17//import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 4//import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage
18//import java.util.LinkedHashMap
19//import java.util.List 5//import java.util.List
20//import org.eclipse.emf.ecore.EAttribute
21//import org.eclipse.emf.ecore.EClass 6//import org.eclipse.emf.ecore.EClass
22//import org.eclipse.emf.ecore.EEnum
23//import org.eclipse.emf.ecore.EEnumLiteral 7//import org.eclipse.emf.ecore.EEnumLiteral
24//import org.eclipse.emf.ecore.EObject
25//import org.eclipse.emf.ecore.EReference 8//import org.eclipse.emf.ecore.EReference
9//import org.eclipse.emf.ecore.EEnum
10//import org.eclipse.emf.ecore.EAttribute
11//import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
12//import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
13//import org.eclipse.emf.ecore.EObject
14//import java.util.LinkedHashMap
15//import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
16//import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
17//import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
18//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19//import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
20//import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
21//import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
22//import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
23//import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
24//import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
25//import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
26//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
27//import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
26//import org.eclipse.emf.ecore.resource.Resource 28//import org.eclipse.emf.ecore.resource.Resource
27//import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 29//import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
30//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
31//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
32//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
33//import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
34//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
35//import java.util.LinkedList
36//import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
37//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicStructureBuilder
38//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
28// 39//
29//class SimpleRun { 40//class SimpleRun {
30// 41//
31// def static void main(String[] args) { 42// def static void main(String[] args) {
32// val inputs = new FileSystemWorkspace('''initialModels/''', "") 43// val inputs = new FileSystemWorkspace('''initialModels/''',"")
33// val workspace = new FileSystemWorkspace('''outputModels/''', "") 44// val workspace = new FileSystemWorkspace('''outputModels/''',"")
34// workspace.initAndClear 45// workspace.initAndClear
35////
36//// println("Input and output workspaces are created")
37////
38//// val metamodel = loadMetamodel()
39//// val partialModel = loadPartialModel(inputs)
40//// val queries = loadQueries(metamodel)
41////
42//// println("DSL loaded")
43////
44//// val Ecore2Logic ecore2Logic = new Ecore2Logic
45//// val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
46//// val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
47//// val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
48////
49//// val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())
50//// val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel)
51//// val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration)
52////
53//// val logicProblem = validModelExtensionProblem.output
54//// //*************xmi.save. advntageous cuz seperate and only contains things that are necessary
55//// //Write to file. This is importnat to understand
56//// //furthermore, output solution1.partialInterpretation contains also the logic probelm
57//// //that needs to be solved
58////
59//// //Logic problem same for vamp,l alloy, viatra. but fr alloy, vamp, it is mapped into the specific ecore metamodel using the xtext.
60//// //initial simple example: take one thing (ex. iff) from the logic problem generated for one of the sample examples, try to make it into vampire
61//// //xtext (but only the instance model, not the lines of code) to see how mapping will work. Then ishteh use vampire on it to "solve" it.
62// // create logic problem
63// var extension builder = new LogicProblemBuilder
64// var LogicProblem problem = builder.createProblem
65//
66// val rock = Element("Rock")
67// val paper = Element("Paper")
68// val scissor = Element("Scissor")
69//
70// problem.elements += rock
71// problem.elements += paper
72// problem.elements += scissor
73//
74//// val red = Element("Red")
75//// val green = Element("Green")
76////
77//// problem.elements += red
78//// problem.elements += green
79//
80//// val allRPS = problem.add(TypeDeclaration("allRPS", true))
81// val oldRPS = problem.add(TypeDefinition("oldRPS", false, rock, paper, scissor)) // n+1 axioms, where n is the number of type definitions. 1. rocjk, paper, scissor are all rps. 2. every object is rps
82//// val newRPS = problem.add(TypeDeclaration("newRPS", false))
83//// val color = problem.add(TypeDefinition("color", false, red, green))
84//// Supertype(oldRPS, allRPS)
85//// Supertype(newRPS, allRPS)
86// 46//
87// val beats2 = problem.add(RelationDeclaration("beats2", oldRPS, oldRPS)) 47// println("Input and output workspaces are created")
88// problem.add(Assertion(Forall[ 48//
89// val x = addVar("x", oldRPS) 49// val metamodel = loadMetamodel()
90// // x.range 50// val partialModel = loadPartialModel(inputs)
91// Exists[ 51// val queries = loadQueries(metamodel)
92// val y = addVar("y", oldRPS) 52//
93// beats2.call(x, y) 53// println("DSL loaded")
94// ] 54//
95// ])) 55// val Ecore2Logic ecore2Logic = new Ecore2Logic
96// 56// val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
97//// val beats = problem.add(RelationDefinition("beats",[ 57// val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
98//// val x = addVar("x",RPS) 58// val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
99//// val y = addVar("y",RPS) 59//
100//// (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock) 60// val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())
101//// ])) 61// val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel)
102//// 62// val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration)
103//// //below needs to be added as an axiom 63//
104//// val beats2 = problem.add(RelationDeclaration("beats2",RPS,RPS)) 64// val logicProblem = validModelExtensionProblem.output
105//// problem.add(Assertion(Forall[ 65//
106//// val x = addVar("x",RPS)
107//// Exists[
108//// val y = addVar("y",RPS)
109//// beats2.call(x,y)
110//// ]
111//// ]))
112// println("Problem created") 66// println("Problem created")
113// var LogicResult solution 67// var LogicResult solution
114// var LogicReasoner reasoner 68// var LogicReasoner reasoner
115// /* 69// //*
116// * reasoner = new ViatraReasoner 70// reasoner = new ViatraReasoner
117// * val viatraConfig = new ViatraReasonerConfiguration => [ 71// val viatraConfig = new ViatraReasonerConfiguration => [
118// * it.typeScopes.maxNewElements = 5 72// it.typeScopes.maxNewElements = 40
119// * it.typeScopes.minNewElements = 5 73// it.typeScopes.minNewElements = 40
120// * it.solutionScope.numberOfRequiredSolution = 1
121// * it.existingQueries = queries.patterns.map[it.internalQueryRepresentation]
122// * it.debugCongiguration.logging = false
123// * it.debugCongiguration.partalInterpretationVisualisationFrequency = 1
124// * it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation
125// * ]
126// * solution = reasoner.solve(logicProblem,viatraConfig,workspace)
127// /*/
128// reasoner = new AlloySolver
129// val alloyConfig = new AlloySolverConfiguration => [
130// it.typeScopes.maxNewElements = 5
131// it.typeScopes.minNewElements = 5
132// it.solutionScope.numberOfRequiredSolution = 1 74// it.solutionScope.numberOfRequiredSolution = 1
133// it.typeScopes.maxNewIntegers = 0 75// it.existingQueries = queries.patterns.map[it.internalQueryRepresentation]
134// it.writeToFile = false 76// it.debugCongiguration.logging = false
77// it.debugCongiguration.partalInterpretationVisualisationFrequency = 1
78// it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation
135// ] 79// ]
136// solution = reasoner.solve(problem, alloyConfig, workspace) 80// solution = reasoner.solve(logicProblem,viatraConfig,workspace)
137// // */ 81// /*/
138// // ************ 82// reasoner = new AlloySolver
139// // since input logic model is also output, we can check out what is the input for alloy and then 83// val alloyConfig = new AlloySolverConfiguration => [
140// // see what should be input for vampire, as it should be similar to alloy. once i can create the input, 84// it.typeScopes.maxNewElements = 5
141// // that is the first step. 85// it.typeScopes.minNewElements = 5
142// // look at allo2logic 86// it.solutionScope.numberOfRequiredSolution = 1
143// // always keep looking at output 87// it.typeScopes.maxNewIntegers = 0
144// // try to figure out what rule is used 88// it.writeToFile = true
145// println("Problem solved") 89// ]
146// 90// solution = reasoner.solve(logicProblem,alloyConfig,workspace)
147//// val interpretations = reasoner.getInterpretations(solution as ModelResult) 91// //*/
148//// val models = new LinkedList 92//
149//// for(interpretation : interpretations) { 93// println("Problem solved")= ^
150//// val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) 94//
151//// models+=instanceModel 95//
152//// } 96// val interpretations = reasoner.getInterpretations(solution as ModelResult)
153//// 97// val models = new LinkedList
154//// solution.writeSolution(workspace, #[]) 98// for(interpretation : interpretations) {
99// val extension b = new LogicStructureBuilder
100// val extension a = new LogicProblemBuilder
101//
102//
103//
104// val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace)
105// models+=instanceModel
106// }
107//
108// solution.writeSolution(workspace, #[])
155// } 109// }
156// 110//
157// def private static loadMetamodel() { 111// def private static loadMetamodel() {
158// val pckg = FunctionalArchitecturePackage.eINSTANCE 112// val pckg = FunctionalArchitecturePackage.eINSTANCE
159// val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList 113// val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList
160// val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList 114// val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList
161// val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 115// val List<EEnumLiteral> literals = enums.map[getELiterals].flatten.toList
162// val List<EReference> references = classes.map[EReferences].flatten.toList 116// val List<EReference> references = classes.map[getEReferences].flatten.toList
163// val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList 117// val List<EAttribute> attributes = classes.map[getEAttributes].flatten.toList
164// return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) 118// return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes)
165// } 119// }
166// 120//
167// def private static loadQueries(EcoreMetamodelDescriptor metamodel) { 121// def private static loadQueries(EcoreMetamodelDescriptor metamodel) {
168// val i = Pattern.instance 122// val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance
169// val patterns = i.specifications.toList 123// val patterns = i.specifications.toList
170// val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet 124// val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
171// val derivedFeatures = new LinkedHashMap 125// val derivedFeatures = new LinkedHashMap
172// derivedFeatures.put(i.type.internalQueryRepresentation, metamodel.attributes.filter[it.name == "type"].head) 126// derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head)
173// derivedFeatures.put(i.model.internalQueryRepresentation, metamodel.references.filter[it.name == "model"].head) 127// derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head)
174// val res = new ViatraQuerySetDescriptor( 128// val res = new ViatraQuerySetDescriptor(
175// patterns, 129// patterns,
176// wfPatterns, 130// wfPatterns,
@@ -178,36 +132,37 @@
178// ) 132// )
179// return res 133// return res
180// } 134// }
181// 135//
182// def static loadPartialModel(ReasonerWorkspace inputs) { 136// def static loadPartialModel(ReasonerWorkspace inputs) {
183// Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); 137// Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());
184// inputs.readModel(EObject, "FAM.xmi").eResource.allContents.toList 138// inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList
185// } 139// }
186// 140//
187// def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List<EObject> models) { 141// def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List<EObject> models) {
188// if (solution instanceof ModelResult) { 142// if(solution instanceof ModelResult) {
189// val representations = solution.representation 143// val representations = solution.representation
190// for (representationIndex : 0 ..< representations.size) { 144// for(representationIndex : 0..<representations.size) {
191// val representation = representations.get(representationIndex) 145// val representation = representations.get(representationIndex)
192// val representationNumber = representationIndex + 1 146// val representationNumber = representationIndex + 1
193// if (representation instanceof PartialInterpretation) { 147// if(representation instanceof PartialInterpretation) {
194// workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') 148// workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
195// val partialInterpretation2GML = new PartialInterpretation2Gml 149// val partialInterpretation2GML = new PartialInterpretation2Gml
196// val gml = partialInterpretation2GML.transform(representation) 150// val gml = partialInterpretation2GML.transform(representation)
197// // ecore2GML.transform(root) 151// //ecore2GML.transform(root)
198// workspace.writeText('''solutionVisualisation.gml''', gml) 152// workspace.writeText('''solutionVisualisation.gml''',gml)
199// 153//
200// } else { 154// } else {
201// workspace.writeText('''solution«representationNumber».txt''', representation.toString) 155// workspace.writeText('''solution«representationNumber».txt''',representation.toString)
202// } 156// }
203// } 157// }
204// for (model : models) { 158// for(model : models) {
205// workspace.writeModel(model, "model.xmi") 159// workspace.writeModel(model,"model.xmi")
206// } 160// }
207// println("Solution saved and visualised") 161// println("Solution saved and visualised")
208// } 162// }
209// } 163// }
210// 164//
211// def static visualizeSolution() { 165// def static visualizeSolution() {
166//
212// } 167// }
213//} 168//}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
index 64914fd0..3d36bbf7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
@@ -50,7 +50,7 @@ class VampireTest {
50 50
51 var LogicProblem problem = builder.createProblem 51 var LogicProblem problem = builder.createProblem
52 52
53 //* 53 /*
54 deMorgan(problem) 54 deMorgan(problem)
55 /*/ 55 /*/
56 rockPaperScisors(problem) 56 rockPaperScisors(problem)
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 03:00:39 +0000