Subject: SDL-News: Assert and Progress in Tau 4.4
From: Cris Fuhrman (christopher.fuhrman#etsmtl.ca)
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, Ive 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,
Prof. Christopher Fuhrman
École de technologie supérieure (ETS) P>+1 (514) 396 8638
--End text from "Cris Fuhrman"
This archive was generated by hypermail 2a23
: Thu May 09 2013 - 16:05:50 GMT
This archive was generated by hypermail 2a23 : Thu May 09 2013 - 16:05:50 GMT