Facilitate #31, close #36

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++
 			}
 		}
 	}

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) {

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 void _transformScope(final LogicSolverConfiguration config, final Logic2V
     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 void _transformScope(final LogicSolverConfiguration config, final Logic2V
         }
       }
     }
-    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 void _transformScope(final LogicSolverConfiguration config, final Logic2V
           final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
           EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
           _formulas.add(uniqueness);
+          ind++;
         }
       }
     }

Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.gitignore

@@ -2,3 +2,4 @@
 /xtend-gen/
 /src-gen/
 /output/*
+/*/

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 ) ) ) .

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")
 

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) {

Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java

@@ -69,6 +69,7 @@ public static String createAndSolveProblem(final EcoreMetamodelDescriptor metamo
         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 static String createAndSolveProblem(final EcoreMetamodelDescriptor metamo
         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) {