Один из вариантов - использовать команду print_usage.Тем не менее, это может быть не слишком много точным, если ваша цель - собрать статистику времени для какой-либо научной цели.
Пример:
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
Разница между конечным временем и временем начала обеспечивает приблизительное измерение времени, необходимого для проверки свойства.
На практике подход, описанный в этом ответе, может быть не совсем эффективным для автоматизированных задач.требующий некоторой степени точности.К счастью, исходный код из NuSMV общедоступен, так что вы можете изменить его так, чтобы он вычислял точное время, затрачиваемое каждым проверяемым свойством.Это может потребовать некоторых c++ навыков разработки.