From 60bd9dd6067412b034d17880f5f1c4466013fdef Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 Jun 2015 23:21:30 +0200 Subject: [PATCH] org: add a new code example This addresses on item of #14. * doc/org/tut20.org: New file. * doc/Makefile.am: Add it. * doc/org/tut.org: Link to it. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Fix some PATH issues. --- doc/Makefile.am | 1 + doc/org/.dir-locals.el.in | 10 +- doc/org/init.el.in | 8 +- doc/org/tut.org | 1 + doc/org/tut20.org | 315 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 327 insertions(+), 8 deletions(-) create mode 100644 doc/org/tut20.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 68a73d6b3..a0bee2a96 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -84,6 +84,7 @@ ORG_FILES = \ org/tut01.org \ org/tut02.org \ org/tut10.org \ + org/tut20.org \ org/satmin.org \ org/satmin.tex \ org/setup.org \ diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in index f7145a4e6..4525081a6 100644 --- a/doc/org/.dir-locals.el.in +++ b/doc/org/.dir-locals.el.in @@ -5,9 +5,10 @@ (org-mode . ((whitespace-style face empty trailing) (eval . (progn - (setq org-babel-sh-command (concat "PATH=../../src/bin" - path-separator - "$PATH sh")) + (setenv "PATH" + (concat "@abs_top_builddir@/src/bin" + path-separator + (getenv "PATH"))) (setenv "PYTHONPATH" (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:" (getenv "PYTHONPATH"))) @@ -22,8 +23,9 @@ (dot . t) (C . t))))) (org-confirm-babel-evaluate . nil) - (org-babel-python-command . "/usr/bin/python3") + (org-babel-python-command . "@PYTHON@") (org-babel-C++-compiler . "./g++wrap") + (shell-file-name . "@SHELL@") (org-publish-project-alist . (("spot-html" :base-directory "." diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 3cbdcc408..55d472968 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -21,12 +21,12 @@ (C . t))) (setq org-confirm-babel-evaluate nil) -(setq org-babel-sh-command - (concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh")) - -(setq org-babel-python-command "/usr/bin/python3") +(setq org-babel-python-command "@PYTHON@") (setq org-babel-C++-compiler "./g++wrap") +(setq shell-file-name "@SHELL@") +(setenv "PATH" + (concat "@abs_top_builddir@/src/bin" path-separator (getenv "PATH"))) (setenv "PYTHONPATH" (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:" (getenv "PYTHONPATH"))) diff --git a/doc/org/tut.org b/doc/org/tut.org index 81ac4a508..23e01556a 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -16,3 +16,4 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut01.org][Parsing and Printing LTL Formulas]] - [[file:tut02.org][Relabeling Formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] +- [[file:tut20.org][Converting a never claim into HOA]] diff --git a/doc/org/tut20.org b/doc/org/tut20.org new file mode 100644 index 000000000..af3752007 --- /dev/null +++ b/doc/org/tut20.org @@ -0,0 +1,315 @@ +#+TITLE: Converting a never claim into HOA +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +The goal is to start from a never claim, as produced by Spin, e.g.: + +#+BEGIN_SRC sh :results verbatim :exports both +spin -f '[]<>foo U bar' > tut20.never +cat tut20.never +#+END_SRC + +#+RESULTS: +#+begin_example +never { /* []<>foo U bar */ +T0_init: + do + :: atomic { ((bar)) -> assert(!((bar))) } + :: (1) -> goto T0_S53 + od; +accept_S42: + do + :: (1) -> goto T0_S42 + od; +T0_S42: + do + :: ((foo)) -> goto accept_S42 + :: (1) -> goto T0_S42 + od; +T0_S53: + do + :: (1) -> goto T0_S53 + :: ((bar) && (foo)) -> goto accept_S42 + :: ((bar)) -> goto T0_S42 + od; +accept_all: + skip +} +#+end_example + +and convert this into an automaton in [[file:hoa.org][the HOA format]]. + +Note that the automaton parser of Spot can read automata written +either as never claims, in LBTT's format or in the HOA format, and +there is no need to specify which format you expect. Even if our +example use a never claim as input, the code we write will work with +any of those formats. + +* Shell + +This is very simple: [[file:autfilt.org][=autfilt=]] can read automata in any of the +supported formats, so all we have to do is to request the HOA output +with =-H=: + +#+BEGIN_SRC sh :results verbatim :exports both +autfilt -H tut20.never +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 0 +AP: 2 "bar" "foo" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[t] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +[0&1] 3 +[0] 4 +State: 3 {0} +[t] 4 +State: 4 +[1] 3 +[t] 4 +--END-- +#+end_example + +* Python + +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 +import spot +print(spot.automaton('tut20.never').to_str('hoa')) +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 0 +AP: 2 "bar" "foo" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[t] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +[0&1] 3 +[0] 4 +State: 3 {0} +[t] 4 +State: 4 +[1] 3 +[t] 4 +--END-- +#+end_example + +* C++ + +Parsing an automaton is almost similar to [[file:tut01.org][parsing an LTL formula]]. The +=hoa_parse()= function (despite the name, it can actually read never +claims, or the LBTT or HOA formats) takes a filename, a reference to a +=hoa_parse_error_list= object to populate (should errors be found) and +a BDD dictionary (to be discussed later on this page). It returns a +shared pointer to a structure that has two fields: =aborted= is a +Boolean telling if the input automaton was voluntarily aborted (a +feature of [[file:hoa.org][the HOA format]]), and =aut= is the actual automaton. The +shared pointer returned by =hoa_parse()= might be null (in which case +the the =hoa_parse_error_list= is guaranteed not to be empty), but +since the parser performs some error recovery it is likely that an +automaton is returned even in the presence of parse errors. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "hoaparse/public.hh" + #include "twaalgos/hoa.hh" + + int main() + { + std::string input = "tut20.never"; + spot::hoa_parse_error_list pel; + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::hoa_aut_ptr h = hoa_parse(input, pel, dict); + if (spot::format_hoa_parse_errors(std::cerr, input, pel)) + return 1; + // This cannot occur when reading a never claim, but + // it could while reading a HOA file. + if (h->aborted) + { + std::cerr << "--ABORT-- read" << '\n'; + return 1; + } + spot::print_hoa(std::cout, h->aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 0 +AP: 2 "bar" "foo" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[t] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +[0&1] 3 +[0] 4 +State: 3 {0} +[t] 4 +State: 4 +[1] 3 +[t] 4 +--END-- +#+end_example + +In automata, transitions guards are represented by BDDs. The role of +=bdd_dict= object is to keep track of the correspondence between BDD +variables and atomic propositions such as =foo= and =bar= in the above +example. So each automaton has a shared pointer to some =bdd_dict= +(this shared pointer is what the =bdd_dict_ptr= type is), and +operations between automata (like a product) can only work on automata +that share the same pointer. Here, when we call the automaton parser, +we supply the =bdd_dict_ptr= that should be used to do the mapping +between atomic propositions and BDD variables. Atomic propositions +that were not already registered will get a new BDD variable number, +and while existing atomic propositions will reuse the existing +variable. + +In the example for [[file:tut10.org][translating LTL into BA]], we did not specify any +=bdd_dict=, because the =translator= object will create a new one by +default. However it is possible to supply such a =bdd_dict= to the +translator as well. Similarly, in the Python bindings, there is a +global =bdd_dict= that is implicitly used for all operations, but it +can be specified if needed. + +* Additional comments + +There are actually different C++ interfaces to the automaton parser, +depending on your use case. For instance the parser is able to read a +stream of automata stored in the same file, so that they could be +processed in a loop. For this, you would instanciate a +=hoa_stream_parser= object and call its =parse()= method in a loop. +Each call to this method will either return one automaton, or +=nullptr= if there is no more automaton to read. The =hoa_parse()= +function is actually a simple wrapper that instanciate +=hoa_stream_parser= and calls =parse()= once. + + +In Python, you can easily iterate over a file containing multiple +automata by doing: + +#+BEGIN_SRC python :results output :exports code +import spot +for aut in spot.automata('tut20.never'): + print(aut.to_str('hoa')) +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 0 +AP: 2 "bar" "foo" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[t] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +[0&1] 3 +[0] 4 +State: 3 {0} +[t] 4 +State: 4 +[1] 3 +[t] 4 +--END-- +#+end_example + +In fact =spot.automaton()= is just a wrapper around =spot.automata()= +to return only the first automaton. + +Still in Python, both =spot.automaton()= and =spot.automata()= can +accept three types of arguments: +- file names (such as in the above examples) +- commands that output automata on their standard output. Those can + be any shell expression, and must have '=|=' as their last + character. For instance here is how to convert Spin's output into + LBTT's formula without using temporary files. +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.automaton('spin -f "[]<>p0" |').to_str('lbtt')) +#+END_SRC + +#+RESULTS: +: 2 1 +: 0 1 -1 +: 1 p0 +: 0 t +: -1 +: 1 0 0 -1 +: 0 t +: -1 +: + +- a string that includes new lines, in which case it is assumed + to describe an automaton, and is passed directly to the parser: + +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[t] 1 +--END-- +""").to_str('spin')) +#+END_SRC + +#+RESULTS: +: never { +: T0_init: +: if +: :: ((a)) -> goto accept_all +: fi; +: accept_all: +: skip +: } +: