- Symbolic counter-example generation for liveness (tck-liveness)
- Choice of symbolic/concrete counter-example to reachability (tck-reach)
- Fixed a bug in generation of symbolic and concrete counter-examples to reachability (tck-reach)
- Added output of asynchronous events in a model (tck-syntax)
- Added finite state machines: transition systems for models with no clocks
- Various improvements