Spinroot

A forum for Spin users

You are not logged in.

#1 2012-12-13 11:23:03

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?

Offline

#2 2012-12-13 14:58:58

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).

Offline

#3 2012-12-13 17:43:44

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)

Offline

Board footer

Powered by FluxBB