nusmv - 属性检查的执行时间

Question

我想知道如何计算在 NuSMV 模型检查器中检查 CTL/LTL 属性的执行时间。

... 谢谢

块引用

……

....

Answer 1

一种选择是使用命令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++开发技能。