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 2011/04/06 21h:13