# Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state.

(0) $\neg A, \neg B$

(1) $\neg A, B$

(2) $A, \neg B$

$\square$ means that for every state in computation the formula $\neg A \cup B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $\cup$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

inline test_and_set(addr, old) {
d_step{
}
}
byte lock;
active [2] proctype proc(){
byte old;
do
:: true ->
wait:
test_and_set(lock, old);
do
:: old != 0 -> test_and_set(lock, old);
:: else -> break;
od
cs:
lock = 0;
od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)


And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

• It may simply be a precedence problem: $\neg A U B$ gets parsed as $\neg (A U B)$. Try $(\neg A) U B$ instead. – Klaus Draeger Apr 15 '17 at 11:05
• So, do you mean that spin should find a counterexample for my formula? So, what is correct interpretation of that? – user68041 Apr 15 '17 at 13:05
• I would need to see the actual Promela program you used. – Klaus Draeger Apr 15 '17 at 15:34
• I've edited. :) – user68041 Apr 15 '17 at 20:15
• Note that you are using the weak until operator W instead of the strong until U. p W q does not require q being eventually true. – chi Apr 15 '17 at 21:00