{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This notebooks shows a basic example of using NuSMV to analyse dynamical properties on a GINsim model.\n",
    "\n",
    "## Model\n",
    "\n",
    "We use GINsim to load a simple model of phage lambda differentiation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import ginsim"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Downloading 'http://ginsim.org/sites/default/files/phageLambda4.zginml'"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "lrg = ginsim.load(\"http://ginsim.org/sites/default/files/phageLambda4.zginml\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Dynamical properties\n",
    "\n",
    "The phage lambda model exhibits the differentiation process between lytic and lysogenic states.\n",
    "\n",
    "In this notebook, we will CTL to express properties on trajectories related to the reachability of lytic and lysogenic attractors.\n",
    "\n",
    "The Python module `colomoto.temporal_logics` provides a programmatic way to specify CTL and LTL properties"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from colomoto.temporal_logics import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Properties on states are specified using the `S` operator.\n",
    "The following property characterize the initial state when all the nodes are inactive:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "initial_state = S(CI=0,CII=0,Cro=0,N=0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The lysogenic state is characterized by the node `CI` being permanently strongly expressed, which is modeled by `CI=2`. The following CTL property express that from the given state, all the reachable states (`AG`) satisfy `CI=2`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "lysogenic = AG(S(CI=2))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The lytic state is characterized by the node `CI` being inactive (value 0), and `Cro` oscillating between activity levels 2 and 3. This is stated by the following CTL property:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "lytic = AG(S(CI=0) & (S(Cro=2) | S(Cro=3)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The following CTL properties is true if all the reachable attractors are either lysogenic or lytic states:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "attractors = AG(EF(lysogenic | lytic))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Setting up NuSMV\n",
    "\n",
    "NuSMV is a symbolic model checker which checks if the provided model verifies a given set of CTL/LTL properties.\n",
    "\n",
    "GINsim provides a translation of Boolean and multivalued networks into NuSMV models:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "smv = ginsim.to_nusmv(lrg)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here, `smv` is a Python object representing the NuSMV model.\n",
    "CTL/LTL specification can be added using the method `add_ctl` and `add_ltl`, respectively.\n",
    "For convenience, a label can be given to a property:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "smv.add_ctl(attractors, name=\"global_attractors\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Properties can also be added by bulk, providing a Python dictionnary specifying the properties.\n",
    "In the following cell, we specify two properties: one verifying that, from the initial state, there exists a trajectory leading to a stable lysogenic state, and another one verifying that, from the initial state, there exists a trajectory leading to a stable lytic state."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "specs = {\n",
    "    \"reach_lyso\": If(initial_state, EF(lysogenic)),\n",
    "    \"reach_lytic\": If(initial_state, EF(lytic))\n",
    "}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "smv.add_ctls(specs)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Invoking NuSMV\n",
    "\n",
    "The method `verify` will execute NuSMV and returns the verification result for each property:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'global_attractors': True, 'reach_lyso': True, 'reach_lytic': True}"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv.verify()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One can also use the method `alltrue` to check if all the given properties are true:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv.alltrue()"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}