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