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

org: syntax-highlight the HOA outputs

Browse source 
* elisp/hoa-mode.el, elisp/Makefile.am, elisp/README: New files.
* debian/copyright, configure.ac, README, Makefile.am: Adjust.
* doc/org/init.el.in: Adjust to load hoa-mode.el.
* doc/org/spot.css: Add entries for HOA mode.
* doc/org/hoa.org, doc/org/ltldo.org, doc/org/oaut.org,
doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org,
doc/org/tut30.org: Make the HOA outputs as HOA.
This commit is contained in:
Alexandre Duret-Lutz 2015-11-20 14:28:51 +01:00
parent d46da963d5
commit 5aba246ff0
16 changed files with 449 additions and 132 deletions
Download patch file Download diff file Expand all files Collapse all files

6
Makefile.am
View file

@ -21,14 +21,14 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>.
if NEVER
# For Automake a conditional directory
# For Automake a, conditional directory
# is conditionally built, but unconditionally distributed.
# So using NEVER here ensures that `make all' will not
# recurse in bench/, but `make dist' will.
NEVER_BENCH = bench
NEVER_SUBDIRS = bench elisp
endif
SUBDIRS = buddy lib src wrap ltdl iface doc $(NEVER_BENCH)
SUBDIRS = buddy lib src wrap ltdl iface doc $(NEVER_SUBDIRS)
UTF8 = utf8/doc/ReleaseNotes utf8/doc/utf8cpp.html utf8/utf8.h \
utf8/utf8/checked.h utf8/utf8/core.h utf8/utf8/unchecked.h

1
README
View file

@ -180,6 +180,7 @@ buddy/ A customized version of BuDDy 2.3 (a BDD library).
ltdl/ Libtool's portable dlopen() wrapper library.
lib/ Gnulib's portability modules.
utf8/ Nemanja Trifunovic's utf-8 routines.
elisp/ Related emacs modes, used for building the documentation.
Build-system stuff
------------------

1
configure.ac
View file

@ -197,6 +197,7 @@ AC_CONFIG_FILES([
doc/tl/Makefile
doc/org/.dir-locals.el
doc/org/init.el
elisp/Makefile
iface/ltsmin/defs
iface/ltsmin/Makefile
iface/Makefile

19
debian/copyright vendored
View file

@ -125,6 +125,25 @@ Copyright: (unknown) D A Gwyn
License: public-domain
(Mostly) portable public-domain implementation -- D A Gwyn
Files: elisp/hoa-mode.el
Copyright: 2015 Alexandre Duret-Lutz
License: GPL-3+
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3 of the License, or
(at your option) any later version.
.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
.
On Debian systems, the complete text of the GNU General
Public License version 3 can be found in "/usr/share/common-licenses/GPL-3".
Files: debian/*
Copyright: 2015 Laboratoire de Recherche et Développement de l'Epita (LRDE)
License: GPL-3+

108
doc/org/hoa.org
View file

@ -139,12 +139,12 @@ EOF
#+RESULTS:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
sed -n '/--BODY/,/--END/p' stvstracc.hoa | grep -v -- --
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
/* state-based acceptance */
State: 0 {0 1}
[0&!1] 0
@ -158,16 +158,16 @@ State: 1 {0}
State: 2
[!0] 1 {0}
[0] 2 {1}
#+end_example
#+END_SRC
will always be stored as a TωA with this transition structure:
#+BEGIN_SRC sh :results verbatim :exports results
#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
autfilt -Ht stvstracc.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
State: 0
[0&!1] 0 {0 1}
[0&1] 1 {0 1}
@ -178,7 +178,7 @@ State: 1
State: 2
[!0] 1 {0}
[0] 2 {1}
#+end_example
#+END_SRC
#+BEGIN_SRC sh :results silent :exports results
rm -f stvstracc.hoa
@ -201,8 +201,8 @@ For instance in the following automaton, the outgoing transitions of
each states belong to the same sets:
#+NAME: state-based-example
#+BEGIN_SRC sh :results verbatim :exports both
cat >sba.hoa <<EOF
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
cat >sba.hoa <<EOF_HOA
HOA: v1
States: 3
Start: 0
@ -220,14 +220,14 @@ State: 2
[!0] 1 {0 1}
[0] 2 {0 1}
--END--
EOF
EOF_HOA
autfilt -H sba.hoa
#+END_SRC
so the HOA output of =autfilt= automatically uses state-based acceptance:
#+RESULTS: state-based-example
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
@ -247,7 +247,7 @@ State: 2 {0 1}
[!0] 1
[0] 2
--END--
#+end_example
#+END_SRC
The rational for this automatic switch to state-based acceptance is as follows:
- Tools that support transition-based acceptance can easily see
@ -265,12 +265,12 @@ Nevertheless, should you really insist on having an output with
transition-based acceptance, you can do so by passing the option =t=
to the HOA printer:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -Ht sba.hoa
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
@ -290,7 +290,7 @@ State: 2
[!0] 1 {0 1}
[0] 2 {0 1}
--END--
#+end_example
#+END_SRC
#+BEGIN_SRC sh :results silent :exports results
rm sba.hoa
@ -302,12 +302,12 @@ format to prevents mixing the two: if you use =-Hm=, the decision of
using state or transition-based acceptance will be made for each state
separately. For instance:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -Hm 'GFa | Fb'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "F(b | GFa)"
States: 3
@ -327,7 +327,7 @@ State: 2
[1] 2 {0}
[!1] 2
--END--
#+end_example
#+END_SRC
So far we have discussed transforming state-based acceptance into
@ -342,12 +342,12 @@ when necessary. Most tools have a =-S= option (or
=--state-based-acceptance=) for this purpose. Compare the following
output with the previous one.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -S -Hm 'GFa | Fb'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "F(b | GFa)"
States: 4
@ -370,7 +370,7 @@ State: 3
[1] 2
[!1] 3
--END--
#+end_example
#+END_SRC
** Generic acceptance
@ -431,7 +431,7 @@ In the following example, you can see =autfilt= removing the duplicate
Rabin pair, and reordering the remaining pair to fit the syntax
corresponding to =Rabin 1=.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -H <<EOF
HOA: v1
States: 3
@ -454,7 +454,7 @@ EOF
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
@ -474,9 +474,7 @@ State: 2 {0 1}
[!0] 1
[0] 2
--END--
#+end_example
#+END_SRC
Internally, the acceptance condition is stored as an array in reverse
polish notation, and the primitives =Inf= and =Fin= are actually
@ -500,12 +498,14 @@ When you look at an acceptance condition output by Spot, you can
actually spot the terms that have been grouped together internally by
looking at the spacing around operators =&= and =|=. For instance:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
randaut -A"Fin(0)|Fin(1)|Fin(2)&Fin(3)&Inf(4)&Inf(5)" -H 0 | grep Acceptance:
#+END_SRC
#+RESULTS:
: Acceptance: 6 (Fin(0)|Fin(1)) | (Fin(2) & Fin(3) & (Inf(4)&Inf(5)))
#+BEGIN_SRC hoa
Acceptance: 6 (Fin(0)|Fin(1)) | (Fin(2) & Fin(3) & (Inf(4)&Inf(5)))
#+END_SRC
Here =Fin(0)|Fin(1)= is actually a single internal term =Fin({0,1})=,
and likewise for =Inf(4)&Inf(5)=.
@ -611,7 +611,7 @@ They are currently two named properties related to the HOA format.
You can see these properties being preserved when an automaton is read and then immediately output:
#+NAME: hello-world
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
cat >hw.hoa <<EOF
HOA: v1
name: "hello world!"
@ -636,7 +636,7 @@ autfilt -H hw.hoa
#+END_SRC
#+RESULTS: hello-world
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "hello world!"
States: 3
@ -657,7 +657,7 @@ State: 2 "so am I" {0 1}
[!0] 1
[0] 2
--END--
#+end_example
#+END_SRC
However if =autfilt= performs some transformation, and actually has to
construct a new automaton, those properties will not be quarried over
@ -670,32 +670,32 @@ the old states and the new ones.
Here is for instance the result when =autfilt= is instructed to
simplify the automaton:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -H --small hw.hoa
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0&!1] 0
[0&1] 1 {0}
[!0] 2 {0}
[0&1] 1
[!0] 2
State: 1
[0&!1] 1
[0&1] 2
State: 2
[!0] 1 {0}
[0] 2 {0}
State: 2 {0}
[!0] 1
[0] 2
--END--
#+end_example
#+END_SRC
Note that if the name of the automaton is important to you, it can be
@ -703,12 +703,12 @@ fixed via the =--name= option. For instance =--name=%M= will
construct the new name by simply copying the one of the original
automaton.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -H --small hw.hoa --name=%M
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "hello world!"
States: 3
@ -716,20 +716,20 @@ Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0&!1] 0
[0&1] 1 {0}
[!0] 2 {0}
[0&1] 1
[!0] 2
State: 1
[0&!1] 1
[0&1] 2
State: 2
[!0] 1 {0}
[0] 2 {0}
State: 2 {0}
[!0] 1
[0] 2
--END--
#+end_example
#+END_SRC
The page about [[file:oaut.org][common output option for automata]] has a section showing
how =--name= can be used to construct complex pipelines with automata that
@ -748,12 +748,12 @@ in the HOA format, and then read those automata with =autfilt= to
randomize the order of their transitions and states before printing
them in HOA format.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
genltl --and-gf=1..3 | ltl2tgba -B -F- -H | autfilt --randomize -H
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "GFp1"
States: 2
@ -762,7 +762,7 @@ AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 1
@ -779,7 +779,7 @@ AP: 2 "p1" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
properties: deterministic stutter-invariant
--BODY--
State: 0
[!0&1] 2
@ -801,7 +801,7 @@ AP: 3 "p1" "p2" "p3"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
properties: deterministic stutter-invariant
--BODY--
State: 0
[!2] 0
@ -821,7 +821,7 @@ State: 3
[0] 1
[!0] 3
--END--
#+end_example
#+END_SRC
It should be noted that the HOA parser is less efficient when it reads

8
doc/org/init.el.in
View file

@ -1,8 +1,12 @@
;; htmlize is not always in the load-path. On Debian it can be found here.
(setq load-path (cons "/usr/share/emacs/site-lisp/emacs-goodies-el" load-path))
(setq load-path (append '("@abs_top_srcdir@/elisp/" ; for hoa-mode.el
;; htmlize is not always in the load-path.
;; On Debian it can be found here.
"/usr/share/emacs/site-lisp/emacs-goodies-el")
load-path))
(or (require 'org-publish nil t) ; Org 7
(require 'ox-publish)) ; Org 8
(require 'org-install)
(require 'hoa-mode)
(print (concat "Org " (org-version)))
(setq org-export-htmlize-output-type 'css)

29
doc/org/ltldo.org
View file

@ -128,19 +128,20 @@ Here is another example, where we use Spin to produce two automata in
the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, but =ltldo= simply
converts the never claim produced by =spin= into this format.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltldo -f a -f GFa 'spin -f %s>%O' -H
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
--BODY--
State: 0 {0}
[0] 1
@ -161,7 +162,7 @@ State: 0
State: 1 {0}
[t] 0
--END--
#+end_example
#+END_SRC
Again, using the shorthands defined below, the previous command can be
simplified to just this:
@ -405,34 +406,35 @@ an LTL formula). In the following example, you can see that the
automaton uses the atomic proposition =Error=, but its name contains a
reference to =p0=.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltldo 'ltl3ba -H' -f '[]!Error' -H
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "BA for ([](!(p0)))"
name: "BA for [](!(p0))"
States: 1
Start: 0
AP: 1 "Error"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
--BODY--
State: 0 "accept_init" {0}
[!0] 0
--END--
#+end_example
#+END_SRC
If this is a problem, you can always force a new name with the
=--name= option:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltldo 'ltl3ba -H' -f '[]!Error' -H --name='BA for %f'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "BA for []!Error"
States: 1
@ -440,12 +442,13 @@ Start: 0
AP: 1 "Error"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
--BODY--
State: 0 "accept_init" {0}
[!0] 0
--END--
#+end_example
#+END_SRC
* Controlling and measuring time

40
doc/org/oaut.org
View file

@ -71,11 +71,11 @@ format can be found on a [[file:hoa.org][separate page]].)
Here is an example where [[file:ltl2tgba.org][=ltl2tgba=]] is used to construct two automata:
one for =a U b= and one for =(Ga -> Gb) W c=.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -H 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "a U b"
States: 2
@ -84,6 +84,7 @@ AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
@ -98,7 +99,7 @@ Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[0] 0 {0}
@ -118,7 +119,7 @@ State: 4
[!1] 3
[1] 4
--END--
#+end_example
#+END_SRC
The above output contains two automata, named after the formulas they
represent. Here is a picture of these two automata:
@ -301,36 +302,37 @@ to use state-based acceptance whenever possible. Option =t= forces
transition-based acceptance. For instance compare this output to the
previous one:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -Ht 'a U b'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "a U b"
States: 2
Start: 0
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
[1] 1
[0&!1] 0
[t] 0 {0}
State: 1
[t] 1 {0}
[1] 0
[0&!1] 1
--END--
#+end_example
#+END_SRC
Option =m= uses mixed acceptance, i.e, some states might use
state-based acceptance while other will not:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -Hm '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "(Gb | F!a) W c"
States: 5
@ -338,7 +340,7 @@ Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels
properties: trans-labels explicit-labels stutter-invariant
--BODY--
State: 0 {0}
[0] 0
@ -358,7 +360,7 @@ State: 4
[!1] 3
[1] 4
--END--
#+end_example
#+END_SRC
It is also possible to output each automaton on a single line, in case
@ -366,12 +368,14 @@ the result should be used with line-based tools or embedded into a CSV
file... Here is an example using both transition-based acceptance,
and single-line output:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -Htl 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
: HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [t] 0 {0} State: 1 [1] 0 [0&!1] 1 --END--
: HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--
#+BEGIN_SRC hoa
HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic stutter-invariant terminal --BODY-- State: 0 [t] 0 {0} State: 1 [1] 0 [0&!1] 1 --END--
HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc stutter-invariant --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--
#+END_SRC
* LBTT output

11
doc/org/spot.css
View file

@ -18,8 +18,10 @@ body a{color:#008181}
div#postamble{visibility:hidden}
.outline-2 h2{border-bottom-style:solid;border-color:#ffe35e}
pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto}
pre.src-hoa{padding-top:8px;border-left-style:solid;border-color:#d70079;overflow:auto}
pre.example{border-left-style:solid;border-color:#d70079}
pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad}
pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
pre.src-hoa:before{content:'HOA';border:none;border-bottom-style:solid;border-color:#d70079;overflow:auto}
img{max-width:100%}
@media screen{
#table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10}
@ -34,7 +36,14 @@ img{max-width:100%}
.org-builtin{font-weight:bold}
.org-preprocessor{font-weight:bold}
.org-string{font-weight:bold;color:#00adad}
.src-hoa .org-string{font-weight:bold;color:#d70079}
.org-function-name{font-weight:bold;color:#d70079}
.org-type{font-weight:bold;color:#00adad}
.org-comment-delimiter{font-weight:bold;color:#a13672}
.org-comment{font-style:italic;color:#a13672}
.org-hoa-keyword{font-weight:bold}
.org-hoa-builtin{font-weight:bold}
.org-hoa-acceptance-set{font-weight:bold}
.org-hoa-header-uppercase{font-weight:bold;color:#00adad}
.org-hoa-header-lowercase{color:#00adad}
.org-hoa-ap-number{color:#d70079}

24
doc/org/tut20.org
View file

@ -52,12 +52,12 @@ This is very simple: [[file:autfilt.org][=autfilt=]] can read automata in any of
supported formats, so all we have to do is to request the HOA output
with =-H=:
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -H tut20.never
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 0
@ -81,7 +81,7 @@ State: 4
[1] 3
[t] 4
--END--
#+end_example
#+END_SRC
* Python
@ -89,13 +89,13 @@ Another one-liner. The =spot.automaton()= function reads a single
automaton, and each automaton has a =to_str()= method that can print
in =hoa=, =lbtt=, =spin= (for never claim) or =dot=.
#+BEGIN_SRC python :results output :exports both
#+BEGIN_SRC python :results output :exports both :wrap SRC hoa
import spot
print(spot.automaton('tut20.never').to_str('hoa'))
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 0
@ -119,7 +119,7 @@ State: 4
[1] 3
[t] 4
--END--
#+end_example
#+END_SRC
* C++
@ -134,7 +134,7 @@ you), and =aut= is the actual automaton. The parser usually tries to
recover from errors, so =aut= may not be null even if =errors= is
non-empty.
#+BEGIN_SRC C++ :results verbatim :exports both
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
#include <string>
#include <iostream>
#include "parseaut/public.hh"
@ -159,7 +159,7 @@ non-empty.
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 0
@ -183,7 +183,7 @@ State: 4
[1] 3
[t] 4
--END--
#+end_example
#+END_SRC
In automata, transitions guards are represented by BDDs. The role of
=bdd_dict= object is to keep track of the correspondence between BDD
@ -221,14 +221,14 @@ an =automaton_stream_parser= and calls its =parse()= method once.
In Python, you can easily iterate over a file containing multiple
automata by doing:
#+BEGIN_SRC python :results output :exports code
#+BEGIN_SRC python :results output :exports code :wrap SRC hoa
import spot
for aut in spot.automata('tut20.never'):
print(aut.to_str('hoa'))
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 0
@ -252,7 +252,7 @@ State: 4
[1] 3
[t] 4
--END--
#+end_example
#+END_SRC
In fact =spot.automaton()= is just a wrapper around =spot.automata()=
to return only the first automaton.

7
doc/org/tut21.org
View file

@ -10,12 +10,11 @@ commands aren't up to the task either.
First let's create an example automaton in HOA format.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -U -H 'Fa | G(Fb&Fc)' | tee tut21.hoa
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
name: "Fa | G(Fb & Fc)"
States: 4
@ -41,7 +40,7 @@ State: 3
[!0&1&!2] 3 {0}
[!0&!1&!2] 3
--END--
#+end_example
#+END_SRC
We now write some C++ to load this automaton [[file:tut20.org][as we did before]], and in
=custom_print()= we print it out in a custom way by explicitly

6
doc/org/tut22.org
View file

@ -5,7 +5,7 @@
This example demonstrates how to create an automaton in C++, and then print it.
#+BEGIN_SRC C++ :results verbatim :exports both
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
#include <iostream>
#include "twaalgos/hoa.hh"
#include "twa/twagraph.hh"
@ -47,7 +47,7 @@ This example demonstrates how to create an automaton in C++, and then print it.
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
@ -64,4 +64,4 @@ State: 1
State: 2
[0 | 1] 1 {0 1}
--END--
#+end_example
#+END_SRC

42
doc/org/tut30.org
View file

@ -20,7 +20,7 @@ autfilt tut30.hoa --dot=.a
#+begin_example
digraph G {
rankdir=LR
label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>)) | (Fin(<font color="#60BD68">❹</font>) &amp; Inf(<font color="#F15854">❺</font>))>
label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>)) | (Fin(<font color="#60BD68">❹</font>) &amp; Inf(<font color="#F15854">❺</font>))>
labelloc="t"
node [shape="circle"]
fontname="Lato"
@ -29,25 +29,25 @@ digraph G {
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 6
0 [label=<0<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
0 [label=<0<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
0 -> 2 [label=<!p1>]
0 -> 4 [label=<p1>]
1 [label=<1<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
1 [label=<1<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
1 -> 4 [label=<!p1>]
1 -> 3 [label=<p1>]
2 [label=<2<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
2 [label=<2<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
2 -> 0 [label=<!p1>]
2 -> 4 [label=<p1>]
3 [label=<3<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
3 [label=<3<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
3 -> 4 [label=<!p1>]
3 -> 1 [label=<p1>]
4 [label=<4<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
4 [label=<4<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
4 -> 4 [label=<!p1>]
4 -> 4 [label=<p1>]
5 [label=<5<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
5 [label=<5<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
5 -> 2 [label=<!p1>]
5 -> 3 [label=<p1>]
6 [label=<6<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
6 [label=<6<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
6 -> 5 [label=<!p1>]
6 -> 5 [label=<p1>]
}
@ -76,12 +76,11 @@ changed to Büchi, but simplification routines (useless SCCs removal,
simulation-based reductions, acceptance sets simplifications,
WDBA-minimization, ...) will also be applied.
#+BEGIN_SRC sh :results verbatim :exports both
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -B -D -H tut30.hoa
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
@ -89,7 +88,7 @@ AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
@ -105,7 +104,7 @@ State: 4
[!0] 0
[0] 4
--END--
#+end_example
#+END_SRC
#+NAME: tut30out
#+BEGIN_SRC sh :results verbatim :exports none
@ -156,14 +155,13 @@ the result further.
The Python version uses the =postprocess()= routine:
#+BEGIN_SRC python :results output :exports both
#+BEGIN_SRC python :results output :exports both :wrap SRC hoa
import spot
aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic')
print(aut.to_str('hoa'))
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
@ -171,7 +169,7 @@ AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
@ -187,7 +185,7 @@ State: 4
[!0] 0
[0] 4
--END--
#+end_example
#+END_SRC
The =postprocess()= function has an interface similar to
[[file:tut10.org][the =translate()= function discussed previously]]:
@ -231,7 +229,7 @@ The C++ version of this code is a bit more verbose, because the
=postprocessor= object, configure it, and then call it for each
automaton to process.
#+BEGIN_SRC C++ :results verbatim :exports both
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
#include <iostream>
#include "parseaut/public.hh"
#include "twaalgos/postproc.hh"
@ -258,7 +256,7 @@ automaton to process.
#+END_SRC
#+RESULTS:
#+begin_example
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
@ -266,7 +264,7 @@ AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
@ -282,7 +280,7 @@ State: 4
[!0] 0
[0] 4
--END--
#+end_example
#+END_SRC
#+BEGIN_SRC sh :results silent :exports results
rm -f tut30.hoa

27
elisp/Makefile.am Normal file
View file

@ -0,0 +1,27 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2015 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
## Spot is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published by
## the Free Software Foundation; either version 3 of the License, or
## (at your option) any later version.
##
## Spot is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
## License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this program. If not, see <http://www.gnu.org/licenses/>.
EXTRA_DIST = hoa-mode.el
GIT = https://gitlab.lrde.epita.fr/spot/emacs-modes/raw/master/
.PHONY: update-el
update-el:
wget $(GIT)/hoa-mode.el -O $(srcdir)/hoa-mode.el
chmod a-w $(srcdir)/hoa-mode.el

3
elisp/README Normal file
View file

@ -0,0 +1,3 @@
hoa-mode.el is used when building the documentation for syntax
highlighting the HOA files displayed in the examples. But you may
also want to use it for editing and displaying HOA files.

249
elisp/hoa-mode.el Normal file
View file

@ -0,0 +1,249 @@
;;; hoa-mode.el --- Major mode for the Hanoi Omega Automata format
;; Copyright (C) 2015 Alexandre Duret-Lutz
;; Author: Alexandre Duret-Lutz <adl@lrde.epita.fr>
;; Maintainer: Alexandre Duret-Lutz <adl@lrde.epita.fr>
;; URL: https://gitlab.lrde.epita.fr/spot/emacs-modes
;; Keywords: major-mode, automata, convenience
;; Created: 2015-11-13
;;; License:
;; This package is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 3, or (at your option)
;; any later version.
;;
;; This package is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;; GNU General Public License for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs. If not, see <http://www.gnu.org/licenses/>.
;;; Commentary:
;; Major mode for editing files in the Hanoi Omega Automata format.
;; (See URL `http://adl.github.io/hoaf/' for that format.) This
;; provides rules for syntax highlighting, some navigation functions,
;; and a convenient way to display the automata in Emacs.
;;; Code:
;;;###autoload
(add-to-list 'auto-mode-alist '("\\.hoa\\'" . hoa-mode))
;;;###autoload
(add-to-list 'magic-mode-alist '("\\<HOA:\\s-*v" . hoa-mode))
(defgroup hoa-mode nil
"Major mode for editing Hanoi Omega Automata files."
:group 'data)
(defgroup hoa-mode-faces nil
"Faces used by `hoa-mode'."
:group 'hoa-mode
:group 'faces)
(defface hoa-header-uppercase-face
'((t :inherit font-lock-type-face :weight bold))
"Face for headers with an uppercase initial."
:group 'hoa-mode-faces)
(defface hoa-header-lowercase-face
'((t :inherit font-lock-type-face :weight normal))
"Face for headers with a lowercase initial."
:group 'hoa-mode-faces)
(defface hoa-keyword-face
'((t :inherit font-lock-keyword-face))
"Face used for --BODY--, --END--, and --ABORT--."
:group 'hoa-mode-faces)
(defface hoa-builtin-face
'((t :inherit font-lock-builtin-face))
"Face used for Inf, Fin, t, and f."
:group 'hoa-mode-faces)
(defface hoa-acceptance-set-face
'((t :inherit font-lock-constant-face :weight bold))
"Face used for acceptance sets."
:group 'hoa-mode-faces)
(defface hoa-alias-face
'((t :inherit font-lock-variable-name-face))
"Face used for aliases."
:group 'hoa-mode-faces)
(defface hoa-ap-number-face
'((t :inherit font-lock-constant-face))
"Face used for numbers that denote atomic propositions."
:group 'hoa-mode-faces)
(defconst hoa-alias-regex
"@[a-zA-Z0-9_-]*\\_>"
"Regex for matching aliases.")
(defvar hoa-font-lock-keywords
(list
'("\\_<[A-Z][a-zA-Z0-9_-]*:" . 'hoa-header-uppercase-face)
'("\\_<[a-z][a-zA-Z0-9_-]*:" . 'hoa-header-lowercase-face)
`(,hoa-alias-regex . 'hoa-alias-face)
'("\\_<--\\(BODY\\|END\\|ABORT\\)--" . 'hoa-keyword-face)
'("\\_<\\(Inf\\|Fin\\|t\\|f\\)\\_>" . 'hoa-builtin-face)
'("(\\s-*\\([0-9]+\\)\\s-*)" 1 'hoa-acceptance-set-face)
'("{\\(\\([0-9]\\|\\s-\\)+\\)}" 1 'hoa-acceptance-set-face)
;; numbers between brackets denote atomic propositions.
'("\\["
("\\_<[0-9]+\\_>"
(save-excursion (search-forward "]" nil t))
nil
(0 'hoa-ap-number-face)))
;; likewise for numbers following an Alias: definition
`(,(concat "Alias:\\s-*" hoa-alias-regex)
("\\_<[0-9]+\\_>"
(save-excursion
(re-search-forward
(concat "\\(" hoa-alias-regex "\\|[0-9|&!]\\|\\s-\\)+") nil t))
nil
(0 'hoa-ap-number-face))))
"Hilighting rules for `hoa-mode'.")
(defvar hoa-mode-syntax-table
(let ((st (make-syntax-table)))
(modify-syntax-entry ?< "." st)
(modify-syntax-entry ?> "." st)
(modify-syntax-entry ?| "." st)
(modify-syntax-entry ?_ "_" st)
(modify-syntax-entry ?- "_" st)
(modify-syntax-entry ?$ "." st)
(modify-syntax-entry ?& "." st)
(modify-syntax-entry ?+ "." st)
(modify-syntax-entry ?/ ". 14bn" st)
(modify-syntax-entry ?* ". 23bn" st)
st)
"Syntax table for `hoa-mode'.")
(defun hoa-start-of-automaton ()
"Move to the start of the automaton at point."
(interactive)
(search-backward "HOA:"))
(defun hoa-end-of-automaton ()
"Move to the end of the automaton at point."
(interactive)
; if we are pointing inside something that looks like --END-- or
; --ABORT--, back out a bit.
(if (looking-at "[ENDABORT-]*-")
(backward-word))
(re-search-forward "--\\(END\\|ABORT\\)--\n?"))
(defun hoa-mark-automaton-at-point ()
"Mark the automaton at point."
(interactive)
(hoa-end-of-automaton)
(set-mark (point))
(hoa-start-of-automaton))
(defcustom hoa-display-error-buffer "*hoa-dot-error*"
"The name of the buffer to display errors from `hoa-display-command'."
:group 'hoa-mode
:type 'string)
(defcustom hoa-display-buffer "*hoa-display*"
"The name of the buffer to display automata."
:group 'hoa-mode
:type 'string)
(defcustom hoa-display-command "autfilt --dot='barf(Lato)' | dot -Tpng"
"Command used to display HOA files.
The command is expected to take the automaton in HOA format on
its standard input, and output an image in PNG format on its
standard output.
The default value uses the tools autfilt (part of the Spot
package, see URL `https://spot.lrde.epita.fr/') and dot (part of
the GraphViz package, see URL `http://www.graphviz.org/')."
:group 'hoa-mode
:type 'string)
(defun hoa-display-automaton-at-point ()
"Display the automaton-at-point.
This uses the command in `hoa-display-command' to convert HOA
into PNG, and then display the result in `hoa-display-buffer'.
If the command terminates with an error, its standard error is
put in `hoa-display-error-buffer' and shown."
(interactive)
(let ((b (save-excursion (if (not (looking-at "HOA:"))
(hoa-start-of-automaton)
(point))))
(e (save-excursion (hoa-end-of-automaton) (point)))
(dotbuf (generate-new-buffer "*hoa-dot-output*"))
(errfile (make-temp-file
(expand-file-name "hoadot" temporary-file-directory)))
(coding-system-for-read 'no-conversion))
(with-current-buffer dotbuf
(set-buffer-multibyte nil))
(let ((exit-status
(call-process-region b e shell-file-name nil (list dotbuf errfile)
nil shell-command-switch hoa-display-command)))
(when (equal 0 exit-status)
(let ((hoa-img (create-image (with-current-buffer dotbuf (buffer-string))
'png t)))
(with-current-buffer (get-buffer-create hoa-display-buffer)
(erase-buffer)
(insert-image hoa-img)
(display-buffer (current-buffer)))))
(when (file-exists-p errfile)
(when (< 0 (nth 7 (file-attributes errfile)))
(with-current-buffer (get-buffer-create hoa-display-error-buffer)
(setq buffer-read-only nil)
(erase-buffer)
(format-insert-file errfile nil)
(display-buffer (current-buffer))))
(delete-file errfile))
(kill-buffer dotbuf))))
(defvar hoa-mode-map
(let ((map (make-keymap)))
(define-key map "\M-e" 'hoa-end-of-automaton)
(define-key map "\M-a" 'hoa-start-of-automaton)
(define-key map "\C-\M-h" 'hoa-mark-automaton-at-point)
(define-key map "\C-c\C-c" 'hoa-display-automaton-at-point)
map)
"Keymap for `hoa-mode'.")
(defcustom hoa-mode-hook nil
"Hook run whenever `hoa-mode' is activated."
:group 'hoa-mode
:type 'hook)
;;;### autoload
(defun hoa-mode ()
"Major mode for editing files in the Hanoi Omega Automata format.
See URL `http://adl.github.io/hoaf/' for a definition of that format.
The following key bindings are installed in hoa-mode:
\\{hoa-mode-map}
By default the `hoa-display-automaton-at-point' function requires
extra software (Spot and GraphViz), but can be configured to use
other tools. See that function for details."
(interactive)
(kill-all-local-variables)
(set-syntax-table hoa-mode-syntax-table)
(set (make-local-variable 'font-lock-defaults) '(hoa-font-lock-keywords))
(use-local-map hoa-mode-map)
(setq major-mode 'hoa-mode)
(setq mode-name "HOA")
(run-hooks 'hoa-mode-hook))
(provide 'hoa-mode)
;;; hoa-mode.el ends here