Does EMF and/or ATL support satisfiability checking?

[Meijuh]

I've been experimenting a little with Eclipse Ecore + ATL and wonder if they support satisfiability checking?
From what I have seen, normally an approach would like the following. In Ecore specify a Product and an Article both with a price. Then (I believe) specify a constraint in OCL like price > 0 for both Product and Article. Furthermore, in ATL I can write a transformation that instantiates an Article from a Product that copies the price. If the transformation is erroneous (e.g., it always sets the price to zero), that can be detected by validation of Article.

Now I want to "lift" my meta model; in Ecore I want to specify an Entity which can be instantiated as a Product and Article including their constraint price > 0. Is there any way I can prove my model transformation from Product to Article preserves the truth of this constraint (assuming it was true for Product)? I know I can use tools like Z3 to accomplish this, but I wonder if this capability is included in Eclipse EMF itself?

[merks]

I can't really speak to what's provided by OCL and ATL.

You can specify named constraints directly in the Ecore model, e.g., here for Ecore.ecore itself:

and then implement them in the generated validator, e.g.,

org.eclipse.emf/plugins/org.eclipse.emf.ecore/src/org/eclipse/emf/ecore/util/EcoreValidator.java

Lines 539 to 571 in 95e4296

	/**
	* Validates the ConsistentTransient constraint of '<em>EAttribute</em>'.
	* <!-- begin-user-doc -->
	* <!-- end-user-doc -->
	* @generated NOT
	*/
	public boolean validateEAttribute_ConsistentTransient(EAttribute eAttribute, DiagnosticChain diagnostics, Map<Object, Object> context)
	{
	EDataType eAttributeType = eAttribute.getEAttributeType();
	boolean result =
	isEffectivelyTransient(eAttribute) ||
	eAttributeType == null ||
	eAttributeType.isSerializable() ||
	FeatureMapUtil.isFeatureMapEntry(eAttributeType);
	if (!result && diagnostics != null)
	{
	String attributeName = eAttribute.getName();
	if (eAttribute.getEContainingClass() != null)
	{
	attributeName = eAttribute.getEContainingClass().getName() + "." + attributeName;
	}
	diagnostics.add
	(createDiagnostic
	(Diagnostic.ERROR,
	DIAGNOSTIC_SOURCE,
	CONSISTENT_TRANSIENT,
	"_UI_EAttributeConsistentTransient_diagnostic",
	new String[] { attributeName },
	new Object[] { eAttribute, EcorePackage.Literals.ESTRUCTURAL_FEATURE__TRANSIENT },
	context));
	}
	return result;
	}