diff --git a/doc/Makefile.am b/doc/Makefile.am index 2c8e97eb2..9f9f46512 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -70,6 +70,8 @@ ORG_FILES = \ org/g++wrap.in \ org/init.el.in \ org/spot.css \ + org/arch.tex \ + $(srcdir)/org/arch.png \ org/autfilt.org \ org/csv.org \ org/compile.org \ @@ -110,6 +112,11 @@ $(srcdir)/org/satmin.png: org/satmin.tex pdflatex -shell-escape satmin.tex && \ rm -f satmin.pdf satmin.aux satmin.log +$(srcdir)/org/arch.png: org/arch.tex + cd $(srcdir)/org && \ + pdflatex -shell-escape arch.tex && \ + rm -f arch.pdf arch.aux arch.log + $(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac) $(MAKE) org && touch $@ diff --git a/doc/org/arch.tex b/doc/org/arch.tex new file mode 100644 index 000000000..8773bd6ec --- /dev/null +++ b/doc/org/arch.tex @@ -0,0 +1,67 @@ +\documentclass[convert={size=640}]{standalone} +\usepackage{tikz} +\usetikzlibrary{arrows} +\usetikzlibrary{arrows.meta} +\usetikzlibrary{shadows} +\usetikzlibrary{positioning} +\usetikzlibrary{calc} +\usetikzlibrary{backgrounds} + +\begin{document} + +\begin{tikzpicture} + \tikzset{cppbox/.style={minimum width=#1,fill=orange!30, minimum height=1.5cm}, + pybox/.style={minimum width=#1,fill=cyan!30, minimum height=1cm}, + shbox/.style={minimum width=#1,fill=red!30, minimum height=8mm}, + usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}} + \node[cppbox=7.3cm] (libspot) {\texttt{libspot\strut}}; + \node[cppbox=4.3cm,right=2mm] + (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{genltl}\\ + \texttt{ltlfilt}\\ + \texttt{randaut}\\ + \texttt{autfilt}\\ + \texttt{ltl2tgba}\\ + \texttt{ltl2tgta}\\ + \texttt{dstar2tgba}\\ + \texttt{ltlcross}\\ + \texttt{ltlgrind}\\ + \texttt{ltldo} + }; + \node[shbox=1.9cm,below left,yshift=-2mm] (divine) at (libltsmin.south east) {\texttt{divine\strut}}; + \node[shbox=1.5cm,left,xshift=-2mm] (spins) at (divine.west) {\texttt{SpinS\strut}}; + \node[pybox=7.5cm,above right,yshift=2mm] (ipython) at (pyspot.north west) {IPython / Jupyter}; + \draw[usedby] (buddy.north) -- ++(0,3mm); + \draw[usedby] (buddy.north) ++(3.7cm,0) -- ++(0,3mm); + \draw[usedby] (spins.north) -- ++(0,3mm); + \draw[usedby] (divine.north) -- ++(0,3mm); + \draw[usedby] (libspot.east) -- ++(3mm,0); + \draw[usedby] (pyspot.south) ++(0,-2mm) -- ++(0,3mm); + \draw[usedby] (pyltsmin.south) ++(0,-2mm) -- ++(0,3mm); + \draw[usedby] (shcmd.south) ++(0,-2mm) -- ++(0,3mm); + \draw[usedby] (pyspot.north) -- ++(0,3mm); + \draw[usedby] (pyltsmin.north) -- ++(0,3mm); + + \begin{pgfonlayer}{background} + \path[fill=gray!15,draw=gray,rounded corners=1mm] + ($(shcmd.north west)+(-1mm,1mm)$) -- + ($(shcmd.north east)+(1mm,1mm)$) -- + ($(pyspot.north west)+(-1mm,1mm)$) -- + ($(pyltsmin.north east)+(1mm,1mm)$) -- + ($(libltsmin.south east)+(1mm,-1mm)$) -- + ($(buddy.north east)+(1mm,1mm)$) -- + ($(buddy.south east)+(1mm,-1mm)$) -- + ($(buddy.south west)+(-1mm,-1mm)$) -- cycle; + \end{pgfonlayer} +\end{tikzpicture} +\end{document} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index e6da60673..15ffe88d8 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -946,13 +946,24 @@ from the command-line, Python, or C++. :CUSTOM_ID: architecture :END: -The Spot project can be broken down into several main parts: +[[file:arch.png]] - - =libbddx=: a customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]], for manipulating [[#bdd][BDDs]]. - - =libspot=: the main library, containing a C++11 implementation of all the +The Spot project can be broken down into several parts, as shown +above. Orange boxes are C/C++ libraries. Red boxes are command-line +program. Blue boxes are Python-related. + + - =libbddx= is a customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]], for manipulating [[#bdd][BDDs]]. + - =libspot= is the main library, containing a C++11 implementation of all the data structures and algorithms. This depends on =libddx=. - - [[file:tools.org][command-line tools]]: built upon the =libspot= library, exporting some of its - features to shell users - - Python bindings for =libbddx= and =libspot=: those make it possible to write - python scripts for specific tasks, and allow interactive use of the library - via environments such a [[http://ipython.org][IPython/Jupyter]]. + - all the supplied [[file:tools.org][command-line tools]] are built upon the =libspot= + library, exporting some of its features to shell users + - =libspot-ltsmin= 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 + currently supports libraries generated from promela models using + 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=]] + for details. + - In addition to the C++11 API, we also provide Python bindings for + =libspot-ltsmin= and most of =libspot=. These are available by + importing =spot= or =spot.ltsmin=, and have readily usable in an + interactive environment such as the [[http://juptter.org][IPython/Jupyter]] notebook.