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:
import ginsim
lrg = ginsim.load("http://ginsim.org/sites/default/files/phageLambda4.zginml")
Downloading 'http://ginsim.org/sites/default/files/phageLambda4.zginml' to 'gen/colomotoeddv2mxsphageLambda4.zginml'
We use the colomoto
python module which offers a generic interface for declaring temporal properties using either LTL or CTL.
from colomoto.temporal_logics import *
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)
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
}
smv_ginsim = ginsim.to_nusmv(lrg)
smv_ginsim.add_ctls(properties)
smv_ginsim.alltrue()
True
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)
an = ginsim.to_pint(lrg)
Source file is in Automata Network (an) format
smv_pint = pypint.to_nusmv(an)
smv_pint.add_ctls(properties)
smv_pint.alltrue()
True