number of inline LTL formulae

koike · 2012-04-19 02:25:42

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.

spinroot · 2012-04-19 03:09:29

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

koike · 2012-04-19 04:05:30

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.

spinroot · 2012-04-20 05:11:25

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

Spinroot

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

number of inline LTL formulae

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

Re: number of inline LTL formulae

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

Re: number of inline LTL formulae

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

Re: number of inline LTL formulae

Board footer