标签: spin

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

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 == …

<ImageView
      android:id="@+id/imageView1"
      android:layout_width="300dp"
      android:layout_height="300dp"
      android:src="@drawable/zaid1"
      android:layout_centerVertical="true"
      android:layout_centerHorizontal="true" />

我在活动中间有一个imageview,我怎么做它让它无休止地旋转360度？

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。

我正在尝试重现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; …

有没有人接触过这个工具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 …

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

我正在使用如下代码在验证模式下运行旋转。名为“从不”的函数出现问题。在执行时，它给了我一个错误，函数 inc()、dec() 和 reset() 从未完成。但是如果我添加一个循环，效果很好。根据文档，“从不”检查每一步的变量。那么，为什么它在没有循环的情况下不起作用？

int x=0
proctype Inc(){
 do
  ::true ->
    if
      ::x<10->x=x+1
    fi
 od
}

proctype Dec(){
 do
  ::true ->
    if
      ::x>0->x=x-1
    fi
 od
}

proctype Reset(){
 do
  ::true ->
   if
    ::x==10->x=0
   fi
 od
}


never {       // if I need this to work, i have to add
  To_Init:    //  this line
    if 
      :: (x<0) || (10<x) -> goto accept
      :: else -> goto To_Init      //  and that line
    fi;
  accept:
}

init{
  run Inc();
  run Dec();
  run …

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