A forum for Spin users
You are not logged in.
Pages: 1
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
Pages: 1