MyersResearchGroup / ATACS

Apache License 2.0
9 stars 1 forks source link

Interleave Optimization Issue #25

Open buggsley opened 8 years ago

buggsley commented 8 years ago

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

It appears that the interleave command may be removing reachable states. This issue was reveled running the regression test as follows:

make Extras=mT

The Extras=mT flag toggles the interleave optimization off. The PRS missmatch was found on the file go.csp. The go.prs file generated without the interleave option has a CSC variable to solve a violation that does not appear when interleave is turned on. This file has appended the bad PRS file with the GOLD file, as well as atacs.log for the run.

egm


Eric G Mercer eemercer@elen.utah.edu MEB 4120 Dept. Electrical Engineering Office: 801-581-8378 University of Utah FAX: 801-581-5281 Salt Lake City, UT 84112 ID: 0x4340C2D9 eemercer@elen.utah.edu Finger Print: C2B3 329C D759 3651 66CD 48D3 605D 32AC 4340 C2D9

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.0.2 (GNU/Linux) Comment: For info see http://www.gnupg.org

iD8DBQE5mcqfYF0yrENAwtkRAsrUAKCAWGPUAY1yns5ZJWs5OPFwdbMWgACZAbzM qO+x3beH+2K2CX66gj7W0dM= =i24D -----END PGP SIGNATURE-----

buggsley commented 8 years ago

It appears actually that the interleave optimization is saving the day here. Without it, it gets a CSC violation because states appear which shouldn't. POSETS, BAP, and Geometric agree. Since interleave is default moving to potential problem.

buggsley commented 8 years ago

The original message was received at Sun, 21 Apr 2002 16:11:49 -0600 from IDENT:atacs-bugs@shang.elen.utah.edu [155.99.23.201]

----- The following addresses had permanent fatal errors ----- eemercer@elen.utah.edu (reason: 551 5.1.1 User has moved; please try eemercer@ece.utah.edu)

----- Transcript of session follows ----- ... while talking to mail.elen.utah.edu.:

RCPT To:eemercer@elen.utah.edu <<< 551 5.1.1 User has moved; please try eemercer@ece.utah.edu 550 5.1.1 eemercer@elen.utah.edu... User unknown