如何在Spin中创建未初始化的变量? [英] how to make a non-initialised variable in Spin?
问题描述
似乎Promela初始化了每个变量(默认情况下为0或声明中给定的值).
It seems that Promela initialises each variable (by default, to 0, or to the value that is given in the declaration).
如何声明由未知值初始化的变量?
How can I declare a variable that is initialised by an unknown value?
文档建议使用if :: p = 0 :: p = 1 fi，但我认为
可行:Spin仍会验证此声明
The documentation suggests if :: p = 0 :: p = 1 fi but I don't think
that it works: Spin still verifies this claim
bit p
init { if :: p = 0 :: p = 1 fi }
ltl { ! p }
(并伪造p)
那么init的语义到底是什么?还有一些
预初始"状态?我该如何解决-不要让我的学生感到困惑?
So what exactly is the semantics of init? There still is some
"pre-initial" state? How can I work around this - and not confuse my students?
推荐答案
这是一个有趣的问题.
文档指出，每个变量都初始化为0，除非型号另有规定.
The documentation says that each and every variable is initialised to 0, unless the model specifies otherwise.
与所有变量声明一样，显式初始化字段是可选的.所有变量的默认初始值为零.这适用于标量变量和数组变量，也适用于全局变量和局部变量.
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，该状态位于赋值之前:
In your model, you don't initialise the variable when you declare it, therefore it is subsequently assigned to the value 0 in the initial state, which is located before your assignment:
bit p
init {
// THE INITIAL STATE IS HERE
if
:: p = 0
:: p = 1
fi
}
ltl { ! p }
一些实验.
避免这种限制的天真" 想法是修改通过旋转生成的 pan.c 的 c源代码当您调用~$ spin -a test.pml时，该变量将被随机初始化.
A "naive" idea for dodging this limitation would be to modify the c source code of pan.c that is generated by spin when you invoke ~$ spin -a test.pml, so that the variable is initialised at random.
代替此初始化功能:
void
iniglobals(int calling_pid)
{
now.p = 0;
#ifdef VAR_RANGES
logval("p", now.p);
#endif
}
一个人可以尝试这样写:
one could try writing this:
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 .
However, once you compile that into a verifier with gcc pan.c, and you attempt to run it, you obtain non-deterministic behaviour depending on the initialization value of the variable p.
它都可以确定该属性被违反:
It can both determine that the property is violated:
~$ ./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
或打印该属性是否满足:
or print that the property is satisfied:
~$ ./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 s.t替换N个不同的初始状态S_i. S允许以ε跃迁到达每个S_i.在这种情况下，您获得的并不是真正的epsilon过渡，但实际上并没有什么区别.
Clearly, the initial state of a promela model verified by spin is assumed to be unique. Afterall, that's a reasonable assumption, since it would needlessly complicate things: you can always replace N different initial states S_i with an initial state S s.t. S allows to reach each S_i with an epsilon-transition. In this context, what you get is not truly an epsilon-transition, but in practice it makes little difference.
编辑 (摘自评论): 原则上，可以通过进一步修改 pan.c 来完成这项工作:
EDIT (from comments): In principle, it is possible to make this work by modifying pan.c a little bit further:
- 将初始状态 initializer 转换为初始状态的生成器
- 修改验证例程，以考虑可能存在多个初始状态，并且该属性必须针对每个初始状态都保持不变
- transform the initial state initialiser into a generator of initial states
- modify the verification routine to take into account that more than one initial state might exist, and that the property must hold for each initial state
话虽如此，除非通过修补 Spin 的源代码来做到这一点，否则可能不值得麻烦.
Having said this, it is likely not worth the hassle, unless this is done by patching Spin's source code.
解决方法.
如果要声明在初始状态或从初始状态开始是正确的，并且考虑到某些不确定性行为，则应编写以下内容:
If you want to state that something is true in the initial state, or starting from the initial state, and take into account some non-deterministic behaviour, then you should write something as follows:
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 is simply guaranteed to be the first process to spawn, and is meant to be used for spawning other processes when, for-example, the other routines take as input some parameters, e.g. some resources are shared. More info here.
我相信文档的片段有点误导:
初始化过程最常用于初始化全局变量， 并通过运行实例化其他流程 操作员，开始执行系统之前.任何过程，而不仅仅是 初始化过程可以做到，尽管
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进程在执行任何其他进程之前先执行所有代码，因此可以说它可以用于在变量被初始化之前对其进行初始化.从编程角度来看由其他进程使用.但这只是一个粗略的近似值，因为初始化过程并不对应于执行模型中的唯一状态 ，而是对应于根目录和状态树中的状态树.根本身仅由全局环境给出，就像在任何进程开始之前一样.
Since it is possible to guarantee that the init process executes all of its code before any other process using the atomic { } statement, one could say that it can be used to initialize variables before they are used by other processes from the programming point of view. But that is just a rough approximation, because the init process does not correspond to a unique state in the execution model, but rather to the tree of states at the root and the root itself is given only by the global environment as it is before any process starts.
这篇关于如何在Spin中创建未初始化的变量?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
