promela - 如何在 Promela 中以非原子方式对布尔 AND 评估进行建模？

Question

如何以非原子方式在 Promela 中对布尔 AND 评估进行建模？

我想为语句建模while (flag[j] == true && victim == i)应该以非原子方式进行 AND 评估的语句进行建模。

这怎么可能？

Answer 1

loop:
if 
:: flag[j] != true -> goto done
:: else
fi;

if 
:: victim != i -> goto done
:: else
fi;

/* body of 'while' */

goto loop;
done:

/* after 'while' */

请注意，虽然我面前没有 Spin 环境，但是是什么让您认为条件首先是原子的？我会用类似的东西进行测试：

byte i = 0

i++ >= 0 && i-- >= 0

never { assert (1 == i) } 

但是，无论哪种方式，上面的第一个代码都显示了如何在需要时使其成为非原子的。