Cadbiom GUI =========== This guide can help you start working with the Cadbiom GUI. Overview -------- .. figure:: _static/demo_gui/overview.png :scale: 85 % :alt: :align: center 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: - Cadbiom file format (.bcx) (see :ref:`models`), - Import BioPAX format from a RDF triplestore (see :ref:`create_from_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 -------------------- .. Le menu "Static analysis/Model information" procure des informations détaillées sur le modèle et ses entités; comme par exemple leur localisation cellulaire, le nombre de places frontières, le nombre de places isolées, etc. Le widget en bas de l'écran affiche selon l'élément sélectionné: - des chiffres globaux sur le modèle chargé (nom du modèle, nombre d'entités, nombre de transitions) - le détail des noeuds (noms) et transitions (noms, horloge, condition) sélectionnés; - visualiser les noeuds impliqués dans la condition de la transition sélectionnée. Les méta données de l'élément peuvent être consultées au format JSON en cliquant sur le bouton "Metadata". 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"``. .. figure:: _static/demo_gui/transition_info.png :scale: 85 % :alt: :align: center Example of information showed for a transition. Editing the models ------------------ .. Le widget intitulé "Model nodes (display and search)" permet de : - rechercher, filtrer et afficher des noeuds en se basant sur leur noms (une expression régulière de type PERL peut être utilisée); - extraire un sous-modèles complet contenant les noeuds et transitions sélectionnés ainsi que les noeuds impliqués dans les conditions de ces transitions; - déselectionner les noeuds. Copier/coller les noeuds est autorisé à tout moment grâce à un clic droit dans le graph editor, au sein du modèle courant ou vers d'autres modèles ouverts; 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; .. figure:: _static/demo_gui/show_nodes.png :scale: 85 % :alt: :align: center Example of nodes selected and then highlighted on the graph editor. Design of models ---------------- .. La barre d'outils supérieur permet un accès facile aux types d'objets pouvant être créés dans un modèle Cadbiom. 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 ------------------------------ The ``"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. .. figure:: _static/demo_gui/property_check_window.png :scale: 85 % :alt: :align: center 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. .. figure:: _static/demo_gui/solutions_window.png :scale: 85 % :alt: :align: center Example of the solutions window; Each line is a set of boundaries that satisfy the searched property. Each solution can be simulated on the graph editor. 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. .. figure:: _static/demo_gui/simulator_window.png :scale: 85 % :alt: :align: center 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. .. figure:: _static/demo_gui/simulation.gif :scale: 85 % :alt: :align: center 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