alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: various improvements

Browse source 
* doc/org/spot.css: Improve style and responsiveness.
* doc/org/oaut.org, doc/org/ioltl.org: Fix some ugly outputs.
This commit is contained in:
Alexandre Duret-Lutz 2020-09-28 17:59:55 +02:00
parent 4ca2f394e4
commit 53a68f99f4
3 changed files with 48 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

3
doc/org/ioltl.org
View file

@ -71,8 +71,7 @@ instance =gfa= is an atomic proposition, but =GFa= actually denotes
the LTL formula =G(F(a))=. Any double-quoted string is also
considered to be an atomic proposition, so if =GFa= had to be an
atomic proposition, it could be written
#+HTML: <code>"GFa"</code>
.
@@html:<code>@@"GFa"@@html::</code>@@.
These double-quote strings also make it possible to embed arbitrarily
complex expressions that represent an atomic proposition that Spot

49
doc/org/oaut.org
View file

@ -14,7 +14,7 @@ are used to specify how to output of automata.
All tools that can output automata implement the following options:
#+BEGIN_SRC sh :exports results
ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
ltl2tgba --help | sed -n 's/ *$//g;/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
@ -26,25 +26,25 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
'unambiguous', 'stutter-invariant',
'stutter-sensitive-example', 'semi-determinism',
or 'strength'.
-d, --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#] GraphViz's format.
Add letters for (1) force numbered states, (a)
show acceptance condition (default), (A) hide
acceptance condition, (b) acceptance sets as
bullets, (B) bullets except for Büchi/co-Büchi
automata, (c) force circular nodes, (C) color
nodes with COLOR, (d) show origins when known, (e)
force elliptic nodes, (E) force rEctangular nodes,
(f(FONT)) use FONT, (g) hide edge labels, (h)
horizontal layout, (k) use state labels when
possible, (K) use transition labels (default), (n)
show name, (N) hide name, (o) ordered transitions,
(r) rainbow colors for acceptance sets, (R) color
acceptance sets by Inf/Fin, (s) with SCCs, (t)
force transition-based acceptance, (u) hide true
states, (v) vertical layout, (y) split universal
edges by color, (+INT) add INT to all set numbers,
(<INT) display at most INT states, (#) show
internal edge numbers
-d, --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#]
GraphViz's format. Add letters for (1) force
numbered states, (a) show acceptance condition
(default), (A) hide acceptance condition, (b)
acceptance sets as bullets, (B) bullets except for
Büchi/co-Büchi automata, (c) force circular
nodes, (C) color nodes with COLOR, (d) show
origins when known, (e) force elliptic nodes, (E)
force rEctangular nodes, (f(FONT)) use FONT, (g)
hide edge labels, (h) horizontal layout, (k) use
state labels when possible, (K) use transition
labels (default), (n) show name, (N) hide name,
(o) ordered transitions, (r) rainbow colors for
acceptance sets, (R) color acceptance sets by
Inf/Fin, (s) with SCCs, (t) force transition-based
acceptance, (u) hide true states, (v) vertical
layout, (y) split universal edges by color, (+INT)
add INT to all set numbers, (<INT) display at most
INT states, (#) show internal edge numbers
-H, --hoaf[=1.1|i|k|l|m|s|t|v] Output the automaton in HOA format
(default). Add letters to select (1.1) version
1.1 of the format, (i) use implicit labels for
@ -399,11 +399,9 @@ of Promela syntax.)
The =-d= or =--dot= option causes automata to be output in GraphViz's
format.
#+NAME: oaut-dot1
#+BEGIN_SRC sh :prologue export SPOT_DOTEXTRA= SPOT_DOTDEFAULT=
ltl2tgba '(Ga -> Gb) W c' -d
#+END_SRC
#+RESULTS: oaut-dot1
#+begin_example
digraph "(Gb | F!a) W c" {
rankdir=LR
@ -438,6 +436,11 @@ This output should be processed with =dot= to be converted into a
picture. For instance use =dot -Tpng= or =dot -Tpdf=. The pictures
on this page are produced with =dot -Tsvg=.
#+NAME: oaut-dot1
#+BEGIN_SRC sh :exports code :prologue export SPOT_DOTEXTRA= SPOT_DOTDEFAULT=
ltl2tgba '(Ga -> Gb) W c' -d | dot -Tsvg
#+END_SRC
#+BEGIN_SRC dot :file oaut-dot1.svg :var txt=oaut-dot1 :exports results
$txt
#+END_SRC
@ -445,6 +448,8 @@ $txt
#+RESULTS:
[[file:oaut-dot1.svg]]
However in this documentation simply omit the calls to =dot -Tsvg=.
** Customizing the dot output
This output can be customized by passing optional characters to the

30
doc/org/spot.css
View file

@ -2,20 +2,25 @@
a{color:inherit;background-color:inherit;font:inherit;text-decoration:inherit}
a:hover{text-decoration:underline}
/* http://paletton.com/#uid=33i0X0kz3BrkeHdpSD1C7r1FAlb */
body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em}
body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:90ch;margin:auto;padding:0 .5em}
body.man{padding:0 .5em 3em .5em}
body #content{padding-top:45px}
body pre{background:#fbfbfb;border:none;font-family:monospace, courier}
body code{font-weight:bold}
body a{color:#008181}
h1{display:block;width:calc(100% - 1em);position:relative;padding:.5em}
h1::before{content:"";position:absolute;z-index:-1;background-color:#ffe35e;left:0em;bottom:0em;width:100%;height:100%;border-radius:10px;transform:skew(10deg)}
#table-of-contents{font-size:80%;padding-left:0.5em;padding-right:0.5em;text-align:right;float:right;border-left:1px solid #ffd300;border-bottom:1px solid #ffd300;background:#ffe35e}
#table-of-contents ul{padding-left:1em}
#table-of-contents h2{font-size:100%;font-weight:normal;padding-left:0.5em;padding-right:0.5em;padding-top:0.05em;padding-bottom:0.05em}
#table-of-contents #text-table-of-contents{text-align:left}
#org-div-home-and-up{text-align:center;font-size:100%}
.outline-2 h2{border-bottom-style:solid;border-color:#ffe35e}
.outline-3 h3{position:relative;z-index:1}
.outline-3 h3:before{content:"";position:absolute;z-index:-1;left:-.2em;bottom:-.05em;height:1.2em;width:1.2em;background-color:#ffe35e;border-radius:5px}
.outline-2 h2{display:block;width:100%;position:relative}
.outline-2 h2::before{content:"";height:100%;width:calc(100% + 2em);position:absolute;z-index:-1;bottom:0em;left:-1em;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 50%,transparent 75%);transform:skew(10deg);border-radius:5px;}
.outline-3 h3{display:block;width:auto;position:relative}
.outline-3 h3::before{content:"";position:absolute;z-index:-1;width:calc(100% + 2em);height:100%;left:-1em;bottom:0em;;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 25%,transparent 50%);transform:skew(10deg);border-radius:3px}
.outline-2 h2:hover::before,.outline-3 h3:hover::before{background-color:#ffe35e}
pre{margin:1.2ex}
pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto;margin-top:0;margin-bottom:0}
pre.src-hoa{border-color:#d70079}
pre.example{border-left-style:solid;border-color:#d70079;margin-top:0;position:relative;z-index:2}
@ -23,16 +28,21 @@ div.org-src-container+pre.example{border-top-width:1px;border-top-color:#ddd;bor
div.org-src-container+div.org-src-container pre.src{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed}
div.org-src-container {margin-top:0;margin-bottom:0;position:relative;z-index:1}
pre.src-text{border-left-style:solid;border-color:#d70079}
pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
pre.src-python:before{content:'Python'}
pre.src-C\+\+:before{content:'C++'}
pre.src-hoa:before{content:'HOA';border-color:#d70079}
pre.src::before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
pre.src-python::before{content:'Python'}
pre.src-C\+\+::before{content:'C++'}
pre.src-hoa::before{content:'HOA';border-color:#d70079}
img{max-width:100%}
svg.org-svg{width:auto;max-width:100%}
table{margin-top:1em}
table.csv-table,table.table-pre{font-family:monospace, courier}
table.csv-table th{vertical-align:bottom}
table.csv-table th div{text-align:center}
table.csv-table th div span{text-align:left;writing-mode:vertical-lr;transform:rotate(180deg);display:inline-block;white-space:nowrap}
@media only screen and (max-width:100ch){
#spotlogo{display:none}
.outline-2 h2::before,.outline-3 h3::before,h1.title::before{transform:none;}
}
@media screen{
#table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10}
#table-of-contents #text-table-of-contents{display:none}
@ -66,9 +76,9 @@ thead tr{background:#ffe35e}
.org-hoa-header-lowercase{color:#00adad}
.org-hoa-ap-number{color:#d70079}
.implem{background:#fff0a6;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#ffe35e;border-style:solid none}
.implem:before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold}
.implem::before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold}
.caveat{background:#ef99c9;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#d70079;border-style:solid none}
.caveat:before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold}
.caveat::before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold}
.spotlogo{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogo}
g.spotlogobg{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogobg}
g#version{transform-origin:50% 50%;animation-duration:3s;animation-name:animspotlogover}