-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmanual.tex
213 lines (186 loc) · 12.2 KB
/
manual.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
\documentclass[english,paper=a4,final]{article}
\usepackage{uppaal}
\usepackage{hyperref}
\usepackage{booktabs}
\usepackage{hyphenat}
\hyphenation{spe-ci-fy}
\title{\LaTeX{} Style for \uppaal Models}
%\date{}
\author{Marius Miku\v{c}ionis \\ {\ttfamily [email protected]}}
\newcommand{\cmdbf}[1]{{\bfseries \textbackslash#1}}
\newcommand{\cmdtt}[1]{{\ttfamily \textbackslash#1}}
\begin{document}
\maketitle
\section{Introduction}
The intent of this manual is to document the features of {\ttfamily uppaal.sty} \LaTeX{} style package.
The {\ttfamily uppaal.sty} package has been developed over many years of publishing papers related to \uppaal.
The initial intent was to gather common definitions used throughout papers.
The common definitions outgrew into package and finally became a piece of software it is now.
\subsection{Example}
Listing~\ref{lst:example1} shows the simplest \LaTeX{} code to typeset \uppaal code:
\lstinputlisting[caption={The simplest \uppaal typesetting in \LaTeX{}.},
label={lst:example1},
language={tex}, keywords={begin,end,caption,label,language},
basicstyle=\uppPlainStyle,frameshape={RYR}{y}{y}{RYR},
numbers=left,numberstyle=\tiny,numbersep=3mm,xleftmargin=5mm]{example1.tex}
The result is the following minimalistic listing:
\input{example1}
Listing~\ref{lst:example2} shows the same listing with customized {\bfseries uppaalcode} environment.
\lstinputlisting[language={tex},caption={\LaTeX{} code.},
language={tex},keywords={begin,end,caption,label,language,captionpos,float,frameshape,frame,rulesepcolor,numbers,numberstyle,numbersep,xleftmargin,xrightmargin},
basicstyle=\uppPlainStyle,frameshape={RYR}{y}{y}{RYR},float={!b},
numbers=left,numberstyle=\tiny,numbersep=3mm,xleftmargin=5mm]{example2.tex}
\input{example2}
Properties can also be typeset as inline code using Listing~\ref{lst:props}:\\
\begin{table}
\centering
\caption{Query text embedded into table.}
\input{props}
\end{table}
\lstinputlisting[language={tex},caption={\LaTeX{} code for queries in a table.},label={lst:props},
language={tex}, keywords={begin,end,caption,label,language,captionpos,float,frameshape,frame,rulesepcolor,numbers,numberstyle,numbersep,xleftmargin,xrightmargin},
basicstyle=\uppPlainStyle,frameshape={RYR}{y}{y}{RYR},float,
numbers=left,numberstyle=\tiny,numbersep=3mm,xleftmargin=5mm]{props.tex}
\subsection{Installation Dependencies}
The style package depends on the following \LaTeX{} packages:
\begin{description}
\item[listings] -- to implement the actual \href{https://www.ctan.org/pkg/listings}{listings} typesetting.
\item[xcolor] -- to define and customize colors.
\item[xspace] -- to omit trailing space for tool names.
\item[beramono] -- \href{http://www.tug.dk/FontCatalogue/beramono/}{Bitstream Vera Mono} fonts, the directory is usually called {\ttfamily bera} and the font files are prefixed with {\ttfamily fvm}.
\end{description}
The packages above are common and usually distributed by \href{https://www.tug.org/texlive/}{TeXLive} and \href{https://miktex.org/}{MikTex}.
For example, Debian GNU/Linux puts them into {\ttfamily texlive-latex-recommended}, {\ttfamily texlive-latex-recommended-doc} and {\ttfamily texlive-fonts-extra} packages.
\section{Package Options}
None is implemented. It would be nice to turn on and off the coloring to gray scale printing, change the typewriter fonts as some proceedings demand using their own.
\section{Environments}
The {\ttfamily uppaal.sty} defines \uppaal language styles for {\ttfamily listings.sty} package, thus all the hard lifting is done by {\ttfamily listings.sty} and the details can be found in {\bfseries listings} documentation.
\begin{description}
\item[lstlisting] environment is the way to typeset any listing, and one needs to specify {\ttfamily language=\{[GUI]Uppaal\}} parameter to turn on syntax highlighting similar to \uppaal editor.
\item[uppaalcode] environment is a shorthand to {\bfseries lstlisting} environment with the language predefined to {\ttfamily [GUI]Uppaal}.
\end{description}
Here is the list of commonly used parameters used to customize the listing:
\begin{description}
\item[language] the style package defines the following \uppaal code variants:
\begin{description}
\item[{\ttfamily Uppaal}] basic \uppaal keywords and font styles for them, only slanting and bold is used, no colors.
\item[{\ttfamily [GUI]Uppaal}] the same font styles as above plus colors similar to \uppaal editor.
\item[{\ttfamily [LIT]Uppaal}] the same features as above except some characters are replaced by mathematical notation.
\end{description}
\item[caption] specifies the text title for the listing.
\item[captionpos] specifies the placemant of the caption relative to the listing, possible values: {\ttfamily t} -- at the top (default), and {\ttfamily b} -- at the bottom.
\item[label] defines a label to refered to by the {\ttfamily \textbackslash ref} command. {\ttfamily lst:} prefix can be useful to distinguish listings from figures and other floats.
\item[float] specifies that the listing must be treated as a float, i.e. the layout must into onto one page and it cannot be broken by a page break.
\item[numbers] adds a number column on the left or right, possible values: {\ttfamily none} (default), {\ttfamily left}, {\ttfamily right}.
\item[numberstyle] specifies the style for numbers, e.g. {\ttfamily \textbackslash tiny}.
\item[numbersep] specifies the space size between numbers and listing.
\item[xleftmargin] specifies the size of the left margin.
\item[frame] draws some frame elements around the listing, possible values: {\ttfamily none} (default), {\ttfamily leftline}, {\ttfamily topline}, {\ttfamily bottomline}, {\ttfamily lines} (top and bottom), {\ttfamily single} (whole frame), {\ttfamily shadowbox} or a subset of {\ttfamily trblTRBL} characters where upper case denotes double lines.
\item[frameround]
\end{description}
There are are many many more options, please see the documentation for {\ttfamily listings.sty} package.
It also plays nicely with {\ttfamily tcolorbox} package for fancy listings in {\ttfamily beamer} presentations.
\section{Inlining \uppaal Code}
Apart from explicit listings \uppaal code can also be typeset inside regular text flow using style similar to the default scheme in \uppaal graphical user interface.
Table~\ref{tab:commands} shows a list of available commands.
\begin{table}[ht]
\caption{List of supported \LaTeX{} commands.}
\label{tab:commands}
\begin{tabular}{@{}l@{ }l@{ }l@{}}
\toprule
{\bfseries Description } & {\bfseries Example} & {\bfseries Result} \\
\midrule
\multicolumn{3}{@{}l}{Labels associated with {\bfseries locations}:} \\
Location name & \cmdtt{uppLoc\{Done\}} & \uppLoc{Done} \\
Invariant expression & \cmdtt{uppInv\{x$<=$7 \&\& y'==0\}} & \uppInv{x<=7 && y'==0} \\
Exponential rate expr. & \cmdtt{uppRate\{1:7\}} & \uppRate{1:7} \\
\midrule
\multicolumn{3}{@{}l}{Labels associated with {\bfseries edges}:} \\
Select statement & \cmdtt{uppSelect\{i:int[1,7]\}} & \uppSelect{i:int[1,7]} \\
Guard expression & \cmdtt{uppGuard\{x$>=$3\}} & \uppGuard{x>=3} \\
Plain synchronization & \cmdtt{uppSync\{message!\}} & \uppSync{message!} \\
Input synchronization & \cmdtt{uppIn\{message\}} & \uppIn{message} \\
Output synchronization & \cmdtt{uppOut\{message\}} & \uppOut{message} \\
Update statement & \cmdtt{uppUpdate\{x=5,y=7\}} & \uppUpdate{x=5,y=7} \\
Weight expression & \cmdtt{uppWeight\{i*10\}} & \uppWeight{i*10} \\
\midrule
\multicolumn{3}{@{}l}{Variable and type names from {\bfseries declarations}:} \\
Variable name & \cmdtt{uppVar\{count\}} & \uppVar{count} \\
Constant name & \cmdtt{uppConst\{MAX\_N\}} & \uppConst{MAX_N} \\
Clock name & \cmdtt{uppClock\{time\}} & \uppClock{time} \\
Channel name & \cmdtt{uppChan\{message\}} & \uppChan{message} \\
Type name & \cmdtt{uppType\{int32\_t\}} & \uppType{int32_t} \\
Function name & \cmdtt{uppFunc\{enqueue()\}} & \uppFunc{enqueue()} \\
Template name & \cmdtt{uppTemp\{Train\}} & \uppTemp{Train} \\
Process name & \cmdtt{uppProc\{Train(3)\}}& \uppProc{Train(3)} \\
\midrule
\multicolumn{3}{@{}l}{Properties and queries from {\bfseries verifier}:} \\
Any property text & \cmdtt{uppProp\{E$<>$ deadlock\}} & \uppProp{E<> deadlock} \\
Exists path with Future & \cmdtt{uppEF\{deadlock\}} & \uppEF{deadlock}\\
Exists path with Global & \cmdtt{uppEG\{counter$<=$9\}} & \uppEG{counter<=9} \\
All paths with Future & \cmdtt{uppAF\{counter$<=$9\}} & \uppAF{counter<=9} \\
All paths with Global & \cmdtt{uppAG\{counter$<=$9\}} & \uppAG{counter<=9} \\
Estimate probability & \cmdtt{uppPr\{[$<=7$]($<>$ done)\}} & \uppPr{[<=7](<> done)}\\
Probability of Future & \cmdtt{uppPrF\{$<=7$\}\{done\}} & \uppPrF{<=7}{done} \\
Probability of Global & \cmdtt{uppPrG\{$<=7$\}\{good\}} & \uppPrG{<=7}{good} \\
Simulate and project & \cmdtt{uppSim\{5\}\{$<=7$\}\{x,y\}} & \uppSim{5}{<=7}{x,y} \\
Simulate with check & \cmdtt{uppSimC\{5\}\{$<=7$\}\{x\}\{3\}\{done\}} & \uppSimC{5}{<=7}{x}{3}{done} \\
\midrule
\multicolumn{3}{@{}l}{Tool names:} \\
\uppaal & \cmdtt{uppaal} & \uppaal \\
\uppaaltron & \cmdtt{uppaaltron} & \uppaaltron \\
\uppaaltiga & \cmdtt{uppaaltiga} & \uppaaltiga \\
\uppaalsmc & \cmdtt{uppaalsmc} & \uppaalsmc \\
\stratego & \cmdtt{stratego} & \stratego \\
\bottomrule
\end{tabular}
\end{table}
\section{Colors and Styles}
Table~\ref{tab:colors} enumerates the colors and styles which can be customized.
\begin{table}[ht]
\caption{Color definitions.}\label{tab:colors}
\centering
\setlength{\fboxsep}{0pt}
\begin{tabular}{llc@{, }c@{, }cc}
\toprule
{\bfseries Color} & {\bfseries Name} & \multicolumn{3}{c}{\bfseries RGB} & {\bfseries Sample} \\
\midrule
\cmdtt{uppCommentColor} & darker red & 0.4 & 0 & 0 & \fbox{\color{uppCommentColor}\rule{10mm}{3mm}} \\
\cmdtt{uppKeywordColor} & dark green & 0 & 0.4 & 0 & \fbox{\color{uppKeywordColor}\rule{10mm}{3mm}} \\
\cmdtt{uppTypeColor} & darker green & 0 & 0.3 & 0 & \fbox{\color{uppTypeColor}\rule{10mm}{3mm}} \\
\midrule
\cmdtt{uppLocColor} & dark red & 0.5 & 0 & 0 & \fbox{\color{uppLocColor}\rule{10mm}{3mm}} \\
\cmdtt{uppInvColor} & dark magenta & 0.4 & 0 & 0.4 & \fbox{\color{uppInvColor}\rule{10mm}{3mm}} \\
\cmdtt{uppRateColor} & pink & 0.875 & 0.25 & 0.5 & \fbox{\color{uppRateColor}\rule{10mm}{3mm}} \\
\cmdtt{uppSelectColor} & dark yellow & 0.4 & 0.4 & 0 & \fbox{\color{uppSelectColor}\rule{10mm}{3mm}} \\
\cmdtt{uppGuardColor} & dark green & 0 & 0.3 & 0 & \fbox{\color{uppGuardColor}\rule{10mm}{3mm}} \\
\cmdtt{uppSyncColor} & dark cyan & 0 & 0.4 & 0.4 & \fbox{\color{uppSyncColor}\rule{10mm}{3mm}} \\
\cmdtt{uppUpdateColor} & dark blue & 0 & 0 & 0.4 & \fbox{\color{uppUpdateColor}\rule{10mm}{3mm}} \\
\cmdtt{uppWeightColor} & dark orange & 0.4 & 0.2 & 0 & \fbox{\color{uppWeightColor}\rule{10mm}{3mm}} \\
\bottomrule
\end{tabular}
\end{table}
\begin{table}[ht]
\caption{Style definitions.}\label{tab:styles}
\begin{tabular}{llll}
\toprule
{\bfseries Style} & {\bfseries Definition} & {\bfseries Purpose} & {\bfseries Sample} \\
\midrule
\cmdbf{uppBasicStyle} & \cmdtt{uppPlainStyle} & basic text & {\uppBasicStyle text} \\
\cmdbf{uppKeywordStyle}& \cmdtt{uppBfStyle} & keywords & {\uppKeywordStyle return} \\
\cmdbf{uppTypeStyle} & \cmdtt{uppBfStyle} & type names & {\uppTypeStyle clock} \\
\cmdbf{uppConstStyle} & \cmdtt{uppBfStyle} & constant names & {\uppConstStyle true} \\
\cmdbf{uppFuncStyle} & \cmdtt{uppSlStyle} & function names & {\uppFuncStyle sin} \\
\cmdbf{uppCommentStyle}& \cmdtt{uppSlStyle} & simple comment & {\uppCommentStyle comment} \\
\cmdbf{uppFCommentStyle}&\cmdtt{uppSlBfStyle}& fancy comment & {\uppFCommentStyle comment} \\
\midrule
\cmdbf{uppPlainStyle} & (plain font) & plain text & {\uppPlainStyle text} \\
\cmdbf{uppBfStyle} & \cmdtt{bfseries} & bold text & {\uppBfStyle text} \\
\cmdbf{uppSlStyle} & \cmdtt{slshape} & slanted text & {\uppSlStyle text} \\
\cmdbf{uppSlBfStyle} & \cmdtt{slshape}\cmdtt{bfseries} & slanted bold text & {\uppSlBfStyle text} \\
\bottomrule
\end{tabular}
\end{table}
\section*{Acknowledgements}
I thank my colleagues for testing and suggesting: Brian~Nielsen, Ulrik~Nyman, Danny~B.~Poulsen, and others.
\end{document}