Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-19 02:25:42

koike
Member
Registered: 2010-12-14
Posts: 2

number of inline LTL formulae

If I specify more than 255 LTL formulae inside a verification model, 255th and later LTL cannot be checked by 'pan -N'.
I suppose this is because the size of 'spin_c_typ' generated by pangen1.c is 'uchar'.
I edited pan.h to change the size of 'spin_c_typ' to 'uint', 255th and later LTL could be checked.

Offline

#2 2012-04-19 03:09:29

spinroot
forum
Registered: 2010-11-18
Posts: 678
Website

Re: number of inline LTL formulae

Interesting -- but really, you needed more than 255 ltl formula...?

Offline

#3 2012-04-19 04:05:30

koike
Member
Registered: 2010-12-14
Posts: 2

Re: number of inline LTL formulae

Yes. We developed and using a tool to auto-generate promela and LTLs from state transition table (state-event matrix).
When the table is large, hundreds of LTLs to check state/transition coverage will be generated.

Offline

#4 2012-04-20 05:11:25

spinroot
forum
Registered: 2010-11-18
Posts: 678
Website

Re: number of inline LTL formulae

you can also do this a few ltl formula at a time (say 100 ....)
and then move on after you've checked those, move on to the next set of 100...

Offline

Board footer

Powered by FluxBB