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.

Model loading

We load a simple model of Phage Lambda using GINsim, http://ginsim.org/node/47:

In [1]:
import ginsim
In [2]:
lrg = ginsim.load("http://ginsim.org/sites/default/files/phageLambda4.zginml")

Downloading 'http://ginsim.org/sites/default/files/phageLambda4.zginml' to 'gen/colomotoeddv2mxsphageLambda4.zginml'

Properties to be verified

We use the colomoto python module which offers a generic interface for declaring temporal properties using either LTL or CTL.

In [3]:
from colomoto.temporal_logics import *
In [4]:
lysogenic = AG(S(CI=2))        # CI is permanently active
lytic = AG(EF(S(CI=0,Cro=2)) & EF(S(CI=0,Cro=3)))  # Cro permanently oscillates between levels 2 and 3
attractors = AG(EF(lysogenic | lytic))   # all the attractors are either lysogenic or lytic
initial_state = S(CI=0,CII=0,Cro=0,N=0)
In [5]:
properties = {
    "s0_lysogenic": If(initial_state, EF(lysogenic)), # lysogenic state is reachable from initial state  
    "s0_lytic": If(initial_state, EF(lytic)),  # lytic state is reachable from initial state
    "attractors": attractors, # all attractors are either lyso or lytic
}

Verification using GINsim export to NuSMV

In [6]:
smv_ginsim = ginsim.to_nusmv(lrg)
smv_ginsim.add_ctls(properties)
smv_ginsim.alltrue()
Out[6]:
True

Verification using Pint export to NuSMV

In [7]:
import pypint

You are using Pint version 2017-12-19 and pypint 1.3.94

We first convert to GINsim model (multi-valued network) to Pint (automata network)

In [8]:
an = ginsim.to_pint(lrg)

Source file is in Automata Network (an) format

In [9]:
smv_pint = pypint.to_nusmv(an)
smv_pint.add_ctls(properties)
smv_pint.alltrue()
Out[9]:
True
In [ ]: