org: update the architecture diagram
For #254. * doc/org/arch.tex: Include libspotgen and its python bindings, genaut, and also the buddy bindings. * doc/org/concepts.org: Adjust the description.
This commit is contained in:
parent
f185aabf44
commit
472cd77098
2 changed files with 58 additions and 34 deletions
|
|
@ -10,18 +10,15 @@
|
||||||
\begin{document}
|
\begin{document}
|
||||||
|
|
||||||
\begin{tikzpicture}
|
\begin{tikzpicture}
|
||||||
\tikzset{cppbox/.style={minimum width=#1,fill=orange!30, minimum height=1.5cm},
|
\tikzset{node distance=2mm,
|
||||||
pybox/.style={minimum width=#1,fill=cyan!30, minimum height=1cm},
|
basicbox/.style={minimum width=#1,minimum height=8mm},
|
||||||
shbox/.style={minimum width=#1,fill=red!30, minimum height=8mm},
|
double height/.style={minimum height=18mm},
|
||||||
|
cppbox/.style={basicbox=#1,fill=orange!30},
|
||||||
|
pybox/.style={basicbox=#1,fill=cyan!30},
|
||||||
|
shbox/.style={basicbox=#1,fill=red!30},
|
||||||
usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}}
|
usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}}
|
||||||
\node[cppbox=7.3cm] (libspot) {\texttt{libspot\strut}};
|
\node[cppbox=14.12cm] (libspot) {\texttt{libspot\strut}};
|
||||||
\node[cppbox=4.3cm,right=2mm]
|
\node[shbox=3cm,above right=2mm and 0mm of libspot.north west,align=center] (shcmd) {
|
||||||
(libltsmin) at (libspot.east) {\texttt{libspot-ltsmin\strut}};
|
|
||||||
\node[cppbox=8cm,below right,yshift=-2mm,minimum height=8mm] (buddy) at (libspot.south west) {\texttt{libbddx\strut}};
|
|
||||||
|
|
||||||
\node[pybox=4.3cm,above=2mm] (pyltsmin) at (libltsmin.north) {\texttt{import spot.ltsmin\strut}};
|
|
||||||
\node[pybox=3cm,left=2mm] (pyspot) at (pyltsmin.west) {\texttt{import spot\strut}};
|
|
||||||
\node[shbox=4.1cm,above left,xshift=-2mm,align=center] (shcmd) at (pyspot.south west) {
|
|
||||||
\texttt{randltl}\\
|
\texttt{randltl}\\
|
||||||
\texttt{genltl}\\
|
\texttt{genltl}\\
|
||||||
\texttt{ltlfilt}\\
|
\texttt{ltlfilt}\\
|
||||||
|
|
@ -34,30 +31,51 @@
|
||||||
\texttt{ltlgrind}\\
|
\texttt{ltlgrind}\\
|
||||||
\texttt{ltldo}
|
\texttt{ltldo}
|
||||||
};
|
};
|
||||||
\node[shbox=1.9cm,below left,yshift=-2mm] (divine) at (libltsmin.south east) {\texttt{divine\strut}};
|
\node[cppbox=4.7cm,above right=0mm and 2mm of shcmd.south east] (libgen) {\texttt{libspotgen\strut}};
|
||||||
\node[shbox=1.5cm,left,xshift=-2mm] (spins) at (divine.west) {\texttt{SpinS\strut}};
|
\node[cppbox=2.5cm,above right=0mm and 2mm of libgen.south east] (buddy) {\texttt{libbddx\strut}};
|
||||||
\node[pybox=7.5cm,above right,yshift=2mm] (ipython) at (pyspot.north west) {IPython / Jupyter};
|
\node[pybox=2.5cm,above right=0mm and 2mm of buddy.south east,double height] (pyspot) {\texttt{import spot}};
|
||||||
|
\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}};
|
||||||
|
|
||||||
|
\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[pybox=12.65cm,above right=2mm and 0mm of pygen.north west] (ipython) {\texttt{python} / \texttt{ipython} / \texttt{jupyter}};
|
||||||
|
|
||||||
\draw[usedby] (buddy.north) -- ++(0,3mm);
|
\draw[usedby] (buddy.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (buddy.north) ++(3.7cm,0) -- ++(0,3mm);
|
\draw[usedby] (buddy.south) -- ++(0,-3mm);
|
||||||
|
\draw[usedby] (pybuddy.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (spins.north) -- ++(0,3mm);
|
\draw[usedby] (spins.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (divine.north) -- ++(0,3mm);
|
\draw[usedby] (divine.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (libspot.east) -- ++(3mm,0);
|
\draw[usedby] (libgen.south |- libspot.north) -- ++(0,3mm);
|
||||||
|
\draw[usedby] (genaut.south |- libgen.north) -- ++(0,3mm);
|
||||||
|
\draw[usedby] (pygen.south |- libgen.north) -- ++(0,3mm);
|
||||||
|
\draw[usedby] (pygen.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (pyspot.south) ++(0,-2mm) -- ++(0,3mm);
|
\draw[usedby] (pyspot.south) ++(0,-2mm) -- ++(0,3mm);
|
||||||
\draw[usedby] (pyltsmin.south) ++(0,-2mm) -- ++(0,3mm);
|
\draw[usedby] (pyltsmin.south) ++(0,-2mm) -- ++(0,3mm);
|
||||||
\draw[usedby] (shcmd.south) ++(0,-2mm) -- ++(0,3mm);
|
\draw[usedby] (shcmd.south) ++(0,-2mm) -- ++(0,3mm);
|
||||||
\draw[usedby] (pyspot.north) -- ++(0,3mm);
|
\draw[usedby] (pyspot.north) -- ++(0,3mm);
|
||||||
\draw[usedby] (pyltsmin.north) -- ++(0,3mm);
|
\draw[usedby] (pyltsmin.north) -- ++(0,3mm);
|
||||||
|
\coordinate (x) at ($(libltsmin.south west)!.5!(libspot.north east)$);
|
||||||
|
\draw[usedby] (libspot.north -| x) -- ++(0,3mm);
|
||||||
|
|
||||||
\begin{pgfonlayer}{background}
|
\begin{pgfonlayer}{background}
|
||||||
\path[fill=gray!15,draw=gray,rounded corners=1mm]
|
\path[fill=gray!15,draw=gray,rounded corners=1mm]
|
||||||
($(shcmd.north west)+(-1mm,1mm)$) --
|
($(shcmd.north west)+(-1mm,1mm)$) --
|
||||||
($(shcmd.north east)+(1mm,1mm)$) --
|
($(shcmd.north east)+(1mm,1mm)$) --
|
||||||
($(pyspot.north west)+(-1mm,1mm)$) --
|
($(genaut.north west)+(-1mm,1mm)$) --
|
||||||
|
($(genaut.north east)+(1mm,1mm)$) --
|
||||||
|
($(pygen.north west)+(-1mm,1mm)$) --
|
||||||
($(pyltsmin.north east)+(1mm,1mm)$) --
|
($(pyltsmin.north east)+(1mm,1mm)$) --
|
||||||
($(libltsmin.south east)+(1mm,-1mm)$) --
|
($(libltsmin.south east)+(1mm,-1mm)$) --
|
||||||
($(buddy.north east)+(1mm,1mm)$) --
|
($(libspot.north east)+(1mm,1mm)$) --
|
||||||
($(buddy.south east)+(1mm,-1mm)$) --
|
($(libspot.south east)+(1mm,-1mm)$) --
|
||||||
($(buddy.south west)+(-1mm,-1mm)$) -- cycle;
|
($(libspot.south west)+(-1mm,-1mm)$) -- cycle;
|
||||||
\end{pgfonlayer}
|
\end{pgfonlayer}
|
||||||
\end{tikzpicture}
|
\end{tikzpicture}
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
|
||||||
|
|
@ -1017,24 +1017,30 @@ from the command-line, Python, or C++.
|
||||||
|
|
||||||
The Spot project can be broken down into several parts, as shown
|
The Spot project can be broken down into several parts, as shown
|
||||||
above. Orange boxes are C/C++ libraries. Red boxes are command-line
|
above. Orange boxes are C/C++ libraries. Red boxes are command-line
|
||||||
program. Blue boxes are Python-related.
|
programs. Blue boxes are Python-related. The gray outline shows the
|
||||||
|
components that are distributed and installed by Spot.
|
||||||
|
|
||||||
- =libbddx= is a customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]], for
|
- =libbddx= is a customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]], for
|
||||||
manipulating [[#bdd][BDDs]].
|
manipulating [[#bdd][BDDs]].
|
||||||
- =libspot= is the main library, containing a C++11 implementation of all the
|
- =libspot= is the main library, containing a C++11 implementation of all the
|
||||||
data structures and algorithms. This depends on =libddx=.
|
data structures and algorithms. This depends on =libddx=.
|
||||||
- all the supplied [[file:tools.org][command-line tools]] are built upon the =libspot=
|
- =libspotgen= is an auxiliary library that contains functions to
|
||||||
library, exporting some of its features to shell users
|
generate families of automata, useful for benchmarking and testing
|
||||||
- =libspot-ltsmin= is a library that helps interfacing Spot with
|
- all the supplied [[file:tools.org][command-line tools]] distributed with Spot are
|
||||||
|
built upon the =libspot= or =libspotgen= libraries
|
||||||
|
- =libspotltsmin= is a library that helps interfacing Spot with
|
||||||
dynamic libraries that [[http://fmt.cs.utwente.nl/tools/ltsmin/][LTSmin]] uses to represent state-spaces. It
|
dynamic libraries that [[http://fmt.cs.utwente.nl/tools/ltsmin/][LTSmin]] uses to represent state-spaces. It
|
||||||
currently supports libraries generated from promela models using
|
currently supports libraries generated from promela models using
|
||||||
SpinS or a patched version of DiVinE, but you have to install
|
SpinS or a patched version of DiVinE, but you have to install
|
||||||
those third-party tools first. See [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/ltsmin/README][=tests/ltsmin/README=]]
|
those third-party tools first. See [[https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/ltsmin/README][=tests/ltsmin/README=]]
|
||||||
for details.
|
for details.
|
||||||
- In addition to the C++11 API, we also provide Python bindings for
|
- In addition to the C++11 API, we also provide Python bindings for
|
||||||
=libspot-ltsmin= and most of =libspot=. These are available by
|
=libspotgen=, =libspotltsmin=, =libbddx=, and most of =libspot=.
|
||||||
importing =spot= or =spot.ltsmin=, and have readily usable in an
|
These are available by importing =spot.gen=, =spot.ltsmin=, =bdd=,
|
||||||
interactive environment such as the [[http://juptter.org][IPython/Jupyter]] notebook.
|
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.
|
||||||
|
|
||||||
* Automaton property flags
|
* Automaton property flags
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CUSTOM_ID: property-flags
|
:CUSTOM_ID: property-flags
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue