Commit 317520ef authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: improve architecture diagram

* doc/org/arch.tex: Improve diagram, add links and online services.
* doc/org/concepts.org: Update text.
parent 56e08af8
......@@ -6,6 +6,7 @@
\usetikzlibrary{positioning}
\usetikzlibrary{calc}
\usetikzlibrary{backgrounds}
\usepackage[hidelinks]{hyperref}
\begin{document}
......@@ -17,21 +18,22 @@
cppbox/.style={basicbox=#1,fill=orange!30},
pybox/.style={basicbox=#1,fill=cyan!30},
shbox/.style={basicbox=#1,fill=red!30},
webbox/.style={basicbox=#1,fill=black!30!green!30!white},
usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}}
\node[cppbox=14.12cm] (libspot) {\texttt{libspot\strut}};
\node[shbox=3cm,above right=2mm and 0mm of libspot.north west,align=center] (shcmd) {
\texttt{randltl}\\
\texttt{ltlfilt}\\
\texttt{randaut}\\
\texttt{autfilt}\\
\texttt{ltl2tgba}\\
\texttt{ltl2tgta}\\
\texttt{dstar2tgba}\\
\texttt{ltlcross}\\
\texttt{ltlgrind}\\
\texttt{ltlsynt}\\
\texttt{ltldo}\\
\texttt{autcross}
\href{https://spot.lrde.epita.fr/randltl.html}{\texttt{randltl}}\\
\href{https://spot.lrde.epita.fr/ltlfilt.html}{\texttt{ltlfilt}}\\
\href{https://spot.lrde.epita.fr/randaut.html}{\texttt{randaut}}\\
\href{https://spot.lrde.epita.fr/autfilt.html}{\texttt{autfilt}}\\
\href{https://spot.lrde.epita.fr/ltl2tgba.html}{\texttt{ltl2tgba}}\\
\href{https://spot.lrde.epita.fr/ltl2tgta.html}{\texttt{ltl2tgta}}\\
\href{https://spot.lrde.epita.fr/dstar2tgba.html}{\texttt{dstar2tgba}}\\
\href{https://spot.lrde.epita.fr/ltlcross.html}{\texttt{ltlcross}}\\
\href{https://spot.lrde.epita.fr/ltlgrind.html}{\texttt{ltlgrind}}\\
\href{https://spot.lrde.epita.fr/ltlsynt.html}{\texttt{ltlsynt}}\\
\href{https://spot.lrde.epita.fr/ltldo.html}{\texttt{ltldo}}\\
\href{https://spot.lrde.epita.fr/autcross.html}{\texttt{autcross}}
};
\node[cppbox=4.7cm,above right=0mm and 2mm of shcmd.south east] (libgen) {\texttt{libspotgen\strut}};
\node[cppbox=2.5cm,above right=0mm and 2mm of libgen.south east] (buddy) {\texttt{libbddx\strut}};
......@@ -39,18 +41,21 @@
\node[cppbox=4cm,above right=0mm and 2mm of pyspot.south east] (libltsmin) {\texttt{libspotltsmin\strut}};
\node[shbox=1.5cm,above right=2mm and 0mm of libgen.north west,align=center] (genaut) {
\texttt{genaut\strut}\\
\texttt{genltl}
\href{https://www.lrde.epita.fr/genaut.html}{\texttt{genaut\strut}}\\
\href{https://www.lrde.epita.fr/genltl.html}{\texttt{genltl}}
};
\node[pybox=3cm,above left=2mm and 0mm of libgen.north east] (pygen) {\texttt{import spot.gen\strut}};
\node[pybox=2.5cm,above=of buddy] (pybuddy) {\texttt{import bdd\strut}};
\node[pybox=4cm,above=2mm] (pyltsmin) at (libltsmin.north) {\texttt{import spot.ltsmin\strut}};
\node[shbox=1.5cm,right=of libspot] (spins) {\texttt{SpinS\strut}};
\node[shbox=1.5cm,right=of spins] (divine) {\texttt{divine\strut}};
\node[shbox=1.5cm,right=of libspot] (spins) {\href{https://github.com/utwente-fmt/spins}{\texttt{SpinS\strut}}};
\node[shbox=1.5cm,right=of spins] (divine) {\href{https://github.com/utwente-fmt/divine2/}{\texttt{divine\strut}}};
\node[pybox=12.65cm,above right=2mm and 0mm of pygen.north west] (ipython) {\texttt{python} / \texttt{ipython} / \texttt{jupyter}};
\node[pybox=12.65cm,above right=2mm and 0mm of pygen.north west] (ipython) {\href{https://www.python.org/}{\texttt{python}} / \href{https://ipython.org/}{\texttt{ipython}} / \href{https://jupyter.org/}{\texttt{jupyter}}};
\node[webbox=6.2cm,above right=2mm and 0mm of ipython.north west] (webapp) {\href{https://spot.lrde.epita.fr/app/}{online LTL translator}};
\node[webbox=6.2cm,above left=2mm and 0mm of ipython.north east] (sandbox) {\href{https://spot-sandbox.lrde.epita.fr/}{Spot sandbox}};
\draw[usedby] (buddy.north) -- ++(0,3mm);
\draw[usedby] (buddy.south) -- ++(0,-3mm);
......@@ -68,6 +73,8 @@
\draw[usedby] (pyltsmin.north) -- ++(0,3mm);
\coordinate (x) at ($(libltsmin.south west)!.5!(libspot.north east)$);
\draw[usedby] (libspot.north -| x) -- ++(0,3mm);
\draw[usedby] (ipython.north -| webapp) -- ++(0,3mm);
\draw[usedby] (ipython.north -| sandbox) -- ++(0,3mm);
\begin{pgfonlayer}{background}
\path[fill=gray!15,draw=gray,rounded corners=1mm]
......
......@@ -1019,7 +1019,9 @@ from the command-line, Python, or C++.
The Spot project can be broken down into several parts, as shown
above. Orange boxes are C/C++ libraries. Red boxes are command-line
programs. Blue boxes are Python-related. The gray outline shows the
components that are distributed and installed by Spot.
components that are distributed and installed by the Spot tarball.
Green boxes represent online services that build upon the Python
layers.
- =libbddx= is a customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]], for
manipulating [[#bdd][BDDs]].
......@@ -1040,7 +1042,14 @@ components that are distributed and installed by Spot.
These are available by importing =spot.gen=, =spot.ltsmin=, =bdd=,
and =spot=. Those Python bindings also includes some additional
code to make them more usable in interactive environments such as
the [[http://juptter.org][IPython/Jupyter]] notebook.
the [[http://jupyter.org][IPython/Jupyter]] notebook.
- While the online services described pictured in green are not
distributed with the rest of Spot, their source-code is publicly
available (in case you want to contribute or run a local version).
The [[https://spot-sandbox.lrde.epita.fr/][=spot-sandbox=]] website runs from a Docker container whose
configuration can be found in [[https://gitlab.lrde.epita.fr/spot/sandbox/tree/master=][this repository]]. The client and
server parts of the [[https://spot.lrde.epita.fr/app/][online LTL translator]] can be found in [[https://gitlab.lrde.epita.fr/spot/spot-web-app/][this
repository]].
* Automaton property flags
:PROPERTIES:
......
Supports Markdown
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