1

对于使用永不声明的验证（使用 ispin），我得到depth reached的输出大于状态数和转换数，例如：

Full statespace search for:
    never claim             + (REQ5)
    assertion violations    + (if within scope of claim)
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  - (disabled by never claim)

State-vector 60 byte, depth reached 87, errors: 1
       41 states, stored
       10 states, matched
       51 transitions (= stored+matched)
        9 atomic steps
hash conflicts:         0 (resolved)

我觉得这有点不直观。某处是否有“深度达到”语义的精确描述（比pan 的输出格式描述更彻底）？或许的意义

最长的深度优先搜索路径包含 87 个转换

不是指 51 个转移，而是指由永不主张组成的系统自动机的转移？

4

1 回答 1

2

是的，当您说它指的是由永不声明组成的系统自动机的转换时，您是正确的。然而同时它是被验证的系统中路径的长度，因为由never claim组成的系统的一步正是系统的一步。当然，根据从不声称，可能需要探索比系统更多或更少的过渡。路径甚至不需要无循环（取决于声明），甚至不是最小的（除非设置了特殊选项）。

于 2017-07-04T16:24:26.840 回答