global AcquireUseRelease(role C, role D, role S1, role S2) {
par {
inf {
ACQ() from C to S1;
PERM() from S1 to C;
fin {
USE(string) from C to S2;
}
REL() from C to S1;
}
} and {
inf {
ACQ() from D to S1;
PERM() from S1 to D;
fin {
USE(string) from D to S2;
}
REL() from D to S1;
}
}
produces the right output but with extra isolated FSMs that should not be there.
This protocol:
produces the right output but with extra isolated FSMs that should not be there.