From f87b4233437f0900c19f462b5e443a3c81b27b6e Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../.classpath | 8 + .../.gitignore | 1 + .../.project | 34 ++++ .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 20 ++ .../build.properties | 4 + .../initialModels/FAM.xmi | 3 + .../initialModels/Yakindu.xmi | 4 + .../initialModels/ecore.xmi | 6 + .../initialModels/fs.xmi | 3 + .../output/files/logProb.logicproblem | 27 +++ .../output/files/vampireCode.tptp | 1 + .../ecse/dslreasoner/vampire/test/SimpleRun.xtend | 213 +++++++++++++++++++++ .../dslreasoner/vampire/test/VampireTest.xtend | 153 +++++++++++++++ .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 0 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 0 -> 6302 bytes .../ecse/dslreasoner/vampire/test/.gitignore | 2 + .../ecse/dslreasoner/vampire/test/VampireTest.java | 140 ++++++++++++++ 18 files changed, 626 insertions(+) create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java (limited to 'Tests') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath new file mode 100644 index 00000000..1c96fe2f --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore @@ -0,0 +1 @@ +/bin/ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project new file mode 100644 index 00000000..eb3347d0 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project @@ -0,0 +1,34 @@ + + + ca.mcgill.ecse.dslreasoner.vampire.test + + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF new file mode 100644 index 00000000..13fcb7b9 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF @@ -0,0 +1,20 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Test +Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test +Bundle-Version: 1.0.0.qualifier +Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Require-Bundle: com.google.guava, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + org.eclipse.xtend.lib.macro, + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", + org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", + hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0" + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties new file mode 100644 index 00000000..41eb6ade --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties @@ -0,0 +1,4 @@ +source.. = src/ +output.. = bin/ +bin.includes = META-INF/,\ + . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi new file mode 100644 index 00000000..c79e58ed --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM.xmi @@ -0,0 +1,3 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi new file mode 100644 index 00000000..49b1f89d --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi @@ -0,0 +1,4 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi new file mode 100644 index 00000000..867e5049 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/ecore.xmi @@ -0,0 +1,6 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi new file mode 100644 index 00000000..56879c1a --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/fs.xmi @@ -0,0 +1,3 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem new file mode 100644 index 00000000..f5f90f38 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/logProb.logicproblem @@ -0,0 +1,27 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp new file mode 100644 index 00000000..ddeec4f4 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/files/vampireCode.tptp @@ -0,0 +1 @@ +%This is an initial Test Comment fof ( assertion1 , axiom , ~ ( constant1 & constant2 ) <=> ( ~ constant1 | ~ constant2 ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend new file mode 100644 index 00000000..feb28dd5 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/SimpleRun.xtend @@ -0,0 +1,213 @@ +//package ca.mcgill.ecse.dslreasoner.vampire.test +// +//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +//import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +//import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage +//import hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern +//import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder +//import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +//import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +//import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +//import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +//import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor +//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +//import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml +//import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +//import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +//import java.util.LinkedHashMap +//import java.util.List +//import org.eclipse.emf.ecore.EAttribute +//import org.eclipse.emf.ecore.EClass +//import org.eclipse.emf.ecore.EEnum +//import org.eclipse.emf.ecore.EEnumLiteral +//import org.eclipse.emf.ecore.EObject +//import org.eclipse.emf.ecore.EReference +//import org.eclipse.emf.ecore.resource.Resource +//import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl +// +//class SimpleRun { +// +// def static void main(String[] args) { +// val inputs = new FileSystemWorkspace('''initialModels/''', "") +// val workspace = new FileSystemWorkspace('''outputModels/''', "") +// workspace.initAndClear +//// +//// println("Input and output workspaces are created") +//// +//// val metamodel = loadMetamodel() +//// val partialModel = loadPartialModel(inputs) +//// val queries = loadQueries(metamodel) +//// +//// println("DSL loaded") +//// +//// val Ecore2Logic ecore2Logic = new Ecore2Logic +//// val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) +//// val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) +//// val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic +//// +//// val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) +//// val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) +//// val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) +//// +//// val logicProblem = validModelExtensionProblem.output +//// //*************xmi.save. advntageous cuz seperate and only contains things that are necessary +//// //Write to file. This is importnat to understand +//// //furthermore, output solution1.partialInterpretation contains also the logic probelm +//// //that needs to be solved +//// +//// //Logic problem same for vamp,l alloy, viatra. but fr alloy, vamp, it is mapped into the specific ecore metamodel using the xtext. +//// //initial simple example: take one thing (ex. iff) from the logic problem generated for one of the sample examples, try to make it into vampire +//// //xtext (but only the instance model, not the lines of code) to see how mapping will work. Then ishteh use vampire on it to "solve" it. +// // create logic problem +// var extension builder = new LogicProblemBuilder +// var LogicProblem problem = builder.createProblem +// +// val rock = Element("Rock") +// val paper = Element("Paper") +// val scissor = Element("Scissor") +// +// problem.elements += rock +// problem.elements += paper +// problem.elements += scissor +// +//// val red = Element("Red") +//// val green = Element("Green") +//// +//// problem.elements += red +//// problem.elements += green +// +//// val allRPS = problem.add(TypeDeclaration("allRPS", true)) +// val oldRPS = problem.add(TypeDefinition("oldRPS", false, rock, paper, scissor)) // n+1 axioms, where n is the number of type definitions. 1. rocjk, paper, scissor are all rps. 2. every object is rps +//// val newRPS = problem.add(TypeDeclaration("newRPS", false)) +//// val color = problem.add(TypeDefinition("color", false, red, green)) +//// Supertype(oldRPS, allRPS) +//// Supertype(newRPS, allRPS) +// +// val beats2 = problem.add(RelationDeclaration("beats2", oldRPS, oldRPS)) +// problem.add(Assertion(Forall[ +// val x = addVar("x", oldRPS) +// // x.range +// Exists[ +// val y = addVar("y", oldRPS) +// beats2.call(x, y) +// ] +// ])) +// +//// val beats = problem.add(RelationDefinition("beats",[ +//// val x = addVar("x",RPS) +//// val y = addVar("y",RPS) +//// (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock) +//// ])) +//// +//// //below needs to be added as an axiom +//// val beats2 = problem.add(RelationDeclaration("beats2",RPS,RPS)) +//// problem.add(Assertion(Forall[ +//// val x = addVar("x",RPS) +//// Exists[ +//// val y = addVar("y",RPS) +//// beats2.call(x,y) +//// ] +//// ])) +// println("Problem created") +// var LogicResult solution +// var LogicReasoner reasoner +// /* +// * reasoner = new ViatraReasoner +// * val viatraConfig = new ViatraReasonerConfiguration => [ +// * it.typeScopes.maxNewElements = 5 +// * it.typeScopes.minNewElements = 5 +// * it.solutionScope.numberOfRequiredSolution = 1 +// * it.existingQueries = queries.patterns.map[it.internalQueryRepresentation] +// * it.debugCongiguration.logging = false +// * it.debugCongiguration.partalInterpretationVisualisationFrequency = 1 +// * it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation +// * ] +// * solution = reasoner.solve(logicProblem,viatraConfig,workspace) +// /*/ +// reasoner = new AlloySolver +// val alloyConfig = new AlloySolverConfiguration => [ +// it.typeScopes.maxNewElements = 5 +// it.typeScopes.minNewElements = 5 +// it.solutionScope.numberOfRequiredSolution = 1 +// it.typeScopes.maxNewIntegers = 0 +// it.writeToFile = false +// ] +// solution = reasoner.solve(problem, alloyConfig, workspace) +// // */ +// // ************ +// // since input logic model is also output, we can check out what is the input for alloy and then +// // see what should be input for vampire, as it should be similar to alloy. once i can create the input, +// // that is the first step. +// // look at allo2logic +// // always keep looking at output +// // try to figure out what rule is used +// println("Problem solved") +// +//// val interpretations = reasoner.getInterpretations(solution as ModelResult) +//// val models = new LinkedList +//// for(interpretation : interpretations) { +//// val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) +//// models+=instanceModel +//// } +//// +//// solution.writeSolution(workspace, #[]) +// } +// +// def private static loadMetamodel() { +// val pckg = FunctionalArchitecturePackage.eINSTANCE +// val List classes = pckg.EClassifiers.filter(EClass).toList +// val List enums = pckg.EClassifiers.filter(EEnum).toList +// val List literals = enums.map[ELiterals].flatten.toList +// val List references = classes.map[EReferences].flatten.toList +// val List attributes = classes.map[EAttributes].flatten.toList +// return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) +// } +// +// def private static loadQueries(EcoreMetamodelDescriptor metamodel) { +// val i = Pattern.instance +// val patterns = i.specifications.toList +// val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet +// val derivedFeatures = new LinkedHashMap +// derivedFeatures.put(i.type.internalQueryRepresentation, metamodel.attributes.filter[it.name == "type"].head) +// derivedFeatures.put(i.model.internalQueryRepresentation, metamodel.references.filter[it.name == "model"].head) +// val res = new ViatraQuerySetDescriptor( +// patterns, +// wfPatterns, +// derivedFeatures +// ) +// return res +// } +// +// def static loadPartialModel(ReasonerWorkspace inputs) { +// Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); +// inputs.readModel(EObject, "FAM.xmi").eResource.allContents.toList +// } +// +// def static writeSolution(LogicResult solution, ReasonerWorkspace workspace, List models) { +// if (solution instanceof ModelResult) { +// val representations = solution.representation +// for (representationIndex : 0 ..< representations.size) { +// val representation = representations.get(representationIndex) +// val representationNumber = representationIndex + 1 +// if (representation instanceof PartialInterpretation) { +// workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') +// val partialInterpretation2GML = new PartialInterpretation2Gml +// val gml = partialInterpretation2GML.transform(representation) +// // ecore2GML.transform(root) +// workspace.writeText('''solutionVisualisation.gml''', gml) +// +// } else { +// workspace.writeText('''solution«representationNumber».txt''', representation.toString) +// } +// } +// for (model : models) { +// workspace.writeModel(model, "model.xmi") +// } +// println("Solution saved and visualised") +// } +// } +// +// def static visualizeSolution() { +// } +//} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend new file mode 100644 index 00000000..64914fd0 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend @@ -0,0 +1,153 @@ +package ca.mcgill.ecse.dslreasoner.vampire.test + + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.Collections +import org.eclipse.emf.common.util.URI +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl + +class VampireTest { + + val static extension LogicProblemBuilder builder = new LogicProblemBuilder + + def static void main(String[] args) { +// val inputs = new FileSystemWorkspace('''initialModels/''',"") + + + //create logic problem + //var LogicProblem problem = builder.createProblem + + + + LogicproblemPackage.eINSTANCE.eClass() + Ecore2logicannotationsPackage.eINSTANCE.eClass() + Viatra2LogicAnnotationsPackage.eINSTANCE.eClass() + val reg = Resource.Factory.Registry.INSTANCE + val map = reg.extensionToFactoryMap + map.put("logicproblem", new XMIResourceFactoryImpl) + VampireLanguageStandaloneSetup.doSetup + + val workspace = new FileSystemWorkspace('''output/models/''',"") + workspace.initAndClear + + // Load and create top level elements + // Load source model + val rs = new ResourceSetImpl + val logicURI = URI.createFileURI("output/files/logProb.logicproblem") + val logRes = rs.createResource(logicURI) + + var LogicProblem problem = builder.createProblem + + //* + deMorgan(problem) + /*/ + rockPaperScisors(problem) + //*/ + + logRes.contents.add(problem) + logRes.save(Collections.EMPTY_MAP) + + //problem.add(Assertion( Y && X <=> X) ) + + println("Problem Created"); + + var LogicResult solution + var LogicReasoner reasoner + + reasoner = new VampireSolver + val vampireConfig = new VampireSolverConfiguration => [ + //add configuration things, in config file first + it.writeToFile = false + ] + + solution = reasoner.solve(problem, vampireConfig, workspace) + +// if(solution instanceof ModelResult) { +// reasoner.getInterpretations(solution) +// } + //^can extract everything (ex, vars) from solver + + + //call the solver + + println("Problem Solved") + + //output solution + + } + + static def deMorgan(LogicProblem problem) { + + + var X = ConstantDeclaration(LogicBool) + var Y = ConstantDeclaration(LogicBool) + problem.add(X) + problem.add(Y) + + //assertion is negated manually because logic problem can only handle axioms (assertions) + //so ya + problem.add(Assertion( !(X && Y) <=> ( !X || !Y)) ) + } + + static def rockPaperScisors(LogicProblem problem) { + + val rock = Element("Rock") + val paper= Element("Paper") + val scissor = Element("Scissor") + + problem.elements += rock + problem.elements += paper + problem.elements += scissor + +// val red = Element("Red") +// val green = Element("Green") +// +// problem.elements += red +// problem.elements += green + + + //val allRPS = problem.add(TypeDeclaration("allRPS", true)) + //val newRPS = problem.add(TypeDeclaration("newRPS", false)) + val oldRPS = problem.add(TypeDefinition("oldRPS", false, rock, paper, scissor)) //n+1 axioms, where n is the number of type definitions. 1. rocjk, paper, scissor are all rps. 2. every object is rps + +// val color = problem.add(TypeDefinition("color", false, red, green )) + //Supertype(oldRPS,allRPS) + //Supertype(newRPS,oldRPS) + + + + + /* Remains + val beats = problem.add(RelationDefinition("beats",[ + val x = addVar("x",oldRPS) + val y = addVar("y",oldRPS) + (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock) + ])) + + /*/ + //below needs to be added as an axiom + val beats2 = problem.add(RelationDeclaration("beats2",oldRPS,oldRPS)) + problem.add(Assertion(Forall[ + val x = addVar("x",oldRPS) + //x.range + Exists[ + val y = addVar("y",oldRPS) + beats2.call(x,y) + ] + ])) + //*/ + + } +} \ No newline at end of file diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin new file mode 100644 index 00000000..b60ffe4c Binary files /dev/null and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin new file mode 100644 index 00000000..881f927c Binary files /dev/null and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore new file mode 100644 index 00000000..f3c47b99 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore @@ -0,0 +1,2 @@ +/.VampireTest.java._trace +/.SimpleRun.java._trace diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java new file mode 100644 index 00000000..73c413b3 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java @@ -0,0 +1,140 @@ +package ca.mcgill.ecse.dslreasoner.vampire.test; + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage; +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; +import java.util.Collections; +import java.util.Map; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class VampireTest { + @Extension + private final static LogicProblemBuilder builder = new LogicProblemBuilder(); + + public static void main(final String[] args) { + try { + LogicproblemPackage.eINSTANCE.eClass(); + Ecore2logicannotationsPackage.eINSTANCE.eClass(); + Viatra2LogicAnnotationsPackage.eINSTANCE.eClass(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + VampireLanguageStandaloneSetup.doSetup(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("output/models/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); + workspace.initAndClear(); + final ResourceSetImpl rs = new ResourceSetImpl(); + final URI logicURI = URI.createFileURI("output/files/logProb.logicproblem"); + final Resource logRes = rs.createResource(logicURI); + LogicProblem problem = VampireTest.builder.createProblem(); + VampireTest.deMorgan(problem); + logRes.getContents().add(problem); + logRes.save(Collections.EMPTY_MAP); + InputOutput.println("Problem Created"); + LogicResult solution = null; + LogicReasoner reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.writeToFile = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + solution = reasoner.solve(problem, vampireConfig, workspace); + InputOutput.println("Problem Solved"); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } + } + + public static Assertion deMorgan(final LogicProblem problem) { + Assertion _xblockexpression = null; + { + ConstantDeclaration X = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); + ConstantDeclaration Y = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); + VampireTest.builder.add(problem, X); + VampireTest.builder.add(problem, Y); + And _and = VampireTest.builder.operator_and(X, Y); + Not _not = VampireTest.builder.operator_not(_and); + Not _not_1 = VampireTest.builder.operator_not(X); + Not _not_2 = VampireTest.builder.operator_not(Y); + Or _or = VampireTest.builder.operator_or(_not_1, _not_2); + Iff _spaceship = VampireTest.builder.operator_spaceship(_not, _or); + _xblockexpression = VampireTest.builder.add(problem, VampireTest.builder.Assertion(_spaceship)); + } + return _xblockexpression; + } + + public static Assertion rockPaperScisors(final LogicProblem problem) { + Assertion _xblockexpression = null; + { + final DefinedElement rock = VampireTest.builder.Element("Rock"); + final DefinedElement paper = VampireTest.builder.Element("Paper"); + final DefinedElement scissor = VampireTest.builder.Element("Scissor"); + EList _elements = problem.getElements(); + _elements.add(rock); + EList _elements_1 = problem.getElements(); + _elements_1.add(paper); + EList _elements_2 = problem.getElements(); + _elements_2.add(scissor); + final Type oldRPS = VampireTest.builder.add(problem, VampireTest.builder.TypeDefinition("oldRPS", false, rock, paper, scissor)); + final Relation beats2 = VampireTest.builder.add(problem, VampireTest.builder.RelationDeclaration("beats2", oldRPS, oldRPS)); + final Function1 _function = (VariableContext it) -> { + Exists _xblockexpression_1 = null; + { + final Variable x = it.addVar("x", oldRPS); + final Function1 _function_1 = (VariableContext it_1) -> { + SymbolicValue _xblockexpression_2 = null; + { + final Variable y = it_1.addVar("y", oldRPS); + _xblockexpression_2 = VampireTest.builder.call(beats2, x, y); + } + return _xblockexpression_2; + }; + _xblockexpression_1 = VampireTest.builder.Exists(_function_1); + } + return _xblockexpression_1; + }; + _xblockexpression = VampireTest.builder.add(problem, + VampireTest.builder.Assertion( + VampireTest.builder.Forall(_function))); + } + return _xblockexpression; + } +} -- cgit v1.2.3-54-g00ecf