actions Mutex using MutexModel;

rule newRule {
	pattern {
    p1:Process -n:next-> p2:Process;
	}
	replace {
    p1 -n1:next-> p:Process -n2:next-> p2;
	}
}

rule killRule {
	pattern {
		p1:Process -n1:next-> p:Process -n2:next-> p2:Process;
	}
	replace {
		p1 -n:next-> p2;
	}
}

rule mountRule {
	pattern {
		p:Process;
	}
	replace {
		p <-t:token- r:Resource;
	}
}

rule unmountRule {
	pattern {
		node r [prio=5000] : Resource;
		p:Process <-t:token- r;
	}
	replace {
		p;
	}
}

rule passRule {
	pattern {
		node r [prio=5000] : Resource;
		r -:token-> p1:Process -n:next-> p2:Process;
		negative {
			r <-req:request- p1;
		}	
	}
	replace {
		p1 -n-> p2 <-t:token- r;
	}
}

rule requestRule {
	pattern {
		p:Process;
		r:Resource;
		negative {
			r -hb:held_by-> p;
		}
		negative {
			p -req:request-> r;
		}
		negative {
			p -req:request-> m:Resource;
		}
	}
	replace {
		p -req:request-> r;
	}
}

rule takeRule {
	pattern {
		node r [prio=5000] : Resource;
		r -t:token-> p:Process -req:request-> r;
	}
	replace {
		r -hb:held_by-> p;
	}
}

rule releaseRule {
	pattern {
		node r [prio=5000] : Resource;
		r -hb:held_by-> p:Process;
		negative {
			p -req:request-> m:Resource;
		}
	}
	replace {
		r -rel:release-> p;
	}
}

rule giveRule {
	pattern {
		node r [prio=5000] : Resource;
		r -rel:release-> p1:Process -n:next-> p2:Process;
	}
	replace {
		p1 -n-> p2 <-t:token- r;
	}
}

rule blockedRule {
	pattern {
		node r [prio=5000] : Resource;
		p1:Process -req:request-> r -hb:held_by-> p2:Process;
	}
	replace {
		p1 -req-> r -hb-> p2;
		p1 <-b:blocked- r;
	}
}

rule waitingRule {
	pattern {
		node r [prio=5000] : Resource;
		r2:Resource -b:blocked-> p1:Process <-hb:held_by- r1:Resource <-req:request- p2:Process;
	}
	replace {
		p1 <-hb- r1 <-req- p2 <-bn:blocked- r2;
	}
}

rule ignoreRule {
	pattern {
		node r [prio=5000] : Resource;
		p:Process <-b:blocked- r;
		negative {
			p <-hb:held_by- m:Resource;
		}
	}
	replace {
		p; r;
	}
}

rule unlockRule {
	pattern {
		node r [prio=5000] : Resource;
		p:Process <-b:blocked- r -hb:held_by->p;
	}
	replace {
		p <-rel:release- r;
	}
}


// Mutex*

rule requestStarRule {
	pattern {
		r1:Resource -h1:held_by-> p1:Process <-n:next- p2:Process <-h2:held_by- r2:Resource;
		negative {
			p1 -req:request-> r2;
		}
	}
	replace {
		r1 -h1-> p1 <-n- p2 <-h2- r2;
		p1 -req:request-> r2;
	}
}

rule releaseStarRule {
	pattern {
		p1:Process -rq:request-> r1:Resource -h1:held_by-> p2:Process <-h2:held_by- r2:Resource;
	}
	replace {
		p1 -rq-> r1 -rl:release-> p2 <-h2- r2;
	}
}


// Mutex'

rule requestSimpleRule {
	pattern {
		node r [prio=5000] : Resource;
		p:Process <-t:token- r;
		negative {
			p -req:request-> r;
		}
	}
	replace {
		p <-t- r;
		p -req:request-> r;
	}
}



// Mutex* aux func.

rule aux_attachResource {
	pattern {
		p:Process;
		negative {
			p <-:held_by- r:Resource;
		}
	}
	replace {
		p <-:held_by- r:Resource;
	}
}