From david@mcs.vuw.ac.nz Fri Sep 2 03:18:26 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j82AIQse029540 for ; Fri, 2 Sep 2005 03:18:26 -0700 (PDT) (envelope-from david@mcs.vuw.ac.nz) X-Original-Received: from mailgate-external2.sri.com (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id j82AIMtk013945 for ; Fri, 2 Sep 2005 03:18:22 -0700 (PDT) (envelope-from david@mcs.vuw.ac.nz) X-Original-Received: from localhost (HELO mailgate-external2.SRI.COM) (127.0.0.1) by mailgate-external2.sri.com with SMTP; 2 Sep 2005 10:18:21 -0000 X-Original-Received: from kaukau.mcs.vuw.ac.nz ([130.195.5.20]) by mailgate-external2.SRI.COM (SMSSMTP 4.0.5.66) with SMTP id M2005090203181425814 for ; Fri, 02 Sep 2005 03:18:21 -0700 X-Original-Received: from 202-154-135-39-palmerston-nth.connections.net.nz (202-154-135-39-palmerston-nth.connections.net.nz [202.154.135.39]) (authenticated bits=0) by kaukau.mcs.vuw.ac.nz (8.13.4/8.12.11) with ESMTP id j82AI8Tl024258 (version=TLSv1/SSLv3 cipher=RC4-MD5 bits=128 verify=NOT) for ; Fri, 2 Sep 2005 22:18:12 +1200 (NZST) From: David Friggens To: sal-help@csl.sri.com Subject: Re: [SAL-HELP] "implements" assertions Date: Fri, 2 Sep 2005 22:18:57 +1200 User-Agent: KMail/1.8.2 References: <200509012025.59187.david@mcs.vuw.ac.nz> <9C2E00E6-DC64-44CE-B9AA-C4F15E58887E@csl.sri.com> In-Reply-To: <9C2E00E6-DC64-44CE-B9AA-C4F15E58887E@csl.sri.com> MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200509022218.58026.david@mcs.vuw.ac.nz> X-Greylist: Sender succeeded SMTP AUTH authentication, not delayed by milter-greylist-2.0 (kaukau.mcs.vuw.ac.nz [130.195.5.20]); Fri, 02 Sep 2005 22:18:12 +1200 (NZST) X-Scanned-By: MIMEDefang 2.52 on 130.195.5.20 X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Fri, 02 Sep 2005 03:18:29 -0700 X-Mailman-Approved-At: Fri, 02 Sep 2005 16:20:16 -0700 X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 02 Sep 2005 10:18:29 -0000 Hi Leonardo > Unfortunately, none of the current tools implement the keywords: > IMPLEMENTS and REFINES. Thanks for letting me know. Is there a plan to implement them in the near future? Cheers David From demoura@csl.sri.com Fri Sep 2 16:29:34 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j82NTYse046357 for ; Fri, 2 Sep 2005 16:29:34 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j82NTYNc083887; Fri, 2 Sep 2005 16:29:34 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: <200509022218.58026.david@mcs.vuw.ac.nz> References: <200509012025.59187.david@mcs.vuw.ac.nz> <9C2E00E6-DC64-44CE-B9AA-C4F15E58887E@csl.sri.com> <200509022218.58026.david@mcs.vuw.ac.nz> Mime-Version: 1.0 (Apple Message framework v734) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] "implements" assertions Date: Fri, 2 Sep 2005 16:29:46 -0700 To: David Friggens X-Mailer: Apple Mail (2.734) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Fri, 02 Sep 2005 16:29:38 -0700 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 02 Sep 2005 23:29:38 -0000 Hi David, > Thanks for letting me know. Is there a plan to implement them in the > near future? We plan to implement it, but not this year. Right now, we are planning to release a better sal-inf-bmc that is more efficient and produce "concrete" counterexamples. We are also working in an explicit state model checker for SAL. Cheers, Leonardo. From rushby@csl.sri.com Fri Sep 2 16:33:24 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j82NXNse046492 for ; Fri, 2 Sep 2005 16:33:23 -0700 (PDT) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (muon.csl.sri.com [130.107.15.116]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j82NXNDP084395 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Fri, 2 Sep 2005 16:33:23 -0700 (PDT) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (localhost.localdomain [127.0.0.1]) by muon.csl.sri.com (8.13.1/8.13.1) with ESMTP id j82NXNgt029541; Fri, 2 Sep 2005 16:33:23 -0700 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id j82NXNV7029540; Fri, 2 Sep 2005 16:33:23 -0700 Date: Fri, 2 Sep 2005 16:33:23 PDT From: John Rushby To: David Friggens Subject: Re: [SAL-HELP] "implements" assertions In-Reply-To: Your message of Fri, 2 Sep 2005 22:18:57 +1200 Message-ID: X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.000 autolearn=no version=2.64 date=Fri, 02 Sep 2005 16:33:25 -0700 X-Mailman-Approved-At: Fri, 02 Sep 2005 16:34:16 -0700 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 02 Sep 2005 23:33:25 -0000 > Thanks for letting me know. Is there a plan to implement them in the > near future? Not in the near future. Depending on exactly what you want, you might be able to fake it: e.g., suppose Abstract and Concrete are deterministic modules that take the same inputs; package their state variables up into tuples A and C respectively, then model check for G(abs(C) = A) where abs is the abstraction function. PVS does do theory interpretations (on the other hand, it doesn't know about state machines). John From demoura@csl.sri.com Tue Sep 20 10:06:28 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j8KH6S6H078937 for ; Tue, 20 Sep 2005 10:06:28 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.3] (ovc-160.csl.sri.com [130.107.97.160]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j8KH889s093060; Tue, 20 Sep 2005 10:08:10 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v734) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: Content-Transfer-Encoding: 7bit From: Leonardo de Moura Date: Tue, 20 Sep 2005 10:08:27 -0700 To: Romulus Apolzan X-Mailer: Apple Mail (2.734) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Tue, 20 Sep 2005 10:06:37 -0700 Cc: sal-help@csl.sri.com Subject: [SAL-HELP] Re: Query about SAT solvers compatible with Mac OS X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 20 Sep 2005 17:06:37 -0000 Hi Romulus, > I've been trying to find at least one SAT solver ( Siege, Berkmin, > Zchaff, > Grasp) that is compatible with Mac OS Tiger, so that I could use it > together with sal-bmc. > > I wasn't able to find one that is compatible with Mac OS. > > Am I doing something wrong here? Is there a SAT solver (other than > ICS) compatible with Mac and usable with sal-bmc? The source code for zchaff is available on the internet. So, in principle, you can compile it on Mac OS X. On the siege website (http://www.cs.sfu.ca/~loryan/personal/), the author says it can provide binaries for other platforms if you ask him. BTW, Grasp is an old SAT solver and it is not competitive anymore. Cheers, Leonardo From rapolzan@turing.une.edu.au Mon Sep 19 18:10:14 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j8K1AD6H060345 for ; Mon, 19 Sep 2005 18:10:14 -0700 (PDT) (envelope-from rapolzan@turing.une.edu.au) X-Original-Received: from mailgate-external2.sri.com (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id j8K1Bmha085605 for ; Mon, 19 Sep 2005 18:11:48 -0700 (PDT) (envelope-from rapolzan@turing.une.edu.au) X-Original-Received: from localhost (HELO mailgate-external2.SRI.COM) (127.0.0.1) by mailgate-external2.sri.com with SMTP; 20 Sep 2005 01:11:48 -0000 X-Original-Received: from mailhub1.une.edu.au ([129.180.1.122]) by mailgate-external2.SRI.COM (SMSSMTP 4.0.5.66) with SMTP id M2005091918114732731 ; Mon, 19 Sep 2005 18:11:48 -0700 X-Original-Received: from turing.une.edu.au (turing.une.edu.au [129.180.11.17]) by mailhub1.une.edu.au (Postfix) with ESMTP id 89E817F55; Tue, 20 Sep 2005 11:11:46 +1000 (EST) X-Original-Received: from turing.une.edu.au (localhost.localdomain [127.0.0.1]) by turing.une.edu.au (8.12.10/8.12.10) with ESMTP id j8K1BkT2009405 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 20 Sep 2005 11:11:46 +1000 X-Original-Received: from localhost (rapolzan@localhost) by turing.une.edu.au (8.12.10/8.12.10/Submit) with ESMTP id j8K1BjMa009401; Tue, 20 Sep 2005 11:11:46 +1000 Date: Tue, 20 Sep 2005 11:11:45 +1000 (EST) From: Romulus Apolzan To: sal-help@csl.sri.com Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Mon, 19 Sep 2005 18:10:18 -0700 X-Mailman-Approved-At: Tue, 20 Sep 2005 10:06:48 -0700 Cc: sal-sri@csl.sri.com Subject: [SAL-HELP] Query about SAT solvers compatible with Mac OS X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 20 Sep 2005 01:10:18 -0000 Hello, I've been trying to find at least one SAT solver ( Siege, Berkmin, Zchaff, Grasp) that is compatible with Mac OS Tiger, so that I could use it together with sal-bmc. I wasn't able to find one that is compatible with Mac OS. Am I doing something wrong here? Is there a SAT solver (other than ICS) compatible with Mac and usable with sal-bmc? Thank you, Romulus. From rapolzan@turing.une.edu.au Tue Sep 20 19:22:11 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j8L2MB6H089669 for ; Tue, 20 Sep 2005 19:22:11 -0700 (PDT) (envelope-from rapolzan@turing.une.edu.au) X-Original-Received: from mailgate-external2.sri.com (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id j8L2NrEp009917 for ; Tue, 20 Sep 2005 19:23:54 -0700 (PDT) (envelope-from rapolzan@turing.une.edu.au) X-Original-Received: from localhost (HELO mailgate-external2.SRI.COM) (127.0.0.1) by mailgate-external2.sri.com with SMTP; 21 Sep 2005 02:23:53 -0000 X-Original-Received: from mailhub2.une.edu.au ([129.180.1.142]) by mailgate-external2.SRI.COM (SMSSMTP 4.0.5.66) with SMTP id M2005092019234910305 ; Tue, 20 Sep 2005 19:23:53 -0700 X-Original-Received: from turing.une.edu.au (turing.une.edu.au [129.180.11.17]) by mailhub2.une.edu.au (Postfix) with ESMTP id 17F617F8B; Wed, 21 Sep 2005 12:23:46 +1000 (EST) X-Original-Received: from turing.une.edu.au (localhost.localdomain [127.0.0.1]) by turing.une.edu.au (8.12.10/8.12.10) with ESMTP id j8L2NkT2000330 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Wed, 21 Sep 2005 12:23:46 +1000 X-Original-Received: from localhost (rapolzan@localhost) by turing.une.edu.au (8.12.10/8.12.10/Submit) with ESMTP id j8L2NjBq000326; Wed, 21 Sep 2005 12:23:45 +1000 Date: Wed, 21 Sep 2005 12:23:45 +1000 (EST) From: Romulus Apolzan To: Leonardo de Moura In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Tue, 20 Sep 2005 19:22:14 -0700 X-Mailman-Approved-At: Wed, 21 Sep 2005 09:13:48 -0700 Cc: sal-help@csl.sri.com Subject: [SAL-HELP] Re: Query about SAT solvers compatible with Mac OS X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Sep 2005 02:22:15 -0000 Thank you Leonardo for your quick answer. I was able to compile zchaff ( versions 2004.5.13 and 2004.11.15 ) on Mac OS. Unfortunately, when using zchaff ( the 2004 versions) in conjunction with sal-bmc, sal-bmc complains that zchaff produces an unknown output and that sal-bmc has been succesfully tested with the first zchaff version 2001.2.17. However, this first version of zchaff was NOT developed for Mac OS (but only for Linux and Solaris) and hence it does NOT compile on MacOS(the list of errors and deprecated headers is long ). I am using Sal-2.4 (the prelease version for Mac OS)in my experiments. Have you ever encountered this problem on Mac? Is there a solution? Cheers, Romulus. > The source code for zchaff is available on the internet. So, in principle, > you can compile it on Mac OS X. > On the siege website (http://www.cs.sfu.ca/~loryan/personal/), the author > says it can provide binaries > for other platforms if you ask him. > BTW, Grasp is an old SAT solver and it is not competitive anymore. > > Cheers, > Leonardo > From demoura@csl.sri.com Wed Sep 21 09:16:17 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j8LGGH6H006470 for ; Wed, 21 Sep 2005 09:16:17 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j8LGI8s2085008; Wed, 21 Sep 2005 09:18:08 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v734) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <550CF682-CB97-4552-B940-76B3BFE91FE8@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] Re: Query about SAT solvers compatible with Mac OS Date: Wed, 21 Sep 2005 09:18:28 -0700 To: Romulus Apolzan X-Mailer: Apple Mail (2.734) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Wed, 21 Sep 2005 09:16:28 -0700 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Sep 2005 16:16:28 -0000 Hi Romulus, > I was able to compile zchaff ( versions 2004.5.13 and 2004.11.15 ) > on Mac OS. > > Unfortunately, when using zchaff ( the 2004 versions) in > conjunction with sal-bmc, sal-bmc complains that zchaff produces an > unknown output and that > sal-bmc has been succesfully tested with the first zchaff version > 2001.2.17. > > However, this first version of zchaff was NOT developed for Mac OS > (but only for Linux and Solaris) and hence it does NOT compile on > MacOS(the list of errors and deprecated headers is long ). > > I am using Sal-2.4 (the prelease version for Mac OS)in my experiments. > > Have you ever encountered this problem on Mac? Is there a solution? I will add support for zchaff 2004. I will send you another email after I post the new binaries on the website. Cheers, Leonardo From demoura@csl.sri.com Wed Sep 21 12:19:51 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j8LJJp6H010950 for ; Wed, 21 Sep 2005 12:19:51 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j8LJLh30024165; Wed, 21 Sep 2005 12:21:43 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v734) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <2C6DF9BF-A1A9-4445-93EA-C305B9E467B4@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] Re: Query about SAT solvers compatible with Mac OS Date: Wed, 21 Sep 2005 12:22:04 -0700 To: Romulus Apolzan X-Mailer: Apple Mail (2.734) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.005 autolearn=no version=2.64 date=Wed, 21 Sep 2005 12:19:55 -0700 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Sep 2005 19:19:55 -0000 Hi Romulus, I updated the page http://sal.csl.sri.com/pre-release.shtml with new SAL 2.4 binaries (Linux and Mac OS) that are compatible with zchaff 2004. Cheers, Leonardo. On Sep 20, 2005, at 7:23 PM, Romulus Apolzan wrote: > Thank you Leonardo for your quick answer. > > I was able to compile zchaff ( versions 2004.5.13 and 2004.11.15 ) > on Mac OS. > > Unfortunately, when using zchaff ( the 2004 versions) in > conjunction with sal-bmc, sal-bmc complains that zchaff produces an > unknown output and that > sal-bmc has been succesfully tested with the first zchaff version > 2001.2.17. > > However, this first version of zchaff was NOT developed for Mac OS > (but only for Linux and Solaris) and hence it does NOT compile on > MacOS(the list of errors and deprecated headers is long ). > > I am using Sal-2.4 (the prelease version for Mac OS)in my experiments. > > Have you ever encountered this problem on Mac? Is there a solution? > > Cheers, > > Romulus. > > >> The source code for zchaff is available on the internet. So, in >> principle, you can compile it on Mac OS X. >> On the siege website (http://www.cs.sfu.ca/~loryan/personal/), the >> author says it can provide binaries >> for other platforms if you ask him. >> BTW, Grasp is an old SAT solver and it is not competitive anymore. >> >> Cheers, >> Leonardo >> > From giovanni_lombardi@libero.it Thu Oct 20 09:59:54 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j9KGxs6H052613 for ; Thu, 20 Oct 2005 09:59:54 -0700 (PDT) (envelope-from giovanni_lombardi@libero.it) X-Original-Received: from mailgate-external1.sri.com (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id j9KH6CGG078926 for ; Thu, 20 Oct 2005 10:06:12 -0700 (PDT) (envelope-from giovanni_lombardi@libero.it) X-Original-Received: from localhost (HELO mailgate-external1.SRI.COM) (127.0.0.1) by mailgate-external1.sri.com with SMTP; 20 Oct 2005 17:06:12 -0000 X-Original-Received: from ingfi1.ing.unifi.it ([150.217.10.2]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.9.35) with SMTP id M2005102010060729181 for ; Thu, 20 Oct 2005 10:06:08 -0700 X-Original-Received: from [127.0.0.1] (suman.dsi.unifi.it [150.217.15.107]) by ingfi1.ing.unifi.it (8.11.6/8.11.6) with ESMTP id j9KH64030437 for ; Thu, 20 Oct 2005 19:06:04 +0200 Message-ID: <4357CE77.4080404@libero.it> Date: Thu, 20 Oct 2005 19:05:59 +0200 From: Giovanni Lombardi User-Agent: Mozilla Thunderbird 1.0.2 (Windows/20050317) X-Accept-Language: it, it-it, en-us, en MIME-Version: 1.0 To: sal-help@csl.sri.com Content-Type: text/plain; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: 7bit X-ingfi1.ing.unifi.it-MailScanner-Information: Please contact the ISP for more information X-MailScanner: Found to be clean X-MailScanner-From: giovanni_lombardi@libero.it X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Thu, 20 Oct 2005 09:59:55 -0700 X-Mailman-Approved-At: Tue, 25 Oct 2005 08:58:21 -0700 Subject: [SAL-HELP] SAL Help me! X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 20 Oct 2005 16:59:55 -0000 I'm Giovanni Lombardi, I am student of Univerity of Florence. I have downloaded and installed SAL for Linux. My question is: exist it a translator for Stateflow to analyze the model with Sal? Thanks in advaced g.l. From rushby@csl.sri.com Tue Oct 25 09:33:45 2005 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id j9PGXj6H083269 for ; Tue, 25 Oct 2005 09:33:45 -0700 (PDT) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (muon.csl.sri.com [130.107.15.116]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id j9PGenSK087354 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 25 Oct 2005 09:40:49 -0700 (PDT) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (localhost.localdomain [127.0.0.1]) by muon.csl.sri.com (8.13.1/8.13.1) with ESMTP id j9PGen81025464; Tue, 25 Oct 2005 09:40:49 -0700 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id j9PGenxP025463; Tue, 25 Oct 2005 09:40:49 -0700 Date: Tue, 25 Oct 2005 9:40:49 PDT From: John Rushby To: Giovanni Lombardi Subject: Re: [SAL-HELP] SAL Help me! In-Reply-To: Your message of Thu, 20 Oct 2005 19:05:59 +0200 Message-ID: X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.000 autolearn=no version=2.64 date=Tue, 25 Oct 2005 09:33:45 -0700 X-Mailman-Approved-At: Tue, 25 Oct 2005 09:35:10 -0700 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 25 Oct 2005 16:33:46 -0000 Hi Giovanni, We have been experimenting with Stateflow semantics and translators, but I'm afraid we do not have anything ready for release yet. John From vincent.hilaire@utbm.fr Tue Jan 31 01:33:36 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0V9XZ6H025130 for ; Tue, 31 Jan 2006 01:33:36 -0800 (PST) (envelope-from vincent.hilaire@utbm.fr) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k0V9tgVw058545 for ; Tue, 31 Jan 2006 01:55:42 -0800 (PST) (envelope-from vincent.hilaire@utbm.fr) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006013101554100559 for ; Tue, 31 Jan 2006 01:55:41 -0800 X-Original-Received: from portail2.utbm.fr (HELO portail1.utbm.fr) (193.48.246.11) by mailgate-external1.sri.com with SMTP; 31 Jan 2006 09:55:38 -0000 X-Original-Received: from portail2.utbm.fr (localhost.localdomain [127.0.0.1]) by portail1.utbm.fr (8.12.8/jtpda-5.4) with ESMTP id k0V9tata029921 for ; Tue, 31 Jan 2006 10:55:36 +0100 X-Original-Received: from [10.85.0.1] ([192.168.1.102]) by portail2.utbm.fr (8.12.8/8.12.8) with ESMTP id k0V9tZ0U029907 for ; Tue, 31 Jan 2006 10:55:36 +0100 Message-ID: <43DF343D.3090305@utbm.fr> Date: Tue, 31 Jan 2006 10:56:13 +0100 From: hilaire Organization: UTBM User-Agent: Mozilla Thunderbird 1.0.2 (Macintosh/20050317) X-Accept-Language: fr, en MIME-Version: 1.0 To: sal-help@csl.sri.com Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Tue, 31 Jan 2006 01:33:36 -0800 X-Mailman-Approved-At: Tue, 31 Jan 2006 09:40:33 -0800 Subject: [SAL-HELP] two stange errors X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 31 Jan 2006 09:33:37 -0000 Hello all, i have two errors i don't understand. The first is [Context: satalt2, line(23), column(62)]: Invalid tuple selection, expression must be a tuple. with the line lockedAgaisntWall: objects[pos+directions]=1 --> sat'=sat-0.4 and sat is a REAL and the second is [Context: satalt2, line(23), column(111)]: Type mismatch in boolean operator. Expected type: bool Actual type: nat with simpleMove: pos + directions < 21 AND pos + directions > 0 AND objects[pos+directions]=0 --> objects'[pos]=0 AND objects'[pos+directions]=2 AND pos'=pos+directions AND sat'=sat+0.1; object' is an ARRAY [0..20] OF INTEGER pos belongs to [0..20] directions is an INTEGER These two errors must be some stupid thing... Thanks Vincent From rimvydas@dcs.qmul.ac.uk Tue Jan 31 09:34:27 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0VHYR6H035047 for ; Tue, 31 Jan 2006 09:34:27 -0800 (PST) (envelope-from rimvydas@dcs.qmul.ac.uk) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k0VHubqH097085 for ; Tue, 31 Jan 2006 09:56:38 -0800 (PST) (envelope-from rimvydas@dcs.qmul.ac.uk) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006013109563728907 for ; Tue, 31 Jan 2006 09:56:37 -0800 X-Original-Received: from tart.dcs.qmul.ac.uk (HELO mail.dcs.qmul.ac.uk) (138.37.95.139) by mailgate-external1.sri.com with SMTP; 31 Jan 2006 17:56:36 -0000 X-Original-Received: from [138.37.90.4] by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.60) (envelope-from ) id 1F3zjz-0005vg-FU; Tue, 31 Jan 2006 17:56:32 +0000 Message-ID: <43DFA4CA.6000800@dcs.qmul.ac.uk> Date: Tue, 31 Jan 2006 17:56:26 +0000 From: Rimvydas Ruksenas User-Agent: Mozilla Thunderbird 1.0.7 (Macintosh/20050923) X-Accept-Language: en-us, en MIME-Version: 1.0 To: sal-help@csl.sri.com Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-DCS-Interface-Port: 465 X-DCS-Auth-User: rimvydas X-DCS-Whoson-User: rimvydas X-DCS-clamav-result: clean (1F3zjz-0005vg-FU) X-DCS-uvscan-result: clean (1F3zjz-0005vg-FU) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests= autolearn=no version=2.64 date=Tue, 31 Jan 2006 09:34:28 -0800 X-Mailman-Approved-At: Tue, 31 Jan 2006 09:40:33 -0800 Subject: [SAL-HELP] Uninformative error message X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: rimvydas@dcs.qmul.ac.uk List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 31 Jan 2006 17:34:28 -0000 Hello, I have no idea what the following error message could mean: <...> flattening module at [Context: scratch, line(1), column(11)] calculating implicit assignments of base module at [Context: user13, line(132), column(2)]... calculating implicit assignments of base module at [Context: cuser14, line(74), column(2)]... Error: no method defined for sal-ast/flat-modules-core, and arguments ( ) I got it while running both sal-deadlock-checker and sal-smc (line(132) and line(74) are just the references to the keyword BEGIN in module definitions). Could anybody help to decipher this message? Thanks, Rimvydas From demoura@csl.sri.com Tue Jan 31 09:44:43 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0VHih6H035349 for ; Tue, 31 Jan 2006 09:44:43 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k0VI6rvE098079; Tue, 31 Jan 2006 10:06:53 -0800 (PST) (envelope-from demoura@csl.sri.com) In-Reply-To: <43DF343D.3090305@utbm.fr> References: <43DF343D.3090305@utbm.fr> Mime-Version: 1.0 (Apple Message framework v746.2) Content-Type: multipart/alternative; boundary=Apple-Mail-8--637658969 Message-Id: From: Leonardo de Moura Subject: Re: [SAL-HELP] two stange errors Date: Tue, 31 Jan 2006 10:06:54 -0800 To: hilaire X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=-0.047,HTML_60_70=0.1, HTML_MESSAGE=0.001 autolearn=no version=2.64 date=Tue, 31 Jan 2006 09:44:44 -0800 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 31 Jan 2006 17:44:44 -0000 --Apple-Mail-8--637658969 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Hi Vicent, > [Context: satalt2, line(23), column(62)]: Invalid tuple selection, > expression must be a tuple. > > with the line > > lockedAgaisntWall: objects[pos+directions]=1 --> sat'=sat-0.4 > > and sat is a REAL Could you send me your SAL file? I will help me to diagnose the problem. > [Context: satalt2, line(23), column(111)]: Type mismatch in boolean > operator. > Expected type: > bool > Actual type: > nat > > with > > simpleMove: pos + directions < 21 AND pos + directions > 0 AND > objects[pos+directions]=0 --> objects'[pos]=0 AND objects'[pos > +directions]=2 AND > pos'=pos+directions AND sat'=sat+0.1; In SAL, ";" is the separator for assignments. You should write your guarded command as: simpleMove: pos + directions < 21 AND pos + directions > 0 AND objects [pos+directions]=0 --> objects'[pos]=0; objects'[pos+directions]=2; pos'=pos+directions; sat'=sat+0.1; Cheers, Leonardo. --Apple-Mail-8--637658969 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1
Hi Vicent,


[Context: satalt2, line(23), = column(62)]: Invalid tuple selection, expression must be a = tuple.

with the line

lockedAgaisntWall: = objects[pos+directions]=3D1 --> sat'=3Dsat-0.4

and sat = is a REAL

Could you send me your SAL = file? I will help me to diagnose the problem.


[Context: satalt2, line(23), column(111)]: Type = mismatch in boolean operator.
Expected = type:
bool
Actual type:
nat


simpleMove: pos + directions < 21 AND pos + = directions > 0 AND objects[pos+directions]=3D0 --> objects'[pos]=3D0= AND objects'[pos+directions]=3D2 AND
=A0 pos'=3Dpos+directions AND = sat'=3Dsat+0.1;

In SAL, ";" is the = separator for assignments. You should write your guarded command = as:

simpleMove: pos + directions < 21 AND pos + = directions > 0 AND objects[pos+directions]=3D0 --> = objects'[pos]=3D0; objects'[pos+directions]=3D2;
=A0 pos'=3Dpos+directions; = sat'=3Dsat+0.1;

Cheers,
Leonardo.
= --Apple-Mail-8--637658969-- From demoura@csl.sri.com Tue Jan 31 09:45:54 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k0VHjr6H035442 for ; Tue, 31 Jan 2006 09:45:53 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k0VI84wJ098194; Tue, 31 Jan 2006 10:08:04 -0800 (PST) (envelope-from demoura@csl.sri.com) In-Reply-To: <43DFA4CA.6000800@dcs.qmul.ac.uk> References: <43DFA4CA.6000800@dcs.qmul.ac.uk> Mime-Version: 1.0 (Apple Message framework v746.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <0844F965-4C60-4E85-AA26-48C595BAA9D7@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] Uninformative error message Date: Tue, 31 Jan 2006 10:08:05 -0800 To: rimvydas@dcs.qmul.ac.uk X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.006 autolearn=no version=2.64 date=Tue, 31 Jan 2006 09:45:54 -0800 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 31 Jan 2006 17:45:54 -0000 Hi Rimvydas, > <...> > flattening module at [Context: scratch, line(1), column(11)] > calculating implicit assignments of base module at [Context: > user13, line(132), column(2)]... > calculating implicit assignments of base module at [Context: > cuser14, line(74), column(2)]... > Error: no method defined for sal-ast/flat-modules-core, and > arguments ( ) This error message is a bug. Could you send me your SAL file? It will help me to fix this bug. Thanks, Leonardo. From ajhs@dcs.shef.ac.uk Fri Mar 10 01:48:39 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2A9mc6H077905 for ; Fri, 10 Mar 2006 01:48:38 -0800 (PST) (envelope-from ajhs@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k2AAGaQd080047 for ; Fri, 10 Mar 2006 02:16:36 -0800 (PST) (envelope-from ajhs@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006031002163512476 for ; Fri, 10 Mar 2006 02:16:35 -0800 X-Original-Received: from marmot.shef.ac.uk (143.167.1.4) by mailgate-external1.sri.com with SMTP; 10 Mar 2006 10:16:34 -0000 X-Original-Received: from holly.dcs.shef.ac.uk ([143.167.8.1]) by marmot.shef.ac.uk with esmtp (Exim 4.52) id 1FHefd-0006vi-SJ for sal-help@csl.sri.com; Fri, 10 Mar 2006 10:16:29 +0000 X-Original-Received: from ivy.dcs.shef.ac.uk (ivy.dcs.shef.ac.uk [143.167.8.2]) by holly.dcs.shef.ac.uk (8.12.10+Sun/8.12.10) with SMTP id k2AAGSbZ003816 for ; Fri, 10 Mar 2006 10:16:29 GMT Message-Id: <200603101016.k2AAGSbZ003816@holly.dcs.shef.ac.uk> Date: Fri, 10 Mar 2006 10:16:28 +0000 (GMT) From: Tony Simons To: sal-help@csl.sri.com MIME-Version: 1.0 Content-Type: MULTIPART/mixed; BOUNDARY=Colony_of_Beavers_020_000 X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.5.7 SunOS 5.9 sun4u sparc X-S0phie-Scan: Yes X-Spam-Level: * X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=1.1 required=4.0 tests=MIME_BASE64_TEXT=1.101 autolearn=no version=2.64 date=Fri, 10 Mar 2006 01:48:41 -0800 X-Mailman-Approved-At: Fri, 10 Mar 2006 09:49:56 -0800 Subject: [SAL-HELP] Recursive datatypes and functions X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: Tony Simons List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 10 Mar 2006 09:48:41 -0000 --Colony_of_Beavers_020_000 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: 3JZJ71ZsHhMm2DuY7I9nDQ== Dear SAL helpers, I can't get recursive datatypes or functions to work as I anticipate in the sal toolset. I enclose two examples - a recursively-defined set datatype (modelled after the List in the language manual) and a simpler example of a recursive size? function added to calculate the cardinality of a set, based on the set.sal example context. I get errors on starting a simulation, which seems to want to expand the recursion or something like that (I'm guessing the fault). Any help on getting recursive things to work would be much appreciated! It could be that there's an extra trick, or perhaps this doesn't work well with the symbolic BDDs. --Tony ========================================================================== Dr Anthony J H Simons a.simons@dcs.shef.ac.uk Senior Lecturer in Computer Science http://www.dcs.shef.ac.uk/~ajhs Department of Computer Science tel: (+44) 114 22 21838 University of Sheffield dept: (+44) 114 22 21800 Regent Court, 211 Portobello Street fax: (+44) 114 22 21810 SHEFFIELD, S1 4DP univ: (+44) 114 22 22000 United Kingdom ========================================================================== --Colony_of_Beavers_020_000 Content-Type: TEXT/plain; name="nset.sal"; charset=ISO-8859-1; x-unix-mode=0644 Content-Transfer-Encoding: BASE64 Content-Description: nset.sal Content-MD5: np7giFze3A18fuQxzy8MaA== bnNldHtUIDogVFlQRTsgfSA6IENPTlRFWFQgPQ0KQkVHSU4NCg0KICBTZXQg OiBUWVBFID0gW1QgLT4gQk9PTEVBTl07DQoNCiAgZW1wdHlfc2V0IDogU2V0 ID0gTEFNQkRBIChlIDogVCkgOiBGQUxTRTsNCg0KICBmdWxsX3NldCA6IFNl dCA9IExBTUJEQSAoZSA6IFQpIDogVFJVRTsNCg0KICBpbnNlcnQgKGFzZXQg OiBTZXQsIGUgOiBUKSA6IFNldCA9IA0KCQlMQU1CREEgKGUxIDogVCkgOiBl ID0gZTEgT1IgYXNldChlMSk7DQoNCiAgcmVtb3ZlIChhc2V0IDogU2V0LCBl IDogVCkgOiBTZXQgPSANCiAgICBMQU1CREEgKGUxIDogVCkgOiBlIC89IGUx IEFORCBhc2V0KGUxKTsNCg0KICBjb250YWlucz8gKGFzZXQgOiBTZXQsIGUg OiBUKSA6IEJPT0xFQU4gPSANCiAgICBhc2V0KGUpOw0KDQogIGVtcHR5PyAo YXNldCA6IFNldCkgOiBCT09MRUFOID0NCiAgICAoRk9SQUxMIChlIDogVCkg OiBhc2V0KGUpID0gRkFMU0UpOw0KDQogIHVuaW9uIChhc2V0MSA6IFNldCwg YXNldDIgOiBTZXQpIDogU2V0ID0NCgkJTEFNQkRBIChlIDogVCkgOiBhc2V0 MShlKSBPUiBhc2V0MihlKTsNCiANCiAgaW50ZXJzZWN0aW9uIChhc2V0MSA6 IFNldCwgYXNldDIgOiBTZXQpIDogU2V0ID0NCiAgICBMQU1CREEgKGUgOiBU KSA6IGFzZXQxKGUpIEFORCBhc2V0MihlKTsNCiANCiAgZGlmZmVyZW5jZSAo YXNldDEgOiBTZXQsIGFzZXQyIDogU2V0KSA6IFNldCA9DQogICAgTEFNQkRB IChlIDogVCkgOiBhc2V0MShlKSBBTkQgTk9UIGFzZXQyKGUpOw0KDQogIHN1 YnNldD8gKGFzZXQxIDogU2V0LCBhc2V0MjogU2V0KSA6IEJPT0xFQU4gPQ0K ICAgIChGT1JBTEwgKGUgOiBUKSA6IGNvbnRhaW5zPyhhc2V0MSwgZSkgPT4g Y29udGFpbnM/KGFzZXQyLCBlKSk7DQoNCg0KDSUlIHJlZHVjZSBib290cyBh biBhcmJpdHJhcnkgZWxlbWVudCBvdXQgb2YgdGhlIHNldCAtIGRlZmluZWQg aW4gdGhlZQolJSBzYW1lIHN0eWxlIGFzIHJlbW92ZS4KCiAgcmVkdWNlIChh c2V0IDogU2V0KSA6IFNldCA9CiAgICBMQU1CREEgKGUxIDogVCkgOiAoRVhJ U1RTIChlIDogVCkgOiBlIC89IGUxIEFORCBhc2V0KGUxKSk7CiAgICAKJSUg c2l6ZT8gaXMgYSByZWN1cnNpdmUgZnVuY3Rpb24gdGhhdCByZWxpZXMgb24g cmVkdWNlLgogCiAgc2l6ZT8gKGFzZXQgOiBTZXQpIDogTkFUVVJBTCA9CiAg ICBJRiBlbXB0eT8oYXNldCkKICAgIFRIRU4gMAogICAgRUxTRSAxICsgc2l6 ZT8ocmVkdWNlKGFzZXQpKQogICAgRU5ESUY7CiAgICAKRU5EDQoNCg0KDQo= --Colony_of_Beavers_020_000 Content-Type: TEXT/plain; name="cset.sal"; charset=ISO-8859-1; x-unix-mode=0644 Content-Transfer-Encoding: BASE64 Content-Description: cset.sal Content-MD5: Lfat7qPLkiHRAVFRcHFVtQ== Y3NldHtUIDogVFlQRTsgfSA6IENPTlRFWFQgPQ0KQkVHSU4NCgolJSBEZWZp bmUgU2V0IGFzIGFuIGluZHVjdGl2ZSBkYXRhdHlwZSB3aXRoIGNvbnN0cnVj dG9ycywgZm9sbG93aW5nIAolJSBzdHlsZSBvZiBsaXN0cyBpbiBTQUwgbGFu Z3VhZ2UgcmVwb3J0LCBwYWdlIDcuICBOb3RlIHRoYXQgY29uc3RydWN0b3IK JSUgJ2VtcHR5JyBjYXVzZXMgU0FMIHRvIGdlbmVyYXRlIHF1ZXJ5IGZ1bmN0 aW9uICdlbXB0eT8nIGF1dG9tYXRpY2FsbHkuCgolJSBUaGUgZW1wdHkgc2V0 IGlzIGNhbGxlZCAnZW1wdHknLCBieSB0aGlzIGNvbnZlbnRpb24sIHJhdGhl ciB0aGFuIHRoZQolJSAnZW1wdHlfc2V0JyBwcmVkaWNhdGUgaW4gdGhlIHNl dCBjb250ZXh0LiAgVGhlcmUgaXMgbm8gY291bnRlcnBhcnQgdG8KJSUgdGhl ICdmdWxsX3NldCcgcHJlZGljYXRlIGluIHRoZSBzZXQgY29udGV4dC4KDQog IFNldCA6IFRZUEUgPSBEQVRBVFlQRQogIAkJYWRkKGVsZW0gOiBULCByZXN0 IDogU2V0KSwKICAJCWVtcHR5CiAgCSAgICBFTkQ7CiAgCSAgCiUlICdpbnNl cnQnIGZ1bmN0aW9uIG11c3QgdGVzdCBpZiBlbGVtZW50IGFscmVhZHkgcHJl c2VudCBpbiBTZXQuCgogIGluc2VydCAoc2V0IDogU2V0LCBlIDogVCkgOiBT ZXQgPQogICAJSUYgZW1wdHk/KHNldCkgCiAgIAkgIFRIRU4gYWRkKGUsIHNl dCkgCiAgIAlFTFNJRiBlID0gZWxlbShzZXQpIAogICAJICBUSEVOIHNldAog ICAJRUxTRQogCSAgYWRkIChlbGVtKHNldCksIGluc2VydChyZXN0KHNldCks IGUpKQogCUVORElGOwoKJSUgJ3JlbW92ZScgZnVuY3Rpb24gbXVzdCBlbnN1 cmUgdGhlIGVsZW1lbnQgaXMgbm90IGluIHRoZSBTZXQuCgogIHJlbW92ZSAo c2V0IDogU2V0LCBlIDogVCkgOiBTZXQgPQogIAlJRiBlbXB0eT8oc2V0KSAK ICAJICBUSEVOIHNldCAKICAJRUxTSUYgZSA9IGVsZW0oc2V0KSAKICAJICBU SEVOIHJlc3Qoc2V0KSAKICAJRUxTRQogIAkgIGFkZChlbGVtKHNldCksIHJl bW92ZShyZXN0KHNldCksIGUpKQogIAlFTkRJRjsKCiAKJSUgJ2NvbnRhaW5z PycgZnVuY3Rpb24gbXVzdCBkZXRlY3QgaWYgdGhlIGVsZW1lbnQgaXMgaW4g dGhlIFNldC4KCg0gICBjb250YWlucz8gKHNldCA6IFNldCwgZSA6IFQpIDog Qk9PTEVBTiA9Cg0JSUYgZW1wdHk/KHNldCkgCg0JICBUSEVOIEZBTFNFIAoN CUVMU0lGIGUgPSBlbGVtKHNldCkgCg0JICBUSEVOIFRSVUUKDQlFTFNFIAoN CSAgY29udGFpbnM/KHJlc3Qoc2V0KSwgZSkKDQlFTkRJRjsKDSAKJSUgJ2Vt cHR5PycgZnVuY3Rpb24gaXMgZ2VuZXJhdGVkIGF1dG9tYXRpY2FsbHk7IHNl ZSBhYm92ZS4KDQolJSAndW5pb24nIGZ1bmN0aW9uIGFkZHMgZWxlbWVudHMg ZnJvbSBzZXQxIHRvIHNldDIgdGhhdCBhcmUgbm90IGluIHNldDIuCgogIHVu aW9uKHNldDEgOiBTZXQsIHNldDIgOiBTZXQpIDogU2V0ID0KICAJSUYgZW1w dHk/KHNldDEpIAogIAkgIFRIRU4gc2V0MiAKICAJRUxTSUYgY29udGFpbnM/ KHNldDIsIGVsZW0oc2V0MSkpIAogIAkgIFRIRU4gdW5pb24ocmVzdChzZXQx KSwgc2V0MikgCiAgCUVMU0UKICAJICBhZGQoZWxlbShzZXQxKSwgdW5pb24o cmVzdChzZXQxKSwgc2V0MikpCiAgCUVORElGOwoKJSUgJ2ludGVyc2VjdGlv bicgZnVuY3Rpb24gcHJlc2VydmVzIGVsZW1lbnRzIGZyb20gc2V0MSB0aGF0 IGFyZSBpbiBzZXQyCgogIGludGVyc2VjdGlvbihzZXQxIDogU2V0LCBzZXQy IDogU2V0KSA6IFNldCA9CiAgCUlGIGVtcHR5PyhzZXQxKSAKICAJICBUSEVO IGVtcHR5IAogIAlFTFNJRiBjb250YWlucz8oc2V0MiwgZWxlbShzZXQxKSkg CiAgCSAgVEhFTiBhZGQoZWxlbShzZXQxKSwgaW50ZXJzZWN0aW9uKHJlc3Qo c2V0MSksIHNldDIpKQogIAlFTFNFCiAgCSAgaW50ZXJzZWN0aW9uKHJlc3Qo c2V0MSksIHNldDIpIAogIAlFTkRJRjsKCiUlICdkaWZmZXJlbmNlJyBmdW5j dGlvbiBwcmVzZXJ2ZXMgZWxlbWVudHMgZnJvbSBzZXQxIHRoYXQgYXJlIG5v dCBpbiBzZXQyLgoKICBkaWZmZXJlbmNlKHNldDEgOiBTZXQsIHNldDIgOiBT ZXQpIDogU2V0ID0KICAJSUYgZW1wdHk/KHNldDEpIAogIAkgIFRIRU4gZW1w dHkgCiAgCUVMU0lGIGNvbnRhaW5zPyhzZXQyLCBlbGVtKHNldDEpKSAKICAJ ICBUSEVOIGRpZmZlcmVuY2UocmVzdChzZXQxKSwgc2V0MikKICAJRUxTRQog IAkgIGFkZChlbGVtKHNldDEpLCBkaWZmZXJlbmNlKHJlc3Qoc2V0MSksIHNl dDIpKQogIAlFTkRJRjsKCiUlICdzdWJzZXQ/JyBmdW5jdGlvbiBjaGVja3Mg aWYgZXZlcnkgZWxlbWVudCBpbiBzZXQxIGlzIGluIHNldDIuCgogIHN1YnNl dChzZXQxIDogU2V0LCBzZXQyIDogU2V0KSA6IEJPT0xFQU4gPQogIAlJRiBl bXB0eT8oc2V0MSkgCiAgCSAgVEhFTiBUUlVFIAogIAlFTFNJRiBjb250YWlu cz8oc2V0MiwgZWxlbShzZXQxKSkgCiAgCSAgVEhFTiBzdWJzZXQocmVzdChz ZXQxKSwgc2V0MikKICAJRUxTRQogIAkgIEZBTFNFCiAgCUVORElGOwoKJSUg IE9sZCBkZWZpbml0aW9uIG1pZ2h0IHN0aWxsIHdvcmssIHRvby4KJSUgIHN1 YnNldD8oc2V0MSA6IFNldCwgc2V0MjogU2V0KSA6IEJPT0xFQU4gPQ0KJSUg ICAgKEZPUkFMTCAoZSA6IFQpIDogY29udGFpbnM/KHNldDEsZSkgPT4gY29u dGFpbnM/KHNldDIsZSkpOw0KICAgIAoNCiUlICdzaXplPycgZnVuY3Rpb24g Y291bnRzIHRoZSBjaGFpbiBvZiBlbGVtZW50cyBpbiB0aGUgZGF0YXR5cGUs IHNpbWlsYXIgCiUlIHRvIHRoZSAnbGVuZ3RoJyBmdW5jdGlvbiBkZWZpbmVk IG9uIGxpc3RzLiAgTm90ZSB0aGF0IHRoaXMgcmV0dXJucyB0aGUKJSUgY2Fy ZGluYWxpdHksIHJhdGhlciB0aGFuIHJlcXVpcmluZyBpdCBhcyBhbiBhcmd1 bWVudC4KDQogIHNpemU/KHNldCA6IFNldCkgOiBOQVRVUkFMID0NCglJRiBl bXB0eT8oc2V0KSAKCSAgVEhFTiAwCglFTFNFCgkgIDEgKyBzaXplPyhyZXN0 KHNldCkpCglFTkRJRjsKDQpFTkQNCg0KDQoNCg== --Colony_of_Beavers_020_000-- From ajhs@dcs.shef.ac.uk Fri Mar 10 02:05:42 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2AA5e6H078098 for ; Fri, 10 Mar 2006 02:05:42 -0800 (PST) (envelope-from ajhs@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.12.11/8.12.11) with SMTP id k2AAXaGw080776 for ; Fri, 10 Mar 2006 02:33:39 -0800 (PST) (envelope-from ajhs@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006031002333613147 for ; Fri, 10 Mar 2006 02:33:36 -0800 X-Original-Received: from marmot.shef.ac.uk (143.167.1.4) by mailgate-external1.sri.com with SMTP; 10 Mar 2006 10:33:36 -0000 X-Original-Received: from holly.dcs.shef.ac.uk ([143.167.8.1]) by marmot.shef.ac.uk with esmtp (Exim 4.52) id 1FHewB-0001T7-7R for sal-help@csl.sri.com; Fri, 10 Mar 2006 10:33:35 +0000 X-Original-Received: from ivy.dcs.shef.ac.uk (ivy.dcs.shef.ac.uk [143.167.8.2]) by holly.dcs.shef.ac.uk (8.12.10+Sun/8.12.10) with SMTP id k2AAXXbZ008077; Fri, 10 Mar 2006 10:33:33 GMT Message-Id: <200603101033.k2AAXXbZ008077@holly.dcs.shef.ac.uk> Date: Fri, 10 Mar 2006 10:33:33 +0000 (GMT) From: Tony Simons To: sal-help@csl.sri.com MIME-Version: 1.0 Content-Type: MULTIPART/mixed; BOUNDARY=Colony_of_Gulls_166_000 X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.5.7 SunOS 5.9 sun4u sparc X-S0phie-Scan: Yes X-Spam-Level: * X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=1.1 required=4.0 tests=MIME_BASE64_TEXT=1.101 autolearn=no version=2.64 date=Fri, 10 Mar 2006 02:05:43 -0800 X-Mailman-Approved-At: Fri, 10 Mar 2006 09:49:56 -0800 Cc: a.simons@holly.dcs.shef.ac.uk Subject: [SAL-HELP] Possible SAL type failure X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: Tony Simons List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 10 Mar 2006 10:05:44 -0000 --Colony_of_Gulls_166_000 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: 6RcemUrcRgUjp4p0JhBp2g== Dear SAL helpers, I've been trying to model relations in SAL as sets of pairs. However, when I try to insert a pair-element into a set, I get an internal type failure error, for context that was syntactically parsed. I enclose the minimal example that causes this fault. See if you get the same fault. Here's what I get: =============== sal-sim ************************************************************ * Welcome to SAL, copyright 2003 SRI International. * * This copy is licensed for NONCOMMERCIAL use to: * * Anthony Simons * * If this is not you, please obtain a license from * * sal.csl.sri.com: SAL is free for noncommercial use. * * For commercial use, please contact fm-license@csl.sri.com. * ************************************************************ SAL Simulator (Version 2.3). Copyright (c) 2003, 2004 SRI International. Build date: Sun Jul 11 04:12:22 PDT 2004 Type `(exit)' to exit. Type `(help)' for help. sal > (import! "testset") sal > (start-simulation! "main") Error at "check-param": Type `pair' expected, `bnil' provided () Remark: the command '(sal/enable-trace-stack! #t)' can be used to force SAL to print the call/trace stack when an error happens. sal > ========================================================================== Dr Anthony J H Simons a.simons@dcs.shef.ac.uk Senior Lecturer in Computer Science http://www.dcs.shef.ac.uk/~ajhs Department of Computer Science tel: (+44) 114 22 21838 University of Sheffield dept: (+44) 114 22 21800 Regent Court, 211 Portobello Street fax: (+44) 114 22 21810 SHEFFIELD, S1 4DP univ: (+44) 114 22 22000 United Kingdom ========================================================================== --Colony_of_Gulls_166_000 Content-Type: TEXT/plain; name="set.sal"; charset=ISO-8859-1; x-unix-mode=0644 Content-Transfer-Encoding: BASE64 Content-Description: set.sal Content-MD5: 291BKt/3I3f8hPpPBAqBTA== c2V0e1QgOiBUWVBFOyB9IDogQ09OVEVYVCA9DQpCRUdJTg0KDQogIFNldCA6 IFRZUEUgPSBbVCAtPiBCT09MRUFOXTsNCg0KICBlbXB0eV9zZXQgOiBTZXQg PSBMQU1CREEgKGUgOiBUKSA6IEZBTFNFOw0KDQogIGZ1bGxfc2V0IDogU2V0 ID0gTEFNQkRBIChlIDogVCkgOiBUUlVFOw0KDQogIGluc2VydCAoYXNldCA6 IFNldCwgZSA6IFQpIDogU2V0ID0gDQoJCUxBTUJEQSAoZTEgOiBUKSA6IGUg PSBlMSBPUiBhc2V0KGUxKTsNCg0KICByZW1vdmUgKGFzZXQgOiBTZXQsIGUg OiBUKSA6IFNldCA9IA0KICAgIExBTUJEQSAoZTEgOiBUKSA6IGUgLz0gZTEg QU5EIGFzZXQoZTEpOw0KDQogIGNvbnRhaW5zPyAoYXNldCA6IFNldCwgZSA6 IFQpIDogQk9PTEVBTiA9IA0KICAgIGFzZXQoZSk7DQoNCiAgZW1wdHk/IChh c2V0IDogU2V0KSA6IEJPT0xFQU4gPQ0KICAgIChGT1JBTEwgKGUgOiBUKSA6 IGFzZXQoZSkgPSBGQUxTRSk7DQoNCiAgdW5pb24oYXNldDEgOiBTZXQsIGFz ZXQyIDogU2V0KSA6IFNldCA9DQoJCUxBTUJEQSAoZSA6IFQpIDogYXNldDEo ZSkgT1IgYXNldDIoZSk7DQogDQogIGludGVyc2VjdGlvbihhc2V0MSA6IFNl dCwgYXNldDIgOiBTZXQpIDogU2V0ID0NCiAgICBMQU1CREEgKGUgOiBUKSA6 IGFzZXQxKGUpIEFORCBhc2V0MihlKTsNCiANCiAgZGlmZmVyZW5jZShhc2V0 MSA6IFNldCwgYXNldDIgOiBTZXQpIDogU2V0ID0NCiAgICBMQU1CREEgKGUg OiBUKSA6IGFzZXQxKGUpIEFORCBOT1QgYXNldDIoZSk7DQoNCiAgc3Vic2V0 Pyhhc2V0MSA6IFNldCwgYXNldDI6IFNldCkgOiBCT09MRUFOID0NCiAgICAo Rk9SQUxMIChlIDogVCkgOiBjb250YWlucz8oYXNldDEsZSkgPT4gY29udGFp bnM/KGFzZXQyLGUpKTsNCiAgICAKJSUgUmF0aGVyIGxhYm9yaW91cyBkZWZp bml0aW9uIG9mIHNpemU/IHRoYXQgd29ya3Mgd2l0aCBmdW5jdGlvbi1lbmNv ZGluZyAgICAKCiAgc2l6ZT8oYXNldDpTZXQsIG46TkFUVVJBTCkgOiBCT09M RUFOID0NCiAgICAoZW1wdHk/IChhc2V0KSBBTkQgbiA9IDApIE9SCiAgICAo RVhJU1RTIChmOltbMS4ubl0gLT4gVF0pIDoNCgkoRk9SQUxMICh4MSx4Mjpb MS4ubl0pIDogZih4MSk9Zih4MikgPT4geDE9eDIpIEFORA0KCShGT1JBTEwg KHk6VCkgOiBhc2V0KHkpIDw9PiAoRVhJU1RTICh4OlsxLi5uXSkgOiBmKHgp ID0geSkpKTsNCg0KRU5EDQoNCg0KDQo= --Colony_of_Gulls_166_000 Content-Type: TEXT/plain; name="testset.sal"; charset=us-ascii; x-unix-mode=0644 Content-Description: testset.sal Content-MD5: WvkFo9nOpAciy4/8WPewXg== testset : CONTEXT = BEGIN Dom : TYPE = {a, b, c}; Ran : TYPE = {p, q, r}; myrel : CONTEXT = set{[Dom,Ran];}; main : MODULE = BEGIN INPUT value : [Dom,Ran] LOCAL group : myrel!Set INITIALIZATION group = myrel!empty_set TRANSITION [ Insert : value = (a, p) --> group' = myrel!insert(group, value) [] NoChange : TRUE --> group' = group ] END; th1 : THEOREM main |- G(myrel!size?(group, 2)); th2 : THEOREM main |- NOT F(myrel!size?(group, 2)); END --Colony_of_Gulls_166_000-- From demoura@csl.sri.com Fri Mar 10 09:58:24 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2AHwO6H088644 for ; Fri, 10 Mar 2006 09:58:24 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k2AIQQUX015563; Fri, 10 Mar 2006 10:26:26 -0800 (PST) (envelope-from demoura@csl.sri.com) In-Reply-To: <200603101033.k2AAXXbZ008077@holly.dcs.shef.ac.uk> References: <200603101033.k2AAXXbZ008077@holly.dcs.shef.ac.uk> Mime-Version: 1.0 (Apple Message framework v746.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <7FC597C0-B6B3-4063-B73B-5A82CC54114A@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] Possible SAL type failure Date: Fri, 10 Mar 2006 10:26:28 -0800 To: Tony Simons X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.012 autolearn=no version=2.64 date=Fri, 10 Mar 2006 09:58:25 -0800 Cc: a.simons@holly.dcs.shef.ac.uk, sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 10 Mar 2006 17:58:26 -0000 Dear Anthony, Please could you try to download the pre-release version of SAL 2.4? This problem doesn't happen in this version. The pre-release version of SAL 2.4 is available at: http://sal.csl.sri.com/pre-release.shtml Cheers, Leonardo On Mar 10, 2006, at 2:33 AM, Tony Simons wrote: > Dear SAL helpers, > > I've been trying to model relations in SAL as sets of pairs. However, > when I try to insert a pair-element into a set, I get an internal > type failure error, for context that was syntactically parsed. > > I enclose the minimal example that causes this fault. See if you > get the same fault. Here's what I get: > > =============== > > sal-sim > ************************************************************ > * Welcome to SAL, copyright 2003 SRI International. * > * This copy is licensed for NONCOMMERCIAL use to: * > * Anthony Simons * > * If this is not you, please obtain a license from * > * sal.csl.sri.com: SAL is free for noncommercial use. * > * For commercial use, please contact fm-license@csl.sri.com. * > ************************************************************ > > SAL Simulator (Version 2.3). Copyright (c) 2003, 2004 SRI > International. > Build date: Sun Jul 11 04:12:22 PDT 2004 > Type `(exit)' to exit. > Type `(help)' for help. > > sal > (import! "testset") > > sal > (start-simulation! "main") > > Error at "check-param": Type `pair' expected, `bnil' provided > () > > Remark: the command '(sal/enable-trace-stack! #t)' can be used to > force SAL to > print the call/trace stack when an error happens. > > sal > > > ====================================================================== > ==== > > Dr Anthony J H Simons a.simons@dcs.shef.ac.uk > Senior Lecturer in Computer Science http://www.dcs.shef.ac.uk/ > ~ajhs > > Department of Computer Science tel: (+44) 114 22 21838 > University of Sheffield dept: (+44) 114 22 21800 > Regent Court, 211 Portobello Street fax: (+44) 114 22 21810 > SHEFFIELD, S1 4DP univ: (+44) 114 22 22000 > United Kingdom > > ====================================================================== > ==== > > set{T : TYPE; } : CONTEXT = > BEGIN > > Set : TYPE = [T -> BOOLEAN]; > > empty_set : Set = LAMBDA (e : T) : FALSE; > > full_set : Set = LAMBDA (e : T) : TRUE; > > insert (aset : Set, e : T) : Set = > LAMBDA (e1 : T) : e = e1 OR aset(e1); > > remove (aset : Set, e : T) : Set = > LAMBDA (e1 : T) : e /= e1 AND aset(e1); > > contains? (aset : Set, e : T) : BOOLEAN = > aset(e); > > empty? (aset : Set) : BOOLEAN = > (FORALL (e : T) : aset(e) = FALSE); > > union(aset1 : Set, aset2 : Set) : Set = > LAMBDA (e : T) : aset1(e) OR aset2(e); > > intersection(aset1 : Set, aset2 : Set) : Set = > LAMBDA (e : T) : aset1(e) AND aset2(e); > > difference(aset1 : Set, aset2 : Set) : Set = > LAMBDA (e : T) : aset1(e) AND NOT aset2(e); > > subset?(aset1 : Set, aset2: Set) : BOOLEAN = > (FORALL (e : T) : contains?(aset1,e) => contains?(aset2,e)); > > %% Rather laborious definition of size? that works with function- > encoding > > size?(aset:Set, n:NATURAL) : BOOLEAN = > (empty? (aset) AND n = 0) OR > (EXISTS (f:[[1..n] -> T]) : > (FORALL (x1,x2:[1..n]) : f(x1)=f(x2) => x1=x2) AND > (FORALL (y:T) : aset(y) <=> (EXISTS (x:[1..n]) : f(x) = y))); > > END > > > > testset : CONTEXT = > BEGIN > > Dom : TYPE = {a, b, c}; > Ran : TYPE = {p, q, r}; > > myrel : CONTEXT = set{[Dom,Ran];}; > > main : MODULE = > BEGIN > INPUT value : [Dom,Ran] > LOCAL group : myrel!Set > INITIALIZATION group = myrel!empty_set > TRANSITION [ > Insert : value = (a, p) > --> group' = myrel!insert(group, value) > [] > NoChange : TRUE > --> group' = group > ] > END; > > th1 : THEOREM main |- G(myrel!size?(group, 2)); > th2 : THEOREM main |- NOT F(myrel!size?(group, 2)); > > END From demoura@csl.sri.com Fri Mar 10 10:03:10 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2AI3A6H088868 for ; Fri, 10 Mar 2006 10:03:10 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k2AIVChB016075; Fri, 10 Mar 2006 10:31:12 -0800 (PST) (envelope-from demoura@csl.sri.com) In-Reply-To: <200603101016.k2AAGSbZ003816@holly.dcs.shef.ac.uk> References: <200603101016.k2AAGSbZ003816@holly.dcs.shef.ac.uk> Mime-Version: 1.0 (Apple Message framework v746.2) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <68C9337A-ECF2-4BE5-AC51-52D7F747569D@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] Recursive datatypes and functions Date: Fri, 10 Mar 2006 10:31:14 -0800 To: Tony Simons X-Mailer: Apple Mail (2.746.2) X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.012 autolearn=no version=2.64 date=Fri, 10 Mar 2006 10:03:11 -0800 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 10 Mar 2006 18:03:11 -0000 Hi Anthony, > I can't get recursive datatypes or functions to work as I anticipate > in the sal toolset. None of the current tools support recursive datatypes. sal-smc, and sal-sim use binary decision diagrams (BDDs) to represent the transition relation. So, the SAL specification must be transformed in boolean formulas, and recursive datatypes are not supported. sal-bmc uses SAT solvers, and has the same limitation. In the next release, sal-inf-bmc will support recursive datatypes. Leonardo From rushby@csl.sri.com Fri Mar 10 10:30:37 2006 X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id k2AIUb6H089347 for ; Fri, 10 Mar 2006 10:30:37 -0800 (PST) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (muon.csl.sri.com [130.107.15.116]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k2AIwdnk018116 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Fri, 10 Mar 2006 10:58:39 -0800 (PST) (envelope-from rushby@csl.sri.com) X-Original-Received: from muon.csl.sri.com (localhost.localdomain [127.0.0.1]) by muon.csl.sri.com (8.13.1/8.13.1) with ESMTP id k2AIwcEV025128; Fri, 10 Mar 2006 10:58:39 -0800 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id k2AIwctF025127; Fri, 10 Mar 2006 10:58:38 -0800 Date: Fri, 10 Mar 2006 10:58:38 PST From: John Rushby To: Tony Simons Subject: Re: [SAL-HELP] Recursive datatypes and functions In-Reply-To: Your message of Fri, 10 Mar 2006 10:16:28 +0000 (GMT) Message-ID: X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=AWL=0.009 autolearn=no version=2.64 date=Fri, 10 Mar 2006 10:30:38 -0800 Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 10 Mar 2006 18:30:38 -0000 Tony, The SAL finite state model checkers (indeed, any finite state model checkers) essentially have to compile the specification into a circuit. Recursion is ok, if it is finitely bounded, but things like removing an arbitrary element from a generic set are not. If it's set of some scalar type, you could probably find a way to specify it that would work. In model checking, one usually abstracts a concrete specification to a more abstract one that is nondeterministic. For example, rather than count the number of elements in a set, you'd note whether it is empty, a singleton, partfull, or full. The process scheduler example around page 22 of the SAL-ATG manual does this. Another possibility might be to represent a set as a record: the set itself plus its current cardinality; each of the set operations would then be defined to keep these in sync. The infinite bounded model checker of SAL shuld be able to handle more generic specifications, but its full capabilities are still under exploration and development. (Though see http://www.cs.indiana.edu/~lepike/pub_pages/bmp.html for a cool example). John From katelman@uiuc.edu Sun Apr 16 15:10:25 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=none autolearn=disabled version=3.1.1 date=Sun, 16 Apr 2006 15:10:27 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3GMAP7J008169 for ; Sun, 16 Apr 2006 15:10:25 -0700 (PDT) (envelope-from katelman@uiuc.edu) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k3GMAP1c014146 for ; Sun, 16 Apr 2006 15:10:25 -0700 (PDT) (envelope-from katelman@uiuc.edu) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006041615102516673 for ; Sun, 16 Apr 2006 15:10:25 -0700 X-Original-Received: from sccimhc91.asp.att.net (63.240.76.165) by mailgate-external1.sri.com with SMTP; 16 Apr 2006 22:10:25 -0000 X-Original-Received: from [192.168.1.102] (12-221-86-44.client.insightbb.com[12.221.86.44]) by sccimhc91.asp.att.net (sccimhc91) with SMTP id <20060416221023i9100a7o9te>; Sun, 16 Apr 2006 22:10:23 +0000 Mime-Version: 1.0 (Apple Message framework v623) Content-Transfer-Encoding: 7bit Message-Id: Content-Type: text/plain; charset=US-ASCII; format=flowed To: sal-help@csl.sri.com From: Michael Katelman Date: Sun, 16 Apr 2006 17:10:23 -0500 X-Mailer: Apple Mail (2.623) X-Mailman-Approved-At: Mon, 24 Apr 2006 12:31:49 -0700 Subject: [SAL-HELP] sal-sim question X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 16 Apr 2006 22:10:27 -0000 How do I load in (via (import! ...)) a parametric context? For example, I tried (import! "arbiter{;4}") in addition to all the other modifications that seemed reasonable to me, but the system didn't seem to like any of them. Thanks for the help. -Mike From demoura@csl.sri.com Mon Apr 24 12:34:59 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44 autolearn=disabled version=3.1.1 date=Mon, 24 Apr 2006 12:34:59 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k3OJYxIG017991 for ; Mon, 24 Apr 2006 12:34:59 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.13.4/8.12.11) with ESMTP id k3OJYw4I024819; Mon, 24 Apr 2006 12:34:58 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v749.3) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <70825C90-A639-466E-8187-0AFDDCC63E46@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] sal-sim question Date: Mon, 24 Apr 2006 12:35:27 -0700 To: Michael Katelman X-Mailer: Apple Mail (2.749.3) Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 24 Apr 2006 19:34:59 -0000 Hi Mike, > How do I load in (via (import! ...)) a parametric context? For > example, I tried (import! "arbiter{;4}") in addition to all the > other modifications that seemed reasonable to me, but the system > didn't seem to like any of them. Thanks for the help. You can do that in SAL 2.4. The pre-release version can be downloaded at: http://sal.csl.sri.com/pre-release.shtml In this version, you can use (import! "arbiter{4}") to import a parametric module. Cheers, Leonardo From swarup.mohalik@gm.com Thu May 18 23:09:14 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=HTML_MESSAGE=0.001, NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Thu, 18 May 2006 23:09:15 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k4J69E2C010948 for ; Thu, 18 May 2006 23:09:14 -0700 (PDT) (envelope-from swarup.mohalik@gm.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.4/8.12.11) with SMTP id k4J69EOe090129 for ; Thu, 18 May 2006 23:09:14 -0700 (PDT) (envelope-from swarup.mohalik@gm.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006051823091424748 for ; Thu, 18 May 2006 23:09:14 -0700 X-Original-Received: from ahgmler3.imr.gm.com (192.85.154.103) by mailgate-external1.sri.com with SMTP; 19 May 2006 06:09:13 -0000 X-Original-Received: from ahgmlir2.imr.gm.com (ahgmlir2-2.imr.gm.com [192.85.154.170]) by ahgmler3.imr.gm.com (8.13.6/8.12.10) with ESMTP id k4J6963T000765 for ; Fri, 19 May 2006 02:09:06 -0400 X-Original-Received: from ahgmlir2.imr.gm.com (localhost [127.0.0.1]) by ahgmlir2.imr.gm.com (8.13.6/8.12.10) with ESMTP id k4J68hoH024871 for ; Fri, 19 May 2006 02:08:43 -0400 X-Original-Received: from usabhmg02.mail.gm.com (USABHMG02.mail.gm.com [164.56.166.171]) by ahgmlir2.imr.gm.com (8.13.6/8.12.10) with ESMTP id k4J68hSk024866 for ; Fri, 19 May 2006 02:08:43 -0400 To: sal-help@csl.sri.com MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.4 HF535 September 07, 2005 Message-ID: From: swarup.mohalik@gm.com Date: Fri, 19 May 2006 11:38:36 +0530 X-MIMETrack: Serialize by Router on USABHMG02/G/GMSERVER/GMC(Release 6.5.4FP1 HF637|March 28, 2006) at 05/19/2006 02:08:44 AM, Serialize complete at 05/19/2006 02:08:44 AM Content-Type: multipart/alternative; boundary="=_alternative 0021BF1365257173_=" X-Mailman-Approved-At: Fri, 19 May 2006 09:22:34 -0700 Subject: [SAL-HELP] Problem in constraints X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 19 May 2006 06:09:15 -0000 This is a multipart message in MIME format. --=_alternative 0021BF1365257173_= Content-Type: text/plain; charset="US-ASCII" Here is a simple SAL context with a simple theorem. del : CONTEXT= BEGIN State : TYPE = {on, off}; delta : {x : REAL | x > 0}; K : INTEGER = 2; main : MODULE= BEGIN LOCAL state : State LOCAL val : REAL INITIALIZATION state = off; val = 3 TRANSITION [ state = off --> val' = val - delta * val [] state = off AND val <= 0 --> state' = on [] state = on --> val' = val + delta * K [] state = on AND val > 8 --> state' = off ] END; th : THEOREM main |- G(val < 8); END The output of sal-inf-bmc --verbose=3 --iterative del th is Counterexample: ======================== Global Constraints ======================== delta > 0; 3 >= 3 * delta + 8; ======================== Path ======================== Step 0: --- System Variables (assignments) --- state = off val = 3 ------------------------ Transition Information: (module instance at [Context: del, line(32), column(15)] transition at [Context: del, line(17), column(6)]) ------------------------ Step 1: --- System Variables (assignments) --- state = off val = delta * 3 * -1 + 3 total execution time: 0.84 secs The set of global constraints is NOT CONSISTENT. Could someone tell me if and where I am wrong. Thanks in advance, ----------------------- Swarup Mohalik --=_alternative 0021BF1365257173_= Content-Type: text/html; charset="US-ASCII"
Here is a simple SAL context with a simple theorem.

del : CONTEXT=
BEGIN
        State : TYPE = {on, off};

        delta : {x : REAL | x > 0};
        K : INTEGER = 2;

        main : MODULE=
        BEGIN
                LOCAL state : State
                LOCAL val : REAL

                INITIALIZATION
                        state = off; val = 3
                TRANSITION
                [
                        state = off -->
                                val' = val - delta * val
                        []
                        state = off AND val <= 0 -->
                                state' = on
                        []
                        state = on  -->
                                val' = val + delta * K
                        []
                        state = on AND val > 8 -->
                                state' = off
                ]

        END;

        th : THEOREM main |- G(val < 8);

END

The output of
        sal-inf-bmc --verbose=3 --iterative  del th
is
Counterexample:
========================
Global Constraints
========================
delta > 0;
3 >= 3 * delta + 8;

========================
Path
========================
Step 0:
--- System Variables (assignments) ---
state = off
val = 3
------------------------
Transition Information:
(module instance at [Context: del, line(32), column(15)]
  transition at [Context: del, line(17), column(6)])
------------------------
Step 1:
--- System Variables (assignments) ---
state = off
val = delta * 3 * -1 + 3
total execution time: 0.84 secs


The set of global constraints is NOT CONSISTENT.

Could someone tell me if and where I am wrong.

Thanks in advance,
-----------------------
Swarup Mohalik --=_alternative 0021BF1365257173_=-- From bruno@csl.sri.com Fri May 19 10:46:48 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44 autolearn=disabled version=3.1.1 date=Fri, 19 May 2006 10:46:49 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.4/8.13.4) with ESMTP id k4JHkmCn026176 for ; Fri, 19 May 2006 10:46:48 -0700 (PDT) (envelope-from bruno@csl.sri.com) X-Original-Received: from [130.107.15.210] (box.csl.sri.com [130.107.15.210]) by mx1.csl.sri.com (8.13.4/8.12.11) with ESMTP id k4JHkm54050360; Fri, 19 May 2006 10:46:48 -0700 (PDT) (envelope-from bruno@csl.sri.com) Message-ID: <446E0488.1070803@csl.sri.com> Date: Fri, 19 May 2006 10:46:48 -0700 From: Bruno Dutertre User-Agent: Mozilla Thunderbird 0.7.3 (X11/20040803) X-Accept-Language: en-us, en MIME-Version: 1.0 To: swarup.mohalik@gm.com Subject: Re: [SAL-HELP] Problem in constraints References: In-Reply-To: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 19 May 2006 17:46:49 -0000 swarup.mohalik@gm.com wrote: > Here is a simple SAL context with a simple theorem. > > del : CONTEXT= > BEGIN > State : TYPE = {on, off}; > > delta : {x : REAL | x > 0}; > K : INTEGER = 2; > > main : MODULE= > BEGIN > LOCAL state : State > LOCAL val : REAL > > INITIALIZATION > state = off; val = 3 > TRANSITION > [ > state = off --> > val' = val - delta * val > [] > state = off AND val <= 0 --> > state' = on > [] > state = on --> > val' = val + delta * K > [] > state = on AND val > 8 --> > state' = off > ] > > END; > > th : THEOREM main |- G(val < 8); > > END > > The output of > sal-inf-bmc --verbose=3 --iterative del th > is > Counterexample: > ======================== > Global Constraints > ======================== > delta > 0; > 3 >= 3 * delta + 8; > > ======================== > Path > ======================== > Step 0: > --- System Variables (assignments) --- > state = off > val = 3 > ------------------------ > Transition Information: > (module instance at [Context: del, line(32), column(15)] > transition at [Context: del, line(17), column(6)]) > ------------------------ > Step 1: > --- System Variables (assignments) --- > state = off > val = delta * 3 * -1 + 3 > total execution time: 0.84 secs > > > The set of global constraints is NOT CONSISTENT. > > Could someone tell me if and where I am wrong. > > Thanks in advance, > ----------------------- > Swarup Mohalik Swarup, You are right. The constaints are not consistent. The problem is caused by the presence of a non-linear expression in your SAL module (so it's not as simple as it may look). state = off --> val' = val - delta * val The current version of ICS has some experimental features for dealing with non-linear arithmetic, but these are far from complete. The ICS incompleteness can cause incorrect counterexamples to be reported. That's what happens in your example. What may be a bit confusing is that all the expressions look linear when pretty-printed by SAL, but internally there are non-linear terms involved. We plan to address these issues with non-linear arithmetic in the future. Right now, the simplest solution is to avoid nonlinear arithmetic if you can. Bruno --- Bruno Dutertre | bruno@csl.sri.com CSL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717 From a.simons@dcs.shef.ac.uk Wed Jun 28 07:34:34 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=none autolearn=disabled version=3.1.1 date=Wed, 28 Jun 2006 07:34:35 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k5SEYXOL036190 for ; Wed, 28 Jun 2006 07:34:34 -0700 (PDT) (envelope-from a.simons@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k5SEYWqZ024408 for ; Wed, 28 Jun 2006 07:34:33 -0700 (PDT) (envelope-from a.simons@dcs.shef.ac.uk) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006062807343213422 for ; Wed, 28 Jun 2006 07:34:32 -0700 X-Original-Received: from marmot.shef.ac.uk (143.167.1.4) by mailgate-external1.sri.com with SMTP; 28 Jun 2006 14:34:30 -0000 X-Original-Received: from holly.dcs.shef.ac.uk ([143.167.8.1]) by marmot.shef.ac.uk with esmtp (Exim 4.52) id 1Fvb7c-0004kM-R9 for sal-help@csl.sri.com; Wed, 28 Jun 2006 15:34:29 +0100 X-Original-Received: from [143.167.8.2] (ivy.dcs.shef.ac.uk [143.167.8.2]) by holly.dcs.shef.ac.uk (8.13.6+Sun/8.13.6) with ESMTP id k5SEYRRQ007009; Wed, 28 Jun 2006 15:34:28 +0100 (BST) Message-ID: <44A29373.1060209@dcs.shef.ac.uk> Date: Wed, 28 Jun 2006 15:34:27 +0100 From: Anthony Simons User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.12) Gecko/20050928 X-Accept-Language: en-us, en MIME-Version: 1.0 To: sal-help@csl.sri.com, Anthony Simons Content-Type: multipart/mixed; boundary="------------090608080605020904010208" X-S0phie-Scan: yes X-Mailman-Approved-At: Wed, 28 Jun 2006 08:24:23 -0700 Cc: Subject: [SAL-HELP] Countable sets X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 28 Jun 2006 14:34:36 -0000 This is a multi-part message in MIME format. --------------090608080605020904010208 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Dear SAL helpers, I'm still trying to work out how to implement countable sets. The attached context file "bitset.sal" implements sets as bit-vectors. However, in order to allow the counting of bits (via the recursive size_aux), the index-type of the bitset must be numerical. Ideally, I'd like to use any scalar type T as the index type. To do this, I imagine using some kind of cache array: rank : ARRAY T OF NATURAL to store the mappings from elements to indices. However, I cannot for the life of me work out how to initialise 'rank' to a unique number for each T element. If you can help me to solve this, that would be much appreciated. Best wishes, -- Tony Simons (with John Derrick and Siobha'n North) --------------090608080605020904010208 Content-Type: text/plain; name="bitset.sal" Content-Transfer-Encoding: 7bit Content-Disposition: inline; filename="bitset.sal" bitset{T : TYPE; N : NATURAL} : CONTEXT = BEGIN %% A bitset is a bit-vector of length N, indexed from 1..N. %% It is used to model a set, whose elements all have a unique %% rank in the range 1..N. The advantage of this encoding is %% that you can recursively count the elements in a set, in a %% way that the SAL toolset can guarantee to terminate. Range : TYPE = [1..N]; %% Rank : TYPE = ARRAY T OF Range; %% rank : Rank = ... %% %% How can you initialise rank to a unique Range value for each %% distinct scalar value T ? Set : TYPE = ARRAY Range OF BOOLEAN; empty_set : Set = [[i : Range] FALSE]; full_set : Set = [[i : Range] TRUE]; size_aux(set : Set, n : NATURAL, s : Range) : Range = IF n = 0 THEN s ELSIF set[n] THEN size_aux(set, n-1, s+1) ELSE size_aux(set, n-1, s) ENDIF; size?(set : Set) : NATURAL = size_aux(set, N, 0); contains? (set : Set, i : Range) : BOOLEAN = set[i]; empty? (set : Set) : BOOLEAN = (FORALL (i : Range) : NOT set[i]); insert (set : Set, i : Range) : Set = set WITH [i] := TRUE; remove (set : Set, i : Range) : Set = set WITH [i] := FALSE; union (aset : Set, bset : Set) : Set = [[i : Range] aset[i] OR bset[i]]; intersection (aset : Set, bset : Set) : Set = [[i : Range] aset[i] AND bset[i]]; difference (aset : Set, bset : Set) : Set = [[i : Range] aset[i] AND NOT bset[i]]; END --------------090608080605020904010208-- From rmbradfo@rockwellcollins.com Mon Jul 31 07:47:39 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=HTML_MESSAGE=0.001, NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Mon, 31 Jul 2006 07:47:40 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k6VEldDZ020541 for ; Mon, 31 Jul 2006 07:47:39 -0700 (PDT) (envelope-from rmbradfo@rockwellcollins.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k6VEldJ3008374 for ; Mon, 31 Jul 2006 07:47:39 -0700 (PDT) (envelope-from rmbradfo@rockwellcollins.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006073107473810920 for ; Mon, 31 Jul 2006 07:47:38 -0700 X-Original-Received: from fw02.rockwellcollins.com (205.175.225.45) by mailgate-external1.sri.com with SMTP; 31 Jul 2006 14:47:36 -0000 X-Original-Received: by fw02.Rockwellcollins.com; id JAA14270; Mon, 31 Jul 2006 09:47:30 -0500 (CDT) From: X-Original-Received: from nodnsquery(131.198.169.131) by fw02.rockwellcollins.com via smap (V5.5) id xma014013; Mon, 31 Jul 06 09:46:29 -0500 X-Original-Received: from vs01.rockwellcollins.com (localhost [127.0.0.1]) by localhost.rockwellcollins.com (Postfix) with ESMTP id 2EEFA318B2 for ; Mon, 31 Jul 2006 09:46:29 -0500 (CDT) X-Original-Received: from crnotes.rockwellcollins.com (crnotes.rockwellcollins.com [131.198.64.150]) by vs01.rockwellcollins.com (Postfix) with ESMTP id ED1E8318AD for ; Mon, 31 Jul 2006 09:46:28 -0500 (CDT) To: sal-help@csl.sri.com MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.2 June 01, 2004 Message-ID: Date: Mon, 31 Jul 2006 09:46:25 -0500 X-MIMETrack: Serialize by Router on CollinsCRSMTP01/CedarRapids/Collins/Rockwell(Release 6.5.4FP3 HF82|May 19, 2006) at 07/31/2006 09:46:28 AM, Serialize complete at 07/31/2006 09:46:28 AM Content-Type: multipart/alternative; boundary="=_alternative 005127A8862571BC_=" X-Mailman-Approved-At: Mon, 31 Jul 2006 09:05:21 -0700 Subject: [SAL-HELP] Syntax for defining (and initializing) an array of constants. X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 31 Jul 2006 14:47:40 -0000 This is a multipart message in MIME format. --=_alternative 005127A8862571BC_= Content-Type: text/plain; charset="US-ASCII" I'm wanting to find out the syntax for defining (and initializing) an array of constants. Is there a one-step define/initialization statement one can use? I have not figured it out from the documentation. Thanks, --Richard Bradford --=_alternative 005127A8862571BC_= Content-Type: text/html; charset="US-ASCII"
I'm wanting to find out the syntax for defining (and initializing) an array of constants.  Is there a one-step define/initialization statement one can use?  I have not figured it out from the documentation.

Thanks,
--Richard Bradford
--=_alternative 005127A8862571BC_=-- From demoura@csl.sri.com Mon Jul 31 09:19:01 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44,AWL=0.039, HTML_MESSAGE=0.001 autolearn=disabled version=3.1.1 date=Mon, 31 Jul 2006 09:19:02 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k6VGJ1Cq023584 for ; Mon, 31 Jul 2006 09:19:01 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.2] (ovc-170.csl.sri.com [130.107.97.170]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k6VGJ1eb016366; Mon, 31 Jul 2006 09:19:01 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: multipart/alternative; boundary=Apple-Mail-2--38117194 Message-Id: <9E80946E-8311-48BE-B978-FF90234F2CD0@csl.sri.com> From: Leonardo de Moura Subject: Re: [SAL-HELP] Syntax for defining (and initializing) an array of constants. Date: Mon, 31 Jul 2006 09:19:01 -0700 To: "" X-Mailer: Apple Mail (2.752.2) Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 31 Jul 2006 16:19:02 -0000 --Apple-Mail-2--38117194 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Hi Richard, You should use an array literal. For example, if you want the array [0]=1, [1]=3, [2]=-1, and [3] = 4 then you should write [ [ i: [0..3] ] IF i = 0 THEN 1 ELSIF i = 1 THEN 3 ELSIF i = 2 THEN -1 ELSE 4 ] Another example, if you want a constant array with domain [0..10] and the value 0 in every index. [ [ i : [0..10] ] 0 ] Cheers, Leonardo On Jul 31, 2006, at 7:46 AM, wrote: > > I'm wanting to find out the syntax for defining (and initializing) > an array of constants. Is there a one-step define/initialization > statement one can use? I have not figured it out from the > documentation. > > Thanks, > --Richard Bradford --Apple-Mail-2--38117194 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1 Hi Richard,

You should use an array = literal. For example, if you
want the array=A0 =A0[0]=3D1, = [1]=3D3, [2]=3D-1, and [3] =3D 4 then you = should
write

[ [ i: [0..3] ]
=A0= IF=A0 =A0=A0 =A0=A0 =A0i =3D 0 THEN 1
=A0 ELSIF i =3D 1 THEN = 3
=A0 ELSIF i =3D 2 THEN -1
=A0 ELSE =A0 =A0=A0 =A0=A0= =A0=A0 =A0=A0 =A0=A0 =A0=A0 =A04
]

Another example, if you = want a constant array with domain [0..10] and
the value=A00 in = every index.

[ = [ i : [0..10] ] 0 ]

Cheers,
Leonardo

= --Apple-Mail-2--38117194-- From lucs12@gmail.com Mon Jul 31 10:44:27 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=2.0 required=4.0 tests=AWL=-0.069,DK_SIGNED=0.001, DK_VERIFIED=-0.001,HTML_10_20=0.945,HTML_MESSAGE=0.001, SUBJ_ALL_CAPS=1.166 autolearn=disabled version=3.1.1 date=Mon, 31 Jul 2006 10:44:27 -0700 X-Spam-Level: ** X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k6VHiRxV025710 for ; Mon, 31 Jul 2006 10:44:27 -0700 (PDT) (envelope-from lucs12@gmail.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k6VHiR03023231 for ; Mon, 31 Jul 2006 10:44:27 -0700 (PDT) (envelope-from lucs12@gmail.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006073110442622625 for ; Mon, 31 Jul 2006 10:44:26 -0700 X-Original-Received: from nf-out-0910.google.com (64.233.182.185) by mailgate-external1.sri.com with SMTP; 31 Jul 2006 17:44:26 -0000 X-Original-Received: by nf-out-0910.google.com with SMTP id k26so711154nfc for ; Mon, 31 Jul 2006 10:44:24 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:sender:to:subject:mime-version:content-type:x-google-sender-auth; b=G0x5iM2slyLWFWzTHZ4NibU1Wc6V9DcU3QflFNaG2uOJiDNmq8wLsnhPZbVEQqqbOO2sq0fSRu0tE/zsiifV2dftmpTzjHFdiAyDxgbQRTFknirnzsLTXqcXcE1hQss3t6DhFH1TifogHlCqY9mEt4kXyMbO9FFJ7XcowhhY9K0= X-Original-Received: by 10.78.145.5 with SMTP id s5mr622690hud; Mon, 31 Jul 2006 10:44:22 -0700 (PDT) X-Original-Received: by 10.78.123.18 with HTTP; Mon, 31 Jul 2006 10:44:22 -0700 (PDT) Message-ID: Date: Mon, 31 Jul 2006 18:44:22 +0100 From: "Lucian-Mircea Patcas" Sender: lucs12@gmail.com To: sal-help@csl.sri.com MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_76230_7757037.1154367862662" X-Google-Sender-Auth: a45b4416b791a951 X-Mailman-Approved-At: Mon, 31 Jul 2006 11:10:38 -0700 Subject: [SAL-HELP] OBLIGATION | CLAIM | LEMMA | THEOREM X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 31 Jul 2006 17:44:27 -0000 ------=_Part_76230_7757037.1154367862662 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi there, Is there any actual difference between these assertion forms? Or it is just a way to better categorise the properties to be proved? Thanks, Lucian ------=_Part_76230_7757037.1154367862662 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi there,

Is there any actual difference between these assertion forms? Or it is just a way to better categorise the properties to be proved?

Thanks,
Lucian
------=_Part_76230_7757037.1154367862662-- From demoura@csl.sri.com Mon Jul 31 11:16:00 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.4 required=4.0 tests=ALL_TRUSTED=-1.44,AWL=0.038 autolearn=disabled version=3.1.1 date=Mon, 31 Jul 2006 11:16:00 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k6VIG0DT026382 for ; Mon, 31 Jul 2006 11:16:00 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [130.107.14.50] (washington.csl.sri.com [130.107.14.50]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k6VIFxj5025710; Mon, 31 Jul 2006 11:16:00 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL-HELP] OBLIGATION | CLAIM | LEMMA | THEOREM Date: Mon, 31 Jul 2006 11:15:59 -0700 To: "Lucian-Mircea Patcas" X-Mailer: Apple Mail (2.752.2) Cc: sal-help@csl.sri.com X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 31 Jul 2006 18:16:00 -0000 Hi Lucian, > Is there any actual difference between these assertion forms? No, there is no difference. Cheers, Leonardo. From David.Friggens@mcs.vuw.ac.nz Wed Aug 2 03:56:21 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.0 required=4.0 tests=none autolearn=disabled version=3.1.1 date=Wed, 02 Aug 2006 03:56:22 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k72AuL3l075113 for ; Wed, 2 Aug 2006 03:56:21 -0700 (PDT) (envelope-from David.Friggens@mcs.vuw.ac.nz) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k72AuIeV087197 for ; Wed, 2 Aug 2006 03:56:20 -0700 (PDT) (envelope-from David.Friggens@mcs.vuw.ac.nz) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006080203562001397 for ; Wed, 02 Aug 2006 03:56:20 -0700 X-Original-Received: from kaukau.mcs.vuw.ac.nz (130.195.5.20) by mailgate-external1.sri.com with SMTP; 2 Aug 2006 10:56:19 -0000 X-Original-Received: from bats.mcs.vuw.ac.nz (bats.mcs.vuw.ac.nz [130.195.5.13]) by kaukau.mcs.vuw.ac.nz (8.13.6.20060614/8.13.3) with ESMTP id k72AuHrv027868 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Wed, 2 Aug 2006 22:56:17 +1200 (NZST) X-Original-Received: from [192.168.17.15] ([202.154.144.252]) (authenticated bits=0) by bats.mcs.vuw.ac.nz (8.13.6.20060614/8.13.3) with ESMTP id k72AuFPg023624 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Wed, 2 Aug 2006 22:56:16 +1200 (NZST) From: David Friggens To: sal-help@csl.sri.com Date: Wed, 2 Aug 2006 22:56:55 +1200 User-Agent: KMail/1.9.3 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200608022256.55761.david@mcs.vuw.ac.nz> X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-2.1.2 (kaukau.mcs.vuw.ac.nz [130.195.5.20]); Wed, 02 Aug 2006 22:56:17 +1200 (NZST) X-Mailman-Approved-At: Sat, 05 Aug 2006 08:09:24 -0700 Subject: [SAL-HELP] Array elimination X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 02 Aug 2006 10:56:22 -0000 Hi. I've been trying to explore what I can do with sal-inf-bmc and induction, and I'm confused by the need for --enable-ate. I have a system with two properties that fail with an error (can't expand quantifier) with ate; without ate one is proved at depth 5 and the other fails with a segmentation violation exception for depths greater than 3. What exactly does it (--enable-ate) do, and what limitations does it impose? Does it mean that sal-inf-bmc can't handle systems with arrays, or just certain types of arrays? If it's required due to a limitation of ICS is there another solver I can use instead? Thanks David From rmbradfo@rockwellcollins.com Thu Aug 10 12:35:51 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=HTML_MESSAGE=0.001, NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Thu, 10 Aug 2006 12:35:53 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k7AJZpM1030551 for ; Thu, 10 Aug 2006 12:35:51 -0700 (PDT) (envelope-from rmbradfo@rockwellcollins.com) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k7AJZlwa075921 for ; Thu, 10 Aug 2006 12:35:51 -0700 (PDT) (envelope-from rmbradfo@rockwellcollins.com) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006081012355131240 for ; Thu, 10 Aug 2006 12:35:51 -0700 X-Original-Received: from fw01.rockwellcollins.com (205.175.225.1) by mailgate-external2.sri.com with SMTP; 10 Aug 2006 19:35:49 -0000 X-Original-Received: by fw01.rockwellcollins.com; id OAA09928; Thu, 10 Aug 2006 14:35:44 -0500 (CDT) From: X-Original-Received: from nodnsquery(131.198.169.131) by fw01.rockwellcollins.com via smap (V5.5) id xma009488; Thu, 10 Aug 06 14:35:07 -0500 X-Original-Received: from vs01.rockwellcollins.com (localhost [127.0.0.1]) by localhost.rockwellcollins.com (Postfix) with ESMTP id 57E573187B; Thu, 10 Aug 2006 14:35:10 -0500 (CDT) X-Original-Received: from crnotes.rockwellcollins.com (crnotes.rockwellcollins.com [131.198.64.150]) by vs01.rockwellcollins.com (Postfix) with ESMTP id 34E1A31873; Thu, 10 Aug 2006 14:35:10 -0500 (CDT) To: sal-help@csl.sri.com MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.2 June 01, 2004 Message-ID: Date: Thu, 10 Aug 2006 14:35:06 -0500 X-MIMETrack: Serialize by Router on CollinsCRSMTP01/CedarRapids/Collins/Rockwell(Release 6.5.4FP3 HF82|May 19, 2006) at 08/10/2006 02:35:08 PM Content-Type: multipart/mixed; boundary="=_mixed 006B9567862571C6_=" X-Mailman-Approved-At: Fri, 11 Aug 2006 09:14:30 -0700 Cc: demoura@csl.sri.com Subject: [SAL-HELP] Floor or ceiling functions in SAL? X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 10 Aug 2006 19:35:54 -0000 --=_mixed 006B9567862571C6_= Content-Type: multipart/alternative; boundary="=_alternative 006B9569862571C6_=" --=_alternative 006B9569862571C6_= Content-Type: text/plain; charset="US-ASCII" I would like to use a constant that is a straightforward function of other constants, with a ceiling function applied to the value. Since it is clearly a constant, I'd like to use it as such -- i.e. I'd like to check an assertion in which it is multiplied by some integer variable, and I'd like to avoid having SAL give me a "nonlinear problem" error. I asked my colleague, Steve Miller, if he knew of some easy way to take the integer portion of a real number, and he sent me the following attempt, which unfortunately gives the "nonlinear problem" error. Are we missing something obvious? --Richard Bradford Rockwell Collins --=_alternative 006B9569862571C6_= Content-Type: text/html; charset="US-ASCII"
I would like to use a constant that is a straightforward function of other constants, with a ceiling function applied to the value.  Since it is clearly a constant, I'd like to use it as such -- i.e. I'd like to check an assertion in which it is multiplied by some integer variable, and I'd like to avoid having SAL give me a "nonlinear problem" error.

I asked my colleague, Steve Miller, if he knew of some easy way to take the integer portion of a real number, and he sent me the following attempt, which unfortunately gives the "nonlinear problem" error.

Are we missing something obvious?

--Richard Bradford
Rockwell Collins


--=_alternative 006B9569862571C6_=-- --=_mixed 006B9567862571C6_= Content-Type: application/octet-stream; name="Floor.sal" Content-Disposition: attachment; filename="Floor.sal" Content-Transfer-Encoding: base64 Rmxvb3I6IENPTlRFWFQgPQ0KQkVHSU4NCg0KCQkNCglyMSA6IFJFQUwgPSA4LjA7DQoJcjIgOiBS RUFMID0gMi4wOw0KCQ0KCWkxIDoge2k6IElOVEVHRVIgfCBpIDw9IHIxL3IyIEFORCBpID4gcjEv cjIgLSAxfTsNCiANCiBtYWluIDogTU9EVUxFID0gDQogICAgQkVHSU4NCiAgICAJTE9DQUwNCiAg ICAJCWkyLCBpMyA6IElOVEVHRVINCiAgICAJSU5JVElBTElaQVRJT04NCiAgICAJCWkyID0gNDsN CiAgICAJCWkzID0gaTIgKiBpMTsNCiAgICAgRU5EOw0KIA0KICAgcHJvcCA6IFRIRU9SRU0gbWFp biB8LSBBRyhpMyA9IDEyKSA7IA0KICAgDQpFTkQNCiAgIA== --=_mixed 006B9567862571C6_=-- From rti@look.ca Fri Aug 11 15:24:30 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=2.7 required=4.0 tests=AWL=0.715,HTML_MESSAGE=0.001, RCVD_IN_SORBS_DUL=1.988 autolearn=disabled version=3.1.1 date=Fri, 11 Aug 2006 15:24:38 -0700 X-Spam-Level: ** X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k7BMOUsE066707 for ; Fri, 11 Aug 2006 15:24:30 -0700 (PDT) (envelope-from rti@look.ca) X-Original-Received: from mailgate-external2.SRI.COM (mailgate-external2.SRI.COM [128.18.85.102]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k7BMOQ8w086256 for ; Fri, 11 Aug 2006 15:24:30 -0700 (PDT) (envelope-from rti@look.ca) X-Original-Received: from mailgate-external2.sri.com ([127.0.0.1]) by mailgate-external2.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006081115242929873 for ; Fri, 11 Aug 2006 15:24:29 -0700 X-Original-Received: from 209-161-223-232.dsl.look.ca (HELO 169.254.189.170) (209.161.223.232) by mailgate-external2.sri.com with SMTP; 11 Aug 2006 22:24:14 -0000 Message-ID: <200608111524.MOOPQLJKJR@169.254.189.170> From: "marg moore" To: "sal-help@csl.sri.com" Date: Fri, 11 Aug 2006 15:24:09 -0700 Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_NextPart_000_0034_01C221EC.6C64F7B0" X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Atomic Mail Sender 2.36 X-MimeOLE: Produced by Microsoft MimeOLE V6.00.2800.1165 X-Mailman-Approved-At: Mon, 14 Aug 2006 06:49:14 -0700 Subject: [SAL-HELP] ATTENTION BEA Partners (BEA, WEBSPHERE, CRM, GREAT PLAINS, EXCHANGE, SQL CUSTOMER LISTS) X-BeenThere: sal-help@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list Reply-To: marg moore List-Id: SAL-HELP List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 11 Aug 2006 22:24:38 -0000 ------=_NextPart_000_0034_01C221EC.6C64F7B0 Content-Type: text/plain; charset="iso-8859-1" I'd like to introduce our company, Repharm Technologies, to you. We are a knowledge base company, and we sell contact lists. We have a variety of lists available, from hardware, software, to technology companies, with on average 10 executive contacts per organization. Our lists are continuously maintained to ensure the highest level of accuracy and completeness. We have hundreds of industry leaders as customers today - many who's names you would recognize. If you'd be interested, we could send you a sample of one of our lists complete with summary information, so that you could evaluate our content. I see from your website that you are an Alliance Partner of BEA and wondered if you'd be interested in acquiring a copy of their customer list? Or, if you'd be interested in finding out about the various lists we have available, in preparation for any sales or marketing campaigns that your organization may be considering in future, we'd love to hear from you. Or, perhaps you'd be interested in acquiring your competitors' customer lists? If you'd like more information, please contact Mike Gordon at our Repharm office at (905) 728-6708, or email rti@look.ca Thank you in advance for your consideration, and we look forward to hearing from you. Regards, Margaret Moore Business Development Representative Repharm Technologies ************************************************************************ *** If you would prefer not to receive communications from us in future, please reply to this email with "remove" in the subject line. ------=_NextPart_000_0034_01C221EC.6C64F7B0 Content-Type: text/html; charset="iso-8859-1" E-mail message content
I'd like to introduce our company, Repharm Technologies, to you. We are
a knowledge base company, and we sell contact lists. We have a variety
of lists available, from hardware, software, to technology companies,
with on average 10 executive contacts per organization. Our lists are
continuously maintained to ensure the highest level of accuracy and
completeness. We have hundreds of industry leaders as customers today -
many who's names you would recognize.
 
If you'd be interested, we could send you a sample of one of our lists
complete with summary information, so that you could evaluate our
content.
 
I see from your website that you are an Alliance Partner of BEA
 and wondered if you'd be interested in acquiring a copy of
their customer list?
Or, if you'd be interested in finding out about the various lists we
have available, in preparation for any sales or marketing campaigns that
your organization may be considering in future, we'd love to hear from
you. Or, perhaps you'd be interested in acquiring your competitors'
customer lists?
 
If you'd like more information, please contact Mike Gordon at our
Repharm office at (905) 728-6708, or email rti@look.ca
 
Thank you in advance for your consideration, and we look forward to
hearing from you.
 
Regards,
 
Margaret Moore
Business Development Representative
Repharm Technologies
 
************************************************************************
***
 
If you would prefer not to receive communications from us in future,
please reply to this email with "remove" in the subject line.
 
 

--- Sent by UNREGISTERED VERSION of Atomic Mail Sender ------=_NextPart_000_0034_01C221EC.6C64F7B0-- From spmiller@rockwellcollins.com Mon Aug 14 06:28:54 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.6 required=4.0 tests=NO_REAL_NAME=0.55 autolearn=disabled version=3.1.1 date=Mon, 14 Aug 2006 06:28:57 -0700 X-Spam-Level: X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29]) by postal.csl.sri.com (8.13.6/8.13.4) with ESMTP id k7EDSrI6049852 for ; Mon, 14 Aug 2006 06:28:53 -0700 (PDT) (envelope-from spmiller@rockwellcollins.com) X-Original-Received: from mailgate-external1.SRI.COM (mailgate-external1.SRI.COM [128.18.85.101]) by mx1.csl.sri.com (8.13.6/8.12.11) with SMTP id k7EDSlgd034521 for ; Mon, 14 Aug 2006 06:28:53 -0700 (PDT) (envelope-from spmiller@rockwellcollins.com) X-Original-Received: from mailgate-external1.sri.com ([127.0.0.1]) by mailgate-external1.SRI.COM (SMSSMTP 4.1.11.41) with SMTP id M2006081406285307677 for ; Mon, 14 Aug 2006 06:28:53 -0700 X-Original-Received: from fw01.rockwellcollins.com (205.175.225.1) by mailgate-external1.sri.com with SMTP; 14 Aug 2006 13:28:52 -0000 X-Original-Received: by fw01.rockwellcollins.com; id IAA25730; Mon, 14 Aug 2006 08:28:50 -0500 (CDT) From: