********
Tutorial
********

Overview
========

Studying the behaviour of dynamic biological systems is made by model checking;
this method generates scenarios based on the constraints defined in a model.
A scenario or a trajectory (i.e. a sequence of states of biomolecules),
can be described with the help of propositional logic formulas.

A SAT solver allows us to analyse constraints from models with **several thousands of places and transitions**.
It is used to either give a satisfiability answer, or generate a set of initial activation states
for the boundaries (frontier places) of the system.
Cadbiom uses the free and open source CryptoMinisat solver [CryptoMiniSat]_ which happens to be a winner
of the 2010 and 2015 SAT Race competitions [SAT-Race2015]_.

Cadbiom has benefited from a major refactoring over the years. Some particularly costly functions in calculation time
have been written in C. An architecture implementing multiprocessing technology has been integrated into
the command line module to take advantage of the computing power of modern computers and distributed
computing infrastructures.
Moreover, an increased computing capacity has been achieved thanks to last versions of CryptoMinisat.

We can thus compare the performance of the old Cadbiom versions with the new one in terms
of the number of solutions obtained per unit of time.

..
    import pandas as pd
    df = pd.DataFrame({
        "Years of development and versions": ["2016\nalpha", "2017\nv0.1.7", "2019\nv0.2", "2020 1st quarter\n(dev branch)"],
        "Solutions per hour": [0.33, 48, 180, 633],
        "Max memory": [2, 1.8, 1.5, 1.1],
    })

    ax = df.plot.bar(
        x="Years of development and versions",
        logy=True,
        ylim=(0.22, 1000), fontsize=8,
        rot=0, secondary_y="Max memory",
    )
    ax.right_ax.set_ylim(0, 3)
    # ax.set_ylim((0.22, 1000))
    # ax.set_yscale('log')
    ax.set_ylabel('Solutions/h')
    ax.right_ax.set_ylabel('Memory consumption (Go)')

    def annotate_patches(axe):
        for p in axe.patches:
            axe.annotate(
                round(p.get_height(), 2),
                (p.get_x() + p.get_width()/2., p.get_height()),
                ha='center', va='center', xytext=(0, 10), textcoords='offset points',
                fontsize=8,
            )

    annotate_patches(ax)
    annotate_patches(ax.right_ax)

    ax.get_figure().savefig("perf_overview.svg")


.. figure:: _static/misc/perf_overview.svg
   :scale: 85 %
   :alt:
   :align: center

   Improved performance over the development years (log scale for y axis).
   Tested on monoprocess usage on the following hardware configuration:
   CPU: i7-3630QM, 3.2GHz;
   Memory: 12 Go DDR3-RAM PC3-12800.
   Query: `SRP9` molecule; Model: `Whole NCI-PID database translated into CADBIOM formalism(and).bcx`.


The modules
===========

While the graphical interface of Cadbiom is the easiest way to explore small models,
the command line is a must-have for larger models with several hundred of entities.

The GUI provides a graph editor to build and explore models;
it purposes a simple query interface to analyse the dynamics of a model (i.e. search properties and
conduct discrete time simulations).

The command line module allows searching trajectories, and necessary and sufficient sets of boundaries
related to the states of the places of interest mentioned in a logical formula built by the user.
These sets are also called Minimal Activation Conditions.

Output files from Cadbiom can be difficult to exploit by hand
(See :ref:`cadbiom_file_format_spec`);
they contain the sequences of transitions necessary to satisfy a problem.
We have developed sub commands that allow to work with these files from the command line.

..
    Nous sommes ainsi capables de générer des graphes de trajectoires depuis les places frontières jusqu'aux entités d'intérêt.
    Ces graphes peuvent être ouverts dans des applications comme Cytoscape ou Gephi.
    Nous pouvons aussi comparer les trajectoires les unes avec les autres.
    Les modèles peuvent être requêtés afin de connaitre facilement leur contenu.


We are thus able to generate trajectory graphs from boundaries to entities of interest.
These graphs can be opened in applications such as Cytoscape or Gephi.
We can also compare trajectories with each other and generate matrices of occurrences of places and heatmaps.
We can work with the models to extract information and easily know their content.

Examples of uses are described in the next chapter.


Examples
========

.. toctree::
   :maxdepth: 2

   gui_package
   workflow_overview
   work_with_models.ipynb
   work_with_solutions.ipynb


.. [CryptoMiniSat] msoos. CryptoMiniSat 5.0.1 released — with MIT license | Wonderings of a SAT geek [Internet]. Available on: https://www.msoos.org/2016/09/cryptominisat-5-0-1-released-with-mit-license/

.. [SAT-Race2015] SAT-Race 2015 [Internet]. [cited dec 7 2017]. Available on: https://baldur.iti.kit.edu/sat-race-2015/index.php?cat=results