Commit e4ccb363 authored by dcoudrin's avatar dcoudrin
Browse files
parents 25890ab0 a9ed19f4
# Building Biocham on Windows 10
Biocham may be built on Windows 10 using the Windows Subsystem for Linux.
## Steps
First, install WSL as per the [instructions](https://docs.microsoft.com/en-us/windows/wsl/install-win10), then install the Ubuntu distribution from the Windows store.
Run Ubuntu and obtain the Biocham sources (e.g. through git)
Then, run `./install.sh` from the source directory to install the project's dependencies and build Biocham.
Follow the instructions given by the install script (e.g. `source ~/.profile` at the end to update the path).
## Running Biocham
As with linux, run `./biocham --notebook` for instance to open a Jupyter notebook that talks to a Biocham kernel.
## Notes
WSL is apparently available on recent releases of Windows Server, but is untested on our side.
......@@ -51,7 +51,8 @@ biocham: $(SWIPL) $(MODULES) toc.org $(CMAES_LIB) \
start" \
--toplevel=toplevel -c $(MODULES)
biocham_debug: $(SWIPL) $(MODULES) $(TEST_MODULES) toc.org Makefile
biocham_debug: $(SWIPL) $(MODULES) $(TEST_MODULES) toc.org \
library/gsl_solver.o Makefile
$(SWIPL) -q -o biocham_debug \
--goal="\
set_prolog_flag(verbose, normal), \
......@@ -135,7 +136,7 @@ web/biocham.zip: biocham-src-$(shell git rev-parse --short HEAD).zip
cp $< $@
web: web/biocham.zip web/index.html web/logo.png doc/index.html
-rsync -avz $^ lifeware:/nfs/web-epi/biocham4/
-rsync -avz $^ doc lifeware:/nfs/web-epi/biocham4/
ssh -t lifeware 'sudo chmod -R g+w /nfs/web-epi/biocham4/ && sudo chown -R www-data.lifeware /nfs/web-epi/biocham4/'
cabernet: web
......
......@@ -8,10 +8,10 @@
about/0
]).
version('4.1.0').
version('4.1.7').
copyright(
'Copyright (C) 2003-2017 Inria, EPI Lifeware, Saclay-Île de France, France'
'Copyright (C) 2003-2018 Inria, EPI Lifeware, Saclay-Île de France, France'
).
license('GNU GPL 2').
......
......@@ -103,7 +103,8 @@ option('', '--list-commands', [], []) :-
forall(
(
current_functor(Functor, Arity),
predicate_info(Functor/Arity, _ArgumentTypes, _, yes, _)
predicate_info(Functor/Arity, _ArgumentTypes, _, BiochamCommand, _),
member(BiochamCommand, [yes, variantargs])
),
(
% Pred =.. [Functor | ArgumentTypes],
......
......@@ -363,10 +363,10 @@ satisfaction_degree(Formula, Objective) :-
type(Objective, [variable_objective]),
option(foltl_magnitude, number, _Magnitude, 'order of magnitude for << and >> operators'),
doc('
computes a continuous satisfaction degree in the interval [0,+∞) for a
FOLTL(Rlin) constraint on the current trace. The degree is greater or
equal than 1 if the formula is satisfied. The greater the degree the more
robust the satisfaction of the formula.
computes a continuous satisfaction degree in the interval [0,+∞) for an
FOLTL(Rlin) property on the current trace with respect to some objective values for the free variables of the formula. The degree is greater or
equal than 1 if the formula is satisfied. The greater the degree the greater the margin in the satisfaction of the formula (i.e. formula satisfaction robustness).
This satisfaction degree is computed by (an approximation of) the distance of the objective point to the validity domain of the formula (if less than 1), or by its penetration depth (if greater than 1).
'),
satisfaction_degree(Formula, Objective, Degree),
format('~f\n', [Degree]).
......
......@@ -114,7 +114,7 @@ else
else
if [[ "$conda_arch" == "Linux" ]]
then
sudo apt-get install python3-pip
sudo apt-get -qy install python3-pip
pip3 install -U jupyter
else
# Note that miniconda is available through brew cask, but to avoid adding
......
%% Cell type:markdown id: tags:
# ADVANCES IN SYSTEMS AND SYNTHETIC BIOLOGY
## Modelling Complex Biological Systems in the Context of Genomics
## Thematic Research School
https://assb.lri.fr 20 March 2018
# Workshop on the BIOCHAM modeling environment
François Fages and Sylvain Soliman, Inria Saclay Ile de France,
[ASSB BIOCHAM workshop](https://assb.lri.fr/en/Abstracts/BIOCHAM.html)
%% Cell type:markdown id: tags:
# Minimal mitotic oscillator
after *[Albert Goldbeter 1991 PNAS](https://doi.org/10.1073/pnas.88.20.9107)*
<img src="oscillator.png" width=300>
%% Cell type:code id: tags:
```
load(oscillator.bc).
```
%% Cell type:code id: tags:
```
list_model.
```
%% Cell type:code id: tags:
```
draw_reactions.
```
%% Cell type:markdown id: tags:
**Question:** _Do you think this system can oscillate? Does it have a_ **negative feedback loop**?
%% Cell type:code id: tags:
```
draw_influences.
```
%% Cell type:markdown id: tags:
**Question:** _Can you find which species are (mass-)conserved in this system?_
%% Cell type:code id: tags:
```
search_conservations.
```
%% Cell type:markdown id: tags:
## Differential semantics
Ordinary differential equations (ODEs) on continuous molecular concentrations
%% Cell type:code id: tags:
```
list_ode.
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
plot(show:Cyclin, against:ProteaseP).
```
%% Cell type:markdown id: tags:
**Question:** _Can you find parameter values that increase or decrease Cyclin's period?_
%% Cell type:code id: tags:
```
%slider vi kd V2 K2
```
%% Cell type:markdown id: tags:
## Stochastic semantics
Continuous time Markov Chain (CTMC) on integer numbers of molecules (conversion factor 100 for concentration 1)
%% Cell type:code id: tags:
```
parameter(vi=0.025, kd=0.01, V2=1.5, K2=0.005).
```
%% Cell type:code id: tags:
```
numerical_simulation(method:ssa). plot.
```
%% Cell type:markdown id: tags:
## Boolean semantics
Non-deterministic asynchronous Boolean transition system on Boolean states of present/absent molecules
## Computation Tree Logic (CTL) for querying the Boolean transition paths.
Logical connectives: /\ (and), \/ (or), not (negation), -> (implication)
Path quantifiers: E (there exists a path), A (for all paths)
Time operators: F (finally at some time point), G (globally at all time points), U (until)
Example: reachable state EF(s), steady state EG(s), stable state AG(s), etc.
%% Cell type:code id: tags:
```
generate_ctl.
```
%% Cell type:code id: tags:
```
expand_ctl(reachable(s)).
```
%% Cell type:code id: tags:
```
expand_ctl(steady(s)).
```
%% Cell type:code id: tags:
```
expand_ctl(stable(s)).
```
%% Cell type:code id: tags:
```
expand_ctl(oscil(f)).
```
%% Cell type:markdown id: tags:
## Model reduction preserving CTL properties
Which reactions can be removed while preserving the (generated) CTL specification of the behavior ?
%% Cell type:code id: tags:
```
reduce_model.
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
load(oscillator.bc).
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:markdown id: tags:
## Linear Time Logic with Constraints over Reals FO-LTL(Rlin)
No path quantifier (single trace analysis)
Only temporal operators F, G, U, X (next)
Free variables over the reals
Linear constraints over real variables
Existential (exists) and universal (forall) quantifiers over real variables
%% Cell type:code id: tags:
```
validity_domain(amplitude(Cyclin,v)).
```
%% Cell type:code id: tags:
```
expand_ltl(amplitude(x,a)).
```
%% Cell type:code id: tags:
```
validity_domain(period(Cyclin,p)).
```
%% Cell type:code id: tags:
```
satisfaction_degree(period(Cyclin,p), [p->25]).
```
%% Cell type:code id: tags:
```
satisfaction_degree(period(Cyclin,p), [p->22]).
```
%% Cell type:markdown id: tags:
## Parameter search
%% Cell type:code id: tags:
```
seed(0). search_parameters(period(Cyclin,p), [0<=vi<=1, 0<=V2<=2], [p -> 22]).
```
%% Cell type:code id: tags:
```
list_parameters.
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
validity_domain(period(Cyclin,p)).
```
%% Cell type:markdown id: tags:
---
Let's now have a closer look at the amplitude of the _Cyclin_…
%% Cell type:code id: tags:
```
plot(show: Cyclin).
```
%% Cell type:code id: tags:
```
validity_domain(amplitude(Cyclin, amp)).
```
%% Cell type:markdown id: tags:
**Question:** _Does this formula capture the amplitude between peaks?_
_Using the_ `local_minimum(Species, min)` _and_ `local_maximum(Species, max)` _constructs, can you write a pattern to capture that?_
%% Cell type:code id: tags:
```
expand_ltl(local_minimum(x,m)).
```
%% Cell type:code id: tags:
```
ltl_pattern(peak_amplitude(Species, Amplitude) =
exists(min, exists(max, local_minimum(Species, min) /\ local_maximum(Species, max) /\ Amplitude <= max - min))).
```
%% Cell type:code id: tags:
```
validity_domain(peak_amplitude(Cyclin, amp)).
```
%% Cell type:code id: tags:
```
seed(0). search_parameters(peak_amplitude(Cyclin, amp), [0<=vi<=1, 0<=V2<=2], [amp -> 0.8]).
```
%% Cell type:code id: tags:
```
option(show: {Cyclin, Protease, Kinase}).
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
validity_domain(peak_amplitude(Cyclin, amp)).
```
%% Cell type:markdown id: tags:
## Robustness of the model w.r.t. an FO-LTL(Rlin) property and parameter perturbations
* Model robustness (mean satisfaction degree for normal distribution of the parameter values)
* Formula satisfaction robustness optimization (maximization of the penetration depth in the validity domain)
%% Cell type:code id: tags:
```
robustness(peak_amplitude(Cyclin, amp), [vi, V2], [amp -> 0.8]).
```
%% Cell type:code id: tags:
```
seed(0). search_parameters(peak_amplitude(Cyclin, amp), [0<=vi<=1, 0<=V2<=2], [amp -> 0.8], cmaes_stop_fitness: -0.1).
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
validity_domain(peak_amplitude(Cyclin, amp)).
```
%% Cell type:code id: tags:
```
robustness(peak_amplitude(Cyclin, amp), [vi, V2], [amp -> 0.8]).
```
%% Cell type:code id: tags:
```
validity_domain(period(Cyclin, p)).
```
%% Cell type:markdown id: tags:
## Synthesis of continuous Biochemical Reaction Networks for Real Functions
* Definition of computable real functions by polynomial initial value problems (PIVPs)
* Synthesis of continuous CRNs from PIVPs (showing Turing completeness of PIVPs)
Synthesis of CRNs for the cosine function as a function of time or of an input x
%% Cell type:code id: tags:
```
clear_model.
```
%% Cell type:code id: tags:
```
compile_from_expression(cos,time,f).
```
%% Cell type:code id: tags:
```
list_model.
```
%% Cell type:code id: tags:
```
option(time:10). numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
numerical_simulation(method:ssa). plot.
```
%% Cell type:code id: tags:
```
clear_model.
```
%% Cell type:code id: tags:
```
compile_from_expression(cos,x,f).
```
%% Cell type:code id: tags:
```
list_model.
```
%% Cell type:code id: tags:
```
present(x_p,4).
```
%% Cell type:code id: tags:
```
numerical_simulation. plot.
```
%% Cell type:code id: tags:
```
seed(0). numerical_simulation(method:ssa). plot.
```
%% Cell type:code id: tags:
```
dose_response(x_p, 0, 6.28, show:{f_p, f_m}).
```
%% Cell type:markdown id: tags:
## Subsidiary question
Implement the cos(time) function with activation reactions (e.g. by phosphorylation) instead of synthesis reactions
Propose a deactivation scheme for the annihilation reactions.
%% Cell type:code id: tags:
```
```
This diff is collapsed.
% Cell cycle adapted from Qu et al, Biophysical journal
% 04/05/05
% kdweem=1, ksweem=0.5 to avoid high levels of Wee1m
% kwpcn=5, Kweem=0.2 instead of 2 and 1 because of Cry-deficient mice
% ksmpf=0.35 (instead of 0.3) for shorter cell cycle in autonomous cell cycle model.
parameter(kd25=1).
parameter(kdmpfp=0.25).
parameter(kampf=5).
parameter(kaapc=1).
parameter(ksweemp=0.001).
parameter(ksweem=0.5).
parameter(kdweem=1).
parameter(Kweem=0.2).
parameter(kwpcn=5).
parameter(Vac=1).
parameter(Kac25=0.01).
parameter(Kic25=0.01).
parameter(kdmpf=2).
parameter(Vaw=1).
parameter(Vapc=0.1).
parameter(Kaw=0.005).
parameter(Kiw=0.005).
parameter(Vapw=0.1).
parameter(Kapc=0.01).
parameter(ks25=1).
parameter(kswee=0.5).
parameter(kimpf=1.5).
parameter(Vic=0.2).
parameter(kiapc=0.5).
parameter(kdwee=1).
parameter(Viw=0.2).
parameter(ksmpf=0.35).
parameter(kdie=0.1).
parameter(ksiep=0).
parameter(ksie=0.3).
parameter(kaapcp=0).
% Reaction rules
% MPF - preMPF
ksmpf for _=>preMPF.
kdmpfp*preMPF for preMPF=>_.
kdmpfp*MPF for MPF=>_.
kdmpf*APC*MPF for MPF=[APC]=>_.
kdmpf*APC*preMPF for preMPF=[APC]=>_.
kampf*C25P*preMPF for preMPF=[C25P]=>MPF.
kimpf*Wee1*MPF for MPF=[Wee1]=>preMPF.
%function(ratio=kampf/kimpf).
% Wee1
Viw*Wee1P/(Kiw+Wee1P) for Wee1P=>Wee1.
(Vapw+Vaw*MPF)*Wee1/(Kaw+Wee1) for Wee1=[MPF]=>Wee1P.
ksweemp for _=>Wee1m.
kdweem*Wee1m for Wee1m=>_.
kswee*Wee1m for _=[Wee1m]=>Wee1.
kdwee*Wee1 for Wee1=>_.
kdwee*Wee1P for Wee1P=>_.
% Cdc25
Vic*C25P/(Kic25+C25P) for C25P=>C25.
(Vapc+Vac*MPF)*C25/(Kac25+C25) for C25=[MPF]=>C25P.
ks25 for _=>C25.
kd25*C25 for C25=>_.
kd25*C25P for C25P=>_.
% APC
ksiep for _=>IE.
ksie*MPF for _=[MPF]=>IE.
kdie*IE for IE=>_.
(kaapcp+kaapc*IE)*APCi/(Kapc+APCi) for APCi=[IE]=>APC.
kiapc*APC/(Kapc+APC) for APC=>APCi.
% Initial state
present(preMPF,0.279939269).
present(MPF,0.747404087).
present(C25,0.629659946).
present(C25P,0.370340054).
present(Wee1,0.00223979517).
present(Wee1P,0.132059534).
present(APC,0.0303504407).
present(IE,0.41856651).
present(Wee1m,0.141190132).
present(APCi,0.973282491).
This diff is collapsed.
%%% Circadian clock model from:
%%% J. Leloup and A.Goldbeter. Toward a detailedcomputational model for the mammalian circadian clock.
%%% Proceedings of the National Academy of Sciences, 100, pp. 7051-7056, 2003.