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

Subject: RE: SDL-News: Assert and Progress in Tau 4.4
From: Cris Fuhrman (christopher.fuhrman#etsmtl.ca)
Date: Tue Mar 02 2004 - 23:08:25 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 "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>

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