From b1bbb821c0e5a3f721de211826dab19c7d9dca4f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 5 Apr 2019 03:32:48 -0400 Subject: Implement containment circularity avoidance #20 --- .../model/FamMetamodel.aird | 644 +++++++++++++++++++++ .../plugin.xml | 18 +- .../dslreasoner/vampire/queries/vampireQueries.vql | 6 +- .../reasoner/VampireAnalyzerConfiguration.xtend | 3 +- .../builder/Logic2VampireLanguageMapper.xtend | 2 +- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 46 +- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 13 +- .../Logic2VampireLanguageMapper_Support.xtend | 8 + .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../reasoner/VampireSolverConfiguration.java | 3 + .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18129 -> 18157 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 9493 -> 10551 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8210 -> 8209 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9828 -> 9839 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 12892 -> 13092 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10704 -> 10705 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes .../builder/Logic2VampireLanguageMapper.java | 2 +- ...ic2VampireLanguageMapper_ContainmentMapper.java | 57 +- .../Logic2VampireLanguageMapper_ScopeMapper.java | 8 +- .../Logic2VampireLanguageMapper_Support.java | 8 + .../output/FAMTest/vampireProblem.tptp | 64 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 4 +- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 6358 -> 6358 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 8578 -> 8623 bytes .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 4 +- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 30 files changed, 838 insertions(+), 52 deletions(-) create mode 100644 Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.aird diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.aird b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.aird new file mode 100644 index 00000000..14cf13c6 --- /dev/null +++ b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.aird @@ -0,0 +1,644 @@ + + + + FamMetamodel.ecore + FamMetamodel.genmodel + + + + + + + + + + + + + + + + + + + + + + + bold + + + + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + bold + + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + bold + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + + + + + + + + KEEP_LOCATION + KEEP_SIZE + KEEP_RATIO + + italic + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + labelSize + + + labelSize + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + italic + + + + + + + + + + + + + + + + + + + + + + bold + + + bold + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml index 2381b84f..beaf5498 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml @@ -1 +1,17 @@ - + + + + + + + + + + + + + + + + + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql index 2bc22f9e..ef61e4d1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql @@ -48,9 +48,9 @@ pattern VLSInequality(term: VLSInequality){ VLSInequality(term); } -pattern VLSFunctionFof(term: VLSFunctionFof){ - VLSFunctionFof(term); -} +//pattern VLSFunctionFof(term: VLSFunctionFof){ +// VLSFunctionFof(term); +//} //pattern VLSFofTerm(term: VLSFofTerm){ // VLSFofTerm(term); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 618980a3..98967181 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -4,7 +4,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration class VampireSolverConfiguration extends LogicSolverConfiguration { - //public var int symmetry = 0 // by default + public var int contCycleLevel = 0 + public var boolean uniquenessDuplicates = false //choose needed backend solver // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index b7ad8f3d..2be6c093 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -87,7 +87,7 @@ class Logic2VampireLanguageMapper { problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] // CONTAINMENT MAPPER - containmentMapper.transformContainment(problem.containmentHierarchies, trace) + containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) // CONSTANT MAPPER // only transforms definitions 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 48ee8789..395b4305 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 @@ -1,6 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable @@ -25,9 +25,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { this.base = base } - def public void transformContainment(List hierarchies, + def public void transformContainment(VampireSolverConfiguration config, List hierarchies, Logic2VampireLanguageMapperTrace trace) { - //TODO throw error is there exists a circular containment that does not involve hierarchy + // TODO throw error is there exists a circular containment that does not involve hierarchy // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST // TEMP val hierarchy = hierarchies.get(0) @@ -94,7 +94,6 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // for (c : support.listSubtypes(toType)) { // addToMap(type2cont, toFunc, rel) // } - // val listForAnd = newArrayList //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) @@ -111,7 +110,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { // STEP 3 // Ensure that an objct only has 1 parent val relFormula = createVLSFofFormula => [ - it.name = support.toIDMultiple("noDupCont", rel.constant.toString) + it.name = support.toIDMultiple("containment_noDup", rel.constant.toString) it.fofRole = "axiom" it.fofFormula = createVLSExistentialQuantifier => [ it.variables += support.duplicate(varA) @@ -133,7 +132,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } -// STEP CONT'D +// STEP 2 CONT'D for (e : type2cont.entrySet) { val relFormula = createVLSFofFormula => [ it.name = support.toIDMultiple("containment", e.key.constant.toString) @@ -159,8 +158,39 @@ class Logic2VampireLanguageMapper_ContainmentMapper { } - // STEP 4 - // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + // STEP 4 + // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed + + + val variables = newArrayList + val disjunctionList = newArrayList + val conjunctionList = newArrayList + for (var i = 1; i <= config.contCycleLevel; i++) { + val ind = i + variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) + for ( var j = 0; j < i;j++){ + for (l : relationsList) { + val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) + disjunctionList.add(rel) + } + conjunctionList.add(support.unfoldOr(disjunctionList)) + disjunctionList.clear + } + + val contCycleForm = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) + it.fofRole = "axiom" + it.fofFormula = createVLSUnaryNegation => [ + it.operand = createVLSExistentialQuantifier => [ + it.variables += support.duplicate(variables) + it.operand = support.unfoldAnd(conjunctionList) + ] + ] + ] + trace.specification.formulas += contCycleForm + conjunctionList.clear + } } protected def VLSTerm makeUnique(List list) { 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 0d0be576..0a8812e4 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 @@ -1,17 +1,15 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import java.util.ArrayList +import java.util.HashMap import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.HashMap -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm -import java.util.List class Logic2VampireLanguageMapper_ScopeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -23,7 +21,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { this.base = base } - def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { + def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { val ABSOLUTE_MIN = 0 val ABSOLUTE_MAX = Integer.MAX_VALUE @@ -40,7 +38,6 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != ABSOLUTE_MIN) { - // * getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) if (consistant) { for (i : trace.uniqueInstances) { @@ -94,7 +91,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { // 3. Specify uniqueness of elements // TEMP - val DUPLICATES = false + val DUPLICATES = config.uniquenessDuplicates val numInst = trace.uniqueInstances.length var ind = 1 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 dd88a53a..195b89bb 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 @@ -77,6 +77,14 @@ class Logic2VampireLanguageMapper_Support { it.terms += duplicate(v) ] } + + def protected List duplicate(List vars) { + var newList = newArrayList + for (v : vars) { + newList.add(duplicate(v)) + } + return newList + } def protected VLSConstant toConstant(VLSFunctionAsTerm term) { return createVLSConstant => [ 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 b5e03979..7394b24e 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 0714f36d..d328dcf2 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/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index 1f6b3d42..ac55ebd7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java @@ -4,4 +4,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; @SuppressWarnings("all") public class VampireSolverConfiguration extends LogicSolverConfiguration { + public int contCycleLevel = 0; + + public boolean uniquenessDuplicates = false; } 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 2cc60591..968a2df8 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/.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 01b0a351..48756fcc 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 cf049bd5..44b06208 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 7bc04e7b..4cab8309 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 a97c7186..ccddb430 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 a473c586..a069a62f 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 4e7796fe..46cd58fb 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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 84d6c63a..1b5e4d0b 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 36a727b2..f04bd7dc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper { this.relationMapper.transformRelation(it, trace); }; problem.getRelations().forEach(_function_3); - this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); + this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); trace.constantDefinitions = this.collectConstantDefinitions(problem); final Consumer _function_4 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); 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 7bc70e9d..4cdc7e6a 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 @@ -1,5 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 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; @@ -16,6 +17,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; +import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; @@ -52,7 +54,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { this.base = base; } - public void transformContainment(final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { + public void transformContainment(final VampireSolverConfiguration config, final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { final ContainmentHierarchy hierarchy = hierarchies.get(0); final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); final EList relationsList = hierarchy.getContainmentRelations(); @@ -135,7 +137,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); + it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); it.setFofRole("axiom"); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_5 = (VLSExistentialQuantifier it_1) -> { @@ -219,6 +221,57 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { _formulas_1.add(relFormula); } } + final ArrayList variables = CollectionLiterals.newArrayList(); + final ArrayList disjunctionList = CollectionLiterals.newArrayList(); + final ArrayList conjunctionList = CollectionLiterals.newArrayList(); + for (int i = 1; (i <= config.contCycleLevel); i++) { + { + final int ind = i; + VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it) -> { + String _string = Integer.toString(ind); + String _plus = ("V" + _string); + it.setName(_plus); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_3, _function_4); + variables.add(_doubleArrow); + for (int j = 0; (j < i); j++) { + { + for (final Relation l_2 : relationsList) { + { + final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); + disjunctionList.add(rel); + } + } + conjunctionList.add(this.support.unfoldOr(disjunctionList)); + disjunctionList.clear(); + } + } + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_5 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); + it.setFofRole("axiom"); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_6 = (VLSUnaryNegation it_1) -> { + VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); + final Procedure1 _function_7 = (VLSExistentialQuantifier it_2) -> { + EList _variables = it_2.getVariables(); + List _duplicate = this.support.duplicate(variables); + Iterables.addAll(_variables, _duplicate); + it_2.setOperand(this.support.unfoldAnd(conjunctionList)); + }; + VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); + it_1.setOperand(_doubleArrow_1); + }; + VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_6); + it.setFofFormula(_doubleArrow_1); + }; + final VLSFofFormula contCycleForm = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_5); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(contCycleForm); + conjunctionList.clear(); + } + } } protected VLSTerm makeUnique(final List list) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 83543c92..f5d35b28 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -1,5 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 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; @@ -13,7 +14,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; @@ -47,7 +47,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.base = base; } - public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int ABSOLUTE_MIN = 0; final int ABSOLUTE_MAX = Integer.MAX_VALUE; final int GLOBAL_MIN = config.typeScopes.minNewElements; @@ -105,7 +105,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } } - final boolean DUPLICATES = false; + final boolean DUPLICATES = config.uniquenessDuplicates; final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; int ind = 1; if ((numInst != 0)) { @@ -246,7 +246,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { _formulas.add(cstDec); } - public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { _transformScope(config, trace); return; } 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 513618a9..89633ca1 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 @@ -129,6 +129,14 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected List duplicate(final List vars) { + ArrayList newList = CollectionLiterals.newArrayList(); + for (final VLSVariable v : vars) { + newList.add(this.duplicate(v)); + } + return newList; + } + protected VLSConstant toConstant(final VLSFunctionAsTerm term) { VLSConstant _createVLSConstant = this.factory.createVLSConstant(); final Procedure1 _function = (VLSConstant it) -> { diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp index 2f2d9718..b4bb6700 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/vampireProblem.tptp @@ -6,22 +6,39 @@ fof ( enumScope_FunctionType_Leaf , axiom , ! [ A ] : ( A = eo3 <=> e_Leaf_Funct 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_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( ~ t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( t_FunctionalInput ( A ) & ~ t_FunctionalOutput ( A ) ) ) ) ) ) ) ) ) ) | ( ~ t_FAMTerminator ( A ) & ( t_FunctionalData ( A ) & ( ~ t_FunctionalInterface ( A ) & ( ~ t_Function ( A ) & ( ~ t_InformationLink ( A ) & ( ~ t_FunctionalElement ( A ) & ( ~ t_FunctionalArchitectureModel ( A ) & ( ~ t_FunctionType ( A ) & ( ~ t_FunctionalInput ( A ) & t_FunctionalOutput ( 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 | ( A = o6 | A = o7 ) ) ) ) ) ) ) ) ) ) ) . +fof ( typeScope_max_object , axiom , ! [ A ] : ( object ( A ) => ( A = eo1 | ( A = eo2 | ( A = eo3 | ( A = o1 | ( A = o2 | ( A = o3 | ( A = o4 | ( A = o5 | ( A = o6 | ( A = o7 | ( A = o8 | ( A = o9 | ( A = o10 | ( A = o11 | ( A = o12 | ( A = o13 | ( A = o14 | ( A = o15 | ( A = o16 | ( A = o17 | ( A = o18 | ( A = o19 | ( A = o20 | ( A = o21 | ( A = o22 | ( A = o23 | ( A = o24 | A = o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . fof ( typeScope_min_t_FunctionalInterface , axiom , ! [ A ] : ( ( A = o2 | A = o3 ) => ( t_FunctionalInterface ( A ) & object ( A ) ) ) ) . fof ( typeScope_min_t_Function , axiom , ! [ A ] : ( A = o4 => ( t_Function ( A ) & object ( A ) ) ) ) . fof ( typeScope_min_t_FunctionalOutput , axiom , ! [ A ] : ( ( A = o5 | ( A = o6 | A = o7 ) ) => ( t_FunctionalOutput ( A ) & object ( A ) ) ) ) . -fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => A = o4 ) ) . -fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | A = o7 ) ) ) ) . -fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & ( eo1 != o5 & ( eo1 != o6 & eo1 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_eo2 , axiom , eo2 != eo1 & ( eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & ( eo2 != o5 & ( eo2 != o6 & eo2 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_eo3 , axiom , eo3 != eo1 & ( eo3 != eo2 & ( eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & ( eo3 != o5 & ( eo3 != o6 & eo3 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o1 , axiom , o1 != eo1 & ( o1 != eo2 & ( o1 != eo3 & ( o1 != o2 & ( o1 != o3 & ( o1 != o4 & ( o1 != o5 & ( o1 != o6 & o1 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o2 , axiom , o2 != eo1 & ( o2 != eo2 & ( o2 != eo3 & ( o2 != o1 & ( o2 != o3 & ( o2 != o4 & ( o2 != o5 & ( o2 != o6 & o2 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o3 , axiom , o3 != eo1 & ( o3 != eo2 & ( o3 != eo3 & ( o3 != o1 & ( o3 != o2 & ( o3 != o4 & ( o3 != o5 & ( o3 != o6 & o3 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o4 , axiom , o4 != eo1 & ( o4 != eo2 & ( o4 != eo3 & ( o4 != o1 & ( o4 != o2 & ( o4 != o3 & ( o4 != o5 & ( o4 != o6 & o4 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o5 , axiom , o5 != eo1 & ( o5 != eo2 & ( o5 != eo3 & ( o5 != o1 & ( o5 != o2 & ( o5 != o3 & ( o5 != o4 & ( o5 != o6 & o5 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o6 , axiom , o6 != eo1 & ( o6 != eo2 & ( o6 != eo3 & ( o6 != o1 & ( o6 != o2 & ( o6 != o3 & ( o6 != o4 & ( o6 != o5 & o6 != o7 ) ) ) ) ) ) ) ) . -fof ( t_uniqueness_o7 , axiom , o7 != eo1 & ( o7 != eo2 & ( o7 != eo3 & ( o7 != o1 & ( o7 != o2 & ( o7 != o3 & ( o7 != o4 & ( o7 != o5 & o7 != o6 ) ) ) ) ) ) ) ) . +fof ( typeScope_max_t_Function , axiom , ! [ A ] : ( ( t_Function ( A ) & object ( A ) ) => ( A = o4 | ( A = o8 | ( A = o9 | ( A = o10 | A = o11 ) ) ) ) ) ) . +fof ( typeScope_max_t_FunctionalOutput , axiom , ! [ A ] : ( ( t_FunctionalOutput ( A ) & object ( A ) ) => ( A = o5 | ( A = o6 | ( A = o7 | A = o8 ) ) ) ) ) . +fof ( t_uniqueness_eo1 , axiom , eo1 != eo2 & ( eo1 != eo3 & ( eo1 != o1 & ( eo1 != o2 & ( eo1 != o3 & ( eo1 != o4 & ( eo1 != o5 & ( eo1 != o6 & ( eo1 != o7 & ( eo1 != o8 & ( eo1 != o9 & ( eo1 != o10 & ( eo1 != o11 & ( eo1 != o12 & ( eo1 != o13 & ( eo1 != o14 & ( eo1 != o15 & ( eo1 != o16 & ( eo1 != o17 & ( eo1 != o18 & ( eo1 != o19 & ( eo1 != o20 & ( eo1 != o21 & ( eo1 != o22 & ( eo1 != o23 & ( eo1 != o24 & eo1 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_eo2 , axiom , eo2 != eo3 & ( eo2 != o1 & ( eo2 != o2 & ( eo2 != o3 & ( eo2 != o4 & ( eo2 != o5 & ( eo2 != o6 & ( eo2 != o7 & ( eo2 != o8 & ( eo2 != o9 & ( eo2 != o10 & ( eo2 != o11 & ( eo2 != o12 & ( eo2 != o13 & ( eo2 != o14 & ( eo2 != o15 & ( eo2 != o16 & ( eo2 != o17 & ( eo2 != o18 & ( eo2 != o19 & ( eo2 != o20 & ( eo2 != o21 & ( eo2 != o22 & ( eo2 != o23 & ( eo2 != o24 & eo2 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_eo3 , axiom , eo3 != o1 & ( eo3 != o2 & ( eo3 != o3 & ( eo3 != o4 & ( eo3 != o5 & ( eo3 != o6 & ( eo3 != o7 & ( eo3 != o8 & ( eo3 != o9 & ( eo3 != o10 & ( eo3 != o11 & ( eo3 != o12 & ( eo3 != o13 & ( eo3 != o14 & ( eo3 != o15 & ( eo3 != o16 & ( eo3 != o17 & ( eo3 != o18 & ( eo3 != o19 & ( eo3 != o20 & ( eo3 != o21 & ( eo3 != o22 & ( eo3 != o23 & ( eo3 != o24 & eo3 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o1 , axiom , o1 != o2 & ( o1 != o3 & ( o1 != o4 & ( o1 != o5 & ( o1 != o6 & ( o1 != o7 & ( o1 != o8 & ( o1 != o9 & ( o1 != o10 & ( o1 != o11 & ( o1 != o12 & ( o1 != o13 & ( o1 != o14 & ( o1 != o15 & ( o1 != o16 & ( o1 != o17 & ( o1 != o18 & ( o1 != o19 & ( o1 != o20 & ( o1 != o21 & ( o1 != o22 & ( o1 != o23 & ( o1 != o24 & o1 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o2 , axiom , o2 != o3 & ( o2 != o4 & ( o2 != o5 & ( o2 != o6 & ( o2 != o7 & ( o2 != o8 & ( o2 != o9 & ( o2 != o10 & ( o2 != o11 & ( o2 != o12 & ( o2 != o13 & ( o2 != o14 & ( o2 != o15 & ( o2 != o16 & ( o2 != o17 & ( o2 != o18 & ( o2 != o19 & ( o2 != o20 & ( o2 != o21 & ( o2 != o22 & ( o2 != o23 & ( o2 != o24 & o2 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o3 , axiom , o3 != o4 & ( o3 != o5 & ( o3 != o6 & ( o3 != o7 & ( o3 != o8 & ( o3 != o9 & ( o3 != o10 & ( o3 != o11 & ( o3 != o12 & ( o3 != o13 & ( o3 != o14 & ( o3 != o15 & ( o3 != o16 & ( o3 != o17 & ( o3 != o18 & ( o3 != o19 & ( o3 != o20 & ( o3 != o21 & ( o3 != o22 & ( o3 != o23 & ( o3 != o24 & o3 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o4 , axiom , o4 != o5 & ( o4 != o6 & ( o4 != o7 & ( o4 != o8 & ( o4 != o9 & ( o4 != o10 & ( o4 != o11 & ( o4 != o12 & ( o4 != o13 & ( o4 != o14 & ( o4 != o15 & ( o4 != o16 & ( o4 != o17 & ( o4 != o18 & ( o4 != o19 & ( o4 != o20 & ( o4 != o21 & ( o4 != o22 & ( o4 != o23 & ( o4 != o24 & o4 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o5 , axiom , o5 != o6 & ( o5 != o7 & ( o5 != o8 & ( o5 != o9 & ( o5 != o10 & ( o5 != o11 & ( o5 != o12 & ( o5 != o13 & ( o5 != o14 & ( o5 != o15 & ( o5 != o16 & ( o5 != o17 & ( o5 != o18 & ( o5 != o19 & ( o5 != o20 & ( o5 != o21 & ( o5 != o22 & ( o5 != o23 & ( o5 != o24 & o5 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o6 , axiom , o6 != o7 & ( o6 != o8 & ( o6 != o9 & ( o6 != o10 & ( o6 != o11 & ( o6 != o12 & ( o6 != o13 & ( o6 != o14 & ( o6 != o15 & ( o6 != o16 & ( o6 != o17 & ( o6 != o18 & ( o6 != o19 & ( o6 != o20 & ( o6 != o21 & ( o6 != o22 & ( o6 != o23 & ( o6 != o24 & o6 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o7 , axiom , o7 != o8 & ( o7 != o9 & ( o7 != o10 & ( o7 != o11 & ( o7 != o12 & ( o7 != o13 & ( o7 != o14 & ( o7 != o15 & ( o7 != o16 & ( o7 != o17 & ( o7 != o18 & ( o7 != o19 & ( o7 != o20 & ( o7 != o21 & ( o7 != o22 & ( o7 != o23 & ( o7 != o24 & o7 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o8 , axiom , o8 != o9 & ( o8 != o10 & ( o8 != o11 & ( o8 != o12 & ( o8 != o13 & ( o8 != o14 & ( o8 != o15 & ( o8 != o16 & ( o8 != o17 & ( o8 != o18 & ( o8 != o19 & ( o8 != o20 & ( o8 != o21 & ( o8 != o22 & ( o8 != o23 & ( o8 != o24 & o8 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o9 , axiom , o9 != o10 & ( o9 != o11 & ( o9 != o12 & ( o9 != o13 & ( o9 != o14 & ( o9 != o15 & ( o9 != o16 & ( o9 != o17 & ( o9 != o18 & ( o9 != o19 & ( o9 != o20 & ( o9 != o21 & ( o9 != o22 & ( o9 != o23 & ( o9 != o24 & o9 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o10 , axiom , o10 != o11 & ( o10 != o12 & ( o10 != o13 & ( o10 != o14 & ( o10 != o15 & ( o10 != o16 & ( o10 != o17 & ( o10 != o18 & ( o10 != o19 & ( o10 != o20 & ( o10 != o21 & ( o10 != o22 & ( o10 != o23 & ( o10 != o24 & o10 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o11 , axiom , o11 != o12 & ( o11 != o13 & ( o11 != o14 & ( o11 != o15 & ( o11 != o16 & ( o11 != o17 & ( o11 != o18 & ( o11 != o19 & ( o11 != o20 & ( o11 != o21 & ( o11 != o22 & ( o11 != o23 & ( o11 != o24 & o11 != o25 ) ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o12 , axiom , o12 != o13 & ( o12 != o14 & ( o12 != o15 & ( o12 != o16 & ( o12 != o17 & ( o12 != o18 & ( o12 != o19 & ( o12 != o20 & ( o12 != o21 & ( o12 != o22 & ( o12 != o23 & ( o12 != o24 & o12 != o25 ) ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o13 , axiom , o13 != o14 & ( o13 != o15 & ( o13 != o16 & ( o13 != o17 & ( o13 != o18 & ( o13 != o19 & ( o13 != o20 & ( o13 != o21 & ( o13 != o22 & ( o13 != o23 & ( o13 != o24 & o13 != o25 ) ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o14 , axiom , o14 != o15 & ( o14 != o16 & ( o14 != o17 & ( o14 != o18 & ( o14 != o19 & ( o14 != o20 & ( o14 != o21 & ( o14 != o22 & ( o14 != o23 & ( o14 != o24 & o14 != o25 ) ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o15 , axiom , o15 != o16 & ( o15 != o17 & ( o15 != o18 & ( o15 != o19 & ( o15 != o20 & ( o15 != o21 & ( o15 != o22 & ( o15 != o23 & ( o15 != o24 & o15 != o25 ) ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o16 , axiom , o16 != o17 & ( o16 != o18 & ( o16 != o19 & ( o16 != o20 & ( o16 != o21 & ( o16 != o22 & ( o16 != o23 & ( o16 != o24 & o16 != o25 ) ) ) ) ) ) ) ) . +fof ( t_uniqueness_o17 , axiom , o17 != o18 & ( o17 != o19 & ( o17 != o20 & ( o17 != o21 & ( o17 != o22 & ( o17 != o23 & ( o17 != o24 & o17 != o25 ) ) ) ) ) ) ) . +fof ( t_uniqueness_o18 , axiom , o18 != o19 & ( o18 != o20 & ( o18 != o21 & ( o18 != o22 & ( o18 != o23 & ( o18 != o24 & o18 != o25 ) ) ) ) ) ) . +fof ( t_uniqueness_o19 , axiom , o19 != o20 & ( o19 != o21 & ( o19 != o22 & ( o19 != o23 & ( o19 != o24 & o19 != o25 ) ) ) ) ) . +fof ( t_uniqueness_o20 , axiom , o20 != o21 & ( o20 != o22 & ( o20 != o23 & ( o20 != o24 & o20 != o25 ) ) ) ) . +fof ( t_uniqueness_o21 , axiom , o21 != o22 & ( o21 != o23 & ( o21 != o24 & o21 != o25 ) ) ) . +fof ( t_uniqueness_o22 , axiom , o22 != o23 & ( o22 != o24 & o22 != o25 ) ) . +fof ( t_uniqueness_o23 , axiom , o23 != o24 & o23 != o25 ) . +fof ( t_uniqueness_o24 , axiom , o24 != o25 ) . 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 ) ) ) ) . @@ -38,17 +55,22 @@ fof ( compliance_terminator_FunctionalData , axiom , ! [ V_0 , V_1 ] : ( r_termi 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 ( noDupCont_r_interface_FunctionalElement , axiom , ? [ A , B ] : ( r_interface_FunctionalElement ( A , B ) => ~ ? [ C , B ] : r_interface_FunctionalElement ( C , B ) ) ) . -fof ( noDupCont_r_rootElements_FunctionalArchitectureModel , axiom , ? [ A , B ] : ( r_rootElements_FunctionalArchitectureModel ( A , B ) => ~ ? [ C , B ] : r_rootElements_FunctionalArchitectureModel ( C , B ) ) ) . -fof ( noDupCont_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_Function ( A , B ) => ~ ? [ C , B ] : r_subElements_Function ( C , B ) ) ) . -fof ( noDupCont_r_data_FunctionalInterface , axiom , ? [ A , B ] : ( r_data_FunctionalInterface ( A , B ) => ~ ? [ C , B ] : r_data_FunctionalInterface ( C , B ) ) ) . -fof ( noDupCont_r_outgoingLinks_FunctionalOutput , axiom , ? [ A , B ] : ( r_outgoingLinks_FunctionalOutput ( A , B ) => ~ ? [ C , B ] : r_outgoingLinks_FunctionalOutput ( C , B ) ) ) . -fof ( noDupCont_r_terminator_FunctionalData , axiom , ? [ A , B ] : ( r_terminator_FunctionalData ( A , B ) => ~ ? [ C , B ] : r_terminator_FunctionalData ( C , B ) ) ) . -fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) . +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_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( B , A ) ) ) . fof ( containment_t_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) . -fof ( containment_t_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( 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 ) ) ) . diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 25ba546a..949abe87 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -93,9 +93,11 @@ class GeneralTest { // add configuration things, in config file first it.documentationLevel = DocumentationLevel::FULL it.typeScopes.minNewElements = 4 - it.typeScopes.maxNewElements = 7 + it.typeScopes.maxNewElements = 25 it.typeScopes.minNewElementsByType = typeMapMin it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false ] solution = reasoner.solve(problem, vampireConfig, workspace) diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 834f3f02..7f92eba4 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/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index e0f9f3f3..2df2ba62 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/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index f3dce1b6..0150ef1d 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -109,9 +109,11 @@ public class GeneralTest { final Procedure1 _function_2 = (VampireSolverConfiguration it) -> { it.documentationLevel = DocumentationLevel.FULL; it.typeScopes.minNewElements = 4; - it.typeScopes.maxNewElements = 7; + it.typeScopes.maxNewElements = 25; it.typeScopes.minNewElementsByType = typeMapMin; it.typeScopes.maxNewElementsByType = typeMapMax; + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function_2); solution = reasoner.solve(problem, vampireConfig, workspace); 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 1661d65f..c0481fd8 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/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index c7de92d2..6c84f917 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-70-g09d2