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

DESpot News

• Dec 29, 2021: DESpot 1.11.0 released. This release ports DESpot to QT 5 and allows it to compile on Windows 10. As a result postcript and encapsulated postcript are no longer supported, but encapsulated PDF is now supported for exporting diagrams of your DES.
  
  
• Dec 30, 2019: DESpot 1.10.0 released. This release adds support for specifying decentralized supervisory control structure for a project, and verifying co-observability.
  
  
• Dec 15, 2019: DESpot 1.9.0 released. This release adds support for Fault-Tolerant (FT) Supervisory Control, including both timed and untimed controllability and nonblocking BDD-based algorithms, for several fault scenarios. This release also adds support for verification of timed controllability, including BDD-based algorithms.
  
  
• Oct 3, 2019: DESpot 1.8.0 released. This release adds regression testing features to the windows version of DESpot. It also includes curved transition arrows for DES diagrams, and the ability to export DES diagrams to EPS. As well, there are a few bug fixes. Most notably, the non-BDD nonblocking algorithm no longer gives a segmentation fault for large projects, and the tabular editor is no longer disabled.
  
  Also, DESpot now targets version 4.8.7 of the Qt libraries, RedHat Enterprise Linux 7, and MS Windows 10 with MS Visual Studios 2019.
  
  
• Dec 30, 2017: DESpot 1.7.0 released. This release adds regression testing for DES algorithms. User can create test suites specifying projects to test, algorithms to run, as well as expected results. This is intended to make it easy to retest known projects when DESpot has been updated to make sure errors haven't been introduced. NOTE: This is currently a Linux only release.
  
  
• 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.
  
  

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.

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, encapsulated postscript (EPS), 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. Update: MPI support is not currently compiling with the latest set of changes.

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

• DESpot supports regression testing for DES algorithms. User can create test suites specifying projects to test, algorithms to run, as well as expected results.

• DESpot supports both timed and untimed Fault-Tolerant Supervisory Control, including BDD-based algorithms.

• DESpot supports specifying decentralized supervisory control structure for a project, and verifying co-observability.

• 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

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.