EST 2nd Edition
Overview
Project: Efficient Symbolic Tools - 2nd Edition
Synopsis: EST 2nd Edition is a toolbox for the formal verification of concurrent systems
Administrator: Robert Meolic (robert@meolic.com)
Authors: Robert Meolic, Tatjana Kapus, Zmago Brezočnik
History: started in 2000, first release in 2003
COBISS-ID: 5626902 (this number is used by Slovenian libraries)
Features:
[all] based on BDD package Biddy, includes API functions for Tcl/Tk GUI called My Interface, uses POSIX threads (currently disabled)
[pa] parser for simple textual representation of processes, encoding and decoding of processes, decoding of compositons, copying processes, process2composition, composition2process
[versis] parallel composition, multi-way parallel composition, checking strong equivalence, observational equivalence, testing equivalence, and trace equivalence, minimization with regard to strong, observational, and trace equivalence, renaming, hiding and forbiding actions, searching for deadlocks and divergences
[mc] ACTL model checking, ACTLW model checking based on EEU, EEG, AAW, and AAF, inevitable model checking, on-the-fly model checking, linear witnesses and counterexamples, diagnostic, witness and counterexample automata
[strucval] synchronous product of LTSs and witness/counterexample automata
[ccs] enhanced CCS parser
[verilog] parser for Verilog netlists
. . .
EST 2nd Edition - release 6.3 (Feb 7, 2019)
New features
[all] output is now via sockets to support remode mode (e.g. WebEST)
[all] modul verilog added which provides a parser for Verilog netlists
[mc] ACTL/ACTLW formulae given in the file can have names
[mc] added support for WASync project
Other significant changes from release 5.7
[all] updated My Interface to 1.3
[all] updated Biddy (v1.8.2 is required for release 6.3)
[all] removed Makefiles for SunOS, linking simplified, without def files on MS Windows
[all] now, the same shared library is used with and without Tk GUI
[all] documentation improved, comment's style changed to support doxygen
[bdd] module bdd reorganized to support additional BDD types and additional BDD packages
[pa] BDD related part of pa module moved to bdd module
[pa] processes and compositions are never overwritted
[pa] a big improvement on state management and Pa_CopyProcess
[pa] a big improvement on counting states and transitions
[versis] improved parallel composition
Download sources
est-2ed-6-3-source.zip, Feb 7, 2019, SVN revision 190
est-2ed-6-2-source.zip, Oct 9, 2017, SVN revision 160
est-2ed-6-1-source.zip, Jul 15, 2016, SVN revision 133
est-2ed-6-0-source.zip, Sep 01, 2015, SVN revision 107
. . .
EST 2nd Edition - release 5.7 (Apr 25, 2015)
New features
[all] added main program (it can be used instead of wish)
[all] added cmdsh mode (tcl api without mish gui)
[bdd] added experimental drawing of BDDs using bddview
[pa] added reporting processes in FSP format (usable with LTSA tool)
[versis] implemented rename/hide/forbid of actions
[versis] implemented deadlock/divergent checking
[mc] model checker enhanced by Spin trail generation (usable with st2msc tool)
[mc] model checker enhanced by MSC generation (usable with mscgen tool)
Other significant changes from release 4.5
[all] updated My Interface to 1.1 (improved menus and xsource command)
[all] Biddy is isolated and does not belong to EST project anymore
[all] Biddy is now dynamically linked (v1.3 is required for release 5.7)
[all] modul gui added which covers functions removed in My Interface
[all] modul bdd added which covers functions removed in Biddy
[all] on MS Windows, bison, flex, and pthreads are now from MINGW distribution
[all] added Makefiles for MacOSX (Darwin)
[all] improved makefiles and packaging files, added debian and rpm packaging
[all] adapted for 64-bit architectures
[all] projects improved and cleaned
[all] examples improved and cleaned
[all] added documentation for examples
[all] now, Tcl Stubs are used everywhere (to support changes in Tcl 8.5.10)
[bdd] added Bdd_StabRS
[bdd] Bdd_RelOp, Bdd_RelOpSimple, and Bdd_RelOpComplex greatly improved
[pa] improved to produce usable result without explicitly enumeration of all transitions
[versis] improved parallel composition
[mc] fixed and greatly improved on-the-fly model checking for ACTL/ACTLW
[ccs] CCS parser improved
Download sources
est-2ed-5-7-source.zip, Apr 25, 2015, SVN revision 104
est-2ed-5-6-source.zip, Jun 20, 2014, SVN revision 86
est-2ed-5-5-source.zip, Apr 29, 2013, SVN revision 78
est-2ed-5-4-source.zip, Jul 6, 2012, SVN revision 64
est-2ed-5-3-source.zip, May 16, 2012, SVN revision 55
est-2ed-5-2-source.zip, Nov 01, 2010, SVN revision 43
est-2ed-5-1-source.zip, Jun 20, 2008, SVN revision 37
est-2ed-5-0-source.zip, Oct 18, 2007, SVN revision 35
. . .
EST 2nd Edition - release 4.5 (Jun 11, 2007)
New features
[mc] ACTL/ACTLW formulae can be read from file without starting model checker
[mc] ACTL/ACTLW formulae can use macros
[mc] added basic on-the-fly model checking for ACTL/ACTLW
[ccs] CCS parser extended to allow complex prefixes and action hiding ( [TAU/x] )
[ccs] CCS parser extended to support composition of minimized processes
[ccs] CCS parser extended to support minimization of composition
[ccs] CCS parser extended to support witness and counterexample automata
[ccs] CCS parser extended to support multi-way composition
[ccs] CCS parser extended to support on-the-fly model checking
[ccs] added parser for Verilog netlists
Other significant changes from release 3.5
[all] module ccs added
[all] bdd package becomes a separated project called Biddy
[all] mingw and sunos specific files removed, makefiles for Linux improved to support gcc v4
[all] examples and projects cleaned
[all] FSF rules to make program free are more strictly considered
[pa] counting states and transitions is now much faster
[pa] implemented smart encoding of processes
[pa] fixed renaming of processes
[versis] CCS parser fixed and more roboust
[versis] CCS parser moved from versis module to ccs module
[versis] fundamental-mode normalization changed
[versis] added step-by-step composition
[mc] added formula table
[mc] fixed diagnostic for AAW
[mc] added inevitable sets calculations for ACTL/ACTLW
Download sources
est-2ed-4-5-source.zip, Jun 11, 2007, SVN revision 30
est-2ed-4-4-source.zip, May 8, 2007, SVN revision 20
est-2ed-4-3-source.zip, Jan 15, 2007, SVN revision 10
est-2ed-4-2-source.zip, Oct 20, 2006, SVN revision 4
est-2ed-4-1-source.zip, Oct 6, 2006, SVN revision 3
est-2ed-4-0-source.zip, Jun 5, 2006
. . .
EST 2nd Edition - release 3.5 (Jun 12, 2006)
New features
[pa] processes can have final states
[pa] processes can be reported in CCS format
[versis] CCS parser extended with new composition types
[mc] strict ACTLW operators
[mc] witness and counterexample automata generation
[mc] minimization of WCA
[strucval] synchronous product
Other significant changes from release 2.2
[all] module strucval added
[all] improved dialogs
[all] makefiles improved, OS is now automaticaly recognized
[all] supported tcl/tk 8.4
[all] program sets unlimited stacksize (not working on Win32)
[all] threads are disabled
[all] functions using threads are now in separated files
[pa] fixed copying of processes
[pa] states, sorts and processes can be deleted
[pa] parser for process algebra is more roboust
[versis] CCS parser fixed
[versis] CCS parser improved, e.g. (a + b).P is now equal to a.P + b.P
[versis] composition of processes is simplified
[mc] semantics of standard ACTL fixed
[mc] precedence of Boolean and temporal operators fixed
[mc] HME and HMA are now strong version of HM operators
[mc] model checking is now based on strict ACTLW operators
[mc] ACTL/ACTLW formula can be given as a string parameter
[mc] parser for ACTL/ACTLW is more roboust
Download sources
est-2ed-3-5-source.zip, Jun 12, 2006
est-2ed-3-4-source.zip, May 26, 2006
est-2ed-3-3-source.zip, Feb 2, 2006
est-2ed-3-2-source.zip, Dec 19, 2005
est-2ed-3-1-source.zip, Nov 16, 2005
est-2ed-3-0-source.zip, Aug 03, 2004
. . .
EST 2nd Edition - release 2.2 (Feb 17, 2004)
New features
[versis] CCS parser
[mc] standard ACTL model checking
[mc] counterexamples and witnesses for standard ACTL operators
Other significant changes from release 2.0
[pa] states can be marked as deleted
[pa] encoding of processes is simplified
[pa] decoding of composed states improved
[pa] the maintaining of gates changed
[pa] option GATES removed from syntax of textual description of LTS
[pa] parser for textual description of LTS can now read the syntax from 1st Edition
[pa] parser for process algebra is now more roboust
[pa] added simple recovery on syntax errors
[versis] equivalences between processes with different sorts fixed
[versis] all minimizations greatly improved
[mc] semantics of ACTLW fixed
[mc] W is used instead of UU for unless
[mc] parser for ACTL/ACTLW is now more roboust
[mc] added simple recovery on syntax errors
Sources
est-2ed-2-2, Feb 17, 2004 (not available)
est-2ed-2-1, Sep 16, 2003 (not available)
. . .
EST 2nd Edition - release 2.0 (Aug 7, 2003)
This was the initial release of EST 2nd Edition. It was capable of representation of concurrent systems with LTSs, parallel composition of LTSs, multi-way parallel composition of LTSs, strong, observational testing and trace equivalence checking between LTSs, minimization of LTSs with regard to strong, observational, and trace equivalence, ACTLW model checking based on EEU, EEG, AAW, and AAF, and generation of counterexamples and witnesses.
Sources
est-2ed-2-0, Aug 7, 2003 (not available)
History notes
Project EST started in 1992 and version 1.0 was ready in 1999. We wanted to keep original branch of the package simple, because of its suitability of demonstrating the basic algorithms. Therefore, we made the copy of a package before introducing new features (September 2000). Original branch became EST 1st Edition while the new one is called EST 2nd Edition. Later, we made a lot of changes in data structures and algorithms of EST 2nd Edition and they become incompatible with the ones used in EST 1st Edition. Hence, modules from EST 1st Edition and EST 2nd Edition are not interchangeable.
In August, 2003, a release 2.0 was formed as a first official release of EST 2nd Edition. We started with number 2 to avoid the confusion with modules in EST 1st Edition.
From August 2003 until October 2006, EST 2nd Edition project used a CVS repository. In October 2006, we deleted it and created a SVN repository
Acknowledgement: Until now, the project EST 2nd Edition has been entirely realized during the research process on Faculty of Electrical Engineering and Computer Science in Maribor, Slovenia. We are collaborating with Formal Methods and Tools Group at ISTI in Pisa, Italy.
