EST 2nd Edition

Overview

Features:

• [all] based on Biddy BDD package, includes API functions for Tcl/Tk GUI called My Interface, uses POSIX threads *
• [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 strict EU, EG, AW, and AF, 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] extended CCS parser, parser for Verilog netlists

Previews: license, menu, dialog,

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.

Download

EST 2nd Edition - release 5.x

• [bdd] added experimental drawing of BDDs using bddview
• [versis] implemented rename/hide/forbid of actions
• [versis] implemented deadlock/divergent checking

• [all] modul gui added which covers functions removed in My Interface v0.99
• [all] modul bdd added which covers functions removed in Biddy v0.99
• [all] pthreads (for Win32) updated to release 2.8.0
• [all] bison (for Win32) updated to release 2.1
• [all] flex (for Win32) updated (still 2.5.4a)
• [all] makefiles for building projects on Win32 added
• [all] makefiles improved and simplified
• [all] Tcl/Tk related files are now compiled with Tcl Stubs
• [all] added experimental Makefiles for Mac OS X
• [mc] fixed and improved on-the-fly model checking for ACTL/ACTLW
• [ccs] CCS parser improved

• est-2ed-5-2a-source.zip, Jul 31, 2008, SVN revision 38
• 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-2ed-5-1-Linux-mish.zip (i386, GNU/Linux, Tcl/Tk),
• est-2ed-5-1-Linux64-mish.zip (i386-64, GNU/Linux, Tcl/Tk),
• est-2ed-5-1-SunOS-mish.zip (sun4u, Solaris, Tcl/Tk),
• est-2ed-5-1-Win-mish.exe (i386, Win32, Tcl/Tk).

• est-2ed-5-1-Linux.zip (i686, GNU/Linux),
• est-2ed-5-1-Linux64.zip (i686-64, GNU/Linux),
• est-2ed-5-1-SunOS.zip (sun4u, Solaris),
• est-2ed-5-1-Win.zip (i686, Win32).

EST 2nd Edition - release 4.5 (Jun 11, 2007)

• [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 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

• [all] module ccs added
• [all] CCS parser moved from module versis to module ccs
• [all] bdd package becomes a separated project called Biddy
• [all] mingw and sunos specific files removed from the project
• [all] examples and projects cleaned
• [all] makefiles for Linux changed to support gcc v4
• [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] 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
• [ccs] CCS parser fixed and more roboust

• 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)

• [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

• [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

• 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)

• [versis] CCS parser
• [mc] standard ACTL model checking
• [mc] counterexamples and witnesses for standard ACTL operators

• [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

• 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.

• est-2ed-2-0, Aug 7, 2003 (not available).

History

• Project EST started in 1992. In 1999, we begin to introduce new features in EST. However, we wanted to keep one branch of the package simple, because of its suitability of demonstrating the basic algorithms. Therefore, we made the copy of a package and called it 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.