write_boolean_model - Writes a flattened and booleanized model of a given SMV file


write_boolean_model [-h] [-o filename]

Writes the currently loaded SMV model in the specified file, after having flattened and booleanized it. Processes are eliminated and a corresponding equivalent model is printed out. If no file is specified, the file specified via the environment variable output_boolean_model_file is used if any, otherwise standard output is used.

Command options:

-o filename
Attempts to write the flat and boolean SMV model in filename.
** New in 2.4.0 and later ** Scalar variables are dumped as DEFINEs whose body is their boolean encoding. This allows the user to still express and see parts of the generated boolean model in terms of the original model's scalar variables names and values, and still keeping the generated model purely boolean. Also, symbolic constants are dumped within a CONSTANTS statement to declare the values of the original scalar variables' for future reading of the generated file.
Last updated on 2010/11/03 21h:54