{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook, we show how the verification of qualitative regulatory networks can be done with different methods, which should give equivalent results, using *GINsim* and *Pint*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Model loading\n",
    "\n",
    "We load a simple model of Phage Lambda using GINsim, http://ginsim.org/node/47:"
   ]
  },
  {
   "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' to 'gen/colomotoeddv2mxsphageLambda4.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": [
    "### Properties to be verified\n",
    "\n",
    "We use the `colomoto` python module which offers a generic interface for declaring temporal properties using either LTL or CTL."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from colomoto.temporal_logics import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "lysogenic = AG(S(CI=2))        # CI is permanently active\n",
    "lytic = AG(EF(S(CI=0,Cro=2)) & EF(S(CI=0,Cro=3)))  # Cro permanently oscillates between levels 2 and 3\n",
    "attractors = AG(EF(lysogenic | lytic))   # all the attractors are either lysogenic or lytic\n",
    "initial_state = S(CI=0,CII=0,Cro=0,N=0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "properties = {\n",
    "    \"s0_lysogenic\": If(initial_state, EF(lysogenic)), # lysogenic state is reachable from initial state  \n",
    "    \"s0_lytic\": If(initial_state, EF(lytic)),  # lytic state is reachable from initial state\n",
    "    \"attractors\": attractors, # all attractors are either lyso or lytic\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Verification using GINsim export to NuSMV"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv_ginsim = ginsim.to_nusmv(lrg)\n",
    "smv_ginsim.add_ctls(properties)\n",
    "smv_ginsim.alltrue()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Verification using Pint export to NuSMV"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "You are using Pint version 2017-12-19 and pypint 1.3.94"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import pypint"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We first convert to GINsim model (multi-valued network) to Pint (automata network)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Source file is in Automata Network (an) format"
      ],
      "text/plain": [
       "<IPython.core.display.Markdown object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "an = ginsim.to_pint(lrg)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "smv_pint = pypint.to_nusmv(an)\n",
    "smv_pint.add_ctls(properties)\n",
    "smv_pint.alltrue()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "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.8.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}