这会是死锁的一个例子吗？
active proctype test(){
bool one;
byte x;
one;
x = x+11;
}
IMHO，编号
遵循维基百科所示的死锁的必要条件列表：
当且仅当以下条件在系统中同时成立：
互斥：必须在不可共享模式。否则，这些过程将不会被阻止避免在必要时使用资源。只有一个进程可以使用资源。
等待或资源持有：进程当前至少持有一个资源，并且请求其他人持有的额外资源过程。
没有抢占权：资源只能自愿释放
循环等待：每个进程都必须等待对于另一个进程所持有的资源正在等待第一个进程释放资源。一般来说存在一组等待过程，P={P1，P2，…，PN}，使得P1正在等待P2持有的资源，P2正在等待资源由P3保持，依此类推，直到PN正在等待由P1.
这四个条件被称为Coffman条件，这是Edward G.Coffman在1971年的一篇文章中首次描述的，Jr.
您的模型包括一个永远挂起的进程，但没有共享资源，没有其他进程持有它，没有循环等待等等。换句话说，它只是一个在无限长的时间内没有任何可执行的进程，因为默认情况下为one分配false，并且在Promela中评估CCD_ 3的表达总是被阻断。
下面是一个简单的死锁示例，取自今年早些时候在特伦托大学举行的讲座"Spin:Introduction"。
文件：mutex_simple_flaw2.pml
bit x, y;
byte cnt;
active proctype A() {
again:
x = 1;
y == 0; /* waits for process B to end: if y != 0, the execution of this
statement is blocked here */
cnt++;
/* critical section */
printf("Process A entered critical section.n");
assert(cnt == 1);
cnt--;
printf("Process A exited critical section.n");
x = 0;
goto again
}
active proctype B() {
again:
y = 1;
x == 0;
cnt++;
/* critical section */
printf("Process B entered critical section.n");
assert(cnt == 1);
cnt--;
printf("Process B exited critical section.n");
y = 0;
goto again
}
当进程A和B"同时">执行指令x = 1和y = 1时，此模型会出现死锁。
以下验证搜索表明存在无效结束状态，该状态对应于满足所有Coffman条件的执行跟踪：
~$ spin -search -bfs mutex_simple_flaw2.pml
pan:1: invalid end state (at depth 2)
pan: wrote mutex_simple_flaw2.pml.trail
(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
+ Breadth-First Search
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 20 byte, depth reached 2, errors: 1
8 states, stored
8 nominal states (stored-atomic)
1 states, matched
9 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)
128.195 total actual memory usage
pan: elapsed time 0 seconds
Spin发现的有问题的执行跟踪如下：
~$ spin -t -p -g -l mutex_simple_flaw2.pml
using statement merging
1: proc 1 (B:1) mutex_simple_flaw2.pml:24 (state 1) [y = 1]
y = 1
2: proc 0 (A:1) mutex_simple_flaw2.pml:7 (state 1) [x = 1]
x = 1
3: proc 0 (A:1) mutex_simple_flaw2.pml:8 (state 2) [((y==0))]
transition failed
spin: trail ends after 3 steps
#processes: 2
x = 1
y = 1
cnt = 0
3: proc 1 (B:1) mutex_simple_flaw2.pml:25 (state 2)
3: proc 0 (A:1) mutex_simple_flaw2.pml:8 (state 2)
2 processes created
您的模型也会导致"无效结束状态">。然而，这并不意味着它一定是死锁，它只意味着执行跟踪在进程到达其代码块的末尾之前终止。根据建模的系统，这并不总是一个实际问题。