Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-07 14:15:56

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

_nr_pr in ltl clause

When the following ltl clause is added to a Promela model:

ltl { <>[] (_nr_pr == 1) }

SPIN 6.0.1 (i.e., spin -a) issues the following error message:

ltl ltl_0: <> ([] ((nr_pr==1)))
spin: _spin_nvr.tmp:3, Error: undeclared variable: nr_pr    saw 'operator: =='

The leading _ of _nr_pr seems to be lost.

When the parentheses around _nr_pr == 1 are removed, SPIN gets even more confused and regards _nr_pr as a constant. The following never claim is then generated:

$ cat _spin_nvr.tmp 
never ltl_0 {    /* !((328==1)) */
accept_init:
T0_init:
    if
    :: (! (((328==1)))) -> goto accept_all
    fi;
accept_all:
    skip
}

Offline

#2 2011-02-07 17:51:43

spinroot
forum
Registered: 2010-11-18
Posts: 700
Website

Re: _nr_pr in ltl clause

yes, confirmed -- it will be fixed in the next release of spin
thanks for the bug report

Offline

Board footer

Powered by FluxBB