From 71108d462c2695d917e87acea6f49d3f2954c6f4 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sun, 8 Sep 2019 16:12:55 -0400 Subject: VAMPIRE: Implement wf constraint handling --- .../execution/GenerationTaskExecutor.xtend | 2 +- .../model/FamMetamodel.ecore | 12 +- .../Examples/ModelGenExampleFAM_plugin/plugin.xml | 13 - .../domains/transima/fam/FamPatterns.vql | 79 +- .../model/PartialInterpretation.aird | 1086 ++++++++++---------- .../ide/.VampireLanguageIdeModule.xtendbin | Bin 1685 -> 1685 bytes .../ide/.VampireLanguageIdeSetup.xtendbin | Bin 2500 -> 2500 bytes .../ui/.VampireLanguageUiModule.xtendbin | Bin 2342 -> 2342 bytes .../.VampireLanguageProposalProvider.xtendbin | Bin 1792 -> 1792 bytes ...ampireLanguageDescriptionLabelProvider.xtendbin | Bin 1965 -> 1965 bytes .../.VampireLanguageLabelProvider.xtendbin | Bin 2405 -> 2405 bytes .../.VampireLanguageOutlineTreeProvider.xtendbin | Bin 1819 -> 1819 bytes .../.VampireLanguageQuickfixProvider.xtendbin | Bin 1786 -> 1786 bytes .../formatting2/VampireLanguageFormatter.xtend | 6 +- .../.VampireLanguageRuntimeModule.xtendbin | Bin 1706 -> 1706 bytes .../.VampireLanguageStandaloneSetup.xtendbin | Bin 1980 -> 1980 bytes .../formatting2/.VampireLanguageFormatter.xtendbin | Bin 3706 -> 3759 bytes .../formatting2/VampireLanguageFormatter.java | 4 + .../generator/.VampireLanguageGenerator.xtendbin | Bin 2338 -> 2338 bytes .../scoping/.VampireLanguageScopeProvider.xtendbin | Bin 1751 -> 1751 bytes .../validation/.VampireLanguageValidator.xtendbin | Bin 1736 -> 1736 bytes .../builder/Logic2VampireLanguageMapper.xtend | 32 +- .../builder/Logic2VampireLanguageMapperTrace.xtend | 2 + ...gic2VampireLanguageMapper_AssertionMapper.xtend | 5 + ...ogic2VampireLanguageMapper_RelationMapper.xtend | 168 ++- .../builder/VampireModelInterpretation.xtend | 150 +-- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 6957 -> 6956 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 17725 -> 17989 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4874 -> 5080 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3165 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 6498 -> 7934 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10676 -> 10676 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13059 -> 13059 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11170 -> 11170 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3858 -> 3858 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 6386 -> 6386 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../builder/Logic2VampireLanguageMapper.java | 17 +- .../builder/Logic2VampireLanguageMapperTrace.java | 4 + ...Logic2VampireLanguageMapper_RelationMapper.java | 92 +- .../output/FAMTest/Fam.logicproblem | 68 +- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 42 +- .../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 +- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 54 files changed, 999 insertions(+), 815 deletions(-) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index c9d38c7d..79732baf 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend @@ -198,7 +198,7 @@ class GenerationTaskExecutor { } // 7. Solver call - val solution = solver.solve(problem,solverConfig,reasonerWorkspaceForRun) + val ewsdzxA = solver.solve(problem,solverConfig,reasonerWorkspaceForRun) console.writeMessage(solution.soutionDescription.toString) // 8. Solution processing diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore index d8331ba8..81b2078f 100644 --- a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore +++ b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore @@ -9,11 +9,7 @@ - -
- - + volatile="true" transient="true" derived="true"/> @@ -25,11 +21,7 @@ - -
- - + changeable="false" volatile="true" transient="true" derived="true"/> - - - - - - @@ -12,13 +6,6 @@ - - - - - - - diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql b/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql index f0e48d42..15f70963 100644 --- a/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql +++ b/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql @@ -11,45 +11,46 @@ pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = { FunctionalInput.terminator(In,T); } -@QueryBasedFeature -pattern type(This : Function, Target : FunctionType) = { - find rootElements(_Model, This); - Target == FunctionType::Root; -} or { - neg find parent(_Child, This); - neg find rootElements(_Model, This); - Target == FunctionType::Leaf; -} or { - find parent(This, _Par); - find parent(_Child, This); - Target == FunctionType::Intermediate; -} - -pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = { - FunctionalArchitectureModel.rootElements(Model, Root); -} - -pattern parent(Func : Function, Par : Function) = { - Function.parent(Func, Par); -} - -@QueryBasedFeature -pattern model(This:FunctionalElement, Target: FunctionalArchitectureModel) { - FunctionalElement(This); - FunctionalArchitectureModel(Target); -} - -pattern hasRoot(F : Function) { - find rootElements(_Model, F); -} -pattern hasInt(F : Function) { - neg find parent(_Child, F); - neg find rootElements(_Model, F); -} -pattern hasLeaf(F : Function) { - find parent(F, _Par); - find parent(_Child, F); -} +//@QueryBasedFeature +//pattern type(This : Function, Target : FunctionType) = { +// find rootElements(_Model, This); +// Target == FunctionType::Root; +//} or { +// neg find parent(_Child, This); +// neg find rootElements(_Model, This); +// Target == FunctionType::Leaf; +//} or { +// find parent(This, _Par); +// find parent(_Child, This); +// Target == FunctionType::Intermediate; +//} +// +////@Constraint +//pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = { +// FunctionalArchitectureModel.rootElements(Model, Root); +//} +// +//pattern parent(Func : Function, Par : Function) = { +// Function.parent(Func, Par); +//} +// +//@QueryBasedFeature +//pattern model(This:FunctionalElement, Target: FunctionalArchitectureModel) { +// FunctionalElement(This); +// FunctionalArchitectureModel(Target); +//} +// +//pattern hasRoot(F : Function) { +// find rootElements(_Model, F); +//} +//pattern hasInt(F : Function) { +// neg find parent(_Child, F); +// neg find rootElements(_Model, F); +//} +//pattern hasLeaf(F : Function) { +// find parent(F, _Par); +// find parent(_Child, F); +//} /* @Constraint(message="noRoot", severity="error", key={fam}) pattern noRoot(fam: FunctionalArchitectureModel) { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/model/PartialInterpretation.aird b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/model/PartialInterpretation.aird index f2a97719..f18bce28 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/model/PartialInterpretation.aird +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/model/PartialInterpretation.aird @@ -1,38 +1,38 @@ - + PartialInterpretation.ecore platform:/resource/hu.bme.mit.inf.dslreasoner.logic.model/model/logicproblem.ecore platform:/resource/hu.bme.mit.inf.dslreasoner.logic.model/model/logiclanguage.ecore http://www.eclipse.org/emf/2002/Ecore - + - + - + - + - + - + - + - - - + + + @@ -66,7 +66,7 @@ - + @@ -273,6 +273,10 @@ + + + + @@ -649,683 +653,691 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + bold - + - + bold - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + - + - + - + - - + + labelSize bold - + labelSize - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - + bold - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor borderSize - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - + bold - + - + - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - + - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - - + + bold - + - - + + bold - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + - - + + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - - + + - + - - + + - + - - + + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - - + + bold - + - + - - + + bold - + - + - - + + bold - + - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - + strokeColor size - + labelSize labelColor - + labelSize labelColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic + + + + + + + + - + - - + + labelSize - + labelSize - + - + size - - + + - + - - + + strokeColor - - + + - + - - + + labelSize - + labelSize - + - - - + + + @@ -1353,7 +1365,7 @@ - + @@ -1817,547 +1829,547 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - - + + - + - - + + - + - - + + - + - - + + - + - + bold - + - + bold - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + labelSize bold - + labelSize - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - - + + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - - + + - + - - + + - + - - + + labelSize - + labelSize - + - - - + + + labelSize - + labelSize - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - - + + - + - - + + - + - - + + bold - + - + - - + + labelSize - + labelSize - + - - - + + + labelSize - + labelSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize italic - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize - + - + - + - + size - + labelSize - + labelSize - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - - + + labelSize - + labelSize - + - + size - + bold - + - + - + size - + bold - + - + - + size - + bold - + - + - - - - + + + + - + - - - + + + labelSize - + labelSize - + - + size - + bold - + - + - - - + + + @@ -2385,7 +2397,7 @@ - + @@ -3059,724 +3071,724 @@ - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - - + + - + - - + + - + - - + + - + - + bold - + - + bold - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + labelSize bold - + labelSize - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor borderSize - + - + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor italic - + - - + + bold - + - - + + bold - + - - + + labelSize - + labelSize - + - - + + labelSize - + labelSize - + - - + + - - + + - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + backgroundColor foregroundColor - + - + - + - + italic - + - + - + strokeColor size - + labelSize labelColor - + labelSize labelColor - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + - - + + labelSize bold - + labelSize - + - - + + labelSize - + labelSize - + - + size - + labelSize - + labelSize - + - + strokeColor - - + + - + - - + + labelSize - + labelSize - + - + - + labelSize - + labelSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + - + bold - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + bold - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + bold - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + bold - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + bold - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + borderSize - + - + bold - + - + bold - + - - + + labelSize - + labelSize - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + italic - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + - + - + italic - + - + KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + - + - + - + italic - + - + - + - - + + - + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index a0d8ad91..0aefc3c7 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index 7f0974a6..f93445d1 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index e814f9af..4266e495 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index acbea6c4..ff67b75e 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 2b006891..67f6087a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index 4c2a01e7..ebd73974 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index f712428d..cdb3137a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index db6e5d42..62560a49 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend index 4fc67b22..fe1c852f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend @@ -23,9 +23,9 @@ class VampireLanguageFormatter extends AbstractFormatter2 { for (VLSComment vLSComment : vampireModel.getComments()) { vLSComment.format; } -// for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { -// vLSFofFormula.format; -// } + for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { + vLSFofFormula.format; + } } // def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index bc9ce4bc..a60c74b4 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index 322bb058..63c46199 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index 2bd5f5f8..b3a43b5a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java index 0daa6fa5..48b973e7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.java @@ -29,6 +29,10 @@ public class VampireLanguageFormatter extends AbstractFormatter2 { for (final VLSComment vLSComment : _comments) { document.format(vLSComment); } + EList _formulas = vampireModel.getFormulas(); + for (final VLSFofFormula vLSFofFormula : _formulas) { + document.format(vLSFofFormula); + } } protected void _format(final VLSFofFormula formula, @Extension final IFormattableDocument document) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index c332270d..f3d705a1 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 60bd0c88..9e2e4cb2 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index fe1d6bf2..0ace8e93 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index a2449fc0..14926280 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -1,5 +1,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion @@ -21,18 +26,14 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral 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.RealLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import java.util.Collections import java.util.HashMap import java.util.List @@ -40,7 +41,7 @@ import java.util.Map import org.eclipse.xtend.lib.annotations.Accessors import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl class Logic2VampireLanguageMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -81,7 +82,8 @@ class Logic2VampireLanguageMapper { // RELATION MAPPER trace.relationDefinitions = problem.collectRelationDefinitions - problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] +// println(problem.relations.filter[class == RelationDefinitionImpl]) + problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)] // CONTAINMENT MAPPER containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) @@ -140,7 +142,7 @@ class Logic2VampireLanguageMapper { // //////////// def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { val res = createVLSFofFormula => [ - it.name = support.toID(assertion.name) + it.name = support.toID("assertion_" + assertion.name) // below is temporary solution it.fofRole = "axiom" it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) @@ -378,8 +380,18 @@ class Logic2VampireLanguageMapper { // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] // ] +// println(relation.name) +// if(relation.class == RelationDefinitionImpl) { +// println("(" + (relation as RelationDefinition).getDefines + ")") +// } return createVLSFunction => [ - it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant + if (relation.class == RelationDeclarationImpl) { + it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant + } + else { + it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant + } + it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] ] } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend index 6b383b12..13778dee 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -47,6 +47,8 @@ class Logic2VampireLanguageMapperTrace { public var Map relationDefinitions public var Map rel2Predicate = new HashMap public var Map predicate2Relation = new HashMap + public var Map relDef2Predicate = new HashMap + public var Map predicate2RelDef = new HashMap //NOT NEEDED //public var VLSFunction constantDec diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend new file mode 100644 index 00000000..cf218270 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_AssertionMapper.xtend @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +class Logic2VampireLanguageMapper_AssertionMapper { + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 18e97020..181c59ca 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend @@ -1,14 +1,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import java.util.ArrayList import java.util.HashMap import java.util.List @@ -25,7 +23,7 @@ class Logic2VampireLanguageMapper_RelationMapper { this.base = base } - def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { + def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { // 1. store all variables in support wrt their name // 1.1 if variable has type, creating list of type declarations @@ -81,91 +79,79 @@ class Logic2VampireLanguageMapper_RelationMapper { trace.specification.formulas += comply } - def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { - -// // 1. store all variables in support wrt their name -// // 1.1 if variable has type, creating list of type declarations -//// val VLSVariable variable = createVLSVariable => [it.name = "A"] -// val Map relationVar2VLS = new HashMap -// val Map relationVar2TypeDecComply = new HashMap -// val Map relationVar2TypeDecRes = new HashMap -// val typedefs = new ArrayList -// -// for (variable : reldef.variables) { -// val v = createVLSVariable => [ -// it.name = support.toIDMultiple("V", variable.name) -// ] -// relationVar2VLS.put(variable, v) -// -// val varTypeComply = createVLSFunction => [ -// it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) -// it.terms += support.duplicate(v) -// ] -// relationVar2TypeDecComply.put(variable, varTypeComply) -// relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) -// } -// val nameArray = reldef.name.split(" ") -// val comply = createVLSFofFormula => [ -// it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), -// nameArray.get(nameArray.length - 1)) -// it.fofRole = "axiom" -// it.fofFormula = createVLSUniversalQuantifier => [ -// for (variable : reldef.variables) { -// it.variables += support.duplicate(variable.lookup(relationVar2VLS)) -// -// } -// it.operand = createVLSImplies => [ -// it.left = createVLSFunction => [ -// it.constant = support.toIDMultiple("rel", reldef.name) -// for (variable : reldef.variables) { -// val v = createVLSVariable => [ -// it.name = variable.lookup(relationVar2VLS).name -// ] -// it.terms += v -// } -// ] -// it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) -// ] -// ] -// ] -// -// val res = createVLSFofFormula => [ -// it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), -// nameArray.get(nameArray.length - 1)) -// it.fofRole = "axiom" -// it.fofFormula = createVLSUniversalQuantifier => [ -// for (variable : reldef.variables) { -// val v = createVLSVariable => [ -// it.name = variable.lookup(relationVar2VLS).name -// ] -// it.variables += v -// -// } -// it.operand = createVLSImplies => [ -// it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) -// it.right = createVLSEquivalent => [ -// it.left = createVLSFunction => [ -// it.constant = support.toIDMultiple("rel", reldef.name) -// for (variable : reldef.variables) { -// val v = createVLSVariable => [ -// it.name = variable.lookup(relationVar2VLS).name -// ] -// it.terms += v -// -// } -// ] -// it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) -// ] -// -// ] -// -// ] -// -// ] -// -// // trace.relationDefinition2Predicate.put(r,res) -// trace.specification.formulas += comply; -// trace.specification.formulas += res; + def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { + +// println("XXXXXXXXXXXXXXXXX") + +// 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations + val Map relVar2VLS = new HashMap + val List vars = newArrayList + val List relVar2TypeDecComply = new ArrayList + for (i : 0 ..< r.parameters.length) { + + val v = createVLSVariable => [ + it.name = support.toIDMultiple("V", i.toString) + ] + relVar2VLS.put(r.variables.get(i), v) + vars.add(v) + + val relType = (r.parameters.get(i) as ComplexTypeReference).referred + val varTypeComply = support.duplicate(relType.lookup(trace.type2Predicate), v) + relVar2TypeDecComply.add(varTypeComply) + + } + + //deciding name of relation + val nameArray = r.name.split(" ") + var relNameVar = "" + if (nameArray.length == 3) { + relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) + } + else { + relNameVar = r.name + } + val relName = relNameVar + + //define logic for pattern +// val map = new HashMap +// map.put(r.variables.get(0), createVLSVariable) + val definition = mapper.transformTerm(r.value, trace, relVar2VLS) + + + + + //get entire contents of and + val compliance = support.unfoldAnd(relVar2TypeDecComply) + val compDefn = createVLSAnd=> [ + it.left = compliance + it.right = definition + ] + + val relDef = createVLSFofFormula=> [ + + it.name = support.toID(relName) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + for (v : vars) { + it.variables += support.duplicate(v) + } + it.operand = createVLSImplies => [ + val rel = createVLSFunction => [ + it.constant = support.toIDMultiple("r", relName) + for (v : vars) { + it.terms += support.duplicate(v) + } + ] + trace.relDef2Predicate.put(r, rel) + trace.predicate2RelDef.put(rel, r) + it.left = support.duplicate(rel) + it.right = compDefn + ] + ] + ] + + trace.specification.formulas += relDef } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index 5df47bbc..ef77b6ca 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend @@ -24,26 +24,28 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl import java.util.Arrays import java.util.HashMap import java.util.List import java.util.Map -import java.util.Set import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import java.util.concurrent.TimeUnit class VampireModelInterpretation implements LogicModelInterpretation { protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE protected val Logic2VampireLanguageMapperTrace forwardTrace; - //These three maps capture all the information found in the Vampire output + // These three maps capture all the information found in the Vampire output private val Map name2DefinedElement = new HashMap private val Map> type2DefinedElement = new HashMap - private val Map> rel2Inst = new HashMap - //end + private val Map> relDec2Inst = new HashMap + private val Map> relDef2Inst = new HashMap + // end public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { this.forwardTrace = trace @@ -77,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { // println() // println(trace.type2Predicate) // Fill keys of map + println(trace.type2Predicate.keySet) val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] val allTypeFunctions = trace.predicate2Type println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) @@ -86,52 +89,64 @@ class VampireModelInterpretation implements LogicModelInterpretation { } // USE THE DECLARE_ FORMULAS TO SEE WHAT THE TYPES ARE - val typeFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_t_"] + val typeFormulas = model.tfformulas.filter [ + name.length > 12 && (name.substring(0, 12) == "predicate_t_" || name.substring(0, 12) == "predicate_e_") + ] // ^this way, we ignore the "object" type - //TODO potentially need to handle the enums in this case as well + // TODO potentially need to handle the enums in this case as well for (formula : typeFormulas) { // get associated type val associatedTypeName = (formula as VLSTffFormula).name.substring(10) - val associatedFunction = allTypeFunctions.keySet.filter[constant == associatedTypeName]. - get(0) as VLSFunction - val associatedTypeAll = associatedFunction.lookup(allTypeFunctions) + print(associatedTypeName) + val associatedFunctions = allTypeFunctions.keySet.filter[constant == associatedTypeName] + if (associatedFunctions.length > 0) { + val associatedFunction = associatedFunctions.get(0) as VLSFunction + val associatedTypeAll = associatedFunction.lookup(allTypeFunctions) // val associatedTypeDeclFormula = model.tfformulas.filter[name == ("declare_t_" + associatedTypeName)].get(0) as VLSTffFormula // val associatedTypeDefn = associatedTypeDeclFormula.fofFormula as VLSOtherDeclaration // val associatedTypeFct = associatedTypeDefn.name as VLSConstant - if (associatedTypeAll.class == TypeDeclarationImpl) { - val associatedType = associatedTypeAll as TypeDeclaration + if (associatedTypeAll.class == TypeDeclarationImpl) { + val associatedType = associatedTypeAll as TypeDeclaration + + // get definedElements + var andFormulaTerm = formula.fofFormula + end = false + val List instances = newArrayList + while (!end) { + if (andFormulaTerm.class == VLSAndImpl) { + val andFormula = andFormulaTerm as VLSAnd + val andRight = andFormula.right + addIfNotNeg(andRight, instances) + andFormulaTerm = andFormula.left + } else { + addIfNotNeg(andFormulaTerm as VLSTerm, instances) + end = true + } - // get definedElements - var andFormulaTerm = formula.fofFormula - end = false - val List instances = newArrayList - while (!end) { - if (andFormulaTerm.class == VLSAndImpl) { - val andFormula = andFormulaTerm as VLSAnd - val andRight = andFormula.right - addIfNotNeg(andRight, instances) - andFormulaTerm = andFormula.left - } else { - addIfNotNeg(andFormulaTerm as VLSTerm, instances) - end = true } - - } - for (elem : instances) { - associatedType.lookup(type2DefinedElement).add(elem) + for (elem : instances) { + associatedType.lookup(type2DefinedElement).add(elem) + } } } + } - + printMap() - + // 3. get relations // Fill keys of map - val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl] - val allRelFunctions = trace.predicate2Relation + val allRelDecls = trace.rel2Predicate.keySet + val allRelDefns = trace.relDef2Predicate.keySet + val allRelDeclFunctions = trace.predicate2Relation + val allRelDefnFunctions = trace.predicate2RelDef for (rel : allRelDecls) { - rel2Inst.put(rel as RelationDeclaration, newArrayList) + relDec2Inst.put(rel as RelationDeclaration, newArrayList) + } + + for (rel : allRelDefns) { + relDef2Inst.put(rel as RelationDefinition, newArrayList) } // USE THE DECLARE_ FORMULAS TO SEE WHAT THE RELATIONS ARE @@ -140,34 +155,40 @@ class VampireModelInterpretation implements LogicModelInterpretation { for (formula : relFormulas) { // get associated type val associatedRelName = (formula as VLSTffFormula).name.substring(10) - val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName]. - get(0) as VLSFunction - val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration - - // get definedElements - var andFormulaTerm = formula.fofFormula - end = false - val List instances = newArrayList - while (!end) { - if (andFormulaTerm.class == VLSAndImpl) { - val andFormula = andFormulaTerm as VLSAnd - val andRight = andFormula.right - addRelIfNotNeg(andRight, instances) - andFormulaTerm = andFormula.left - } else { - addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) - end = true + + // TRY FOR DECLARATION + val associatedRelFunctionList = allRelDeclFunctions.keySet.filter[constant == associatedRelName] + if (associatedRelFunctionList.isEmpty) { + // THEN IT IS NOT A DECLARATION + } else { + val associatedRelFunction = associatedRelFunctionList.get(0) as VLSFunction // ASSUMING ONLY 1 SATISFIES QUERY + val associatedRel = associatedRelFunction.lookup(allRelDeclFunctions) as RelationDeclaration + + // get definedElements + var andFormulaTerm = formula.fofFormula + end = false + val List instances = newArrayList + while (!end) { + if (andFormulaTerm.class == VLSAndImpl) { + val andFormula = andFormulaTerm as VLSAnd + val andRight = andFormula.right + addRelIfNotNeg(andRight, instances) + andFormulaTerm = andFormula.left + } else { + addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) + end = true + } + + } + for (elem : instances) { + associatedRel.lookup(relDec2Inst).add(elem) } } - for (elem : instances) { - associatedRel.lookup(rel2Inst).add(elem) - } } // printMap2() - } def printMap() { @@ -182,12 +203,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { } println() } - + def printMap2() { println("------------------") - for (key : rel2Inst.keySet) { + for (key : relDec2Inst.keySet) { println(key.name + "==>") - for (elem : key.lookup(rel2Inst)) { + for (elem : key.lookup(relDec2Inst)) { print("[" + elem.get(0) + "-" + elem.get(1) + "], ") } println() @@ -203,7 +224,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { list.add(defnElem) } } - + def private addRelIfNotNeg(VLSTerm term, List list) { if (term.class != VLSUnaryNegationImpl) { val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor @@ -232,14 +253,19 @@ class VampireModelInterpretation implements LogicModelInterpretation { } override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { + print("-- " + relation.name) val node1 = (parameterSubstitution.get(0) as DefinedElement).name val node2 = (parameterSubstitution.get(1) as DefinedElement).name - val realRelations = relation.lookup(rel2Inst) - for (real : realRelations){ - if(real.contains(node1) && real.contains(node2)){ + val realRelations = relation.lookup(relDec2Inst) + for (real : realRelations) { + if (real.contains(node1) && real.contains(node2)) { + println(" true") + TimeUnit.SECONDS.sleep(1) return true } } + println(" false") + TimeUnit.SECONDS.sleep(1) return false } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index a1d6f783..972af7b4 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 6ac0457b..071db3ce 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index f5991439..b1e3b95d 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 0d6c8b61..31cc2f43 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index 659d4637..552bcd6c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 927327e1..680bcfe1 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index d8fc0296..9cc64d7c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index bc3caa3b..803b5fed 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 299c4e0c..0083e90f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index da8c1d26..7e8b1703 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index adc3fff4..081757ca 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 2ab5b32f..3471f95b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 41af19ec..1c707ca6 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 2b46d5c2..d8e3808c 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 58da7ccd..f8a65187 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -21,6 +21,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; +import com.google.common.base.Objects; import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; @@ -52,6 +53,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.Arrays; @@ -117,7 +119,8 @@ public class Logic2VampireLanguageMapper { } trace.relationDefinitions = this.collectRelationDefinitions(problem); final Consumer _function_3 = (Relation it) -> { - this.relationMapper.transformRelation(it, trace); + Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); + this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); }; problem.getRelations().forEach(_function_3); this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); @@ -169,7 +172,9 @@ public class Logic2VampireLanguageMapper { { VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toID(assertion.getName())); + String _name = assertion.getName(); + String _plus = ("assertion_" + _name); + it.setName(this.support.toID(_plus)); it.setFofRole("axiom"); it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); }; @@ -346,7 +351,13 @@ public class Logic2VampireLanguageMapper { protected VLSTerm _transformSymbolicReference(final Relation relation, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(CollectionsUtil.lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); + Class _class = relation.getClass(); + boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class); + if (_equals) { + it.setConstant(CollectionsUtil.lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); + } else { + it.setConstant(CollectionsUtil.lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant()); + } EList _terms = it.getTerms(); final Function1 _function_1 = (Term p) -> { return this.transformTerm(p, trace, variables); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 4e77d45d..22df456b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -55,6 +55,10 @@ public class Logic2VampireLanguageMapperTrace { public Map predicate2Relation = new HashMap(); + public Map relDef2Predicate = new HashMap(); + + public Map predicate2RelDef = new HashMap(); + public final Map relationVar2VLS = new HashMap(); public final Map relationVar2TypeDec = new HashMap(); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index 143d3db5..c175c72a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -17,11 +18,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.Arrays; +import java.util.HashMap; import java.util.List; +import java.util.Map; import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; import org.eclipse.xtext.xbase.lib.Extension; @@ -41,7 +46,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { this.base = base; } - public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { + public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { final List relVar2VLS = new ArrayList(); final List relVar2TypeDecComply = new ArrayList(); int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; @@ -109,19 +114,94 @@ public class Logic2VampireLanguageMapper_RelationMapper { _formulas.add(comply); } - public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { + public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { + final Map relVar2VLS = new HashMap(); + final List vars = CollectionLiterals.newArrayList(); + final List relVar2TypeDecComply = new ArrayList(); + int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); + for (final Integer i : _doubleDotLessThan) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("V", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + relVar2VLS.put(r.getVariables().get((i).intValue()), v); + vars.add(v); + TypeReference _get = r.getParameters().get((i).intValue()); + final Type relType = ((ComplexTypeReference) _get).getReferred(); + final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.lookup(relType, trace.type2Predicate), v); + relVar2TypeDecComply.add(varTypeComply); + } + } + final String[] nameArray = r.getName().split(" "); + String relNameVar = ""; + int _length_1 = nameArray.length; + boolean _equals = (_length_1 == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = r.getName(); + } + final String relName = relNameVar; + final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); + final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(compliance); + it.setRight(definition); + }; + final VLSAnd compDefn = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toID(relName)); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + for (final VLSVariable v : vars) { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(v); + _variables.add(_duplicate); + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_3 = (VLSImplies it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_4 = (VLSFunction it_3) -> { + it_3.setConstant(this.support.toIDMultiple("r", relName)); + for (final VLSVariable v_1 : vars) { + EList _terms = it_3.getTerms(); + VLSVariable _duplicate_1 = this.support.duplicate(v_1); + _terms.add(_duplicate_1); + } + }; + final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_4); + trace.relDef2Predicate.put(r, rel); + trace.predicate2RelDef.put(rel, r); + it_2.setLeft(this.support.duplicate(rel)); + it_2.setRight(compDefn); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula relDef = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(relDef); } - public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { + public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { if (r instanceof RelationDeclaration) { - _transformRelation((RelationDeclaration)r, trace); + _transformRelation((RelationDeclaration)r, trace, mapper); return; } else if (r instanceof RelationDefinition) { - _transformRelation((RelationDefinition)r, trace); + _transformRelation((RelationDefinition)r, trace, mapper); return; } else { throw new IllegalArgumentException("Unhandled parameter types: " + - Arrays.asList(r, trace).toString()); + Arrays.asList(r, trace, mapper).toString()); } } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index dcbb21eb..fe14bb31 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem @@ -1,5 +1,5 @@ - + @@ -496,6 +496,22 @@ + + + + + + + + + + + + + + + + @@ -556,11 +572,57 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -580,4 +642,6 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend index 1045189c..3c6a65ca 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend @@ -7,6 +7,7 @@ import functionalarchitecture.FunctionalArchitectureModel import functionalarchitecture.FunctionalInterface 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.logic.model.builder.DocumentationLevel @@ -14,15 +15,14 @@ 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.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.visualisation.pi2graphviz.GraphvizVisualiser import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl +import functionalarchitecture.FAMTerminator class FAMTest { def static void main(String[] args) { @@ -47,15 +47,15 @@ class FAMTest { // Load DSL val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") -// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) - val queries = null + val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) +// val queries = null println("DSL loaded") val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) var problem = modelGenerationProblem.output problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output -// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output workspace.writeModel(problem, "Fam.logicproblem") println("Problem created") @@ -73,7 +73,8 @@ class FAMTest { // classMapMin.put(FunctionalArchitectureModel, 1) // classMapMin.put(Function, 1) // classMapMin.put(FunctionalInterface, 2) - classMapMin.put(FunctionalOutput, 3) +// classMapMin.put(FunctionalOutput, 3) + classMapMin.put(FAMTerminator, 1) val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) @@ -93,7 +94,7 @@ class FAMTest { it.typeScopes.minNewElements = 4//24 it.typeScopes.maxNewElements = 5//25 -// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin + if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 it.uniquenessDuplicates = false @@ -108,22 +109,23 @@ class FAMTest { // Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) ) // ) // println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType) + print(interpretations.class) for (interpretation : interpretations) { val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) workspace.writeModel(model, "model.xmi") - val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations - if (representation instanceof PartialInterpretation) { - val vis1 = new PartialInterpretation2Gml - val gml = vis1.transform(representation) - workspace.writeText("model.gml", gml) - - val vis2 = new GraphvizVisualiser - val dot = vis2.visualiseConcretization(representation) - dot.writeToFile(workspace, "model.png") - } else { - println("ERROR") - } +// val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations +// if (representation instanceof PartialInterpretation) { +// val vis1 = new PartialInterpretation2Gml +// val gml = vis1.transform(representation) +// workspace.writeText("model.gml", gml) +// +// val vis2 = new GraphvizVisualiser +// val dot = vis2.visualiseConcretization(representation) +// dot.writeToFile(workspace, "model.png") +// } else { +// println("ERROR") +// } // look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor } 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(); 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 7ab6b54b..91c99504 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin 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 f7c267ec..dec17082 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin 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 index e91e816f..3c55afad 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf