aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner
diff options
context:
space:
mode:
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/.DslTest.xtendbinbin0 -> 5966 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbinbin0 -> 4870 bytes
-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 -> 6292 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore12
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java111
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java78
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java142
20 files changed, 679 insertions, 0 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/.DslTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.DslTest.xtendbin
new file mode 100644
index 00000000..59f57d8b
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.DslTest.xtendbin
Binary files differ
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
new file mode 100644
index 00000000..fe447779
--- /dev/null
+++ 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
new file mode 100644
index 00000000..8e57f5e7
--- /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..9d12dab4
--- /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..2760bac4
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore
@@ -0,0 +1,12 @@
1/.VampireTest.java._trace
2/.SimpleRun.java._trace
3/.DslTest.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/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java
new file mode 100644
index 00000000..7b4849e1
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/FAMTest.java
@@ -0,0 +1,111 @@
1package ca.mcgill.ecse.dslreasoner.vampire.test;
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 DslTest {
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("outputDslModels/");
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 = DslTest.loadMetamodel();
56 final List<EObject> partialModel = DslTest.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 LogicProblem logicProblem = modelGenerationProblem.getOutput();
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 = false;
73 };
74 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
75 solution = reasoner.solve(logicProblem, vampireConfig, workspace);
76 InputOutput.<String>println("Problem solved");
77 } catch (Throwable _e) {
78 throw Exceptions.sneakyThrow(_e);
79 }
80 }
81
82 private static EcoreMetamodelDescriptor loadMetamodel() {
83 final FunctionalarchitecturePackage pckg = FunctionalarchitecturePackage.eINSTANCE;
84 final List<EClass> classes = IterableExtensions.<EClass>toList(Iterables.<EClass>filter(pckg.getEClassifiers(), EClass.class));
85 final List<EEnum> enums = IterableExtensions.<EEnum>toList(Iterables.<EEnum>filter(pckg.getEClassifiers(), EEnum.class));
86 final Function1<EEnum, EList<EEnumLiteral>> _function = (EEnum it) -> {
87 return it.getELiterals();
88 };
89 final List<EEnumLiteral> literals = IterableExtensions.<EEnumLiteral>toList(Iterables.<EEnumLiteral>concat(ListExtensions.<EEnum, EList<EEnumLiteral>>map(enums, _function)));
90 final Function1<EClass, EList<EReference>> _function_1 = (EClass it) -> {
91 return it.getEReferences();
92 };
93 final List<EReference> references = IterableExtensions.<EReference>toList(Iterables.<EReference>concat(ListExtensions.<EClass, EList<EReference>>map(classes, _function_1)));
94 final Function1<EClass, EList<EAttribute>> _function_2 = (EClass it) -> {
95 return it.getEAttributes();
96 };
97 final List<EAttribute> attributes = IterableExtensions.<EAttribute>toList(Iterables.<EAttribute>concat(ListExtensions.<EClass, EList<EAttribute>>map(classes, _function_2)));
98 return new EcoreMetamodelDescriptor(classes, Collections.<EClass>unmodifiableSet(CollectionLiterals.<EClass>newHashSet()), false, enums, literals, references, attributes);
99 }
100
101 private static List<EObject> loadPartialModel(final ReasonerWorkspace inputs) {
102 List<EObject> _xblockexpression = null;
103 {
104 Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap();
105 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
106 _extensionToFactoryMap.put("*", _xMIResourceFactoryImpl);
107 _xblockexpression = IteratorExtensions.<EObject>toList(inputs.<EObject>readModel(EObject.class, "FunctionalArchitectureModel.xmi").eResource().getAllContents());
108 }
109 return _xblockexpression;
110 }
111}
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
new file mode 100644
index 00000000..ece0a9bb
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java
@@ -0,0 +1,78 @@
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.LogicReasoner;
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage;
9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
12import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage;
13import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
14import java.util.Map;
15import org.eclipse.emf.common.util.URI;
16import org.eclipse.emf.ecore.EObject;
17import org.eclipse.emf.ecore.resource.Resource;
18import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;
19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
20import org.eclipse.xtend2.lib.StringConcatenation;
21import org.eclipse.xtext.xbase.lib.Exceptions;
22import org.eclipse.xtext.xbase.lib.InputOutput;
23import org.eclipse.xtext.xbase.lib.ObjectExtensions;
24import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
25
26@SuppressWarnings("all")
27public class MedicalSystem {
28 public static void main(final String[] args) {
29 try {
30 MedicalSystem.init();
31 StringConcatenation _builder = new StringConcatenation();
32 _builder.append("output/MedicalSystem/");
33 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), "");
34 workspace.initAndClear();
35 final LogicProblem root = MedicalSystem.load();
36 InputOutput.<String>println("Problem Loaded");
37 LogicResult solution = null;
38 LogicReasoner reasoner = null;
39 VampireSolver _vampireSolver = new VampireSolver();
40 reasoner = _vampireSolver;
41 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
42 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
43 it.writeToFile = true;
44 };
45 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
46 solution = reasoner.solve(root, vampireConfig, workspace);
47 InputOutput.<String>println("Problem Solved");
48 } catch (Throwable _e) {
49 throw Exceptions.sneakyThrow(_e);
50 }
51 }
52
53 protected static LogicProblem load() {
54 LogicProblem _xblockexpression = null;
55 {
56 final ResourceSetImpl resourceSet = new ResourceSetImpl();
57 final Resource resource = resourceSet.getResource(URI.createURI("inputLPs/newMedicalSystem.logicproblem"), true);
58 EObject _get = resource.getContents().get(0);
59 final LogicProblem root = ((LogicProblem) _get);
60 _xblockexpression = root;
61 }
62 return _xblockexpression;
63 }
64
65 protected static void init() {
66 LogiclanguagePackage.eINSTANCE.eClass();
67 LogicproblemPackage.eINSTANCE.eClass();
68 Ecore2logicannotationsPackage.eINSTANCE.eClass();
69 Viatra2LogicAnnotationsPackage.eINSTANCE.eClass();
70 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
71 final Map<String, Object> map = reg.getExtensionToFactoryMap();
72 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
73 map.put("logicproblem", _xMIResourceFactoryImpl);
74 XMIResourceFactoryImpl _xMIResourceFactoryImpl_1 = new XMIResourceFactoryImpl();
75 map.put("tptp", _xMIResourceFactoryImpl_1);
76 VampireLanguageStandaloneSetup.doSetup();
77 }
78}
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..74f117f2
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java
@@ -0,0 +1,142 @@
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.Distinct;
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists;
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription;
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
25import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
26import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
27import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage;
28import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
29import java.util.Map;
30import org.eclipse.emf.common.util.EList;
31import org.eclipse.emf.ecore.resource.Resource;
32import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
33import org.eclipse.xtend2.lib.StringConcatenation;
34import org.eclipse.xtext.xbase.lib.Exceptions;
35import org.eclipse.xtext.xbase.lib.Extension;
36import org.eclipse.xtext.xbase.lib.Functions.Function1;
37import org.eclipse.xtext.xbase.lib.InputOutput;
38import org.eclipse.xtext.xbase.lib.ObjectExtensions;
39import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
40
41@SuppressWarnings("all")
42public class VampireTest {
43 @Extension
44 private final static LogicProblemBuilder builder = new LogicProblemBuilder();
45
46 public static void main(final String[] args) {
47 try {
48 LogicproblemPackage.eINSTANCE.eClass();
49 Ecore2logicannotationsPackage.eINSTANCE.eClass();
50 Viatra2LogicAnnotationsPackage.eINSTANCE.eClass();
51 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
52 final Map<String, Object> map = reg.getExtensionToFactoryMap();
53 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
54 map.put("logicproblem", _xMIResourceFactoryImpl);
55 VampireLanguageStandaloneSetup.doSetup();
56 StringConcatenation _builder = new StringConcatenation();
57 _builder.append("output/VampireTest");
58 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), "");
59 workspace.initAndClear();
60 final String filename = "problem.logicproblem";
61 LogicProblem problem = VampireTest.builder.createProblem();
62 VampireTest.rockPaperScisors(problem);
63 workspace.writeModel(problem, filename);
64 InputOutput.<String>println("Problem Created");
65 LogicResult solution = null;
66 LogicReasoner reasoner = null;
67 VampireSolver _vampireSolver = new VampireSolver();
68 reasoner = _vampireSolver;
69 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
70 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
71 it.writeToFile = true;
72 };
73 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
74 solution = reasoner.solve(problem, vampireConfig, workspace);
75 InputOutput.<String>println("Problem Solved");
76 } catch (Throwable _e) {
77 throw Exceptions.sneakyThrow(_e);
78 }
79 }
80
81 public String name() {
82 return this.getClass().getSimpleName();
83 }
84
85 public static Assertion deMorgan(final LogicProblem problem) {
86 Assertion _xblockexpression = null;
87 {
88 ConstantDeclaration X = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool());
89 ConstantDeclaration Y = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool());
90 VampireTest.builder.add(problem, X);
91 VampireTest.builder.add(problem, Y);
92 And _and = VampireTest.builder.operator_and(X, Y);
93 Not _not = VampireTest.builder.operator_not(_and);
94 Not _not_1 = VampireTest.builder.operator_not(X);
95 Not _not_2 = VampireTest.builder.operator_not(Y);
96 Or _or = VampireTest.builder.operator_or(_not_1, _not_2);
97 Iff _spaceship = VampireTest.builder.operator_spaceship(_not, _or);
98 _xblockexpression = VampireTest.builder.add(problem, VampireTest.builder.Assertion(_spaceship));
99 }
100 return _xblockexpression;
101 }
102
103 public static Assertion rockPaperScisors(final LogicProblem problem) {
104 Assertion _xblockexpression = null;
105 {
106 final DefinedElement rock = VampireTest.builder.Element("Rock");
107 final DefinedElement paper = VampireTest.builder.Element("Paper");
108 final DefinedElement scissor = VampireTest.builder.Element("Scissor");
109 EList<DefinedElement> _elements = problem.getElements();
110 _elements.add(rock);
111 EList<DefinedElement> _elements_1 = problem.getElements();
112 _elements_1.add(paper);
113 EList<DefinedElement> _elements_2 = problem.getElements();
114 _elements_2.add(scissor);
115 final Type oldRPS = VampireTest.builder.add(problem, VampireTest.builder.TypeDefinition("oldRPS", false, rock, paper, scissor));
116 final Relation beats2 = VampireTest.builder.add(problem, VampireTest.builder.RelationDeclaration("beats2", oldRPS, oldRPS));
117 final Function1<VariableContext, TermDescription> _function = (VariableContext it) -> {
118 Exists _xblockexpression_1 = null;
119 {
120 final Variable x = it.addVar("x", oldRPS);
121 final Function1<VariableContext, TermDescription> _function_1 = (VariableContext it_1) -> {
122 And _xblockexpression_2 = null;
123 {
124 final Variable y = it_1.addVar("y", oldRPS);
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)));
129 }
130 return _xblockexpression_2;
131 };
132 _xblockexpression_1 = VampireTest.builder.Exists(_function_1);
133 }
134 return _xblockexpression_1;
135 };
136 _xblockexpression = VampireTest.builder.add(problem,
137 VampireTest.builder.Assertion(
138 VampireTest.builder.Forall(_function)));
139 }
140 return _xblockexpression;
141 }
142}