如何在 Spin 中创建一个未初始化的变量？
how to make a non-initialised variable in Spin?
似乎 Promela 初始化了每个变量（默认情况下，初始化为 0，或声明中给出的值）。
如何声明一个由未知值初始化的变量？
文档建议 if :: p = 0 :: p = 1 fi 但我不认为
它有效：Spin 仍然验证此声明
bit p
init { if :: p = 0 :: p = 1 fi }
ltl { ! p }
（并伪造 p）
那么 init 的语义到底是什么？还是有的
"pre-initial"状态？我怎样才能解决这个问题 - 而不是让我的学生感到困惑？
这是一个有趣的问题。
documentation 表示每个变量都初始化为 0，除非模型另有说明。
As with all variable declarations, an explicit initialization field is optional. The default initial value for all variables is zero. This applies both to scalar variables and to array variables, and it applies to both global and to local variables.
在您的模型中，您在声明变量时并未对其进行初始化，因此随后将其分配给初始状态下的值 0，该值位于您赋值之前：
bit p
init {
// THE INITIAL STATE IS HERE
if
:: p = 0
:: p = 1
fi
}
ltl { ! p }
一些实验。
"naive" 一个避免此限制的想法是修改 c 源代码 pan.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
}
并在 header 部分添加一个 #include <time.h>。
但是，一旦您使用 gcc pan.c 将其编译成验证器并尝试 运行 它，您将获得 non-deterministic 行为 取决于变量的初始化值 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 模型 的 初始状态 被 spin 验证为是独一无二的。 毕竟，这是一个合理的假设，因为它会不必要地使事情复杂化：您总是可以用初始状态 S s.t 替换 N 个不同的初始状态 S_i。 S 允许使用 epsilon-transition 到达每个 S_i。在这种情况下，您得到的并不是真正的 epsilon-transition，但在实践中几乎没有区别。
编辑 （来自评论）：
原则上，可以通过稍微进一步修改 pan.c 来完成这项工作：
- 将初始状态初始化器转换为初始状态
的生成器
- 修改验证例程以考虑可能存在多个初始状态，并且 属性 必须对每个初始状态成立
话虽如此，这可能不值得麻烦，除非这是通过修补 Spin 的源代码来完成的。
解决方法。
如果你想声明某事在初始状态下为真，或者从初始状态开始，并考虑到一些non-deterministic行为，那么你应该写如下内容：
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 只是保证是 生成的第一个进程 ，并且意味着 用于生成other processes when, for-example, other routines 输入一些参数, 例如一些资源是共享的。更多信息 here.
我认为 documentation 的这个片段有点误导：
The init process is most commonly used to initialize global variables,
and to instantiate other processes, through the use of the run
operator, before system execution starts. Any process, not just the
init process, can do so, though
由于可以使用 atomic { } 语句保证 init 进程在任何其他进程之前执行其所有代码，因此可以说它可以从编程的角度，用于在变量被其他进程使用之前初始化变量。但这只是一个粗略的近似，因为init进程并不对应执行模型中的唯一状态，而是对应于树根状态，根本身仅由 全局环境 给出，就像在任何进程启动之前一样。
似乎 Promela 初始化了每个变量（默认情况下，初始化为 0，或声明中给出的值）。
如何声明一个由未知值初始化的变量？
文档建议 if :: p = 0 :: p = 1 fi 但我不认为
它有效：Spin 仍然验证此声明
bit p
init { if :: p = 0 :: p = 1 fi }
ltl { ! p }
（并伪造 p）
那么 init 的语义到底是什么？还是有的
"pre-initial"状态？我怎样才能解决这个问题 - 而不是让我的学生感到困惑？
这是一个有趣的问题。
documentation 表示每个变量都初始化为 0，除非模型另有说明。
As with all variable declarations, an explicit initialization field is optional. The default initial value for all variables is zero. This applies both to scalar variables and to array variables, and it applies to both global and to local variables.
在您的模型中，您在声明变量时并未对其进行初始化，因此随后将其分配给初始状态下的值 0，该值位于您赋值之前：
bit p
init {
// THE INITIAL STATE IS HERE
if
:: p = 0
:: p = 1
fi
}
ltl { ! p }
一些实验。
"naive" 一个避免此限制的想法是修改 c 源代码 pan.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
}
并在 header 部分添加一个 #include <time.h>。
但是，一旦您使用 gcc pan.c 将其编译成验证器并尝试 运行 它，您将获得 non-deterministic 行为 取决于变量的初始化值 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 模型 的 初始状态 被 spin 验证为是独一无二的。 毕竟，这是一个合理的假设，因为它会不必要地使事情复杂化：您总是可以用初始状态 S s.t 替换 N 个不同的初始状态 S_i。 S 允许使用 epsilon-transition 到达每个 S_i。在这种情况下，您得到的并不是真正的 epsilon-transition，但在实践中几乎没有区别。
编辑 （来自评论）： 原则上，可以通过稍微进一步修改 pan.c 来完成这项工作：
- 将初始状态初始化器转换为初始状态 的生成器
- 修改验证例程以考虑可能存在多个初始状态，并且 属性 必须对每个初始状态成立
话虽如此，这可能不值得麻烦，除非这是通过修补 Spin 的源代码来完成的。
解决方法。
如果你想声明某事在初始状态下为真，或者从初始状态开始，并考虑到一些non-deterministic行为，那么你应该写如下内容：
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 只是保证是 生成的第一个进程 ，并且意味着 用于生成other processes when, for-example, other routines 输入一些参数, 例如一些资源是共享的。更多信息 here.
我认为 documentation 的这个片段有点误导：
The init process is most commonly used to initialize global variables, and to instantiate other processes, through the use of the run operator, before system execution starts. Any process, not just the init process, can do so, though
由于可以使用 atomic { } 语句保证 init 进程在任何其他进程之前执行其所有代码，因此可以说它可以从编程的角度，用于在变量被其他进程使用之前初始化变量。但这只是一个粗略的近似，因为init进程并不对应执行模型中的唯一状态，而是对应于树根状态，根本身仅由 全局环境 给出，就像在任何进程启动之前一样。