The Biochemical Abstract Machine (Biocham) is a software environment for
modeling and analyzing biochemical systems.
Biocham is mainly composed of:
\\begin{itemize}
\\item a rule-based language for modeling biochemical systems (compatible with
SBML and SBGN),
\\item static analysers for inferring various dynamical properties from the structure of the model;
\\item simulators for the different semantics: continuous (differential equations), stochastic, asynchronous Boolean;
\\item a temporal logic based language to formalize the temporal behaviours of
biological systems, validate models with respect to such specifications by model-checking methods,
infer parameter values in high dimension with temporal logic constraints,
measure parameter sensitivity indices and robustness of temporal properties;
\\item unique features for developing/correcting/completing/reducing/coupling
models.
\\end{itemize}
The Biochemical Abstract Machine (Biocham) is a modelling software for cell systems biology, with some unique features for static and dynamic analyses using temporal logic constraints.
Biocham v4 is mainly composed of :
\\begin{itemize}
\\item
a rule-based language for modeling biochemical processes with reactions and/or influences (respectively SBML2 and SBML3-qual compatible),
\\item
a hierarchy of semantics (differential, stochastic, Petri Net, Boolean) to interpret such models,
\\item
a temporal logic based language to formalize the temporal behaviors of biochemical systems,
\\item
several unique features for developing/analyzing/correcting/completing/calibrating/coupling/synthesizing reaction and influence systems with respect to formal specifications of their behaviour.
\\end{itemize}
Biocham v4 is a complete rewriting of Biocham v3.
It introduces some new features, mainly:
\\begin{itemize}
\\item
\\item
\\item
\\item
\\item
\\end{itemize}
Some features of Biocham v3 have not been implemented yet, mainly:
\\begin{itemize}
\\item the Graphical User Interface (only the notebook)
\\item the graphical editor (SBGN compatible)
\\item the sensivity and robustness measures
\\item the detection of model reductions by subgraph epimorphisms (SEPI)
\\item hybrid simulations
\\end{itemize}
').
:-doc('
Biocham is a free software protected by the GNU General Public License GPL
version 2. This is an Open Source license that allows free usage of this
@@ -14,8 +14,8 @@ Some other file formats are used.').
:-doc('
Biocham models can be imported from, and exported to, other file formats using the following suffixes:
\\begin{itemize}
\\item \\texttt{.xml} for Systems Biology Markup Language (SBML) files, more precisely SBML2 files for reaction systems and SBML3qual files for influence systems;
\\item \\texttt{.ode} for Ordinary Differential Equation files (ODEs in XXPAUT format), allowing us to import a reaction system from ODEs using a heuristic inference algorithm described in \\cite{FGS15tcs}.
\\item \\texttt{.xml} for Systems Biology Markup Language (SBML) files, more precisely SBML2 files for reaction networks and SBML3qual files for influence networks;
\\item \\texttt{.ode} for Ordinary Differential Equation files (ODEs in XXPAUT format), allowing us to infer and import a reaction network from ODEs using a heuristic inference algorithm described in \\cite{FGS15tcs}.
\\end{itemize}
Biocham numerical data time series can be imported/exported in
:-doc('Petri Net Place-invariants provide linear conservation laws for the differential semantics of a reaction system.
:-doc('Petri Net Place-invariants provide linear conservation laws for the differential semantics of a reaction network.
They can be verified or computed with the commands below. Note that such invariants are useful information but it may be not a good idea to use them to reduce
the dimensionality of the system since it may introduce numerical unstabilities.').
...
...
@@ -79,7 +79,7 @@ check_conservations :-
search_conservations:-
biocham_command,
doc(
'computes and displays the P-invariants of the system up to the maximal
'computes and displays the P-invariants of the network up to the maximal
size given by the option conservation_size and defaulting to 4. Such
P-invariants are particular mass conservation laws that are independent
:-doc('The Computation Tree Logic CTL can be used to express qualitative properties of the behavior of a system in a given (set of) initial states, at the boolean level of abstraction \\cite{CCDFS04tcs}.
:-doc('The Computation Tree Logic CTL can be used to express qualitative properties of the behavior of a network in a given (set of) initial states, at the boolean level of abstraction \\cite{CCDFS04tcs}.
CTL extends propositional logic with modal operators to specify where (E: on some path, A: on all paths)
and when (X: next state, F: finally at some future state, G: globally on all states, U: until a second formula is true, R: release)
a formula is true. As in any logic, these modalities can be combined with logical connectives and imbricated,
...
...
@@ -142,7 +142,7 @@ ctl(E) :-
:-devdoc('\\section{Commands}').
:-doc('The qualitative behavior of a system can be specified by a set of CTL formulas using the following commands:').
:-doc('The qualitative behavior of a network can be specified by a set of CTL formulas using the following commands:').
list_ctl:-
...
...
@@ -178,12 +178,12 @@ delete_ctl :-
delete_items([kind:ctl_spec]).
:-doc('The set of CTL formulas of some simple form that are true in the current set of initial states
can also be automatically generated as a specification of the system using the following commands.').
can also be automatically generated as a specification of the network using the following commands.').
generate_ctl(Formula):-
biocham_command,
type(Formula,ctl),
doc('adds to the CTL specification all the CTL formulas that are true, not subsumed by another CTL formula in the specification, and that match the argument formula in which the names that are not molecules are treated as wildcards and replaced by distinct molecules of the system. This command is a variant with subsumption test of \\command{add_ctl} if all names match system molecule names, otherwise it enumerates all m^v instances (where m is the number of molecules and v the number of wildcards in the formula).'),
doc('adds to the CTL specification all the CTL formulas that are true, not subsumed by another CTL formula in the specification, and that match the argument formula in which the names that are not molecules are treated as wildcards and replaced by distinct molecules of the network. This command is a variant with subsumption test of \\command{add_ctl} if all names match network molecule names, otherwise it enumerates all m^v instances (where m is the number of molecules and v the number of wildcards in the formula).'),
:-doc('Biocham can also compile mathematical expressions and solutions of polynomial differential equations into biochemical reaction systems using only positive concentration values.').
:-doc('Biocham can also compile mathematical expressions and solutions of polynomial differential equations into biochemical reaction networks using only positive concentration values.').
:-doc('Bipartite molecule-influence graphs can be associated to both influence models and reaction systems. The influence graph of a reaction system is an abstraction defined from the stoichiometry of the reactions, which is equivalent, under general conditions, to the influence graph defined by the signs of the Jacobian matrix of the ODEs \\cite{FS08fmsb,FGS15tcs}.').
%:- doc('Bipartite molecule-influence graphs can be associated to both influence and reaction systems. The influence graph of a reaction system is an abstraction defined from the stoichiometry of the reactions, which is equivalent, under general conditions, to the influence graph defined by the signs of the Jacobian matrix of the ODEs \\cite{FS08fmsb,FGS15tcs}.').
:-devdoc('\\section{Commands}').
influence_graph:-
biocham_command,
doc('infers the graph of influences of the current model.'),
new_graph,
set_graph_name(influence_graph),
get_current_graph(GraphId),
influence_graph(GraphId).
influence_hypergraph:-
draw_influence_hypergraph:-
biocham_command,
doc('builds the hypergraph of the influence rules of the current model.'),
new_graph,
set_graph_name(influence_hypergraph),
get_current_graph(GraphId),
influence_hypergraph(GraphId).
doc('
Draws the hypergraph of the influence rules of the current model. The hypergraph distinguishes each influence. Equivalent to \\texttt{influence_hypergraph. draw_graph}.
'),
setup_call_cleanup(
new_graph(GraphId),
(
influence_hypergraph(GraphId),
draw_graph(GraphId)
),
delete_item(GraphId)
).
draw_influences:-
biocham_command,
doc('
infers and draws the influence graph of the current model.
Draws the influence graph between molecular species of the current model, by merging the different influences. Equivalent to \\texttt{influence_graph. draw_graph}.
\\begin{example}
'),
biocham_silent(clear_model),
...
...
@@ -56,20 +54,22 @@ draw_influences :-
delete_item(GraphId)
).
influence_hypergraph:-
biocham_command,
doc('builds the hypergraph of the influence rules of the current model.'),
new_graph,
set_graph_name(influence_hypergraph),
get_current_graph(GraphId),
influence_hypergraph(GraphId).
draw_influence_hypergraph:-
influence_graph:-
biocham_command,
doc('
Draws the hypergraph of the influence rules of the current model.
'),
setup_call_cleanup(
new_graph(GraphId),
(
influence_hypergraph(GraphId),
draw_graph(GraphId)
),
delete_item(GraphId)
).
doc('builds the influence graph between molecular species without distinguishing the different influences.'),
:-doc('BIOCHAM models can also be defined by influence systems with forces between molecular species. In the syntax described below, one influence rule (either positive "->" or negative "-<") expresses that a conjunction of sources (or their negation after the separator "/" for inhibitors) has an influence on a target molecular species. This syntax necessitates to write the Boolean activation (resp. deactivation) function of a molecular species in Disjunctive Normal Form with several positive (resp. negative) influences \\cite{FMRS16cmsb}.').
:-doc('BIOCHAM models can also be defined by influence systems with forces, possibly mixed to reactions with rates.').
:-doc('In the syntax described by the grammar below, one influence rule (either positive "->" or negative "-<") expresses that a conjunction of sources (or their negation after the separator "/" for inhibitors) has an influence on a target molecular species. This syntax necessitates to write the Boolean activation (resp. deactivation) functions of the molecular species in Disjunctive Normal Form, i.e. with several positive (resp. negative) influences in which the sources are interpreted by a conjunction \\cite{FMRS16cmsb}.').
:-doc('Biocham can also manipulate ODE systems written in the following XPP syntax, and infer a reaction system, or an influence system, with the same ODE semantics. This is useful for using Biocham analyzers on ODE models.').
:-doc('Biocham can also manipulate ODE systems written in the following XPP syntax, and infer a reaction or influence network, with the same ODE semantics. This is useful for importing MatLab models in SBML, and using Biocham analyzers on ODE models.').
:-doc('\\emph{Warning}: XPP format has restrictions on names and does not distinguish between upper case and lower case letters. As a consequence, some complex names may be not properly exported in ode files, and when an ode file is imported, the names are read in lower case.').
:-doc("This part describes the syntax of BIOCHAM models of biochemical processes. They are essentially of two forms: reaction systems (i.e. Feinberg's Chemical Reaction Networks, CRNs, compatible with SBML) and influence systems (variant of Thomas's regulatory networks, compatible with qualSBML). Both types of models can be interpreted in a hierarchy of semantics, including the differential semantics (Ordinary Differential Equations), stochastic semantics (Continuous-time Markov Chain), Petri Net semantics, and several Boolean semantics \\cite{FMRS16cmsb}.").
:-doc("This part describes the syntax of BIOCHAM models of biochemical processes. They are essentially of two forms:
\\begin{itemize}
\\item reaction systems (i.e. Feinberg's Chemical Reaction Networks, CRNs, compatible with SBML)
\\item and influence systems (variant of Thomas's regulatory networks, compatible with qualSBML).
\\end{itemize}
Both types of models can be interpreted in a hierarchy of semantics, including the differential semantics (Ordinary Differential Equations), stochastic semantics (Continuous-time Markov Chain), Petri net semantics, and Boolean semantics with several variants \\cite{FMRS16cmsb}.").
:-doc('In Biocham v4, a reaction system is a multiset of reactions. Reactions can thus be in multiple copies in which case their reaction rates are summed.').
:-devcom('\\begin{todo}For several reasons, we should automatically introduce kinetic parameters k_1, k_2, etc. for the default mass action law kinetics of reactions given without kinetic expression. The same could go for initial_state concentrations which BTW should be definable by parameters or functions, introducing concentration parameters c_1, c_2, etc. for present molecules. The pros are an encouragement to use parameters, parameter search, sensitivity and robustness analyses. The cons are an irrelevant encouragement for logical models. \\end{todo}').
add_reaction(Reaction):-
...
...
@@ -48,6 +46,10 @@ add_reaction(Reaction) :-
)
).
:-doc('\\begin{remark}In Biocham v4, a reaction system is a multiset of reactions. Reactions can thus be added in multiple copies in which case their reaction rates are summed.\\end{remark}').
:-doc('A BIOCHAM model can be defined by a reaction system, i.e. a finite (multi)set of directed reaction rules with rate functions using the syntax below.
A reaction system represents a Chemical Reaction Network (CRN) and is compatible with the Systems Biology Markup Language SBML.').
:-doc('(Bio)chemical reaction networks (CRNs) can be described in BIOCHAM by a reaction system,
i.e. a finite (multi)set of directed reaction rules with rate functions, with the syntax defined by the grammar below.
BIOCHAM reaction systems are compatible with the Systems Biology Markup Language SBML version 2.').
:-doc('Numerical data time series, produced by biological experiments or by simulations, can be stored in \\texttt{.csv} files, and loaded as a specification of the behavior. They can also be modified by the following commands.').
:-doc('Numerical data time series, produced by biological experiments or by simulations, can be stored in \\texttt{.csv} files, and loaded.
They can also be modified by the following commands.').
The exhaustive list of Biocham commands avaiable at toplevel is described in the following sections.
New reactions and new influences can also be entered directly at toplevel, as a short hand for the commands \\texttt{add_reaction} and \\texttt{add_influence} respectively.
The exhaustive list of Biocham commands available at toplevel is described in the rest of this manual.
').
:-doc('
Some commands (e.g., \\command{numerical_simulation/0} in the example below) take named options
New reactions and new influences can also be entered directly at toplevel, as a short hand for the commands \\texttt{add_reaction} and \\texttt{add_influence} respectively.
').
:-biocham_silent('clear_model').
:-doc('Some commands (e.g., \\command{numerical_simulation/0} in the example below) take named options
as arguments.
All the options can be defined either locally for a single command or
:-doc('\\begin{example}This example shows the dose-response diagrams of the MAPK model of Huang and Ferrell in BiomModels revealing the amplifier and analog-digital converter functions
of this network at the second and third level of the cascade. ').
:-doc('\\begin{example}This example shows a memory effect (and erroneous dose-response diagrams) in the MAPK network when using too short simulation times.
:-doc('Biocham can compile a GPAC circuit (Shannon\'sGeneralPurposeAnalogComputer)intoanabstractreactionsystemusingpositiveaswellasnegativeconcentrationvalues.OnlyweakGPACs,inwhichtheintegrationgateiswithrespecttotimeandnotavariable,areconsidered.Thevariablesassociatedtothedifferentpointsofthecircuitscanbenamedwiththe"::"operator.Dydefaulttheyarenamedx0,x1,...ThesyntaxofweakGPACcircuitsisasfollows:').
:-doc('Biocham can compile a GPAC circuit (Shannon\'sGeneralPurposeAnalogComputer)intoanabstractreactionnetworkusingpositiveaswellasnegativeconcentrationvalues.OnlyweakGPACs,inwhichtheintegrationgateiswithrespecttotimeandnotavariable,areconsidered.Thevariablesassociatedtothedifferentpointsofthecircuitscanbenamedwiththe"::"operator.Dydefaulttheyarenamedx0,x1,...ThesyntaxofweakGPACcircuitsisasfollows:').