diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
18 files changed, 626 insertions, 0 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath new file mode 100644 index 00000000..1c96fe2f --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath | |||
@@ -0,0 +1,8 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <classpath> | ||
3 | <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/> | ||
4 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | ||
5 | <classpathentry kind="src" path="src"/> | ||
6 | <classpathentry kind="src" path="xtend-gen"/> | ||
7 | <classpathentry kind="output" path="bin"/> | ||
8 | </classpath> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore | |||
@@ -0,0 +1 @@ | |||
/bin/ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project new file mode 100644 index 00000000..eb3347d0 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project | |||
@@ -0,0 +1,34 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <projectDescription> | ||
3 | <name>ca.mcgill.ecse.dslreasoner.vampire.test</name> | ||
4 | <comment></comment> | ||
5 | <projects> | ||
6 | </projects> | ||
7 | <buildSpec> | ||
8 | <buildCommand> | ||
9 | <name>org.eclipse.xtext.ui.shared.xtextBuilder</name> | ||
10 | <arguments> | ||
11 | </arguments> | ||
12 | </buildCommand> | ||
13 | <buildCommand> | ||
14 | <name>org.eclipse.jdt.core.javabuilder</name> | ||
15 | <arguments> | ||
16 | </arguments> | ||
17 | </buildCommand> | ||
18 | <buildCommand> | ||
19 | <name>org.eclipse.pde.ManifestBuilder</name> | ||
20 | <arguments> | ||
21 | </arguments> | ||
22 | </buildCommand> | ||
23 | <buildCommand> | ||
24 | <name>org.eclipse.pde.SchemaBuilder</name> | ||
25 | <arguments> | ||
26 | </arguments> | ||
27 | </buildCommand> | ||
28 | </buildSpec> | ||
29 | <natures> | ||
30 | <nature>org.eclipse.pde.PluginNature</nature> | ||
31 | <nature>org.eclipse.jdt.core.javanature</nature> | ||
32 | <nature>org.eclipse.xtext.ui.shared.xtextNature</nature> | ||
33 | </natures> | ||
34 | </projectDescription> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs | |||
@@ -0,0 +1,7 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled | ||
3 | org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 | ||
4 | org.eclipse.jdt.core.compiler.compliance=1.8 | ||
5 | org.eclipse.jdt.core.compiler.problem.assertIdentifier=error | ||
6 | org.eclipse.jdt.core.compiler.problem.enumIdentifier=error | ||
7 | org.eclipse.jdt.core.compiler.source=1.8 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF new file mode 100644 index 00000000..13fcb7b9 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF | |||
@@ -0,0 +1,20 @@ | |||
1 | Manifest-Version: 1.0 | ||
2 | Bundle-ManifestVersion: 2 | ||
3 | Bundle-Name: Test | ||
4 | Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test | ||
5 | Bundle-Version: 1.0.0.qualifier | ||
6 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test | ||
7 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | ||
8 | Require-Bundle: com.google.guava, | ||
9 | org.eclipse.xtext.xbase.lib, | ||
10 | org.eclipse.xtend.lib, | ||
11 | org.eclipse.xtend.lib.macro, | ||
12 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", | ||
13 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | ||
14 | ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", | ||
15 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | ||
16 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", | ||
17 | org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", | ||
18 | hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", | ||
19 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0" | ||
20 | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties new file mode 100644 index 00000000..41eb6ade --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties | |||
@@ -0,0 +1,4 @@ | |||
1 | source.. = src/ | ||
2 | output.. = bin/ | ||
3 | bin.includes = META-INF/,\ | ||
4 | . | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi new file mode 100644 index 00000000..c79e58ed --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi | |||
@@ -0,0 +1,3 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <fam:FunctionalArchitectureModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" | ||
3 | xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:fam="FAM" xsi:schemaLocation="FAM FAM.ecore"/> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi new file mode 100644 index 00000000..49b1f89d --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi | |||
@@ -0,0 +1,4 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <hu.bme.mit.inf.yakindumm:Statechart xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" | ||
3 | xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:hu.bme.mit.inf.yakindumm="hu.bme.mit.inf.yakindumm" | ||
4 | xsi:schemaLocation="hu.bme.mit.inf.yakindumm yakindu_simplified.ecore"/> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi new file mode 100644 index 00000000..867e5049 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi | |||
@@ -0,0 +1,6 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <ecore:EPackage | ||
3 | xmi:version="2.0" | ||
4 | xmlns:xmi="http://www.omg.org/XMI" | ||
5 | xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" | ||
6 | name="init"/> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi new file mode 100644 index 00000000..56879c1a --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi | |||
@@ -0,0 +1,3 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <FS:Model xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
3 | xmlns:FS="FS" xsi:schemaLocation="FS FileSytem.ecore"/> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem new file mode 100644 index 00000000..f5f90f38 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem | |||
@@ -0,0 +1,27 @@ | |||
1 | <?xml version="1.0" encoding="ASCII"?> | ||
2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"> | ||
3 | <assertions name="assertion1"> | ||
4 | <value xsi:type="language_1:Iff"> | ||
5 | <leftOperand xsi:type="language_1:Not"> | ||
6 | <operand xsi:type="language_1:And"> | ||
7 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@constants.0"/> | ||
8 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@constants.1"/> | ||
9 | </operand> | ||
10 | </leftOperand> | ||
11 | <rightOperand xsi:type="language_1:Or"> | ||
12 | <operands xsi:type="language_1:Not"> | ||
13 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@constants.0"/> | ||
14 | </operands> | ||
15 | <operands xsi:type="language_1:Not"> | ||
16 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@constants.1"/> | ||
17 | </operands> | ||
18 | </rightOperand> | ||
19 | </value> | ||
20 | </assertions> | ||
21 | <constants xsi:type="language_1:ConstantDeclaration" name="constant1"> | ||
22 | <type xsi:type="language_1:BoolTypeReference"/> | ||
23 | </constants> | ||
24 | <constants xsi:type="language_1:ConstantDeclaration" name="constant2"> | ||
25 | <type xsi:type="language_1:BoolTypeReference"/> | ||
26 | </constants> | ||
27 | </language:LogicProblem> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp new file mode 100644 index 00000000..ddeec4f4 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp | |||
@@ -0,0 +1 @@ | |||
%This is an initial Test Comment fof ( assertion1 , axiom , ~ ( constant1 & constant2 ) <=> ( ~ constant1 | ~ constant2 ) ) . | |||
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 new file mode 100644 index 00000000..feb28dd5 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend | |||
@@ -0,0 +1,213 @@ | |||
1 | //package ca.mcgill.ecse.dslreasoner.vampire.test | ||
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 | ||
17 | //import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
18 | //import java.util.LinkedHashMap | ||
19 | //import java.util.List | ||
20 | //import org.eclipse.emf.ecore.EAttribute | ||
21 | //import org.eclipse.emf.ecore.EClass | ||
22 | //import org.eclipse.emf.ecore.EEnum | ||
23 | //import org.eclipse.emf.ecore.EEnumLiteral | ||
24 | //import org.eclipse.emf.ecore.EObject | ||
25 | //import org.eclipse.emf.ecore.EReference | ||
26 | //import org.eclipse.emf.ecore.resource.Resource | ||
27 | //import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
28 | // | ||
29 | //class SimpleRun { | ||
30 | // | ||
31 | // def static void main(String[] args) { | ||
32 | // val inputs = new FileSystemWorkspace('''initialModels/''', "") | ||
33 | // val workspace = new FileSystemWorkspace('''outputModels/''', "") | ||
34 | // 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 | // | ||
87 | // val beats2 = problem.add(RelationDeclaration("beats2", oldRPS, oldRPS)) | ||
88 | // problem.add(Assertion(Forall[ | ||
89 | // val x = addVar("x", oldRPS) | ||
90 | // // x.range | ||
91 | // Exists[ | ||
92 | // val y = addVar("y", oldRPS) | ||
93 | // beats2.call(x, y) | ||
94 | // ] | ||
95 | // ])) | ||
96 | // | ||
97 | //// val beats = problem.add(RelationDefinition("beats",[ | ||
98 | //// val x = addVar("x",RPS) | ||
99 | //// val y = addVar("y",RPS) | ||
100 | //// (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock) | ||
101 | //// ])) | ||
102 | //// | ||
103 | //// //below needs to be added as an axiom | ||
104 | //// val beats2 = problem.add(RelationDeclaration("beats2",RPS,RPS)) | ||
105 | //// problem.add(Assertion(Forall[ | ||
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") | ||
113 | // var LogicResult solution | ||
114 | // var LogicReasoner reasoner | ||
115 | // /* | ||
116 | // * reasoner = new ViatraReasoner | ||
117 | // * val viatraConfig = new ViatraReasonerConfiguration => [ | ||
118 | // * it.typeScopes.maxNewElements = 5 | ||
119 | // * it.typeScopes.minNewElements = 5 | ||
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 | ||
133 | // it.typeScopes.maxNewIntegers = 0 | ||
134 | // it.writeToFile = false | ||
135 | // ] | ||
136 | // solution = reasoner.solve(problem, alloyConfig, workspace) | ||
137 | // // */ | ||
138 | // // ************ | ||
139 | // // since input logic model is also output, we can check out what is the input for alloy and then | ||
140 | // // see what should be input for vampire, as it should be similar to alloy. once i can create the input, | ||
141 | // // that is the first step. | ||
142 | // // look at allo2logic | ||
143 | // // always keep looking at output | ||
144 | // // try to figure out what rule is used | ||
145 | // println("Problem solved") | ||
146 | // | ||
147 | //// val interpretations = reasoner.getInterpretations(solution as ModelResult) | ||
148 | //// val models = new LinkedList | ||
149 | //// for(interpretation : interpretations) { | ||
150 | //// val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) | ||
151 | //// models+=instanceModel | ||
152 | //// } | ||
153 | //// | ||
154 | //// solution.writeSolution(workspace, #[]) | ||
155 | // } | ||
156 | // | ||
157 | // def private static loadMetamodel() { | ||
158 | // val pckg = FunctionalArchitecturePackage.eINSTANCE | ||
159 | // val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList | ||
160 | // val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList | ||
161 | // val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList | ||
162 | // val List<EReference> references = classes.map[EReferences].flatten.toList | ||
163 | // val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList | ||
164 | // return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) | ||
165 | // } | ||
166 | // | ||
167 | // def private static loadQueries(EcoreMetamodelDescriptor metamodel) { | ||
168 | // val i = Pattern.instance | ||
169 | // val patterns = i.specifications.toList | ||
170 | // val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet | ||
171 | // val derivedFeatures = new LinkedHashMap | ||
172 | // derivedFeatures.put(i.type.internalQueryRepresentation, metamodel.attributes.filter[it.name == "type"].head) | ||
173 | // derivedFeatures.put(i.model.internalQueryRepresentation, metamodel.references.filter[it.name == "model"].head) | ||
174 | // val res = new ViatraQuerySetDescriptor( | ||
175 | // patterns, | ||
176 | // wfPatterns, | ||
177 | // derivedFeatures | ||
178 | // ) | ||
179 | // return res | ||
180 | // } | ||
181 | // | ||
182 | // def static loadPartialModel(ReasonerWorkspace inputs) { | ||
183 | // Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | ||
184 | // inputs.readModel(EObject, "FAM.xmi").eResource.allContents.toList | ||
185 | // } | ||
186 | // | ||
187 | // def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List<EObject> models) { | ||
188 | // if (solution instanceof ModelResult) { | ||
189 | // val representations = solution.representation | ||
190 | // for (representationIndex : 0 ..< representations.size) { | ||
191 | // val representation = representations.get(representationIndex) | ||
192 | // val representationNumber = representationIndex + 1 | ||
193 | // if (representation instanceof PartialInterpretation) { | ||
194 | // workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') | ||
195 | // val partialInterpretation2GML = new PartialInterpretation2Gml | ||
196 | // val gml = partialInterpretation2GML.transform(representation) | ||
197 | // // ecore2GML.transform(root) | ||
198 | // workspace.writeText('''solutionVisualisation.gml''', gml) | ||
199 | // | ||
200 | // } else { | ||
201 | // workspace.writeText('''solution«representationNumber».txt''', representation.toString) | ||
202 | // } | ||
203 | // } | ||
204 | // for (model : models) { | ||
205 | // workspace.writeModel(model, "model.xmi") | ||
206 | // } | ||
207 | // println("Solution saved and visualised") | ||
208 | // } | ||
209 | // } | ||
210 | // | ||
211 | // def static visualizeSolution() { | ||
212 | // } | ||
213 | //} | ||
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 new file mode 100644 index 00000000..64914fd0 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend | |||
@@ -0,0 +1,153 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test | ||
2 | |||
3 | |||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
11 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | ||
12 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
13 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
14 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
15 | import java.util.Collections | ||
16 | import org.eclipse.emf.common.util.URI | ||
17 | import org.eclipse.emf.ecore.resource.Resource | ||
18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | ||
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
20 | |||
21 | class VampireTest { | ||
22 | |||
23 | val static extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
24 | |||
25 | def static void main(String[] args) { | ||
26 | // val inputs = new FileSystemWorkspace('''initialModels/''',"") | ||
27 | |||
28 | |||
29 | //create logic problem | ||
30 | //var LogicProblem problem = builder.createProblem | ||
31 | |||
32 | |||
33 | |||
34 | LogicproblemPackage.eINSTANCE.eClass() | ||
35 | Ecore2logicannotationsPackage.eINSTANCE.eClass() | ||
36 | Viatra2LogicAnnotationsPackage.eINSTANCE.eClass() | ||
37 | val reg = Resource.Factory.Registry.INSTANCE | ||
38 | val map = reg.extensionToFactoryMap | ||
39 | map.put("logicproblem", new XMIResourceFactoryImpl) | ||
40 | VampireLanguageStandaloneSetup.doSetup | ||
41 | |||
42 | val workspace = new FileSystemWorkspace('''output/models/''',"") | ||
43 | workspace.initAndClear | ||
44 | |||
45 | // Load and create top level elements | ||
46 | // Load source model | ||
47 | val rs = new ResourceSetImpl | ||
48 | val logicURI = URI.createFileURI("output/files/logProb.logicproblem") | ||
49 | val logRes = rs.createResource(logicURI) | ||
50 | |||
51 | var LogicProblem problem = builder.createProblem | ||
52 | |||
53 | //* | ||
54 | deMorgan(problem) | ||
55 | /*/ | ||
56 | rockPaperScisors(problem) | ||
57 | //*/ | ||
58 | |||
59 | logRes.contents.add(problem) | ||
60 | logRes.save(Collections.EMPTY_MAP) | ||
61 | |||
62 | //problem.add(Assertion( Y && X <=> X) ) | ||
63 | |||
64 | println("Problem Created"); | ||
65 | |||
66 | var LogicResult solution | ||
67 | var LogicReasoner reasoner | ||
68 | |||
69 | reasoner = new VampireSolver | ||
70 | val vampireConfig = new VampireSolverConfiguration => [ | ||
71 | //add configuration things, in config file first | ||
72 | it.writeToFile = false | ||
73 | ] | ||
74 | |||
75 | solution = reasoner.solve(problem, vampireConfig, workspace) | ||
76 | |||
77 | // if(solution instanceof ModelResult) { | ||
78 | // reasoner.getInterpretations(solution) | ||
79 | // } | ||
80 | //^can extract everything (ex, vars) from solver | ||
81 | |||
82 | |||
83 | //call the solver | ||
84 | |||
85 | println("Problem Solved") | ||
86 | |||
87 | //output solution | ||
88 | |||
89 | } | ||
90 | |||
91 | static def deMorgan(LogicProblem problem) { | ||
92 | |||
93 | |||
94 | var X = ConstantDeclaration(LogicBool) | ||
95 | var Y = ConstantDeclaration(LogicBool) | ||
96 | problem.add(X) | ||
97 | problem.add(Y) | ||
98 | |||
99 | //assertion is negated manually because logic problem can only handle axioms (assertions) | ||
100 | //so ya | ||
101 | problem.add(Assertion( !(X && Y) <=> ( !X || !Y)) ) | ||
102 | } | ||
103 | |||
104 | static def rockPaperScisors(LogicProblem problem) { | ||
105 | |||
106 | val rock = Element("Rock") | ||
107 | val paper= Element("Paper") | ||
108 | val scissor = Element("Scissor") | ||
109 | |||
110 | problem.elements += rock | ||
111 | problem.elements += paper | ||
112 | problem.elements += scissor | ||
113 | |||
114 | // val red = Element("Red") | ||
115 | // val green = Element("Green") | ||
116 | // | ||
117 | // problem.elements += red | ||
118 | // problem.elements += green | ||
119 | |||
120 | |||
121 | //val allRPS = problem.add(TypeDeclaration("allRPS", true)) | ||
122 | //val newRPS = problem.add(TypeDeclaration("newRPS", false)) | ||
123 | 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 | ||
124 | |||
125 | // val color = problem.add(TypeDefinition("color", false, red, green )) | ||
126 | //Supertype(oldRPS,allRPS) | ||
127 | //Supertype(newRPS,oldRPS) | ||
128 | |||
129 | |||
130 | |||
131 | |||
132 | /* Remains | ||
133 | val beats = problem.add(RelationDefinition("beats",[ | ||
134 | val x = addVar("x",oldRPS) | ||
135 | val y = addVar("y",oldRPS) | ||
136 | (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock) | ||
137 | ])) | ||
138 | |||
139 | /*/ | ||
140 | //below needs to be added as an axiom | ||
141 | val beats2 = problem.add(RelationDeclaration("beats2",oldRPS,oldRPS)) | ||
142 | problem.add(Assertion(Forall[ | ||
143 | val x = addVar("x",oldRPS) | ||
144 | //x.range | ||
145 | Exists[ | ||
146 | val y = addVar("y",oldRPS) | ||
147 | beats2.call(x,y) | ||
148 | ] | ||
149 | ])) | ||
150 | //*/ | ||
151 | |||
152 | } | ||
153 | } \ No newline at end of file | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin new file mode 100644 index 00000000..b60ffe4c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin new file mode 100644 index 00000000..881f927c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore new file mode 100644 index 00000000..f3c47b99 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore | |||
@@ -0,0 +1,2 @@ | |||
1 | /.VampireTest.java._trace | ||
2 | /.SimpleRun.java._trace | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java new file mode 100644 index 00000000..73c413b3 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java | |||
@@ -0,0 +1,140 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
26 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage; | ||
27 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | ||
28 | import java.util.Collections; | ||
29 | import java.util.Map; | ||
30 | import org.eclipse.emf.common.util.EList; | ||
31 | import org.eclipse.emf.common.util.URI; | ||
32 | import org.eclipse.emf.ecore.resource.Resource; | ||
33 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; | ||
34 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | ||
35 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
37 | import org.eclipse.xtext.xbase.lib.Extension; | ||
38 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
42 | |||
43 | @SuppressWarnings("all") | ||
44 | public class VampireTest { | ||
45 | @Extension | ||
46 | private final static LogicProblemBuilder builder = new LogicProblemBuilder(); | ||
47 | |||
48 | public static void main(final String[] args) { | ||
49 | try { | ||
50 | LogicproblemPackage.eINSTANCE.eClass(); | ||
51 | Ecore2logicannotationsPackage.eINSTANCE.eClass(); | ||
52 | Viatra2LogicAnnotationsPackage.eINSTANCE.eClass(); | ||
53 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | ||
54 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); | ||
55 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); | ||
56 | map.put("logicproblem", _xMIResourceFactoryImpl); | ||
57 | VampireLanguageStandaloneSetup.doSetup(); | ||
58 | StringConcatenation _builder = new StringConcatenation(); | ||
59 | _builder.append("output/models/"); | ||
60 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); | ||
61 | workspace.initAndClear(); | ||
62 | final ResourceSetImpl rs = new ResourceSetImpl(); | ||
63 | final URI logicURI = URI.createFileURI("output/files/logProb.logicproblem"); | ||
64 | final Resource logRes = rs.createResource(logicURI); | ||
65 | LogicProblem problem = VampireTest.builder.createProblem(); | ||
66 | VampireTest.deMorgan(problem); | ||
67 | logRes.getContents().add(problem); | ||
68 | logRes.save(Collections.EMPTY_MAP); | ||
69 | InputOutput.<String>println("Problem Created"); | ||
70 | LogicResult solution = null; | ||
71 | LogicReasoner reasoner = null; | ||
72 | VampireSolver _vampireSolver = new VampireSolver(); | ||
73 | reasoner = _vampireSolver; | ||
74 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | ||
75 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | ||
76 | it.writeToFile = false; | ||
77 | }; | ||
78 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | ||
79 | solution = reasoner.solve(problem, vampireConfig, workspace); | ||
80 | InputOutput.<String>println("Problem Solved"); | ||
81 | } catch (Throwable _e) { | ||
82 | throw Exceptions.sneakyThrow(_e); | ||
83 | } | ||
84 | } | ||
85 | |||
86 | public static Assertion deMorgan(final LogicProblem problem) { | ||
87 | Assertion _xblockexpression = null; | ||
88 | { | ||
89 | ConstantDeclaration X = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); | ||
90 | ConstantDeclaration Y = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); | ||
91 | VampireTest.builder.add(problem, X); | ||
92 | VampireTest.builder.add(problem, Y); | ||
93 | And _and = VampireTest.builder.operator_and(X, Y); | ||
94 | Not _not = VampireTest.builder.operator_not(_and); | ||
95 | Not _not_1 = VampireTest.builder.operator_not(X); | ||
96 | Not _not_2 = VampireTest.builder.operator_not(Y); | ||
97 | Or _or = VampireTest.builder.operator_or(_not_1, _not_2); | ||
98 | Iff _spaceship = VampireTest.builder.operator_spaceship(_not, _or); | ||
99 | _xblockexpression = VampireTest.builder.add(problem, VampireTest.builder.Assertion(_spaceship)); | ||
100 | } | ||
101 | return _xblockexpression; | ||
102 | } | ||
103 | |||
104 | public static Assertion rockPaperScisors(final LogicProblem problem) { | ||
105 | Assertion _xblockexpression = null; | ||
106 | { | ||
107 | final DefinedElement rock = VampireTest.builder.Element("Rock"); | ||
108 | final DefinedElement paper = VampireTest.builder.Element("Paper"); | ||
109 | final DefinedElement scissor = VampireTest.builder.Element("Scissor"); | ||
110 | EList<DefinedElement> _elements = problem.getElements(); | ||
111 | _elements.add(rock); | ||
112 | EList<DefinedElement> _elements_1 = problem.getElements(); | ||
113 | _elements_1.add(paper); | ||
114 | EList<DefinedElement> _elements_2 = problem.getElements(); | ||
115 | _elements_2.add(scissor); | ||
116 | final Type oldRPS = VampireTest.builder.add(problem, VampireTest.builder.TypeDefinition("oldRPS", false, rock, paper, scissor)); | ||
117 | final Relation beats2 = VampireTest.builder.add(problem, VampireTest.builder.RelationDeclaration("beats2", oldRPS, oldRPS)); | ||
118 | final Function1<VariableContext, TermDescription> _function = (VariableContext it) -> { | ||
119 | Exists _xblockexpression_1 = null; | ||
120 | { | ||
121 | final Variable x = it.addVar("x", oldRPS); | ||
122 | final Function1<VariableContext, TermDescription> _function_1 = (VariableContext it_1) -> { | ||
123 | SymbolicValue _xblockexpression_2 = null; | ||
124 | { | ||
125 | final Variable y = it_1.addVar("y", oldRPS); | ||
126 | _xblockexpression_2 = VampireTest.builder.call(beats2, x, y); | ||
127 | } | ||
128 | return _xblockexpression_2; | ||
129 | }; | ||
130 | _xblockexpression_1 = VampireTest.builder.Exists(_function_1); | ||
131 | } | ||
132 | return _xblockexpression_1; | ||
133 | }; | ||
134 | _xblockexpression = VampireTest.builder.add(problem, | ||
135 | VampireTest.builder.Assertion( | ||
136 | VampireTest.builder.Forall(_function))); | ||
137 | } | ||
138 | return _xblockexpression; | ||
139 | } | ||
140 | } | ||