RE: SDL-News: Assert and Progress in Tau 4.4


Subject: RE: SDL-News: Assert and Progress in Tau 4.4
From: Erik Mats (Erik.Mats#telelogic.com)
Date: Mon Mar 08 2004 - 20:38:16 GMT


Become an SDL Forum Society member <http://www.sdl-forum.org/Society/members.htm>
The originator of this message is responsible for its content.
-----From Erik Mats <Erik.Mats#telelogic.com> to sdlnews -----

Dear Cris,

xProgress is in fact a global variable and not a function. What you can do
is add this in a task box:

        /*##CODE
        {
          extern int xProgress;
          xProgress = 1;
        }
        */

If you wanted higher-level language support for xProgress and xAssert, I
think you will find that the following procedure should work for you:

  procedure xProgress;
    start;
      task '' /*##CODE
        ##ifdef SCTSBAUI
        {
          extern int xProgress;
          xProgress = 1;
        }
        ##endif
      */;
    return;
  endprocedure xProgress;

Now, in order to signify progress, you just add a "call xProgress;" to the
transition in question, and you should be good to go.

If building with e.g. an application or simulation kernel, the ##ifdef will
make sure there are no linking errors. Note that some compilers may ask you
to indent the ##ifdef etc differently; I indented for clarity but some
compilers may require that this be at the beginning of the line. If building
for optimized code size you may want to combine both the above approaches in
order to not introduce an unnecessary function definition and call.

Best regards
/Erik
------------------------------------------------------------------------
Think outside the box! Discover DOORS/Analyst - industry-first visual
modeling INSIDE a requirements management tool.
Learn more at www.telelogic.com/doorsanalyst
------------------------------------------------------------------------
Telelogic TAU Support
1-800-577-8449 x 1
mailto:TAUSupport.US#Telelogic.com

Erik Mats
Senior Technical Support Engineer, Team Lead, TAU Support
Telelogic North America Inc,
400 Valley Road Ste 200, Mount Arlington NJ 07856
http://www.telelogic.com
mailto:erik.mats#telelogic.com

Telelogic - Automating the development lifecycle!
------------------------------------------------------------------------
The information contained in this e-mail, including any attachment or
enclosure, is intended only for the person or entity to which it is
addressed and may contain confidential material. Any unauthorized use,
review, retransmission, dissemination, copying or other use of this
information by persons or entities other than the intended recipient is
prohibited.

-----Original Message-----
From: Cris Fuhrman [mailto:christopher.fuhrman#etsmtl.ca]
Sent: Tuesday, March 02, 2004 6:08 PM
To: 'Sdlnews#Sdl-Forum. Org'
Subject: RE: SDL-news: Assert and Progress in Tau 4.4

Become an SDL Forum Society member
<http://www.sdl-forum.org/Society/members.htm>
The originator of this message is responsible for its content.
-----From "Cris Fuhrman" <christopher.fuhrman#etsmtl.ca> to sdlnews -----

I'm partially answering my own question here, but thought it would be useful
for the archives.

xAssert can be hard-coded into a task box in SDL/GR using the /*##CODE ... */
feature, per the example in the documentation:

/*##CODE
##ifdef XASSERT
if (##(s) == ##(r))
xAssertError("s is equal to r");
##endif*/

I have tested this in the SDT validator and it works just fine. It's not
exactly very clean inside an SDL box, but I'm not complaining! No other .c
or .h files are needed.

On the other hand, I've tried the same approach with "xProgress()" not being
sure of the format of this function (the SDT documentation only mentions it
in one place, and I couldn't find anything else, even in searching .h files
in the installation). My attempts to call it with no parameters, with an
integer value of 1, etc. all result in CRASHES during validation. The
linking goes fine, because type-checking isn't too tough in the C compiler I
supposed. I'm not good enough with the Microsoft Visual C++ debugger on a
Pentium 4 to figure it out.

I've sent a support request to Telelogic about the crashing, and will report
back any information.

Regards,

Cris

--
Prof. Christopher Fuhrman
École de technologie supérieure (ETS)
+1 (514) 396 8638

-----Original Message----- From: owner-sdlnews#sdl-forum.org [mailto:owner-sdlnews#sdl-forum.org] On Behalf Of Cris Fuhrman Sent: Monday, 01 March 2004 18:55 To: Sdlnews#Sdl-Forum. Org Subject: SDL-news: Assert and Progress in Tau 4.4

Hello,   This is a question specific to Telelogic Tau 4.4, which is what we use currently in our courses at the ETS.   Reading the documentation, I've come to the conclusion that it is not possible to use the functionality of "assert" (safety property) and "progress" (liveness property) for validation (state exploration) without declaring the functions in C. This seems counter intuitive, since decisions blocks (which are Booleans after all) are supported in Tau 4.4 without having to generate C functions.   Is there a way to do xAssert/xProgress in a pure SDL model without having to pass into the realm of C? For the early stages of my course, I would like for my students to not be bogged down with .h files for their lightweight models, yet still be able to validate them.   Has anyone considered SDL support for assert/progress on a higher level?   Thanks in advance,   Cris Fuhrman   -- Prof. Christopher Fuhrman École de technologie supérieure (ETS) +1 (514) 396 8638  

--End text from "Cris Fuhrman" <christopher.fuhrman#etsmtl.ca> to sdlnews --- For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm> or (iff this does not answer your question) email: owner-sdlnews#sdl-forum.org --End text from Erik Mats <Erik.Mats#telelogic.com> to sdlnews --- For extra SDL Forum Society benefits join at <http://www.sdl-forum.org/Society/members.htm>



This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT