From the Tools menu, select Verify Project Integrity or from the toolbar, click
on the Verify Project Integrity button . This
will run a series of checks to verify the project is Valid. If the project
fails any of these checks, a message box will display the number of errors and warnings, and the
Output Tab will provide a list of errors and warnings. Note that most
algorithms (nonblocking, controllability, sync, etc) will refuse to run on an invalid project.
WARNING: if the project integrity check passes, but you get an integrity related error about DES when running an algorithm, run Clean Project, and then re-run the integrity test.
From the Tools menu, select Check Project or from the toolbar, click
on the Check Project button . This will open the
following window.
From here you can choose which properties to check. An Incremental check will check all the properties that you have selected and that have either not been checked, or have failed during the last check. A Complete Recheck will check all the properties you have selected regardless of current status.
From the Tools menu, select Clean Project. This will discard any data saved from a previous check and "clean" the project and DES of any precomputed information. This means that you will have to re-check the various properties of your project in order to have each property valid again. If a project was created by an earlier version of DESpot and is producing odd results, doing a "Clean Project" may solve the issue.
From the Tools menu, select Nonblocking or from the toolbar, click
on the Check Nonblocking button . This will
run an automata based algorithm to check that the synchronous product of your project is nonblocking.
From the Tools menu, select Controllabiltiy or from the toolbar, click
on the Check Controllability button .
This will run an automata-based algorithm to verify that the synchronous product of your project supervisor DES
is controllable for the synchronous product of your plant DES. Note that the algorithm assumes that your closed-loop
system is constructed using the synchronous product.
From the Tools menu, select Project Meet or from the toolbar, click
on the Meet button . Please Note: This will create
a DES from the synchronous product of all project DES. In order to perform a meet operation, the event sets of all
the DES in the project must be identical.
From the Tools menu, select Project Sync or from the toolbar, click on the
Sync button . This will create a DES from the
synchronous product of all project DES.
From the Tools menu, select Project Synthesis. This will create a
supremal, controllable, nonblocking supervisor for the project.
Please note: This feature is not yet implemented.
From the Tools menu, select System Simulation or from the toolbar, click
on the System Simulation button . This will open
the DES System Simulation window. Please note that the project must be
Valid before the simulator can be used.
From the Tools menu, select TDES Controllability. This will run an automata-based algorithm to verify that the synchronous product of your project supervisor DES is TDES controllable for the synchronous product of your plant DES. Note that the algorithm assumes that your closed-loop system is constructed using the synchronous product. It is required that each DES in the project must contain a controllable event called tick, with alias t.
DESpot does not currently allow one to directly specify which events are forcible in a timed DES. Instead it uses the sampled-data supervisory control assumption that the set of forcible events is equal to the set of prohibitable (controllable non-tick) events.