Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-04 17:26:28

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

Offline

#2 2011-11-04 19:52:51

spinroot
forum
Registered: 2010-11-18
Posts: 678
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)

Offline

Board footer

Powered by FluxBB