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

Subject: RE: SDL-News: Assert and Progress in Tau 4.4
michael.andersson#telelogic.com
Date: Mon Mar 08 2004 - 11:00:59 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 michael.andersson#telelogic.com to sdlnews -----

Hi Chris,

since neither the Assert nor the Progress mechanisms are SDL concepts,
Telelogic has chosen a "cheaper" C solution on how to support these
extensions to SDL systems, while normal SDL concepts are transparantly
implemented by C. (Since you need a C compiler environment to run the
Validator as well as the Simulator and C Code generators, the difference is
really only appearance.)

If you want a "nicer" appearance of this, just embed the task containing C
in an SDL operator or an SDL procedure. These can be placed in a "validation
utility" package that your students can import to their system when working
with Validation.

Example:
  procedure Report; fpar in str charstring;
    start;
      task '' /*##CODE xAssertError( ##SDL(str)+1 ); */;
      return;
  endprocedure Report;

  <...>

  decision s = r;
    (true) :
      call Report('s is equal to r');
  <...>

Unfortunately, I do not have any experience of using xProgress, so I cannot
help you with this.

regards
Michael
----------------------------------------------------------------------------
----------
Telelogic Tau Generation 2 - Development Visualized. Productivity Realized.
Learn more about Telelogic's new software development solution at
http://www.taug2.com

Michael Andersson <mailto:michael.andersson#telelogic.com>
Field Application Engineer Phone: +46 40 17 47 00
Telelogic Direct: +46 40 17 47 65
P.O. Box 4128 Mobile: +46 705 17 47 65
SE 203 12 MALMO Fax: +46 40 17 47 47
Sweden <http://www.telelogic.com>

Telelogic - Automating the development lifecycle
----------------------------------------------------------------------------
----------

> -----Original Message-----
> From: Cris Fuhrman [mailto:christopher.fuhrman#etsmtl.ca]
> Sent: den 3 mars 2004 00:08
> 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>
> For help, email "majordomo#sdl-forum.org" with the body of
> your email as:
> help
> or (iff this does not answer your question) email:
> owner-sdlnews#sdl-forum.org
>

--End text from michael.andersson#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