Spinroot

medmuf

Member

Registered: 2012-12-11

Posts: 6

Spin doesn't halt on specified ltl property

The minimum way to reproduce this case:
init{
  skip
}
#define fair_run (([]<> (_last == 3)) && ([]<> (_last == 4)) && ([]<> (_last == 5)) && ([]<> (_last == 6)))
ltl fr {!fair_run }

Is my ltl specified in a wrong way?

medmuf

Member

Registered: 2012-12-11

Posts: 6

Re: Spin doesn't halt on specified ltl property

Sorry to disturb. This minimum example finally compiled and it spent some time to generate the automata (with 3122 lines, 170082 characters).

spinroot

forum

Registered: 2010-11-18

Posts: 694

Website

Re: Spin doesn't halt on specified ltl property

This is a good example of a 'separable' property.
Instead of trying to prove all 4 clauses in a single run,
split them up and prove them separately,,,,
(generates the never claim much faster)