VAMPIRE: close #22, improve test structure for #39, .vql file trouble

Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml

@@ -3,6 +3,35 @@
     <!-- @generated yakindu_simplified -->
     <package class="hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage" genModel="model/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/>
   </extension>
+  <extension id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns" id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns">
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.entryInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noEntryInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleEntryInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.transition"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.incomingToEntry"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noOutgoingTransitionFromEntry"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.multipleTransitionFromEntry"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.outgoingFromExit"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.outgoingFromFinal"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.noStateInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.StateInRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoOutgoing"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.choiceHasNoIncoming"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchHasNoOutgoing"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchHasNoIncoming"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedIncomingInSameRegion"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.notSynchronizingStates"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleOutgoingTrainsition"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleIncomingTrainsition"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedRegionsAreNotSiblings"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.child"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.SynchronizedRegionDoesNotHaveMultipleRegions"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.hasMultipleRegions"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.synchThree"/>
+      <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.twoSynch"/>
+    </group>
+  </extension>
   <extension id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated" point="org.eclipse.viatra.query.runtime.queryspecification">
     <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated" id="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated">
       <query-specification fqn="hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.entryInRegion_M0"/>

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend

@@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 		for (l : relationsList) {
 			var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type
 			containmentListCopy.remove(pointingTo)
-			for (c : pointingTo.subtypes) {
+			var List<Type> allSubtypes = newArrayList
+			support.listSubtypes(pointingTo, allSubtypes)
+			for (c : allSubtypes) {
+				containmentListCopy.remove(c)
+			}
+		}
+
+		for (c : containmentListCopy) {
+			if(c.isIsAbstract) {
 				containmentListCopy.remove(c)
 			}
 		}
@@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
 // STEP 2 CONT'D
 		for (e : type2cont.entrySet) {
 			val relFormula = createVLSFofFormula => [
-				it.name = support.toIDMultiple("containment", e.key.constant.toString)
+				it.name = support.toIDMultiple("containment_contained", e.key.constant.toString)
 				it.fofRole = "axiom"
 
 				it.fofFormula = createVLSUniversalQuantifier => [

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend

@@ -44,17 +44,28 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
 		}
 
+		//deciding name of relation
+		val nameArray = r.name.split(" ")
+		var relNameVar = ""
+		if (nameArray.length == 3) {
+			relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+		}
+		else {
+			relNameVar = r.name
+		}
+		val relName = relNameVar
+
 		val comply = createVLSFofFormula=> [
-			val nameArray = r.name.split(" ")
-			it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2))
+
+			it.name = support.toIDMultiple("compliance", relName)
 			it.fofRole = "axiom"
 			it.fofFormula = createVLSUniversalQuantifier => [
 				for (v : relVar2VLS) {
 					it.variables += support.duplicate(v)
 				}
 				it.operand = createVLSImplies => [
 					val rel = createVLSFunction => [
-						it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2))
+						it.constant = support.toIDMultiple("r", relName)
 						for (v : relVar2VLS) {
 							it.terms += support.duplicate(v)
 						}
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
 	def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) {
 
-		// 1. store all variables in support wrt their name
-		// 1.1 if variable has type, creating list of type declarations
-//		val VLSVariable variable = createVLSVariable => [it.name = "A"]
-		val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
-		val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
-		val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
-		val typedefs = new ArrayList<VLSTerm>
-
-		for (variable : reldef.variables) {
-			val v = createVLSVariable => [
-				it.name = support.toIDMultiple("V", variable.name)
-			]
-			relationVar2VLS.put(variable, v)
-
-			val varTypeComply = createVLSFunction => [
-				it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
-				it.terms += support.duplicate(v)
-			]
-			relationVar2TypeDecComply.put(variable, varTypeComply)
-			relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
-		}
-		val nameArray = reldef.name.split(" ")
-		val comply = createVLSFofFormula => [
-			it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
-				nameArray.get(nameArray.length - 1))
-			it.fofRole = "axiom"
-			it.fofFormula = createVLSUniversalQuantifier => [
-				for (variable : reldef.variables) {
-					it.variables += support.duplicate(variable.lookup(relationVar2VLS))
-
-				}
-				it.operand = createVLSImplies => [
-					it.left = createVLSFunction => [
-						it.constant = support.toIDMultiple("rel", reldef.name)
-						for (variable : reldef.variables) {
-							val v = createVLSVariable => [
-								it.name = variable.lookup(relationVar2VLS).name
-							]
-							it.terms += v
-						}
-					]
-					it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
-				]
-			]
-		]
-
-		val res = createVLSFofFormula => [
-			it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
-				nameArray.get(nameArray.length - 1))
-			it.fofRole = "axiom"
-			it.fofFormula = createVLSUniversalQuantifier => [
-				for (variable : reldef.variables) {
-					val v = createVLSVariable => [
-						it.name = variable.lookup(relationVar2VLS).name
-					]
-					it.variables += v
-
-				}
-				it.operand = createVLSImplies => [
-					it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
-					it.right = createVLSEquivalent => [
-						it.left = createVLSFunction => [
-							it.constant = support.toIDMultiple("rel", reldef.name)
-							for (variable : reldef.variables) {
-								val v = createVLSVariable => [
-									it.name = variable.lookup(relationVar2VLS).name
-								]
-								it.terms += v
-
-							}
-						]
-						it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
-					]
-
-				]
-
-			]
-
-		]
-
-		// trace.relationDefinition2Predicate.put(r,res)
-		trace.specification.formulas += comply;
-		trace.specification.formulas += res;
+//		// 1. store all variables in support wrt their name
+//		// 1.1 if variable has type, creating list of type declarations
+////		val VLSVariable variable = createVLSVariable => [it.name = "A"]
+//		val Map<Variable, VLSVariable> relationVar2VLS = new HashMap
+//		val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap
+//		val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap
+//		val typedefs = new ArrayList<VLSTerm>
+//
+//		for (variable : reldef.variables) {
+//			val v = createVLSVariable => [
+//				it.name = support.toIDMultiple("V", variable.name)
+//			]
+//			relationVar2VLS.put(variable, v)
+//
+//			val varTypeComply = createVLSFunction => [
+//				it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name)
+//				it.terms += support.duplicate(v)
+//			]
+//			relationVar2TypeDecComply.put(variable, varTypeComply)
+//			relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply))
+//		}
+//		val nameArray = reldef.name.split(" ")
+//		val comply = createVLSFofFormula => [
+//			it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2),
+//				nameArray.get(nameArray.length - 1))
+//			it.fofRole = "axiom"
+//			it.fofFormula = createVLSUniversalQuantifier => [
+//				for (variable : reldef.variables) {
+//					it.variables += support.duplicate(variable.lookup(relationVar2VLS))
+//
+//				}
+//				it.operand = createVLSImplies => [
+//					it.left = createVLSFunction => [
+//						it.constant = support.toIDMultiple("rel", reldef.name)
+//						for (variable : reldef.variables) {
+//							val v = createVLSVariable => [
+//								it.name = variable.lookup(relationVar2VLS).name
+//							]
+//							it.terms += v
+//						}
+//					]
+//					it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values))
+//				]
+//			]
+//		]
+//
+//		val res = createVLSFofFormula => [
+//			it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2),
+//				nameArray.get(nameArray.length - 1))
+//			it.fofRole = "axiom"
+//			it.fofFormula = createVLSUniversalQuantifier => [
+//				for (variable : reldef.variables) {
+//					val v = createVLSVariable => [
+//						it.name = variable.lookup(relationVar2VLS).name
+//					]
+//					it.variables += v
+//
+//				}
+//				it.operand = createVLSImplies => [
+//					it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values))
+//					it.right = createVLSEquivalent => [
+//						it.left = createVLSFunction => [
+//							it.constant = support.toIDMultiple("rel", reldef.name)
+//							for (variable : reldef.variables) {
+//								val v = createVLSVariable => [
+//									it.name = variable.lookup(relationVar2VLS).name
+//								]
+//								it.terms += v
+//
+//							}
+//						]
+//						it.right = base.transformTerm(reldef.value, trace, relationVar2VLS)
+//					]
+//
+//				]
+//
+//			]
+//
+//		]
+//
+//		// trace.relationDefinition2Predicate.put(r,res)
+//		trace.specification.formulas += comply;
+//		trace.specification.formulas += res;
 
 	}
 

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend

@@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
 //		TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
 //		TODO HANDLE 
 		// 1. make a list of constants equaling the min number of specified objects
+		//These numbers do not include enums or initial model elements
 		val GLOBAL_MIN = config.typeScopes.minNewElements
 		val GLOBAL_MAX = config.typeScopes.maxNewElements
 

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend

@@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support {
 		}
 	}
 
-	def protected List<Type> listSubtypes(Type t) {
-		var List<Type> allSubtypes = newArrayList
-		if (!t.subtypes.isEmpty) {
-			for (subt : t.subtypes) {
-				allSubtypes.add(subt)
-				allSubtypes = listSubtypes(subt)
-			}
+	def protected void listSubtypes(Type t, List<Type> allSubtypes) {
+		for (subt : t.subtypes) {
+			allSubtypes.add(subt)
+			listSubtypes(subt, allSubtypes)
 		}
-		return allSubtypes
 	}
 
 	def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) {

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend

@@ -44,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
 			// Create a VLSFunction for each Enum Element
 			val List<VLSFunction> orElems = newArrayList
+
 			for (e : type.elements) {
+				val nameArray = e.name.split(" ")
+				var relNameVar = ""
+				if (nameArray.length == 3) {
+					relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+				} else {
+					relNameVar = e.name
+				}
+				val relName = relNameVar
+
 				val enumElemPred = createVLSFunction => [
-					val splitName = e.name.split(" ")
-					if (splitName.length > 2) {
-						it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2))
-					} else {
-						it.constant = support.toIDMultiple("e", splitName.get(0))
-					}
+					it.constant = support.toIDMultiple("e", relName)
 					it.terms += support.duplicate(variable)
 				]
 				trace.element2Predicate.put(e, enumElemPred)
@@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper {
 
 			// Implement Enum Inheritence Hierarchy
 			val res = createVLSFofFormula => [
-				it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
+				it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString)
 				it.fofRole = "axiom"
 				it.fofFormula = createVLSUniversalQuantifier => [
 					it.variables += support.duplicate(variable)
@@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper {
 				val cst = support.toConstant(cstTerm)
 				trace.uniqueInstances.add(cst)
 
-				val index = i
+				val index = i-globalCounter
 				val enumScope = createVLSFofFormula => [
-					it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0),
+					it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString,
 						type.elements.get(index).name.split(" ").get(0))
 					it.fofRole = "axiom"
 					it.fofFormula = createVLSUniversalQuantifier => [

Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java

@@ -64,12 +64,19 @@ public void transformContainment(final VampireSolverConfiguration config, final
         Type _referred = ((ComplexTypeReference) _get).getReferred();
         Type pointingTo = ((Type) _referred);
         containmentListCopy.remove(pointingTo);
-        EList<Type> _subtypes = pointingTo.getSubtypes();
-        for (final Type c : _subtypes) {
+        List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList();
+        this.support.listSubtypes(pointingTo, allSubtypes);
+        for (final Type c : allSubtypes) {
           containmentListCopy.remove(c);
         }
       }
     }
+    for (final Type c : containmentListCopy) {
+      boolean _isIsAbstract = c.isIsAbstract();
+      if (_isIsAbstract) {
+        containmentListCopy.remove(c);
+      }
+    }
     final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString();
     final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate));
     VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
@@ -132,7 +139,7 @@ public void transformContainment(final VampireSolverConfiguration config, final
         final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);
         this.addToMap(type2cont, toFunc, rel);
         EList<Type> _subtypes = toType.getSubtypes();
-        for (final Type c : _subtypes) {
+        for (final Type c_1 : _subtypes) {
           this.addToMap(type2cont, toFunc, rel);
         }
         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
@@ -184,7 +191,7 @@ public void transformContainment(final VampireSolverConfiguration config, final
       {
         VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
         final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
-          it.setName(this.support.toIDMultiple("containment", e.getKey().getConstant().toString()));
+          it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));
           it.setFofRole("axiom");
           VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
           final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {