Commit f9a5eba5 authored by Sylvain Soliman's avatar Sylvain Soliman

v4.4.9

parents b3940f4f cf17eecb
......@@ -8,7 +8,7 @@
about/0
]).
version('4.4.8').
version('4.4.9').
copyright(
'Copyright (C) 2003-2020 Inria, EPI Lifeware, Saclay-Île de France, France'
......
FROM registry.gitlab.inria.fr/lifeware/biocham:v4.4.8
FROM registry.gitlab.inria.fr/lifeware/biocham:v4.4.9
{
"name": "gui",
"version": "4.4.8",
"version": "4.4.9",
"description": "biocham gui in jupyter notebook",
"main": "src/index.js",
"scripts": {
......
"""Example magic"""
__version__ = '4.4.8'
__version__ = '4.4.9'
......@@ -90,30 +90,23 @@ ctl(E -> F) :-
ctl(reachable(E)) :-
ctl(E).
:- doc('\\emphright{reachable(f) is a shorthand for EF(f)}').
ctl(must_reach(E)) :-
ctl(E).
:- doc('\\emphright{mustreach(f) is a shorthand for AF(f)}').
ctl(steady(E)) :-
ctl(E).
:- doc('\\emphright{steady(f) is a shorthand for EG(f)}').
ctl(stable(E)) :-
ctl(E).
:- doc('\\emphright{stable(f) is a shorthand for AG(f)}').
ctl(checkpoint(E, F)) :-
ctl(E),
ctl(F).
:- doc('\\emphright{checkpoint(f, g) is a shorthand for not EU(not f, g)). Note that such a factual property does not imply any causality relationship from f to g.}').
ctl(checkpoint2(E, F)) :-
ctl(E),
ctl(F).
%:- doc('\\emphright{checkpoint2(f, g) is a shorthand for EF(not f)/\\\\EF(g)/\\\\checkpoint(f,g)}'). % good point for EF(g) not sure for EF(not f)
:- doc('\\emphright{checkpoint2(f, g) is a shorthand for EF(g)/\\\\checkpoint(f,g)}').
%ctl(predecessor_checkpoint(E, F)) :-
% ctl(E),
......@@ -122,23 +115,27 @@ ctl(checkpoint2(E, F)) :-
ctl(oscil2(E)) :-
ctl(E).
:- doc('\\emphright{oscil2(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))) which is true if f has at least two peaks on one path}').
ctl(oscil3(E)) :-
ctl(E).
:- doc('\\emphright{oscil3(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))))) which is true if f has at least three peaks on one path}').
ctl(oscil(E)) :-
ctl(E).
:- doc('\\emphright{oscil(f) is a shorthand for oscil3(f) /\\\\ EG(EF(f) /\\\\ EF(not f)) which is a necessary (not sufficient) condition for infinite oscillations in CTL}').
ctl(current_spec).
ctl(E) :-
object(E).
:- doc('\\emphright{reachable(f) is a shorthand for EF(f)}').
:- doc('\\emphright{mustreach(f) is a shorthand for AF(f)}').
:- doc('\\emphright{steady(f) is a shorthand for EG(f)}').
:- doc('\\emphright{stable(f) is a shorthand for AG(f)}').
:- doc('\\emphright{checkpoint(f, g) is a shorthand for not EU(not f, g)). Note that such a factual property does not imply any causality relationship from f to g.}').
:- doc('\\emphright{checkpoint2(f, g) is a shorthand for not(g)/\\\\ EF(g)/\\\\checkpoint(f,g)}').
:- doc('\\emphright{oscil2(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))) which is true if f has at least two peaks on one path}').
:- doc('\\emphright{oscil3(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))))) which is true if f has at least three peaks on one path}').
:- doc('\\emphright{oscil(f) is a shorthand for oscil3(f) /\\\\ EG(EF(f) /\\\\ EF(not f)) which is a necessary (not sufficient) condition for infinite oscillations in CTL}').
......@@ -352,7 +349,7 @@ normalize_query(checkpoint(A, B), QQ, L1, L2) :-
normalize_query(checkpoint2(A, B), QQ, L1, L2) :-
!,
normalize_query('EF'(B) /\ not('EU'(not(A), B)), QQ, L1, L2).
normalize_query(not(B) /\ 'EF'(B) /\ not('EU'(not(A), B)), QQ, L1, L2).
%normalize_query(predecessor_checkpoint(A, B), QQ, L1, L2) :-
% !,
......
a1*E1*KKK for KKK+E1=>E1_KKK.
b1*E1_KKK for E1_KKK=>KKK+E1.
c1*E1_KKK for E1_KKK=>E1+KKKp.
a2*E2*KKKp for KKKp+E2=>E2_KKKp.
b2*E2_KKKp for E2_KKKp=>KKKp+E2.
c2*E2_KKKp for E2_KKKp=>E2+KKK.
a3*KK*KKKp for KK+KKKp=>KKKp_KK.
b3*KKKp_KK for KKKp_KK=>KK+KKKp.
c3*KKKp_KK for KKKp_KK=>KKp+KKKp.
a4*KKp*KKPase for KKp+KKPase=>KKPase_KKp.
b4*KKPase_KKp for KKPase_KKp=>KKp+KKPase.
c4*KKPase_KKp for KKPase_KKp=>KK+KKPase.
a5*KKp*KKKp for KKp+KKKp=>KKKp_KKp.
b5*KKKp_KKp for KKKp_KKp=>KKp+KKKp.
c5*KKKp_KKp for KKKp_KKp=>KKpp+KKKp.
a6*KKpp*KKPase for KKpp+KKPase=>KKPase_KKpp.
b6*KKPase_KKpp for KKPase_KKpp=>KKpp+KKPase.
c6*KKPase_KKpp for KKPase_KKpp=>KKp+KKPase.
a7*K*KKpp for K+KKpp=>KKpp_K.
b7*KKpp_K for KKpp_K=>K+KKpp.
c7*KKpp_K for KKpp_K=>Kp+KKpp.
a8*Kp*KPase for Kp+KPase=>KPase_Kp.
b8*KPase_Kp for KPase_Kp=>Kp+KPase.
c8*KPase_Kp for KPase_Kp=>K+KPase.
a9*Kp*KKpp for Kp+KKpp=>KKpp_Kp.
b9*KKpp_Kp for KKpp_Kp=>Kp+KKpp.
c9*KKpp_Kp for KKpp_Kp=>KKpp+Kpp.
a10*Kpp*KPase for Kpp+KPase=>KPase_Kpp.
b10*KPase_Kpp for KPase_Kpp=>Kpp+KPase.
c10*KPase_Kpp for KPase_Kpp=>Kp+KPase.
present(E1,3.0e-5).
present(KKK,0.003).
present(E2,0.0003).
present(KK,1.2).
present(KKPase,0.0003).
present(K,1.2).
present(KPase,0.12).
parameter(
compartment = 4.0e-12,
Kppnorm_max = 0.900049,
a1 = 1000.0,
b1 = 150.0,
c1 = 150.0,
a2 = 1000.0,
b2 = 150.0,
c2 = 150.0,
a3 = 1000.0,
b3 = 150.0,
c3 = 150.0,
a4 = 1000.0,
b4 = 150.0,
c4 = 150.0,
a5 = 1000.0,
b5 = 150.0,
c5 = 150.0,
a6 = 1000.0,
b6 = 150.0,
c6 = 150.0,
a7 = 1000.0,
b7 = 150.0,
c7 = 150.0,
a8 = 1000.0,
b8 = 150.0,
c8 = 150.0,
a9 = 1000.0,
b9 = 150.0,
c9 = 150.0,
a10 = 1000.0,
b10 = 150.0,
c10 = 150.0
).
function(
ratioKpp = Kpp/(Kpp+Kp+K+KKpp_K+KKpp_Kp+KPase_Kpp+KPase_Kp),
ratioKKpp = KKpp/(KKpp+KKp+KK+KKpp_K+KKpp_Kp+KKKp_KK+KKKp_KKp+KKPase_KKpp+KKPase_KKp),
ratioKKKp = KKKp/(KKK+KKKp+KKKp_KK+KKKp_KKp)
).
#include <stdlib.h>
#include <cstddef>
#include <random>
#include <chrono>
#include <ppl.hh>
#include "ppl_validity_domain.hh"
#include "gsl_solver.hh"
......@@ -71,7 +72,11 @@ main(int argc, char *argv[])
{
double population[DIMENSION];
std::default_random_engine generator;
generator.seed(SEED);
if (SEED > 0) {
generator.seed(SEED);
} else {
generator.seed(std::chrono::system_clock::now().time_since_epoch().count());
}
std::normal_distribution<double> distribution[DIMENSION];
int i, j;
// https://en.wikipedia.org/wiki/Algorithms_for_calculating_variance
......
......@@ -19,8 +19,8 @@ No complex invariant found
<img src="plot-1.csv" alt="Simulation results">
<img src="plot-2.csv" alt="Simulation results">
<img src="plot-3.csv" alt="Simulation results">
[A-0,B-0]
[A-1,B-0]
present({}).
present({A}).
reachable(stable(A))
reachable(stable(not A))
reachable(stable(not B))
......@@ -31,7 +31,7 @@ AG(f)
EG(f)
EF(EG(s))
not EU(not x,y)
EF(y)/\not EU(not x,y)
not y/\EF(y)/\not EU(not x,y)
reachable(checkpoint2(not A,not B)) is true
reachable(checkpoint2(not B,not A)) is false
<img src="plot-4.csv" alt="Simulation results">
......@@ -89,7 +89,7 @@ m=0/\M=67383000
T>287.057
0.946074
<img src="plot-1.csv" alt="Simulation results">
T>109.48
T>88.2305
acetone_p*glucose_p for glucose_p+acetone_p=>resorufin_p+glucose_p+acetone_p.
acetone_n*glucose_n for glucose_n+acetone_n=>resorufin_p+glucose_n+acetone_n.
MA(1) for resorufin_p=>_.
......
......@@ -442,8 +442,15 @@ gather_initial_values(InitialValues) :-
(
between(0, VariableMax, VariableIndex),
variable(Molecule, VariableIndex),
%get_initial_state(Molecule, State),
get_ode_initial_state(Molecule, State),
(
% try first in the model in case Concentration is a parameter
get_initial_state(Molecule, present(Concentration))
->
State = present(Concentration)
;
% otherwise use the ODE system
get_ode_initial_state(Molecule, State)
),
(
State = present(Concentration)
->
......
......@@ -39,7 +39,7 @@ boolean_semantics(negative).
:- doc('\\emphright{The default value is \\texttt{negative}}').
:- initial(option(boolean_semantics: negative)).
:- doc('The negative Boolean semantics interpret reaction inhibitors with a negation in the condition. The positive Boolean semantics ignore reaction inhibitors.').
:- doc('\\emphright{The negative Boolean semantics interpret reaction inhibitors with a negation in the condition. The positive Boolean semantics ignore reaction inhibitors.}').
:- grammar(boolean_initial_states).
......@@ -58,23 +58,21 @@ boolean_initial_states(all_then_some).
:- grammar(boolean_state_display).
boolean_state_display(present).
:- doc('Display boolean states as a \\texttt{present} command. (default)').
boolean_state_display(table).
:- doc('Display boolean states as a TAB separated table of TRUE/FALSE values.').
boolean_state_display(vector).
:- doc('Display boolean states as association-lists with 0/1 values.').
:- doc('\\emphright{Display boolean states as a \\texttt{present} command. (default), or a TAB separated table of TRUE/FALSE values, or an association-list with 0/1 values.}').
:- initial(option(boolean_initial_states: all)).
:- doc('The formulae can be checked in all or some initial states.').
:- doc('\\emphright{CTL formulae can be checked in all or some initial states.}').
:- initial(option(boolean_trace: no)).
:- doc('Boolean traces can be provided for formulae, either provably true by a single trace in some initial state, or falsified by one counter example initial state (default value is no trace).').
:- doc('\\emphright{Display either a Boolean trace proving the formula in some initial state, or a counter example initial state falsifying the formula (default value is no trace).}').
:- initial(option(nusmv_topological_order: no)).
:- doc('Ordering of variables for the NuSMV model-checker.').
:- doc('\\emphright{Ordering of variables for the NuSMV model-checker.}').
:- initial(option(query: current_spec)).
......
......@@ -32,7 +32,7 @@
</head>
<body>
<h1>The Biochemical Abstract Machine BIOCHAM 4</h1>
<h1>version 4.4.8 April 2020</h1>
<h1>version 4.4.9 April 2020</h1>
<div class="authors">
<p>
......
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