变换的自旋模型NuSMV模型

SPIN and NuSMV are two kinds of different model checkers. SPIN is used to model the distributed software systems. Its on-the-fly traversal and partial order reduction strategy often shorten the time dramatically. NuSMV is used to describe state transition systems. Symbol model checking and bounded model checking are NuSMV"s main features. This project is aim to develop a tool to connect these two model checker together by translating SPIN program to NuSMV program.