diff --git a/doc/org/arch.tex b/doc/org/arch.tex index 4c346efbd..0e9e97e4a 100644 --- a/doc/org/arch.tex +++ b/doc/org/arch.tex @@ -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] diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 2402f8b13..05cc91863 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -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: