SDL-News: Assert and Progress in Tau 4.4

Subject: SDL-News: Assert and Progress in Tau 4.4
From: Cris Fuhrman (
Date: Mon Mar 01 2004 - 23:55:02 GMT



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) P>+1 (514) 396 8638

--End text from "Cris Fuhrman" to sdlnews --- For extra SDL Forum Society benefits join at

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