属性检查的执行时间

Question

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

... 谢谢

Blockquote

.....

....

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++ 开发技能。

属性检查的执行时间

Execution time of properties checking

nusmv