From 5aba246ff044bee0227f80de1d7c7a67aba94835 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 20 Nov 2015 14:28:51 +0100 Subject: [PATCH] org: syntax-highlight the HOA outputs * 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. --- Makefile.am | 6 +- README | 1 + configure.ac | 1 + debian/copyright | 19 ++++ doc/org/hoa.org | 108 ++++++++++---------- doc/org/init.el.in | 8 +- doc/org/ltldo.org | 29 +++--- doc/org/oaut.org | 40 ++++---- doc/org/spot.css | 11 +- doc/org/tut20.org | 24 ++--- doc/org/tut21.org | 7 +- doc/org/tut22.org | 6 +- doc/org/tut30.org | 42 ++++---- elisp/Makefile.am | 27 +++++ elisp/README | 3 + elisp/hoa-mode.el | 249 +++++++++++++++++++++++++++++++++++++++++++++ 16 files changed, 449 insertions(+), 132 deletions(-) create mode 100644 elisp/Makefile.am create mode 100644 elisp/README create mode 100644 elisp/hoa-mode.el diff --git a/Makefile.am b/Makefile.am index 0d40a33aa..5c035e992 100644 --- a/Makefile.am +++ b/Makefile.am @@ -21,14 +21,14 @@ ## along with this program. If not, see . 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 diff --git a/README b/README index e4b5f349e..2832c0f51 100644 --- a/README +++ b/README @@ -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 ------------------ diff --git a/configure.ac b/configure.ac index 0d7d32642..73ba3811c 100644 --- a/configure.ac +++ b/configure.ac @@ -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 diff --git a/debian/copyright b/debian/copyright index 28664c02a..55ad09caf 100644 --- a/debian/copyright +++ b/debian/copyright @@ -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 . + . + 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+ diff --git a/doc/org/hoa.org b/doc/org/hoa.org index b3184986d..9601f0344 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -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 <sba.hoa <hw.hoa <%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 diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 68f4fa424..dff34b408 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 diff --git a/doc/org/spot.css b/doc/org/spot.css index 1d7e29de9..44d6123cd 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -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} diff --git a/doc/org/tut20.org b/doc/org/tut20.org index 08600fe7d..59ea25d4a 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -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 #include #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. diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 991ae360f..a8dcbafd8 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -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 diff --git a/doc/org/tut22.org b/doc/org/tut22.org index 56fc020fd..d8f405775 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -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 #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 diff --git a/doc/org/tut30.org b/doc/org/tut30.org index e52d69323..c08fb76f2 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -20,7 +20,7 @@ autfilt tut30.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸)) | (Fin(❹) & Inf(❺))> + label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸)) | (Fin(❹) & Inf(❺))> 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
❷❺>] + 0 [label=<0
❷❺>] 0 -> 2 [label=] 0 -> 4 [label=] - 1 [label=<1
❷❺>] + 1 [label=<1
❷❺>] 1 -> 4 [label=] 1 -> 3 [label=] - 2 [label=<2
❸❹>] + 2 [label=<2
❸❹>] 2 -> 0 [label=] 2 -> 4 [label=] - 3 [label=<3
❸❹>] + 3 [label=<3
❸❹>] 3 -> 4 [label=] 3 -> 1 [label=] - 4 [label=<4
❶❷❹>] + 4 [label=<4
❶❷❹>] 4 -> 4 [label=] 4 -> 4 [label=] - 5 [label=<5
❷❹>] + 5 [label=<5
❷❹>] 5 -> 2 [label=] 5 -> 3 [label=] - 6 [label=<6
❷❹>] + 6 [label=<6
❷❹>] 6 -> 5 [label=] 6 -> 5 [label=] } @@ -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 #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 diff --git a/elisp/Makefile.am b/elisp/Makefile.am new file mode 100644 index 000000000..0b1213234 --- /dev/null +++ b/elisp/Makefile.am @@ -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 . + +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 diff --git a/elisp/README b/elisp/README new file mode 100644 index 000000000..97e556ec8 --- /dev/null +++ b/elisp/README @@ -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. diff --git a/elisp/hoa-mode.el b/elisp/hoa-mode.el new file mode 100644 index 000000000..2cd7ec552 --- /dev/null +++ b/elisp/hoa-mode.el @@ -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 +;; Maintainer: Alexandre Duret-Lutz +;; 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 . + +;;; 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 '("\\" + "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