From 8de524adb0193687eb8fe08423a205a5eb9f3c33 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Jun 2015 23:53:04 +0200 Subject: [PATCH] org: add a first code example The difficulty is not the example, but setting up org-mode to allow Python and C++ example that use the local libraries, not those installed system-wide. * doc/org/.dir-locals.el: Rename as... * doc/org/.dir-locals.el.in: ... this, so we can easily define PYTHONPATH and other environment variables. * doc/org/init.el.in: Enable C++, and make sure but Python and C++ use the local libraries. * doc/org/g++wrap.in, doc/org/tut01.org: New files. * doc/Makefile.am, configure.ac: Adjust. * wrap/python/spot.py (to_str): Take a parenth argument. --- configure.ac | 2 + doc/Makefile.am | 4 +- doc/org/{.dir-locals.el => .dir-locals.el.in} | 10 +- doc/org/g++wrap.in | 6 + doc/org/init.el.in | 13 +- doc/org/tut01.org | 218 ++++++++++++++++++ wrap/python/spot.py | 12 +- 7 files changed, 255 insertions(+), 10 deletions(-) rename doc/org/{.dir-locals.el => .dir-locals.el.in} (74%) create mode 100755 doc/org/g++wrap.in create mode 100644 doc/org/tut01.org diff --git a/configure.ac b/configure.ac index 4e83efe97..aa1ae109f 100644 --- a/configure.ac +++ b/configure.ac @@ -191,6 +191,7 @@ AC_CONFIG_FILES([ doc/Doxyfile doc/Makefile doc/tl/Makefile + doc/org/.dir-locals.el doc/org/init.el iface/ltsmin/defs iface/ltsmin/Makefile @@ -224,6 +225,7 @@ AC_CONFIG_FILES([ wrap/python/tests/Makefile tools/x-to-1 ]) +AC_CONFIG_FILES([doc/org/g++wrap], [chmod +x doc/org/g++wrap]) AC_CONFIG_FILES([doc/dot], [chmod +x doc/dot]) AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run]) AC_OUTPUT diff --git a/doc/Makefile.am b/doc/Makefile.am index 40e27448e..c7176c450 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -57,7 +57,8 @@ org: rm -rf tmp ORG_FILES = \ - org/.dir-locals.el \ + org/.dir-locals.el.in \ + org/g++wrap.in \ org/init.el.in \ org/syntax.css \ org/spot.css \ @@ -77,6 +78,7 @@ ORG_FILES = \ org/randaut.org \ org/randltl.org \ org/tools.org \ + org/tut01.org \ org/satmin.org \ org/satmin.tex \ org/setup.org \ diff --git a/doc/org/.dir-locals.el b/doc/org/.dir-locals.el.in similarity index 74% rename from doc/org/.dir-locals.el rename to doc/org/.dir-locals.el.in index a5908c461..f7145a4e6 100644 --- a/doc/org/.dir-locals.el +++ b/doc/org/.dir-locals.el.in @@ -8,14 +8,22 @@ (setq org-babel-sh-command (concat "PATH=../../src/bin" path-separator "$PATH sh")) + (setenv "PYTHONPATH" + (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:" + (getenv "PYTHONPATH"))) + (setenv "DYLD_LIBRARY_PATH" + (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/src/.libs:@abs_top_builddir@/buddy/src/.libs:" + (getenv "DYLD_LIBRARY_PATH"))) (setenv "SPOT_DOTDEFAULT" "Brf(Lato)") (setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"] edge[arrowhead=vee, arrowsize=.7]") (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (python . t) - (dot . t))))) + (dot . t) + (C . t))))) (org-confirm-babel-evaluate . nil) (org-babel-python-command . "/usr/bin/python3") + (org-babel-C++-compiler . "./g++wrap") (org-publish-project-alist . (("spot-html" :base-directory "." diff --git a/doc/org/g++wrap.in b/doc/org/g++wrap.in new file mode 100755 index 000000000..4ed248848 --- /dev/null +++ b/doc/org/g++wrap.in @@ -0,0 +1,6 @@ +#!/bin/sh +# This is a wrapper around the compiler, to ensure that the code +# example run from the org-mode file are all linked with Spot. +exec @top_builddir@/libtool link \ + @CXX@ -std=c++11 -Wall -I@abs_top_srcdir@/src -I@abs_top_builddir@/src \ + "$@" @abs_top_builddir@/src/libspot.la diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 7056cd8c8..3cbdcc408 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -13,17 +13,26 @@ ;; conditions when doing concurrent builds. (setq org-publish-timestamp-directory "@abs_top_builddir@/.org-timestamps/") -(setq org-babel-python-command "/usr/bin/python3") (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t) - (python . t))) + (python . t) + (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-C++-compiler "./g++wrap") + +(setenv "PYTHONPATH" + (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/wrap/python:@abs_top_srcdir@/wrap/python:" + (getenv "PYTHONPATH"))) +(setenv "DYLD_LIBRARY_PATH" + (concat "@abs_top_builddir@/wrap/python/.libs:@abs_top_builddir@/src/.libs:@abs_top_builddir@/buddy/src/.libs:" + (getenv "DYLD_LIBRARY_PATH"))) (setenv "SPOT_DOTDEFAULT" "Brf(Lato)") (setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"] edge[arrowhead=vee, arrowsize=.7]") diff --git a/doc/org/tut01.org b/doc/org/tut01.org new file mode 100644 index 000000000..dcdf7a9a8 --- /dev/null +++ b/doc/org/tut01.org @@ -0,0 +1,218 @@ +#+TITLE: Parsing and Printing LTL Formulas +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +Our first task is to read formulas and print them in another syntax. + +* Shell command + +Using =ltlfilt=, you can easily read an LTL formula in one syntax, and +output it in another syntax. By default the parser will accept a +formula in [[file:ioltl.org][any infix syntax]], but if the input is in the prefix syntax +of LBT, you should use [[file:ioltl.org][=--lbt-input=]]. The output syntax is controlled +using different options such as (=--spin=, =--lbt=, =--latex=, etc.). +Full parentheses can also be requested using =-p=. + +#+BEGIN_SRC sh :results verbatim :exports both +formula='[]<>p0 || <>[]p1' +ltlfilt -f "$formula" --lbt +ltlfilt -f "$formula" --spin -p +ltlfilt --lbt-input -f '& & G p0 p1 p2' --latex +#+END_SRC + +#+RESULTS: +: | G F p0 F G p1 +: ([](<>(p0))) || (<>([](p1))) +: p_{1} \land p_{2} \land \G p_{0} + +The reason the LBT parser has to be explicitly enabled is because of +some corner cases that have different meanings in the two syntaxes. +(For instance =t= and =f= are the true constant in LBT's syntax, but they +are considered as atomic propositions in all the other syntaxes.) + +* Python bindings + +Here are the same operation in Python + +#+BEGIN_SRC python :results output :exports both +import spot +f = spot.formula('[]<>p0 || <>[]p1') +print(f.to_str('lbt')) +print(f.to_str('spin', parenth=True)) +print(spot.formula('& & G p0 p1 p2').to_str('latex')) +#+END_SRC + +#+RESULTS: +: | G F p0 F G p1 +: ([](<>(p0))) || (<>([](p1))) +: p_{1} \land p_{2} \land \G p_{0} + +The =spot.formula= function wraps the calls to the two formula parsers +of Spot. It first tries to parse the formula using infix syntaxes, +and if it fails, it tries to parse it with the prefix parser. (So +this this might fail to correctly interpret =t= or =f= if you are +processing a list of LBT formulas.) Using =spot.formula=, parse +errors are returned as an exception. + +* C++ + +** Simple wrapper for the two parsers + +We first start with the easy parser interface, similar to the one used +above in the python bindings. Here parse errors would be returned as +exceptions. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include "ltlparse/public.hh" + #include "ltlvisit/tostring.hh" + #include "ltlvisit/lbt.hh" + + int main() + { + const spot::ltl::formula* f = spot::ltl::parse_formula("[]<>p0 || <>[]p1"); + to_lbt_string(f, std::cout) << '\n'; + to_spin_string(f, std::cout, true) << '\n'; + to_latex_string(spot::ltl::parse_formula("& & G p0 p1 p2"), std::cout); + } +#+END_SRC + +#+RESULTS: +: | G F p0 F G p1 +: ([](<>(p0))) || (<>([](p1))) +: p_{1} \land p_{2} \land \G p_{0} + + +We do not recommend using this =parse_formula()= interface because of +the potential formulas (like =f= or =t=) that have different meanings +in the two parsers that are tried. + +Instead, depending on whether you want to parse formulas with infix +syntax, or formulas with prefix syntax, you should call the specific +parser. Additionally, this give you control over how to print errors. + +** Calling the infix parser explicitly + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "ltlparse/public.hh" + #include "ltlvisit/tostring.hh" + #include "ltlvisit/lbt.hh" + + int main() + { + std::string input = "[]<>p0 || <>[]p1"; + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = spot::ltl::parse(input, pel); + if (spot::ltl::format_parse_errors(std::cerr, input, pel)) + { + if (f) + f->destroy(); + return 1; + } + to_lbt_string(f, std::cout) << '\n'; + to_spin_string(f, std::cout, true) << '\n'; + f->destroy(); + } +#+END_SRC + +#+RESULTS: +: | G F p0 F G p1 +: ([](<>(p0))) || (<>([](p1))) + +So =parse()= process the =input=, and stores any diagnostic in =pel=, +which is a list of pairs associating each error to a location. You could +iterate over that list to print it by yourself as you wish, or you can +call =format_parse_errors()= to do that for you. + +If =pel= is empty, =format_parse_errors()= will do nothing and return +false. + +If =pel= is non empty, =format_parse_errors()= will display the errors +messages and return true. In the above code, we have decided to +aborts the execution in this case. + +However the parser usually tries to do some error recovery. For +instance if you have input =(a U b))= the parser will complain about +the extra parenthesis (=pel= not empty), but it will still return an +=f= that is equivalent to =a U b=. So you could decide to continue +with the "fixed" formula if you wish. Here is an example: + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "ltlparse/public.hh" + #include "ltlvisit/tostring.hh" + #include "ltlvisit/lbt.hh" + + int main() + { + std::string input = "(a U b))"; + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = spot::ltl::parse(input, pel); + // Use std::cout instead of std::cerr because we can only + // show the output of std::cout in this documentation. + (void) spot::ltl::format_parse_errors(std::cout, input, pel); + if (f == nullptr) + return 1; + to_lbt_string(f, std::cout) << '\n'; + to_spin_string(f, std::cout, true) << '\n'; + f->destroy(); + } +#+END_SRC + +#+RESULTS: +#+begin_example +>>> (a U b)) + ^ +syntax error, unexpected closing parenthesis + +>>> (a U b)) + ^ +ignoring trailing garbage + +U "a" "b" +(a) U (b) +#+end_example + + +The formula =f= is only returned as null when the parser really cannot +recover anything. + +Did you notice the calls to =f->destroy()= in these two examples? The +LTL formula objects are implemented as DAG with sharing of +subformulas. Each (sub)formula is therefore reference counted, and +currently this is done manually by calling =f->clone()= and +=f->destroy()= (do not ever =delete= a formula, always call +=f->destroy()=). + +** Calling the prefix parser explicitly + +The only difference here is the call to =parse_lbt()= instead of +=parse()=. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "ltlparse/public.hh" + #include "ltlvisit/tostring.hh" + + int main() + { + std::string input = "& & G p0 p1 p2"; + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = spot::ltl::parse_lbt(input, pel); + if (spot::ltl::format_parse_errors(std::cerr, input, pel)) + { + if (f) + f->destroy(); + return 1; + } + to_latex_string(f, std::cout) << '\n'; + f->destroy(); + } +#+END_SRC + +#+RESULTS: +: p_{1} \land p_{2} \land \G p_{0} diff --git a/wrap/python/spot.py b/wrap/python/spot.py index a46d0c57d..74ad828c4 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -98,21 +98,21 @@ ta.show = _return_automaton_as_svg def _formula_str_ctor(self, str): self.this = parse_formula(str) -def _formula_to_str(self, format = 'spot'): +def _formula_to_str(self, format = 'spot', parenth = False): if format == 'spot': - return to_string(self) + return to_string(self, parenth) elif format == 'spin': - return to_spin_string(self) + return to_spin_string(self, parenth) elif format == 'utf8': - return to_utf8_string(self) + return to_utf8_string(self, parenth) elif format == 'lbt': return to_lbt_string(self) elif format == 'wring': return to_wring_string(self) elif format == 'latex': - return to_latex_string(self) + return to_latex_string(self, parenth) elif format == 'sclatex': - return to_sclatex_string(self) + return to_sclatex_string(self, parenth) else: raise ValueError("unknown string format: " + format)