From nobody Wed Sep 6 11:36:18 2023 X-Original-To: freebsd-hackers@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4RggMX0Qd3z4sRqM for ; Wed, 6 Sep 2023 11:37:12 +0000 (UTC) (envelope-from c@bow.st) Received: from comms.drone (in.bow.st [71.19.146.166]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 4RggMV3BQjz4XYW; Wed, 6 Sep 2023 11:37:10 +0000 (UTC) (envelope-from c@bow.st) Authentication-Results: mx1.freebsd.org; dkim=none; spf=pass (mx1.freebsd.org: domain of c@bow.st designates 71.19.146.166 as permitted sender) smtp.mailfrom=c@bow.st; dmarc=none Received: from homebase (unknown [IPv6:fe80::ff1d:976a:a7e4:ee6a]) by comms.drone (Postfix) with ESMTPSA id B1735FCDC; Wed, 6 Sep 2023 11:36:53 +0000 (UTC) From: "Mathew\, Cherry G.*" To: Alexander Leidinger Cc: adridg@freebsd.org, freebsd-hackers@freebsd.org Subject: Re: ARC model specified in spinroot/promela References: <85jzt96qjz.fsf@bow.st> <9c424a574cdd39fc879c9ed9192556c0@Leidinger.net> <858r9o6ee0.fsf@bow.st> <85pm304dzi.fsf@bow.st> <85a5u22oxx.fsf@bow.st> <1e3a17e39094a9630eebce9f91f00e30@Leidinger.net> Date: Wed, 06 Sep 2023 11:36:18 +0000 In-Reply-To: <1e3a17e39094a9630eebce9f91f00e30@Leidinger.net> (Alexander Leidinger's message of "Mon, 04 Sep 2023 21:47:27 +0200") Message-ID: <85bkefh6tp.fsf@bow.st> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (berkeley-unix) List-Id: Technical discussions relating to FreeBSD List-Archive: https://lists.freebsd.org/archives/freebsd-hackers List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-freebsd-hackers@freebsd.org MIME-Version: 1.0 Content-Type: text/plain X-Spamd-Bar: / X-Spamd-Result: default: False [-0.19 / 15.00]; HFILTER_HELO_IP_A(1.00)[comms.drone]; NEURAL_HAM_LONG(-0.99)[-0.993]; NEURAL_HAM_SHORT(-0.97)[-0.974]; NEURAL_SPAM_MEDIUM(0.68)[0.681]; HFILTER_HELO_NORES_A_OR_MX(0.30)[comms.drone]; R_SPF_ALLOW(-0.20)[+mx]; MIME_GOOD(-0.10)[text/plain]; ONCE_RECEIVED(0.10)[]; TO_DN_SOME(0.00)[]; R_DKIM_NA(0.00)[]; FROM_EQ_ENVFROM(0.00)[]; MIME_TRACE(0.00)[0:+]; RCVD_TLS_ALL(0.00)[]; ASN(0.00)[asn:47066, ipnet:71.19.146.0/24, country:US]; FROM_HAS_DN(0.00)[]; MLMMJ_DEST(0.00)[freebsd-hackers@freebsd.org]; ARC_NA(0.00)[]; RCPT_COUNT_THREE(0.00)[3]; RCVD_COUNT_ONE(0.00)[1]; DMARC_NA(0.00)[bow.st]; TO_MATCH_ENVRCPT_SOME(0.00)[]; MID_RHS_MATCH_FROM(0.00)[]; RCVD_VIA_SMTP_AUTH(0.00)[] X-Rspamd-Queue-Id: 4RggMV3BQjz4XYW [...] > 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