alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: improve architecture diagram

Browse source 
* doc/org/arch.tex: Improve diagram, add links and online services.
* doc/org/concepts.org: Update text.
This commit is contained in:
Alexandre Duret-Lutz 2019-12-03 17:48:46 +01:00
parent 3d4e400cda
commit 3be394d2eb
2 changed files with 35 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

41
doc/org/arch.tex
View file

@ -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]

13
doc/org/concepts.org
View file

@ -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: