write_coi_model - Writes a flat model of SMV file, restricted to the COI of the model properties
write_coi_model [-h] [-o filename] [-n | -p | -P ] | [-c] | [-l] | [-i] | [-s] | [-q] | [-p expr] | [-C] | [-g]
Writes the currently loaded SMV model in the
specified file, after having flattened it. If a property is
specified, the dumped model is the result of applying the COI over
that property. otherwise, a restricted SMV model is dumped for each
property in the property database.
Processes are eliminated and a corresponding equivalent model is
printed out.
If no file is specified, stderr is used for output
Command options:
- -o filename
- Attempts to write the flat and boolean SMV model in
filename.
- -c
- Dumps COI model for all CTL properties
- -l
- Dumps COI model for all LTL properties
- -i
- Dumps COI model for all INVAR properties
- -s
- Dumps COI model for all PSL properties
- -q
- Dumps COI model for all COMPUTE properties
- -p expr
- Applies COI for the given expression "expr"
- -n idx
- Applies COI for property stored at index "idx"
- -P name
- Applies COI for property named "name" idx
- -C
- Only prints the list of variables that are in
the COI of properties
- -g
- Dumps the COI model that represents the union of all COI properties
Last updated on 2010/05/19 15h:56