plugins/org.eclipse.qvtd.pivot.qvtbase/model/QVTbase.ocl

import 'platform:/resource/org.eclipse.qvtd.pivot.qvtbase/model/QVTbase.ecore'
--import 'http://www.eclipse.org/ocl/2015/Pivot'

package qvtbase

context Domain
inv NameIsTypedModelName:
	typedModel <> null implies name = typedModel.name

inv TypedModelIsTransformationModelParameter:
	oclContainer().oclIsKindOf(Transformation) and typedModel <> null implies
	oclContainer().oclAsType(Transformation).modelParameter->includes(typedModel)

context Function
inv ParametersAreFunctionParameter:
	ownedParameters->forAll(oclIsKindOf(FunctionParameter))

inv ReturnTypeIsQueryType:
	queryExpression <> null implies queryExpression.type?.conformsTo(type)

context Predicate
inv ConditionIsBoolean:
conditionExpression.type = Boolean

context Rule
inv DomainNameIsUnique:
	domain->isUnique(name)

inv AtLeastOneDomainIsCheckableOrEnforceable:
	domain->notEmpty() implies domain->exists(isCheckable or isEnforceable)

inv NoOverridesCycle:
	overridden->closure(overridden)->excludes(self)

--inv OverridesRuleIsExtendedRule:
--	overrides <> null and transformation <> null implies
--	let extendedRules = transformation->closure(_extends)->excluding(transformation)?->collect(rule)
--	in extendedRules->includes(overrides)

inv AbstractRuleIsOverridden:
	isAbstract implies overrides->notEmpty()

inv OverridingRuleOverridesAllDomains:
	overridden <> null implies
	overridden.domain->forAll(od | self.domain.name->includes(od.name))

context Transformation
inv ContextTypeIsTransformation:
	ownedContext <> null implies ownedContext.type.oclIsKindOf(Transformation)

inv ExtendedTypedModelIsExtended:
	_extends <> null implies
	_extends.modelParameter->forAll(etm |
		self.modelParameter->select(name = etm.name).usedPackage->includesAll(etm.usedPackage)
	)

inv ModelParameterIsUnique:
	modelParameter->isUnique(name)

inv NoExtendsCycle:
	_extends->closure(_extends)->excludes(self)

context TypedModel
inv ExclusivePrimitiveThisTrace:
	if isPrimitive then 1 else 0 endif + if isThis then 1 else 0 endif + if isTrace then 1 else 0 endif <= 1

endpackage