VAMPIRE: Implement Vampire measurement code

13 files changed, 635 insertions, 84 deletions

diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore
index d8331ba8..3fab9a1d 100644
--- a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore
+++ b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore
@@ -9,7 +9,7 @@
     <eStructuralFeatures xsi:type="ecore:EReference" name="interface" eType="#//FunctionalInterface"

         containment="true" eOpposite="#//FunctionalInterface/element"/>

     <eStructuralFeatures xsi:type="ecore:EReference" name="model" lowerBound="1" eType="#//FunctionalArchitectureModel"

-        volatile="true" transient="true" derived="true">

+        volatile="true" transient="true">

       <eAnnotations source="org.eclipse.viatra.query.querybasedfeature">

         <details key="patternFQN" value="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/>

       </eAnnotations>

@@ -25,7 +25,7 @@
     <eStructuralFeatures xsi:type="ecore:EReference" name="subElements" upperBound="-1"

         eType="#//FunctionalElement" containment="true" eOpposite="#//FunctionalElement/parent"/>

     <eStructuralFeatures xsi:type="ecore:EAttribute" name="type" lowerBound="1" eType="#//FunctionType"

-        changeable="false" volatile="true" transient="true" derived="true">

+        volatile="true" transient="true">

       <eAnnotations source="org.eclipse.viatra.query.querybasedfeature">

         <details key="patternFQN" value="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/>

       </eAnnotations>

diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
index d6f22c95..07fd662c 100644
--- a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
+++ b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml
@@ -3,12 +3,6 @@
     <!-- @generated FamMetamodel -->

     <package class="functionalarchitecture.FunctionalarchitecturePackage" genModel="model/FamMetamodel.genmodel" uri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/>

   </extension>

-  <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.model" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features">

-    <wellbehaving-derived-feature classifier-name="FunctionalElement" feature-name="model" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/>

-  </extension>

-  <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.type" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features">

-    <wellbehaving-derived-feature classifier-name="Function" feature-name="type" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/>

-  </extension>

   <extension id="hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification">

     <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns" id="hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns">

       <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/>

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF
index f2fd2ff3..f8973169 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/META-INF/MANIFEST.MF
@@ -15,6 +15,7 @@ Require-Bundle: org.eclipse.viatra.query.runtime,
   org.eclipse.core.runtime,
   org.eclipse.emf.ecore;visibility:=reexport,
   com.google.guava;bundle-version="15.0.0"
-Bundle-RequiredExecutionEnvironment: JavaSE-1.8
-Bundle-ActivationPolicy: lazy
 Import-Package: org.apache.log4j
+Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph
+Bundle-ActivationPolicy: lazy
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/Entry.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/Entry.java
index de8cdb07..994ffd96 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/Entry.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/Entry.java
@@ -8,10 +8,45 @@ package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm;
  * A representation of the model object '<em><b>Entry</b></em>'.

  * <!-- end-user-doc -->

  *

+ * <p>

+ * The following features are supported:

+ * </p>

+ * <ul>

+ *   <li>{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry#getType <em>Type</em>}</li>

+ * </ul>

  *

  * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage#getEntry()

  * @model

  * @generated

  */

 public interface Entry extends Pseudostate {

+

+        /**

+         * Returns the value of the '<em><b>Type</b></em>' attribute.

+         * The literals are from the enumeration {@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType}.

+         * <!-- begin-user-doc -->

+         * <p>

+         * If the meaning of the '<em>Type</em>' attribute isn't clear,

+         * there really should be more of a description here...

+         * </p>

+         * <!-- end-user-doc -->

+         * @return the value of the '<em>Type</em>' attribute.

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType

+         * @see #setType(EntryType)

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage#getEntry_Type()

+         * @model

+         * @generated

+         */

+        EntryType getType();

+

+        /**

+         * Sets the value of the '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry#getType <em>Type</em>}' attribute.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @param value the new value of the '<em>Type</em>' attribute.

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType

+         * @see #getType()

+         * @generated

+         */

+        void setType(EntryType value);

 } // Entry

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/EntryType.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/EntryType.java
new file mode 100644
index 00000000..4f5d1a31
--- /dev/null
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/EntryType.java
@@ -0,0 +1,239 @@
+/**
+ */
+package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm;
+
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+
+import org.eclipse.emf.common.util.Enumerator;
+
+/**
+ * <!-- begin-user-doc -->
+ * A representation of the literals of the enumeration '<em><b>Entry Type</b></em>',
+ * and utility methods for working with them.
+ * <!-- end-user-doc -->
+ * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage#getEntryType()
+ * @model
+ * @generated
+ */
+public enum EntryType implements Enumerator {
+        /**
+         * The '<em><b>Normal</b></em>' literal object.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @see #NORMAL_VALUE
+         * @generated
+         * @ordered
+         */
+        NORMAL(0, "Normal", "Normal"),
+
+        /**
+         * The '<em><b>History</b></em>' literal object.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @see #HISTORY_VALUE
+         * @generated
+         * @ordered
+         */
+        HISTORY(0, "History", "History"),
+
+        /**
+         * The '<em><b>Deep History</b></em>' literal object.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @see #DEEP_HISTORY_VALUE
+         * @generated
+         * @ordered
+         */
+        DEEP_HISTORY(0, "DeepHistory", "DeepHistory");
+
+        /**
+         * The '<em><b>Normal</b></em>' literal value.
+         * <!-- begin-user-doc -->
+         * <p>
+         * If the meaning of '<em><b>Normal</b></em>' literal object isn't clear,
+         * there really should be more of a description here...
+         * </p>
+         * <!-- end-user-doc -->
+         * @see #NORMAL
+         * @model name="Normal"
+         * @generated
+         * @ordered
+         */
+        public static final int NORMAL_VALUE = 0;
+
+        /**
+         * The '<em><b>History</b></em>' literal value.
+         * <!-- begin-user-doc -->
+         * <p>
+         * If the meaning of '<em><b>History</b></em>' literal object isn't clear,
+         * there really should be more of a description here...
+         * </p>
+         * <!-- end-user-doc -->
+         * @see #HISTORY
+         * @model name="History"
+         * @generated
+         * @ordered
+         */
+        public static final int HISTORY_VALUE = 0;
+
+        /**
+         * The '<em><b>Deep History</b></em>' literal value.
+         * <!-- begin-user-doc -->
+         * <p>
+         * If the meaning of '<em><b>Deep History</b></em>' literal object isn't clear,
+         * there really should be more of a description here...
+         * </p>
+         * <!-- end-user-doc -->
+         * @see #DEEP_HISTORY
+         * @model name="DeepHistory"
+         * @generated
+         * @ordered
+         */
+        public static final int DEEP_HISTORY_VALUE = 0;
+
+        /**
+         * An array of all the '<em><b>Entry Type</b></em>' enumerators.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        private static final EntryType[] VALUES_ARRAY =
+                new EntryType[] {
+                        NORMAL,
+                        HISTORY,
+                        DEEP_HISTORY,
+                };
+
+        /**
+         * A public read-only list of all the '<em><b>Entry Type</b></em>' enumerators.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        public static final List<EntryType> VALUES = Collections.unmodifiableList(Arrays.asList(VALUES_ARRAY));
+
+        /**
+         * Returns the '<em><b>Entry Type</b></em>' literal with the specified literal value.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @param literal the literal.
+         * @return the matching enumerator or <code>null</code>.
+         * @generated
+         */
+        public static EntryType get(String literal) {
+                for (int i = 0; i < VALUES_ARRAY.length; ++i) {
+                        EntryType result = VALUES_ARRAY[i];
+                        if (result.toString().equals(literal)) {
+                                return result;
+                        }
+                }
+                return null;
+        }
+
+        /**
+         * Returns the '<em><b>Entry Type</b></em>' literal with the specified name.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @param name the name.
+         * @return the matching enumerator or <code>null</code>.
+         * @generated
+         */
+        public static EntryType getByName(String name) {
+                for (int i = 0; i < VALUES_ARRAY.length; ++i) {
+                        EntryType result = VALUES_ARRAY[i];
+                        if (result.getName().equals(name)) {
+                                return result;
+                        }
+                }
+                return null;
+        }
+
+        /**
+         * Returns the '<em><b>Entry Type</b></em>' literal with the specified integer value.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @param value the integer value.
+         * @return the matching enumerator or <code>null</code>.
+         * @generated
+         */
+        public static EntryType get(int value) {
+                switch (value) {
+                        case NORMAL_VALUE: return NORMAL;
+                }
+                return null;
+        }
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        private final int value;
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        private final String name;
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        private final String literal;
+
+        /**
+         * Only this class can construct instances.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        private EntryType(int value, String name, String literal) {
+                this.value = value;
+                this.name = name;
+                this.literal = literal;
+        }
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        public int getValue() {
+          return value;
+        }
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        public String getName() {
+          return name;
+        }
+
+        /**
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        public String getLiteral() {
+          return literal;
+        }
+
+        /**
+         * Returns the literal value of the enumerator, which is its string representation.
+         * <!-- begin-user-doc -->
+         * <!-- end-user-doc -->
+         * @generated
+         */
+        @Override
+        public String toString() {
+                return literal;
+        }
+        
+} //EntryType
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/YakindummPackage.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/YakindummPackage.java
index 18a4b105..a9269e05 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/YakindummPackage.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/YakindummPackage.java
@@ -2,7 +2,9 @@
  */

 package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm;

 

+import org.eclipse.emf.ecore.EAttribute;

 import org.eclipse.emf.ecore.EClass;

+import org.eclipse.emf.ecore.EEnum;

 import org.eclipse.emf.ecore.EPackage;

 import org.eclipse.emf.ecore.EReference;

 

@@ -333,13 +335,22 @@ public interface YakindummPackage extends EPackage {
         int ENTRY__OUTGOING_TRANSITIONS = PSEUDOSTATE__OUTGOING_TRANSITIONS;

 

         /**

+         * The feature id for the '<em><b>Type</b></em>' attribute.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         * @ordered

+         */

+        int ENTRY__TYPE = PSEUDOSTATE_FEATURE_COUNT + 0;

+

+        /**

          * The number of structural features of the '<em>Entry</em>' class.

          * <!-- begin-user-doc -->

          * <!-- end-user-doc -->

          * @generated

          * @ordered

          */

-        int ENTRY_FEATURE_COUNT = PSEUDOSTATE_FEATURE_COUNT + 0;

+        int ENTRY_FEATURE_COUNT = PSEUDOSTATE_FEATURE_COUNT + 1;

 

         /**

          * The number of operations of the '<em>Entry</em>' class.

@@ -639,6 +650,17 @@ public interface YakindummPackage extends EPackage {
 

 

         /**

+         * The meta object id for the '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType <em>Entry Type</em>}' enum.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl.YakindummPackageImpl#getEntryType()

+         * @generated

+         */

+        int ENTRY_TYPE = 13;

+

+

+        /**

          * Returns the meta object for class '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Pseudostate <em>Pseudostate</em>}'.

          * <!-- begin-user-doc -->

          * <!-- end-user-doc -->

@@ -754,6 +776,17 @@ public interface YakindummPackage extends EPackage {
         EClass getEntry();

 

         /**

+         * Returns the meta object for the attribute '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry#getType <em>Type</em>}'.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @return the meta object for the attribute '<em>Type</em>'.

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry#getType()

+         * @see #getEntry()

+         * @generated

+         */

+        EAttribute getEntry_Type();

+

+        /**

          * Returns the meta object for class '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Synchronization <em>Synchronization</em>}'.

          * <!-- begin-user-doc -->

          * <!-- end-user-doc -->

@@ -835,6 +868,16 @@ public interface YakindummPackage extends EPackage {
         EClass getFinalState();

 

         /**

+         * Returns the meta object for enum '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType <em>Entry Type</em>}'.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @return the meta object for enum '<em>Entry Type</em>'.

+         * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType

+         * @generated

+         */

+        EEnum getEntryType();

+

+        /**

          * Returns the factory that creates the instances of the model.

          * <!-- begin-user-doc -->

          * <!-- end-user-doc -->

@@ -958,6 +1001,14 @@ public interface YakindummPackage extends EPackage {
                 EClass ENTRY = eINSTANCE.getEntry();

 

                 /**

+                 * The meta object literal for the '<em><b>Type</b></em>' attribute feature.

+                 * <!-- begin-user-doc -->

+                 * <!-- end-user-doc -->

+                 * @generated

+                 */

+                EAttribute ENTRY__TYPE = eINSTANCE.getEntry_Type();

+

+                /**

                  * The meta object literal for the '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl.SynchronizationImpl <em>Synchronization</em>}' class.

                  * <!-- begin-user-doc -->

                  * <!-- end-user-doc -->

@@ -1035,6 +1086,16 @@ public interface YakindummPackage extends EPackage {
                  */

                 EClass FINAL_STATE = eINSTANCE.getFinalState();

 

+                /**

+                 * The meta object literal for the '{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType <em>Entry Type</em>}' enum.

+                 * <!-- begin-user-doc -->

+                 * <!-- end-user-doc -->

+                 * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType

+                 * @see hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl.YakindummPackageImpl#getEntryType()

+                 * @generated

+                 */

+                EEnum ENTRY_TYPE = eINSTANCE.getEntryType();

+

         }

 

 } //YakindummPackage

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/EntryImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/EntryImpl.java
index 35003e0d..27041630 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/EntryImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/EntryImpl.java
@@ -3,19 +3,47 @@
 package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl;

 

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry;

+import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage;

 

+import org.eclipse.emf.common.notify.Notification;

 import org.eclipse.emf.ecore.EClass;

+import org.eclipse.emf.ecore.impl.ENotificationImpl;

 

 /**

  * <!-- begin-user-doc -->

  * An implementation of the model object '<em><b>Entry</b></em>'.

  * <!-- end-user-doc -->

+ * <p>

+ * The following features are implemented:

+ * </p>

+ * <ul>

+ *   <li>{@link hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl.EntryImpl#getType <em>Type</em>}</li>

+ * </ul>

  *

  * @generated

  */

 public class EntryImpl extends PseudostateImpl implements Entry {

         /**

+         * The default value of the '{@link #getType() <em>Type</em>}' attribute.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @see #getType()

+         * @generated

+         * @ordered

+         */

+        protected static final EntryType TYPE_EDEFAULT = EntryType.NORMAL;

+        /**

+         * The cached value of the '{@link #getType() <em>Type</em>}' attribute.

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @see #getType()

+         * @generated

+         * @ordered

+         */

+        protected EntryType type = TYPE_EDEFAULT;

+

+        /**

          * <!-- begin-user-doc -->

          * <!-- end-user-doc -->

          * @generated

@@ -34,4 +62,99 @@ public class EntryImpl extends PseudostateImpl implements Entry {
                 return YakindummPackage.Literals.ENTRY;

         }

 

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        public EntryType getType() {

+                return type;

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        public void setType(EntryType newType) {

+                EntryType oldType = type;

+                type = newType == null ? TYPE_EDEFAULT : newType;

+                if (eNotificationRequired())

+                        eNotify(new ENotificationImpl(this, Notification.SET, YakindummPackage.ENTRY__TYPE, oldType, type));

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public Object eGet(int featureID, boolean resolve, boolean coreType) {

+                switch (featureID) {

+                        case YakindummPackage.ENTRY__TYPE:

+                                return getType();

+                }

+                return super.eGet(featureID, resolve, coreType);

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public void eSet(int featureID, Object newValue) {

+                switch (featureID) {

+                        case YakindummPackage.ENTRY__TYPE:

+                                setType((EntryType)newValue);

+                                return;

+                }

+                super.eSet(featureID, newValue);

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public void eUnset(int featureID) {

+                switch (featureID) {

+                        case YakindummPackage.ENTRY__TYPE:

+                                setType(TYPE_EDEFAULT);

+                                return;

+                }

+                super.eUnset(featureID);

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public boolean eIsSet(int featureID) {

+                switch (featureID) {

+                        case YakindummPackage.ENTRY__TYPE:

+                                return type != TYPE_EDEFAULT;

+                }

+                return super.eIsSet(featureID);

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public String toString() {

+                if (eIsProxy()) return super.toString();

+

+                StringBuilder result = new StringBuilder(super.toString());

+                result.append(" (Type: ");

+                result.append(type);

+                result.append(')');

+                return result.toString();

+        }

+

 } //EntryImpl

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummFactoryImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummFactoryImpl.java
index 9c4fc4f1..d4fc2d01 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummFactoryImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummFactoryImpl.java
@@ -5,6 +5,7 @@ package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl;
 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.*;

 

 import org.eclipse.emf.ecore.EClass;

+import org.eclipse.emf.ecore.EDataType;

 import org.eclipse.emf.ecore.EObject;

 import org.eclipse.emf.ecore.EPackage;

 

@@ -75,6 +76,36 @@ public class YakindummFactoryImpl extends EFactoryImpl implements YakindummFacto
          * <!-- end-user-doc -->

          * @generated

          */

+        @Override

+        public Object createFromString(EDataType eDataType, String initialValue) {

+                switch (eDataType.getClassifierID()) {

+                        case YakindummPackage.ENTRY_TYPE:

+                                return createEntryTypeFromString(eDataType, initialValue);

+                        default:

+                                throw new IllegalArgumentException("The datatype '" + eDataType.getName() + "' is not a valid classifier");

+                }

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        @Override

+        public String convertToString(EDataType eDataType, Object instanceValue) {

+                switch (eDataType.getClassifierID()) {

+                        case YakindummPackage.ENTRY_TYPE:

+                                return convertEntryTypeToString(eDataType, instanceValue);

+                        default:

+                                throw new IllegalArgumentException("The datatype '" + eDataType.getName() + "' is not a valid classifier");

+                }

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

         public Region createRegion() {

                 RegionImpl region = new RegionImpl();

                 return region;

@@ -165,6 +196,26 @@ public class YakindummFactoryImpl extends EFactoryImpl implements YakindummFacto
          * <!-- end-user-doc -->

          * @generated

          */

+        public EntryType createEntryTypeFromString(EDataType eDataType, String initialValue) {

+                EntryType result = EntryType.get(initialValue);

+                if (result == null) throw new IllegalArgumentException("The value '" + initialValue + "' is not a valid enumerator of '" + eDataType.getName() + "'");

+                return result;

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        public String convertEntryTypeToString(EDataType eDataType, Object instanceValue) {

+                return instanceValue == null ? null : instanceValue.toString();

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

         public YakindummPackage getYakindummPackage() {

                 return (YakindummPackage)getEPackage();

         }

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummPackageImpl.java b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummPackageImpl.java
index 77092c17..e6da53ec 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummPackageImpl.java
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/ecore-gen/hu/bme/mit/inf/dslreasoner/domains/yakindu/sgraph/yakindumm/impl/YakindummPackageImpl.java
@@ -5,6 +5,7 @@ package hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.impl;
 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Choice;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.CompositeElement;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Entry;

+import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.EntryType;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Exit;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.FinalState;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Pseudostate;

@@ -18,7 +19,9 @@ import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Vertex;
 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummFactory;

 import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage;

 

+import org.eclipse.emf.ecore.EAttribute;

 import org.eclipse.emf.ecore.EClass;

+import org.eclipse.emf.ecore.EEnum;

 import org.eclipse.emf.ecore.EPackage;

 import org.eclipse.emf.ecore.EReference;

 

@@ -123,6 +126,13 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
         private EClass finalStateEClass = null;

 

         /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

+        private EEnum entryTypeEEnum = null;

+

+        /**

          * Creates an instance of the model <b>Package</b>, registered with

          * {@link org.eclipse.emf.ecore.EPackage.Registry EPackage.Registry} by the package

          * package URI value.

@@ -150,7 +160,7 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
 

         /**

          * Creates, registers, and initializes the <b>Package</b> for this model, and for any others upon which it depends.

-         * 

+         *

          * <p>This method is used to initialize {@link YakindummPackage#eINSTANCE} when that field is accessed.

          * Clients should not invoke it directly. Instead, they should simply access that field to obtain the package.

          * <!-- begin-user-doc -->

@@ -164,7 +174,8 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
                 if (isInited) return (YakindummPackage)EPackage.Registry.INSTANCE.getEPackage(YakindummPackage.eNS_URI);

 

                 // Obtain or create and register package

-                YakindummPackageImpl theYakindummPackage = (YakindummPackageImpl)(EPackage.Registry.INSTANCE.get(eNS_URI) instanceof YakindummPackageImpl ? EPackage.Registry.INSTANCE.get(eNS_URI) : new YakindummPackageImpl());

+                Object registeredYakindummPackage = EPackage.Registry.INSTANCE.get(eNS_URI);

+                YakindummPackageImpl theYakindummPackage = registeredYakindummPackage instanceof YakindummPackageImpl ? (YakindummPackageImpl)registeredYakindummPackage : new YakindummPackageImpl();

 

                 isInited = true;

 

@@ -177,7 +188,6 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
                 // Mark meta-data to indicate it can't be changed

                 theYakindummPackage.freeze();

 

-  

                 // Update the registry and return the package

                 EPackage.Registry.INSTANCE.put(YakindummPackage.eNS_URI, theYakindummPackage);

                 return theYakindummPackage;

@@ -287,6 +297,15 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
          * <!-- end-user-doc -->

          * @generated

          */

+        public EAttribute getEntry_Type() {

+                return (EAttribute)entryEClass.getEStructuralFeatures().get(0);

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

         public EClass getSynchronization() {

                 return synchronizationEClass;

         }

@@ -359,6 +378,15 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
          * <!-- end-user-doc -->

          * @generated

          */

+        public EEnum getEntryType() {

+                return entryTypeEEnum;

+        }

+

+        /**

+         * <!-- begin-user-doc -->

+         * <!-- end-user-doc -->

+         * @generated

+         */

         public YakindummFactory getYakindummFactory() {

                 return (YakindummFactory)getEFactoryInstance();

         }

@@ -398,6 +426,7 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
                 statechartEClass = createEClass(STATECHART);

 

                 entryEClass = createEClass(ENTRY);

+                createEAttribute(entryEClass, ENTRY__TYPE);

 

                 synchronizationEClass = createEClass(SYNCHRONIZATION);

 

@@ -413,6 +442,9 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
                 exitEClass = createEClass(EXIT);

 

                 finalStateEClass = createEClass(FINAL_STATE);

+

+                // Create enums

+                entryTypeEEnum = createEEnum(ENTRY_TYPE);

         }

 

         /**

@@ -471,6 +503,7 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
                 initEClass(statechartEClass, Statechart.class, "Statechart", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

 

                 initEClass(entryEClass, Entry.class, "Entry", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

+                initEAttribute(getEntry_Type(), this.getEntryType(), "Type", null, 0, 1, Entry.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

 

                 initEClass(synchronizationEClass, Synchronization.class, "Synchronization", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

 

@@ -487,6 +520,12 @@ public class YakindummPackageImpl extends EPackageImpl implements YakindummPacka
 

                 initEClass(finalStateEClass, FinalState.class, "FinalState", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

 

+                // Initialize enums and add enum literals

+                initEEnum(entryTypeEEnum, EntryType.class, "EntryType");

+                addEEnumLiteral(entryTypeEEnum, EntryType.NORMAL);

+                addEEnumLiteral(entryTypeEEnum, EntryType.HISTORY);

+                addEEnumLiteral(entryTypeEEnum, EntryType.DEEP_HISTORY);

+

                 // Create resource

                 createResource(eNS_URI);

         }

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore
index 0d6b4ac6..51b0ca5b 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.ecore
@@ -19,7 +19,9 @@
         eType="#//Vertex" eOpposite="#//Vertex/outgoingTransitions"/>

   </eClassifiers>

   <eClassifiers xsi:type="ecore:EClass" name="Statechart" eSuperTypes="#//CompositeElement"/>

-  <eClassifiers xsi:type="ecore:EClass" name="Entry" eSuperTypes="#//Pseudostate"/>

+  <eClassifiers xsi:type="ecore:EClass" name="Entry" eSuperTypes="#//Pseudostate">

+    <eStructuralFeatures xsi:type="ecore:EAttribute" name="Type" eType="#//EntryType"/>

+  </eClassifiers>

   <eClassifiers xsi:type="ecore:EClass" name="Synchronization" eSuperTypes="#//Pseudostate"/>

   <eClassifiers xsi:type="ecore:EClass" name="State" eSuperTypes="#//RegularState #//CompositeElement"/>

   <eClassifiers xsi:type="ecore:EClass" name="RegularState" abstract="true" eSuperTypes="#//Vertex"/>

@@ -30,4 +32,9 @@
   <eClassifiers xsi:type="ecore:EClass" name="Choice" eSuperTypes="#//Pseudostate"/>

   <eClassifiers xsi:type="ecore:EClass" name="Exit" eSuperTypes="#//Pseudostate"/>

   <eClassifiers xsi:type="ecore:EClass" name="FinalState" eSuperTypes="#//RegularState"/>

+  <eClassifiers xsi:type="ecore:EEnum" name="EntryType">

+    <eLiterals name="Normal"/>

+    <eLiterals name="History"/>

+    <eLiterals name="DeepHistory"/>

+  </eClassifiers>

 </ecore:EPackage>

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.genmodel b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.genmodel
index 4e34cf1d..4419a75a 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.genmodel
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/model/yakindu_simplified.genmodel
@@ -7,6 +7,11 @@
   <foreignModel>yakindu_simplified.ecore</foreignModel>

   <genPackages prefix="Yakindumm" basePackage="hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph"

       disposableProviderFactory="true" ecorePackage="yakindu_simplified.ecore#/">

+    <genEnums typeSafeEnumCompatible="false" ecoreEnum="yakindu_simplified.ecore#//EntryType">

+      <genEnumLiterals ecoreEnumLiteral="yakindu_simplified.ecore#//EntryType/Normal"/>

+      <genEnumLiterals ecoreEnumLiteral="yakindu_simplified.ecore#//EntryType/History"/>

+      <genEnumLiterals ecoreEnumLiteral="yakindu_simplified.ecore#//EntryType/DeepHistory"/>

+    </genEnums>

     <genClasses image="false" ecoreClass="yakindu_simplified.ecore#//Pseudostate"/>

     <genClasses image="false" ecoreClass="yakindu_simplified.ecore#//Vertex">

       <genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference yakindu_simplified.ecore#//Vertex/incomingTransitions"/>

@@ -20,7 +25,9 @@
       <genFeatures property="None" notify="false" createChild="false" ecoreFeature="ecore:EReference yakindu_simplified.ecore#//Transition/source"/>

     </genClasses>

     <genClasses ecoreClass="yakindu_simplified.ecore#//Statechart"/>

-    <genClasses ecoreClass="yakindu_simplified.ecore#//Entry"/>

+    <genClasses ecoreClass="yakindu_simplified.ecore#//Entry">

+      <genFeatures createChild="false" ecoreFeature="ecore:EAttribute yakindu_simplified.ecore#//Entry/Type"/>

+    </genClasses>

     <genClasses ecoreClass="yakindu_simplified.ecore#//Synchronization"/>

     <genClasses ecoreClass="yakindu_simplified.ecore#//State"/>

     <genClasses image="false" ecoreClass="yakindu_simplified.ecore#//RegularState"/>

@@ -29,5 +36,6 @@
     </genClasses>

     <genClasses ecoreClass="yakindu_simplified.ecore#//Choice"/>

     <genClasses ecoreClass="yakindu_simplified.ecore#//Exit"/>

+    <genClasses ecoreClass="yakindu_simplified.ecore#//FinalState"/>

   </genPackages>

 </genmodel:GenModel>

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml
index 8069f168..02c67af1 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/plugin.xml
@@ -18,13 +18,6 @@
       <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"/>

diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
index f4bfa3c1..09fb45c8 100644
--- a/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
+++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph/queries/hu/bme/mit/inf/dslreasoner/partialsnapshot_mavo/yakindu/patterns.vql
@@ -88,67 +88,67 @@ pattern choiceHasNoIncoming(c: Choice) {
         neg find transition(_, _, c);

 }

 

-/////////

-// Synchronization

-/////////

-

-@Constraint(severity="error", message="error", key = {s})

-pattern synchHasNoOutgoing(s : Synchronization) {

-        neg find transition(_, s, _);

-}

-

-@Constraint(severity="error", message="error", key = {s})

-pattern synchHasNoIncoming(s : Synchronization) {

-        neg find transition(_, _, s);

-}

-

-@Constraint(severity="error", message="error", key = {s})

-pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) {

-        find transition(t1, v1, s);

-        find transition(t2, v2, s);

-        t1!=t2;

-        Region.vertices(r, v1);

-        Region.vertices(r, v2);

-} or {

-        find transition(t1, s, v1);

-        find transition(t2, s, v2);

-        t1!=t2;

-        Region.vertices(r, v1);

-        Region.vertices(r, v2);

-}

-

-@Constraint(severity="error", message="error", key = {s})

-pattern notSynchronizingStates(s : Synchronization) {

-        neg find hasMultipleOutgoingTrainsition(s);

-        neg find hasMultipleIncomingTrainsition(s);

-}

-

-pattern hasMultipleOutgoingTrainsition(v : Synchronization) {

-        find transition(_, v, trg1);

-        find transition(_, v, trg2);

-        trg1 != trg2;

-}

-

-pattern hasMultipleIncomingTrainsition(v : Synchronization) {

-        find transition(_, src1, v);

-        find transition(_, src2, v);

-        src1 != src2;

-}

-

-@Constraint(severity="error", message="error", key = {s})

-pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) {

-        find transition(_, v1, s);

-        find transition(_, v2, s);

-        CompositeElement.regions.vertices(r1, v1);

-        CompositeElement.regions.vertices(r2, v2);

-        r1 != r2;

-} or {

-        find transition(_, s, v1);

-        find transition(_, s, v2);

-        CompositeElement.regions.vertices(r1, v1);

-        CompositeElement.regions.vertices(r2, v2);

-        r1 != r2;

-}

+///////////

+//// Synchronization

+///////////

+//

+//@Constraint(severity="error", message="error", key = {s})

+//pattern synchHasNoOutgoing(s : Synchronization) {

+//      neg find transition(_, s, _);

+//}

+//

+//@Constraint(severity="error", message="error", key = {s})

+//pattern synchHasNoIncoming(s : Synchronization) {

+//      neg find transition(_, _, s);

+//}

+//

+//@Constraint(severity="error", message="error", key = {s})

+//pattern SynchronizedIncomingInSameRegion(s : Synchronization, v1 : Vertex, v2 : Vertex) {

+//      find transition(t1, v1, s);

+//      find transition(t2, v2, s);

+//      t1!=t2;

+//      Region.vertices(r, v1);

+//      Region.vertices(r, v2);

+//} or {

+//      find transition(t1, s, v1);

+//      find transition(t2, s, v2);

+//      t1!=t2;

+//      Region.vertices(r, v1);

+//      Region.vertices(r, v2);

+//}

+//

+//@Constraint(severity="error", message="error", key = {s})

+//pattern notSynchronizingStates(s : Synchronization) {

+//      neg find hasMultipleOutgoingTrainsition(s);

+//      neg find hasMultipleIncomingTrainsition(s);

+//}

+//

+//pattern hasMultipleOutgoingTrainsition(v : Synchronization) {

+//      find transition(_, v, trg1);

+//      find transition(_, v, trg2);

+//      trg1 != trg2;

+//}

+//

+//pattern hasMultipleIncomingTrainsition(v : Synchronization) {

+//      find transition(_, src1, v);

+//      find transition(_, src2, v);

+//      src1 != src2;

+//}

+//

+//@Constraint(severity="error", message="error", key = {s})

+//pattern SynchronizedRegionsAreNotSiblings(s : Synchronization, v1 : Vertex, v2 : Vertex) {

+//      find transition(_, v1, s);

+//      find transition(_, v2, s);

+//      CompositeElement.regions.vertices(r1, v1);

+//      CompositeElement.regions.vertices(r2, v2);

+//      r1 != r2;

+//} or {

+//      find transition(_, s, v1);

+//      find transition(_, s, v2);

+//      CompositeElement.regions.vertices(r1, v1);

+//      CompositeElement.regions.vertices(r2, v2);

+//      r1 != r2;

+//}

 

 ///////////////////////////////

 // Extra