Systems of communicating machines (SCM) is a formal model for the specification, verification and testing of communication protocols, which has been used to specify and verify several well-known protocols. The authors discuss a program, called mushroom, which automates the analysis using the SCM model. The program generates either the system state analysis or the full reachability analysis. The automation of this model is expected to greatly facilitate the use of the model for protocol design and analysis. The program has been used to verify some theoretical results, serving to confirm these earlier results.>