diff --git a/content/applying-automata-learning.tex b/content/applying-automata-learning.tex index cd280de..ba0fb68 100644 --- a/content/applying-automata-learning.tex +++ b/content/applying-automata-learning.tex @@ -164,7 +164,6 @@ Other products can be connected to an engine that pre- or postprocess the paper, \node at (es.north) [rounded corners, fill=black!10] {Engine Software}; \stopscope \stoptikzpicture} -%\externalfigure[ESRAOverview.pdf][width=0.5\textwidth] \stopplacefigure \in{Figure}[fig:esra-overview] gives an overview of the software in a printer or copier. @@ -267,7 +266,64 @@ These messages are placed in a queue to be processed later. \startplacefigure [title={Top states and transitions of the ESM.}, reference=fig:esm-states] -\externalfigure[ESMStates.pdf][width=\textwidth] +\hbox{\switchtobodyfont[small]\starttikzpicture + [comp/.style={draw, rounded corners, minimum width=1.7cm, minimum height=0.6cm, inner sep=2pt}, + grco/.style={comp, fill=black!10}, + conn/.style={->, shorten >=1pt}, + dot/.style={fill, circle}, + x=1.4cm, y=-0.45cm] +\forgetall +\node[dot, inner sep=2.5pt] at ( 0, 0) (init) {}; +\node[comp] at ( 0, 2) (startup) {startup}; +\node[grco] at ( 0, 4) (idle) {idle}; +\node[comp] at ( 1, 6) (goingToStandby) {goingToStandby}; +\node[grco] at ( 0, 8) (standby) {standby}; +\node[comp] at (-1, 6) (resetting) {resetting}; +\node[comp] at (-1,10) (starting) {starting}; +\node[grco] at ( 0,12) (running) {running}; +\node[grco] at ( 1,10) (stopping) {stopping}; +\node[grco] at (-2.5, 8) (medium) {medium}; +\node[comp] at ( 3, 8) (goingToLowPower) {goingToLowPower}; +\node[comp] at ( 3, 6) (lowPower) {lowPower}; +\node[comp] at ( 1.75, 2) (awakening) {awakening}; +\node[grco] at ( 3.25, 0) (defect) {defect}; +\node[grco] at ( 3.25, 2) (sleep) {sleep}; +\node[comp] at ( 4.75, 0) (goingToDefect) {goingToDefect}; +\node[comp] at ( 4.75, 2) (goingToSleep) {goingToSleep}; +\node[dot, inner sep=2pt] at ( 3.25, 4) (off0) {}; +\node[draw, circle, inner sep=3pt] at (off0) (off) {}; + +\path[conn] + (init) edge node[right]{power on} (startup) + (startup) edge (idle) + (idle) edge (goingToStandby) + (goingToStandby) edge (resetting) + (goingToStandby) edge (standby) + (standby) edge (resetting) + (standby) edge (goingToLowPower) + (standby) edge (starting) + (resetting) edge (idle) + (starting) edge (running) + (running) edge (stopping) + (stopping) edge (starting) + (stopping) edge (standby) + (goingToLowPower) edge (lowPower) + (lowPower) edge (goingToStandby) + (awakening) edge (idle) + (defect) edge (sleep) + (sleep) edge (awakening) + (sleep) edge node[right]{power off} (off) + (goingToDefect) edge (defect) + (goingToSleep) edge (sleep); +\draw[conn, <->, shorten <=1pt] (standby) -- (medium); +\draw[conn, <->, shorten <=1pt] (medium) -- (-2.5, 4) -- (idle); + +\node[draw, rounded corners, fit=(medium) (init) (goingToDefect) (running), inner sep=10pt] (outer) {}; + +\draw + (goingToDefect -| outer.east) edge[conn] (goingToDefect) + (goingToSleep -| outer.east) edge[conn] (goingToSleep); +\stoptikzpicture} \stopplacefigure \in{Figure}[fig:esm-states] shows the top states of the ESM statechart. @@ -493,7 +549,28 @@ In the end we decided to implement the required model transformations ourselves. \startplacefigure [title={Formats for representing models and transformations between formats.}, reference=fig:formats] -\externalfigure[formats.pdf][width=0.7\textwidth] +\hbox{\switchtobodyfont[small]\starttikzpicture + [ format/.style={tape, draw, tape bend top=none, tape bend bottom=out and in, align=right, text width=1.8cm, minimum width=1.8cm, minimum height=1.2cm}, + lab/.style={above, anchor=south west}, + x=3.5cm, y=-1cm ] +\forgetall +\node[format] at (0, 0) (rrrt) {\rightaligned{UML\\statechart}}; +\node[lab] at (rrrt.north west) {RRRT}; +\node[format] at (1, 0) (papyrus) {HEFSM}; +\node[lab] at (papyrus.north west) {PapyrusUML}; +\node[format] at (2, 0) (uppaal) {\rightaligned{RFSM\\.xml}}; +\node[lab] at (uppaal.north west) {Uppaal}; +\node[format] at (1, 2) (learnlib) {\rightaligned{Mealy\\Machine\\.dot}}; +\node[lab] at (learnlib.north west) {LearnLib}; +\node[format] at (2, 2) (cadp) {LTS}; +\node[lab] at (cadp.north west) {CADP}; + +\path + (rrrt) edge[->] (papyrus) + (papyrus) edge[->] (uppaal) + (uppaal) edge[->] (cadp) + (learnlib) edge[->] (cadp); +\stoptikzpicture} \stopplacefigure We used the bisimulation checker of CADP by \citet[GaravelLMS11] to check the equivalence of labelled transition system models in {\tt .aut} format. diff --git a/environment/tikz.tex b/environment/tikz.tex index 6e997ca..7142e5f 100644 --- a/environment/tikz.tex +++ b/environment/tikz.tex @@ -1,7 +1,7 @@ \startenvironment tikz \usemodule[tikz] -\usetikzlibrary[automata, arrows, positioning, matrix, fit, decorations.pathreplacing, shapes.geometric, shadows, backgrounds] +\usetikzlibrary[automata, arrows, positioning, matrix, fit, decorations.pathreplacing, shapes.geometric, shapes.symbols, shadows, backgrounds] \usemodule[pgfplots]