|
 |
|
 | |  |
|
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;
}
}
| | | |