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.

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")


### 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.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)

True