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.

Please help me .

inline test_and_set(addr, old) {
    old = addr;
    addr = 1;
byte lock;
active [2] proctype proc(){
  byte old;
  :: true ->
      test_and_set(lock, old);
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
    lock = 0;

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.


  • $\begingroup$ It may simply be a precedence problem: $\neg A U B$ gets parsed as $\neg (A U B)$. Try $(\neg A) U B$ instead. $\endgroup$ – Klaus Draeger Apr 15 '17 at 11:05
  • $\begingroup$ So, do you mean that spin should find a counterexample for my formula? So, what is correct interpretation of that? $\endgroup$ – user68041 Apr 15 '17 at 13:05
  • 1
    $\begingroup$ I would need to see the actual Promela program you used. $\endgroup$ – Klaus Draeger Apr 15 '17 at 15:34
  • $\begingroup$ I've edited. :) $\endgroup$ – user68041 Apr 15 '17 at 20:15
  • $\begingroup$ 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. $\endgroup$ – chi Apr 15 '17 at 21:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy