A forum for Spin users
You are not logged in.
Pages: 1
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.
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.
Pages: 1