module RunToCompletionContract;
create eval:UMLMM refining modeles:UMLMM;


--verify if the target state of a given transition is activated in the target state machine instance specification
helper context UMLMM!Transition def : hasBeenPassedInTarget(smInstTarget : UMLMM!StateMachineInstanceSpecification) : Boolean =
let targetTransition : UMLMM!Transition = smInstTarget.getMappedTransition(self) in
let states : Set(UMLMM!State)= smInstTarget.ActiveStates() -> collect (s | s.state) in
--case where the target state is a pseudoState and more precisely an history state
if  targetTransition.target.oclIsKindOf(UMLMM!Pseudostate) then
	if targetTransition.target.kind = #deepHistory or targetTransition.target.kind = #shallowHistory then
		let targetActiveRegion : UMLMM!ActiveRegion = smInstTarget.historyConfiguration->any(r | r.region.name = targetTransition.target.container.name) in
			let  activeStates : Set(UMLMM!ActiveState) = targetActiveRegion.getActiveStates() in 
				true 
	else
		--other kind of pseudostate: currently not managed
		false
	endif
else
	states -> exists ( s | targetTransition.target.name = s.name)
endif;


-------------------Mapping functions------------------------
helper context UMLMM!StateMachineInstanceSpecification def : getStateMachineInstanceSpecificationMapping() : UMLMM!StateMachineInstanceSpecification = 
	UMLMM!StateMachineInstanceSpecification.allInstances()->select(i | i.modelName='target' and i.stateMachine.name = self.stateMachine.name);


helper context UMLMM!StateMachineInstanceSpecification def : MappingStateMachineInstanceSpecification(statemachineinstancespecification : UMLMM!StateMachineInstanceSpecification) : Boolean =
       self.name=statemachineinstancespecification.name
;


helper context UMLMM!StateMachineInstanceSpecification def : isSource : Boolean =
        self.modelName = 'source';


helper context UMLMM!StateMachineInstanceSpecification def : getMappedTransition(trans : UMLMM!Transition) : UMLMM!Transition = 
	UMLMM!Transition.allInstances()->select(t | t.name=trans.name).asSet()->any(t|t.modelName = 'target');


-----------------get active states of an instance------------
helper context UMLMM!ActiveRegion def : getActiveStates() : Set(UMLMM!ActiveState) = 
	if self.activeSubvertex.activeRegion->size() = 0  then 
		Set{self.activeSubvertex}
	else
		self.activeSubvertex.activeRegion->collect(r | r.getActiveStates() ).including(self.activeSubvertex)
	endif;


helper context UMLMM!StateMachineInstanceSpecification def : ActiveStates() : Set(UMLMM!ActiveState) = 
	if self.activeRegion.oclIsUndefined() then
		let bag : Set(UMLMM!ActiveState) = bag.including(self) in 
		bag and self.debug('Error: no Active State')
	else
		let set : Set(UMLMM!ActiveState) = self.activeRegion->collect(c | c.getActiveStates())->flatten() in
		if set->size() > 0 then 
			set
		else 
			self.activeRegion.debug('Error : no active state collected')
		endif
	endif;


--fetch the given transition supposed to be crossed
helper context UMLMM!ActiveState def: getTransitionForEvent(trig : UMLMM!Trigger) : UMLMM!Transition =
if self.state.hasTransitionCrossable(trig) then
	let transBag : Bag(UMLMM!Transition) =  UMLMM!Transition.allInstances()->select( t | t.source.name = self.state.name) in 
	let trans : UMLMM!Transition = transBag->any(t | t.trigger->exists(tr | tr.name = trig.name)) in
		trans 
else 
		self.activeContainer.activeState.getTransitionForEvent(trig)
	endif
;


--check if a state has a possible transition to be crossed
helper context UMLMM!State def : hasTransitionCrossable(trig : UMLMM!Trigger) : Boolean = 
	let transBag : Bag(UMLMM!Transition) =  UMLMM!Transition.allInstances()->select( t | t.source.name = self.name) in 
	let trans : UMLMM!Transition = transBag->any(t | t.trigger->exists(tr | tr.name = trig.name)) in
		not trans.oclIsUndefined();
	

-- starting from the leaf, check in its hierarchy if there is an active state having a crossable transition
helper context UMLMM!ActiveState def: hasTransitionForEvent(trig : UMLMM!Trigger) : Boolean = 
if self.state.hasTransitionCrossable(trig) then
	true
else if self.activeContainer.activeState.oclIsUndefined() then
		false
	else self.activeContainer.activeState.hasTransitionForEvent(trig) 
	endif 
endif;		


-- collect leaves states active for a given state machine instance specification 
helper context UMLMM!StateMachineInstanceSpecification def : activeLeaves() : Set(UMLMM!ActiveState) = 
	if self.activeRegion.oclIsUndefined() then
		let bag : Set(UMLMM!ActiveState) = bag.including(self) in 
		bag and self.debug('Error: no Active State')
	else
		let set : Set(UMLMM!ActiveState) = self.activeRegion->collect(c | c.getActiveLeaves())->flatten() in
		if set->size() > 0 then 
			set
		else 
			self.activeRegion.debug('Error: no active leaves collected.')
		endif
	endif;

	
--recursively collect the active leaves of a given region 
helper context UMLMM!ActiveRegion def : getActiveLeaves() : Set(UMLMM!ActiveState) = 
	if self.activeSubvertex.activeRegion->size() = 0  then 
		Set{self.activeSubvertex}
	else
		self.activeSubvertex.activeRegion->collect(r | r.getActiveLeaves() )
	endif;

	
--get activeStates responding to the triggered event, and check if corresponding transitions have been crossed	
helper context UMLMM!StateMachineInstanceSpecification def : respectUMLPriority(target :UMLMM!StateMachineInstanceSpecification, event : UMLMM!Trigger) : Boolean =
let activeStatesForEvent : Set(UMLMM!ActiveState) = self.activeLeaves() -> select ( s | s.hasTransitionForEvent(event)) in
let activeTransitions : Set(UMLMM!Transition) = activeStatesForEvent -> collect ( s | s.getTransitionForEvent(event)) in
activeTransitions -> forAll ( t | t.hasBeenPassedInTarget(target));


helper context UMLMM!StateMachineInstanceSpecification def : respectUMLPriorityState() : Boolean =
	if self.isSource then
	let event : UMLMM!Trigger = UMLMM!ContractOperation.allInstances()->any(op | op.name='run_to_completion').parameters->any(p | p.name='event').reference in
	let target : UMLMM!StateMachineInstanceSpecification = UMLMM!StateMachineInstanceSpecification.allInstances()
				->select(c|not c.isSource)->any(cib|cib.MappingStateMachineInstanceSpecification(self)) in
	self.respectUMLPriority(target,event) 
	else
		false
	endif;


-------------------Rules to check transition priority respect------------------------

rule checkingOK {
from source : UMLMM!StateMachineInstanceSpecification(
		source.isSource and source.respectUMLPriorityState() 
)

to 
targetIS : UMLMM!StateMachineInstanceSpecification(
	classifier <- source.classifier,
	modelName <- source.modelName,
	activeRegion <- source.activeRegion,
	historyConfiguration <-source.historyConfiguration
),
targetRes : UMLMM!Correct(
	element <- targetIS,
	comment <- 'target active states are correct'
),
target : UMLMM!ContractEvaluation(
	globalResult <- true,
	base <- UMLMM!ContractBase.allInstances()->first(),
	results <- targetRes	 
	)
}
	

rule checkingNotOK {
from source : UMLMM!StateMachineInstanceSpecification(
		source.isSource and not source.respectUMLPriorityState() 
)
to 
targetIS : UMLMM!StateMachineInstanceSpecification(
	classifier <- source.classifier,
	modelName <- source.modelName,
	activeRegion <- source.activeRegion,
	historyConfiguration <-source.historyConfiguration
),
targetRes : UMLMM!Error(
	element <- targetIS,
	comment <- 'active states on target side are not correct regarding to the source ones and the associated event'
),
target : UMLMM!ContractEvaluation(
	globalResult <- false,
	base <- UMLMM!ContractBase.allInstances()->first(),
	results <- targetRes	 
	)
}