{
"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": [
{
"data": {
"text/html": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"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": [
""
]
},
"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": [
""
]
},
"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": [
""
]
},
"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.6.4"
}
},
"nbformat": 4,
"nbformat_minor": 2
}