This guide can help you start working with the Cadbiom GUI.
Currently, the following types of files are supported:
- Cadbiom file format (.bcx) (see Models),
- Import BioPAX format from a RDF triplestore (see Creation of a Cadbiom model from a BioPAX endpoint),
- PID file format (.xml),
- Cadlang file format (.cl).
The models can be exported to the following formats:
- Cadbiom file format (.bcx)
- Cadlang file format (.cl)
- Image (.png)
Exploring the models¶
"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
Editing the models¶
"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;
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.
Model checking/property search¶
"Check" (3) button opens the checker window.
The checker is aimed to find answers to some queries. It is oriented to signal propagation problems.
Two type of properties can be searched:
- reachability: the property P will happen
- non reachability: P will never happen (¬P)
A property is written as a sequence of place names, linked together by logical operators (and, or, not); it is always checked on a finite horizon (number of steps).
An answer to a query, also called a solution, is a set of boundaries that must be activated to satisfy the property during a scenario. Places that are not in the solution are unactivated at initialization.
Most of time, a solution contains essential places but also noisy places. These places correspond to trajectory fragments without relation with the property. Minimal Activation Conditions (MAC) focus on necessary and sufficient places. Indeed, a MAC is a solution such that no subset of places can lead to the satisfiability of the property.
Generally speaking, obtaining solutions implies obtaining MACs.
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.
F1: Add InputNode
F2: Add SimpleNode
F3: Add PermNode
F4: Add StartNode
F5: Add TrapNode
F7: View and edit model constraints
F8: Model checking and property search
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