Breach doc: Graphical User Interfaces (GUIs)

Home       Download and install       Systems       Simulation       Temporal Logic       Parameter sets       Graphical User Interfaces      

Systems, parameters and properties files

The upper part of Breach main GUI is as follows.

images/breach_main_gui_top.png

The top of the window indicates in which folder Breach is operating. In the above case, we are working with the Lorenz system.

The System panel

This panel contains basic informations on the system and some adjustable options for the numerical solver. DimX is the number of variables and DimP the number of parameters (including initial conditions) of the system. The most important tunable parameters for the numerical solver in this panel are AbsTol and RelTol which are absolute and relative tolerances. Correctly tuning those is crucial to obtain accurate simulations. A discussion on how to do this can be found, e.g., there. A (relatively) general rule is that RelTol should be no larger than 1e-4 and AbsTol should be small with respect to typical values taken by the variables.

Note that options for the solver are set in the CreateSystem.m script and a finer tuning can be achieved by using CVodeSetOptions and CVodeSetFSAOptions (for sensitivity analysis) functions but make sure you know what you are doing there.

The Param. Sets panel

This panels allows to manipulate and save parameter sets. At the top of it, the path of the file which stores all parameter sets currently loaded is given. A default name for this file is SystemName_param_sets.mat.

Here is the purpose of each button (though their function should be relatively obvious from their names):

  • New creates a new default parameter set
  • Copy creates a copy of the selected parameter set
  • Remove delete the selected parameter set
  • Save in save the current parameter set in another file
  • Save save all parameter sets in their current state. There is no automatic saving, so don't forget to use this button before closing Breach
  • Rename change name of the current parameter set

The (*) before a parameter set indicates that this set contains computed trajectories, which you can explore by clicking on "Explore trajectories". Note that computed trajectories can take a lot of memory.

The Properties panel

This panels manages set of properties for the system. A default file named SystemName_properties.mat is loaded when Breach is started and saves all the properties defined by the user. but other files of properties can be loaded and saved using through the File menu. Here are what the buttons good for :

  • New ok, you guessed it.
  • Del same here
  • Edit allows to modify the parameters bound to the selected property, if it has any
  • Check check the property for all parameters defined in the current parameter set. It pops up a dialog box asking for a time span for the trajectory computation, which can be left empty if trajectories were computed beforehand, and a time for the property verification, i.e., from when to evaluate the property for the trajectories

Note properties are automatically saved after each modification.

Modify and plot the current parameter set

The bottom part of the main GUI allows to view and modify the parameter set selected in the "Param. sets" panel. In the following screenshot, we edit the parameter set P1 (see above).

images/breach_main_gui_bottom.png

A parameter set is composed of a number of subsets. Here there are 60 of them. Each subset consists in a parameter valuation and a range, making it technically a centered hyperbox. A projection of these hyperboxes can be plotted in the bottom right part of the interface.

Fixed and uncertain parameters

The "Fixed Parameters" panel lists all parameters of the systems (the DimX first ones being initial conditions). The "Uncertain Parameters" list parameters which can vary in a given range. All parameters which are not present in the "Uncertain Parameter" list have the same value for all subsets of the current parameter set. Parameters can be moved from the "Fixed" list to the "Uncertain" list only if the parameter sets does not have subsets.

Selecting and modifying subsets

The "Select subset" panel allows to browse subsets by mean of a slider and select/unselect ("Selected" checkbox) the current subset pointed by the slider. Selected subsets can be copied into a new parameter set or removed using the dedicated buttons. Note that the "Select… " menu proposes other options to select/unselect groups of subsets based, e.g., on the property satisfaction of trajectories.

The "Modif current subset" panel allows to change the value and range of the current uncertain parameter of the current subset.

Refining subsets

Refining a parameter set divides it into subsets. If "Refine all" is checked, all subsets will be refined similarly. Otherwise only the current subset is refined. If "quasi-random" is checked, the textbox should be given a number file: and when the subsets are refined into k subsets uniformly distributed quasi-randomly. Otherwise subsets are refined into regular grid of size in every directions. Grids with different sizes in different directions can be obtained by providing a vector. E.g., if =[4 4 10] is entered, the subsets will be refined into regular 3D grids of size 4x4x10.

Computing and exploring trajectories

When the button Compute Trajectories is used, a dialog box appears requesting a time span for computing trajectories. The most commonly used format is t0:dt:tf. E.g., 0:.1:10 will compute trajectories at times 0, 0.1, 0.2, …, 9.9, 10. When computation is over, a star appears before the name of the current parameter set in the list of parameter sets. This means this set has computed trajectories associated with it. To explore them, click on Explore trajectories. The GUI for the state-space exploration of trajectories is presented here.