资 源 简 介
What is it?
The psl2ba tool translates formulas of the IEEE standard "Property Specification Language" (PSL) into Büchi automata.
These automata are used in the model checkers NuSMV, SMV, or SPIN.
Features
The translator supports the linear-time logics LTL and PSL with past operators.
The output of psl2ba can be used in the symblic model checker NuSMV.
For further information see the README.TXT file in the package.
