Translation between S/R and Promela

S/R and Promela are two concurrent programming languages used in finite state automated verification of communication protocols. The semantics of S/R supports synchronous parallel composition, while semantics of Promela supports an interleaving parallel composition of processes. Because of the differences in the execution model, the verification tools available for the models written in these languages are optimized differently. SPIN, a verification tool for models written in Promela, uses partial order reduction reductions based upon commutativity of interleaving to combat the state explosion problem due to the amount of concurrency in concurrent models. COSPAN, a tool used largely for hardware verification for models written in S/R, offers implicit enumeration and automatic reduction of the specification with respect to the properties to be verified. Because of such differences in the techniques used for combating the practical problems faced in verification of protocols, it may be d..