EST 2nd Edition, version 4.5, released on Jun 11, 2007.

Changes 5.0a versus 4.5
- modul gui added which covers functions removed from My Interface
- modul bdd added which covers functions removed from Biddy
- makefiles improved and simplified
- makefiles for building projects on Win32 added
- implemented rename/hide/forbid of actions
- implemented deadlock/divergent checking

Changes 5.0b versus 5.0a
- added experimental drawing of BDDs using bddview
- some reorganisation of bdd modul

Changes 5.0c versus 5.0b
- modul bdd simplified and optimized

Changes 5.0 versus 5.0c
- released on Oct 18, 2007
- fixed Win32 specific files corrupted in 5.0c
- fixed experimental drawing of BDDs on Win32
- removed minor bugs from experimental drawing of BDDs

Changes 5.1 versus 5.0
- released on Jun 18, 2008
- Biddy and bddview updated
- CCS parser improved
- Tcl/Tk related files are now compiled with Tcl Stubs
- added experimental Makefiles for MacOSX
- sources cleaned and fixed

Changes 5.2 versus 5.1
- released on Nov 01, 2010
- fixed inevitable model checking of HMA
- improved on-the-fly model checking
- Biddy is removed from EST project
- Biddy is now dynamically linked
- executable script renamed to est2ed.tcl
- pkgIndex.tcl added
- library is now just one file called libest2
- improved Makefiles for MacOSX
- added debian and rpm packaging

Changes 5.3 versus 5.2
- released on May 16, 2012
- all modules are using TCL stubs (to support changes in Tcl 8.5.10)
- improved xsource command in gui
- on MS Windows, bison, flex, and pthreads from MINGW distribution are used
- improved packaging on MS Windows (using 7zsd.sfx)

Changes 5.4 versus 5.3
- released on Jul 06, 2012
- improved menus in gui
- added main program (it can be used instead of wish)
- improved packaging on Linux (using pbuilder)

Changes 5.5 versus 5.4
- released on Apr 29, 2013
- changed to use Biddy v1.1 (not compatible with Biddy v1.0)
- character '\' is now correctly shown in gui
- improved pa for better CCS support (PROC1 = PROC2)
- added reporting processes in FSP format (usable with LTSA tool)
- model checker enhanced by Spin trail generation (usable with st2msc tool)
- model checker enhanced by MSC generation (usable with mscgen tool)
- for AND, OR, EQV, and IMPL model checker now explains one part, only
- improved ccs parser (multi-line formulae)
- fixed and improved many examples
- added documentation for examples
