Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-04 19:11:30

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

Offline

#2 2011-11-04 19:40:58

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

Offline

Board footer

Powered by FluxBB