Commit 8edd0648 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* doc/tl/tl.tex: Convert to utf-8.

parent 2616ea7c
......@@ -2,7 +2,7 @@
\documentclass[a4paper,twoside,10pt,DIV=12]{scrreprt}
\usepackage[stretch=10]{microtype}
\usepackage[american]{babel}
\usepackage[latin1]{inputenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage[sc]{mathpazo}
......@@ -983,7 +983,7 @@ right & $\U,\,\W,\,\M,\,\R$
Beware that not all tools agree on the associativity of these
operators. For instance Spin, ltl2ba (same parser as spin), Wring,
psl2ba, Modella, and NuSMV all have $\U$ and $\R$ as left-associative,
while Goal (hence Bchi store), LTL2AUT, and LTL2Bchi (from
while Goal (hence Büchi store), LTL2AUT, and LTL2Büchi (from
JavaPathFinder) have $\U$ and $\R$ as right-associative. Vis and LBTT
have these two operators as non-associative (parentheses required).
Similarly the tools do not aggree on the associativity of $\IMPLIES$
......@@ -1137,13 +1137,13 @@ rules:
\node[align=center] (saf) at (1,1) {Safety\\ $\G p$};
\node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$};
\node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Bchi\\Automata};
\node[align=left,below right](weak) at (6.2,6.7) {Weak Bchi\\Automata};
\node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\Bchi\\Automata};
\node[align=left,above right](ter) at (6.2,1.7) {Terminal\\Bchi\\Automata};
\node[align=right,above left](occ) at (-.2,2) {Terminal\\co-Bchi\\Automata};
\node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Büchi\\Automata};
\node[align=left,below right](weak) at (6.2,6.7) {Weak Büchi\\Automata};
\node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\Büchi\\Automata};
\node[align=left,above right](ter) at (6.2,1.7) {Terminal\\Büchi\\Automata};
\node[align=right,above left](occ) at (-.2,2) {Terminal\\co-Büchi\\Automata};
\node[above right] (buc) at (3.35,7) {General Bchi Automata};
\node[above right] (buc) at (3.35,7) {General Büchi Automata};
\draw[annote] (rec) -- (det);
\draw[annote] (per) -- (weak);
......@@ -1961,4 +1961,5 @@ $f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g} & & &
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% coding: utf-8
%%% End:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment