Cadbiom GUI

This guide can help you start working with the Cadbiom GUI.


Overview of the Cadbiom Graphical User Interface. (1): Graph editor and its tabs; (2): Toolbar to design models; (3): Search properties and conduct discrete time simulations; (4): Explore nodes of the model (search/show/extract); (5): Show data about the item that is currently selected (model/node/transition).

Loading files

Currently, the following types of files are supported:

The models can be exported to the following formats:

  • Cadbiom file format (.bcx)
  • Cadlang file format (.cl)
  • Image (.png)

Exploring the models

The "Static analysis/Model information" menu provides detailed information on the model and its entities; for example, their cellular location, the number of boundaries, the number of isolated places, etc.

The widget at the bottom of the screen (5) displays according to the selected item:

  • global data on the loaded model (model name, number of entities, number of transitions)
  • the details of the nodes (names) and transitions (names, clock, condition) selected;
  • view the nodes involved in the condition of the selected transition.

The metadata of the element can be consulted in JSON format by clicking on the button "Metadata".

Example of information showed for a transition.

Editing the models

The "Model nodes (display and search)" widget (4) allows to:

  • search, filter and display nodes based on their names (a regular expression of type PERL can be used);
  • extract a complete sub-model containing the selected nodes and transitions as well as the nodes involved in the conditions of these transitions;
  • deselect the nodes.

Copy/paste the nodes is allowed at any time by right clicking in the graph editor, within the current model or to other open models;

Example of nodes selected and then highlighted on the graph editor.

Design of models

The top toolbar (2) provides easy access to the types of objects that can be created in a Cadbiom model:

  • SimpleNode: add a new simple node (most nodes of a model);
  • PermNode: add a permanent node (always activated node);
  • StartNode: add a start node (without incoming transition, used to unlock cycles (Strongly Connected Components));
  • TrapNode: add a trap node (without outgoing transition);
  • Transition: add a transition. Draw an arrow between a node and another.

Simulation of trajectories

Discrete time simulation can be performed on the model.

The simulation window can be reached from the main GUI via the "Simulation" button (3), and from a similar button in the solutions window that is displayed after the property search. The first way reloads previously saved results, while the second applies to a chosen solution.

The simulation window is mainly composed of a "step" button allowing to synchronize the graph editor with a step of the considered solution. By clicking on "step" in an iterative way you visualize the trajectory taken by the software to satisfy the desired property.

Example of the checker window; Property C is searched with the place A as a start property. This place is not a boundary so we artificially activate it that way.

Example of simulation step by step on the graph editor.

Keyboard shortcuts

  • F1: Add InputNode
  • F2: Add SimpleNode
  • F3: Add PermNode
  • F4: Add StartNode
  • F5: Add TrapNode
  • F6: Transition
  • F7: View and edit model constraints
  • F8: Model checking and property search
  • F9: Simulation
  • Ctrl+O: Open a Cadbiom model file
  • Ctrl+N: Create a new model
  • Ctrl+W: Close the current tab
  • Ctrl+Q: Quit Cadbiom
  • Escape: Close a subwindow