From 2f8149678539a94f2f4ca2e7ff5640ff5d7087cc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 15 Apr 2019 00:06:29 -0400 Subject: VAMPIRE: close #22, improve test structure for #39, .vql file trouble --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../plugin.xml | 29 + .../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 ...c2VampireLanguageMapper_ContainmentMapper.xtend | 12 +- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 183 ++--- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 1 + .../Logic2VampireLanguageMapper_Support.xtend | 12 +- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 23 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18156 -> 18156 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4215 -> 4215 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 10551 -> 10674 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8209 -> 6457 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9839 -> 9839 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13093 -> 13046 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10705 -> 10792 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 ...ic2VampireLanguageMapper_ContainmentMapper.java | 15 +- ...Logic2VampireLanguageMapper_RelationMapper.java | 159 +---- .../Logic2VampireLanguageMapper_Support.java | 18 +- .../Logic2VampireLanguageMapper_TypeMapper.java | 25 +- .../metamodels/filesystem.aird | 379 +++++++++++ .../metamodels/yakindu.aird | 111 ++- .../plugin.xml | 7 - .../test/fam/queries/TerminatorAndInformation.java | 747 --------------------- .../.classpath | 1 + .../META-INF/MANIFEST.MF | 6 +- .../initialModels/FAM/FaModel.xmi | 7 + .../initialModels/FaModel.xmi | 7 - .../output/FAMTest/Fam.logicproblem | 7 +- .../output/FAMTest/vampireProblem.tptp | 72 -- .../plugin.xml | 20 +- .../dslreasoner/vampire/queries/FamPatterns.java | 53 -- .../vampire/queries/TerminatorAndInformation.java | 747 --------------------- .../ecse/dslreasoner/vampire/icse/EcoreTest.xtend | 76 +-- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 8 +- .../dslreasoner/vampire/icse/FileSystemTest.xtend | 13 +- .../dslreasoner/vampire/icse/YakinduTest.xtend | 6 +- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6358 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6825 -> 6296 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6088 -> 6618 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 6456 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 6042 -> 6040 bytes .../ecse/dslreasoner/vampire/icse/EcoreTest.java | 61 +- .../ecse/dslreasoner/vampire/icse/FAMTest.java | 7 +- .../dslreasoner/vampire/icse/FileSystemTest.java | 11 +- .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 4 +- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 69 files changed, 735 insertions(+), 2092 deletions(-) create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/filesystem.aird delete mode 100644 Tests/ca.mcgill.ecse.dslreasoner.standalone.test/src-gen/ca/mcgill/ecse/dslreasoner/standalone/test/fam/queries/TerminatorAndInformation.java create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FaModel.xmi delete mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi delete mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp delete mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java delete mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index d6392a0b..9edfdac5 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index c97efa0f..0979473a 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml index 9ace526f..8069f168 100644 --- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml @@ -3,6 +3,35 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 024dcab9..10495630 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 7e128ad1..295d9ec2 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 0bf8ccc6..83b00f77 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 58a18bbb..f8a7a2f3 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 205afcc4..544f5811 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 b388bd43..62aac4ca 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 3092be97..31d4543e 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 8b23f34d..7b230b65 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 84682c47..a24c2795 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 e3f67a0c..b35605ae 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 bf354098..5e9cd3bd 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 da62f4c1..0001d80f 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 482b884e..b189414a 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 81c1f803..b4eec95c 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_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend index 395b4305..8e0e0b11 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper { for (l : relationsList) { var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type containmentListCopy.remove(pointingTo) - for (c : pointingTo.subtypes) { + var List allSubtypes = newArrayList + support.listSubtypes(pointingTo, allSubtypes) + for (c : allSubtypes) { + containmentListCopy.remove(c) + } + } + + for (c : containmentListCopy) { + if(c.isIsAbstract) { containmentListCopy.remove(c) } } @@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 2 CONT'D for (e : type2cont.entrySet) { val relFormula = createVLSFofFormula => [ - it.name = support.toIDMultiple("containment", e.key.constant.toString) + it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ 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 0ae06bc3..2dec281d 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 @@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper { } + //deciding name of relation + val nameArray = r.name.split(" ") + var relNameVar = "" + if (nameArray.length == 3) { + relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) + } + else { + relNameVar = r.name + } + val relName = relNameVar + val comply = createVLSFofFormula=> [ - val nameArray = r.name.split(" ") - it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) + + it.name = support.toIDMultiple("compliance", relName) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ for (v : relVar2VLS) { @@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper { } it.operand = createVLSImplies => [ val rel = createVLSFunction => [ - it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) + it.constant = support.toIDMultiple("r", relName) for (v : relVar2VLS) { it.terms += support.duplicate(v) } @@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper { def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { - // 1. store all variables in support wrt their name - // 1.1 if variable has type, creating list of type declarations -// val VLSVariable variable = createVLSVariable => [it.name = "A"] - val Map relationVar2VLS = new HashMap - val Map relationVar2TypeDecComply = new HashMap - val Map relationVar2TypeDecRes = new HashMap - val typedefs = new ArrayList - - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = support.toIDMultiple("V", variable.name) - ] - relationVar2VLS.put(variable, v) - - val varTypeComply = createVLSFunction => [ - it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) - it.terms += support.duplicate(v) - ] - relationVar2TypeDecComply.put(variable, varTypeComply) - relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) - } - val nameArray = reldef.name.split(" ") - val comply = createVLSFofFormula => [ - it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), - nameArray.get(nameArray.length - 1)) - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - for (variable : reldef.variables) { - it.variables += support.duplicate(variable.lookup(relationVar2VLS)) - - } - it.operand = createVLSImplies => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", reldef.name) - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.terms += v - } - ] - it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) - ] - ] - ] - - val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), - nameArray.get(nameArray.length - 1)) - it.fofRole = "axiom" - it.fofFormula = createVLSUniversalQuantifier => [ - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.variables += v - - } - it.operand = createVLSImplies => [ - it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) - it.right = createVLSEquivalent => [ - it.left = createVLSFunction => [ - it.constant = support.toIDMultiple("rel", reldef.name) - for (variable : reldef.variables) { - val v = createVLSVariable => [ - it.name = variable.lookup(relationVar2VLS).name - ] - it.terms += v - - } - ] - it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) - ] - - ] - - ] - - ] - - // trace.relationDefinition2Predicate.put(r,res) - trace.specification.formulas += comply; - trace.specification.formulas += res; +// // 1. store all variables in support wrt their name +// // 1.1 if variable has type, creating list of type declarations +//// val VLSVariable variable = createVLSVariable => [it.name = "A"] +// val Map relationVar2VLS = new HashMap +// val Map relationVar2TypeDecComply = new HashMap +// val Map relationVar2TypeDecRes = new HashMap +// val typedefs = new ArrayList +// +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = support.toIDMultiple("V", variable.name) +// ] +// relationVar2VLS.put(variable, v) +// +// val varTypeComply = createVLSFunction => [ +// it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) +// it.terms += support.duplicate(v) +// ] +// relationVar2TypeDecComply.put(variable, varTypeComply) +// relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) +// } +// val nameArray = reldef.name.split(" ") +// val comply = createVLSFofFormula => [ +// it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), +// nameArray.get(nameArray.length - 1)) +// it.fofRole = "axiom" +// it.fofFormula = createVLSUniversalQuantifier => [ +// for (variable : reldef.variables) { +// it.variables += support.duplicate(variable.lookup(relationVar2VLS)) +// +// } +// it.operand = createVLSImplies => [ +// it.left = createVLSFunction => [ +// it.constant = support.toIDMultiple("rel", reldef.name) +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.terms += v +// } +// ] +// it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) +// ] +// ] +// ] +// +// val res = createVLSFofFormula => [ +// it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), +// nameArray.get(nameArray.length - 1)) +// it.fofRole = "axiom" +// it.fofFormula = createVLSUniversalQuantifier => [ +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.variables += v +// +// } +// it.operand = createVLSImplies => [ +// it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) +// it.right = createVLSEquivalent => [ +// it.left = createVLSFunction => [ +// it.constant = support.toIDMultiple("rel", reldef.name) +// for (variable : reldef.variables) { +// val v = createVLSVariable => [ +// it.name = variable.lookup(relationVar2VLS).name +// ] +// it.terms += v +// +// } +// ] +// it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) +// ] +// +// ] +// +// ] +// +// ] +// +// // trace.relationDefinition2Predicate.put(r,res) +// trace.specification.formulas += comply; +// trace.specification.formulas += res; } 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 0a8812e4..4a8d2827 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 @@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS // TODO HANDLE // 1. make a list of constants equaling the min number of specified objects + //These numbers do not include enums or initial model elements val GLOBAL_MIN = config.typeScopes.minNewElements val GLOBAL_MAX = config.typeScopes.maxNewElements 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 195b89bb..680213ab 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 @@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support { } } - def protected List listSubtypes(Type t) { - var List allSubtypes = newArrayList - if (!t.subtypes.isEmpty) { - for (subt : t.subtypes) { - allSubtypes.add(subt) - allSubtypes = listSubtypes(subt) - } + def protected void listSubtypes(Type t, List allSubtypes) { + for (subt : t.subtypes) { + allSubtypes.add(subt) + listSubtypes(subt, allSubtypes) } - return allSubtypes } def protected withAddition(Map map1, Map map2) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index 3bc945df..2f3af593 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper { // Create a VLSFunction for each Enum Element val List orElems = newArrayList + for (e : type.elements) { + val nameArray = e.name.split(" ") + var relNameVar = "" + if (nameArray.length == 3) { + relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) + } else { + relNameVar = e.name + } + val relName = relNameVar + val enumElemPred = createVLSFunction => [ - val splitName = e.name.split(" ") - if (splitName.length > 2) { - it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) - } else { - it.constant = support.toIDMultiple("e", splitName.get(0)) - } + it.constant = support.toIDMultiple("e", relName) it.terms += support.duplicate(variable) ] trace.element2Predicate.put(e, enumElemPred) @@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper { // Implement Enum Inheritence Hierarchy val res = createVLSFofFormula => [ - it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) + it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ it.variables += support.duplicate(variable) @@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper { val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) - val index = i + val index = i-globalCounter val enumScope = createVLSFofFormula => [ - it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), + it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, type.elements.get(index).name.split(" ").get(0)) it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ 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 43e1e477..1ea7e30a 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 4e6f6ca0..ee06cb39 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 707a6089..648d9600 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 3171324f..a02821a5 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 301df7fa..b01f92a6 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index 5e53ea26..7634af4b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index b378ed09..4906adfc 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 605ac88c..e2c945e3 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 0c289e29..f465506c 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 cb72fd90..e046604a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index cfe1e8cd..aff62dca 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 c2079147..7212cce7 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 3c70bc14..d23bacad 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 9ef20b23..be78cace 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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 4cdc7e6a..9deab87f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -64,12 +64,19 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { Type _referred = ((ComplexTypeReference) _get).getReferred(); Type pointingTo = ((Type) _referred); containmentListCopy.remove(pointingTo); - EList _subtypes = pointingTo.getSubtypes(); - for (final Type c : _subtypes) { + List allSubtypes = CollectionLiterals.newArrayList(); + this.support.listSubtypes(pointingTo, allSubtypes); + for (final Type c : allSubtypes) { containmentListCopy.remove(c); } } } + for (final Type c : containmentListCopy) { + boolean _isIsAbstract = c.isIsAbstract(); + if (_isIsAbstract) { + containmentListCopy.remove(c); + } + } final String topName = CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(containmentListCopy.get(0), trace.type2Predicate)); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -132,7 +139,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); this.addToMap(type2cont, toFunc, rel); EList _subtypes = toType.getSubtypes(); - for (final Type c : _subtypes) { + for (final Type c_1 : _subtypes) { this.addToMap(type2cont, toFunc, rel); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -184,7 +191,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { { VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString())); + it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { 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 d5745333..c6565f6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -3,7 +3,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; @@ -17,14 +16,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.Arrays; -import java.util.Collection; -import java.util.HashMap; import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.ExclusiveRange; @@ -64,10 +59,19 @@ public class Logic2VampireLanguageMapper_RelationMapper { relVar2TypeDecComply.add(varTypeComply); } } + final String[] nameArray = r.getName().split(" "); + String relNameVar = ""; + int _length_1 = nameArray.length; + boolean _equals = (_length_1 == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = r.getName(); + } + final String relName = relNameVar; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - final String[] nameArray = r.getName().split(" "); - it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); + it.setName(this.support.toIDMultiple("compliance", relName)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { @@ -80,7 +84,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { final Procedure1 _function_2 = (VLSImplies it_2) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); + it_3.setConstant(this.support.toIDMultiple("r", relName)); for (final VLSVariable v_1 : relVar2VLS) { EList _terms = it_3.getTerms(); VLSVariable _duplicate_1 = this.support.duplicate(v_1); @@ -104,145 +108,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { } public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { - final Map relationVar2VLS = new HashMap(); - final Map relationVar2TypeDecComply = new HashMap(); - final Map relationVar2TypeDecRes = new HashMap(); - final ArrayList typedefs = new ArrayList(); - EList _variables = reldef.getVariables(); - for (final Variable variable : _variables) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", variable.getName())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relationVar2VLS.put(variable, v); - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(v); - _terms.add(_duplicate); - }; - final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - relationVar2TypeDecComply.put(variable, varTypeComply); - relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); - } - } - final String[] nameArray = reldef.getName().split(" "); - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - EList _variables_2 = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.lookup(variable_1, relationVar2VLS)); - _variables_2.add(_duplicate); - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_3 = reldef.getVariables(); - for (final Variable variable_2 : _variables_3) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_4) -> { - it_4.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); - EList _terms = it_3.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - it_2.setLeft(_doubleArrow); - Collection _values = relationVar2TypeDecComply.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setRight(this.support.unfoldAnd(_arrayList)); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - int _length = nameArray.length; - int _minus = (_length - 2); - int _length_1 = nameArray.length; - int _minus_1 = (_length_1 - 1); - it.setName(this.support.toIDMultiple("relation", nameArray[_minus], - nameArray[_minus_1])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables_1 = reldef.getVariables(); - for (final Variable variable_1 : _variables_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_2) -> { - it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_3); - EList _variables_2 = it_1.getVariables(); - _variables_2.add(v); - } - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { - Collection _values = relationVar2TypeDecRes.values(); - ArrayList _arrayList = new ArrayList(_values); - it_2.setLeft(this.support.unfoldAnd(_arrayList)); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_3) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_5 = (VLSFunction it_4) -> { - it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); - EList _variables_2 = reldef.getVariables(); - for (final Variable variable_2 : _variables_2) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_5) -> { - it_5.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - EList _terms = it_4.getTerms(); - _terms.add(v); - } - } - }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); - it_3.setLeft(_doubleArrow); - it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_2.setRight(_doubleArrow); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(comply); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(res); } public void transformRelation(final Relation r, 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 89633ca1..f1d73bec 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 @@ -403,20 +403,14 @@ public class Logic2VampireLanguageMapper_Support { return _xifexpression; } - protected List listSubtypes(final Type t) { - List allSubtypes = CollectionLiterals.newArrayList(); - boolean _isEmpty = t.getSubtypes().isEmpty(); - boolean _not = (!_isEmpty); - if (_not) { - EList _subtypes = t.getSubtypes(); - for (final Type subt : _subtypes) { - { - allSubtypes.add(subt); - allSubtypes = this.listSubtypes(subt); - } + protected void listSubtypes(final Type t, final List allSubtypes) { + EList _subtypes = t.getSubtypes(); + for (final Type subt : _subtypes) { + { + allSubtypes.add(subt); + this.listSubtypes(subt, allSubtypes); } } - return allSubtypes; } protected HashMap withAddition(final Map map1, final Map map2) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java index 9b8f049d..b9c1d28d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java @@ -78,16 +78,19 @@ public class Logic2VampireLanguageMapper_TypeMapper { EList _elements = type_1.getElements(); for (final DefinedElement e : _elements) { { + final String[] nameArray = e.getName().split(" "); + String relNameVar = ""; + int _length = nameArray.length; + boolean _equals = (_length == 3); + if (_equals) { + relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); + } else { + relNameVar = e.getName(); + } + final String relName = relNameVar; VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - final String[] splitName = e.getName().split(" "); - int _length = splitName.length; - boolean _greaterThan = (_length > 2); - if (_greaterThan) { - it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); - } else { - it.setConstant(this.support.toIDMultiple("e", splitName[0])); - } + it.setConstant(this.support.toIDMultiple("e", relName)); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); @@ -123,7 +126,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); + it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { @@ -160,10 +163,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final int index = i; + final int index = (i - globalCounter); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_3 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + it.setName(this.support.toIDMultiple("enumScope", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), type_1.getElements().get(index).getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/filesystem.aird b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/filesystem.aird new file mode 100644 index 00000000..50f2ba11 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/filesystem.aird @@ -0,0 +1,379 @@ + + + + filesystem.ecore + filesystem.genmodel + + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + labelSize + bold + + + labelSize + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/yakindu.aird b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/yakindu.aird index ef3746fa..be45a301 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/yakindu.aird +++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/metamodels/yakindu.aird @@ -52,7 +52,7 @@ - + @@ -61,7 +61,7 @@ - + @@ -70,7 +70,7 @@ - + @@ -79,7 +79,7 @@ - + @@ -88,7 +88,7 @@ - + @@ -97,7 +97,7 @@ - + @@ -106,7 +106,7 @@ - + @@ -115,7 +115,7 @@ - + @@ -124,7 +124,7 @@ - + @@ -133,7 +133,7 @@ - + @@ -142,7 +142,7 @@ - + @@ -151,7 +151,7 @@ - + @@ -160,22 +160,22 @@ - + - + - + - + - + @@ -191,7 +191,7 @@ - + @@ -207,7 +207,7 @@ - + @@ -223,7 +223,7 @@ - + @@ -239,7 +239,7 @@ - + @@ -255,7 +255,7 @@ - + @@ -271,7 +271,7 @@ - + @@ -287,7 +287,7 @@ - + @@ -303,7 +303,7 @@ - + @@ -319,7 +319,7 @@ - + @@ -335,7 +335,7 @@ - + @@ -351,39 +351,39 @@ - + - + - + - + - + - + - + - + - + @@ -392,6 +392,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO italic @@ -401,6 +404,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO italic @@ -410,6 +416,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -418,6 +427,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -426,6 +438,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -434,6 +449,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -442,6 +460,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -450,6 +471,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -458,6 +482,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO italic @@ -467,6 +494,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO italic @@ -476,6 +506,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -484,6 +517,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO @@ -492,6 +528,9 @@ + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml index f9d517b9..c0c367a1 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/plugin.xml @@ -20,13 +20,6 @@ - - - - - - - diff --git a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/src-gen/ca/mcgill/ecse/dslreasoner/standalone/test/fam/queries/TerminatorAndInformation.java b/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/src-gen/ca/mcgill/ecse/dslreasoner/standalone/test/fam/queries/TerminatorAndInformation.java deleted file mode 100644 index 69a6b9f4..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.standalone.test/src-gen/ca/mcgill/ecse/dslreasoner/standalone/test/fam/queries/TerminatorAndInformation.java +++ /dev/null @@ -1,747 +0,0 @@ -/** - * Generated from platform:/resource/ca.mcgill.ecse.dslreasoner.standalone.test/queries/ca/mcgill/ecse/dslreasoner/standalone/test/fam/queries/famPatterns.vql - */ -package ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries; - -import ca.mcgill.ecse.dslreasoner.standalone.test.fam.FAMTerminator; -import ca.mcgill.ecse.dslreasoner.standalone.test.fam.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.standalone.test.fam.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.standalone.test.fam.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.standalone.test.fam.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((ca.mcgill.ecse.dslreasoner.standalone.test.fam.FAMTerminator) parameters[0], (ca.mcgill.ecse.dslreasoner.standalone.test.fam.InformationLink) parameters[1]); - } - - /** - * Inner class allowing the singleton instance of {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.TerminatorAndInformation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.standalone.test.fam.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.standalone.test.fam.queries.TerminatorAndInformation (visibility: PUBLIC, simpleName: TerminatorAndInformation, identifier: ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.TerminatorAndInformation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.standalone.test.fam.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", "ca.mcgill.ecse.dslreasoner.standalone.test.fam.FAMTerminator", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("FamMetamodel", "FAMTerminator")), PParameterDirection.INOUT); - - private final PParameter parameter_I = new PParameter("I", "ca.mcgill.ecse.dslreasoner.standalone.test.fam.InformationLink", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("FamMetamodel", "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.standalone.test.fam.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("FamMetamodel", "FAMTerminator"))); - new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "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("FamMetamodel", "FunctionalOutput"))); - PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}"); - new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FamMetamodel", "FunctionalOutput", "outgoingLinks"))); - new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "InformationLink"))); - new Equality(body, var__virtual_0_, var_I); - // FunctionalOutput.terminator(Out,T) - new TypeConstraint(body, Tuples.flatTupleOf(var_Out), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "FunctionalOutput"))); - PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}"); - new TypeConstraint(body, Tuples.flatTupleOf(var_Out, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FamMetamodel", "FunctionalData", "terminator"))); - new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "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("FamMetamodel", "FAMTerminator"))); - new TypeConstraint(body, Tuples.flatTupleOf(var_I), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "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("FamMetamodel", "InformationLink"))); - PVariable var__virtual_0_ = body.getOrCreateVariableByName(".virtual{0}"); - new TypeConstraint(body, Tuples.flatTupleOf(var_I, var__virtual_0_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FamMetamodel", "InformationLink", "to"))); - new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_0_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "FunctionalInput"))); - new Equality(body, var__virtual_0_, var_In); - // FunctionalInput.terminator(In,T) - new TypeConstraint(body, Tuples.flatTupleOf(var_In), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "FunctionalInput"))); - PVariable var__virtual_1_ = body.getOrCreateVariableByName(".virtual{1}"); - new TypeConstraint(body, Tuples.flatTupleOf(var_In, var__virtual_1_), new EStructuralFeatureInstancesKey(getFeatureLiteral("FamMetamodel", "FunctionalData", "terminator"))); - new TypeConstraint(body, Tuples.flatTupleOf(var__virtual_1_), new EClassTransitiveInstancesKey((EClass)getClassifierLiteral("FamMetamodel", "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/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath index 3f0838b6..f03a6d83 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath @@ -5,5 +5,6 @@ + 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 2ea274a4..8b69d9a8 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 @@ -3,7 +3,11 @@ 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 +Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, + ca.mcgill.ecse.dslreasoner.vampire.test.queries.ecore, + ca.mcgill.ecse.dslreasoner.vampire.test.queries.fam, + ca.mcgill.ecse.dslreasoner.vampire.test.queries.filesystem, + ca.mcgill.ecse.dslreasoner.vampire.test.queries.yakindu Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, org.eclipse.emf.ecore, org.eclipse.viatra.query.runtime.rete, diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FaModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FaModel.xmi new file mode 100644 index 00000000..cef17e1b --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FAM/FaModel.xmi @@ -0,0 +1,7 @@ + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi deleted file mode 100644 index cef17e1b..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/FaModel.xmi +++ /dev/null @@ -1,7 +0,0 @@ - - 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 18e58ab0..4f0bbdb1 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,6 +10,8 @@ + + @@ -557,7 +559,8 @@ - + + 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 deleted file mode 100644 index 3d49d42c..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ /dev/null @@ -1,72 +0,0 @@ -% This is an initial Test Comment -fof ( typeDef_FunctionType , axiom , ! [ A ] : ( t_FunctionType ( A ) <=> ( object ( A ) & ( ( e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ( ~ e_Root_FunctionType ( A ) & ( e_Intermediate_FunctionType ( A ) & ~ e_Leaf_FunctionType ( A ) ) ) | ( ~ e_Root_FunctionType ( A ) & ( ~ e_Intermediate_FunctionType ( A ) & e_Leaf_FunctionType ( A ) ) ) ) ) ) ) ) . -fof ( enumScope_FunctionType_Root , axiom , ! [ A ] : ( A = eo1 <=> e_Root_FunctionType ( A ) ) ) . -fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_Intermediate_FunctionType ( A ) ) ) . -fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_FunctionType ( A ) ) ) . -fof ( notObjectHandler , axiom , ! [ A ] : ( ~ object ( A ) <=> ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ~ t_FunctionType ( A ) ) ) ) ) ) ) ) ) ) ) ) . -fof ( inheritanceHierarchyHandler , axiom , ! [ A ] : ( object ( A ) <=> ( ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalOutput ( A ) & ( t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( t_InformationLink ( A ) & ~ t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionalInput ( A ) & ( ~ t_Function ( A ) & ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalOutput ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_InformationLink ( A ) & t_FunctionalInterface ( A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . -fof ( typeScope_min_object , axiom , ! [ A ] : ( ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = eo1 | ( A = eo2 | A = eo3 ) ) ) ) ) ) => object ( A ) ) ) . -fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | A = o5 ) ) ) ) ) ) ) ) ) . -fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o2 => ( t_Function ( A ) & object ( A ) ) ) ) . -fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o3 | ( A = o4 | A = o5 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . -fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o6 | A = o7 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . -fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o2 ) ) . -fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o3 | ( A = o4 | A = o5 ) ) ) ) . -fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & eo1 != o5 ) ) ) ) ) ) . -fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & eo2 != o5 ) ) ) ) ) . -fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & eo3 != o5 ) ) ) ) . -fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & o1 != o5 ) ) ) . -fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & o2 != o5 ) ) . -fof ( t_uniqueness_o3 , axiom , o3 != o4 & o3 != o5 ) . -fof ( t_uniqueness_o4 , axiom , o4 != o5 ) . -fof ( compliance_interface_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . -fof ( compliance_model_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_model_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_FunctionalArchitectureModel ( V_1 ) ) ) ) . -fof ( compliance_parent_FunctionalElement , axiom , ! [ V_0 , V_1 ] : ( r_parent_FunctionalElement ( V_0 , V_1 ) => ( t_FunctionalElement ( V_0 ) & t_Function ( V_1 ) ) ) ) . -fof ( compliance_rootElements_FunctionalArchitectureModel , axiom , ! [ V_0 , V_1 ] : ( r_rootElements_FunctionalArchitectureModel ( V_0 , V_1 ) => ( t_FunctionalArchitectureModel ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . -fof ( compliance_subElements_Function , axiom , ! [ V_0 , V_1 ] : ( r_subElements_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . -fof ( compliance_data_FAMTerminator , axiom , ! [ V_0 , V_1 ] : ( r_data_FAMTerminator ( V_0 , V_1 ) => ( t_FAMTerminator ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . -fof ( compliance_from_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_from_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalOutput ( V_1 ) ) ) ) . -fof ( compliance_to_InformationLink , axiom , ! [ V_0 , V_1 ] : ( r_to_InformationLink ( V_0 , V_1 ) => ( t_InformationLink ( V_0 ) & t_FunctionalInput ( V_1 ) ) ) ) . -fof ( compliance_data_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_data_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalData ( V_1 ) ) ) ) . -fof ( compliance_element_FunctionalInterface , axiom , ! [ V_0 , V_1 ] : ( r_element_FunctionalInterface ( V_0 , V_1 ) => ( t_FunctionalInterface ( V_0 ) & t_FunctionalElement ( V_1 ) ) ) ) . -fof ( compliance_IncomingLinks_FunctionalInput , axiom , ! [ V_0 , V_1 ] : ( r_IncomingLinks_FunctionalInput ( V_0 , V_1 ) => ( t_FunctionalInput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . -fof ( compliance_outgoingLinks_FunctionalOutput , axiom , ! [ V_0 , V_1 ] : ( r_outgoingLinks_FunctionalOutput ( V_0 , V_1 ) => ( t_FunctionalOutput ( V_0 ) & t_InformationLink ( V_1 ) ) ) ) . -fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_terminator_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FAMTerminator ( V_1 ) ) ) ) . -fof ( compliance_interface_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_interface_FunctionalData ( V_0 , V_1 ) => ( t_FunctionalData ( V_0 ) & t_FunctionalInterface ( V_1 ) ) ) ) . -fof ( compliance_type_Function , axiom , ! [ V_0 , V_1 ] : ( r_type_Function ( V_0 , V_1 ) => ( t_Function ( V_0 ) & t_FunctionType ( V_1 ) ) ) ) . -fof ( containment_topLevel_t_FunctionalArchitectureModel , axiom , ! [ A ] : ( t_FunctionalArchitectureModel ( A ) <=> A = o1 ) ) . -fof ( containment_noDup_r_interface_FunctionalElement , axiom , ? [ A , B ] : ( r_interface_FunctionalElement ( A , B ) => ~ ? [ C , B ] : r_interface_FunctionalElement ( C , B ) ) ) . -fof ( containment_noDup_r_rootElements_FunctionalArchitectureModel , axiom , ? [ A , B ] : ( r_rootElements_FunctionalArchitectureModel ( A , B ) => ~ ? [ C , B ] : r_rootElements_FunctionalArchitectureModel ( C , B ) ) ) . -fof ( containment_noDup_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_Function ( A , B ) => ~ ? [ C , B ] : r_subElements_Function ( C , B ) ) ) . -fof ( containment_noDup_r_data_FunctionalInterface , axiom , ? [ A , B ] : ( r_data_FunctionalInterface ( A , B ) => ~ ? [ C , B ] : r_data_FunctionalInterface ( C , B ) ) ) . -fof ( containment_noDup_r_outgoingLinks_FunctionalOutput , axiom , ? [ A , B ] : ( r_outgoingLinks_FunctionalOutput ( A , B ) => ~ ? [ C , B ] : r_outgoingLinks_FunctionalOutput ( C , B ) ) ) . -fof ( containment_noDup_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_terminator_FunctionalData ( A , B ) => ~ ? [ C , B ] : r_terminator_FunctionalData ( C , B ) ) ) . -fof ( containment_t_FunctionalElement , axiom , ! [ A ] : ( t_FunctionalElement ( A ) => ? [ B ] : ( ( r_rootElements_FunctionalArchitectureModel ( B , A ) & ~ r_subElements_Function ( B , A ) ) | ( ~ r_rootElements_FunctionalArchitectureModel ( B , A ) & r_subElements_Function ( B , A ) ) ) ) ) . -fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) . -fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) . -fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) . -fof ( containment_t_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) . -fof ( containment_noCycle_1 , axiom , ~ ? [ V1 ] : ( r_interface_FunctionalElement ( V1 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V1 ) | ( r_subElements_Function ( V1 , V1 ) | ( r_data_FunctionalInterface ( V1 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V1 ) | r_terminator_FunctionalData ( V1 , V1 ) ) ) ) ) ) ) . -fof ( containment_noCycle_2 , axiom , ~ ? [ V1 , V2 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V2 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V1 ) | ( r_subElements_Function ( V2 , V1 ) | ( r_data_FunctionalInterface ( V2 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V1 ) | r_terminator_FunctionalData ( V2 , V1 ) ) ) ) ) ) ) ) . -fof ( containment_noCycle_3 , axiom , ~ ? [ V1 , V2 , V3 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V3 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V1 ) | ( r_subElements_Function ( V3 , V1 ) | ( r_data_FunctionalInterface ( V3 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V1 ) | r_terminator_FunctionalData ( V3 , V1 ) ) ) ) ) ) ) ) ) . -fof ( containment_noCycle_4 , axiom , ~ ? [ V1 , V2 , V3 , V4 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V4 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V1 ) | ( r_subElements_Function ( V4 , V1 ) | ( r_data_FunctionalInterface ( V4 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V1 ) | r_terminator_FunctionalData ( V4 , V1 ) ) ) ) ) ) ) ) ) ) . -fof ( containment_noCycle_5 , axiom , ~ ? [ V1 , V2 , V3 , V4 , V5 ] : ( ( r_interface_FunctionalElement ( V1 , V2 ) | ( r_rootElements_FunctionalArchitectureModel ( V1 , V2 ) | ( r_subElements_Function ( V1 , V2 ) | ( r_data_FunctionalInterface ( V1 , V2 ) | ( r_outgoingLinks_FunctionalOutput ( V1 , V2 ) | r_terminator_FunctionalData ( V1 , V2 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V2 , V3 ) | ( r_rootElements_FunctionalArchitectureModel ( V2 , V3 ) | ( r_subElements_Function ( V2 , V3 ) | ( r_data_FunctionalInterface ( V2 , V3 ) | ( r_outgoingLinks_FunctionalOutput ( V2 , V3 ) | r_terminator_FunctionalData ( V2 , V3 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V3 , V4 ) | ( r_rootElements_FunctionalArchitectureModel ( V3 , V4 ) | ( r_subElements_Function ( V3 , V4 ) | ( r_data_FunctionalInterface ( V3 , V4 ) | ( r_outgoingLinks_FunctionalOutput ( V3 , V4 ) | r_terminator_FunctionalData ( V3 , V4 ) ) ) ) ) ) & ( ( r_interface_FunctionalElement ( V4 , V5 ) | ( r_rootElements_FunctionalArchitectureModel ( V4 , V5 ) | ( r_subElements_Function ( V4 , V5 ) | ( r_data_FunctionalInterface ( V4 , V5 ) | ( r_outgoingLinks_FunctionalOutput ( V4 , V5 ) | r_terminator_FunctionalData ( V4 , V5 ) ) ) ) ) ) & ( r_interface_FunctionalElement ( V5 , V1 ) | ( r_rootElements_FunctionalArchitectureModel ( V5 , V1 ) | ( r_subElements_Function ( V5 , V1 ) | ( r_data_FunctionalInterface ( V5 , V1 ) | ( r_outgoingLinks_FunctionalOutput ( V5 , V1 ) | r_terminator_FunctionalData ( V5 , V1 ) ) ) ) ) ) ) ) ) ) ) . -fof ( upperMultiplicity_interface_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalElement ( V_src , V_trg_1 ) & r_interface_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( lowerMultiplicity_model_FunctionalElement , axiom , ! [ V_src ] : ( t_FunctionalElement ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalArchitectureModel ( V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_1 ) ) ) ) . -fof ( upperMultiplicity_model_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_FunctionalArchitectureModel ( V_trg_1 ) & t_FunctionalArchitectureModel ( V_trg_2 ) ) ) => ( ( r_model_FunctionalElement ( V_src , V_trg_1 ) & r_model_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_parent_FunctionalElement , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalElement ( V_src ) & ( t_Function ( V_trg_1 ) & t_Function ( V_trg_2 ) ) ) => ( ( r_parent_FunctionalElement ( V_src , V_trg_1 ) & r_parent_FunctionalElement ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_data_FAMTerminator , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FAMTerminator ( V_src ) & ( t_FunctionalData ( V_trg_1 ) & t_FunctionalData ( V_trg_2 ) ) ) => ( ( r_data_FAMTerminator ( V_src , V_trg_1 ) & r_data_FAMTerminator ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_from_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalOutput ( V_trg_1 ) & t_FunctionalOutput ( V_trg_2 ) ) ) => ( ( r_from_InformationLink ( V_src , V_trg_1 ) & r_from_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( lowerMultiplicity_to_InformationLink , axiom , ! [ V_src ] : ( t_InformationLink ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionalInput ( V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_1 ) ) ) ) . -fof ( upperMultiplicity_to_InformationLink , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_InformationLink ( V_src ) & ( t_FunctionalInput ( V_trg_1 ) & t_FunctionalInput ( V_trg_2 ) ) ) => ( ( r_to_InformationLink ( V_src , V_trg_1 ) & r_to_InformationLink ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_element_FunctionalInterface , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalInterface ( V_src ) & ( t_FunctionalElement ( V_trg_1 ) & t_FunctionalElement ( V_trg_2 ) ) ) => ( ( r_element_FunctionalInterface ( V_src , V_trg_1 ) & r_element_FunctionalInterface ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_terminator_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FAMTerminator ( V_trg_1 ) & t_FAMTerminator ( V_trg_2 ) ) ) => ( ( r_terminator_FunctionalData ( V_src , V_trg_1 ) & r_terminator_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( upperMultiplicity_interface_FunctionalData , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_FunctionalData ( V_src ) & ( t_FunctionalInterface ( V_trg_1 ) & t_FunctionalInterface ( V_trg_2 ) ) ) => ( ( r_interface_FunctionalData ( V_src , V_trg_1 ) & r_interface_FunctionalData ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . -fof ( oppositeReference_interface_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_FunctionalInterface ( V_trg ) ) => ( r_interface_FunctionalElement ( V_src , V_trg ) <=> r_element_FunctionalInterface ( V_trg , V_src ) ) ) ) . -fof ( oppositeReference_parent_FunctionalElement , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalElement ( V_src ) & t_Function ( V_trg ) ) => ( r_parent_FunctionalElement ( V_src , V_trg ) <=> r_subElements_Function ( V_trg , V_src ) ) ) ) . -fof ( oppositeReference_data_FAMTerminator , axiom , ! [ V_src , V_trg ] : ( ( t_FAMTerminator ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FAMTerminator ( V_src , V_trg ) <=> r_terminator_FunctionalData ( V_trg , V_src ) ) ) ) . -fof ( oppositeReference_from_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalOutput ( V_trg ) ) => ( r_from_InformationLink ( V_src , V_trg ) <=> r_outgoingLinks_FunctionalOutput ( V_trg , V_src ) ) ) ) . -fof ( oppositeReference_to_InformationLink , axiom , ! [ V_src , V_trg ] : ( ( t_InformationLink ( V_src ) & t_FunctionalInput ( V_trg ) ) => ( r_to_InformationLink ( V_src , V_trg ) <=> r_IncomingLinks_FunctionalInput ( V_trg , V_src ) ) ) ) . -fof ( oppositeReference_data_FunctionalInterface , axiom , ! [ V_src , V_trg ] : ( ( t_FunctionalInterface ( V_src ) & t_FunctionalData ( V_trg ) ) => ( r_data_FunctionalInterface ( V_src , V_trg ) <=> r_interface_FunctionalData ( V_trg , V_src ) ) ) ) . -fof ( lowerMultiplicity_type_Function , axiom , ! [ V_src ] : ( t_Function ( V_src ) => ? [ V_trg_1 ] : ( t_FunctionType ( V_trg_1 ) & r_type_Function ( V_src , V_trg_1 ) ) ) ) . -fof ( upperMultiplicity_type_Function , axiom , ! [ V_src , V_trg_1 , V_trg_2 ] : ( ( t_Function ( V_src ) & ( t_FunctionType ( V_trg_1 ) & t_FunctionType ( V_trg_2 ) ) ) => ( ( r_type_Function ( V_src , V_trg_1 ) & r_type_Function ( V_src , V_trg_2 ) ) => ~ V_trg_1 != V_trg_2 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml index 3770f0af..0d17c01b 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml @@ -1,7 +1,10 @@ - - - + + + + + + @@ -11,7 +14,18 @@ + + + + + + + + + + + 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 deleted file mode 100644 index cf1378da..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.java +++ /dev/null @@ -1,53 +0,0 @@ -/** - * 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 deleted file mode 100644 index cb0708ad..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src-gen/ca/mcgill/ecse/dslreasoner/vampire/queries/TerminatorAndInformation.java +++ /dev/null @@ -1,747 +0,0 @@ -/** - * 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 18b3badd..35b76350 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 @@ -1,11 +1,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse +import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration -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 @@ -13,91 +12,48 @@ import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import java.util.List -import org.eclipse.emf.ecore.EAttribute -import org.eclipse.emf.ecore.EClass -import org.eclipse.emf.ecore.EEnum -import org.eclipse.emf.ecore.EEnumLiteral -import org.eclipse.emf.ecore.EObject -import org.eclipse.emf.ecore.EReference -import org.eclipse.emf.ecore.resource.Resource -import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl class EcoreTest { def static void main(String[] args) { val inputs = new FileSystemWorkspace('''initialModels/''', "") - val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") + val workspace = new FileSystemWorkspace('''output/FEcoreTest/''', "") workspace.initAndClear println("Input and output workspaces are created") - val metamodel = loadMetamodel() - val partialModel = loadPartialModel(inputs) -// val queries = loadQueries(metamodel) + val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE) + val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi") +// val queries = GeneralTest.loadQueries(metamodel, ecorePatterns.instance) + val queries = null println("DSL loaded") - + val Ecore2Logic ecore2Logic = new Ecore2Logic val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic - - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) - val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) + val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) // val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) - val logicProblem = modelGenerationProblem.output // val logicProblem = modelExtensionProblem.output // val logicProblem = validModelExtensionProblem.output - - println("Problem created") - + var LogicResult solution var LogicReasoner reasoner - //* + // * reasoner = new VampireSolver val vampireConfig = new VampireSolverConfiguration => [ - //add configuration things, in config file first + // add configuration things, in config file first it.documentationLevel = DocumentationLevel::FULL ] - - solution = reasoner.solve(logicProblem, vampireConfig, workspace) - - println("Problem solved") - - - } - def private static loadMetamodel() { - val pckg = FunctionalarchitecturePackage.eINSTANCE - 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) - } + solution = reasoner.solve(logicProblem, vampireConfig, workspace) - def private static loadPartialModel(ReasonerWorkspace inputs) { - Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); -// inputs.readModel(EObject,"FunctionalArchitectureModel.xmi").eResource.allContents.toList - inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList - } + println("Problem solved") - def private static loadQueries(EcoreMetamodelDescriptor metamodel) { -// val i = Patterns.instance -// val patterns = i.specifications.toList -// val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet -// val derivedFeatures = new LinkedHashMap -// derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) -// derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) -// val res = new ViatraQuerySetDescriptor( -// patterns, -// wfPatterns, -// derivedFeatures -// ) -// return res } + } 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 f66ad93c..3fc3d70f 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,6 +1,5 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import functionalarchitecture.Function @@ -39,14 +38,15 @@ class FAMTest { // Load DSL val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "FaModel.xmi") - val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) + val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") +// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) + val queries = null println("DSL loaded") val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) var problem = modelGenerationProblem.output -// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output + problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output workspace.writeModel(problem, "Fam.logicproblem") diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend index 50639577..d4cbb299 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend @@ -1,7 +1,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import ca.mcgill.ecse.dslreasoner.vampire.queries import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage +import ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic @@ -24,7 +24,7 @@ class FileSystemTest { // Workspace setup val inputs = new FileSystemWorkspace('''initialModels/''', "") - val workspace = new FileSystemWorkspace('''output/FAMTest/''', "") + val workspace = new FileSystemWorkspace('''output/FileSystemTest/''', "") workspace.initAndClear // Logicproblem writing setup @@ -34,9 +34,10 @@ class FileSystemTest { println("Input and output workspaces are created") + val metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi") - //val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance) + val queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance) println("DSL loaded") @@ -44,7 +45,7 @@ class FileSystemTest { var problem = modelGenerationProblem.output // problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output - workspace.writeModel(problem, "Fam.logicproblem") + workspace.writeModel(problem, "FileSystem.logicproblem") println("Problem created") @@ -75,8 +76,8 @@ class FileSystemTest { // add configuration things, in config file first it.documentationLevel = DocumentationLevel::FULL - it.typeScopes.minNewElements = 4 - it.typeScopes.maxNewElements = 5 + it.typeScopes.minNewElements = 40 + it.typeScopes.maxNewElements = 59 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 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 1fac968b..f0d88b49 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 @@ -35,7 +35,7 @@ class YakinduTest { val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") -// val queries = GeneralTest.loadQueries(metamodel, FamPa +// val queries = GeneralTest.loadQueries(metamodel, yakinduPatterns.instance) val queries = null println("DSL loaded") @@ -75,8 +75,8 @@ class YakinduTest { // add configuration things, in config file first it.documentationLevel = DocumentationLevel::FULL - it.typeScopes.minNewElements = 20 - it.typeScopes.maxNewElements = 30 + it.typeScopes.minNewElements = 53 + it.typeScopes.maxNewElements = 53 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 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 55d90ac7..2cecdaac 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 8eeb2d28..a34ab846 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 ab6aaf6e..a18fd1a5 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 cd75a66c..0969c84c 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 1b920064..f0af3ba5 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 820dd354..7019f162 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 @@ -1,9 +1,9 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; +import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage; +import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; -import com.google.common.collect.Iterables; -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.Ecore2Logic_Trace; @@ -17,27 +17,11 @@ import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; -import java.util.Collections; -import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; -import org.eclipse.emf.ecore.EAttribute; -import org.eclipse.emf.ecore.EClass; -import org.eclipse.emf.ecore.EEnum; -import org.eclipse.emf.ecore.EEnumLiteral; import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.EReference; -import org.eclipse.emf.ecore.resource.Resource; -import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Exceptions; -import org.eclipse.xtext.xbase.lib.Functions.Function1; import org.eclipse.xtext.xbase.lib.InputOutput; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.IteratorExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -49,12 +33,13 @@ public class EcoreTest { _builder.append("initialModels/"); final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FAMTest/"); + _builder_1.append("output/FEcoreTest/"); final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); workspace.initAndClear(); InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = EcoreTest.loadMetamodel(); - final List partialModel = EcoreTest.loadPartialModel(inputs); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); + final Object queries = null; InputOutput.println("DSL loaded"); final Ecore2Logic ecore2Logic = new Ecore2Logic(); final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); @@ -80,38 +65,4 @@ public class EcoreTest { throw Exceptions.sneakyThrow(_e); } } - - private static EcoreMetamodelDescriptor loadMetamodel() { - final FunctionalarchitecturePackage pckg = FunctionalarchitecturePackage.eINSTANCE; - final List classes = IterableExtensions.toList(Iterables.filter(pckg.getEClassifiers(), EClass.class)); - final List enums = IterableExtensions.toList(Iterables.filter(pckg.getEClassifiers(), EEnum.class)); - final Function1> _function = (EEnum it) -> { - return it.getELiterals(); - }; - final List literals = IterableExtensions.toList(Iterables.concat(ListExtensions.>map(enums, _function))); - final Function1> _function_1 = (EClass it) -> { - return it.getEReferences(); - }; - final List references = IterableExtensions.toList(Iterables.concat(ListExtensions.>map(classes, _function_1))); - final Function1> _function_2 = (EClass it) -> { - return it.getEAttributes(); - }; - final List attributes = IterableExtensions.toList(Iterables.concat(ListExtensions.>map(classes, _function_2))); - return new EcoreMetamodelDescriptor(classes, Collections.unmodifiableSet(CollectionLiterals.newHashSet()), false, enums, literals, references, attributes); - } - - private static List loadPartialModel(final ReasonerWorkspace inputs) { - List _xblockexpression = null; - { - Map _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - _extensionToFactoryMap.put("*", _xMIResourceFactoryImpl); - _xblockexpression = IteratorExtensions.toList(inputs.readModel(EObject.class, "FamInstance.xmi").eResource().getAllContents()); - } - return _xblockexpression; - } - - private static Object loadQueries(final EcoreMetamodelDescriptor metamodel) { - return null; - } } 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 5fc2a391..08f1b4a7 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,7 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; -import ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import functionalarchitecture.Function; @@ -18,7 +17,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; -import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; import java.util.HashMap; @@ -53,12 +51,13 @@ 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, "FaModel.xmi"); - final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); + final Object queries = null; InputOutput.println("DSL loaded"); Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); LogicProblem problem = modelGenerationProblem.getOutput(); + problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); workspace.writeModel(problem, "Fam.logicproblem"); InputOutput.println("Problem created"); long startTime = System.currentTimeMillis(); diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java index eedec995..f7f8a5ee 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java @@ -2,6 +2,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; +import ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; @@ -15,6 +16,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; +import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; import java.util.HashMap; @@ -40,7 +42,7 @@ public class FileSystemTest { _builder.append("initialModels/"); final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FAMTest/"); + _builder_1.append("output/FileSystemTest/"); final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); workspace.initAndClear(); final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; @@ -50,11 +52,12 @@ public class FileSystemTest { InputOutput.println("Input and output workspaces are created"); final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); + final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FileSystemPatterns.instance()); InputOutput.println("DSL loaded"); Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); LogicProblem problem = modelGenerationProblem.getOutput(); - workspace.writeModel(problem, "Fam.logicproblem"); + workspace.writeModel(problem, "FileSystem.logicproblem"); InputOutput.println("Problem created"); long startTime = System.currentTimeMillis(); LogicReasoner reasoner = null; @@ -67,8 +70,8 @@ public class FileSystemTest { VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { it.documentationLevel = DocumentationLevel.FULL; - it.typeScopes.minNewElements = 4; - it.typeScopes.maxNewElements = 5; + it.typeScopes.minNewElements = 40; + it.typeScopes.maxNewElements = 59; int _size = typeMapMin.size(); boolean _notEquals = (_size != 0); if (_notEquals) { 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 81079764..3a322ee0 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 @@ -68,8 +68,8 @@ public class YakinduTest { VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); final Procedure1 _function = (VampireSolverConfiguration it) -> { it.documentationLevel = DocumentationLevel.FULL; - it.typeScopes.minNewElements = 20; - it.typeScopes.maxNewElements = 30; + it.typeScopes.minNewElements = 53; + it.typeScopes.maxNewElements = 53; int _size = typeMapMin.size(); boolean _notEquals = (_size != 0); if (_notEquals) { 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 29f8df00..c5ed4b90 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 72d33e5d..21fdd9b7 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 e9c4c0a4..b1887ff2 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf