Spinroot

KeesPronk

Member

Registered: 2011-01-04

Posts: 12

strange error message from ltl-clause

The following program, when translated with spin -a p7.pml

byte p;
byte q;

ltl p7 {p equivalent q}
ltl p7a {p <-> q}

init{skip;}

will give the following unexpected error message:

ltl p7: (p) <-> (q)
ltl p7a: (p) <-> (q)
spin: _spin_nvr.tmp:4, Error: syntax error    saw ';'
spin: _spin_nvr.tmp:13, Error: syntax error    saw ';'
spin: p7.pml:18, Error: proctype p7a not found

Kees

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: strange error message from ltl-clause

the problem is that the new parser for inline ltl expressions does not
recognize the operator <-> (or its equivalent 'equivalent').
will be fixed in the next release
for now, looks like you'll have to specify this as (p -> q) && (q -> p)
(or use spin -f to do the conversion into a never claim, instead of an inline ltl formula)