aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-02-01 16:03:30 -0500
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-07 19:06:28 -0400
commit57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch)
tree16806454dff463419af99b14f6abfab3d1fa5291 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner
parentFAM MM transformation works (diff)
downloadVIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz
VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst
VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbinbin0 -> 6811 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbinbin0 -> 4111 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin0 -> 4124 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbinbin0 -> 7276 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin0 -> 3643 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.gitignore6
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java116
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java38
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java38
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java127
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java10
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icseTest/.gitignore1
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbinbin4870 -> 4870 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbinbin687 -> 687 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbinbin6307 -> 6292 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore8
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java (renamed from Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.java)0
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java4
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java26
19 files changed, 360 insertions, 14 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
new file mode 100644
index 00000000..cf5c79b4
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
new file mode 100644
index 00000000..33fae225
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
new file mode 100644
index 00000000..56144b8f
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
new file mode 100644
index 00000000..29d89e94
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
new file mode 100644
index 00000000..c0d35b2f
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.gitignore
new file mode 100644
index 00000000..1b426999
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.gitignore
@@ -0,0 +1,6 @@
1/.FAMTest.java._trace
2/.YakinduTest.java._trace
3/.EcoreTest.java._trace
4/.fileSystemTest.java._trace
5/.FileSystemTest.java._trace
6/.GeneralTest.java._trace
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java
new file mode 100644
index 00000000..f3dc8572
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java
@@ -0,0 +1,116 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
5import com.google.common.collect.Iterables;
6import functionalarchitecture.FunctionalarchitecturePackage;
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
10import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
15import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
18import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
19import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
20import java.util.Collections;
21import java.util.List;
22import java.util.Map;
23import org.eclipse.emf.common.util.EList;
24import org.eclipse.emf.ecore.EAttribute;
25import org.eclipse.emf.ecore.EClass;
26import org.eclipse.emf.ecore.EEnum;
27import org.eclipse.emf.ecore.EEnumLiteral;
28import org.eclipse.emf.ecore.EObject;
29import org.eclipse.emf.ecore.EReference;
30import org.eclipse.emf.ecore.resource.Resource;
31import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
32import org.eclipse.xtend2.lib.StringConcatenation;
33import org.eclipse.xtext.xbase.lib.CollectionLiterals;
34import org.eclipse.xtext.xbase.lib.Exceptions;
35import org.eclipse.xtext.xbase.lib.Functions.Function1;
36import org.eclipse.xtext.xbase.lib.InputOutput;
37import org.eclipse.xtext.xbase.lib.IterableExtensions;
38import org.eclipse.xtext.xbase.lib.IteratorExtensions;
39import org.eclipse.xtext.xbase.lib.ListExtensions;
40import org.eclipse.xtext.xbase.lib.ObjectExtensions;
41import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
42
43@SuppressWarnings("all")
44public class EcoreTest {
45 public static void main(final String[] args) {
46 try {
47 StringConcatenation _builder = new StringConcatenation();
48 _builder.append("initialModels/");
49 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
50 StringConcatenation _builder_1 = new StringConcatenation();
51 _builder_1.append("output/FAMTest/");
52 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
53 workspace.initAndClear();
54 InputOutput.<String>println("Input and output workspaces are created");
55 final EcoreMetamodelDescriptor metamodel = EcoreTest.loadMetamodel();
56 final List<EObject> partialModel = EcoreTest.loadPartialModel(inputs);
57 InputOutput.<String>println("DSL loaded");
58 final Ecore2Logic ecore2Logic = new Ecore2Logic();
59 final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);
60 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
61 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
62 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
63 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
64 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);
65 final LogicProblem logicProblem = modelGenerationProblem.getOutput();
66 InputOutput.<String>println("Problem created");
67 LogicResult solution = null;
68 LogicReasoner reasoner = null;
69 VampireSolver _vampireSolver = new VampireSolver();
70 reasoner = _vampireSolver;
71 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
72 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
73 it.writeToFile = true;
74 };
75 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
76 solution = reasoner.solve(logicProblem, vampireConfig, workspace);
77 InputOutput.<String>println("Problem solved");
78 } catch (Throwable _e) {
79 throw Exceptions.sneakyThrow(_e);
80 }
81 }
82
83 private static EcoreMetamodelDescriptor loadMetamodel() {
84 final FunctionalarchitecturePackage pckg = FunctionalarchitecturePackage.eINSTANCE;
85 final List<EClass> classes = IterableExtensions.<EClass>toList(Iterables.<EClass>filter(pckg.getEClassifiers(), EClass.class));
86 final List<EEnum> enums = IterableExtensions.<EEnum>toList(Iterables.<EEnum>filter(pckg.getEClassifiers(), EEnum.class));
87 final Function1<EEnum, EList<EEnumLiteral>> _function = (EEnum it) -> {
88 return it.getELiterals();
89 };
90 final List<EEnumLiteral> literals = IterableExtensions.<EEnumLiteral>toList(Iterables.<EEnumLiteral>concat(ListExtensions.<EEnum, EList<EEnumLiteral>>map(enums, _function)));
91 final Function1<EClass, EList<EReference>> _function_1 = (EClass it) -> {
92 return it.getEReferences();
93 };
94 final List<EReference> references = IterableExtensions.<EReference>toList(Iterables.<EReference>concat(ListExtensions.<EClass, EList<EReference>>map(classes, _function_1)));
95 final Function1<EClass, EList<EAttribute>> _function_2 = (EClass it) -> {
96 return it.getEAttributes();
97 };
98 final List<EAttribute> attributes = IterableExtensions.<EAttribute>toList(Iterables.<EAttribute>concat(ListExtensions.<EClass, EList<EAttribute>>map(classes, _function_2)));
99 return new EcoreMetamodelDescriptor(classes, Collections.<EClass>unmodifiableSet(CollectionLiterals.<EClass>newHashSet()), false, enums, literals, references, attributes);
100 }
101
102 private static List<EObject> loadPartialModel(final ReasonerWorkspace inputs) {
103 List<EObject> _xblockexpression = null;
104 {
105 Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap();
106 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
107 _extensionToFactoryMap.put("*", _xMIResourceFactoryImpl);
108 _xblockexpression = IteratorExtensions.<EObject>toList(inputs.<EObject>readModel(EObject.class, "FamInstance.xmi").eResource().getAllContents());
109 }
110 return _xblockexpression;
111 }
112
113 private static Object loadQueries(final EcoreMetamodelDescriptor metamodel) {
114 return null;
115 }
116}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
new file mode 100644
index 00000000..92803b7f
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -0,0 +1,38 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import functionalarchitecture.FunctionalarchitecturePackage;
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
9import java.util.Map;
10import org.eclipse.emf.common.util.EList;
11import org.eclipse.emf.ecore.EObject;
12import org.eclipse.emf.ecore.resource.Resource;
13import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
14import org.eclipse.xtend2.lib.StringConcatenation;
15import org.eclipse.xtext.xbase.lib.InputOutput;
16
17@SuppressWarnings("all")
18public class FAMTest {
19 public static void main(final String[] args) {
20 StringConcatenation _builder = new StringConcatenation();
21 _builder.append("initialModels/");
22 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
23 StringConcatenation _builder_1 = new StringConcatenation();
24 _builder_1.append("output/FAMTest/");
25 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
26 workspace.initAndClear();
27 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
28 final Map<String, Object> map = reg.getExtensionToFactoryMap();
29 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
30 map.put("logicproblem", _xMIResourceFactoryImpl);
31 InputOutput.<String>println("Input and output workspaces are created");
32 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);
33 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi");
34 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());
35 InputOutput.<String>println("DSL loaded");
36 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace);
37 }
38}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
new file mode 100644
index 00000000..5994b4b4
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
@@ -0,0 +1,38 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import functionalarchitecture.FunctionalarchitecturePackage;
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns;
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
7import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
8import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
9import java.util.Map;
10import org.eclipse.emf.common.util.EList;
11import org.eclipse.emf.ecore.EObject;
12import org.eclipse.emf.ecore.resource.Resource;
13import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
14import org.eclipse.xtend2.lib.StringConcatenation;
15import org.eclipse.xtext.xbase.lib.InputOutput;
16
17@SuppressWarnings("all")
18public class FileSystemTest {
19 public static void main(final String[] args) {
20 StringConcatenation _builder = new StringConcatenation();
21 _builder.append("initialModels/");
22 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
23 StringConcatenation _builder_1 = new StringConcatenation();
24 _builder_1.append("output/FAMTest/");
25 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
26 workspace.initAndClear();
27 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
28 final Map<String, Object> map = reg.getExtensionToFactoryMap();
29 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
30 map.put("logicproblem", _xMIResourceFactoryImpl);
31 InputOutput.<String>println("Input and output workspaces are created");
32 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);
33 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi");
34 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());
35 InputOutput.<String>println("DSL loaded");
36 GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace);
37 }
38}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
new file mode 100644
index 00000000..92cf666c
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -0,0 +1,127 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
5import com.google.common.base.Objects;
6import com.google.common.collect.Iterables;
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
10import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
15import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
17import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;
18import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
20import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
21import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
22import java.util.Collections;
23import java.util.List;
24import java.util.Map;
25import java.util.Set;
26import org.eclipse.emf.common.util.EList;
27import org.eclipse.emf.ecore.EAttribute;
28import org.eclipse.emf.ecore.EClass;
29import org.eclipse.emf.ecore.EEnum;
30import org.eclipse.emf.ecore.EEnumLiteral;
31import org.eclipse.emf.ecore.EObject;
32import org.eclipse.emf.ecore.EPackage;
33import org.eclipse.emf.ecore.EReference;
34import org.eclipse.emf.ecore.EStructuralFeature;
35import org.eclipse.emf.ecore.resource.Resource;
36import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
37import org.eclipse.viatra.query.runtime.api.IQueryGroup;
38import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
39import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
40import org.eclipse.xtext.xbase.lib.CollectionLiterals;
41import org.eclipse.xtext.xbase.lib.Exceptions;
42import org.eclipse.xtext.xbase.lib.Functions.Function1;
43import org.eclipse.xtext.xbase.lib.InputOutput;
44import org.eclipse.xtext.xbase.lib.IterableExtensions;
45import org.eclipse.xtext.xbase.lib.ListExtensions;
46import org.eclipse.xtext.xbase.lib.ObjectExtensions;
47import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
48
49@SuppressWarnings("all")
50public class GeneralTest {
51 public static String createAndSolveProblem(final EcoreMetamodelDescriptor metamodel, final List<EObject> partialModel, final ViatraQuerySetDescriptor queries, final FileSystemWorkspace workspace) {
52 try {
53 String _xblockexpression = null;
54 {
55 final Ecore2Logic ecore2Logic = new Ecore2Logic();
56 final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);
57 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
58 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
59 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
60 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
61 LogicProblem problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
62 Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();
63 problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, _viatra2LogicConfiguration).getOutput();
64 workspace.writeModel(problem, "Fam.logicproblem");
65 InputOutput.<String>println("Problem created");
66 LogicResult solution = null;
67 LogicReasoner reasoner = null;
68 VampireSolver _vampireSolver = new VampireSolver();
69 reasoner = _vampireSolver;
70 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
71 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
72 it.writeToFile = true;
73 };
74 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
75 solution = reasoner.solve(problem, vampireConfig, workspace);
76 _xblockexpression = InputOutput.<String>println("Problem solved");
77 }
78 return _xblockexpression;
79 } catch (Throwable _e) {
80 throw Exceptions.sneakyThrow(_e);
81 }
82 }
83
84 public static EcoreMetamodelDescriptor loadMetamodel(final EPackage pckg) {
85 final List<EClass> classes = IterableExtensions.<EClass>toList(Iterables.<EClass>filter(pckg.getEClassifiers(), EClass.class));
86 final List<EEnum> enums = IterableExtensions.<EEnum>toList(Iterables.<EEnum>filter(pckg.getEClassifiers(), EEnum.class));
87 final Function1<EEnum, EList<EEnumLiteral>> _function = (EEnum it) -> {
88 return it.getELiterals();
89 };
90 final List<EEnumLiteral> literals = IterableExtensions.<EEnumLiteral>toList(Iterables.<EEnumLiteral>concat(ListExtensions.<EEnum, EList<EEnumLiteral>>map(enums, _function)));
91 final Function1<EClass, EList<EReference>> _function_1 = (EClass it) -> {
92 return it.getEReferences();
93 };
94 final List<EReference> references = IterableExtensions.<EReference>toList(Iterables.<EReference>concat(ListExtensions.<EClass, EList<EReference>>map(classes, _function_1)));
95 final Function1<EClass, EList<EAttribute>> _function_2 = (EClass it) -> {
96 return it.getEAttributes();
97 };
98 final List<EAttribute> attributes = IterableExtensions.<EAttribute>toList(Iterables.<EAttribute>concat(ListExtensions.<EClass, EList<EAttribute>>map(classes, _function_2)));
99 return new EcoreMetamodelDescriptor(classes, Collections.<EClass>unmodifiableSet(CollectionLiterals.<EClass>newHashSet()), false, enums, literals, references, attributes);
100 }
101
102 public static EList<EObject> loadPartialModel(final ReasonerWorkspace inputs, final String path) {
103 EList<EObject> _xblockexpression = null;
104 {
105 Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap();
106 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
107 _extensionToFactoryMap.put("*", _xMIResourceFactoryImpl);
108 _xblockexpression = inputs.<EObject>readModel(EObject.class, path).eResource().getContents();
109 }
110 return _xblockexpression;
111 }
112
113 public static ViatraQuerySetDescriptor loadQueries(final EcoreMetamodelDescriptor metamodel, final IQueryGroup i) {
114 final List<IQuerySpecification<?>> patterns = IterableExtensions.<IQuerySpecification<?>>toList(i.getSpecifications());
115 final Function1<IQuerySpecification<?>, Boolean> _function = (IQuerySpecification<?> it) -> {
116 final Function1<PAnnotation, Boolean> _function_1 = (PAnnotation it_1) -> {
117 String _name = it_1.getName();
118 return Boolean.valueOf(Objects.equal(_name, "Constraint"));
119 };
120 return Boolean.valueOf(IterableExtensions.<PAnnotation>exists(it.getAllAnnotations(), _function_1));
121 };
122 final Set<IQuerySpecification<?>> wfPatterns = IterableExtensions.<IQuerySpecification<?>>toSet(IterableExtensions.<IQuerySpecification<?>>filter(patterns, _function));
123 final Map<IQuerySpecification<?>, EStructuralFeature> derivedFeatures = CollectionLiterals.<IQuerySpecification<?>, EStructuralFeature>emptyMap();
124 final ViatraQuerySetDescriptor res = new ViatraQuerySetDescriptor(patterns, wfPatterns, derivedFeatures);
125 return res;
126 }
127}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
new file mode 100644
index 00000000..fa4ef6b9
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -0,0 +1,10 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2
3@SuppressWarnings("all")
4public class YakinduTest {
5 public static void main(final String[] args) {
6 throw new Error("Unresolved compilation problems:"
7 + "\nmissing \')\' at \'GeneralTest\'"
8 + "\nType mismatch: cannot convert from String to IQueryGroup");
9 }
10}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icseTest/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icseTest/.gitignore
new file mode 100644
index 00000000..f3e21798
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icseTest/.gitignore
@@ -0,0 +1 @@
/.FAMTest.java._trace
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index 01664d90..fe447779 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
Binary files differ
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
index 6a36d4d4..8e57f5e7 100644
--- 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
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
index 93a2e4f4..9d12dab4 100644
--- 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
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
index 15b5afc4..2760bac4 100644
--- 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
@@ -2,3 +2,11 @@
2/.SimpleRun.java._trace 2/.SimpleRun.java._trace
3/.DslTest.java._trace 3/.DslTest.java._trace
4/.MedicalSystem.java._trace 4/.MedicalSystem.java._trace
5/.DslTest.xtendbin
6/.MedicalSystem.xtendbin
7/.SimpleRun.xtendbin
8/.VampireTest.xtendbin
9/DslTest.java
10/MedicalSystem.java
11/VampireTest.java
12/.FAMTest.java._trace
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java
index 7b4849e1..7b4849e1 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/DslTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
index d4f53d65..ece0a9bb 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
@@ -29,7 +29,7 @@ public class MedicalSystem {
29 try { 29 try {
30 MedicalSystem.init(); 30 MedicalSystem.init();
31 StringConcatenation _builder = new StringConcatenation(); 31 StringConcatenation _builder = new StringConcatenation();
32 _builder.append("outputModels/"); 32 _builder.append("output/MedicalSystem/");
33 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); 33 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), "");
34 workspace.initAndClear(); 34 workspace.initAndClear();
35 final LogicProblem root = MedicalSystem.load(); 35 final LogicProblem root = MedicalSystem.load();
@@ -40,7 +40,7 @@ public class MedicalSystem {
40 reasoner = _vampireSolver; 40 reasoner = _vampireSolver;
41 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 41 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
42 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 42 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
43 it.writeToFile = false; 43 it.writeToFile = true;
44 }; 44 };
45 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 45 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
46 solution = reasoner.solve(root, vampireConfig, workspace); 46 solution = reasoner.solve(root, vampireConfig, workspace);
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
index d02174f7..74f117f2 100644
--- 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
@@ -11,6 +11,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And;
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; 11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion;
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; 12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration;
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; 13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; 15import 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.Iff;
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; 17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not;
@@ -25,12 +26,9 @@ import 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.logic.model.logicresult.LogicResult;
26import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage; 27import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage;
27import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; 28import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
28import java.util.Collections;
29import java.util.Map; 29import java.util.Map;
30import org.eclipse.emf.common.util.EList; 30import org.eclipse.emf.common.util.EList;
31import org.eclipse.emf.common.util.URI;
32import org.eclipse.emf.ecore.resource.Resource; 31import org.eclipse.emf.ecore.resource.Resource;
33import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;
34import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 32import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
35import org.eclipse.xtend2.lib.StringConcatenation; 33import org.eclipse.xtend2.lib.StringConcatenation;
36import org.eclipse.xtext.xbase.lib.Exceptions; 34import org.eclipse.xtext.xbase.lib.Exceptions;
@@ -56,16 +54,13 @@ public class VampireTest {
56 map.put("logicproblem", _xMIResourceFactoryImpl); 54 map.put("logicproblem", _xMIResourceFactoryImpl);
57 VampireLanguageStandaloneSetup.doSetup(); 55 VampireLanguageStandaloneSetup.doSetup();
58 StringConcatenation _builder = new StringConcatenation(); 56 StringConcatenation _builder = new StringConcatenation();
59 _builder.append("output/models/"); 57 _builder.append("output/VampireTest");
60 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); 58 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), "");
61 workspace.initAndClear(); 59 workspace.initAndClear();
62 final ResourceSetImpl rs = new ResourceSetImpl(); 60 final String filename = "problem.logicproblem";
63 final URI logicURI = URI.createFileURI("output/files/logProb.logicproblem");
64 final Resource logRes = rs.createResource(logicURI);
65 LogicProblem problem = VampireTest.builder.createProblem(); 61 LogicProblem problem = VampireTest.builder.createProblem();
66 VampireTest.rockPaperScisors(problem); 62 VampireTest.rockPaperScisors(problem);
67 logRes.getContents().add(problem); 63 workspace.writeModel(problem, filename);
68 logRes.save(Collections.EMPTY_MAP);
69 InputOutput.<String>println("Problem Created"); 64 InputOutput.<String>println("Problem Created");
70 LogicResult solution = null; 65 LogicResult solution = null;
71 LogicReasoner reasoner = null; 66 LogicReasoner reasoner = null;
@@ -73,7 +68,7 @@ public class VampireTest {
73 reasoner = _vampireSolver; 68 reasoner = _vampireSolver;
74 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 69 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
75 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 70 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
76 it.writeToFile = false; 71 it.writeToFile = true;
77 }; 72 };
78 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 73 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
79 solution = reasoner.solve(problem, vampireConfig, workspace); 74 solution = reasoner.solve(problem, vampireConfig, workspace);
@@ -83,6 +78,10 @@ public class VampireTest {
83 } 78 }
84 } 79 }
85 80
81 public String name() {
82 return this.getClass().getSimpleName();
83 }
84
86 public static Assertion deMorgan(final LogicProblem problem) { 85 public static Assertion deMorgan(final LogicProblem problem) {
87 Assertion _xblockexpression = null; 86 Assertion _xblockexpression = null;
88 { 87 {
@@ -120,10 +119,13 @@ public class VampireTest {
120 { 119 {
121 final Variable x = it.addVar("x", oldRPS); 120 final Variable x = it.addVar("x", oldRPS);
122 final Function1<VariableContext, TermDescription> _function_1 = (VariableContext it_1) -> { 121 final Function1<VariableContext, TermDescription> _function_1 = (VariableContext it_1) -> {
123 SymbolicValue _xblockexpression_2 = null; 122 And _xblockexpression_2 = null;
124 { 123 {
125 final Variable y = it_1.addVar("y", oldRPS); 124 final Variable y = it_1.addVar("y", oldRPS);
126 _xblockexpression_2 = VampireTest.builder.call(beats2, x, y); 125 SymbolicValue _call = VampireTest.builder.call(beats2, x, y);
126 Distinct _notEquals = VampireTest.builder.operator_notEquals(x, y);
127 _xblockexpression_2 = VampireTest.builder.And(_call, _notEquals,
128 VampireTest.builder.Not(VampireTest.builder.call(beats2, y, x)));
127 } 129 }
128 return _xblockexpression_2; 130 return _xblockexpression_2;
129 }; 131 };