标签: model-checking

符号执行和模型检查之间有什么区别(例如在模型转换中)？我不明白他们的区别.它们是一样的吗？!

有没有人接触过这个工具SPIN的模型检查,更多的模型检查信息(并发程序)

以下是导致此问题的代码.

        if 
            :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> 
              proc2clk[0] ? fromProc[0]; // Woke up
            :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) ->
              clk2proc[0] ! 0;  
            ::else -> 
              time = time + 1; // just for debugging
        fi; 

如果我在第一个条件中删除了nempty调用,则错误消失.根据我的阅读,你不能使用else语句,如果你在条件中使用receive或send语句,但据我所知,nempty不是发送或接收语句,而只是检查一个通道是否是不是空的.那么,我在做什么错,我怎么能解决这个问题.

我正在使用 SPIN 模型检查器 GUI - iSPIN。GUI 带有一个不错的 Automaton 视图生成器，但是为了查看完整的自动机，我需要放大/缩小。如果可能的话，我还想将该自动机保存在一个漂亮的图像中（避免使用打印屏幕）。有没有办法根据 Promela 模型从 SPIN 或其他可以生成自动机的工具中保存生成的自动机图像？

PS 下面是一张图像，显示了我想保存的生成的自动机图像。显然，我无法仅通过打印屏幕来重新创建它。

我使用的是 Windows 操作系统，在 Cygwin 中输入：wish -f ispin.tcl打开 ispin 界面。我打开一个文件test.pml，其中包含：

byte state = 2;

proctype A()
{   (state == 1) -> state = 3
}

proctype B()
{   state = state - 1
}

init
{   run A(); run B()
}

之后，我使用随机方式运行它，种子 = 123。结果打印在输出中，没有问题：

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting A with pid 1
  1:    proc  0 (:init::1) creates proc  1 (A)
  1:    proc  0 (:init::1) test.pml:12 (state 1)    [(run A())]
Starting B with …

我希望能够将系统建模为有限状态机，并根据时间逻辑规范测试模型的属性。

我知道 StateFlow 的模型检查功能，但如果可能的话，我更愿意使用 Python，因为它是开源的。我也知道 TuLiP 是设计和模拟有限状态机的可靠选择，但据我所知，它不进行模型检查。Python wiki 上的 FSM 包列表似乎充满了类似的以实现为中心的包。

有谁知道一个不同的 Python 包，它能够根据时间逻辑设计规范进行模型检查？

我想在检查模型时打印所有状态。当发生断言冲突时，我们确实获得了跟踪文件，但是即使没有断言冲突，我也想查看状态。我怎样才能做到这一点？

是否有任何操作返回Alloy中关系的范围和域.

假设我在Alloy中定义了一个sig:

sig A {r : B }

sig B {}

我正在寻找和操作应用于r并给我B(可能像r [B]返回B)

上面的情况可能看起来很愚蠢,因为r [B]会返回B,所以为什么我不首先使用B!实际上我发现有一个范围和域操作(如果它们存在)在编写事实(约束)时非常有用.例如:

sig O {sup:O}

sig M{mid: O, sup:O} {mid.sup=sup}

sig F{fid:O, sup:O}{fid.sup=sup}


fact K{
   all o:O | lone so:M | so.mid=o 
   all o:O | lone so:F | so.fid=o
   all o:O | one i:(fid+mid) | o in i[O]   //I want to say fid+mid is injective, so expecting i[O] return range of i
 }

任何的想法？:)