XSTAMINA GUI (STAMINA/STORM Only)

The XStamina GUI requires a few more dependencies as opposed to the CLI version of STAMINA/STORM. In addition to the dependencies required for STAMINA/STORM, the following packages are required for XStamina:

sudo apt install libqt5-dev libkf5xmlgui-dev libkf5textwidgets-dev libkf5kio-dev libkf5texteditor-dev qtbase5-dev qtdeclarative5-dev libqt5svg5-dev libkf5i18n-dev libkf5coreaddons-dev extra-cmake-modules

For Arch/Manjaro distributions:

sudo pacman -S kde-sdk-meta

(Click to expand)

1. Toolbar and menubar
2. Model information tree (only shows information if the model is built)
3. Model editing window
4. Quick model information
5. Tab-bar: gives acces to the model editor, properties editor, results viewer and log window.

Using xSTAMINA

Editing

Model files, in the PRISM language, are edited in the Model Editor tab. An autocomplete is provided which contains PRISM keywords, module and variable names, constants, and other useful model information. This autocomplete is updated when the model is parsed (i.e., the model tree is rebuilt). This can only happen when the model has no syntax errors.

Property files are similarly edited in the Properties Editor tab.

Both editors provide the following syntax highlighting scheme (colors are editable):

• Keywords: any keyword in the PRISM language, by default highlighted in a deep blue. The following keywords are highligted and therefore cannot be used as identifiers:

A, clock, const, ctmc, C, double, dtmc, E, endinit, endinvariant, endmodule, endobservables, endrewards, endsystem, false, formula, filter, func, F, global, G, init, invariant, I, label, max, mdp, min, module, X, nondeterministic, observable, observables, of, Pmax, Pmin, P, pomdp, popta, probabilistic, prob, pta, rate, rewards, Rmax, Rmin, R, S, stochastic, system, true, U, W

(see https://www.prismmodelchecker.org/manual/ThePRISMLanguage/ModulesAndVariables)

• Comments: Single-line comments, which start with //, or multi-line comments, which begin with /* and end with */. Generally a muted grey.


• Numerics: PRISM by default does not allow floating point variables (only natural numbers), but does allow floating point values in constant expressions. Both will highlight in red by default.


• Datatypes: Any datatype supported by PRISM, specifically int, double, or bool. Additionally, formula, invariant, and label are also highlighted by this.


• Functions: Anything which looks like an invocation of a function, namely ending with (.*).


• Strings: PRISM only supports double-quote separated strings, so "foo" is valid, but 'foo' is not.


• Constants: Constants may be defined by any identifier, but by convention, they are in all caps, so xSTAMINA highlights anything in UPPER_SNAKE_CASE as a constant.

By default, the editor uses tabs, and has a tab width of 4 characters. This, the typeface of the main editor, and the colors used in syntax highlighting can be edited in the General tab of the Edit → Preferences dialog, shown below. Colors and font size and typeface are stored in a preferences file

(Click to expand)

Both the model and properties file can be edited using a find and replace editor, accessible via Ctl+F or Ctl+R for find and replace respectively.

(Click to expand)

(Click to expand)

Text size can be changed via Ctl++ and Ctl+-.

Model Checking

Parameters such as κ, r_κ, and w can be found in the preferences window. These are not saved in a configuration file and can be changed before each model checking. All properties in the property file can be checked via Ctl+Shift+Return, or the Build Model and Check Properties button on the Model Editor tab.

Keyboard Shortcuts

The following keyboard shortcuts are available in the GUI:

File Shortcuts

• Ctl+N: Creates a new model file
• Ctl+Shift+N: Creates a new properties file
• Ctl+O: Opens a model or properties file
• Ctl+S: Saves the active file (model or properties) to the current filename
• Ctl+Shift+S: Saves the active file (model or properties) as a new filename
• Ctl+Shift+I: Imports SBML (not yet implemented)
• Ctl+Shift+E: Exports model to an explicit format

Editing Shortcuts

• Ctl+C, Ctl+V, Ctl+X: Copy, Paste, and Cut text
• Ctl+Alt+M: Inserts the skeleton code for a PRISM module
• Ctl+Alt+V: Inserts the skeleton code for a PRISM variable
• Alt+F: Inserts the skeleton code for a PRISM formula
• Alt+L: Inserts the skeleton code for a PRISM label
• Ctl+Alt+F: Inserts a skeleton for a global CSL or PCTL property
• Ctl+Alt+Shift+U: Inserts a skeleton for an until CSL or PCTL property
• Alt+Shift+E: Inserts a skeleton for an eventually CSL or PCTL property
• Alt+Shift+S: Inserts a skeleton for a steady state CSL or PCTL query
• Ctl+F, Ctl+R: Find or find and replace text
• Ctl+Z, Ctl+Shift+Z: Undo and Redo
• Ctl+Tab, Ctl+Shift+Tab: Increase and decrease indent
• Ctl+/, Ctl+Shift+/: Toggle and untoggle comment
• Ctl+Shift+Space: Trims whitespace
• Ctl+Alt+U, Ctl+Shift+U, Ctl+U: Set text as Title Case, lower case, or ALL CAPS respectively
• Alt+Shift+P: Show preferences dialog

Viewing and Visualization Shortcuts

• Ctl+M: Shows the model editor
• Ctl+Shift+P: Shows the properties editor
• Ctl+Shift+R: Shows the results editor
• Ctl++: Zooms in on the editor
• Ctl+-: Zooms out on the editor

Other Keyboard Shortcuts

• Ctl+Shift+B: Builds model and checks properties
• Ctl+Enter: Checks all properties with built model
• Ctl+Shift+Enter: Checks current property with built model