From srihari.sukumaran@philips.com Wed Feb 22 03:23:20 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 k1MBNK6H025365 for ; Wed, 22 Feb 2006 03:23:20 -0800 (PST) (envelope-from srihari.sukumaran@philips.com) 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 k1MBmpH8006344 for ; Wed, 22 Feb 2006 03:48:51 -0800 (PST) (envelope-from srihari.sukumaran@philips.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 M2006022203485016579 for ; Wed, 22 Feb 2006 03:48:50 -0800 X-Original-Received: from gw-eur4.philips.com (161.85.125.10) by mailgate-external1.sri.com with SMTP; 22 Feb 2006 11:48:50 -0000 X-Original-Received: from smtpscan-eur4.philips.com (smtpscan-eur4.mail.philips.com [130.144.57.167]) by gw-eur4.philips.com (Postfix) with ESMTP id 1E3A94974E for ; Wed, 22 Feb 2006 11:48:50 +0000 (UTC) X-Original-Received: from smtpscan-eur4.philips.com (localhost [127.0.0.1]) by localhost.philips.com (Postfix) with ESMTP id DC62859 for ; Wed, 22 Feb 2006 11:48:49 +0000 (GMT) X-Original-Received: from smtprelay-eur2.philips.com (smtprelay-eur2.philips.com [130.144.57.171]) by smtpscan-eur4.philips.com (Postfix) with ESMTP id BAD1557 for ; Wed, 22 Feb 2006 11:48:49 +0000 (GMT) X-Original-Received: from ehvrmh02.diamond.philips.com (ehvrmh02-srv.diamond.philips.com [130.139.27.125]) by smtprelay-eur2.philips.com (Postfix) with ESMTP id 9EB2936 for ; Wed, 22 Feb 2006 11:48:49 +0000 (GMT) To: sal@csl.sri.com MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.0.3 September 26, 2003 From: Srihari Sukumaran Message-ID: Date: Wed, 22 Feb 2006 17:17:31 +0530 X-MIMETrack: Serialize by Router on ehvrmh02/H/SERVER/PHILIPS(Release 6.5.3FP1HF291 | September 19, 2005) at 22/02/2006 12:47:32, Serialize complete at 22/02/2006 12:47:32 Content-Type: multipart/alternative; boundary="=_alternative 0040E4436525711D_=" 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.118,HTML_MESSAGE=0.001 autolearn=no version=2.64 date=Wed, 22 Feb 2006 03:23:20 -0800 X-Mailman-Approved-At: Wed, 22 Feb 2006 09:13:19 -0800 Subject: [SAL] Assignments/Definitions in SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Feb 2006 11:23:21 -0000 This is a multipart message in MIME format. --=_alternative 0040E4436525711D_= Content-Type: text/plain; charset="US-ASCII" Hello I had a couple of questions regarding (guarded) assignements in SAL: 1) Does the ";" represent a sequencing of assignments/commands in INITIALIZATION or TRANSITION sections? In A1;A2 is it A2 always performed after A1? 2) For a guarded command does the semantics state that all the assignments in "Assignements" are executed atomically? Or can actions from other concurrently composed modules be interleaved with these? eg: if M1 is "G -> A1 ; A2" and M2 is "A3" can it happen that A3 is executed between A1 and A2 in M1 [] M2? Thank you Srihari Sukumaran Philips Research India - Bangalore Philips Innovation Campus No 1, Murphy Road, Ulsoor, Bangalore 560008. INDIA Tel: +91 80 25579000 ext 1011 --=_alternative 0040E4436525711D_= Content-Type: text/html; charset="US-ASCII"
Hello

I had a couple of questions regarding (guarded) assignements in SAL:

1) Does the ";" represent a sequencing of assignments/commands in INITIALIZATION or TRANSITION sections? In A1;A2 is it A2 always performed after A1?

2) For a guarded command does the semantics state that all the assignments in "Assignements" are executed atomically? Or can actions from other concurrently composed modules be interleaved with these? eg: if  M1 is "G -> A1 ; A2" and M2 is "A3" can it happen that A3 is executed between A1 and A2 in M1 [] M2?

Thank you

Srihari Sukumaran
Philips Research India - Bangalore
Philips Innovation Campus
No 1, Murphy Road, Ulsoor,
Bangalore 560008. INDIA
Tel: +91 80 25579000 ext 1011 --=_alternative 0040E4436525711D_=-- From demoura@csl.sri.com Wed Feb 22 09:20: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 k1MHKh6H036238 for ; Wed, 22 Feb 2006 09:20:43 -0800 (PST) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.5] (ovc-191.csl.sri.com [130.107.97.191]) by mx1.csl.sri.com (8.12.11/8.12.11) with ESMTP id k1MHkGta035817; Wed, 22 Feb 2006 09:46:16 -0800 (PST) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v746.2) Content-Type: multipart/alternative; boundary=Apple-Mail-1--885580151 Message-Id: <8676CA4D-6DA2-4A5A-BE8D-7608B9234936@csl.sri.com> From: Leonardo de Moura Subject: Re: [SAL] Assignments/Definitions in SAL Date: Wed, 22 Feb 2006 09:46:17 -0800 To: Srihari Sukumaran 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.2 required=4.0 tests=AWL=-0.233,HTML_20_30=0.474, HTML_MESSAGE=0.001 autolearn=no version=2.64 date=Wed, 22 Feb 2006 09:20:44 -0800 X-Mailman-Approved-At: Wed, 22 Feb 2006 09:25:51 -0800 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Feb 2006 17:20:44 -0000 --Apple-Mail-1--885580151 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Hi Srihari, > 1) Does the ";" represent a sequencing of assignments/commands in > INITIALIZATION or TRANSITION sections? In A1;A2 is it A2 always > performed after A1? No, A1 and A2 are executed atomically in parallel. > 2) For a guarded command does the semantics state that all the > assignments in "Assignements" are executed atomically? Or can > actions from other concurrently composed modules be interleaved > with these? eg: if M1 is "G -> A1 ; A2" and M2 is "A3" can it > happen that A3 is executed between A1 and A2 in M1 [] M2? No, A1 and A2 are executed also atomically in parallel. Cheers, Leonardo --Apple-Mail-1--885580151 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1 Hi Srihari,

1) Does the ";" = represent a sequencing of assignments/commands in INITIALIZATION or = TRANSITION sections? In A1;A2 is it A2 always performed after A1? =

No,= A1 and A2 are executed atomically in parallel.

2) For a guarded = command does the semantics state that all the assignments in = "Assignements" are executed atomically? Or can actions from other = concurrently composed modules be interleaved with these? eg: if =A0M1 is = "G -> A1 ; A2" and M2 is "A3" can it happen that A3 is executed = between A1 and A2 in M1 [] M2?

No, A1 and A2 are executed = also atomically in parallel.

Cheers,
Leonardo
= --Apple-Mail-1--885580151-- From rimvydas@dcs.qmul.ac.uk Fri Jun 16 04:22:03 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=Fri, 16 Jun 2006 04:22:06 -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 k5GBM3oj062001 for ; Fri, 16 Jun 2006 04:22:03 -0700 (PDT) (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.13.6/8.12.11) with SMTP id k5GBM3Nh002295 for ; Fri, 16 Jun 2006 04:22:03 -0700 (PDT) (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 M2006061604220322149 for ; Fri, 16 Jun 2006 04:22:03 -0700 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; 16 Jun 2006 11:22:00 -0000 X-Original-Received: from host138-37-90-87.dcs.qmul.ac.uk ([138.37.90.87]) by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.62) (envelope-from ) id 1FrCOk-0000yQ-L3; Fri, 16 Jun 2006 12:21:59 +0100 Message-ID: <44929452.1070303@dcs.qmul.ac.uk> Date: Fri, 16 Jun 2006 12:21:54 +0100 From: Rimvydas Ruksenas User-Agent: Thunderbird 1.5.0.4 (Macintosh/20060530) MIME-Version: 1.0 To: sal@csl.sri.com, pvs@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-Mailman-Approved-At: Fri, 16 Jun 2006 08:15:02 -0700 Cc: Subject: [SAL] CfP: 1st Int. Workshop on Formal Methods for Interactive Systems (FMIS 2006) X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 16 Jun 2006 11:22:06 -0000 [Apologizes for multiple receptions] ---------------------------------------------------------------------- Call for Papers ---------------------------------------------------------------------- FMIS 2006 1st International Workshop on FORMAL METHODS FOR INTERACTIVE SYSTEMS Macau SAR China, 31 October 2006 http://fmis.iist.unu.edu/ ********************************************************************** IMPORTANT DATES Submission deadline: 23 July, 2006 Acceptance notification: 10 September, 2006 Final version for the pre-proceedings due: 12 October, 2006 Final version for the ENTCS proceedings due: 1 December, 2006 ********************************************************************** BACKGROUND AND OBJECTIVES Reducing the likelihood of human error in the use of interactive systems is increasingly important: the use of such systems is becoming widespread in applications that demand high reliability due to safety, security, financial or similar considerations. Consequently, the use of formal methods in verifying the correctness of interactive systems should also include analysis of human behaviour in interacting with the interface. The aim of this workshop is to bring together researchers in computer science and cognitive psychology, from both academia and industry, who are interested in developing formal and semi-formal methodologies and tools for the evaluation and verification of interactive systems. The outcome is to establish a worldwide network of researchers interested in applying formal methods to HCI. The workshop will focus on, though will not be restricted to, * general design and verification methodologies based on cognitive psychology as well as application areas such as * mobile devices; * embedded systems; * safety-critical systems; * high-reliability systems; * shared control systems; * digital libraries; * eGovernment; * pervasive systems; * augmented reality. The one-day workshop will feature a one hour presentation by a keynote speaker together with contributed papers that will undergo a peer-review process. Contributed papers may be accepted either for full presentation or short presentation. PUBLICATION Papers accepted as full paper presentations will be published by Elsevier in the series Electronic Notes in Theoretical Computer Science (ENTCS). Papers accepted as short paper presentations will be published in the participants' proceedings at the workshop only. Detailed information on the submission procedure is available below. Publication of a selection of the papers in a journal special issue is also under consideration. INVITED SPEAKER * Harold Thimbleby, University of Wales Swansea, UK SPONSORS AND ORGANISATION IFMIS 2006 will be organised jointly between the International Institute for Software Technology of the United Nations University (UNU-IIST) and the EPSRC Human Error Modelling (HUM) Project of the University of London (QMUL and UCL). UNU-IIST and EPSRC-HUM are also sponsors of ICTAC 2006. SUBMISSION AND PUBLICATION Submissions to the workshop must not have been published or be concurrently considered for publication elsewhere. All submissions will be peer-reviewed and judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the workshop. Papers should be written in English and not exceed 16 pages in ENTCS format. Authors should utilize the ENTCS macro files that have been specially prepared for use with ENTCS. The generic ENTCS package, which contains files common for all volumes in ENTCS and includes several examples, as well as instructions, can be downloaded from http://www.entcs.org/generic.tar.gz. The entcsmacro.sty file in the ENTCS package should be be replaced by the prentcsmacro.sty file, which is specific to FMIS 2006 and can be downloaded from http://www.entcs.org/files/fmis/prentcsmacro.sty. File prentcsmacro.sty has to be renamed entcsmacro.sty. File example.tex has to be used as a template for the paper, making sure that key words are included in the frontmatter section where indicated. Authors also should not use any formatting commands that alter the ENTCS style definitions. This includes the format of Definitions, Lemmas, Theorems, etc., as well as the spacing that is defined by the ENTCS Macros. Authors must submit their papers in pdf format to the website http://confman.iist.unu.edu/FMIS2006/REG-paper/ no later than Sunday 23 July 2006. All queries should be sent to: fmis2006 AT iist.unu.edu. ORGANISERS * Antonio Cerone, UNI-IIST, Macau SAR China * Paul Curzon, Queen Mary, University of London, UK PROGRAM COMMITTEE * Ann Blandford, UCL Interaction Center, UK * Ralph Back, Abo Akademi, Finland * Howard Bowman, University of Kent, UK * George Buchanan, University of Wales Swansea, UK * Antonio Cerone, UNI-IIST, Macau SAR China (Co-chair) * Paul Cairns, UCL Interaction Center, UK * Jose Creissac Campos, University of Minho, Portugal * Paul Curzon, Queen Mary, University of London, UK (Co-chair) * Gavin Doherty, Trinity College, University of Dublin, Ireland * Michael Harrison, University of Newcastle upon Tyne, UK * C. Michael Holloway, NASA Langley Research Center, USA * Chris Johnson, University of Glasgow, UK * Alan Dix, Lancaster University, UK * Li Siu Pan, Macao Polytechnic Institute, Macau SAR China * Peter Lindsay, The University of Queensland, Australia * Philippe Palanque, University of Toulouse III, France * Fabio Paterno, CNR-ISTI, Italy * Rimvydas Ruksenas, Queen Mary, University of London, UK From harryh23@hotmail.com Sat Jun 17 06:53:40 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=MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sat, 17 Jun 2006 06:53: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 k5HDrdCk092244 for ; Sat, 17 Jun 2006 06:53:39 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5HDrUWk039602 for ; Sat, 17 Jun 2006 06:53:39 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061706533907307 for ; Sat, 17 Jun 2006 06:53:39 -0700 X-Original-Received: from bay105-f14.bay105.hotmail.com (HELO hotmail.com) (65.54.224.24) by mailgate-external1.sri.com with SMTP; 17 Jun 2006 13:53:39 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sat, 17 Jun 2006 06:53:39 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sat, 17 Jun 2006 13:53:35 GMT X-Originating-IP: [70.28.235.58] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com From: "harry huang" To: sal@csl.sri.com Date: Sat, 17 Jun 2006 13:53:35 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 17 Jun 2006 13:53:39.0033 (UTC) FILETIME=[6F903C90:01C69215] X-Mailman-Approved-At: Sat, 17 Jun 2006 09:03:14 -0700 Subject: [SAL] Some questions for using SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 17 Jun 2006 13:53:40 -0000 Hi, I have some questions regarding the SAL. 1. Can I write the assertion in the module ? For instance, I want to express "assert(a==b)", how to write it in module as I see the example that the assertion written in the Theorem. 2. Is there way to express the wait condition ? For instance, I want to express the java expression "while ( a != 0) wait();" in SAL . Anway, I saw example that has "sleeping, trying, critical ". Are those keywords SAL reserved keywords or user defined ? 3. How to expression the invariant in SAL ? Does the invariant can be defined in DEFINITION ? 4. Is there "for" loop in SAL ? Thanks. Harry From harryh23@hotmail.com Sat Jun 17 16:12:36 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=MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sat, 17 Jun 2006 16:12: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 k5HNCaG5003445 for ; Sat, 17 Jun 2006 16:12:36 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5HNCasH083159 for ; Sat, 17 Jun 2006 16:12:36 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061716123601200 for ; Sat, 17 Jun 2006 16:12:36 -0700 X-Original-Received: from bay105-f2.bay105.hotmail.com (HELO hotmail.com) (65.54.224.12) by mailgate-external1.sri.com with SMTP; 17 Jun 2006 23:12:35 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sat, 17 Jun 2006 16:12:34 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sat, 17 Jun 2006 23:12:33 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: sal@csl.sri.com Date: Sat, 17 Jun 2006 23:12:33 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 17 Jun 2006 23:12:34.0849 (UTC) FILETIME=[8477A910:01C69263] X-Mailman-Approved-At: Sat, 17 Jun 2006 16:14:02 -0700 Subject: [SAL] A question when using SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 17 Jun 2006 23:12:38 -0000 Hi, I have a question when using SAL. I want to express a process doing in below after try to verify that eventually that i == 100 === int i; for (i = 1; i<100; i++); === So , I made a SAL program in below ==== simple1: CONTEXT = BEGIN process: MODULE = BEGIN OUTPUT i: INTEGER INITIALIZATION i = 1 TRANSITION [ increment: i<100 --> i' = i+1; ] END; th1: THEOREM process |- F(i=100); END ===== But when I used the command "sal-smc simple1 th1", it gave me the error " Error: [Context: simple1, line(6), column(16)]: Finite type representation cannot be generated, type is not finite. Reason: [Context: prelude, line(189), column(20)]: Type is not a bounded subtype of integer, or it was not possible to determine the bound. " Can someone give me some hints ? Thanks. Harry From harryh23@hotmail.com Sat Jun 17 16:14:17 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=MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sat, 17 Jun 2006 16:14:17 -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 k5HNEHN8003621 for ; Sat, 17 Jun 2006 16:14:17 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5HNEGrR083465 for ; Sat, 17 Jun 2006 16:14:17 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061716141601798 for ; Sat, 17 Jun 2006 16:14:16 -0700 X-Original-Received: from bay105-f20.bay105.hotmail.com (HELO hotmail.com) (65.54.224.30) by mailgate-external2.sri.com with SMTP; 17 Jun 2006 23:14:16 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sat, 17 Jun 2006 16:14:16 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sat, 17 Jun 2006 23:14:12 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: sal@csl.sri.com Date: Sat, 17 Jun 2006 23:14:12 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 17 Jun 2006 23:14:16.0029 (UTC) FILETIME=[C0C680D0:01C69263] X-Mailman-Approved-At: Sat, 17 Jun 2006 16:15:33 -0700 Subject: [SAL] Another question when using SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 17 Jun 2006 23:14:17 -0000 Hi, I have another question when using SAL. how can i express the loop in SAL. For instance, "For (i =0; i <10; i++) ....". How to transfer this code into SAL ? Thanks. Harry From David.Friggens@mcs.vuw.ac.nz Sat Jun 17 16:23:18 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=Sat, 17 Jun 2006 16:23:19 -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 k5HNNH0i003977 for ; Sat, 17 Jun 2006 16:23:17 -0700 (PDT) (envelope-from David.Friggens@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.13.6/8.12.11) with SMTP id k5HNNHkc084398 for ; Sat, 17 Jun 2006 16:23:17 -0700 (PDT) (envelope-from David.Friggens@mcs.vuw.ac.nz) 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 M2006061716231702172 for ; Sat, 17 Jun 2006 16:23:17 -0700 X-Original-Received: from kaukau.mcs.vuw.ac.nz (130.195.5.20) by mailgate-external2.sri.com with SMTP; 17 Jun 2006 23:23:16 -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/8.13.3) with ESMTP id k5HNN7rP006495 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Sun, 18 Jun 2006 11:23:08 +1200 (NZST) X-Original-Received: from [192.168.17.15] (202-154-146-37.actrix.co.nz [202.154.146.37]) (authenticated bits=0) by bats.mcs.vuw.ac.nz (8.13.6/8.13.3) with ESMTP id k5HNMut4017839 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Sun, 18 Jun 2006 11:23:03 +1200 (NZST) From: David Friggens To: sal@csl.sri.com Date: Sun, 18 Jun 2006 11:22:28 +1200 User-Agent: KMail/1.9.1 References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200606181122.28509.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]); Sun, 18 Jun 2006 11:23:08 +1200 (NZST) X-Mailman-Approved-At: Sat, 17 Jun 2006 16:25:16 -0700 Cc: harry huang Subject: [SAL] Re: Some questions for using SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 17 Jun 2006 23:23:19 -0000 Hi Harry > I have some questions regarding the SAL. Hopefully I can answer some of your questions. First, I'll point out that SAL is not a procedural language - you define the transitions by writing the changes that happen to the variables. If you want to model some code from a procedural language you'll need to define a program counter variable. Then you can define transitions from location1 to location2, from location2 to location3, etc. The msclock example (in SAL 2.4) is a good example of this. > 1. Can I write the assertion in the module ? For instance, I want to > express "assert(a==b)", how to write it in module as I see the > example that the assertion written in the Theorem. You can put a=b in the guard of the transition, and have another one that goes to an error state. For example pc = locX AND a = b --> pc' = locY and pc = locX AND a /= b --> pc' = locError Then you could test that the module doesn't ever enter the error state: THEOREM system |- G(pc /= locError) > 2. Is there way to express the wait condition ? For instance, I want > to express the java expression "while ( a != 0) wait();" in SAL . You could use a transition like: pc = locX AND a = 0 --> pc' = locY This transition is only enabled if the module is at location locX and a is zero, so if it's at locX and a isn't zero, then it has to wait until a transition becomes enabled (i.e. when a becomes zero). > Anway, I saw example that has "sleeping, trying, critical ". Are > those keywords SAL reserved keywords or user defined ? These are user defined. > 3. How to expression the invariant in SAL ? If you want to prove that a property "p" is an invariant you can use the LTL formula G(p). For example THEOREM system |- G(a <= 5 AND b >= 10). > 4. Is there "for" loop in SAL ? Not explicitly, but you can express it easily. Cheers David From tiwari@csl.sri.com Sat Jun 17 16:51:55 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=Sat, 17 Jun 2006 16:51:56 -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 k5HNptXC004495 for ; Sat, 17 Jun 2006 16:51:55 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from fury.csl.sri.com (fury.csl.sri.com [130.107.5.225]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5HNptCq086575 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Sat, 17 Jun 2006 16:51:55 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from fury.csl.sri.com (fury.csl.sri.com [127.0.0.1]) by fury.csl.sri.com (8.12.10/8.12.10) with ESMTP id k5HNptLD032114; Sat, 17 Jun 2006 16:51:55 -0700 X-Original-Received: from localhost (tiwari@localhost) by fury.csl.sri.com (8.12.10/8.12.10/Submit) with ESMTP id k5HNptLc032110; Sat, 17 Jun 2006 16:51:55 -0700 Date: Sat, 17 Jun 2006 16:51:55 -0700 (PDT) From: Ashish Tiwari To: harry huang Subject: Re: [SAL] A question when using SAL In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Mailman-Approved-At: Sat, 17 Jun 2006 16:52:48 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 17 Jun 2006 23:51:56 -0000 The type "INTEGER" is not bounded; it has infinitely many elements. You will have to replace it by a finite subrange type (e.g. [0..100]) for sal-smc to work on this example. Hope this helps, -Ashish On Sat, 17 Jun 2006, harry huang wrote: > Hi, > > I have a question when using SAL. > > I want to express a process doing in below after try to verify that > eventually that i == 100 > === > int i; > for (i = 1; i<100; i++); > === > > So , I made a SAL program in below > > ==== > simple1: CONTEXT = > BEGIN > > process: MODULE = > BEGIN > OUTPUT i: INTEGER > INITIALIZATION > i = 1 > TRANSITION > [ > increment: > i<100 --> i' = i+1; > ] > END; > > th1: THEOREM process |- F(i=100); > END > ===== > > But when I used the command "sal-smc simple1 th1", it gave me the error > " > Error: [Context: simple1, line(6), column(16)]: Finite type representation > cannot be generated, type is not finite. > Reason: [Context: prelude, line(189), column(20)]: Type is not a bounded > subtype of integer, or it was not possible to determine the bound. > > " > > Can someone give me some hints ? Thanks. > > Harry > > From harryh23@hotmail.com Sun Jun 18 14:02:51 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=-0.138, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:02:51 -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 k5IL2ocv025437 for ; Sun, 18 Jun 2006 14:02:50 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5IL2ofg090768 for ; Sun, 18 Jun 2006 14:02:50 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061814025026283 for ; Sun, 18 Jun 2006 14:02:50 -0700 X-Original-Received: from bay105-f15.bay105.hotmail.com (HELO hotmail.com) (65.54.224.25) by mailgate-external1.sri.com with SMTP; 18 Jun 2006 21:02:48 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sun, 18 Jun 2006 14:02:38 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sun, 18 Jun 2006 21:02:35 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: tiwari@csl.sri.com Subject: Re: [SAL] A question when using SAL Date: Sun, 18 Jun 2006 21:02:35 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 18 Jun 2006 21:02:38.0767 (UTC) FILETIME=[880DB3F0:01C6931A] X-Mailman-Approved-At: Sun, 18 Jun 2006 14:04:52 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:02:51 -0000 Hi, Thanks for information. I modified the program and it is on below: ==== simple1: CONTEXT = BEGIN process: MODULE = BEGIN OUTPUT i: [0..100] -- modified (1) LOCAL high: BOOLEAN -- modified (2) DEFINITION high = i > 100 -- modified (3) INITIALIZATION i = 1 TRANSITION [ i<100 --> i' = i+1; ] END; th1: THEOREM process |- F(i=110); -- modified (4) END ==== (1), (2), (3), (4) are the modified code. This code passed the compiler. But I have some two issues do not understand. First, for the modification (4), it should not hold because in the transition, the loop stops incrementing i by 1 if i reach 100. But when I used "sal-smc simple1 th1", it still said proved. Second, I saw there is way to define invariant in the "DEFINITION", so I define a invariant in modification (3). But why the using of "sal-smc simple1 th1" still said it is proved ? Can someone gives me hints ? Thanks. harry >From: Ashish Tiwari >To: harry huang >CC: sal@csl.sri.com >Subject: Re: [SAL] A question when using SAL >Date: Sat, 17 Jun 2006 16:51:55 -0700 (PDT) > > >The type "INTEGER" is not bounded; it has infinitely >many elements. >You will have to replace it by a finite subrange type >(e.g. [0..100]) for sal-smc to work on this example. > >Hope this helps, >-Ashish > >On Sat, 17 Jun 2006, harry huang wrote: > >>Hi, >> >>I have a question when using SAL. >> >>I want to express a process doing in below after try to verify that >>eventually that i == 100 >>=== >>int i; >>for (i = 1; i<100; i++); >>=== >> >>So , I made a SAL program in below >> >>==== >>simple1: CONTEXT = >>BEGIN >> >>process: MODULE = >> BEGIN >> OUTPUT i: INTEGER >> INITIALIZATION >> i = 1 >> TRANSITION >> [ >> increment: >> i<100 --> i' = i+1; >> ] >> END; >> >>th1: THEOREM process |- F(i=100); >>END >>===== >> >>But when I used the command "sal-smc simple1 th1", it gave me the error >>" >>Error: [Context: simple1, line(6), column(16)]: Finite type representation >>cannot be generated, type is not finite. >>Reason: [Context: prelude, line(189), column(20)]: Type is not a bounded >>subtype of integer, or it was not possible to determine the bound. >> >>" >> >>Can someone give me some hints ? Thanks. >> >>Harry >> >> > From demoura@csl.sri.com Sun Jun 18 14:09:32 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.3 required=4.0 tests=ALL_TRUSTED=-1.44, AWL=-0.138, MAILTO_TO_SPAM_ADDR=0.276 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:09:33 -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 k5IL9WLL025656 for ; Sun, 18 Jun 2006 14:09:32 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-223.csl.sri.com [130.107.97.223]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5IL9Vgu091434; Sun, 18 Jun 2006 14:09:31 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v750) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <060008F4-78E9-4681-A6A3-484F6BBA7172@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL] A question when using SAL Date: Sun, 18 Jun 2006 14:09:30 -0700 To: "harry huang" X-Mailer: Apple Mail (2.750) X-Mailman-Approved-At: Sun, 18 Jun 2006 14:09:55 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:09:33 -0000 Hi Harry, sal-smc assumes the transition relation is total, that is, there are no deadlocks. The module "process" deadlocks when i = 100. You can find deadlocks using the tool sal-deadlock-checker. You can avoid the deadlock with a ELSE transition: [ i<100 --> i' = i+1; ELSE --> ] Cheers, Leonardo On Jun 18, 2006, at 2:02 PM, harry huang wrote: > Hi, > > Thanks for information. I modified the program and it is on below: > > ==== > simple1: CONTEXT = > BEGIN > > process: MODULE = > BEGIN > OUTPUT i: [0..100] -- modified (1) > LOCAL high: BOOLEAN -- modified (2) > DEFINITION high = i > 100 -- modified (3) > INITIALIZATION > i = 1 > TRANSITION > [ > i<100 --> i' = i+1; > ] > END; > > th1: THEOREM process |- F(i=110); -- modified (4) > END > ==== > > (1), (2), (3), (4) are the modified code. This code passed the > compiler. But I have some two issues do not understand. First, for > the modification (4), it should not hold because in the transition, > the loop stops incrementing i by 1 if i reach 100. But when I used > "sal-smc simple1 th1", it still said proved. Second, I saw there is > way to define invariant in the "DEFINITION", so I define a > invariant in modification (3). But why the using of "sal-smc > simple1 th1" still said it is proved ? > > Can someone gives me hints ? Thanks. > > harry > > >> From: Ashish Tiwari >> To: harry huang >> CC: sal@csl.sri.com >> Subject: Re: [SAL] A question when using SAL >> Date: Sat, 17 Jun 2006 16:51:55 -0700 (PDT) >> >> >> The type "INTEGER" is not bounded; it has infinitely >> many elements. >> You will have to replace it by a finite subrange type >> (e.g. [0..100]) for sal-smc to work on this example. >> >> Hope this helps, >> -Ashish >> >> On Sat, 17 Jun 2006, harry huang wrote: >> >>> Hi, >>> >>> I have a question when using SAL. >>> >>> I want to express a process doing in below after try to verify >>> that eventually that i == 100 >>> === >>> int i; >>> for (i = 1; i<100; i++); >>> === >>> >>> So , I made a SAL program in below >>> >>> ==== >>> simple1: CONTEXT = >>> BEGIN >>> >>> process: MODULE = >>> BEGIN >>> OUTPUT i: INTEGER >>> INITIALIZATION >>> i = 1 >>> TRANSITION >>> [ >>> increment: >>> i<100 --> i' = i+1; >>> ] >>> END; >>> >>> th1: THEOREM process |- F(i=100); >>> END >>> ===== >>> >>> But when I used the command "sal-smc simple1 th1", it gave me the >>> error >>> " >>> Error: [Context: simple1, line(6), column(16)]: Finite type >>> representation cannot be generated, type is not finite. >>> Reason: [Context: prelude, line(189), column(20)]: Type is not a >>> bounded subtype of integer, or it was not possible to determine >>> the bound. >>> >>> " >>> >>> Can someone give me some hints ? Thanks. >>> >>> Harry >>> >>> >> > From rushby@csl.sri.com Sun Jun 18 14:14:24 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.3 required=4.0 tests=ALL_TRUSTED=-1.44,AWL=0.176 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:14:25 -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 k5ILEOrL025837 for ; Sun, 18 Jun 2006 14:14:24 -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.13.6/8.12.11) with ESMTP id k5ILEO2r092023 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Sun, 18 Jun 2006 14:14:24 -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 k5ILEN3B011267; Sun, 18 Jun 2006 14:14:24 -0700 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id k5ILENmY011266; Sun, 18 Jun 2006 14:14:23 -0700 Date: Sun, 18 Jun 2006 14:14:23 PDT From: John Rushby To: "harry huang" Subject: Re: [SAL] A question when using SAL In-Reply-To: Your message of Sun, 18 Jun 2006 21:02:35 +0000 Message-ID: X-Mailman-Approved-At: Sun, 18 Jun 2006 14:15:20 -0700 Cc: tiwari@csl.sri.com, sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:14:25 -0000 Harry, > But when I used "sal-smc simple1 th1", it still said proved That's because your specification deadlocks (no action is possible when i=100). If you do sal-deadlock-checker simple1 process this will be reported to you. F properties only apply to infinite traces and this specification has none (because of the deadlock). If you add an else clause so it reads i<100 --> i' = i+1; [] ELSE --> then the deadlock is fixed and you'll get a counterexample to your property. > Second, I saw there is way to define invariant in the "DEFINITION", > so I define a invariant in modification (3). One the deadlock is fixed, this works ok: th2: THEOREM process |- F(high); Good luck, John From harryh23@hotmail.com Sun Jun 18 14:16:54 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.118, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:16:55 -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 k5ILGsKl025989 for ; Sun, 18 Jun 2006 14:16:54 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5ILGsgH092399 for ; Sun, 18 Jun 2006 14:16:54 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061814165422865 for ; Sun, 18 Jun 2006 14:16:54 -0700 X-Original-Received: from bay105-f28.bay105.hotmail.com (HELO hotmail.com) (65.54.224.38) by mailgate-external2.sri.com with SMTP; 18 Jun 2006 21:16:53 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sun, 18 Jun 2006 14:16:53 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sun, 18 Jun 2006 21:16:52 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: <200606181122.28509.david@mcs.vuw.ac.nz> From: "harry huang" To: David.Friggens@mcs.vuw.ac.nz Subject: RE: [SAL] Re: Some questions for using SAL Date: Sun, 18 Jun 2006 21:16:52 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 18 Jun 2006 21:16:53.0088 (UTC) FILETIME=[8544BE00:01C6931C] X-Mailman-Approved-At: Sun, 18 Jun 2006 14:17:40 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:16:55 -0000 Hi David, Thanks. I still have two questions regarding (3), (4). For (3), is it possible to define the invariant in "DEFINITION" ? I saw the SAL language manual said something about it . For (4), can you give me explicitly SAL semantics for "for (int i =0; i <10; i++) System.out.println("hello")" in Java ? In addition, in the tutorial it mentions that SAL is a framework for model checking and theorem proving. But how can I apply theorem proving techniques in SAL ? Thanks. Harry >From: David Friggens >To: sal@csl.sri.com >CC: harry huang >Subject: [SAL] Re: Some questions for using SAL >Date: Sun, 18 Jun 2006 11:22:28 +1200 > >Hi Harry > > > I have some questions regarding the SAL. > >Hopefully I can answer some of your questions. First, I'll point out >that SAL is not a procedural language - you define the transitions by >writing the changes that happen to the variables. If you want to model >some code from a procedural language you'll need to define a program >counter variable. Then you can define transitions from location1 to >location2, from location2 to location3, etc. > >The msclock example (in SAL 2.4) is a good example of this. > > > 1. Can I write the assertion in the module ? For instance, I want to > > express "assert(a==b)", how to write it in module as I see the > > example that the assertion written in the Theorem. > >You can put a=b in the guard of the transition, and have another one >that goes to an error state. For example > >pc = locX AND a = b --> pc' = locY > >and > >pc = locX AND a /= b --> pc' = locError > >Then you could test that the module doesn't ever enter the error state: >THEOREM system |- G(pc /= locError) > > > > 2. Is there way to express the wait condition ? For instance, I want > > to express the java expression "while ( a != 0) wait();" in SAL . > >You could use a transition like: > >pc = locX AND a = 0 --> pc' = locY > >This transition is only enabled if the module is at location locX and a >is zero, so if it's at locX and a isn't zero, then it has to wait until >a transition becomes enabled (i.e. when a becomes zero). > > > Anway, I saw example that has "sleeping, trying, critical ". Are > > those keywords SAL reserved keywords or user defined ? > >These are user defined. > > > 3. How to expression the invariant in SAL ? > >If you want to prove that a property "p" is an invariant you can use the >LTL formula G(p). For example >THEOREM system |- G(a <= 5 AND b >= 10). > > > 4. Is there "for" loop in SAL ? > >Not explicitly, but you can express it easily. > > >Cheers >David > From harryh23@hotmail.com Sun Jun 18 14:29:37 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.104, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:29: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 k5ILTbmo026318 for ; Sun, 18 Jun 2006 14:29:37 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5ILTa44093499 for ; Sun, 18 Jun 2006 14:29:37 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061814293723444 for ; Sun, 18 Jun 2006 14:29:37 -0700 X-Original-Received: from bay105-f9.bay105.hotmail.com (HELO hotmail.com) (65.54.224.19) by mailgate-external2.sri.com with SMTP; 18 Jun 2006 21:29:34 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sun, 18 Jun 2006 14:29:32 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sun, 18 Jun 2006 21:29:30 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: rushby@csl.sri.com Subject: Re: [SAL] A question when using SAL Date: Sun, 18 Jun 2006 21:29:30 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 18 Jun 2006 21:29:32.0480 (UTC) FILETIME=[49E6C400:01C6931E] X-Mailman-Approved-At: Sun, 18 Jun 2006 14:35:40 -0700 Cc: tiwari@csl.sri.com, sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:29:38 -0000 Hi John, Thanks for the information, I tried the suggestions in below and it works. Two more questions, does "ELSE --> (without nothing)" mean break the loop ? What is "[]" ? Is it means two process asynchronously executing "i' = i+1" and "ELSE" parts ? (I do not think I have two processes, but only 1 process). Thanks. Harry >From: John Rushby >To: "harry huang" >CC: tiwari@csl.sri.com, sal@csl.sri.com >Subject: Re: [SAL] A question when using SAL >Date: Sun, 18 Jun 2006 14:14:23 PDT > >Harry, > > > But when I used "sal-smc simple1 th1", it still said proved > >That's because your specification deadlocks (no action is possible >when i=100). If you do > sal-deadlock-checker simple1 process >this will be reported to you. F properties only apply to infinite >traces and this specification has none (because of the deadlock). > >If you add an else clause so it reads > > i<100 --> i' = i+1; > [] > ELSE --> > >then the deadlock is fixed and you'll get a counterexample to your >property. > > > Second, I saw there is way to define invariant in the "DEFINITION", > > so I define a invariant in modification (3). > >One the deadlock is fixed, this works ok: > > th2: THEOREM process |- F(high); > > >Good luck, >John > From rushby@csl.sri.com Sun Jun 18 14:38:12 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.3 required=4.0 tests=ALL_TRUSTED=-1.44,AWL=0.141 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:38:12 -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 k5ILcC6w026607 for ; Sun, 18 Jun 2006 14:38:12 -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.13.6/8.12.11) with ESMTP id k5ILcAfs094285 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Sun, 18 Jun 2006 14:38:10 -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 k5ILcAYu011326; Sun, 18 Jun 2006 14:38:10 -0700 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id k5ILcAoZ011325; Sun, 18 Jun 2006 14:38:10 -0700 Date: Sun, 18 Jun 2006 14:38:10 PDT From: John Rushby To: "harry huang" Subject: Re: [SAL] A question when using SAL In-Reply-To: Your message of Sun, 18 Jun 2006 21:29:30 +0000 Message-ID: X-Mailman-Approved-At: Sun, 18 Jun 2006 14:39:09 -0700 Cc: tiwari@csl.sri.com, sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:38:12 -0000 > What is "[]" ? Is it means two process asynchronously executing This is a pretty basic question. I suggest you take a few hours to read the documentation and some of the examples and tutorials at http://sal.csl.sri.com/documentation.shtml John From tiwari@csl.sri.com Sun Jun 18 14:40:20 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.3 required=4.0 tests=ALL_TRUSTED=-1.44, AWL=-0.138, MAILTO_TO_SPAM_ADDR=0.276 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 14:40:21 -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 k5ILeKOx026783 for ; Sun, 18 Jun 2006 14:40:20 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from fury.csl.sri.com (fury.csl.sri.com [130.107.5.225]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5ILeIur094591 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Sun, 18 Jun 2006 14:40:18 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from fury.csl.sri.com (fury.csl.sri.com [127.0.0.1]) by fury.csl.sri.com (8.12.10/8.12.10) with ESMTP id k5ILeILD013707; Sun, 18 Jun 2006 14:40:18 -0700 X-Original-Received: from localhost (tiwari@localhost) by fury.csl.sri.com (8.12.10/8.12.10/Submit) with ESMTP id k5ILeIo9013703; Sun, 18 Jun 2006 14:40:18 -0700 Date: Sun, 18 Jun 2006 14:40:18 -0700 (PDT) From: Ashish Tiwari To: harry huang Subject: Re: [SAL] A question when using SAL In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Mailman-Approved-At: Sun, 18 Jun 2006 14:41:59 -0700 Cc: sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 21:40:21 -0000 Hi Harry, [] means that the process can nondeterministically choose either of the alternatives (depending on the guards of the guarded transitions). The ELSE guard has a special semantics which means that it is chosen only when all other guards fail. So, there is just one process, but is composed of "asynchronous composition" of several "guarded transitions". --Ashish On Sun, 18 Jun 2006, harry huang wrote: > Hi John, > > Thanks for the information, I tried the suggestions in below and it works. > Two more questions, does "ELSE --> (without nothing)" mean break the loop ? > What is "[]" ? Is it means two process asynchronously executing "i' = i+1" > and "ELSE" parts ? (I do not think I have two processes, but only 1 process). > Thanks. > > Harry > > >> From: John Rushby >> To: "harry huang" >> CC: tiwari@csl.sri.com, sal@csl.sri.com >> Subject: Re: [SAL] A question when using SAL >> Date: Sun, 18 Jun 2006 14:14:23 PDT >> >> Harry, >> >> > But when I used "sal-smc simple1 th1", it still said proved >> >> That's because your specification deadlocks (no action is possible >> when i=100). If you do >> sal-deadlock-checker simple1 process >> this will be reported to you. F properties only apply to infinite >> traces and this specification has none (because of the deadlock). >> >> If you add an else clause so it reads >> >> i<100 --> i' = i+1; >> [] >> ELSE --> >> >> then the deadlock is fixed and you'll get a counterexample to your >> property. >> >> > Second, I saw there is way to define invariant in the "DEFINITION", >> > so I define a invariant in modification (3). >> >> One the deadlock is fixed, this works ok: >> >> th2: THEOREM process |- F(high); >> >> >> Good luck, >> John >> > > From harryh23@hotmail.com Sun Jun 18 15:10:46 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.092, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 15:10:47 -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 k5IMAk0C027496 for ; Sun, 18 Jun 2006 15:10:46 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5IMAjuj097603 for ; Sun, 18 Jun 2006 15:10:46 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061815104625312 for ; Sun, 18 Jun 2006 15:10:46 -0700 X-Original-Received: from bay105-f8.bay105.hotmail.com (HELO hotmail.com) (65.54.224.18) by mailgate-external2.sri.com with SMTP; 18 Jun 2006 22:10:43 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Sun, 18 Jun 2006 15:10:41 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Sun, 18 Jun 2006 22:10:39 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: tiwari@csl.sri.com Subject: Re: [SAL] A question when using SAL Date: Sun, 18 Jun 2006 22:10:39 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 18 Jun 2006 22:10:41.0974 (UTC) FILETIME=[09D5A560:01C69324] X-Mailman-Approved-At: Sun, 18 Jun 2006 15:23:39 -0700 Cc: sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 22:10:47 -0000 Hi Ashish, Thanks for the clarification. That make sense. As I was wondering the keyword "ELSE" usually appears with "IF" statement, but there is no "IF" in the program although I tried to implicitly express this idea. But "[]" looked like to be used asynchronously in the concurrent environment. So the explaination of "asynchronous composition" of several "guarded transitions" in one process cleans my confusion. In addition, the process jumps out transition after executing "ELSE -->" ? Anyway, is there more substantial notes to introduce the semantics of SAL. I just read the tutoral and language manual. But I feel it is not sufficient enough to understand some basic language semantics because SAL actually is somewhat different with other popular language such as java, C. Promela, etc. The language manual presents a good language parser tree, but how to use even basic parts such as "IF... ELSE", "For", etc have not explicatly stated. Thanks. Thanks. Harry >From: Ashish Tiwari >To: harry huang >CC: rushby@csl.sri.com, sal@csl.sri.com >Subject: Re: [SAL] A question when using SAL >Date: Sun, 18 Jun 2006 14:40:18 -0700 (PDT) > > >Hi Harry, > >[] means that the process can nondeterministically choose either of the >alternatives (depending on the guards of >the guarded transitions). >The ELSE guard has a special semantics which means that it >is chosen only when all other guards fail. >So, there is just one process, but is composed of >"asynchronous composition" of several "guarded transitions". > >--Ashish > >On Sun, 18 Jun 2006, harry huang wrote: > >>Hi John, >> >>Thanks for the information, I tried the suggestions in below and it works. >>Two more questions, does "ELSE --> (without nothing)" mean break the loop >>? What is "[]" ? Is it means two process asynchronously executing "i' = >>i+1" and "ELSE" parts ? (I do not think I have two processes, but only 1 >>process). Thanks. >> >>Harry >> >> >>>From: John Rushby >>>To: "harry huang" >>>CC: tiwari@csl.sri.com, sal@csl.sri.com >>>Subject: Re: [SAL] A question when using SAL >>>Date: Sun, 18 Jun 2006 14:14:23 PDT >>> >>>Harry, >>> >>> > But when I used "sal-smc simple1 th1", it still said proved >>> >>>That's because your specification deadlocks (no action is possible >>>when i=100). If you do >>> sal-deadlock-checker simple1 process >>>this will be reported to you. F properties only apply to infinite >>>traces and this specification has none (because of the deadlock). >>> >>>If you add an else clause so it reads >>> >>> i<100 --> i' = i+1; >>> [] >>> ELSE --> >>> >>>then the deadlock is fixed and you'll get a counterexample to your >>>property. >>> >>> > Second, I saw there is way to define invariant in the "DEFINITION", >>> > so I define a invariant in modification (3). >>> >>>One the deadlock is fixed, this works ok: >>> >>> th2: THEOREM process |- F(high); >>> >>> >>>Good luck, >>>John >>> >> >> From rushby@csl.sri.com Sun Jun 18 15:30:41 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=-1.3 required=4.0 tests=ALL_TRUSTED=-1.44,AWL=0.117 autolearn=disabled version=3.1.1 date=Sun, 18 Jun 2006 15:30:41 -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 k5IMUfjT027863 for ; Sun, 18 Jun 2006 15:30:41 -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.13.6/8.12.11) with ESMTP id k5IMUeOu099148 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Sun, 18 Jun 2006 15:30:40 -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 k5IMUeVF011404; Sun, 18 Jun 2006 15:30:40 -0700 X-Original-Received: (from rushby@localhost) by muon.csl.sri.com (8.13.1/8.13.1/Submit) id k5IMUePd011403; Sun, 18 Jun 2006 15:30:40 -0700 Date: Sun, 18 Jun 2006 15:30:40 PDT From: John Rushby To: "harry huang" Subject: Re: [SAL] A question when using SAL In-Reply-To: Your message of Sun, 18 Jun 2006 22:10:39 +0000 Message-ID: X-Mailman-Approved-At: Sun, 18 Jun 2006 15:31:02 -0700 Cc: tiwari@csl.sri.com, sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Jun 2006 22:30:41 -0000 Harry, > The language manual presents a good language parser tree, but how to > use even basic parts such as "IF... ELSE", "For", etc have not explicatly > stated. OK. We'll have to improve those descriptions. How about the tutorial: http://www.csl.sri.com/users/rushby/abstracts/om1 ? John From tiwari@csl.sri.com Mon Jun 19 10:20:32 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.069 autolearn=disabled version=3.1.1 date=Mon, 19 Jun 2006 10:20:33 -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 k5JHKWKl049489 for ; Mon, 19 Jun 2006 10:20:32 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from aryabhata.csl.sri.com (aryabhata.csl.sri.com [130.107.15.160]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5JHKWx5095455 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Mon, 19 Jun 2006 10:20:32 -0700 (PDT) (envelope-from tiwari@csl.sri.com) X-Original-Received: from aryabhata.csl.sri.com (localhost.localdomain [127.0.0.1]) by aryabhata.csl.sri.com (8.13.1/8.13.1) with ESMTP id k5JHKVFP015141; Mon, 19 Jun 2006 10:20:31 -0700 X-Original-Received: from localhost (tiwari@localhost) by aryabhata.csl.sri.com (8.13.1/8.13.1/Submit) with ESMTP id k5JHKVRW015138; Mon, 19 Jun 2006 10:20:31 -0700 Date: Mon, 19 Jun 2006 10:20:31 -0700 (PDT) From: Ashish Tiwari To: harry huang Subject: Re: [SAL] A question when using SAL In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Mailman-Approved-At: Mon, 19 Jun 2006 10:21:54 -0700 Cc: sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 19 Jun 2006 17:20:33 -0000 > > In addition, the process jumps out transition after executing "ELSE -->" ? In your example, once the counter i reaches 100, the "ELSE --> " transition is taken infinitely many times, that is, the process remains in the state i=100 and keeps looping in that state. (It does not deadlock). -Ashish >>>> If you add an else clause so it reads >>>> >>>> i<100 --> i' = i+1; >>>> [] >>>> ELSE --> >>>> From harryh23@hotmail.com Mon Jun 19 12:48:24 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.083, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Mon, 19 Jun 2006 12:48:24 -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 k5JJmODl052309 for ; Mon, 19 Jun 2006 12:48:24 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5JJmOKO009256 for ; Mon, 19 Jun 2006 12:48:24 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061912482305778 for ; Mon, 19 Jun 2006 12:48:23 -0700 X-Original-Received: from bay105-f6.bay105.hotmail.com (HELO hotmail.com) (65.54.224.16) by mailgate-external2.sri.com with SMTP; 19 Jun 2006 19:48:23 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 19 Jun 2006 12:48:22 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Mon, 19 Jun 2006 19:48:20 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: rushby@csl.sri.com Subject: Re: [SAL] A question when using SAL Date: Mon, 19 Jun 2006 19:48:20 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 19 Jun 2006 19:48:22.0867 (UTC) FILETIME=[528B1230:01C693D9] X-Mailman-Approved-At: Mon, 19 Jun 2006 12:49:31 -0700 Cc: tiwari@csl.sri.com, sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 19 Jun 2006 19:48:24 -0000 Hi John, The new tutorial is much better. I understand more of SAL. But would it possible to have a language manual that briefly describes how to use each semantics in SAL, such as "what is module?", "how to define the parameters(return value, etc) in program ?", etc. Thanks. Harry >From: John Rushby >To: "harry huang" >CC: tiwari@csl.sri.com, sal@csl.sri.com, rushby@csl.sri.com >Subject: Re: [SAL] A question when using SAL >Date: Sun, 18 Jun 2006 15:30:40 PDT > >Harry, > > > The language manual presents a good language parser tree, but how to > > use even basic parts such as "IF... ELSE", "For", etc have not >explicatly > > stated. > >OK. We'll have to improve those descriptions. > >How about the tutorial: http://www.csl.sri.com/users/rushby/abstracts/om1 ? > >John > From harryh23@hotmail.com Mon Jun 19 12:58:47 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.075, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Mon, 19 Jun 2006 12:58:47 -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 k5JJwlKs052638 for ; Mon, 19 Jun 2006 12:58:47 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5JJwlNe010291 for ; Mon, 19 Jun 2006 12:58:47 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006061912584613924 for ; Mon, 19 Jun 2006 12:58:46 -0700 X-Original-Received: from bay105-f12.bay105.hotmail.com (HELO hotmail.com) (65.54.224.22) by mailgate-external1.sri.com with SMTP; 19 Jun 2006 19:58:46 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 19 Jun 2006 12:58:45 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Mon, 19 Jun 2006 19:58:45 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: tiwari@csl.sri.com Subject: Re: [SAL] A question when using SAL Date: Mon, 19 Jun 2006 19:58:45 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 19 Jun 2006 19:58:45.0436 (UTC) FILETIME=[C59F8FC0:01C693DA] X-Mailman-Approved-At: Mon, 19 Jun 2006 12:59:48 -0700 Cc: sal@csl.sri.com, rushby@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 19 Jun 2006 19:58:48 -0000 Hi Ashish, Thanks. But what is semantics in SAL stating jumping out the transition ? As "ELSE -->" means the process remains in the state i=100 and keeps looping in that state, so if I uses "ELSE --> A", does that mean the process jumps out the "for" loop and comes to state A ? Harry >From: Ashish Tiwari >To: harry huang >CC: sal@csl.sri.com, rushby@csl.sri.com >Subject: Re: [SAL] A question when using SAL >Date: Mon, 19 Jun 2006 10:20:31 -0700 (PDT) > >> >>In addition, the process jumps out transition after executing "ELSE -->" >>? > >In your example, once the counter i reaches 100, >the "ELSE --> " transition is taken infinitely many >times, that is, the process remains in the state >i=100 and keeps looping in that state. (It does not >deadlock). > >-Ashish > >>>>>If you add an else clause so it reads >>>>> >>>>> i<100 --> i' = i+1; >>>>> [] >>>>> ELSE --> >>>>> > From harryh23@hotmail.com Tue Jun 20 11:59:35 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=0.069, MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Tue, 20 Jun 2006 11:59: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 k5KIxY6O095852 for ; Tue, 20 Jun 2006 11:59:34 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5KIxYku048779 for ; Tue, 20 Jun 2006 11:59:34 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006062011593408346 for ; Tue, 20 Jun 2006 11:59:34 -0700 X-Original-Received: from bay105-f15.bay105.hotmail.com (HELO hotmail.com) (65.54.224.25) by mailgate-external1.sri.com with SMTP; 20 Jun 2006 18:59:34 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Tue, 20 Jun 2006 11:59:34 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Tue, 20 Jun 2006 18:59:33 GMT X-Originating-IP: [130.63.86.111] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: sal@csl.sri.com Date: Tue, 20 Jun 2006 18:59:33 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 20 Jun 2006 18:59:34.0045 (UTC) FILETIME=[AB3E0CD0:01C6949B] X-Mailman-Approved-At: Tue, 20 Jun 2006 12:00:21 -0700 Subject: [SAL] Command issues for adder example X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 20 Jun 2006 18:59:35 -0000 Hi, I am running the example -- adder in the examples/adder folder in the SAL directory. The README in that example says "sal-path-finder -v 3 --module='adder{;5}!Nbitadder'" to generate an execution trace up to depth 10, for a 5-bit adder. But when I issue that command, there is error mesaage in below: "Nbitadder: Event not found." Can someone give me suggestions ? Haeey From r.venky@tcs.com Tue Jun 20 20:31:26 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=Tue, 20 Jun 2006 20:31: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 k5L3VQDk006034 for ; Tue, 20 Jun 2006 20:31:26 -0700 (PDT) (envelope-from r.venky@tcs.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 k5L3VQTP098638 for ; Tue, 20 Jun 2006 20:31:26 -0700 (PDT) (envelope-from r.venky@tcs.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 M2006062020312605707 for ; Tue, 20 Jun 2006 20:31:26 -0700 X-Original-Received: from inmumg01.tcs.com (219.64.33.12) by mailgate-external2.sri.com with SMTP; 21 Jun 2006 03:31:25 -0000 X-Original-Received: from unknown (HELO InMumM01.tcs.com) ([172.17.9.117]) by inmumg01.tcs.com with ESMTP; 21 Jun 2006 09:03:41 +0530 X-IronPort-AV: i="4.06,158,1149445800"; d="scan'208"; a="11762459:sNHT27990783" To: sal@csl.sri.com MIME-Version: 1.0 X-Mailer: Lotus Notes Build V70_M6_06302005 Beta 4 June 30, 2005 From: r.venky@tcs.com Message-ID: Date: Wed, 21 Jun 2006 09:01:28 +0530 X-MIMETrack: Serialize by Router on InMumM01/TCS(Release 6.5.3FP1HF274 | August 23, 2005) at 06/21/2006 09:01:28, Serialize complete at 06/21/2006 09:01:28 Content-Type: multipart/alternative; boundary="=_alternative 00135C3965257194_=" X-Mailman-Approved-At: Wed, 21 Jun 2006 08:20:31 -0700 Subject: [SAL] SAL error message - seek explanation X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 03:31:27 -0000 This is a multipart message in MIME format. --=_alternative 00135C3965257194_= Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="us-ascii" When we run SAL on a big file we get the following error message. Can someone tell me what is the likely cause? *** ERROR:bigloo:slot-value: slot :flat-module not found in -- #unspecified Error: slot :flat-module not found in sal-smc --enable-slicer REQUEST_TYPE1_CONTROL rw_race_18 12.82s user 0.37s system 101% cpu 12.999 total Thanks, Venky =====-----=====-----===== Notice: The information contained in this e-mail message and/or attachments to it may contain confidential or privileged information. If you are not the intended recipient, any dissemination, use, review, distribution, printing or copying of the information contained in this e-mail message and/or attachments to it are strictly prohibited. If you have received this communication in error, please notify us by reply e-mail or telephone and immediately and permanently delete the message and any attachments. Thank you --=_alternative 00135C3965257194_= Content-Transfer-Encoding: 7bit Content-Type: text/html; charset="us-ascii"
When we run SAL on a big file we get the following error message. Can someone tell me what is the likely cause?


*** ERROR:bigloo:slot-value:
slot :flat-module not found in <primitive> -- #unspecified
Error: slot :flat-module not found in <primitive>
sal-smc --enable-slicer REQUEST_TYPE1_CONTROL rw_race_18  12.82s user 0.37s system 101% cpu 12.999 total


Thanks,
Venky 
=====-----=====-----=====
Notice: The information contained in this e-mail
message and/or attachments to it may contain 
confidential or privileged information. If you are 
not the intended recipient, any dissemination, use, 
review, distribution, printing or copying of the 
information contained in this e-mail message 
and/or attachments to it are strictly prohibited. If 
you have received this communication in error, 
please notify us by reply e-mail or telephone and 
immediately and permanently delete the message 
and any attachments. Thank you
--=_alternative 00135C3965257194_=-- From swarup.mohalik@gm.com Wed Jun 21 03:07:48 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=AWL=0.090,HTML_MESSAGE=0.001, NO_REAL_NAME=0.55,UPPERCASE_25_50=0 autolearn=disabled version=3.1.1 date=Wed, 21 Jun 2006 03:07: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.6/8.13.4) with ESMTP id k5LA7mh8014640 for ; Wed, 21 Jun 2006 03:07:48 -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.6/8.12.11) with SMTP id k5LA7m8B041410 for ; Wed, 21 Jun 2006 03:07:48 -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 M2006062103074828477 for ; Wed, 21 Jun 2006 03:07:48 -0700 X-Original-Received: from plgmler3.imr.gm.com (199.228.142.103) by mailgate-external1.sri.com with SMTP; 21 Jun 2006 10:07:47 -0000 X-Original-Received: from plgmlir2.imr.gm.com (plgmlir2-2.imr.gm.com [199.228.142.170]) by plgmler3.imr.gm.com (8.13.6/8.12.10) with ESMTP id k5LA7kRa019853 for ; Wed, 21 Jun 2006 05:07:46 -0500 X-Original-Received: from plgmlir2.imr.gm.com (localhost [127.0.0.1]) by plgmlir2.imr.gm.com (8.13.6/8.12.10) with ESMTP id k5LA7a4a019921 for ; Wed, 21 Jun 2006 05:07:36 -0500 X-Original-Received: from usabhmg02.mail.gm.com (USABHMG02.mail.gm.com [164.56.166.171]) by plgmlir2.imr.gm.com (8.13.6/8.12.10) with ESMTP id k5LA7a0O019916 for ; Wed, 21 Jun 2006 05:07:36 -0500 To: sal@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: Wed, 21 Jun 2006 15:37:30 +0530 X-MIMETrack: Serialize by Router on USABHMG02/G/GMSERVER/GMC(Release 6.5.4FP1 HF649|April 03, 2006) at 06/21/2006 06:07:36 AM, Serialize complete at 06/21/2006 06:07:36 AM Content-Type: multipart/alternative; boundary="=_alternative 00379E0565257194_=" X-Mailman-Approved-At: Wed, 21 Jun 2006 08:20:31 -0700 Subject: [SAL] --hide-locals X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 10:07:49 -0000 This is a multipart message in MIME format. --=_alternative 00379E0565257194_= Content-Type: text/plain; charset="US-ASCII" Hello all, [SAL on cygwin on a windows XP.] The --hide-locals option does not seem to work. simp_leader : CONTEXT= BEGIN State : TYPE = {on}; main[delta : REAL] : MODULE= BEGIN LOCAL state : State LOCAL acc,v1,v0 : REAL LOCAL gap : REAL INITIALIZATION state = on; TRANSITION [state = on --> v1' = v1 + acc * delta; v0' = v0 + (acc + v1 - v0) * delta; gap' = gap + (v1 - v0) ] END; th3 : THEOREM main[1] |- (gap >= 0) AND (v1 <= v0) => G(gap >= 0); END bash>sal-inf-bmc simp_leader th3 -v 0 --delta-path --hide-locals Counterexample: ======================== Path ======================== Step 0: --- System Variables (assignments) --- --- Constraints --- v0 >= v1; gap >= 0; ------------------------ Step 1: --- System Variables (assignments) --- --- Constraints --- gap = -1 * PRE(v0) + PRE(v1) + PRE(gap); ba-pc!1 >= 0; v1 = PRE(acc) + PRE(v1); acc = PRE(acc); -1 + ba-pc!1 = 0; ba-pc!1 >= 1; ba-pc!1 <= 2; v0 = PRE(acc) + PRE(v1); gap < 0; ------------------------ Step 2: --- System Variables (assignments) --- --- Constraints --- v0 = PRE(acc) + PRE(v1); acc = PRE(acc); gap = -1 * PRE(v0) + PRE(v1) + PRE(gap); v1 = PRE(acc) + PRE(v1); Please look into this. ----------------------- Swarup Mohalik --=_alternative 00379E0565257194_= Content-Type: text/html; charset="US-ASCII"
Hello all,
[SAL on cygwin on a windows XP.]

The --hide-locals option does not seem to work.

simp_leader : CONTEXT=
BEGIN
        State : TYPE = {on};

        main[delta : REAL] : MODULE=
        BEGIN
                LOCAL state     : State
                LOCAL acc,v1,v0 : REAL  
                LOCAL gap       : REAL

                INITIALIZATION
                        state = on;
                TRANSITION
                [state = on -->
                        v1'  = v1 + acc * delta;
                        v0'  = v0 + (acc + v1 - v0) * delta;
                        gap' = gap + (v1 - v0)
                ]

        END;

     
        th3 : THEOREM main[1] |- (gap >= 0) AND (v1 <= v0) => G(gap >= 0);

END

bash>sal-inf-bmc simp_leader th3 -v 0 --delta-path --hide-locals

Counterexample:
========================
Path
========================
Step 0:
--- System Variables (assignments) ---
--- Constraints ---
v0 >= v1;
gap >= 0;
------------------------
Step 1:
--- System Variables (assignments) ---
--- Constraints ---
gap = -1 * PRE(v0) + PRE(v1) + PRE(gap);
ba-pc!1 >= 0;
v1 = PRE(acc) + PRE(v1);
acc = PRE(acc);
-1 + ba-pc!1 = 0;
ba-pc!1 >= 1;
ba-pc!1 <= 2;
v0 = PRE(acc) + PRE(v1);
gap < 0;
------------------------
Step 2:
--- System Variables (assignments) ---
--- Constraints ---
v0 = PRE(acc) + PRE(v1);
acc = PRE(acc);
gap = -1 * PRE(v0) + PRE(v1) + PRE(gap);
v1 = PRE(acc) + PRE(v1);


Please look into this.
-----------------------
Swarup Mohalik --=_alternative 00379E0565257194_=-- From demoura@csl.sri.com Wed Jun 21 08:22:21 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.011 autolearn=disabled version=3.1.1 date=Wed, 21 Jun 2006 08:22: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 k5LFMLal023562 for ; Wed, 21 Jun 2006 08:22:21 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-160.csl.sri.com [130.107.97.160]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5LFMLXC075989; Wed, 21 Jun 2006 08:22:21 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v750) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <9749FB75-F590-41E3-A4C0-7F1D5785B864@csl.sri.com> Content-Transfer-Encoding: 7bit From: Leonardo de Moura Subject: Re: [SAL] Command issues for adder example Date: Wed, 21 Jun 2006 08:22:22 -0700 To: "harry huang" X-Mailer: Apple Mail (2.750) X-Mailman-Approved-At: Wed, 21 Jun 2006 08:33:37 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 15:22:22 -0000 Hi Harry, You are probably using tcsh or csh. You should use a `\` before the `!`. sal-path-finder -v 3 --module='adder{;5}\!Nbitadder Cheers, Leonardo On Jun 20, 2006, at 11:59 AM, harry huang wrote: > Hi, > > I am running the example -- adder in the examples/adder folder in > the SAL directory. The README in that example says "sal-path-finder > -v 3 --module='adder{;5}!Nbitadder'" to generate an execution trace > up to depth 10, for a 5-bit adder. But when I issue that command, > there is error mesaage in below: > > "Nbitadder: Event not found." > > Can someone give me suggestions ? > > Haeey > From demoura@csl.sri.com Wed Jun 21 08:23:55 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.010, HTML_MESSAGE=0.001 autolearn=disabled version=3.1.1 date=Wed, 21 Jun 2006 08:23:56 -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 k5LFNtxR023608 for ; Wed, 21 Jun 2006 08:23:55 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-160.csl.sri.com [130.107.97.160]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5LFNtjn076103; Wed, 21 Jun 2006 08:23:55 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v750) Content-Type: multipart/alternative; boundary=Apple-Mail-17-797544929 Message-Id: From: Leonardo de Moura Subject: Re: [SAL] SAL error message - seek explanation Date: Wed, 21 Jun 2006 08:23:56 -0700 To: r.venky@tcs.com X-Mailer: Apple Mail (2.750) X-Mailman-Approved-At: Wed, 21 Jun 2006 08:33:37 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 15:23:56 -0000 --Apple-Mail-17-797544929 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Hi Venky, Could you send us the file that produced the error message? Thanks, Leonardo On Jun 20, 2006, at 8:31 PM, r.venky@tcs.com wrote: > > When we run SAL on a big file we get the following error message. > Can someone tell me what is the likely cause? > > > *** ERROR:bigloo:slot-value: > slot :flat-module not found in -- #unspecified > Error: slot :flat-module not found in > sal-smc --enable-slicer REQUEST_TYPE1_CONTROL rw_race_18 12.82s > user 0.37s system 101% cpu 12.999 total > > > Thanks, > Venky > =====-----=====-----===== > Notice: The information contained in this e-mail > message and/or attachments to it may contain > confidential or privileged information. If you are > not the intended recipient, any dissemination, use, > review, distribution, printing or copying of the > information contained in this e-mail message > and/or attachments to it are strictly prohibited. If > you have received this communication in error, > please notify us by reply e-mail or telephone and > immediately and permanently delete the message > and any attachments. Thank you > > --Apple-Mail-17-797544929 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1 Hi Venky,

Could you send us the file = that produced the error message?

Thanks,
Leonardo

On Jun 20, 2006, at 8:31 PM, r.venky@tcs.com wrote:


When we run SAL on a big file we get the = following error message. Can someone tell me what is the likely = cause?


*** = ERROR:bigloo:slot-value:
slot :flat-module not found in <primitive> -- = #unspecified
Error: slot = :flat-module not found in <primitive>
sal-smc --enable-slicer REQUEST_TYPE1_CONTROL = rw_race_18 =A012.82s user 0.37s system 101% cpu 12.999 total =


Thanks,
Venky 
=3D=3D=3D=3D=3D-----=3D=3D=3D=3D=
=3D-----=3D=3D=3D=3D=3D
Notice: The information contained in this e-mail
message and/or attachments to it may contain=20
confidential or privileged information. If you are=20
not the intended recipient, any dissemination, use,=20
review, distribution, printing or copying of the=20
information contained in this e-mail message=20
and/or attachments to it are strictly prohibited. If=20
you have received this communication in error,=20
please notify us by reply e-mail or telephone and=20
immediately and permanently delete the message=20
and any attachments. Thank you

= --Apple-Mail-17-797544929-- From demoura@csl.sri.com Wed Jun 21 08:33:12 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.009, HTML_MESSAGE=0.001 autolearn=disabled version=3.1.1 date=Wed, 21 Jun 2006 08:33:12 -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 k5LFXBco023775 for ; Wed, 21 Jun 2006 08:33:12 -0700 (PDT) (envelope-from demoura@csl.sri.com) X-Original-Received: from [192.168.0.4] (ovc-160.csl.sri.com [130.107.97.160]) by mx1.csl.sri.com (8.13.6/8.12.11) with ESMTP id k5LFXBTY076836; Wed, 21 Jun 2006 08:33:11 -0700 (PDT) (envelope-from demoura@csl.sri.com) In-Reply-To: References: Mime-Version: 1.0 (Apple Message framework v750) Content-Type: multipart/alternative; boundary=Apple-Mail-18-798100915 Message-Id: <1C36B874-CFD7-4B1C-BBF3-B6B4C80404BE@csl.sri.com> From: Leonardo de Moura Subject: Re: [SAL] --hide-locals Date: Wed, 21 Jun 2006 08:33:12 -0700 To: swarup.mohalik@gm.com X-Mailer: Apple Mail (2.750) X-Mailman-Approved-At: Wed, 21 Jun 2006 08:33:37 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 15:33:13 -0000 --Apple-Mail-18-798100915 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Hi, The option --hide-locals only affects the "-- System Variables (assignments) --" section. The constraints section is used when the decision procedure failed to produced a concrete counterexample, and returned a set constraints. Last week, we updated the SAL 2.4 pre-release binaries. They use a new decision procedure that is faster and produces concrete counterexamples. The binaries can be downloaded at: http://sal.csl.sri.com/pre-release.shtml Cheers, Leonardo On Jun 21, 2006, at 3:07 AM, swarup.mohalik@gm.com wrote: > > Hello all, > [SAL on cygwin on a windows XP.] > > The --hide-locals option does not seem to work. > > simp_leader : CONTEXT= > BEGIN > State : TYPE = {on}; > > main[delta : REAL] : MODULE= > BEGIN > LOCAL state : State > LOCAL acc,v1,v0 : REAL > LOCAL gap : REAL > > INITIALIZATION > state = on; > TRANSITION > [state = on --> > v1' = v1 + acc * delta; > v0' = v0 + (acc + v1 - v0) * delta; > gap' = gap + (v1 - v0) > ] > > END; > > > th3 : THEOREM main[1] |- (gap >= 0) AND (v1 <= v0) => G(gap > >= 0); > > END > > bash>sal-inf-bmc simp_leader th3 -v 0 --delta-path --hide-locals > > Counterexample: > ======================== > Path > ======================== > Step 0: > --- System Variables (assignments) --- > --- Constraints --- > v0 >= v1; > gap >= 0; > ------------------------ > Step 1: > --- System Variables (assignments) --- > --- Constraints --- > gap = -1 * PRE(v0) + PRE(v1) + PRE(gap); > ba-pc!1 >= 0; > v1 = PRE(acc) + PRE(v1); > acc = PRE(acc); > -1 + ba-pc!1 = 0; > ba-pc!1 >= 1; > ba-pc!1 <= 2; > v0 = PRE(acc) + PRE(v1); > gap < 0; > ------------------------ > Step 2: > --- System Variables (assignments) --- > --- Constraints --- > v0 = PRE(acc) + PRE(v1); > acc = PRE(acc); > gap = -1 * PRE(v0) + PRE(v1) + PRE(gap); > v1 = PRE(acc) + PRE(v1); > > > Please look into this. > ----------------------- > Swarup Mohalik --Apple-Mail-18-798100915 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1 Hi,

The option --hide-locals = only affects the "-- System Variables (assignments) = --"
section.=A0 The constraints section is used when the = decision procedure failed
to produced a concrete = counterexample, and returned a set constraints.=A0
Last week, = we updated the SAL 2.4 pre-release binaries. They use a = new
decision procedure that is faster and produces concrete = counterexamples.
The binaries can be downloaded = at:


Cheers,
Leonardo

On = Jun 21, 2006, at 3:07 AM, swarup.mohalik@gm.com = wrote:


Hello all, =
[SAL on cygwin on a windows = XP.]

The = --hide-locals option does not seem to work.

simp_leader : CONTEXT=3D
BEGIN
=A0 =A0 =A0 =A0 State : TYPE =3D {on};
=
=A0 =A0 =A0 =A0 main[delta : = REAL] : MODULE=3D
=A0 =A0 = =A0 =A0 BEGIN
=A0 =A0 =A0 = =A0 =A0 =A0 =A0 =A0 LOCAL state =A0 =A0 : State
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 LOCAL = acc,v1,v0 : REAL =A0
=A0 = =A0 =A0 =A0 =A0 =A0 =A0 =A0 LOCAL gap =A0 =A0 =A0 : REAL
=
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 = INITIALIZATION
=A0 =A0 =A0= =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 state =3D on;
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 = TRANSITION
=A0 =A0 =A0 =A0= =A0 =A0 =A0 =A0 [state =3D on -->
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 v1' = =A0=3D v1 + acc * delta;
=A0= =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 v0' =A0=3D v0 + (acc + v1 - = v0) * delta;
=A0 =A0 =A0 = =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 gap' =3D gap + (v1 - v0) =
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 = ]

=A0 =A0 =A0 =A0 = END;

=A0 =A0 =A0 =
=A0 =A0 =A0 =A0 th3 : = THEOREM main[1] |- (gap >=3D 0) AND (v1 <=3D v0) =3D> G(gap = >=3D 0);

END

bash>sal-inf-bmc simp_leader th3 -v 0 = --delta-path --hide-locals

Counterexample:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D
Path
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D
Step = 0:
--- System Variables = (assignments) ---
--- = Constraints ---
v0 >=3D= v1;
gap >=3D = 0;
------------------------
Step 1:
--- System Variables (assignments) --- =
--- Constraints --- =
gap =3D -1 * PRE(v0) + PRE(v1) = + PRE(gap);
ba-pc!1 = >=3D 0;
v1 =3D = PRE(acc) + PRE(v1);
acc = =3D PRE(acc);
-1 + = ba-pc!1 =3D 0;
ba-pc!1 = >=3D 1;
ba-pc!1 <=3D= 2;
v0 =3D PRE(acc) + = PRE(v1);
gap < = 0;
------------------------
Step 2:
--- System Variables (assignments) --- =
--- Constraints --- =
v0 =3D PRE(acc) + = PRE(v1);
acc =3D = PRE(acc);
gap =3D -1 * = PRE(v0) + PRE(v1) + PRE(gap);
v1 =3D PRE(acc) + PRE(v1);

=
Please look into this. =
-----------------------
= Swarup Mohalik

= --Apple-Mail-18-798100915-- From harryh23@hotmail.com Wed Jun 21 11:01:25 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.2 required=4.0 tests=AWL=-0.074, MAILTO_TO_SPAM_ADDR=0.276,MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Wed, 21 Jun 2006 11:01:25 -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 k5LI1PR6028589 for ; Wed, 21 Jun 2006 11:01:25 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5LI12YT095570 for ; Wed, 21 Jun 2006 11:01:25 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006062111012527011 for ; Wed, 21 Jun 2006 11:01:25 -0700 X-Original-Received: from bay105-f18.bay105.hotmail.com (HELO hotmail.com) (65.54.224.28) by mailgate-external1.sri.com with SMTP; 21 Jun 2006 18:01:24 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Wed, 21 Jun 2006 11:01:24 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Wed, 21 Jun 2006 18:01:20 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: <9749FB75-F590-41E3-A4C0-7F1D5785B864@csl.sri.com> From: "harry huang" To: demoura@csl.sri.com Subject: Re: [SAL] Command issues for adder example Date: Wed, 21 Jun 2006 18:01:20 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 21 Jun 2006 18:01:24.0254 (UTC) FILETIME=[B593F3E0:01C6955C] X-Mailman-Approved-At: Wed, 21 Jun 2006 11:09:44 -0700 Cc: sal@csl.sri.com X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 21 Jun 2006 18:01:26 -0000 Hi Leonardo, Thanks. It works. harry >From: Leonardo de Moura >To: "harry huang" >CC: sal@csl.sri.com >Subject: Re: [SAL] Command issues for adder example >Date: Wed, 21 Jun 2006 08:22:22 -0700 > >Hi Harry, > >You are probably using tcsh or csh. You should use a `\` before the `!`. > >sal-path-finder -v 3 --module='adder{;5}\!Nbitadder > >Cheers, >Leonardo > > >On Jun 20, 2006, at 11:59 AM, harry huang wrote: > >>Hi, >> >>I am running the example -- adder in the examples/adder folder in the SAL >>directory. The README in that example says "sal-path-finder -v 3 >>--module='adder{;5}!Nbitadder'" to generate an execution trace up to >>depth 10, for a 5-bit adder. But when I issue that command, there is >>error mesaage in below: >> >>"Nbitadder: Event not found." >> >>Can someone give me suggestions ? >> >>Haeey >> > From harryh23@hotmail.com Mon Jun 26 07:04:27 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=0.069, MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Mon, 26 Jun 2006 07:04:28 -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 k5QE4Rsv068299 for ; Mon, 26 Jun 2006 07:04:27 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5QE4RYp041709 for ; Mon, 26 Jun 2006 07:04:27 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006062607042725633 for ; Mon, 26 Jun 2006 07:04:27 -0700 X-Original-Received: from bay105-f4.bay105.hotmail.com (HELO hotmail.com) (65.54.224.14) by mailgate-external2.sri.com with SMTP; 26 Jun 2006 14:04:27 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 26 Jun 2006 07:04:26 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Mon, 26 Jun 2006 14:04:23 GMT X-Originating-IP: [70.28.235.58] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: <200606181122.28509.david@mcs.vuw.ac.nz> From: "harry huang" To: sal@csl.sri.com Date: Mon, 26 Jun 2006 14:04:23 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 26 Jun 2006 14:04:26.0897 (UTC) FILETIME=[6F703010:01C69929] X-Mailman-Approved-At: Mon, 26 Jun 2006 10:02:30 -0700 Subject: [SAL] Simulates a concurrent program X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 26 Jun 2006 14:04:28 -0000 Hi, I am just wondering about how to simulate a procedure concurrent program and its wait condition. For instance, the pseudo-code of a concurrent program : === class A Begin wait until A.1 = true .... A.2 wait untile A.3 = true End === I thought about simulating this code into SAL tansition. Is it possible to transform it into the below transition : ====== TRANSITION [ Firstwait: pc = locX and A.1 = true --> pc' = locY -- (HHH) [] Processingcode: pc = locY --> A.2 ; pc' = locZ -- (FFF) [] Secondwait: pc = locZ and A.3 = true --> pc' = locV [] ELSE --> ] ===== I have 3 questions for the above transition. (1). Does it correctly behave the pseudo-code version of the procedure language ? (2).Is the guard in the SAL transition a wait condition ? In other words, the guard " pc = locX and A.1" waits until it becomes true ? However, since there is "ELSE" transition indicating in the above transition,, so if the guard " pc = locX and A.1" is unsatisfied , does the transition jump to execute "ELSE" part , which is not we want to see because "ELSE" part represents the end of our procedure program. (3). For the FFF and HHH mark in the above transition, I am wondering the "pc = locX and A.1 = true" and "A.2 ; pc' = locZ " are atomic ? Thanks. Harry From harryh23@hotmail.com Mon Jun 26 11:14:30 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=0.064, MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Mon, 26 Jun 2006 11:14:30 -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 k5QIEUE7075278 for ; Mon, 26 Jun 2006 11:14:30 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5QIEUYK068193 for ; Mon, 26 Jun 2006 11:14:30 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006062611143010098 for ; Mon, 26 Jun 2006 11:14:30 -0700 X-Original-Received: from bay105-f34.bay105.hotmail.com (HELO hotmail.com) (65.54.224.44) by mailgate-external1.sri.com with SMTP; 26 Jun 2006 18:14:30 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 26 Jun 2006 11:14:30 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Mon, 26 Jun 2006 18:14:29 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com From: "harry huang" To: sal@csl.sri.com Date: Mon, 26 Jun 2006 18:14:29 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 26 Jun 2006 18:14:30.0081 (UTC) FILETIME=[5E086310:01C6994C] X-Mailman-Approved-At: Mon, 26 Jun 2006 11:19:10 -0700 Subject: [SAL] A question for SAL language manual X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 26 Jun 2006 18:14:31 -0000 Hi, I am reading the online SAL language manual and wondering about the following question. In the code example on page 15, should "DEFINITION high = i > 100" be "DEFINITION high = temp > 100" ?. Harry From harryh23@hotmail.com Mon Jun 26 15:16:08 2006 X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com X-Spam-Status: No, hits=0.1 required=4.0 tests=AWL=0.060, MSGID_FROM_MTA_HEADER=0 autolearn=disabled version=3.1.1 date=Mon, 26 Jun 2006 15:16:10 -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 k5QMG8R1080738 for ; Mon, 26 Jun 2006 15:16:08 -0700 (PDT) (envelope-from harryh23@hotmail.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 k5QMG8Wn090728 for ; Mon, 26 Jun 2006 15:16:08 -0700 (PDT) (envelope-from harryh23@hotmail.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 M2006062615160722490 for ; Mon, 26 Jun 2006 15:16:07 -0700 X-Original-Received: from bay105-f18.bay105.hotmail.com (HELO hotmail.com) (65.54.224.28) by mailgate-external1.sri.com with SMTP; 26 Jun 2006 22:16:07 -0000 X-Original-Received: from mail pickup service by hotmail.com with Microsoft SMTPSVC; Mon, 26 Jun 2006 15:16:07 -0700 Message-ID: X-Original-Received: from 65.54.224.200 by by105fd.bay105.hotmail.msn.com with HTTP; Mon, 26 Jun 2006 22:16:02 GMT X-Originating-IP: [130.63.86.137] X-Originating-Email: [harryh23@hotmail.com] X-Sender: harryh23@hotmail.com In-Reply-To: From: "harry huang" To: sal@csl.sri.com Date: Mon, 26 Jun 2006 22:16:02 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed X-OriginalArrivalTime: 26 Jun 2006 22:16:07.0200 (UTC) FILETIME=[1EFD3200:01C6996E] X-Mailman-Approved-At: Mon, 26 Jun 2006 15:32:46 -0700 Subject: [SAL] Simulates concurrent program to SAL X-BeenThere: sal@csl.sri.com X-Mailman-Version: 2.1.3 Precedence: list List-Id: SAL List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 26 Jun 2006 22:16:10 -0000 Hi, I am just wondering about how to simulate a procedure concurrent program and its wait condition. For instance, the pseudo-code of a concurrent program : === class A Begin wait until A.1 = true .... A.2 wait untile A.3 = true End === I thought about simulating this code into SAL tansition. Is it possible to transform it into the below transition : ====== TRANSITION [ Firstwait: pc = locX and A.1 = true --> pc' = locY -- (HHH) [] Processingcode: pc = locY --> A.2 ; pc' = locZ -- (FFF) [] Secondwait: pc = locZ and A.3 = true --> pc' = locV [] ELSE --> ] ===== I have 3 questions for the above transition. (1). Does it correctly behave the pseudo-code version of the procedure language ? (2).Is the guard in the SAL transition a wait condition ? In other words, the guard " pc = locX and A.1" waits until it becomes true ? However, since there is "ELSE" transition indicating in the above transition,, so if the guard " pc = locX and A.1" is unsatisfied , does the transition jump to execute "ELSE" part , which is not we want to see because "ELSE" part represents the end of our procedure program. (3). For the FFF and HHH mark in the above transition, I am wonder