Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
1 files changed, 167 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql
new file mode 100644
index 00000000..5b38189f
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql
@@ -0,0 +1,167 @@
+package hu.bme.mit.inf.dslreasoner.logic.model.patterns
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
+import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
+/// Basic util patterns ///
+/**
+ * Direct supertypes of a type.
+ */
+private pattern supertypeDirect(subtype : Type, supertype : Type) {
+        Type.supertypes(subtype, supertype);
+}
+/**
+ * All supertypes of a type.
+ */
+pattern supertypeStar(subtype: Type, supertype: Type) {
+        subtype == supertype;
+} or {
+        find supertypeDirect+(subtype,supertype);
+}
+/**
+ * Direct element of a type
+ */
+pattern typeDirectElements(type: TypeDefinition, element: DefinedElement) {
+        TypeDefinition.elements(type,element);
+}
+/// Complex type reasoning patterns ///
+//
+// In a valid type system, for each element e there is exactly one type T where
+// 1: T(e) - but we dont know this for type declaration
+// 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true.
+// 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e:
+//     D(e) && D-->T && !T(e)
+// 3: There is no T' that T'->T and T'(e)
+// 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T:
+//    D(e) && ![T--->D] && T(e)
+// 4: T is not abstract
+// Such type T is called Dynamic type of e, while other types are called static types.
+// 
+// The following patterns checks the possible dynamic types for an element
+pattern possibleDynamicType(problem: LogicProblem, dynamic:Type, element:DefinedElement)
+// case 1: element is defined in at least once
+{
+        LogicProblem.types(problem,dynamic);
+        // select a random definition
+        find typeDirectElements(definition,element);
+        // 2e is not true: D(e) && D-->T && !T(e)
+        find supertypeStar(dynamic,definition);
+        neg find dynamicTypeNotSubtypeOfADefinition(problem,element,dynamic);
+        // 3e is not true: D(e) && ![T--->D] && T(e)
+        neg find dynamicTypeIsSubtypeOfANonDefinition(problem,element,dynamic);
+        // 4: T is not abstract
+        Type.isAbstract(dynamic,false);
+}       or
+// case 2: element is defined is not defined
+{
+        LogicProblem.types(problem,dynamic);
+        // there is no definition
+        neg find typeDirectElements(_,element);
+        // 2e is not true: D(e) && D-->T && !T(e)
+        // because non of the definition contains element, the type cannot have defined supertype
+        neg find typesWithDefinedSupertype(problem,dynamic);
+        // 3e is not true: D(e) && ![T--->D] && T(e)
+        // because there is no definition, dynamic covers all definition
+}
+/**
+ * supertype -------> element <------- otherSupertype
+ *     A                                     A
+ *     |                                     |
+ * wrongDynamic -----------------------------X
+ */
+private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, element:DefinedElement, wrongDynamic : Type) {
+        LogicProblem.types(problem,wrongDynamic);
+        find typeDirectElements(supertype,element);
+        find supertypeStar(wrongDynamic,supertype);
+        find typeDirectElements(otherSupertype,element);
+        neg find supertypeStar(wrongDynamic,otherSupertype);
+        //otherSupertype != wrongDynamic;
+}
+/**
+ * supertype -------> element <---X--- otherSupertype
+ *     A                                     A
+ *     |                                     |
+ * wrongDynamic -----------------------------+
+ */
+private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, element:DefinedElement, wrongDynamic:Type) {
+        LogicProblem.types(problem,wrongDynamic);
+        find typeDirectElements(supertype, element);
+        find supertypeStar(wrongDynamic, supertype);
+        find supertypeStar(wrongDynamic, otherSupertype);
+        TypeDefinition(otherSupertype);
+        neg find typeDirectElements(otherSupertype, element);
+}
+private pattern typesWithDefinedSupertype(problem: LogicProblem, type:TypeDeclaration) {
+        LogicProblem.types(problem,type);
+        find supertypeStar(type,definedSupertype);
+        TypeDefinition(definedSupertype);
+}
+/**
+ * Types that 
+ */
+pattern mustTypeElement(problem: LogicProblem, type:Type, element:DefinedElement) {
+        LogicProblem.types(problem,type);
+        TypeDefinition.elements(type,element);
+} or {
+        TypeDeclaration(type);
+        LogicProblem.types(problem,type);
+        LogicProblem.types(problem,subtype);
+        TypeDefinition.elements(subtype,element);
+        find supertypeStar(subtype,type);
+}
+/// Validation patterns ///
+@Constraint(severity = "warning",key = {problem},
+        message="Type system is inconsistent."
+)
+pattern typeSystemIsInconsistent(problem:LogicProblem) {
+        find elementWithNoPossibleDynamicType(problem,_);
+} or {
+        find elementNotDefinedInSupertype(problem,_,_,_);
+}
+/**
+ * An element is defined in a type, but not defined in a supertype
+ */
+@Constraint(severity = "warning",key = {element},
+        message="An element is defined in a type, but not defined in a supertype."
+)
+pattern elementNotDefinedInSupertype(problem: LogicProblem,
+        element: DefinedElement,
+        directType:TypeDefinition,
+        notDefinedIn: TypeDefinition)
+{
+        LogicProblem.elements(problem,element);
+        find typeDirectElements(directType,element);
+        find supertypeStar(directType,notDefinedIn);
+        neg find typeDirectElements(notDefinedIn,element);
+}
+@Constraint(severity = "warning",key = {element},
+        message="There is no possible dynamic type for an element."
+)
+pattern elementWithNoPossibleDynamicType(problem:LogicProblem, element:DefinedElement) {
+        LogicProblem.elements(problem,element);
+        neg find possibleDynamicType(problem,_,element);
+}
+@Constraint(severity = "error",key = {t},
+        message="Circle in the type hierarchy"
+)
+pattern cyclicTypeHierarchy(t: Type) {
+        find supertypeDirect+(t,t);
+}
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql new file mode 100644 index 00000000..5b38189f --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql
@@ -0,0 +1,167 @@
	1	package hu.bme.mit.inf.dslreasoner.logic.model.patterns
	2
	3	import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
	4	import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
	5
	6	/// Basic util patterns ///
	7
	8	/**
	9	* Direct supertypes of a type.
	10	*/
	11	private pattern supertypeDirect(subtype : Type, supertype : Type) {
	12	Type.supertypes(subtype, supertype);
	13	}
	14
	15	/**
	16	* All supertypes of a type.
	17	*/
	18	pattern supertypeStar(subtype: Type, supertype: Type) {
	19	subtype == supertype;
	20	} or {
	21	find supertypeDirect+(subtype,supertype);
	22	}
	23
	24	/**
	25	* Direct element of a type
	26	*/
	27	pattern typeDirectElements(type: TypeDefinition, element: DefinedElement) {
	28	TypeDefinition.elements(type,element);
	29	}
	30
	31	/// Complex type reasoning patterns ///
	32	//
	33	// In a valid type system, for each element e there is exactly one type T where
	34	// 1: T(e) - but we dont know this for type declaration
	35	// 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true.
	36	// 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e:
	37	// D(e) && D-->T && !T(e)
	38	// 3: There is no T' that T'->T and T'(e)
	39	// 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T:
	40	// D(e) && ![T--->D] && T(e)
	41	// 4: T is not abstract
	42	// Such type T is called Dynamic type of e, while other types are called static types.
	43	//
	44	// The following patterns checks the possible dynamic types for an element
	45
	46	pattern possibleDynamicType(problem: LogicProblem, dynamic:Type, element:DefinedElement)
	47	// case 1: element is defined in at least once
	48	{
	49	LogicProblem.types(problem,dynamic);
	50	// select a random definition
	51	find typeDirectElements(definition,element);
	52	// 2e is not true: D(e) && D-->T && !T(e)
	53	find supertypeStar(dynamic,definition);
	54	neg find dynamicTypeNotSubtypeOfADefinition(problem,element,dynamic);
	55	// 3e is not true: D(e) && ![T--->D] && T(e)
	56	neg find dynamicTypeIsSubtypeOfANonDefinition(problem,element,dynamic);
	57	// 4: T is not abstract
	58	Type.isAbstract(dynamic,false);
	59	} or
	60	// case 2: element is defined is not defined
	61	{
	62	LogicProblem.types(problem,dynamic);
	63	// there is no definition
	64	neg find typeDirectElements(_,element);
	65	// 2e is not true: D(e) && D-->T && !T(e)
	66	// because non of the definition contains element, the type cannot have defined supertype
	67	neg find typesWithDefinedSupertype(problem,dynamic);
	68	// 3e is not true: D(e) && ![T--->D] && T(e)
	69	// because there is no definition, dynamic covers all definition
	70	}
	71
	72	/**
	73	* supertype -------> element <------- otherSupertype
	74	* A A
	75	* \| \|
	76	* wrongDynamic -----------------------------X
	77	*/
	78	private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, element:DefinedElement, wrongDynamic : Type) {
	79	LogicProblem.types(problem,wrongDynamic);
	80	find typeDirectElements(supertype,element);
	81	find supertypeStar(wrongDynamic,supertype);
	82	find typeDirectElements(otherSupertype,element);
	83	neg find supertypeStar(wrongDynamic,otherSupertype);
	84	//otherSupertype != wrongDynamic;
	85	}
	86
	87
	88	/**
	89	* supertype -------> element <---X--- otherSupertype
	90	* A A
	91	* \| \|
	92	* wrongDynamic -----------------------------+
	93	*/
	94	private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, element:DefinedElement, wrongDynamic:Type) {
	95	LogicProblem.types(problem,wrongDynamic);
	96	find typeDirectElements(supertype, element);
	97	find supertypeStar(wrongDynamic, supertype);
	98	find supertypeStar(wrongDynamic, otherSupertype);
	99	TypeDefinition(otherSupertype);
	100	neg find typeDirectElements(otherSupertype, element);
	101	}
	102
	103	private pattern typesWithDefinedSupertype(problem: LogicProblem, type:TypeDeclaration) {
	104	LogicProblem.types(problem,type);
	105	find supertypeStar(type,definedSupertype);
	106	TypeDefinition(definedSupertype);
	107	}
	108
	109	/**
	110	* Types that
	111	*/
	112	pattern mustTypeElement(problem: LogicProblem, type:Type, element:DefinedElement) {
	113	LogicProblem.types(problem,type);
	114	TypeDefinition.elements(type,element);
	115	} or {
	116	TypeDeclaration(type);
	117	LogicProblem.types(problem,type);
	118	LogicProblem.types(problem,subtype);
	119	TypeDefinition.elements(subtype,element);
	120	find supertypeStar(subtype,type);
	121	}
	122
	123
	124	/// Validation patterns ///
	125
	126	@Constraint(severity = "warning",key = {problem},
	127	message="Type system is inconsistent."
	128	)
	129	pattern typeSystemIsInconsistent(problem:LogicProblem) {
	130	find elementWithNoPossibleDynamicType(problem,_);
	131	} or {
	132	find elementNotDefinedInSupertype(problem,_,_,_);
	133	}
	134
	135	/**
	136	* An element is defined in a type, but not defined in a supertype
	137	*/
	138	@Constraint(severity = "warning",key = {element},
	139	message="An element is defined in a type, but not defined in a supertype."
	140	)
	141	pattern elementNotDefinedInSupertype(problem: LogicProblem,
	142	element: DefinedElement,
	143	directType:TypeDefinition,
	144	notDefinedIn: TypeDefinition)
	145	{
	146	LogicProblem.elements(problem,element);
	147	find typeDirectElements(directType,element);
	148	find supertypeStar(directType,notDefinedIn);
	149	neg find typeDirectElements(notDefinedIn,element);
	150	}
	151
	152	@Constraint(severity = "warning",key = {element},
	153	message="There is no possible dynamic type for an element."
	154	)
	155	pattern elementWithNoPossibleDynamicType(problem:LogicProblem, element:DefinedElement) {
	156	LogicProblem.elements(problem,element);
	157	neg find possibleDynamicType(problem,_,element);
	158	}
	159
	160
	161
	162	@Constraint(severity = "error",key = {t},
	163	message="Circle in the type hierarchy"
	164	)
	165	pattern cyclicTypeHierarchy(t: Type) {
	166	find supertypeDirect+(t,t);
	167	}