aboutsummaryrefslogtreecommitdiffstats
path: root/Tests
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-01-15 12:44:33 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-01-15 12:44:33 -0500
commit20f131a3f09edf8e1455f20b4f486629147e7eff (patch)
tree690ee30b62caf76bdc7d45f183382965e4e7bf05 /Tests
parentViatraSolver as default (diff)
downloadVIATRA-Generator-20f131a3f09edf8e1455f20b4f486629147e7eff.tar.gz
VIATRA-Generator-20f131a3f09edf8e1455f20b4f486629147e7eff.tar.zst
VIATRA-Generator-20f131a3f09edf8e1455f20b4f486629147e7eff.zip
Initial workspace setup
Diffstat (limited to 'Tests')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath8
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore1
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project34
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs7
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF20
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties4
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi3
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi4
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi6
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi3
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem27
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp1
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend213
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend153
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbinbin0 -> 687 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbinbin0 -> 6302 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore2
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java140
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 @@
1eclipse.preferences.version=1
2org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
3org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
4org.eclipse.jdt.core.compiler.compliance=1.8
5org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
6org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
7org.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 @@
1Manifest-Version: 1.0
2Bundle-ManifestVersion: 2
3Bundle-Name: Test
4Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test
5Bundle-Version: 1.0.0.qualifier
6Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test
7Bundle-RequiredExecutionEnvironment: JavaSE-1.8
8Require-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 @@
1source.. = src/
2output.. = bin/
3bin.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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.test
2
3
4import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
5import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
11import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
12import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
13import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
14import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import java.util.Collections
16import org.eclipse.emf.common.util.URI
17import org.eclipse.emf.ecore.resource.Resource
18import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
20
21class 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.test;
2
3import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage;
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder;
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext;
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And;
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion;
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration;
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists;
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff;
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
23import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
25import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
26import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage;
27import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
28import java.util.Collections;
29import java.util.Map;
30import org.eclipse.emf.common.util.EList;
31import org.eclipse.emf.common.util.URI;
32import org.eclipse.emf.ecore.resource.Resource;
33import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;
34import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
35import org.eclipse.xtend2.lib.StringConcatenation;
36import org.eclipse.xtext.xbase.lib.Exceptions;
37import org.eclipse.xtext.xbase.lib.Extension;
38import org.eclipse.xtext.xbase.lib.Functions.Function1;
39import org.eclipse.xtext.xbase.lib.InputOutput;
40import org.eclipse.xtext.xbase.lib.ObjectExtensions;
41import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
42
43@SuppressWarnings("all")
44public 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:36:37 +0000