-- Short Transformation Sequences
-- see http://www.cs.bme.hu/~gervarro/publication/TUB-TR-05-EE17.pdf
-- $Id$
module STS;

metamodel TRACE : 'http://www.eclipse.org/m2m/atl/emftvm/2011/Trace';
metamodel Mutex : 'http://soft.vub.ac.be/simplegt/2011/MutexA';
transform M : Mutex, T : TRACE;

context Mutex!Process def : reqCount : Integer = 10;

static def : processes : Sequence(Mutex!Process) =
	Mutex!Process.allInstancesFrom('M');

---------- PHASE 1 ----------

abstract rule phase1 {
	not t : TRACE!TraceLink in T
}

rule newRule extends phase1 {
	from p : Mutex!Process in M (next =~ p2),
		p2 : Mutex!Process in M
	not p : Mutex!Process in M (reqCount =~ Env::processes->size())
	to p : Mutex!Process (next =~ p1),
		p1 : Mutex!Process (next =~ p2),
		p2 : Mutex!Process
}

rule mountRule extends phase1 {
	from p : Mutex!Process in M
	not r : Mutex!Resource in M
	to p : Mutex!Process,
		r : Mutex!Resource (token =~ p)
}

rule endPhase1 extends mountRule {
	to t : TRACE!TraceLink
}

---------- PHASE 2 ----------

abstract rule phase2 {
	from t : TRACE!TraceLink in T
	not s : TRACE!SourceElement in T
	to t : TRACE!TraceLink in T
}

unique rule requestRule extends phase2 {
	from p : Mutex!Process in M,
		r : Mutex!Resource in M
	not p : Mutex!Process in M (request =~ m),
		m : Mutex!Resource in M
	not r : Mutex!Resource in M (held_by =~ p)
	to p : Mutex!Process (request =~ r),
		r : Mutex!Resource
}

rule endPhase2 extends phase2 {
	to s : TRACE!SourceElement
}

---------- PHASE 3 ----------

abstract rule phase3 {
	from s : TRACE!SourceElement in T,
		r : Mutex!Resource in M
	to s : TRACE!SourceElement,
		r : Mutex!Resource
}

rule takeRule extends phase3 {
	from r : Mutex!Resource in M (token =~ p), 
		p : Mutex!Process in M (request =~ r)
	to r : Mutex!Resource (held_by =~ p),
		p : Mutex!Process
}

rule releaseRule extends phase3 {
	from r : Mutex!Resource in M (held_by =~ p),
		p : Mutex!Process in M
	not p : Mutex!Process in M (request =~ m),
		m : Mutex!Resource in M
	to r : Mutex!Resource (release =~ p),
		p : Mutex!Process
}

rule giveRule extends phase3 {
	from r : Mutex!Resource in M (release =~ p1),
		p1 : Mutex!Process in M (next =~ p2),
		p2 : Mutex!Process in M
	to r : Mutex!Resource (token =~ p2),
		p1 : Mutex!Process (next =~ p2),
		p2 : Mutex!Process
}