Visualizing the counter-example of an assertion violation

Dharma · 2011-09-21 17:31:04

Hi,

Tried spin on the model given below. It reported a violation of the assertion. Is there a way to see the actual interleaving that led to this violation?

byte n = 0, finish = 0;

active [2] proctype P() {
byte register, counter = 0;
do :: counter = 10 -> break
:: else ->
register = n;
register++;
n = register;
counter++
od;
finish++
}

active proctype WaitForFinish() {
finish == 2;
assert (n > 0);
}

Tried spin -s -t primer.pml and got this output. It appears n = 0. But not clear to me what interleaving has led to this failure. Any comments? Thank a lot.

-----
spin: primer.pml:17, Error: assertion violated
spin: text of failed assertion: assert((n>0))
spin: trail ends after 6 steps
#processes: 3
n = 0
finish = 2
6: proc 2 (WaitForFinish) primer.pml:18 (state 3) <valid end state>
6: proc 1 (P) primer.pml:13 (state 12) <valid end state>
6: proc 0 (P) primer.pml:13 (state 12) <valid end state>
3 processes created

---

spinroot · 2011-09-21 23:41:50

try: spin -p -t primer.pml
or even more verbose:
spin -p -g -l -v -t primer.pml

Dharma · 2011-09-23 23:43:10

Thanks. Tried it. It is mind-boggling to see the assertion violation. It is still unclear to me how come n is 0 when finish is 2. Any comment?

The output I got

ubuntu@ubuntu10:~/Downloads/Spin/iSpin/ltl_examples$ spin -p -g -l -v -t primer.pml

spin: warning, primer.pml, proctype P, 'byte counter' variable is never used
i=3 pno 1
1: proc 1 (P) primer.pml:5 (state 1) [counter = 10]
P(1):counter = 10
i=3 pno 0
2: proc 0 (P) primer.pml:5 (state 1) [counter = 10]
P(0):counter = 10
i=3 pno 1
3: proc 1 (P) primer.pml:12 (state 11) [finish = (finish+1)]
finish = 1
i=3 pno 0
4: proc 0 (P) primer.pml:12 (state 11) [finish = (finish+1)]
finish = 2
i=3 pno 2
5: proc 2 (WaitForFinish) primer.pml:16 (state 1) [((finish==2))]
i=3 pno 2
spin: primer.pml:17, Error: assertion violated
spin: text of failed assertion: assert((n>0))
6: proc 2 (WaitForFinish) primer.pml:17 (state 2) [assert((n>0))]
spin: trail ends after 6 steps
#processes: 3
n = 0
finish = 2
6: proc 2 (WaitForFinish) primer.pml:18 (state 3) <valid end state>
6: proc 1 (P) primer.pml:13 (state 12) <valid end state>
6: proc 0 (P) primer.pml:13 (state 12) <valid end state>
3 processes created

spinroot · 2011-09-24 00:01:31

n is initially zero and not modified in this counter-example trail
so it is still zero at the time that the assertion is evaluated

instead of "counter = 10" in the first two processes, you probably meant to say "counter == 10"

Dharma · 2011-09-24 00:40:34

Ha ha, it was a typo in the ACM Inroads: " A Primer on Model Checking" by Mordechai (Moti) Ben-Ari, see page 44

Yes, counter == 10 not counter = 10.

Thanks!

benari · 2011-11-09 08:56:57

> A typo in the ACM Inroads: " A Primer on Model Checking" by Mordechai (Moti) Ben-Ari
> page 44: counter == 10 not counter = 10

Correct, this is a typo.
My apologies.

Moti

Spinroot

#1 2011-09-21 17:31:04

Visualizing the counter-example of an assertion violation

#2 2011-09-21 23:41:50

Re: Visualizing the counter-example of an assertion violation

#3 2011-09-23 23:43:10

Re: Visualizing the counter-example of an assertion violation

#4 2011-09-24 00:01:31

Re: Visualizing the counter-example of an assertion violation

#5 2011-09-24 00:40:34

Re: Visualizing the counter-example of an assertion violation

#6 2011-11-09 08:56:57

Re: Visualizing the counter-example of an assertion violation

Board footer