2

似乎 Promela 初始化了每个变量（默认为 0，或声明中给出的值）。

如何声明由未知值初始化的变量？

文档建议if :: p = 0 :: p = 1 fi但我认为它不起作用：Spin 仍然验证此声明

bit p 
init {   if ::  p = 0 :: p = 1 fi }
ltl {  ! p  }

（并伪造p）

那么 的语义究竟是什么init？还有一些“预初始”状态？我怎样才能解决这个问题 - 而不是让我的学生感到困惑？

4

1 回答 1

3

这是个有趣的问题。

文档说每个变量都初始化为 0，除非模型另有说明。

与所有变量声明一样，显式初始化字段是可选的。所有变量的默认初始值为零。这适用于标量变量和数组变量，也适用于全局变量和局部变量。

在您的模型中，您不会在声明变量时对其进行初始化，因此随后在初始状态下将其分配给值 0，该值位于您的分配之前：

bit p

init {
  // THE INITIAL STATE IS HERE
  if
    :: p = 0
    :: p = 1
  fi
}

ltl {  ! p  }

一些实验。

避免此限制的“天真”想法是修改调用时由 spin 生成的pan.c的c 源代码，以便随机初始化变量。~$ spin -a test.pml

而不是这个初始化函数：

void
iniglobals(int calling_pid)
{
        now.p = 0;
#ifdef VAR_RANGES
        logval("p", now.p);
#endif
}

可以尝试这样写：

void
iniglobals(int calling_pid)
{
        srand(time(NULL));
        now.p = rand() % 2;
#ifdef VAR_RANGES
        logval("p", now.p);
#endif
}

并在标题部分添加一个#include <time.h>。

但是，一旦您将其编译为带有 的验证程序gcc pan.c并尝试运行它，您将获得取决于变量p的初始化值的非确定性行为。

它都可以确定该属性被违反：

~$ ./a.out -a
pan:1: assertion violated  !( !( !(p))) (at depth 0)
pan: wrote test.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (ltl_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 0, errors: 1
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds

或打印该属性已满足：

~$ ./a.out -a
(Spin Version 6.4.3 -- 16 December 2014)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (ltl_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 0, errors: 0
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in init
    test.pml:8, state 5, "-end-"
    (1 of 5 states)
unreached in claim ltl_0
    _spin_nvr.tmp:8, state 8, "-end-"
    (1 of 8 states)

pan: elapsed time 0 seconds

显然，通过自旋验证的promela 模型的初始状态被假定为唯一的。毕竟，这是一个合理的假设，因为它会使事情变得不必要地复杂化：您总是可以用初始状态 S st S 替换 N 个不同的初始状态 S_i 允许通过 epsilon-transition 到达每个 S_i。在这种情况下，你得到的并不是真正的 epsilon-transition，但在实践中它几乎没有什么区别。

编辑 （来自评论）：原则上，可以通过进一步修改pan.c来完成这项工作：

  • 将初始状态初始化器转换为初始状态生成器
  • 修改验证例程以考虑可能存在多个初始状态，并且该属性必须为每个初始状态保持

话虽如此，这可能不值得麻烦，除非这是通过修补Spin的源代码来完成的。

解决方法。

如果你想声明某事在初始状态下是真的，或者从初始状态开始，并考虑到一些非确定性的行为，那么你应该写如下内容：

bit p
bool init_state = false

init {
  if
    :: p = 0
    :: p = 1
  fi
  init_state = true // TARGET STATE
  init_state = false
}

ltl {  init_state & ! p  }

你得到：

~$ ./a.out -a

pan:1: assertion violated  !( !((initialised& !(p)))) (at depth 0)
pan: wrote 2.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (ltl_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 0, errors: 1
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds

初始化语义。

Init只是保证是第一个生成的进程，并且用于生成其他进程，例如，当其他例程将某些参数作为输入时，例如某些资源是共享的。更多信息在这里。

我相信这个文档片段有点误导：

init 进程最常用于初始化全局变量s，并在系统执行开始之前通过使用 run 运算符来实例化其他进程。但是，任何进程，不仅仅是 init 进程，都可以这样做

由于可以保证 init 进程在使用该语句的任何其他进程之前执行其所有代码，因此从编程的角度来看atomic { }，可以说它可用于在其他进程使用变量之前对其进行初始化。但这只是一个粗略的近似，因为 init 进程并不对应于执行模型中的唯一状态，而是对应于根的状态树，而根本身仅由全局环境给出，因为它在任何之前都是如此。过程开始。

于 2016-11-02T08:42:25.767 回答