=========================================================================== Murphi Release 3.0 Finite-state Concurrent System Verifier. Copyright (C) 1992 - 1999 by the Board of Trustees of Leland Stanford Junior University. Responsible for this release: Ulrich Stern (uli@verify.stanford.edu) =========================================================================== 1. Introduction If you are a new Murphi user, please take a look at the Readme file in the doc directory. There, you will find some information about the avail- able documentation and recommendations on what to read first. The Murphi Release 3.0 includes the following methods for reducing the memory requirements during verification: - symmetry and multiset reduction - hash compaction Both of the above techniques were present in the Release 2.91S already. The new features of Release 3.0 are: - improved portability - improvements in hash compaction - faster verification - and some bug-fixes Currently, we are working on new Murphi versions that will combine the existing methods for reducing the memory requirements with new ones and on a parallel Murphi version. Check the Murphi web-page for the latest news (http://sprout.stanford.edu/dill/murphi.html). There, you can also download several papers about Murphi. Please see the license file for details of terms and conditions, and mail bug reports, questions, suggestions, etc. to "murphi@verify.stanford.edu". If you are using Murphi, please register by sending mail to the same address saying who you are and as much as you like about what you are using it for. We will add you to a mailing list for announcements of new releases, etc. 2. Improved Portability The Murphi Compiler (mu) has traditionally been pretty portable. If you do not find an executable of the compiler for your machine in the bin directory, go to the src directory and follow the instructions in the Readme file to generate the Murphi Compiler. However, compiling the Murphi Verifier for your protocol using the C++ file generated by the Murphi Compiler has previously not always been easy. The Murphi Verifier now compiles with more C++ compilers and on more machines. It works on the machines listed in the following. However, for some compilers special options have to be used. Please look at one of the Makefiles in the ex (example) directories to find out what is required to get it working. It is recommended to tailor this Makefile to your needs. Tested environments: Computer OS C++ Compiler ---------------------------------------------------------------------- SGI INDY IRIX 5.3 g++ 2.6.3, OCC 3.2.1 and DCC 4.0 Sun SPARC20 SunOS 4.1.3_U1 g++ 2.6.0 Sun SPARC20 SunOS 4.1.4 g++ 2.7.2 and CC 3.x Sun SPARC20 SunOS 5.4 g++ 2.7.2 Sun SPARCserver-1000 SunOS 5.5 CC 4.1 HP 9000/770 HP-UX 10.10 HP C++ 10.09 Intel (PC) Linux 1.3.48 g++ 2.7.0 Intel (PC) Linux 2.0.27 g++ 2.8.1 Intel (PC) Linux 2.0.34 egcs-1.0.2 It was tried to make Murphi conform to the C++ semantics given in "The Annotated C++ Reference Manual", 1990, reprinted with corrections April, 1995. This book is being used for an ANSI Standardization of C++. Unfortunately, many compilers - especially older g++ versions - allowed several "tricks" that were not allowed according to this book. The g++ compilers can be obtained via anonymous FTP on the Internet. We got them from prep.ai.mit.edu. >>> Important <<< To check if Murphi is working correctly on your system, you might want to go to the ex/sci directory and follow the instructions in the file Murphi.Check. This check is especially recommendable if you are not run- ning Murphi in one of the environments listed above. 3. Improvements in Hash Compaction As in the previous Murphi release, hash compaction is only used when you COMPILE the protocol with "mu -c protocol.m". When you run the verifier for this protocol, you can now choose the number of bits for the compressed states. See Section 8.2 of the Murphi user manual (doc directory) for some information on how to choose this number. The default value is 40 bits, which typically gives you a probability that you omitted even one state during the state space exploration of less than 0.1%. Murphi now reports the omission probabilities at the end of the state space exploration. Thus, the Murphi user can asses if she/he wants to change the number of bits in the compressed values or re-run the ver- ifier. Again, see Section 8.2 of the user manual. When using hash compaction together with breadth-first search, Murphi can now also generate error traces. The information needed to generate the error traces is stored in a temporary file ("protocol-name.trace"). The user has to specify the directory for this file with the verifier option "-d dir" - otherwise the file will not be created and no trace can be printed in the case of protocol errors. The memory requirements for each state in this file are the compressed value (rounded up to full bytes) plus another 4 bytes. 4. Faster Verification Our experience on bigger examples is that Murphi Release 3.0 runs rough- ly 2-4 times faster than the previous Release 2.91S. =========================================================================== This directory should contain the following: Bugfixes : list of bugs fixed after first release date License : license file for details of terms and conditions Readme : this file bin : executables for the Murphi compiler doc : documents on how to use Murphi ex : examples written in the Murphi description language include : include files for compilation of Murphi verifier src : sources codes for the Murphi compiler ===========================================================================