Date: Wed, 06 Sep 2023 11:36:18 +0000 From: "Mathew\, Cherry G.*" <c@bow.st> To: Alexander Leidinger <Alexander@Leidinger.net> Cc: adridg@freebsd.org, freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela Message-ID: <85bkefh6tp.fsf@bow.st> In-Reply-To: <1e3a17e39094a9630eebce9f91f00e30@Leidinger.net> (Alexander Leidinger's message of "Mon, 04 Sep 2023 21:47:27 %2B0200") References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st> <c2197ad9446eca4edae2db09a859d66b@Leidinger.net> <85pm304dzi.fsf@bow.st> <85a5u22oxx.fsf@bow.st> <1e3a17e39094a9630eebce9f91f00e30@Leidinger.net>
next in thread | previous in thread | raw e-mail | index | archive | help
[...] > 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?85bkefh6tp.fsf>