From df12163128073296c4d811fa67b02e37ceb20179 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 5 Mar 2019 13:37:02 -0500 Subject: Implement type scope handling --- .../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 .../.VampireLanguageRuntimeModule.xtendbin | Bin 1706 -> 1706 bytes .../.VampireLanguageStandaloneSetup.xtendbin | Bin 1980 -> 1980 bytes .../formatting2/.VampireLanguageFormatter.xtendbin | Bin 4130 -> 4130 bytes .../generator/.VampireLanguageGenerator.xtendbin | Bin 2338 -> 2338 bytes .../scoping/.VampireLanguageScopeProvider.xtendbin | Bin 1751 -> 1751 bytes .../validation/.VampireLanguageValidator.xtendbin | Bin 1736 -> 1736 bytes .../builder/Logic2VampireLanguageMapper.xtend | 2 +- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 6 +- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 69 +- .../Logic2VampireLanguageMapper_Support.xtend | 28 +- ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 24 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2382 -> 2399 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5941 -> 5941 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18004 -> 18006 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3137 -> 3137 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8246 -> 8245 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 5890 -> 6090 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 9766 -> 10536 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 3223 -> 3223 bytes ...geMapper_TypeMapperTrace_FilteredTypes.xtendbin | Bin 2643 -> 2643 bytes ...anguageMapper_TypeMapper_FilteredTypes.xtendbin | Bin 9048 -> 8978 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../builder/Logic2VampireLanguageMapper.java | 2 +- ...Logic2VampireLanguageMapper_RelationMapper.java | 6 +- .../Logic2VampireLanguageMapper_ScopeMapper.java | 73 +- .../Logic2VampireLanguageMapper_Support.java | 36 +- ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 46 +- .../.classpath | 1 + .../.project | 6 + .../META-INF/MANIFEST.MF | 67 +- .../build.properties | 6 +- .../initialModels/FunctionalArchitectureModel.xmi | 2 + .../initialModels/FunctionalArchitectureModel2.xmi | 4 + .../initialModels/yakindu/yakindu.ecore | 26 + .../output/FAMTest/Fam.logicproblem | 272 +------- .../output/FAMTest/vampireProblem.tptp | 95 ++- .../output/MedicalSystem/vampireProblem.tptp | 6 +- .../output/VampireTest/vampireProblem.tptp | 8 +- .../plugin.xml | 8 +- .../ecse/dslreasoner/vampire/queries/.gitignore | 50 ++ .../dslreasoner/vampire/queries/FamPatterns.java | 53 ++ .../vampire/queries/TerminatorAndInformation.java | 747 +++++++++++++++++++++ .../ecse/dslreasoner/vampire/icse/EcoreTest.xtend | 6 +- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 8 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 52 +- .../dslreasoner/vampire/icse/YakinduTest.xtend | 6 +- .../dslreasoner/vampire/queries/FamPatterns.vql | 2 +- .../dslreasoner/vampire/test/MedicalSystem.xtend | 10 +- .../dslreasoner/vampire/test/VampireTest.xtend | 13 +- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6811 -> 6358 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 4111 -> 4155 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 4124 -> 4115 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 7276 -> 7655 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 3643 -> 4054 bytes .../ecse/dslreasoner/vampire/icse/EcoreTest.java | 3 +- .../ecse/dslreasoner/vampire/icse/FAMTest.java | 8 +- .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 4 +- .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 30 +- .../vampire/test/.MedicalSystem.xtendbin | Bin 4870 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6292 -> 6500 bytes .../ecse/dslreasoner/vampire/test/.gitignore | 12 +- .../dslreasoner/vampire/test/MedicalSystem.java | 3 +- .../ecse/dslreasoner/vampire/test/VampireTest.java | 4 +- 76 files changed, 1267 insertions(+), 537 deletions(-) create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java 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 7bfd4e09..fef8d621 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 4c4cd6a3..3c37bd02 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 dedb3ece..76127556 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 a6d502ef..467395cb 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 b2dc17a0..601c5a4c 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 73d9cdd1..c60c4d59 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 7880fdd6..030267ff 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 6a8836d4..ef7ffcdf 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/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 e0367170..219fec58 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 906c39f5..47712412 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 47a395a0..831f0df4 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/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index 74f517cf..696d67c0 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 3c09270e..9bef3ff9 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 96e8559a..dd65afb4 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 e2c15b75..54c44c72 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 @@ -238,7 +238,7 @@ class Logic2VampireLanguageMapper { def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map variables) { return createVLSFunction => [ - it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (instanceOf.range as ComplexTypeReference).referred.name) it.terms += instanceOf.value.transformTerm(trace, variables) ] } 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 60653a42..6f3b13ef 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 @@ -39,7 +39,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2VLS.put(variable, v) val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", variable.name) ] @@ -47,7 +47,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2TypeDecComply.put(variable, varTypeComply) val varTypeRes = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", variable.name) ] @@ -136,7 +136,7 @@ class Logic2VampireLanguageMapper_RelationMapper { relationVar2VLS.add(v) val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) + it.constant = support.toIDMultiple("t", (r.parameters.get(i) as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = support.toIDMultiple("Var", i.toString) ] diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 84aa521d..4b7ea3d0 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -18,7 +18,6 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { val VLSVariable variable = createVLSVariable => [it.name = "A"] - // 1. make a list of constants equaling the min number of specified objects val List instances = newArrayList for (var i = 0; i < config.typeScopes.minNewElements; i++) { @@ -28,47 +27,37 @@ class Logic2VampireLanguageMapper_ScopeMapper { ] instances.add(cst) } - - - // TODO: specify for the max - - // 2. Create initial fof formula to specify the number of elems - val cstDec = createVLSFofFormula => [ - it.name = "typeScope" - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += support.duplicate(variable) - // check below - it.operand = createVLSEquivalent => [ - it.left = support.topLevelTypeFunc - it.right = support.unfoldOr(instances.map [ i | - createVLSEquality => [ - it.left = createVLSVariable => [it.name = variable.name] - it.right = i - ] - ]) + // TODO: specify for the max + if (config.typeScopes.minNewElements != 0) { + // 2. Create initial fof formula to specify the number of elems + val cstDec = createVLSFofFormula => [ + it.name = "typeScope" + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + // check below + it.operand = createVLSEquivalent => [ + it.left = support.topLevelTypeFunc + it.right = support.unfoldOr(instances.map [ i | + createVLSEquality => [ + it.left = createVLSVariable => [it.name = variable.name] + it.right = i + ] + ]) + ] ] ] - ] - trace.specification.formulas += cstDec - - - // TODO: specify for scope per type - - - - // 3. Specify uniqueness of elements - val uniqueness = createVLSFofFormula => [ - it.name = "typeUniqueness" - it.fofRole = "axiom" - it.fofFormula = support.unfoldOr(instances.map [ i | - createVLSEquality => [ - it.left = createVLSVariable => [it.name = variable.name] - it.right = i - ] - ]) - ] - trace.specification.formulas += cstDec + trace.specification.formulas += cstDec + + // TODO: specify for scope per type + // 3. Specify uniqueness of elements + val uniqueness = createVLSFofFormula => [ + it.name = "typeUniqueness" + it.fofRole = "axiom" + it.fofFormula = support.establishUniqueness(instances) + ] + trace.specification.formulas += uniqueness + } } } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index e69f0d51..06ec585c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -13,6 +13,8 @@ import java.util.HashMap import java.util.List import java.util.Map import org.eclipse.emf.common.util.EList +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality class Logic2VampireLanguageMapper_Support { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -26,6 +28,7 @@ class Logic2VampireLanguageMapper_Support { ids.split("\\s+").join("_") } + //TODO Make more general def protected VLSVariable duplicate(VLSVariable vrbl) { return createVLSVariable => [it.name = vrbl.name] } @@ -38,6 +41,25 @@ class Logic2VampireLanguageMapper_Support { ] ] } + + //TODO Make more general + def establishUniqueness(List terms) { + val List eqs = newArrayList + for (t1 : terms.subList(1, terms.length)){ + for (t2 : terms.subList(0, terms.indexOf(t1))){ + val eq = createVLSInequality => [ + //TEMP + it.left = createVLSConstant => [it.name = t2.name] + it.right = createVLSConstant => [it.name = t1.name] + //TEMP + ] + eqs.add(eq) + } + } + + return unfoldAnd(eqs) + + } // Support Functions // booleans @@ -111,7 +133,7 @@ class Logic2VampireLanguageMapper_Support { val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { val eq = createVLSFunction => [ - it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = toIDMultiple("Var", variable.name) ] @@ -138,7 +160,7 @@ class Logic2VampireLanguageMapper_Support { val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { val eq = createVLSFunction => [ - it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.constant = toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) it.terms += createVLSVariable => [ it.name = toIDMultiple("Var", variable.name) ] @@ -157,5 +179,7 @@ class Logic2VampireLanguageMapper_Support { def protected withAddition(Map map1, Map map2) { new HashMap(map1) => [putAll(map2)] } + + } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend index eed10656..88e1e23a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -89,27 +89,25 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates // and store in a map -// val List type2PossibleNot = new ArrayList -// val List type2And = new ArrayList - for (type : types.filter[!isIsAbstract]) { - for (type2 : types) { + for (t1 : types.filter[!isIsAbstract]) { + for (t2 : types) { // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes - if (type == type2 || dfsSupertypeCheck(type, type2)) { - typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ - it.constant = type2.lookup(typeTrace.type2Predicate).constant - it.terms += createVLSVariable => [it.name = "A"] + if (t1 == t2 || dfsSupertypeCheck(t1, t2)) { + typeTrace.type2PossibleNot.put(t2, createVLSFunction => [ + it.constant = t2.lookup(typeTrace.type2Predicate).constant + it.terms += support.duplicate(variable) ]) } else { - typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ + typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ it.operand = createVLSFunction => [ - it.constant = type2.lookup(typeTrace.type2Predicate).constant - it.terms += createVLSVariable => [it.name = "A"] + it.constant = t2.lookup(typeTrace.type2Predicate).constant + it.terms += support.duplicate(variable) ] ]) } // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) } - typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) + typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) typeTrace.type2PossibleNot.clear } @@ -123,7 +121,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp it.name = "hierarchyHandler" it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ - it.variables += createVLSVariable => [it.name = "A"] + it.variables += support.duplicate(variable) it.operand = createVLSEquivalent => [ it.left = support.topLevelTypeFunc it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) 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 9a2a1b15..4a4eedf5 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 ce05b92c..55f0ac1e 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 379d0683..e91f89cc 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 76dd192f..154ff393 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 936ab9ca..5d6ad730 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_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 e0f442f5..7c787543 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 493ff288..34f3b285 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 13281767..f8d6cd3f 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 1a777880..7b2b11f8 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index e8658e7b..7e8336e2 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_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_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index aec1688a..a2229dba 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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 e77b9866..d82649ff 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 100a52b8..030a0be9 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 231c1995..87203ed8 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 b67a307c..65689b0c 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 89c9637e..6643576f 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 @@ -273,7 +273,7 @@ public class Logic2VampireLanguageMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { TypeReference _range = instanceOf.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); _terms.add(_transformTerm); 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 561402a7..bce50fcc 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 @@ -61,7 +61,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { @@ -75,7 +75,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); final Procedure1 _function_2 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_3 = (VLSVariable it_1) -> { @@ -215,7 +215,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _get = r.getParameters().get((i).intValue()); - it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); + it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _get).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 86d8b648..8967839d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -51,42 +51,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { instances.add(cst); } } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName("typeScope"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_3 = (VLSEquivalent it_2) -> { - it_2.setLeft(this.support.topLevelTypeFunc()); - final Function1 _function_4 = (VLSConstant i) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { - it_4.setName(variable.getName()); + if ((config.typeScopes.minNewElements != 0)) { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName("typeScope"); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_3 = (VLSEquivalent it_2) -> { + it_2.setLeft(this.support.topLevelTypeFunc()); + final Function1 _function_4 = (VLSConstant i) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_5 = (VLSEquality it_3) -> { + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_6 = (VLSVariable it_4) -> { + it_4.setName(variable.getName()); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_6); + it_3.setLeft(_doubleArrow); + it_3.setRight(i); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_6); - it_3.setLeft(_doubleArrow); - it_3.setRight(i); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(instances, _function_4))); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(instances, _function_4))); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + it_1.setOperand(_doubleArrow); }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); - it_1.setOperand(_doubleArrow); + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(cstDec); + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(cstDec); + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName("typeUniqueness"); + it.setFofRole("axiom"); + it.setFofFormula(this.support.establishUniqueness(instances)); + }; + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(uniqueness); + } } public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index b111732f..dfe624be 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.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.vampireLanguage.VLSAnd; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -25,6 +26,7 @@ import java.util.List; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.xtend2.lib.StringConcatenation; +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; @@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + public VLSTerm establishUniqueness(final List terms) { + final List eqs = CollectionLiterals.newArrayList(); + List _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); + for (final VLSConstant t1 : _subList) { + List _subList_1 = terms.subList(0, terms.indexOf(t1)); + for (final VLSConstant t2 : _subList_1) { + { + VLSInequality _createVLSInequality = this.factory.createVLSInequality(); + final Procedure1 _function = (VLSInequality it) -> { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function_1 = (VLSConstant it_1) -> { + it_1.setName(t2.getName()); + }; + VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_1); + it.setLeft(_doubleArrow); + VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); + final Procedure1 _function_2 = (VLSConstant it_1) -> { + it_1.setName(t1.getName()); + }; + VLSConstant _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSConstant_1, _function_2); + it.setRight(_doubleArrow_1); + }; + final VLSInequality eq = ObjectExtensions.operator_doubleArrow(_createVLSInequality, _function); + eqs.add(eq); + } + } + } + return this.unfoldAnd(eqs); + } + protected VLSTerm unfoldAnd(final List operands) { int _size = operands.size(); boolean _equals = (_size == 1); @@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { @@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); EList _terms = it.getTerms(); VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_2 = (VLSVariable it_1) -> { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 71e98871..1e845d94 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java @@ -115,47 +115,39 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log return Boolean.valueOf((!_isIsAbstract)); }; Iterable _filter_1 = IterableExtensions.filter(types, _function_1); - for (final Type type_2 : _filter_1) { + for (final Type t1 : _filter_1) { { - for (final Type type2 : types) { - if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { + for (final Type t2 : types) { + if ((Objects.equal(t1, t2) || this.dfsSupertypeCheck(t1, t2))) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_2 = (VLSFunction it) -> { - it.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + it.setConstant(CollectionsUtil.lookup(t2, typeTrace.type2Predicate).getConstant()); EList _terms = it.getTerms(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_1) -> { - it_1.setName("A"); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); - _terms.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); }; VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); - typeTrace.type2PossibleNot.put(type2, _doubleArrow); + typeTrace.type2PossibleNot.put(t2, _doubleArrow); } else { VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); final Procedure1 _function_3 = (VLSUnaryNegation it) -> { VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); final Procedure1 _function_4 = (VLSFunction it_1) -> { - it_1.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + it_1.setConstant(CollectionsUtil.lookup(t2, typeTrace.type2Predicate).getConstant()); EList _terms = it_1.getTerms(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_5 = (VLSVariable it_2) -> { - it_2.setName("A"); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_5); - _terms.add(_doubleArrow_1); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); }; VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_4); it.setOperand(_doubleArrow_1); }; VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); + typeTrace.type2PossibleNot.put(t2, _doubleArrow_1); } } Collection _values = typeTrace.type2PossibleNot.values(); ArrayList _arrayList = new ArrayList(_values); - typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); + typeTrace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); typeTrace.type2PossibleNot.clear(); } } @@ -166,21 +158,17 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { EList _variables = it_1.getVariables(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_2) -> { - it_2.setName("A"); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_4); - _variables.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_5 = (VLSEquivalent it_2) -> { + final Procedure1 _function_4 = (VLSEquivalent it_2) -> { it_2.setLeft(this.support.topLevelTypeFunc()); Collection _values = typeTrace.type2And.values(); ArrayList _arrayList = new ArrayList(_values); it_2.setRight(this.support.unfoldOr(_arrayList)); }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); - it_1.setOperand(_doubleArrow_1); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_1.setOperand(_doubleArrow); }; VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); it.setFofFormula(_doubleArrow); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath index 1c96fe2f..3f0838b6 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath @@ -3,6 +3,7 @@ + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project index eb3347d0..87dc2baa 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.project @@ -5,6 +5,11 @@ + + org.eclipse.viatra.query.tooling.ui.projectbuilder + + + org.eclipse.xtext.ui.shared.xtextBuilder @@ -30,5 +35,6 @@ org.eclipse.pde.PluginNature org.eclipse.jdt.core.javanature org.eclipse.xtext.ui.shared.xtextNature + org.eclipse.viatra.query.projectnature diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF index fedee0e4..1995ee52 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF @@ -1,31 +1,36 @@ -Manifest-Version: 1.0 -Bundle-ManifestVersion: 2 -Bundle-Name: Test -Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true -Bundle-Version: 1.0.0.qualifier -Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test -Bundle-RequiredExecutionEnvironment: JavaSE-1.8 -Require-Bundle: com.google.guava, - org.eclipse.xtext.xbase.lib, - org.eclipse.xtend.lib, - org.eclipse.xtend.lib.macro, - ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", - org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", - hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", - ModelGenExampleFAM_plugin;bundle-version="1.0.0", - ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", - org.eclipse.viatra.query.runtime;bundle-version="2.1.0", - org.eclipse.collections;bundle-version="9.2.0", - hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0" - +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Test +Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true +Bundle-Version: 1.0.0.qualifier +Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries +Require-Bundle: org.eclipse.emf.ecore, + org.eclipse.viatra.query.runtime.rete, + org.eclipse.viatra.query.runtime.localsearch, + com.google.guava, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + org.eclipse.xtend.lib.macro, + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", + org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", + hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", + ModelGenExampleFAM_plugin;bundle-version="1.0.0", + ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", + org.eclipse.viatra.query.runtime;bundle-version="2.1.0", + org.eclipse.collections;bundle-version="9.2.0", + hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Import-Package: org.apache.log4j +Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties index 41eb6ade..efae4b07 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/build.properties @@ -1,4 +1,6 @@ -source.. = src/ -output.. = bin/ bin.includes = META-INF/,\ . +source.. = src/,\ + src-gen/,\ + src-gen/ +output.. = bin/ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi index 61256334..8500678c 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel.xmi @@ -7,4 +7,6 @@ xsi:schemaLocation="http://www.inf.mit.bme.hu/viatrasolver/example/fam ../../ModelGenExampleFAM_plugin/model/FamMetamodel.ecore"> + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi new file mode 100644 index 00000000..59935a2c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FunctionalArchitectureModel2.xmi @@ -0,0 +1,4 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore new file mode 100644 index 00000000..0c944db8 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore @@ -0,0 +1,26 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + 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 5792ceed..a0b5d6ea 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,7 +1,7 @@ - + @@ -10,8 +10,6 @@ - - @@ -496,7 +494,7 @@ - + @@ -505,7 +503,7 @@ - + @@ -572,235 +570,7 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + @@ -816,12 +586,12 @@ - - + + - - + + @@ -831,16 +601,12 @@ - - - - - - + + - - + + @@ -849,8 +615,7 @@ - - + @@ -870,13 +635,6 @@ - - - - - - - - - + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index 242c404c..1f220d6f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp @@ -1,55 +1,42 @@ % This is an initial Test Comment -fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( type_FunctionType_enum ( A ) <=> ( A = "aRoot literal FunctionType" | ( A = "aIntermediate literal FunctionType" | A = "aLeaf literal FunctionType" ) ) ) ) . -fof ( typeDef_FunctionalArchitectureModel_class_DefinedPart , axiom , ! [ A ] : ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) <=> A = "ao 1" ) ) . -fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_FunctionType_enum ( A ) & ( type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( type_FunctionalInput_class ( A ) & ~ type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_FunctionType_enum ( A ) & ( ~ type_FunctionalData_class ( A ) & ( ~ type_Function_class ( A ) & ( ~ type_InformationLink_class ( A ) & ( ~ type_FunctionalOutput_class ( A ) & ( ~ type_FunctionalArchitectureModel_class ( A ) & ( ~ type_FunctionalElement_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_DefinedPart ( A ) & ( ~ type_FAMTerminator_class ( A ) & ( ~ type_FunctionalArchitectureModel_class_UndefinedPart ( A ) & ( ~ type_FunctionalInput_class ( A ) & type_FunctionalInterface_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . -fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) . -fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) . -fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( type_FunctionalElement_class ( Var_0 ) & type_Function_class ( Var_1 ) ) ) ) . -fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( type_FunctionalArchitectureModel_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( type_FAMTerminator_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) . -fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalOutput_class ( Var_1 ) ) ) ) . -fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( type_InformationLink_class ( Var_0 ) & type_FunctionalInput_class ( Var_1 ) ) ) ) . -fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalData_class ( Var_1 ) ) ) ) . -fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( type_FunctionalInterface_class ( Var_0 ) & type_FunctionalElement_class ( Var_1 ) ) ) ) . -fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( type_FunctionalInput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) . -fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( type_FunctionalOutput_class ( Var_0 ) & type_InformationLink_class ( Var_1 ) ) ) ) . -fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FAMTerminator_class ( Var_1 ) ) ) ) . -fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( type_FunctionalData_class ( Var_0 ) & type_FunctionalInterface_class ( Var_1 ) ) ) ) . -fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( type_Function_class ( Var_0 ) & type_FunctionType_enum ( Var_1 ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasRoot ( Var_parameter_F ) <=> ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasInt ( Var_parameter_F ) <=> ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_F ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) & ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_F ) ) ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) => type_Function_class ( Var_parameter_F ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf , axiom , ! [ Var_parameter_F ] : ( type_Function_class ( Var_parameter_F ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_hasLeaf ( Var_parameter_F ) <=> ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_F , Var_variable_Par ) & rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_F ) ) ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Target ) & type_FunctionalElement_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_model ( Var_parameter_This , Var_parameter_Target ) <=> ( type_FunctionalElement_class ( Var_parameter_This ) & type_FunctionalArchitectureModel_class ( Var_parameter_Target ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) => ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements , axiom , ! [ Var_parameter_Model , Var_parameter_Root ] : ( ( type_FunctionalArchitectureModel_class ( Var_parameter_Model ) & type_Function_class ( Var_parameter_Root ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_parameter_Model , Var_parameter_Root ) <=> ( type_Function_class ( Var_parameter_Root ) & rel_rootElements_reference_FunctionalArchitectureModel ( Var_parameter_Model , Var_parameter_Root ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) => ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type , axiom , ! [ Var_parameter_This , Var_parameter_Target ] : ( ( type_FunctionType_enum ( Var_parameter_Target ) & type_Function_class ( Var_parameter_This ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_type ( Var_parameter_This , Var_parameter_Target ) <=> ( ? [ Var_variable_Model ] : ( type_FunctionalArchitectureModel_class ( Var_variable_Model ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aRoot literal FunctionType" ) ) | ( ! [ Var_variable_Child , Var_variable_Model ] : ( ( type_Function_class ( Var_variable_Child ) & type_FunctionalArchitectureModel_class ( Var_variable_Model ) ) => ( type_Function_class ( Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & ( ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_rootElements ( Var_variable_Model , Var_parameter_This ) & Var_parameter_Target = "aLeaf literal FunctionType" ) ) ) ) | ? [ Var_variable_Par , Var_variable_Child ] : ( type_Function_class ( Var_variable_Par ) & ( type_Function_class ( Var_variable_Child ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_This , Var_variable_Par ) & ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_variable_Child , Var_parameter_This ) & Var_parameter_Target = "aIntermediate literal FunctionType" ) ) ) ) ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) => ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent , axiom , ! [ Var_parameter_Func , Var_parameter_Par ] : ( ( type_Function_class ( Var_parameter_Par ) & type_Function_class ( Var_parameter_Func ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_parent ( Var_parameter_Func , Var_parameter_Par ) <=> ( type_Function_class ( Var_parameter_Func ) & ( rel_parent_reference_FunctionalElement ( Var_parameter_Func , Var_parameter_Par ) & type_Function_class ( Var_parameter_Par ) ) ) ) ) ) . -fof ( compliance_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) ) ) . -fof ( relation_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( type_FAMTerminator_class ( Var_parameter_T ) & type_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( type_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( type_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & ( type_FunctionalInput_class ( Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) ) . -fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( type_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . -fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_FunctionalArchitectureModel_class ( Var_trg_1 ) & type_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalElement_class ( Var_src ) & ( type_Function_class ( Var_trg_1 ) & type_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FAMTerminator_class ( Var_src ) & ( type_FunctionalData_class ( Var_trg_1 ) & type_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalOutput_class ( Var_trg_1 ) & type_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( type_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) . -fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_InformationLink_class ( Var_src ) & ( type_FunctionalInput_class ( Var_trg_1 ) & type_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalInterface_class ( Var_src ) & ( type_FunctionalElement_class ( Var_trg_1 ) & type_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FAMTerminator_class ( Var_trg_1 ) & type_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_FunctionalData_class ( Var_src ) & ( type_FunctionalInterface_class ( Var_trg_1 ) & type_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) . -fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalElement_class ( Var_src ) & type_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) . -fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( type_FAMTerminator_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . -fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) . -fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( type_InformationLink_class ( Var_src ) & type_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) . -fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( type_FunctionalInterface_class ( Var_src ) & type_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . -fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( type_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( type_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) . -fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Function_class ( Var_src ) & ( type_FunctionType_enum ( Var_trg_1 ) & type_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . -fof ( errorpattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( type_FAMTerminator_class ( Var_p0 ) & type_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_hu_bme_mit_inf_dslreasoner_domains_transima_fam_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) . +fof ( typeDef_FunctionType_enum , axiom , ! [ A ] : ( t_FunctionType_enum ( A ) <=> ( e_Root_literal_FunctionType_FunctionType_enum ( A ) | ( e_Intermediate_literal_FunctionType_FunctionType_enum ( A ) | e_Leaf_literal_FunctionType_FunctionType_enum ( A ) ) ) ) ) . +fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( t_FunctionalInterface_class ( A ) & ~ t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_InformationLink_class ( A ) & ( ~ t_FunctionType_enum ( A ) & ( ~ t_FunctionalData_class ( A ) & ( ~ t_FunctionalOutput_class ( A ) & ( ~ t_Function_class ( A ) & ( ~ t_FunctionalInput_class ( A ) & ( ~ t_FunctionalArchitectureModel_class ( A ) & ( ~ t_FunctionalElement_class ( A ) & ( ~ t_FunctionalInterface_class ( A ) & t_FAMTerminator_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) . +fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & ( o3 != o4 & ( o1 != o5 & ( o2 != o5 & ( o3 != o5 & o4 != o5 ) ) ) ) ) ) ) ) ) . +fof ( compliance_interface_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . +fof ( compliance_model_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_model_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_FunctionalArchitectureModel_class ( Var_1 ) ) ) ) . +fof ( compliance_parent_reference_FunctionalElement , axiom , ! [ Var_0 , Var_1 ] : ( rel_parent_reference_FunctionalElement ( Var_0 , Var_1 ) => ( t_FunctionalElement_class ( Var_0 ) & t_Function_class ( Var_1 ) ) ) ) . +fof ( compliance_rootElements_reference_FunctionalArchitectureModel , axiom , ! [ Var_0 , Var_1 ] : ( rel_rootElements_reference_FunctionalArchitectureModel ( Var_0 , Var_1 ) => ( t_FunctionalArchitectureModel_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . +fof ( compliance_subElements_reference_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_subElements_reference_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . +fof ( compliance_data_reference_FAMTerminator , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FAMTerminator ( Var_0 , Var_1 ) => ( t_FAMTerminator_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . +fof ( compliance_from_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_from_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalOutput_class ( Var_1 ) ) ) ) . +fof ( compliance_to_reference_InformationLink , axiom , ! [ Var_0 , Var_1 ] : ( rel_to_reference_InformationLink ( Var_0 , Var_1 ) => ( t_InformationLink_class ( Var_0 ) & t_FunctionalInput_class ( Var_1 ) ) ) ) . +fof ( compliance_data_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_data_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalData_class ( Var_1 ) ) ) ) . +fof ( compliance_element_reference_FunctionalInterface , axiom , ! [ Var_0 , Var_1 ] : ( rel_element_reference_FunctionalInterface ( Var_0 , Var_1 ) => ( t_FunctionalInterface_class ( Var_0 ) & t_FunctionalElement_class ( Var_1 ) ) ) ) . +fof ( compliance_IncomingLinks_reference_FunctionalInput , axiom , ! [ Var_0 , Var_1 ] : ( rel_IncomingLinks_reference_FunctionalInput ( Var_0 , Var_1 ) => ( t_FunctionalInput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . +fof ( compliance_outgoingLinks_reference_FunctionalOutput , axiom , ! [ Var_0 , Var_1 ] : ( rel_outgoingLinks_reference_FunctionalOutput ( Var_0 , Var_1 ) => ( t_FunctionalOutput_class ( Var_0 ) & t_InformationLink_class ( Var_1 ) ) ) ) . +fof ( compliance_terminator_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_terminator_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FAMTerminator_class ( Var_1 ) ) ) ) . +fof ( compliance_interface_reference_FunctionalData , axiom , ! [ Var_0 , Var_1 ] : ( rel_interface_reference_FunctionalData ( Var_0 , Var_1 ) => ( t_FunctionalData_class ( Var_0 ) & t_FunctionalInterface_class ( Var_1 ) ) ) ) . +fof ( compliance_type_attribute_Function , axiom , ! [ Var_0 , Var_1 ] : ( rel_type_attribute_Function ( Var_0 , Var_1 ) => ( t_Function_class ( Var_0 ) & t_FunctionType_enum ( Var_1 ) ) ) ) . +fof ( compliance_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) => ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) ) ) . +fof ( relation_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_parameter_T , Var_parameter_I ] : ( ( t_FAMTerminator_class ( Var_parameter_T ) & t_InformationLink_class ( Var_parameter_I ) ) => ( rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_parameter_T , Var_parameter_I ) <=> ( ? [ Var_variable_Out ] : ( t_FunctionalOutput_class ( Var_variable_Out ) & ( rel_outgoingLinks_reference_FunctionalOutput ( Var_variable_Out , Var_parameter_I ) & rel_terminator_reference_FunctionalData ( Var_variable_Out , Var_parameter_T ) ) ) | ? [ Var_variable_In ] : ( t_FunctionalInput_class ( Var_variable_In ) & ( rel_to_reference_InformationLink ( Var_parameter_I , Var_variable_In ) & rel_terminator_reference_FunctionalData ( Var_variable_In , Var_parameter_T ) ) ) ) ) ) ) . +fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ Var_src ] : ( t_FunctionalElement_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) ) ) ) . +fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_FunctionalArchitectureModel_class ( Var_trg_1 ) & t_FunctionalArchitectureModel_class ( Var_trg_2 ) ) ) => ( ( rel_model_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_model_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalElement_class ( Var_src ) & ( t_Function_class ( Var_trg_1 ) & t_Function_class ( Var_trg_2 ) ) ) => ( ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg_1 ) & rel_parent_reference_FunctionalElement ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FAMTerminator_class ( Var_src ) & ( t_FunctionalData_class ( Var_trg_1 ) & t_FunctionalData_class ( Var_trg_2 ) ) ) => ( ( rel_data_reference_FAMTerminator ( Var_src , Var_trg_1 ) & rel_data_reference_FAMTerminator ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_from_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalOutput_class ( Var_trg_1 ) & t_FunctionalOutput_class ( Var_trg_2 ) ) ) => ( ( rel_from_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_from_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ Var_src ] : ( t_InformationLink_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionalInput_class ( Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) ) ) ) . +fof ( upperMultiplicity_to_InformationLink , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_InformationLink_class ( Var_src ) & ( t_FunctionalInput_class ( Var_trg_1 ) & t_FunctionalInput_class ( Var_trg_2 ) ) ) => ( ( rel_to_reference_InformationLink ( Var_src , Var_trg_1 ) & rel_to_reference_InformationLink ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalInterface_class ( Var_src ) & ( t_FunctionalElement_class ( Var_trg_1 ) & t_FunctionalElement_class ( Var_trg_2 ) ) ) => ( ( rel_element_reference_FunctionalInterface ( Var_src , Var_trg_1 ) & rel_element_reference_FunctionalInterface ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FAMTerminator_class ( Var_trg_1 ) & t_FAMTerminator_class ( Var_trg_2 ) ) ) => ( ( rel_terminator_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_terminator_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_FunctionalData_class ( Var_src ) & ( t_FunctionalInterface_class ( Var_trg_1 ) & t_FunctionalInterface_class ( Var_trg_2 ) ) ) => ( ( rel_interface_reference_FunctionalData ( Var_src , Var_trg_1 ) & rel_interface_reference_FunctionalData ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_FunctionalInterface_class ( Var_trg ) ) => ( rel_interface_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_element_reference_FunctionalInterface ( Var_trg , Var_src ) ) ) ) . +fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalElement_class ( Var_src ) & t_Function_class ( Var_trg ) ) => ( rel_parent_reference_FunctionalElement ( Var_src , Var_trg ) <=> rel_subElements_reference_Function ( Var_trg , Var_src ) ) ) ) . +fof ( oppositeReference_data_FAMTerminator , axiom , ! [ Var_src , Var_trg ] : ( ( t_FAMTerminator_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FAMTerminator ( Var_src , Var_trg ) <=> rel_terminator_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . +fof ( oppositeReference_from_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalOutput_class ( Var_trg ) ) => ( rel_from_reference_InformationLink ( Var_src , Var_trg ) <=> rel_outgoingLinks_reference_FunctionalOutput ( Var_trg , Var_src ) ) ) ) . +fof ( oppositeReference_to_InformationLink , axiom , ! [ Var_src , Var_trg ] : ( ( t_InformationLink_class ( Var_src ) & t_FunctionalInput_class ( Var_trg ) ) => ( rel_to_reference_InformationLink ( Var_src , Var_trg ) <=> rel_IncomingLinks_reference_FunctionalInput ( Var_trg , Var_src ) ) ) ) . +fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ Var_src , Var_trg ] : ( ( t_FunctionalInterface_class ( Var_src ) & t_FunctionalData_class ( Var_trg ) ) => ( rel_data_reference_FunctionalInterface ( Var_src , Var_trg ) <=> rel_interface_reference_FunctionalData ( Var_trg , Var_src ) ) ) ) . +fof ( lowerMultiplicity_type_Function , axiom , ! [ Var_src ] : ( t_Function_class ( Var_src ) => ? [ Var_trg_1 ] : ( t_FunctionType_enum ( Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_1 ) ) ) ) . +fof ( upperMultiplicity_type_Function , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( t_Function_class ( Var_src ) & ( t_FunctionType_enum ( Var_trg_1 ) & t_FunctionType_enum ( Var_trg_2 ) ) ) => ( ( rel_type_attribute_Function ( Var_src , Var_trg_1 ) & rel_type_attribute_Function ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . +fof ( errorpattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation , axiom , ! [ Var_p0 , Var_p1 ] : ( ( t_FAMTerminator_class ( Var_p0 ) & t_InformationLink_class ( Var_p1 ) ) => ~ rel_pattern_ca_mcgill_ecse_dslreasoner_vampire_queries_terminatorAndInformation ( Var_p0 , Var_p1 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp index aa088242..c23afb9a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/MedicalSystem/vampireProblem.tptp @@ -1,6 +1,6 @@ % This is an initial Test Comment fof ( typeDef_HealthSystem_class_DefinedPart , axiom , ! [ A ] : ( type_HealthSystem_class_DefinedPart ( A ) <=> A = "ao 1" ) ) . -fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_Allergy_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_HealthSystem_class ( A ) & ( type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_Allergy_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( type_Medication_class ( A ) & ~ type_HealthProblem_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( type_Immunization_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( ~ type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & ~ type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ type_MedicalRecord_class ( A ) & ( ~ type_Medicine_class ( A ) & ( ~ type_ExaminationResult_class ( A ) & ( ~ type_HealthSystem_class_DefinedPart ( A ) & ( ~ type_Patient_class ( A ) & ( ~ type_HealthSystem_class_UndefinedPart ( A ) & ( ~ type_Immunization_class ( A ) & ( type_Treatment_class ( A ) & ( ~ type_Disease_class ( A ) & ( ~ type_HealthSystem_class ( A ) & ( ~ type_Examination_class ( A ) & ( ~ type_Injury_class ( A ) & ( ~ type_Allergy_class ( A ) & ( ~ type_Symptom_class ( A ) & ( ~ type_HealthProblem_class ( A ) & type_Medication_class ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . fof ( compliance_records_reference_Patient , axiom , ! [ Var_0 , Var_1 ] : ( rel_records_reference_Patient ( Var_0 , Var_1 ) => ( type_Patient_class ( Var_0 ) & type_MedicalRecord_class ( Var_1 ) ) ) ) . fof ( compliance_healthsystem_reference_Patient , axiom , ! [ Var_0 , Var_1 ] : ( rel_healthsystem_reference_Patient ( Var_0 , Var_1 ) => ( type_Patient_class ( Var_0 ) & type_HealthSystem_class ( Var_1 ) ) ) ) . fof ( compliance_patient_reference_HealthSystem , axiom , ! [ Var_0 , Var_1 ] : ( rel_patient_reference_HealthSystem ( Var_0 , Var_1 ) => ( type_HealthSystem_class ( Var_0 ) & type_Patient_class ( Var_1 ) ) ) ) . @@ -35,8 +35,8 @@ fof ( compliance_pattern_ca_mcgill_dp19_queries_allergy , axiom , ! [ Var_parame fof ( relation_pattern_ca_mcgill_dp19_queries_allergy , axiom , ! [ Var_parameter_mr , Var_parameter_al ] : ( ( type_Allergy_class ( Var_parameter_al ) & type_MedicalRecord_class ( Var_parameter_mr ) ) => ( rel_pattern_ca_mcgill_dp19_queries_allergy ( Var_parameter_mr , Var_parameter_al ) <=> ( type_Allergy_class ( Var_parameter_al ) & rel_pattern_ca_mcgill_dp19_queries_healthProblems ( Var_parameter_mr , Var_parameter_al ) ) ) ) ) . fof ( compliance_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom , axiom , ! [ Var_parameter_mr ] : ( rel_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom ( Var_parameter_mr ) => type_MedicalRecord_class ( Var_parameter_mr ) ) ) . fof ( relation_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom , axiom , ! [ Var_parameter_mr ] : ( type_MedicalRecord_class ( Var_parameter_mr ) => ( rel_pattern_ca_mcgill_dp19_queries_allergyWithoutSymptom ( Var_parameter_mr ) <=> ? [ Var_variable_al ] : ( type_Allergy_class ( Var_variable_al ) & ! [ Var_variable_0 ] : ( type_Symptom_class ( Var_variable_0 ) => ( rel_pattern_ca_mcgill_dp19_queries_allergy ( Var_parameter_mr , Var_variable_al ) & ~ rel_pattern_ca_mcgill_dp19_queries_symptom ( Var_parameter_mr , Var_variable_0 ) ) ) ) ) ) ) . -fof ( compliance_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) => ( type_Medicine_class ( Var_parameter_med ) & type_HealthProblem_class ( Var_parameter_hp ) ) ) ) . -fof ( relation_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( ( type_Medicine_class ( Var_parameter_med ) & type_HealthProblem_class ( Var_parameter_hp ) ) => ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) <=> ( rel_recommended_medicine_reference_HealthProblem ( Var_parameter_hp , Var_parameter_med ) & type_Medicine_class ( Var_parameter_med ) ) ) ) ) . +fof ( compliance_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) => ( type_HealthProblem_class ( Var_parameter_hp ) & type_Medicine_class ( Var_parameter_med ) ) ) ) . +fof ( relation_pattern_ca_mcgill_dp19_queries_recommended , axiom , ! [ Var_parameter_hp , Var_parameter_med ] : ( ( type_HealthProblem_class ( Var_parameter_hp ) & type_Medicine_class ( Var_parameter_med ) ) => ( rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_parameter_hp , Var_parameter_med ) <=> ( rel_recommended_medicine_reference_HealthProblem ( Var_parameter_hp , Var_parameter_med ) & type_Medicine_class ( Var_parameter_med ) ) ) ) ) . fof ( compliance_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended , axiom , ! [ Var_parameter_mr , Var_parameter_med ] : ( rel_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended ( Var_parameter_mr , Var_parameter_med ) => ( type_Medicine_class ( Var_parameter_med ) & type_MedicalRecord_class ( Var_parameter_mr ) ) ) ) . fof ( relation_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended , axiom , ! [ Var_parameter_mr , Var_parameter_med ] : ( ( type_Medicine_class ( Var_parameter_med ) & type_MedicalRecord_class ( Var_parameter_mr ) ) => ( rel_pattern_ca_mcgill_dp19_queries_prescribedMedicineNotRecommended ( Var_parameter_mr , Var_parameter_med ) <=> ? [ Var_variable_hp , Var_variable_tr ] : ( type_HealthProblem_class ( Var_variable_hp ) & ( type_Treatment_class ( Var_variable_tr ) & ( rel_pattern_ca_mcgill_dp19_queries_healthProblems ( Var_parameter_mr , Var_variable_hp ) & ( rel_pattern_ca_mcgill_dp19_queries_treatment ( Var_parameter_mr , Var_variable_tr ) & ( rel_medicine_reference_Treatment ( Var_variable_tr , Var_parameter_med ) & ( type_Medicine_class ( Var_parameter_med ) & ~ rel_pattern_ca_mcgill_dp19_queries_recommended ( Var_variable_hp , Var_parameter_med ) ) ) ) ) ) ) ) ) ) . fof ( upperMultiplicity_healthsystem_Patient , axiom , ! [ Var_src , Var_trg_1 , Var_trg_2 ] : ( ( type_Patient_class ( Var_src ) & ( type_HealthSystem_class ( Var_trg_1 ) & type_HealthSystem_class ( Var_trg_2 ) ) ) => ( ( rel_healthsystem_reference_Patient ( Var_src , Var_trg_1 ) & rel_healthsystem_reference_Patient ( Var_src , Var_trg_2 ) ) => ~ Var_trg_1 != Var_trg_2 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp index a4afb86e..4c368859 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/VampireTest/vampireProblem.tptp @@ -1 +1,7 @@ -% This is an initial Test Comment fof ( typeDef_oldRPS , axiom , ! [ A ] : ( type_oldRPS ( A ) <=> ( A = "aRock" | ( A = "aPaper" | A = "aScissor" ) ) ) ) . fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> type_oldRPS ( A ) ) ) . fof ( compliance_beats2 , axiom , ! [ Var_0 , Var_1 ] : ( rel_beats2 ( Var_0 , Var_1 ) => ( type_oldRPS ( Var_0 ) & type_oldRPS ( Var_1 ) ) ) ) . fof ( assertion1 , axiom , ! [ Var_x ] : ( type_oldRPS ( Var_x ) => ? [ Var_y ] : ( type_oldRPS ( Var_y ) & ( rel_beats2 ( Var_x , Var_y ) & ( Var_x != Var_y & ~ rel_beats2 ( Var_y , Var_x ) ) ) ) ) ) . \ No newline at end of file +% This is an initial Test Comment +fof ( typeDef_oldRPS , axiom , ! [ A ] : ( t_oldRPS ( A ) <=> ( e_Rock_oldRPS ( A ) | ( e_Paper_oldRPS ( A ) | e_Scissor_oldRPS ( A ) ) ) ) ) . +fof ( hierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> t_oldRPS ( A ) ) ) . +fof ( typeScope , axiom , ! [ A ] : ( object ( A ) <=> ( A = o1 | ( A = o2 | ( A = o3 | A = o4 ) ) ) ) ) . +fof ( typeUniqueness , axiom , o1 != o2 & ( o1 != o3 & ( o2 != o3 & ( o1 != o4 & ( o2 != o4 & o3 != o4 ) ) ) ) ) . +fof ( compliance_beats2 , axiom , ! [ Var_0 , Var_1 ] : ( rel_beats2 ( Var_0 , Var_1 ) => ( t_oldRPS ( Var_0 ) & t_oldRPS ( Var_1 ) ) ) ) . +fof ( assertion1 , axiom , ! [ Var_x ] : ( t_oldRPS ( Var_x ) => ? [ Var_y ] : ( t_oldRPS ( Var_y ) & ( rel_beats2 ( Var_x , Var_y ) & ( Var_x != Var_y & ~ rel_beats2 ( Var_y , Var_x ) ) ) ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml index 2f4febdb..38efb459 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml @@ -1 +1,7 @@ - + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore new file mode 100644 index 00000000..96fc598c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/.gitignore @@ -0,0 +1,50 @@ +/.EntryInRegion_M0.java._trace +/.EntryInRegion_M1.java._trace +/.EntryInRegion_M2.java._trace +/.FamPatterns.java._trace +/.MultipleEntryInRegion_M0.java._trace +/.MultipleEntryInRegion_M1.java._trace +/.MultipleEntryInRegion_M2.java._trace +/.MultipleEntryInRegion_M3.java._trace +/.MultipleEntryInRegion_M4.java._trace +/.MultipleEntryInRegion_M5.java._trace +/.NoEntryInRegion_M0.java._trace +/.NoEntryInRegion_M1.java._trace +/.NoEntryInRegion_M2.java._trace +/.NoEntryInRegion_M3.java._trace +/.NoEntryInRegion_M4.java._trace +/.NoEntryInRegion_M5.java._trace +/.TerminatorAndInformation.java._trace +/.Transition_M0.java._trace +/.Transition_M1.java._trace +/.EntryInRegion.java._trace +/.IncomingToEntry.java._trace +/.MultipleEntryInRegion.java._trace +/.MultipleTransitionFromEntry.java._trace +/.NoEntryInRegion.java._trace +/.NoOutgoingTransitionFromEntry.java._trace +/.NoStateInRegion.java._trace +/.OutgoingFromExit.java._trace +/.OutgoingFromFinal.java._trace +/.StateInRegion.java._trace +/.Transition.java._trace +/.Child.java._trace +/.ChoiceHasNoIncoming.java._trace +/.ChoiceHasNoOutgoing.java._trace +/.HasMultipleIncomingTrainsition.java._trace +/.HasMultipleOutgoingTrainsition.java._trace +/.HasMultipleRegions.java._trace +/.NotSynchronizingStates.java._trace +/.SynchHasNoIncoming.java._trace +/.SynchHasNoOutgoing.java._trace +/.SynchThree.java._trace +/.SynchronizedIncomingInSameRegion.java._trace +/.SynchronizedRegionDoesNotHaveMultipleRegions.java._trace +/.SynchronizedRegionsAreNotSiblings.java._trace +/.TwoSynch.java._trace +/.YakinduPatterns.java._trace +/.Transition_M2.java._trace +/.Transition_M3.java._trace +/.IncomingToEntry_1.java._trace +/.IncomingToEntry_M0.java._trace +/.Transition_M4.java._trace diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java new file mode 100644 index 00000000..cf1378da --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java @@ -0,0 +1,53 @@ +/** + * Generated from platform:/resource/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql + */ +package ca.mcgill.ecse.dslreasoner.vampire.queries; + +import ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation; +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine; +import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedPatternGroup; + +/** + * A pattern group formed of all public patterns defined in FamPatterns.vql. + * + *

Use the static instance as any {@link interface org.eclipse.viatra.query.runtime.api.IQueryGroup}, to conveniently prepare + * a VIATRA Query engine for matching all patterns originally defined in file FamPatterns.vql, + * in order to achieve better performance than one-by-one on-demand matcher initialization. + * + *

From package ca.mcgill.ecse.dslreasoner.vampire.queries, the group contains the definition of the following patterns:

    + *
  • terminatorAndInformation
    • + *
+ * + * @see IQueryGroup + * + */ +@SuppressWarnings("all") +public final class FamPatterns extends BaseGeneratedPatternGroup { + /** + * Access the pattern group. + * + * @return the singleton instance of the group + * @throws ViatraQueryRuntimeException if there was an error loading the generated code of pattern specifications + * + */ + public static FamPatterns instance() { + if (INSTANCE == null) { + INSTANCE = new FamPatterns(); + } + return INSTANCE; + } + + private static FamPatterns INSTANCE; + + private FamPatterns() { + querySpecifications.add(TerminatorAndInformation.instance()); + } + + public TerminatorAndInformation getTerminatorAndInformation() { + return TerminatorAndInformation.instance(); + } + + public TerminatorAndInformation.Matcher getTerminatorAndInformation(final ViatraQueryEngine engine) { + return TerminatorAndInformation.Matcher.on(engine); + } +} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java new file mode 100644 index 00000000..cb0708ad --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java @@ -0,0 +1,747 @@ +/** + * Generated from platform:/resource/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql + */ +package ca.mcgill.ecse.dslreasoner.vampire.queries; + +import functionalarchitecture.FAMTerminator; +import functionalarchitecture.InformationLink; +import java.util.Arrays; +import java.util.Collection; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Objects; +import java.util.Optional; +import java.util.Set; +import java.util.function.Consumer; +import java.util.stream.Collectors; +import java.util.stream.Stream; +import org.apache.log4j.Logger; +import org.eclipse.emf.ecore.EClass; +import org.eclipse.viatra.query.runtime.api.IPatternMatch; +import org.eclipse.viatra.query.runtime.api.IQuerySpecification; +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine; +import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFPQuery; +import org.eclipse.viatra.query.runtime.api.impl.BaseGeneratedEMFQuerySpecification; +import org.eclipse.viatra.query.runtime.api.impl.BaseMatcher; +import org.eclipse.viatra.query.runtime.api.impl.BasePatternMatch; +import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey; +import org.eclipse.viatra.query.runtime.emf.types.EStructuralFeatureInstancesKey; +import org.eclipse.viatra.query.runtime.matchers.backend.QueryEvaluationHint; +import org.eclipse.viatra.query.runtime.matchers.psystem.PBody; +import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable; +import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; +import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.ParameterReference; +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.Equality; +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExportedParameter; +import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint; +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter; +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection; +import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility; +import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple; +import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples; +import org.eclipse.viatra.query.runtime.util.ViatraQueryLoggingUtil; + +/** + * A pattern-specific query specification that can instantiate Matcher in a type-safe way. + * + *

Original source: + * 

+ *         {@literal @}Constraint(message="terminatorAndInformation", severity="error", key={T})
+ *         pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {
+ *         	FunctionalOutput.outgoingLinks(Out,I);
+ *         	FunctionalOutput.terminator(Out,T); 
+ *         } or {
+ *         	InformationLink.to(I,In);
+ *         	FunctionalInput.terminator(In,T);
+ *         }
+ *
+ * + * @see Matcher + * @see Match + * + */ +@SuppressWarnings("all") +public final class TerminatorAndInformation extends BaseGeneratedEMFQuerySpecification { + /** + * Pattern-specific match representation of the ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation pattern, + * to be used in conjunction with {@link Matcher}. + * + *

Class fields correspond to parameters of the pattern. Fields with value null are considered unassigned. + * Each instance is a (possibly partial) substitution of pattern parameters, + * usable to represent a match of the pattern in the result of a query, + * or to specify the bound (fixed) input parameters when issuing a query. + * + * @see Matcher + * + */ + public static abstract class Match extends BasePatternMatch { + private FAMTerminator fT; + + private InformationLink fI; + + private static List parameterNames = makeImmutableList("T", "I"); + + private Match(final FAMTerminator pT, final InformationLink pI) { + this.fT = pT; + this.fI = pI; + } + + @Override + public Object get(final String parameterName) { + if ("T".equals(parameterName)) return this.fT; + if ("I".equals(parameterName)) return this.fI; + return null; + } + + public FAMTerminator getT() { + return this.fT; + } + + public InformationLink getI() { + return this.fI; + } + + @Override + public boolean set(final String parameterName, final Object newValue) { + if (!isMutable()) throw new java.lang.UnsupportedOperationException(); + if ("T".equals(parameterName) ) { + this.fT = (FAMTerminator) newValue; + return true; + } + if ("I".equals(parameterName) ) { + this.fI = (InformationLink) newValue; + return true; + } + return false; + } + + public void setT(final FAMTerminator pT) { + if (!isMutable()) throw new java.lang.UnsupportedOperationException(); + this.fT = pT; + } + + public void setI(final InformationLink pI) { + if (!isMutable()) throw new java.lang.UnsupportedOperationException(); + this.fI = pI; + } + + @Override + public String patternName() { + return "ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"; + } + + @Override + public List parameterNames() { + return TerminatorAndInformation.Match.parameterNames; + } + + @Override + public Object[] toArray() { + return new Object[]{fT, fI}; + } + + @Override + public TerminatorAndInformation.Match toImmutable() { + return isMutable() ? newMatch(fT, fI) : this; + } + + @Override + public String prettyPrint() { + StringBuilder result = new StringBuilder(); + result.append("\"T\"=" + prettyPrintValue(fT) + ", "); + result.append("\"I\"=" + prettyPrintValue(fI)); + return result.toString(); + } + + @Override + public int hashCode() { + return Objects.hash(fT, fI); + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) + return true; + if (obj == null) { + return false; + } + if ((obj instanceof TerminatorAndInformation.Match)) { + TerminatorAndInformation.Match other = (TerminatorAndInformation.Match) obj; + return Objects.equals(fT, other.fT) && Objects.equals(fI, other.fI); + } else { + // this should be infrequent + if (!(obj instanceof IPatternMatch)) { + return false; + } + IPatternMatch otherSig = (IPatternMatch) obj; + return Objects.equals(specification(), otherSig.specification()) && Arrays.deepEquals(toArray(), otherSig.toArray()); + } + } + + @Override + public TerminatorAndInformation specification() { + return TerminatorAndInformation.instance(); + } + + /** + * Returns an empty, mutable match. + * Fields of the mutable match can be filled to create a partial match, usable as matcher input. + * + * @return the empty match. + * + */ + public static TerminatorAndInformation.Match newEmptyMatch() { + return new Mutable(null, null); + } + + /** + * Returns a mutable (partial) match. + * Fields of the mutable match can be filled to create a partial match, usable as matcher input. + * + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return the new, mutable (partial) match object. + * + */ + public static TerminatorAndInformation.Match newMutableMatch(final FAMTerminator pT, final InformationLink pI) { + return new Mutable(pT, pI); + } + + /** + * Returns a new (partial) match. + * This can be used e.g. to call the matcher with a partial match. + *

The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return the (partial) match object. + * + */ + public static TerminatorAndInformation.Match newMatch(final FAMTerminator pT, final InformationLink pI) { + return new Immutable(pT, pI); + } + + private static final class Mutable extends TerminatorAndInformation.Match { + Mutable(final FAMTerminator pT, final InformationLink pI) { + super(pT, pI); + } + + @Override + public boolean isMutable() { + return true; + } + } + + private static final class Immutable extends TerminatorAndInformation.Match { + Immutable(final FAMTerminator pT, final InformationLink pI) { + super(pT, pI); + } + + @Override + public boolean isMutable() { + return false; + } + } + } + + /** + * Generated pattern matcher API of the ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation pattern, + * providing pattern-specific query methods. + * + *

Use the pattern matcher on a given model via {@link #on(ViatraQueryEngine)}, + * e.g. in conjunction with {@link ViatraQueryEngine#on(QueryScope)}. + * + *

Matches of the pattern will be represented as {@link Match}. + * + *

Original source: + * 

+   * {@literal @}Constraint(message="terminatorAndInformation", severity="error", key={T})
+   * pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {
+   * 	FunctionalOutput.outgoingLinks(Out,I);
+   * 	FunctionalOutput.terminator(Out,T); 
+   * } or {
+   * 	InformationLink.to(I,In);
+   * 	FunctionalInput.terminator(In,T);
+   * }
+   *
+ * + * @see Match + * @see TerminatorAndInformation + * + */ + public static class Matcher extends BaseMatcher { + /** + * Initializes the pattern matcher within an existing VIATRA Query engine. + * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned. + * + * @param engine the existing VIATRA Query engine in which this matcher will be created. + * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation + * + */ + public static TerminatorAndInformation.Matcher on(final ViatraQueryEngine engine) { + // check if matcher already exists + Matcher matcher = engine.getExistingMatcher(querySpecification()); + if (matcher == null) { + matcher = (Matcher)engine.getMatcher(querySpecification()); + } + return matcher; + } + + /** + * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation + * @return an initialized matcher + * @noreference This method is for internal matcher initialization by the framework, do not call it manually. + * + */ + public static TerminatorAndInformation.Matcher create() { + return new Matcher(); + } + + private final static int POSITION_T = 0; + + private final static int POSITION_I = 1; + + private final static Logger LOGGER = ViatraQueryLoggingUtil.getLogger(TerminatorAndInformation.Matcher.class); + + /** + * Initializes the pattern matcher within an existing VIATRA Query engine. + * If the pattern matcher is already constructed in the engine, only a light-weight reference is returned. + * + * @param engine the existing VIATRA Query engine in which this matcher will be created. + * @throws ViatraQueryRuntimeException if an error occurs during pattern matcher creation + * + */ + private Matcher() { + super(querySpecification()); + } + + /** + * Returns the set of all matches of the pattern that conform to the given fixed values of some parameters. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return matches represented as a Match object. + * + */ + public Collection getAllMatches(final FAMTerminator pT, final InformationLink pI) { + return rawStreamAllMatches(new Object[]{pT, pI}).collect(Collectors.toSet()); + } + + /** + * Returns a stream of all matches of the pattern that conform to the given fixed values of some parameters. + *

+ * NOTE: It is important not to modify the source model while the stream is being processed. + * If the match set of the pattern changes during processing, the contents of the stream is undefined. + * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return a stream of matches represented as a Match object. + * + */ + public Stream streamAllMatches(final FAMTerminator pT, final InformationLink pI) { + return rawStreamAllMatches(new Object[]{pT, pI}); + } + + /** + * Returns an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters. + * Neither determinism nor randomness of selection is guaranteed. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return a match represented as a Match object, or null if no match is found. + * + */ + public Optional getOneArbitraryMatch(final FAMTerminator pT, final InformationLink pI) { + return rawGetOneArbitraryMatch(new Object[]{pT, pI}); + } + + /** + * Indicates whether the given combination of specified pattern parameters constitute a valid pattern match, + * under any possible substitution of the unspecified parameters (if any). + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return true if the input is a valid (partial) match of the pattern. + * + */ + public boolean hasMatch(final FAMTerminator pT, final InformationLink pI) { + return rawHasMatch(new Object[]{pT, pI}); + } + + /** + * Returns the number of all matches of the pattern that conform to the given fixed values of some parameters. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return the number of pattern matches found. + * + */ + public int countMatches(final FAMTerminator pT, final InformationLink pI) { + return rawCountMatches(new Object[]{pT, pI}); + } + + /** + * Executes the given processor on an arbitrarily chosen match of the pattern that conforms to the given fixed values of some parameters. + * Neither determinism nor randomness of selection is guaranteed. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @param processor the action that will process the selected match. + * @return true if the pattern has at least one match with the given parameter values, false if the processor was not invoked + * + */ + public boolean forOneArbitraryMatch(final FAMTerminator pT, final InformationLink pI, final Consumer processor) { + return rawForOneArbitraryMatch(new Object[]{pT, pI}, processor); + } + + /** + * Returns a new (partial) match. + * This can be used e.g. to call the matcher with a partial match. + *

The returned match will be immutable. Use {@link #newEmptyMatch()} to obtain a mutable match object. + * @param pT the fixed value of pattern parameter T, or null if not bound. + * @param pI the fixed value of pattern parameter I, or null if not bound. + * @return the (partial) match object. + * + */ + public TerminatorAndInformation.Match newMatch(final FAMTerminator pT, final InformationLink pI) { + return TerminatorAndInformation.Match.newMatch(pT, pI); + } + + /** + * Retrieve the set of values that occur in matches for T. + * @return the Set of all values or empty set if there are no matches + * + */ + protected Stream rawStreamAllValuesOfT(final Object[] parameters) { + return rawStreamAllValues(POSITION_T, parameters).map(FAMTerminator.class::cast); + } + + /** + * Retrieve the set of values that occur in matches for T. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfT() { + return rawStreamAllValuesOfT(emptyArray()).collect(Collectors.toSet()); + } + + /** + * Retrieve the set of values that occur in matches for T. + * @return the Set of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfT() { + return rawStreamAllValuesOfT(emptyArray()); + } + + /** + * Retrieve the set of values that occur in matches for T. + *

+ * NOTE: It is important not to modify the source model while the stream is being processed. + * If the match set of the pattern changes during processing, the contents of the stream is undefined. + * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code. + * + * @return the Stream of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfT(final TerminatorAndInformation.Match partialMatch) { + return rawStreamAllValuesOfT(partialMatch.toArray()); + } + + /** + * Retrieve the set of values that occur in matches for T. + *

+ * NOTE: It is important not to modify the source model while the stream is being processed. + * If the match set of the pattern changes during processing, the contents of the stream is undefined. + * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code. + * + * @return the Stream of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfT(final InformationLink pI) { + return rawStreamAllValuesOfT(new Object[]{null, pI}); + } + + /** + * Retrieve the set of values that occur in matches for T. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfT(final TerminatorAndInformation.Match partialMatch) { + return rawStreamAllValuesOfT(partialMatch.toArray()).collect(Collectors.toSet()); + } + + /** + * Retrieve the set of values that occur in matches for T. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfT(final InformationLink pI) { + return rawStreamAllValuesOfT(new Object[]{null, pI}).collect(Collectors.toSet()); + } + + /** + * Retrieve the set of values that occur in matches for I. + * @return the Set of all values or empty set if there are no matches + * + */ + protected Stream rawStreamAllValuesOfI(final Object[] parameters) { + return rawStreamAllValues(POSITION_I, parameters).map(InformationLink.class::cast); + } + + /** + * Retrieve the set of values that occur in matches for I. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfI() { + return rawStreamAllValuesOfI(emptyArray()).collect(Collectors.toSet()); + } + + /** + * Retrieve the set of values that occur in matches for I. + * @return the Set of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfI() { + return rawStreamAllValuesOfI(emptyArray()); + } + + /** + * Retrieve the set of values that occur in matches for I. + *

+ * NOTE: It is important not to modify the source model while the stream is being processed. + * If the match set of the pattern changes during processing, the contents of the stream is undefined. + * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code. + * + * @return the Stream of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfI(final TerminatorAndInformation.Match partialMatch) { + return rawStreamAllValuesOfI(partialMatch.toArray()); + } + + /** + * Retrieve the set of values that occur in matches for I. + *

+ * NOTE: It is important not to modify the source model while the stream is being processed. + * If the match set of the pattern changes during processing, the contents of the stream is undefined. + * In such cases, either rely on {@link #getAllMatches()} or collect the results of the stream in end-user code. + * + * @return the Stream of all values or empty set if there are no matches + * + */ + public Stream streamAllValuesOfI(final FAMTerminator pT) { + return rawStreamAllValuesOfI(new Object[]{pT, null}); + } + + /** + * Retrieve the set of values that occur in matches for I. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfI(final TerminatorAndInformation.Match partialMatch) { + return rawStreamAllValuesOfI(partialMatch.toArray()).collect(Collectors.toSet()); + } + + /** + * Retrieve the set of values that occur in matches for I. + * @return the Set of all values or empty set if there are no matches + * + */ + public Set getAllValuesOfI(final FAMTerminator pT) { + return rawStreamAllValuesOfI(new Object[]{pT, null}).collect(Collectors.toSet()); + } + + @Override + protected TerminatorAndInformation.Match tupleToMatch(final Tuple t) { + try { + return TerminatorAndInformation.Match.newMatch((FAMTerminator) t.get(POSITION_T), (InformationLink) t.get(POSITION_I)); + } catch(ClassCastException e) { + LOGGER.error("Element(s) in tuple not properly typed!",e); + return null; + } + } + + @Override + protected TerminatorAndInformation.Match arrayToMatch(final Object[] match) { + try { + return TerminatorAndInformation.Match.newMatch((FAMTerminator) match[POSITION_T], (InformationLink) match[POSITION_I]); + } catch(ClassCastException e) { + LOGGER.error("Element(s) in array not properly typed!",e); + return null; + } + } + + @Override + protected TerminatorAndInformation.Match arrayToMatchMutable(final Object[] match) { + try { + return TerminatorAndInformation.Match.newMutableMatch((FAMTerminator) match[POSITION_T], (InformationLink) match[POSITION_I]); + } catch(ClassCastException e) { + LOGGER.error("Element(s) in array not properly typed!",e); + return null; + } + } + + /** + * @return the singleton instance of the query specification of this pattern + * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded + * + */ + public static IQuerySpecification querySpecification() { + return TerminatorAndInformation.instance(); + } + } + + private TerminatorAndInformation() { + super(GeneratedPQuery.INSTANCE); + } + + /** + * @return the singleton instance of the query specification + * @throws ViatraQueryRuntimeException if the pattern definition could not be loaded + * + */ + public static TerminatorAndInformation instance() { + try{ + return LazyHolder.INSTANCE; + } catch (ExceptionInInitializerError err) { + throw processInitializerError(err); + } + } + + @Override + protected TerminatorAndInformation.Matcher instantiate(final ViatraQueryEngine engine) { + return TerminatorAndInformation.Matcher.on(engine); + } + + @Override + public TerminatorAndInformation.Matcher instantiate() { + return TerminatorAndInformation.Matcher.create(); + } + + @Override + public TerminatorAndInformation.Match newEmptyMatch() { + return TerminatorAndInformation.Match.newEmptyMatch(); + } + + @Override + public TerminatorAndInformation.Match newMatch(final Object... parameters) { + return TerminatorAndInformation.Match.newMatch((functionalarchitecture.FAMTerminator) parameters[0], (functionalarchitecture.InformationLink) parameters[1]); + } + + /** + * Inner class allowing the singleton instance of {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * not at the class load time of the outer class, + * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.vampire.queries.TerminatorAndInformation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * + *

This workaround is required e.g. to support recursion. + * + */ + private static class LazyHolder { + private final static TerminatorAndInformation INSTANCE = new TerminatorAndInformation(); + + /** + * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. + * This initialization order is required to support indirect recursion. + * + *

The static initializer is defined using a helper field to work around limitations of the code generator. + * + */ + private final static Object STATIC_INITIALIZER = ensureInitialized(); + + public static Object ensureInitialized() { + INSTANCE.ensureInitializedInternal(); + return null; + } + } + + private static class GeneratedPQuery extends BaseGeneratedEMFPQuery { + private final static TerminatorAndInformation.GeneratedPQuery INSTANCE = new GeneratedPQuery(); + + private final PParameter parameter_T = new PParameter("T", "functionalarchitecture.FAMTerminator", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator")), PParameterDirection.INOUT); + + private final PParameter parameter_I = new PParameter("I", "functionalarchitecture.InformationLink", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink")), PParameterDirection.INOUT); + + private final List parameters = Arrays.asList(parameter_T, parameter_I); + + private GeneratedPQuery() { + super(PVisibility.PUBLIC); + } + + @Override + public String getFullyQualifiedName() { + return "ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"; + } + + @Override + public List getParameterNames() { + return Arrays.asList("T","I"); + } + + @Override + public List getParameters() { + return parameters; + } + + @Override + public Set doGetContainedBodies() { + setEvaluationHints(new QueryEvaluationHint(null, QueryEvaluationHint.BackendRequirement.UNSPECIFIED)); + Set bodies = new LinkedHashSet<>(); + { + PBody body = new PBody(this); + PVariable var_T = body.getOrCreateVariableByName("T"); + PVariable var_I = body.getOrCreateVariableByName("I"); + PVariable var_Out = body.getOrCreateVariableByName("Out"); + new TypeConstraint(body, Tuples.flatTupleOf(var_T), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator"))); + new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink"))); + body.setSymbolicParameters(Arrays.asList( + new ExportedParameter(body, var_T, parameter_T), + new ExportedParameter(body, var_I, parameter_I) + )); + // FunctionalOutput.outgoingLinks(Out,I) + new TypeConstraint(body, Tuples.flatTupleOf(var_Out), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput"))); + PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}"); + new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput", "outgoingLinks"))); + new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink"))); + new Equality(body, var__virtual_0_, var_I); + // FunctionalOutput.terminator(Out,T) + new TypeConstraint(body, Tuples.flatTupleOf(var_Out), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalOutput"))); + PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}"); + new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalData", "terminator"))); + new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator"))); + new Equality(body, var__virtual_1_, var_T); + bodies.add(body); + } + { + PBody body = new PBody(this); + PVariable var_T = body.getOrCreateVariableByName("T"); + PVariable var_I = body.getOrCreateVariableByName("I"); + PVariable var_In = body.getOrCreateVariableByName("In"); + new TypeConstraint(body, Tuples.flatTupleOf(var_T), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator"))); + new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink"))); + body.setSymbolicParameters(Arrays.asList( + new ExportedParameter(body, var_T, parameter_T), + new ExportedParameter(body, var_I, parameter_I) + )); + // InformationLink.to(I,In) + new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink"))); + PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}"); + new TypeConstraint(body, Tuples.flatTupleOf(var_I, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "InformationLink", "to"))); + new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalInput"))); + new Equality(body, var__virtual_0_, var_In); + // FunctionalInput.terminator(In,T) + new TypeConstraint(body, Tuples.flatTupleOf(var_In), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalInput"))); + PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}"); + new TypeConstraint(body, Tuples.flatTupleOf(var_In, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FunctionalData", "terminator"))); + new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("http://www.inf.mit.bme.hu/viatrasolver/example/fam", "FAMTerminator"))); + new Equality(body, var__virtual_1_, var_T); + bodies.add(body); + } + { + PAnnotation annotation = new PAnnotation("Constraint"); + annotation.addAttribute("message", "terminatorAndInformation"); + annotation.addAttribute("severity", "error"); + annotation.addAttribute("key", Arrays.asList(new Object[] { + new ParameterReference("T") + })); + addAnnotation(annotation); + } + return bodies; + } + } +} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend index 54114189..18b3badd 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend @@ -6,6 +6,7 @@ import functionalarchitecture.FunctionalarchitecturePackage import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore @@ -22,9 +23,6 @@ import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.EReference import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns -import java.util.LinkedHashMap -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor class EcoreTest { def static void main(String[] args) { @@ -62,7 +60,7 @@ class EcoreTest { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL ] solution = reasoner.solve(logicProblem, vampireConfig, workspace) 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 9ae00f8d..95bfd87a 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 @@ -1,8 +1,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse +import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace +import java.util.LinkedList +import org.eclipse.emf.ecore.EObject import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl @@ -21,12 +23,12 @@ class FAMTest { println("Input and output workspaces are created") val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi") + val partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi") val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) println("DSL loaded") - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) + GeneralTest.createAndSolveProblem(metamodel, new LinkedList, queries, workspace) } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 2c53d181..8a60f486 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -26,56 +26,74 @@ import org.eclipse.emf.ecore.EReference import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.eclipse.viatra.query.runtime.api.IQueryGroup +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel class GeneralTest { - def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List partialModel, ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { + def static String createAndSolveProblem(EcoreMetamodelDescriptor metamodel, List partialModel, + ViatraQuerySetDescriptor queries, FileSystemWorkspace workspace) { val Ecore2Logic ecore2Logic = new Ecore2Logic val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic - - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) - var problem = instanceModel2Logic.transform(modelGenerationProblem,partialModel).output - problem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration).output - + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + var problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output + problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output + workspace.writeModel(problem, "Fam.logicproblem") - + println("Problem created") - + var LogicResult solution var LogicReasoner reasoner + //* reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ - //add configuration things, in config file first - it.writeToFile = true + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + it.typeScopes.minNewElements = 5 ] + solution = reasoner.solve(problem, vampireConfig, workspace) - solution = reasoner.solve(problem, vampireConfig, workspace) + /*/ + reasoner = new AlloySolver + val alloyConfig = new AlloySolverConfiguration => [ + it.typeScopes.maxNewElements = 7 + it.typeScopes.minNewElements = 3 + it.solutionScope.numberOfRequiredSolution = 1 + it.typeScopes.maxNewIntegers = 0 + it.documentationLevel = DocumentationLevel::NORMAL + ] + solution = reasoner.solve(problem, alloyConfig, workspace) + //*/ + println("Problem solved") } - + def static loadMetamodel(EPackage pckg) { val List classes = pckg.getEClassifiers.filter(EClass).toList val List enums = pckg.getEClassifiers.filter(EEnum).toList val List literals = enums.map[getELiterals].flatten.toList val List references = classes.map[getEReferences].flatten.toList val List attributes = classes.map[getEAttributes].flatten.toList - return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) + return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes) } def static loadPartialModel(ReasonerWorkspace inputs, String path) { Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); - inputs.readModel(EObject,path).eResource.contents + inputs.readModel(EObject, path).eResource.contents // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList } def static loadQueries(EcoreMetamodelDescriptor metamodel, IQueryGroup i) { val patterns = i.specifications.toList - val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet + val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet val derivedFeatures = emptyMap - //NO DERIVED FEATURES + // NO DERIVED FEATURES // val derivedFeatures = new LinkedHashMap // derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) // derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) @@ -86,4 +104,4 @@ class GeneralTest { ) return res } -} \ No newline at end of file +} diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index e4f6f87a..eb3f4b14 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend @@ -1,11 +1,11 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.y import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage +import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.queries.YakinduPatterns class YakinduTest { def static void main(String[] args) { @@ -23,11 +23,11 @@ class YakinduTest { val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi") - val queries = GeneralTest.loadQueries(metamodel, +// val queries = GeneralTest.loadQueries(metamodel, FamPa println("DSL loaded") - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) +// GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace) } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql index 013d0419..60679874 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql @@ -1,4 +1,4 @@ -package hu.bme.mit.inf.dslreasoner.domains.fam +package ca.mcgill.ecse.dslreasoner.vampire.queries import epackage "http://www.inf.mit.bme.hu/viatrasolver/example/fam" diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend index 15f9e1fe..40cb70a7 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.xtend @@ -1,19 +1,17 @@ package ca.mcgill.ecse.dslreasoner.vampire.test import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.Collections import org.eclipse.emf.common.util.URI import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl @@ -41,7 +39,7 @@ class MedicalSystem { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL ] solution = reasoner.solve(root, vampireConfig, workspace) diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend index 4fc81ad8..bbb14f1f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend @@ -1,23 +1,19 @@ package ca.mcgill.ecse.dslreasoner.vampire.test - import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.Collections -import org.eclipse.emf.common.util.URI import org.eclipse.emf.ecore.resource.Resource -import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import java.io.File class VampireTest { @@ -65,7 +61,8 @@ class VampireTest { reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ //add configuration things, in config file first - it.writeToFile = true + it.documentationLevel = DocumentationLevel::FULL + it.typeScopes.minNewElements = 4 ] solution = reasoner.solve(problem, vampireConfig, workspace) 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 cf5c79b4..59a3bc01 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 33fae225..1406c597 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 56144b8f..20397ff3 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 29d89e94..ebca0881 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 c0d35b2f..8fc60bab 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/EcoreTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java index f3dc8572..820dd354 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java @@ -8,6 +8,7 @@ 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; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; @@ -70,7 +71,7 @@ public class EcoreTest { reasoner = _vampireSolver; VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.writeToFile = true; + it.documentationLevel = DocumentationLevel.FULL; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); solution = reasoner.solve(logicProblem, vampireConfig, workspace); 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 92803b7f..dd061008 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 @@ -1,11 +1,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; +import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns; import functionalarchitecture.FunctionalarchitecturePackage; -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; +import java.util.LinkedList; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EObject; @@ -30,9 +31,10 @@ public class FAMTest { map.put("logicproblem", _xMIResourceFactoryImpl); InputOutput.println("Input and output workspaces are created"); final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel.xmi"); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "FunctionalArchitectureModel2.xmi"); final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); InputOutput.println("DSL loaded"); - GeneralTest.createAndSolveProblem(metamodel, partialModel, queries, workspace); + LinkedList _linkedList = new LinkedList(); + GeneralTest.createAndSolveProblem(metamodel, _linkedList, queries, workspace); } } diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index 92cf666c..2401e710 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -8,6 +8,7 @@ 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; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; @@ -69,7 +70,8 @@ public class GeneralTest { reasoner = _vampireSolver; VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.writeToFile = true; + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 5; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); solution = reasoner.solve(problem, vampireConfig, workspace); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index fa4ef6b9..bea4e8a6 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java @@ -1,10 +1,34 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; +import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; +import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage; +import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; +import java.util.Map; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.InputOutput; + @SuppressWarnings("all") public class YakinduTest { public static void main(final String[] args) { - throw new Error("Unresolved compilation problems:" - + "\nmissing \')\' at \'GeneralTest\'" - + "\nType mismatch: cannot convert from String to IQueryGroup"); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/YakinduTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "Yakindu.xmi"); + InputOutput.println("DSL loaded"); } } 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 fe447779..e9359697 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 8e57f5e7..78d32090 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 9d12dab4..1f7b3ee7 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 diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore index 2760bac4..a16d5bbd 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore @@ -1,12 +1,2 @@ -/.VampireTest.java._trace -/.SimpleRun.java._trace -/.DslTest.java._trace /.MedicalSystem.java._trace -/.DslTest.xtendbin -/.MedicalSystem.xtendbin -/.SimpleRun.xtendbin -/.VampireTest.xtendbin -/DslTest.java -/MedicalSystem.java -/VampireTest.java -/.FAMTest.java._trace +/.VampireTest.java._trace diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java index ece0a9bb..0b96a2f3 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/MedicalSystem.java @@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; @@ -40,7 +41,7 @@ public class MedicalSystem { reasoner = _vampireSolver; VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.writeToFile = true; + it.documentationLevel = DocumentationLevel.FULL; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); solution = reasoner.solve(root, vampireConfig, workspace); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java index 74f117f2..7228b48a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java @@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; @@ -68,7 +69,8 @@ public class VampireTest { reasoner = _vampireSolver; VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.writeToFile = true; + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 4; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); solution = reasoner.solve(problem, vampireConfig, workspace); -- cgit v1.2.3-54-g00ecf