diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend | 25 |
1 files changed, 14 insertions, 11 deletions
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 3d36bbf7..4fc81ad8 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 | |||
@@ -17,6 +17,7 @@ import org.eclipse.emf.common.util.URI | |||
17 | import org.eclipse.emf.ecore.resource.Resource | 17 | import org.eclipse.emf.ecore.resource.Resource |
18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | 18 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl |
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
20 | import java.io.File | ||
20 | 21 | ||
21 | class VampireTest { | 22 | class VampireTest { |
22 | 23 | ||
@@ -39,15 +40,11 @@ class VampireTest { | |||
39 | map.put("logicproblem", new XMIResourceFactoryImpl) | 40 | map.put("logicproblem", new XMIResourceFactoryImpl) |
40 | VampireLanguageStandaloneSetup.doSetup | 41 | VampireLanguageStandaloneSetup.doSetup |
41 | 42 | ||
42 | val workspace = new FileSystemWorkspace('''output/models/''',"") | 43 | val workspace = new FileSystemWorkspace('''output/VampireTest''',"") |
43 | workspace.initAndClear | 44 | workspace.initAndClear |
44 | 45 | ||
45 | // Load and create top level elements | 46 | //Storing the logicProblem |
46 | // Load source model | 47 | val filename = "problem.logicproblem" |
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 | 48 | var LogicProblem problem = builder.createProblem |
52 | 49 | ||
53 | /* | 50 | /* |
@@ -56,8 +53,7 @@ class VampireTest { | |||
56 | rockPaperScisors(problem) | 53 | rockPaperScisors(problem) |
57 | //*/ | 54 | //*/ |
58 | 55 | ||
59 | logRes.contents.add(problem) | 56 | workspace.writeModel(problem, filename) |
60 | logRes.save(Collections.EMPTY_MAP) | ||
61 | 57 | ||
62 | //problem.add(Assertion( Y && X <=> X) ) | 58 | //problem.add(Assertion( Y && X <=> X) ) |
63 | 59 | ||
@@ -69,7 +65,7 @@ class VampireTest { | |||
69 | reasoner = new VampireSolver | 65 | reasoner = new VampireSolver |
70 | val vampireConfig = new VampireSolverConfiguration => [ | 66 | val vampireConfig = new VampireSolverConfiguration => [ |
71 | //add configuration things, in config file first | 67 | //add configuration things, in config file first |
72 | it.writeToFile = false | 68 | it.writeToFile = true |
73 | ] | 69 | ] |
74 | 70 | ||
75 | solution = reasoner.solve(problem, vampireConfig, workspace) | 71 | solution = reasoner.solve(problem, vampireConfig, workspace) |
@@ -88,6 +84,10 @@ class VampireTest { | |||
88 | 84 | ||
89 | } | 85 | } |
90 | 86 | ||
87 | def name() { | ||
88 | return this.class.simpleName | ||
89 | } | ||
90 | |||
91 | static def deMorgan(LogicProblem problem) { | 91 | static def deMorgan(LogicProblem problem) { |
92 | 92 | ||
93 | 93 | ||
@@ -144,7 +144,10 @@ class VampireTest { | |||
144 | //x.range | 144 | //x.range |
145 | Exists[ | 145 | Exists[ |
146 | val y = addVar("y",oldRPS) | 146 | val y = addVar("y",oldRPS) |
147 | beats2.call(x,y) | 147 | And(beats2.call(x,y), |
148 | x != y, | ||
149 | Not(beats2.call(y, x)) | ||
150 | ) | ||
148 | ] | 151 | ] |
149 | ])) | 152 | ])) |
150 | //*/ | 153 | //*/ |