I want to know how to calculate the execution time of CTL/LTL properties checking in NuSMV model checker.
... thanks
Blockquote
....
....
One option is to use the command print_usage. However, this might not be that much precise if your purpose is to collect timing statistics for some scientific purpose.
Example:
NuSMV > reset
NuSMV > read_model -i some_model.smv
NuSMV > go
NuSMV > print_usage
...
User time 0.268 seconds
System time 0.043 seconds
...
NuSMV > check_property
-- specification AG (AF state = MOVE) is false
-- as demonstrated by the following execution sequence
...
NuSMV > print_usage
...
User time 0.494 seconds
System time 0.051 seconds
...
NuSMV > quit
The difference between the final time and the starting time provides a rough measurement of the time required for checking the property.
In practice, the approach described in this answer may not be quite effective for automated tasks requiring some degree of precision. Luckily, the source code of NuSMV is publicly available, so you can actually modify it so that it computes the exact time taken by each property being checked. This may require some c++ development skills.