Commit b10a32ba authored by FAGES Francois's avatar FAGES Francois

doc francois

parent 9db215c7
......@@ -2,8 +2,9 @@
Documentation
-------------
La documentation est générée automatiquement à partir du code
dans les repertoire doc/index.html et devdoc/index.html
La documentation est générée automatiquement
à partir du code et du fichier toc.org (ouverture des sous sections avec tab)
dans les repertoireq doc/index.html et devdoc/index.html
(versions index.tex également disponibles pour xelatex)
Il est bon de documenter les prédicats
......
File added
......@@ -29,6 +29,30 @@
software.
').
% FF ca cree un bug que je ne comprends pas
%:- doc('
%Biocham file names are suffixed by \\texttt{.bc}. In a Biocham file, everything following the character percent is a comment.
%Some other file formats are used.
%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}.
%\\end{itemize}
%Biocham numerical data time series can be imported/exported in
%\\begin{itemize}
%\\item \\texttt{.csv} comma-separated values format (spreadsheet format).
%\\end{itemize}
%The following files can also be used to export some Biocham objects:
%\\begin{itemize}
%\\item \\texttt{.tex} LaTeX format for exporting ODEs and graphs;
%\\item \\texttt{.dot} for exporting graphs;
%\\item \\texttt{.plot} for exporting numerical data time series;
%\\item \\texttt{.smv} for exporting boolean transition systems and Computation Tree Logic (CTL) queries for the NuSMV model-checker;
%\\item \\texttt{.dot} for exporting graphs.
%\\end{itemize}
%').
start :-
about,
initialize,
......
File added
File added
#x
20
10
30
15
Domain
compute_domain(Table table) {
PPL::Variable x0(0);
Domain domain0(1, PPL::EMPTY);
Domain domain1(1, PPL::EMPTY);
Domain domain2(1, PPL::EMPTY);
Domain domain3(1, PPL::EMPTY);
Domain domain4(1, PPL::EMPTY);
for (Table::reverse_iterator i = table.rbegin(); i != table.rend(); ++i) {
Domain next_domain4(1, (*i)[0] > 10 ? PPL::UNIVERSE : PPL::EMPTY);
Domain next_domain3(domain4);
Domain next_domain2(1, PPL::EMPTY);
PPL::Constraint_System cs;
cs.insert((*i)[0] == x0);
next_domain2.add_disjunct(PPL::C_Polyhedron(cs));
Domain next_domain1(next_domain2);
next_domain1.intersection_assign(next_domain3);
Domain next_domain0(domain0);
for (
Domain::iterator j = next_domain1.begin();
j != next_domain1.end(); ++j
) {
next_domain0.add_disjunct(j->pointset());
}
domain4 = next_domain4;
domain3 = next_domain3;
domain2 = next_domain2;
domain1 = next_domain1;
domain0 = next_domain0;
}
return domain0;
}
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
set input_file nusmv.smv
go
set default_trace_plugin 2
set counter_examples 1
check_ctlspec -p "EF b"
quit
MODULE main
VAR a: boolean;
INIT a in TRUE;
VAR b: boolean;
INIT b in FALSE;
TRANS (a <-> next(a)) & (b <-> next(b)) & (!a | FALSE) & (!a | !b | FALSE) | a & TRUE & next(b) & TRUE & TRUE | a & b & TRUE & next(a) & TRUE & TRUE
File added
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
set term png
set output "plot4.png"
set style data lines
set datafile separator ","
plot "plot.csv" using 1:2 title "MAPKPH", "plot.csv" using 1:3 title "MAPK~{p1}", "plot.csv" using 1:4 title "MAPK~{p1,p2}-MAPKPH", "plot.csv" using 1:5 title "MAPK", "plot.csv" using 1:6 title "MAPK~{p1}-MAPKPH", "plot.csv" using 1:7 title "MEK~{p1,p2}", "plot.csv" using 1:8 title "MAPK~{p1,p2}", "plot.csv" using 1:9 title "MAPK~{p1}-MEK~{p1,p2}", "plot.csv" using 1:10 title "MAPK-MEK~{p1,p2}", "plot.csv" using 1:11 title "MEKPH", "plot.csv" using 1:12 title "MEK~{p1}", "plot.csv" using 1:13 title "MEK~{p1,p2}-MEKPH", "plot.csv" using 1:14 title "MEK", "plot.csv" using 1:15 title "MEK~{p1}-MEKPH", "plot.csv" using 1:16 title "RAF~{p1}", "plot.csv" using 1:17 title "MEK-RAF~{p1}", "plot.csv" using 1:18 title "MEK~{p1}-RAF~{p1}", "plot.csv" using 1:19 title "RAFPH", "plot.csv" using 1:20 title "RAF", "plot.csv" using 1:21 title "RAF~{p1}-RAFPH", "plot.csv" using 1:22 title "RAFK", "plot.csv" using 1:23 title "RAF-RAFK"
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
File added
This diff is collapsed.
This diff is collapsed.
set input_file nusmv.smv
go
set default_trace_plugin 2
set counter_examples 1
check_ctlspec -p "EF b"
quit
This diff is collapsed.
File added
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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