Re: ARC model specified in spinroot/promela

[...]


>       spinmodel.pml:80, state 28, "D_STEP80"
>       spinmodel.pml:80, state 53, "D_STEP80"
>       spinmodel.pml:154, state 70, "B1.item_list?_"
>       spinmodel.pml:80, state 79, "D_STEP80"
>       spinmodel.pml:90, state 85, "D_STEP90"
>       spinmodel.pml:78, state 86,
>(((len(T1.item_list)!=0)&&((len(T1.item_list)>p)||(B2.item_list??[eval(x[x_iid].iid)]&&(len(T1.item_list)==p)))))"
>       spinmodel.pml:78, state 86, "else"
>       spinmodel.pml:73, state 88, "D_STEP73"
>       spinmodel.pml:159, state 90, "assert((len(B1.item_list)==0))"
>       spinmodel.pml:160, state 94, "D_STEP160"
>       spinmodel.pml:152, state 95, "((len(T1.item_list)<64))"
>       spinmodel.pml:152, state 95, "else"
>       spinmodel.pml:183, state 100, "B2.item_list?_"
>       spinmodel.pml:198, state 128, "(1)"
>       spinmodel.pml:268, state 155, "-end-"
>       (13 of 155 states)

[...]

These correspond to "Case A" in arc.pml, which were never entered
because the driver file wasn't able to create the right sequence to
exercise those code paths. I'll look at this later - as this is an
illustrative project, it may even make sense to just find an input
"trace" as an input array that is guaranteed to make the state machine
enter all paths.

Thanks for the confirmation trace!
-- 
~cherry