DYNAMO Tool Description: Para2Smv

Name

Para2Smv: Para to SMV translator.

Description

Para2Smv reads a Para file and converts it into input for an SMV Model Checker. Para2Smv only provides the automatic generation of the state information. The CTL file must be provided seperately by the user. The user may do this by manually editting the generated file or by including an existing file using the -c option.

Operating System Dependencies

Para2Smv is compilable under UNIX or Solaris operating systems.

Program Dependencies

To compile Para2Smv, the SMVModel code must already be compiled. Download information and compilation instructions for SMVModel can be found here.

Compilation Instructions

Once SMVModel has been installed on the system, the user will need to modify the Para2Smv makefile to point to the current location of the SMVModel installation:

SMVMODELHOME = current path to SmvModel

Then type "make" to generate the Para2Smv executable.

Download

Para2Smv source code for unix/solaris can be downloaded here.

Point of Contact

dynamo-support@cc.gatech.edu

Last modified: Mon Mar 11 15:08:32 EST 2002