Commit 358899e3 authored by FAGES Francois's avatar FAGES Francois
Browse files

nusmv_all_then_some TD8 TD9

parent b4d33084
% Transmembrane inputs
MA(k25) for glucoseext => glucose.
MA(k26) for acetoneext => acetone.
% Glucose pathway to NADH
MA(k19) for G_1DH + NAD => Cia1.
MA(k20) for Cia1 => G_1DH + NAD.
MA(k21) for Cia1 + glucose => Cib1.
MA(k22) for Cib1 => Cia1 + glucose.
MA(k23) for Cib1 => Cfa1 + NADH.
MA(k24) for Cfa1 => G_1DH + gluconolacrone.
% Acetone pathway to Resorufin by consuming NADH
MA(k13) for ADH + NADH => Cia2.
MA(k14) for Cia2 => ADH + NADH.
MA(k15) for Cia2 + acetone => Cib2.
MA(k16) for Cib2 => Cia2 + acetone.
MA(k17) for Cib2 => Cfa2 + NAD.
MA(k18) for Cfa2 => ADH + isopropanol.
MA(k1) for HRP + H_2O_2 => Cia5.
MA(k2) for Cia5 => HRP + H_2O_2.
MA(k3) for Cia5 + resazurin => Cib5.
MA(k4) for Cib5 => Cia5 + resazurin.
MA(k5) for Cib5 => HRP + resorufin.
MA(k6) for HRP2 + NADH => Cf4.
MA(k7) for Cf4 => HRP2 + NADH.
MA(k8) for Cf4 => HRP2 + NADN.
MA(k9) for AO + isopropanol => Cf3.
MA(k10) for Cf3 => AO + isopropanol.
MA(k11) for Cf3 => Cio3 + H_2O_2.
MA(k12) for Cio3 => AO + HRP2.
% kinetic parameters
parameter(k1= 1.15157e-5).
parameter(k2=24).
parameter(k3=7.77313e-006).
......@@ -22,85 +55,23 @@ parameter(k21=9.71641e-009).
parameter(k22=20).
parameter(k23=200).
parameter(k24=400).
parameter(k25=5e-3).
parameter(k26=1e-2).
% Inputs
MA(k26) for acetoneext => acetone.
MA(k25) for glucoseext => glucose.
% Output 2: resorufin
MA(k1) for HRP + H_2O_2 => Cia5.
MA(k2) for Cia5 => HRP + H_2O_2.
MA(k3) for Cia5 + resazurin => Cib5.
MA(k4) for Cib5 => Cia5 + resazurin.
MA(k5) for Cib5 => HRP + resorufin.
% Output 1: NADH
MA(k6) for HRP2 + NADH => Cf4.
MA(k7) for Cf4 => HRP2 + NADH.
MA(k8) for Cf4 => HRP2 + NADN.
MA(k9) for AO + isopropanol => Cf3.
MA(k10) for Cf3 => AO + isopropanol.
MA(k11) for Cf3 => Cio3 + H_2O_2.
MA(k12) for Cio3 => AO + HRP2.
MA(k13) for ADH + NADH => Cia2.
MA(k14) for Cia2 => ADH + NADH.
MA(k15) for Cia2 + acetone => Cib2.
MA(k16) for Cib2 => Cia2 + acetone.
MA(k17) for Cib2 => Cfa2 + NAD.
MA(k18) for Cfa2 => ADH + isopropanol.
MA(k19) for G_1DH + NAD => Cia1.
MA(k20) for Cia1 => G_1DH + NAD.
MA(k21) for Cia1 + glucose => Cib1.
MA(k22) for Cib1 => Cia1 + glucose.
MA(k23) for Cib1 => Cfa1 + NADH.
MA(k24) for Cfa1 => G_1DH + gluconolacrone.
present(glucose, 0).
present(gluconolacrone, 0).
% initial conditions
present(G_1DH, c).
present(acetone, 0).
present(isopropanol, 0).
present(ADH, a).
present(NADH, 31533).
present(NAD, 1576691971).
present(resazurin, 315338394).
present(resorufin, 0).
present(HRP, 6565).
present(H_2O_2, 0).
present(AO, b).
present(NADN, 0).
present(HRP2, 6565).
present(Cfa5, 0).
present(Cia5, 0).
present(Cib5, 0).
present(Cf4, 0).
present(Cf3, 0).
present(Cio3, 0).
present(Cfa2, 0).
present(Cia2, 0).
present(Cib2, 0).
present(Cfa1, 0).
present(Cia1, 0).
parameter(b=175012).
parameter(c=2232595).
parameter(a=92078816).
present(glucoseext, d).
present(acetoneext, e).
parameter(d=0, e=0).
parameter(a=92078816, b=175012, c=2232595).
parameter(d=3e8, e=3e8).
%option(show_molecules:{NADN, acetone, glucose, resorufin, NADH}).
% time horizon
option(time:3600).
......@@ -41,10 +41,10 @@ nusmv_initial_states(all).
nusmv_initial_states(some).
nusmv_initial_states(all_or_some).
nusmv_initial_states(all_then_some).
:- doc('
\\emphright{The default value is \\texttt{all}. The value
\\texttt{all_or_some} tries for all initial states, and if that fails, for
\\texttt{all_then_some} tries for all initial states, and if that fails, for
some}').
:- initial(option(nusmv_initial_states: all)).
......@@ -504,7 +504,7 @@ enumerate_all_molecules(Molecules) :-
check_ctl_impl(Query, all_or_some, NusmvCX, BoolSem, Result) :-
check_ctl_impl(Query, all_then_some, NusmvCX, BoolSem, Result) :-
check_ctl_impl(Query, all, NusmvCX, BoolSem, AllResult),
(
AllResult == 'true'
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment