Facilitate #31, close #36

13 files changed, 110 insertions, 39 deletions

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 54fcdc86..5e8819a6 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
@@ -36,31 +36,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 

                 val localInstances = newArrayList

 

+                val consistant = GLOBAL_MAX > GLOBAL_MIN

+

                 // Handling Minimum_General

                 if (GLOBAL_MIN != ABSOLUTE_MIN) {

-                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false)

-                        for (i : trace.uniqueInstances) {

-                                localInstances.add(support.duplicate(i))

+                        // *

+                        getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant)

+                        if (consistant) {

+                                for (i : trace.uniqueInstances) {

+                                        localInstances.add(support.duplicate(i))

+                                }

+                                makeFofFormula(localInstances, trace, true, null)

+                        } else {

+                                makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)

                         }

-

-                        makeFofFormula(localInstances, trace, true, null)

-

-//                      //For testing Min>Max scope

-//                      getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true)

-//                      makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null)

-//                      //end for testing

-

                 }

 

                 // Handling Maximum_General

                 if (GLOBAL_MAX != ABSOLUTE_MAX) {

-                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true)

-                        makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

-

-//                      //For testing Min>Max scope

-//                      getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false)

-//                      makeFofFormula(localInstances, trace, false, null)

-//                      //end for testing

+                        getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant)

+                        if (consistant) {

+                                makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null)

+                        } else {

+                                makeFofFormula(localInstances, trace, false, null)

+                        }

                 }

 

                 // Handling Minimum_Specific

@@ -94,14 +93,30 @@ class Logic2VampireLanguageMapper_ScopeMapper {
                 }

 

 // 3. Specify uniqueness of elements

-                if (trace.uniqueInstances.length != 0) {

+                val numInst = trace.uniqueInstances.length

+                var ind = 1

+                if (numInst != 0) {

+                        /*

+                         * // SHORTER

+                         * for (e : trace.uniqueInstances.subList(0, numInst-1)) {

+                         /*/

+                        // LONGER

                         for (e : trace.uniqueInstances) {

+                                // */

+                                val x = ind

                                 val uniqueness = createVLSFofFormula => [

                                         it.name = support.toIDMultiple("t_uniqueness", e.name)

                                         it.fofRole = "axiom"

+                                        /*

+                                         * // SHORTER

+                                         * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e)

+                                         /*/

+                                        // LONGER

                                         it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e)

+                                // */

                                 ]

                                 trace.specification.formulas += uniqueness

+                                ind++

                         }

                 }

         }

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 b00dad42..dd88a53a 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
@@ -109,6 +109,8 @@ class Logic2VampireLanguageMapper_Support {
 
 // TODO Make more general
         def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) {
+                
+//              OLD
 //              val List<VLSInequality> eqs = newArrayList
 //              for (t1 : terms.subList(1, terms.length)) {
 //                      for (t2 : terms.subList(0, terms.indexOf(t1))) {
@@ -122,6 +124,8 @@ class Logic2VampireLanguageMapper_Support {
 //                      }
 //              }
 //              return unfoldAnd(eqs)
+//              END OLD
+
                 val List<VLSInequality> eqs = newArrayList
                 for (t1 : terms) {
                         if (t1 != t2) {
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 6c46d2e3..2cc60591 100644
--- 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
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 e5600049..1108945f 100644
--- 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
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 f9813a92..a473c586 100644
--- 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
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 d40b0dd2..24b46e3e 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
@@ -52,16 +52,25 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
     final int GLOBAL_MIN = config.typeScopes.minNewElements;

     final int GLOBAL_MAX = config.typeScopes.maxNewElements;

     final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();

+    final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);

     if ((GLOBAL_MIN != ABSOLUTE_MIN)) {

-      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false);

-      for (final VLSConstant i : trace.uniqueInstances) {

-        localInstances.add(this.support.duplicate(i));

+      this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));

+      if (consistant) {

+        for (final VLSConstant i : trace.uniqueInstances) {

+          localInstances.add(this.support.duplicate(i));

+        }

+        this.makeFofFormula(localInstances, trace, true, null);

+      } else {

+        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null);

       }

-      this.makeFofFormula(localInstances, trace, true, null);

     }

     if ((GLOBAL_MAX != ABSOLUTE_MAX)) {

-      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true);

-      this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

+      this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);

+      if (consistant) {

+        this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);

+      } else {

+        this.makeFofFormula(localInstances, trace, false, null);

+      }

     }

     int i_1 = 1;

     int minNum = (-1);

@@ -95,11 +104,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
         }

       }

     }

-    int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

-    boolean _notEquals = (_length != 0);

-    if (_notEquals) {

+    final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;

+    int ind = 1;

+    if ((numInst != 0)) {

       for (final VLSConstant e : trace.uniqueInstances) {

         {

+          final int x = ind;

           VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();

           final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {

             it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));

@@ -109,6 +119,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
           final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);

           EList<VLSFofFormula> _formulas = trace.specification.getFormulas();

           _formulas.add(uniqueness);

+          ind++;

         }

       }

     }

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore
index 7d818ce2..20d8648e 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore
@@ -2,3 +2,4 @@
 /xtend-gen/
 /src-gen/
 /output/*
+/*/
\ No newline at end of file
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 098cc640..2f2d9718 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
@@ -5,9 +5,23 @@ fof ( enumScope_FunctionType_Intermediate , axiom , ! [ A ] : ( A = eo2 <=> e_In
 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_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 ( t_uniqueness_eo1 , axiom , eo1 != eo2 & eo1 != eo3 ) .

-fof ( t_uniqueness_eo2 , axiom , eo2 != eo1 & eo2 != eo3 ) .

-fof ( t_uniqueness_eo3 , axiom , eo3 != eo1 & eo3 != eo2 ) .

+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_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 ( 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 ) ) ) ) .

@@ -30,11 +44,11 @@ fof ( noDupCont_r_subElements_Function , axiom , ? [ A , B ] : ( r_subElements_F
 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_FunctionalInterface , axiom , ! [ A ] : ( t_FunctionalInterface ( A ) => ? [ B ] : r_interface_FunctionalElement ( B , A ) ) ) .

+fof ( containment_t_InformationLink , axiom , ! [ A ] : ( t_InformationLink ( A ) => ? [ B ] : r_outgoingLinks_FunctionalOutput ( B , A ) ) ) .

 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_FAMTerminator , axiom , ! [ A ] : ( t_FAMTerminator ( A ) => ? [ B ] : r_terminator_FunctionalData ( 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_FunctionalData , axiom , ! [ A ] : ( t_FunctionalData ( A ) => ? [ B ] : r_data_FunctionalInterface ( B , A ) ) ) .

 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/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index a9314376..ef2e0c2f 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
@@ -19,6 +19,7 @@ class FAMTest {
                 val reg = Resource.Factory.Registry.INSTANCE

                 val map = reg.extensionToFactoryMap

                 map.put("logicproblem", new XMIResourceFactoryImpl)

+                

 

                 println("Input and output workspaces are created")

 

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 5b49543d..25ba546a 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
@@ -48,6 +48,8 @@ class GeneralTest {
                 workspace.writeModel(problem, "Fam.logicproblem")

 

                 println("Problem created")

+                

+                var startTime = System.currentTimeMillis

 

                 var LogicResult solution

                 var LogicReasoner reasoner

@@ -90,10 +92,10 @@ class GeneralTest {
                 val vampireConfig = new VampireSolverConfiguration => [

                         // add configuration things, in config file first

                         it.documentationLevel = DocumentationLevel::FULL

-//                      it.typeScopes.minNewElements = 501

-//                      it.typeScopes.maxNewElements = 500

-//                      it.typeScopes.minNewElementsByType = typeMapMin

-//                      it.typeScopes.maxNewElementsByType = typeMapMax

+                        it.typeScopes.minNewElements = 4

+                        it.typeScopes.maxNewElements = 7

+                        it.typeScopes.minNewElementsByType = typeMapMin

+                        it.typeScopes.maxNewElementsByType = typeMapMax

                 ]

                 solution = reasoner.solve(problem, vampireConfig, workspace)

 

@@ -109,7 +111,17 @@ class GeneralTest {
                  * ]

                  * solution = reasoner.solve(problem, alloyConfig, workspace)

                  //*/

+                 

+                 

+                var totalTimeMin = (System.currentTimeMillis - startTime)/60000

+                var totalTimeSec = ((System.currentTimeMillis - startTime)/1000)% 60

+                 

                 println("Problem solved")

+                println("Time was: " + totalTimeMin + ":" + totalTimeSec)

+                

+                

+                

+                

         }

 

         def static loadMetamodel(EPackage pckg) {

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 0af87258..6c37b8ce 100644
--- 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
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 77c5f740..9bb0bdbd 100644
--- 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
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 af47ba7a..f3dce1b6 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
@@ -69,6 +69,7 @@ public class GeneralTest {
         LogicProblem problem = modelGenerationProblem.getOutput();

         workspace.writeModel(problem, "Fam.logicproblem");

         InputOutput.<String>println("Problem created");

+        long startTime = System.currentTimeMillis();

         LogicResult solution = null;

         LogicReasoner reasoner = null;

         VampireSolver _vampireSolver = new VampireSolver();

@@ -107,10 +108,22 @@ public class GeneralTest {
         VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

         final Procedure1<VampireSolverConfiguration> _function_2 = (VampireSolverConfiguration it) -> {

           it.documentationLevel = DocumentationLevel.FULL;

+          it.typeScopes.minNewElements = 4;

+          it.typeScopes.maxNewElements = 7;

+          it.typeScopes.minNewElementsByType = typeMapMin;

+          it.typeScopes.maxNewElementsByType = typeMapMax;

         };

         final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function_2);

         solution = reasoner.solve(problem, vampireConfig, workspace);

-        _xblockexpression = InputOutput.<String>println("Problem solved");

+        long _currentTimeMillis = System.currentTimeMillis();

+        long _minus = (_currentTimeMillis - startTime);

+        long totalTimeMin = (_minus / 60000);

+        long _currentTimeMillis_1 = System.currentTimeMillis();

+        long _minus_1 = (_currentTimeMillis_1 - startTime);

+        long _divide = (_minus_1 / 1000);

+        long totalTimeSec = (_divide % 60);

+        InputOutput.<String>println("Problem solved");

+        _xblockexpression = InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));

       }

       return _xblockexpression;

     } catch (Throwable _e) {