DESpot - unlock the DES potential

DESpot is a discrete-event system (DES) software research tool. It supports both flat projects (collection of plant and supervisor DES), and Hierarchical Interface-Based Supervisory Control (HISC) projects. DESpot also supports timed DES projects that use Sampled-data Supervisory Control.

To the left is an image of a DESpot HISC project editor. For more screenshots, see the online help files for DESpot here.

You can download a copy of DESpot here.


[Picture of DESpot HISC Project Window]

DESpot Mailing List

If you would like to be added to DESpot's low volume mailing list for new releases, please send an e-mail to (leduc aT mcmaster dOt ca) with subject: add to DESpot list.


DESpot News

  • Dec 30, 2015: DESpot 1.6.0 released. New features include support for defining template DES, and then instantiating multiple copies for flat or HISC projects. If you have multiple DES identical up to relabelling, this will be a big time saver. This version also includes several important bug fixes for the HISC project interface.
  • Feb 24, 2015: DESpot 1.5.0 released. New features include support for per-component simulation for HISC projects as well as simulation of automatically generated counter examples. You can also choose to start simulating at the first failed state encountered during a verification.
  • Dec 30, 2013: DESpot 1.4.0 released. New features include support for multi-level HISC projects including experimental support for multi-level HISC with low data events for the non-BDD algorithms. Multi-level synthesis is not yet supported. This release also adds distributed algorithms for the Linux version of DESpot using MPI libraries.
  • Dec 7, 2012: DESpot 1.2.0-2 under Mac OS X. The new version now compiles and runs under Mac Os X. The build instructions have been updated to now include Mac OS X compilation.
  • Nov 27, 2012: Issue with BDDSD Algorithms. The SD controllability and S-singular prohibitable behavior checks require that you first make sure the project is ALF or they could go into an infinite loop. Running the "Check All" menu command will enforce this. This restriction will be removed in the next version.
  • Nov 13, 2012: DESpot 1.2.0-1 released. This fixes a minor output bug under Windows that caused the state names in error messages from the BDD code to be printed incorrectly.
  • Oct 17, 2012: DESpot 1.2.0 released. New features include the integration of the bddSD algorithms. These are binary-decision diagram (BDD) based algorithms capable of handling systems at least as large as 10^15 states. They can verify nonblocking, untimed controllability, SD controllability, proper time behavior, S-singular prohibitable behavior, plant completeness, and activity-loop-free checks.

Help Browser

DESpot comes with a detailed help browser. The help pages can also be viewed here. You will find a detailed description of the features offered by DESpot, instructions on how to use DESpot, as well as many screenshots. You can download DESpot's user manual (same material as above link) in PDF form here


DESpot Features

  • Supports flat DES projects and HISC projects, including low data events. For more information on HISC, see the publication list below.

  • DESpot has a graphical DES editor, including export to postscript and PNG graphic formats.

  • DESpot can verify the three main HISC properties individually, or as a group using the "Check Project" menu item. Check project runs each property check in a separate thread, so if you have a quad-core CPU, you could see around a 3x speedup.

  • DESpot now includes the bddHISC algorithms. bddHISC can verify an HISC project, or do HISC synthesis using binary-decision diagram (BDD) based algorithms capable of handling individual components at least as large as 10^15 states. The bddHISC algorithms have now been extended to support systems with low data events.

  • DESpot allows the entry of timed DES (TDES) projects for use with Sampled-data Supervisory Control (see publication list below). DESpot now includes the bddSD algorithms. These are binary-decision diagram (BDD) based algorithms capable of handling systems at least as large as 10^15 states. They can verify nonblocking, untimed controllability, SD controllability, proper time behavior, S-singular prohibitable behavior, plant completeness, and activity-loop-free checks.

  • DESpot has a built in DES simulator that includes graphical simulation of the DES. DESpot can also use the HISC structure to accelerate the simulation.

  • DESpot supports multi-level HISC projects including experimental support for multi-level HISC with low data events for the non-BDD algorithms. Multi-level synthesis is not yet supported.

  • The Linux version of DESpot supports distributed algorithms allowing DESpot verification and synthesis operations to be distributed over a network of computers. MPI libraries are used for this. Please note that the distributed algorithms do not currently support projects with templates.

  • DESpot supports per-component simulation for HISC projects as well as simulation of automatically generated counter examples.

  • DESpot supports template DES which can then be instantiated multiple times.

  • The DESpot DES and project files are XML, so they can be edited using a text editor, if needed.

  • DESpot is open source software, released under the GNU General Public license (GPL), version 2. See below for more information.


Download Information

You can download a copy of DESpot here.

If you make use of DESpot, please send an e-mail to (leduc@mcmaster.ca) stating so, and providing the name of the organization you work for. We would simply like to get an idea of how useful people are finding DESpot.


DESpot Contributors

For a list of contributors to DESpot, see here.


Publications Relevant to DESpot

R.J. Leduc, "Hierarchical Interface-Based Supervisory Control with Data Events," International Journal of Control, vol. 82, no. 5, pp. 783 - 800, May, 2009. [Online Access]. See also Software Quality Research Laboratory Technical report No. 44.

R.J. Leduc, P. Dai, and R. Song, "Synthesis Method for Hierarchical Interface-Based Supervisory Control," IEEE Trans. on Automatic Control, vol 54, no 7, pp. 1548-1560, Jul. 2009. [Online Access] See also Software Quality Research Laboratory Technical report No. 46.

Ryan Leduc and Yu Wang. Sampled-data supervisory control. Proc. 10th International Workshop on Discrete Event Systems (WODES'10), pages 353-359, Berlin, Germany, Aug 2010. Click here to download PDF copy: sdContwodes2010.pdf (253KB).

R.C. Hill, J.E.R. Cury, M.H. de Queiroz, D.M. Tilbury, and S. Lafortune, "Multi-level hierarchical interface-based supervisory control," Automatica, vol 46, no 7, pp. 1152-1164, July. 2010. [Online Access].


Copyright

The software available from this page has been release under the GNU General Public license (GPL), version 2. For specific details of the terms of the GPL, please read the license here. For more information on the GPL, please see the Free Software Foundation.

The general idea is that the GPL allows you to take a copy of the software and pretty much do what you want with it. You are also given access to the source code. You are free to use the source code to make a new program, but the new program must also be released under the GPL. You can include parts or all of the program in your own program, as long as you distribute your program under the GPL or a compatible license.

You could also choose to add functionality to the program, to suit your own needs.


The programs on this page are distributed in the hope that they will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.


Please send any problem reports to: leduc@mcmaster.ca