diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import functionalarchitecture.FunctionalarchitecturePackage | ||
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.ecore2logic.EcoreMetamodelDescriptor | ||
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.logic2ecore.Logic2Ecore | ||
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
16 | import java.util.List | ||
17 | import org.eclipse.emf.ecore.EAttribute | ||
18 | import org.eclipse.emf.ecore.EClass | ||
19 | import org.eclipse.emf.ecore.EEnum | ||
20 | import org.eclipse.emf.ecore.EEnumLiteral | ||
21 | import org.eclipse.emf.ecore.EObject | ||
22 | import org.eclipse.emf.ecore.EReference | ||
23 | import org.eclipse.emf.ecore.resource.Resource | ||
24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
25 | |||
26 | class 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
15 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
16 | import java.util.Collections | ||
17 | import org.eclipse.emf.common.util.URI | ||
18 | import org.eclipse.emf.ecore.resource.Resource | ||
19 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | ||
20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
21 | |||
22 | class 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) |