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

Better formula I/O for ipython.

Browse source 
* src/ltlparse/public.hh, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll (parse_error): New class.
(parse_formula): New function that raises a parse_error
exception on error.
* src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc:
(to_sclatex_string): New method.
* wrap/python/spot.i: Catch the parser_error exception,
and use the to_sclatex_string for MathJax rendering.
* wrap/python/tests/run.in: Start ipython on demand.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-24 14:00:59 +02:00
parent 6d7c258fd7
commit ae35cc29f5
7 changed files with 150 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ltlparse/ltlparse.yy
View file

@ -33,6 +33,7 @@
%code requires
{
#include <string>
#include <sstream>
#include "public.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
@ -1034,6 +1035,24 @@ namespace spot
return result;
}
const formula*
parse_formula(const std::string& ltl_string, environment& env)
{
parse_error_list pel;
const formula* f = parse(ltl_string, pel, env);
std::ostringstream s;
if (format_parse_errors(s, ltl_string, pel))
{
parse_error_list pel2;
const formula* g = parse_lbt(ltl_string, pel2, env);
if (pel2.empty())
return g;
else
throw parse_error(s.str());
}
return f;
}
}
}

6
src/ltlparse/ltlscan.ll
View file

@ -110,7 +110,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
unput(')');
if (!missing_parent)
error_list.push_back(
spot::ltl::parse_error(*yylloc,
spot::ltl::one_parse_error(*yylloc,
"missing closing parenthese"));
missing_parent = true;
}
@ -164,7 +164,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
unput(')');
if (!missing_parent)
error_list.push_back(
spot::ltl::parse_error(*yylloc,
spot::ltl::one_parse_error(*yylloc,
"missing closing brace"));
missing_parent = true;
}
@ -204,7 +204,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
if (errno || yylval->num != n)
{
error_list.push_back(
spot::ltl::parse_error(*yylloc,
spot::ltl::one_parse_error(*yylloc,
"value too large ignored"));
// Skip this number and read next token
yylloc->step();

26
src/ltlparse/public.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -40,9 +40,9 @@ namespace spot
#ifndef SWIG
/// \brief A parse diagnostic with its location.
typedef std::pair<location, std::string> parse_error;
typedef std::pair<location, std::string> one_parse_error;
/// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<parse_error> parse_error_list;
typedef std::list<one_parse_error> parse_error_list;
#else
// Turn parse_error_list into an opaque type for Swig.
struct parse_error_list {};
@ -124,6 +124,24 @@ namespace spot
environment& env = default_environment::instance(),
bool debug = false);
struct SPOT_API parse_error: public std::runtime_error
{
parse_error(const std::string& s): std::runtime_error(s)
{
}
};
/// \brief A simple wrapper to parse() and parse_lbt().
///
/// This is mostly meant for interactive use. It first tries parse(); if
/// this fails it tries parse_lbt(); and if both fails it returns the errors
/// of the first call to parse() as a std::runtime_error().
SPOT_API const formula*
parse_formula(const std::string& ltl_string,
environment& env = default_environment::instance());
/// \brief Build a formula from a string representing a SERE.
/// \param sere_string The string to parse.
/// \param error_list A list that will be filled with

61
src/ltlvisit/tostring.cc
View file

@ -260,6 +260,47 @@ namespace spot
"\\SereGoto{",
};
const char* sclatex_kw[] = {
"\\ffalse",
"\\ttrue",
"\\varepsilon",
" \\oplus ",
" \\rightarrow ",
" \\leftrightarrow ",
" \\mathbin{\\mathsf{U}} ",
" \\mathbin{\\mathsf{R}} ",
" \\mathbin{\\mathsf{W}} ",
" \\mathbin{\\mathsf{M}} ",
("\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt"
"\\hbox{$\\mathord{\\rightarrow}$}} "),
("\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt"
"\\hbox{$\\mathord{\\Rightarrow}$}} "),
"\\seqM ",
"\\seqXM ",
("\\mathrel{\\Box\\kern-1.7pt\\raise.4pt"
"\\hbox{$\\mathord{\\rightarrow}$}} "),
("\\mathrel{\\Box\\kern-1.7pt\\raise.4pt"
"\\hbox{$\\mathord{\\Rightarrow}$}} "),
"\\lnot ",
"\\mathsf{X} ",
"\\mathsf{F} ",
"\\mathsf{G} ",
" \\lor ",
" \\cup ",
" \\land ",
" \\cap ",
" \\mathbin{\\mathsf{\\&}} ",
" \\mathbin{\\mathsf{;}} ",
" \\mathbin{\\mathsf{:}} ",
"\\{",
"\\}",
"}",
"^{\\star",
"^+",
"^{=",
"^{\\to",
};
static bool
is_bare_word(const char* str)
{
@ -370,7 +411,7 @@ namespace spot
}
else
{
if (kw_ == latex_kw)
if (kw_ == latex_kw || kw_ == sclatex_kw)
{
size_t s = str.size();
while (str[s - 1] >= '0' && str[s - 1] <= '9')
@ -945,6 +986,24 @@ namespace spot
return os.str();
}
std::ostream&
to_sclatex_string(const formula* f, std::ostream& os,
bool full_parent, bool ratexp)
{
to_string_visitor v(os, full_parent, ratexp, sclatex_kw);
f->accept(v);
return os;
}
std::string
to_sclatex_string(const formula* f,
bool full_parent, bool ratexp)
{
std::ostringstream os;
to_sclatex_string(f, os, full_parent, ratexp);
return os.str();
}
}
}

30
src/ltlvisit/tostring.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -101,8 +101,7 @@ namespace spot
SPOT_API std::string
to_wring_string(const formula* f);
/// \brief Output a formula as an LaTeX string which is parsable unless
/// the formula contains automaton operators (used in ELTL formulae).
/// \brief Output a formula as an LaTeX string which is parsable.
/// \param f The formula to translate.
/// \param os The stream where it should be output.
/// \param full_parent Whether or not the string should by fully
@ -112,7 +111,7 @@ namespace spot
to_latex_string(const formula* f, std::ostream& os,
bool full_parent = false, bool ratexp = false);
/// \brief Output a formula as a LaTeX string which is parsable
/// \brief Output a formula as a LaTeX string which is parsable.
/// unless the formula contains automaton operators (used in ELTL formulae).
/// \param f The formula to translate.
/// \param full_parent Whether or not the string should by fully
@ -122,6 +121,29 @@ namespace spot
to_latex_string(const formula* f,
bool full_parent = false, bool ratexp = false);
/// \brief Output a formula as a self-contained LaTeX string.
///
/// The result cannot be parsed back.
/// \param f The formula to translate.
/// \param os The stream where it should be output.
/// \param full_parent Whether or not the string should by fully
/// parenthesized.
/// \param ratexp Whether we are printing a SERE.
SPOT_API std::ostream&
to_sclatex_string(const formula* f, std::ostream& os,
bool full_parent = false, bool ratexp = false);
/// \brief Output a formula as a self-contained LaTeX string.
///
/// The result cannot be parsed bacl.
/// \param f The formula to translate.
/// \param full_parent Whether or not the string should by fully
/// parenthesized.
/// \param ratexp Whether we are printing a SERE.
SPOT_API std::string
to_sclatex_string(const formula* f,
bool full_parent = false, bool ratexp = false);
/// @}
}
}

22
wrap/python/spot.i
View file

@ -31,6 +31,7 @@
%include "std_shared_ptr.i"
%include "std_string.i"
%include "std_list.i"
%include "exception.i"
// git grep 'typedef.*std::shared_ptr' | grep -v const
// sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g'
@ -172,6 +173,19 @@ using namespace spot;
};
%apply char** OUTPUT { char** err };
%exception {
try {
$action
}
catch (const spot::ltl::parse_error& e)
{
std::string er("\n");
er += e.what();
SWIG_exception(SWIG_SyntaxError, er.c_str());
}
}
// False and True cannot be redefined in Python3, even in a class.
// Spot uses these in an enum of the constant class.
%rename(FalseVal) False;
@ -286,12 +300,12 @@ namespace spot {
size_t __hash__() { return self->hash(); }
std::string
__str__(void)
std::string __repr__() { return spot::ltl::to_string(self); }
std::string _repr_latex_()
{
return spot::ltl::to_string(self);
return std::string("$") + spot::ltl::to_sclatex_string(self) + '$';
}
std::string __str__() { return spot::ltl::to_string(self); }
}
%nodefaultctor std::ostream;

2
wrap/python/tests/run.in
View file

@ -40,6 +40,8 @@ case $1 in
PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ "$@";;
*.test)
exec sh -x "$@";;
ipython*)
PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec "$@";;
*)
echo "Unknown extension" >&2
exit 2;;