From 4aee5bcc86b9e6b515fbbdac030df42147be7dc1 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sun, 8 Sep 2019 16:12:55 -0400 Subject: VAMPIRE: Implement wf constraint handling --- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4554 -> 4554 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 7087 -> 7364 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6204 -> 6204 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 6456 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 7055 -> 7055 bytes .../ecse/dslreasoner/vampire/icse/FAMTest.java | 32 +++++++++------------ 6 files changed, 14 insertions(+), 18 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse') 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 index 771e1d1a..775c1663 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin 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 index ad844992..4e802213 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin 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 index 7dcb4392..f7e42672 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin 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 index dc040005..ae8b52eb 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin 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 index 2bb8be0d..73b1182c 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin differ 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 index 8ef096d9..7f6dfcd5 100644 --- 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 @@ -3,10 +3,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import functionalarchitecture.FAMTerminator; import functionalarchitecture.Function; import functionalarchitecture.FunctionalArchitectureModel; import functionalarchitecture.FunctionalOutput; import functionalarchitecture.FunctionalarchitecturePackage; +import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; @@ -20,12 +22,10 @@ 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.logic2ecore.Logic2Ecore; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; +import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation; -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.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; -import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser; import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; import java.util.HashMap; import java.util.List; @@ -37,7 +37,6 @@ 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.InputOutput; -import org.eclipse.xtext.xbase.lib.IteratorExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -64,12 +63,14 @@ public class FAMTest { InputOutput.println("Input and output workspaces are created"); final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); final EList partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); - final Object queries = null; + final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); InputOutput.println("DSL loaded"); Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); LogicProblem problem = modelGenerationProblem.getOutput(); problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); + Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); + problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, _viatra2LogicConfiguration).getOutput(); workspace.writeModel(problem, "Fam.logicproblem"); InputOutput.println("Problem created"); long startTime = System.currentTimeMillis(); @@ -77,7 +78,7 @@ public class FAMTest { VampireSolver _vampireSolver = new VampireSolver(); reasoner = _vampireSolver; final HashMap classMapMin = new HashMap(); - classMapMin.put(FunctionalOutput.class, Integer.valueOf(3)); + classMapMin.put(FAMTerminator.class, Integer.valueOf(1)); final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); final HashMap classMapMax = new HashMap(); classMapMax.put(FunctionalArchitectureModel.class, Integer.valueOf(3)); @@ -90,27 +91,22 @@ public class FAMTest { it.documentationLevel = DocumentationLevel.FULL; it.typeScopes.minNewElements = 4; it.typeScopes.maxNewElements = 5; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } it.contCycleLevel = 5; it.uniquenessDuplicates = false; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); List interpretations = reasoner.getInterpretations(((ModelResult) solution)); + InputOutput.>print(interpretations.getClass()); for (final LogicModelInterpretation interpretation : interpretations) { { final EObject model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.getTrace()); workspace.writeModel(model, "model.xmi"); - final PartialInterpretation representation = im2pi.transform(modelGenerationProblem, IteratorExtensions.toList(model.eAllContents()), false); - if ((representation instanceof PartialInterpretation)) { - final PartialInterpretation2Gml vis1 = new PartialInterpretation2Gml(); - final String gml = vis1.transform(representation); - workspace.writeText("model.gml", gml); - final GraphvizVisualiser vis2 = new GraphvizVisualiser(); - final PartialInterpretationVisualisation dot = vis2.visualiseConcretization(representation); - dot.writeToFile(workspace, "model.png"); - } else { - InputOutput.println("ERROR"); - } } } long _currentTimeMillis = System.currentTimeMillis(); -- cgit v1.2.3-70-g09d2