Spinroot

KeesPronk

Member

Registered: 2011-01-04

Posts: 12

spin compiler hangs on complex ltl expression

When doing 'spin -a p3c.pml' on the following (not so useful) program, the spin compiler seems to hang.

bool p;
bool q;
bool z;

ltl p3c {p V q V z W q W q W z}

init{skip;}

Kees Pronk
// Problem detected while working on the Epispin environment

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: spin compiler hangs on complex ltl expression

this one is just an issue of complexity.
the tool just churns on this forever, because it expands so much
simplifying the formula (or shortening it) will help