I am trying to understand why the assert in this model isn't triggered.
ltl { !A@wa U B@sb && !B@wb U A@sa }
byte p = 0
byte q = 0
int x = 0
inline signal(sem) { sem++ }
inline wait (sem) { atomic { sem > 0 ; sem-- } }
proctype A() {
x = 10*x + 1
signal(p)
sa: wait(q)
wa: x = 10*x + 2
}
proctype B() {
x = 10*x + 3
signal(q)
sb: wait(p)
wb: x = 10*x + 4
}
init {
atomic { run A(); run B() }
_nr_pr == 1
assert(x != 1324)
}
Clearly, there is an order of operations that produces the final value x = 1324
:
- Initially
x = 0
A
setsx = 10*0 + 1 = 1
B
setsx = 10*1 + 3 = 13
A
andB
allow each other to proceedA
setsx = 10*13 + 2 = 132
B
setsx = 10*132 + 4 = 1324
The assertion isn't triggered because it is "never reached" when the solver proves that the property
is true.
Take a look at the output that is given by the solver, it clearly states that:
it is checking any assertion, but only if within the scope of the claim:
the assertion isn't reached:
You can use the option
-noclaim
so to check the model only for the assertion, which is then easily proven false: