标签: promela

我是旋转模型检查的新手,想知道这个错误意味着什么:

unreached in proctype P1
    ex2.pml:16, state 11, "-end-"
    (1 of 11 states)
unreached in proctype P2
    ex2.pml:29, state 11, "-end-"
    (1 of 11 states)

这是我的代码:

int y1, y2;
byte insideCritical;

active proctype P1(){
do
    ::true->
        y2 = y1 + 1;
        (y1 == 0 || y2 < y1);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y2 = 0;
od
}
active proctype P2(){
do
    ::true->
        y1 = y2 + 1;
        (y2 == …

有谁知道你是否可以使用(或转换)vim语法高亮定义文件与Sublime文本？

我正在为promela寻找荧光笔,只找到一个用于vim,但我使用sublime-text作为我的默认编辑器

定义我发现https://github.com/vim-scripts/promela.vim/blob/master/syntax/promela.vim

我正在尝试重现Dijkstra在题为"协作顺序进程"的文章中编写的ALGOL 60代码,代码是第一次尝试解决互斥问题,这里是语法:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end 

所以我试着在Promela中重现上面的代码,这是我的代码:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn; …

我对这个词的含义不太确定。我在我们学习并发的课程中看到了它。我已经看到了许多有关数据交织的定义，但是我可以找到有关进程交织的任何信息。

当我直觉告诉我这是使用线程同时运行多个进程时，是正确的吗？

The "Automata View" in iSpin (v. 1.1.4) shows .. exactly what? It seems it is just a graph of the control flow of one process.

How would I get the full state space of the system?

例如，在Ben-Ari：自旋模型检查器的原理中，我想要图4.1。或在Overview中，我想要图1。

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

        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 …

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

当我尝试使用ispin验证模型时,我得到一个错误"长长时间对于gcc来说太长了".我的gcc有问题吗？