V0.8

• 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

v0.7

• added JSON output and one-step simulation to tck-simulate (please, refer to wiki for details)
• added concrete run counter-examples to tck-reack (algorithms reach and covreach) -- contribution by Ocan Sankur

v0.6

• Safe implementation of DBMs (clean type for difference bounds)
• Symbolic reachability counter-examples
• Backward state-space computation
• Various bugfix and improvements

v0.5

• reduction in memory usage by sharing state components (tuple of locations, zones, etc) between states of transition systems (zone graph)
• allocators with collection of unused shared objects for transition systems
• upgraded unit tests to Catch2 librabry v3

v0.4

• Added command line simulator tck-simulate
• Added liveness checking tool tck-liveness
• Improved syntax check in tck-syntax
• Various bug fix

Fixed build issues

• Fixes #2 #3 #4
• Fixes compilation issues
• Improved documentation

First public version of TChecker

v0.1