0

我正在努力进行一些简单的验证。我有这样的自动机和值 x:

自动机 自动机2

当开始处的 x 与 0 不同时,满足 E<> x !=0,但当 x = 0 时,则不满足,满足 E<> x == 0 和 A<> x == 0。但我想对 E<> x !=0 不满意,即使 x 在开始时与 0 不同。

我应该改变什么?验证器是如何工作的?空路径,什么都不执行的时候也是正确的路径吗?所有可能路径的集合也包含这个空路径吗?

4

1 回答 1

0

初始状态与任何其他状态一样,因此如果 x 在初始状态下为 0,则从该状态开始的所有路径最终将处于x = 0成立状态。如果要检查是否x = 0处于任何其他状态,则需要在查询中排除初始状态。例如E<> x=0 and not line1.S0.

于 2019-02-18T17:30:02.290 回答