版权
为了区分商品，很多名称被制造商和销售商声明为商标。如果这些名称出现在本书中，并且Addison-Wesley出版社意识到这是一个商标声明，则该名称首字母大写或全部大写。
作者和出版商在编写本书时已经小心谨慎，但不作任何明示或暗示的保证，对错误或遗漏不承担任何责任。对于因使用本书包含的信息或程序而产生的偶然或间接损失，我们不承担任何责任。
在订购按照数量进行特价销售时，出版商提供这本书的折扣。 获取更多资讯，请联系：
U.S. Corporate and Government Sales: (800) 382-3419
corpsales@pearsontechgroup.com
如需在美国境外销售，请联系：
International Sales: (317) 581-3793
international@pearsontechgroup.com
访问Addison-Wesley出版社的网站：awprofessional.com
美国国会图书馆编目出版数据
Holzmann, Gerard J.
The Spin model checker: primer and reference manual / Gerard J. Holzmannp. cm
Includes bibliographical references and index.
ISBN 0-321-22862-6
1.Systems engineering––Mathematical models. 2.Computer programs––Testing. I. Title.
TA168.H65 2003
620'.001'171––dc22
2003057704
CIP
Copyright © 2004 Lucent Technologies Inc., Bell Laboratories.
保留所有权利。未经出版商事先同意，不得以任何形式或通过任何手段（电子，机械，影印，录制或其他方式）复制，存储在检索系统中或传播本出版物的任何部分。本书在美国影印。 同时在加拿大出版。
本书由作者编写，设计和排版，同时隶属于贝尔实验室的计算科学研究中心。他目前隶属于美国宇航局喷气推进实验室/加州理工学院的可靠软件实验室。
有关获得使用此作品中材料的许可的信息，请提交请求：
Pearson Education, Inc.
Rights and Contracts Department
75 Arlington Street, Suite 300
Boston, MA 0211
Fax: (617) 848-7047
文字印在再生纸上
第一次印刷，2003年9月
