Commit 25de479e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: add a spot.automata(filename) interface, yielding automata

* src/hoaparse/fmterror.cc, src/hoaparse/public.hh,
src/hoaparse/hoaparse.yy (hoa_stream_parser::parse_strict): New method
that raises an exception whenever a syntax error is encountered.
* src/ltlparse/public.hh (parse_error): Move ...
* src/misc/common.hh: ... here.
* wrap/python/spot_impl.i: Wrap the hoa output.
* wrap/python/spot.py: Implement spot.automata.
* wrap/python/tests/automata-io.ipynb: New test.
* wrap/python/tests/Makefile.am: Add it.
parent 8e6b35e5
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -24,8 +24,8 @@ namespace spot ...@@ -24,8 +24,8 @@ namespace spot
{ {
bool bool
format_hoa_parse_errors(std::ostream& os, format_hoa_parse_errors(std::ostream& os,
const std::string& filename, const std::string& filename,
hoa_parse_error_list& error_list) hoa_parse_error_list& error_list)
{ {
bool printed = false; bool printed = false;
spot::hoa_parse_error_list::iterator it; spot::hoa_parse_error_list::iterator it;
......
...@@ -1612,7 +1612,9 @@ static void fix_properties(result_& r) ...@@ -1612,7 +1612,9 @@ static void fix_properties(result_& r)
namespace spot namespace spot
{ {
hoa_stream_parser::hoa_stream_parser(const std::string& name) hoa_stream_parser::hoa_stream_parser(const std::string& name,
bool ignore_abort)
: filename_(name), ignore_abort_(ignore_abort)
{ {
if (hoayyopen(name)) if (hoayyopen(name))
throw std::runtime_error(std::string("Cannot open file ") + name); throw std::runtime_error(std::string("Cannot open file ") + name);
...@@ -1630,6 +1632,7 @@ namespace spot ...@@ -1630,6 +1632,7 @@ namespace spot
ltl::environment& env, ltl::environment& env,
bool debug) bool debug)
{ {
restart:
result_ r; result_ r;
r.h = std::make_shared<spot::hoa_aut>(); r.h = std::make_shared<spot::hoa_aut>();
r.h->aut = make_tgba_digraph(dict); r.h->aut = make_tgba_digraph(dict);
...@@ -1652,7 +1655,11 @@ namespace spot ...@@ -1652,7 +1655,11 @@ namespace spot
last_loc = r.h->loc; last_loc = r.h->loc;
last_loc.step(); last_loc.step();
if (r.h->aborted) if (r.h->aborted)
return r.h; {
if (ignore_abort_)
goto restart;
return r.h;
}
if (!r.h->aut) if (!r.h->aut)
return nullptr; return nullptr;
if (r.state_names) if (r.state_names)
...@@ -1662,6 +1669,29 @@ namespace spot ...@@ -1662,6 +1669,29 @@ namespace spot
fix_properties(r); fix_properties(r);
return r.h; return r.h;
}; };
tgba_digraph_ptr
hoa_stream_parser::parse_strict(const bdd_dict_ptr& dict,
ltl::environment& env,
bool debug)
{
hoa_parse_error_list pel;
auto a = parse(pel, dict, env, debug);
if (!pel.empty())
{
std::ostringstream s;
if (format_hoa_parse_errors(s, filename_, pel))
throw parse_error(s.str());
}
if (!a)
return nullptr;
if (a->aborted)
throw parse_error("parsing aborted");
return a->aut;
}
} }
// Local Variables: // Local Variables:
......
...@@ -60,14 +60,21 @@ namespace spot ...@@ -60,14 +60,21 @@ namespace spot
class SPOT_API hoa_stream_parser class SPOT_API hoa_stream_parser
{ {
spot::location last_loc; spot::location last_loc;
std::string filename_;
bool ignore_abort_;
public: public:
hoa_stream_parser(const std::string& filename); hoa_stream_parser(const std::string& filename, bool ignore_abort = false);
~hoa_stream_parser(); ~hoa_stream_parser();
hoa_aut_ptr parse(hoa_parse_error_list& error_list, hoa_aut_ptr parse(hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict, const bdd_dict_ptr& dict,
ltl::environment& env = ltl::environment& env =
ltl::default_environment::instance(), ltl::default_environment::instance(),
bool debug = false); bool debug = false);
// Raises a parse_error on any syntax error
tgba_digraph_ptr parse_strict(const bdd_dict_ptr& dict,
ltl::environment& env =
ltl::default_environment::instance(),
bool debug = false);
}; };
/// \brief Build a spot::tgba_digraph from a HOA file or a neverclaim. /// \brief Build a spot::tgba_digraph from a HOA file or a neverclaim.
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche // Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -123,20 +123,11 @@ namespace spot ...@@ -123,20 +123,11 @@ namespace spot
environment& env = default_environment::instance(), environment& env = default_environment::instance(),
bool debug = false); 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(). /// \brief A simple wrapper to parse() and parse_lbt().
/// ///
/// This is mostly meant for interactive use. It first tries parse(); if /// 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 /// 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(). /// of the first call to parse() as a parse_error exception.
SPOT_API const formula* SPOT_API const formula*
parse_formula(const std::string& ltl_string, parse_formula(const std::string& ltl_string,
environment& env = default_environment::instance()); environment& env = default_environment::instance());
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -109,3 +109,15 @@ ...@@ -109,3 +109,15 @@
// Useful when forwarding methods such as: // Useful when forwarding methods such as:
// auto func(int param) SPOT_RETURN(implem_.func(param)); // auto func(int param) SPOT_RETURN(implem_.func(param));
#define SPOT_RETURN(code) -> decltype(code) { return code; } #define SPOT_RETURN(code) -> decltype(code) { return code; }
namespace spot
{
struct SPOT_API parse_error: public std::runtime_error
{
parse_error(const std::string& s)
: std::runtime_error(s)
{
}
};
}
...@@ -80,6 +80,46 @@ formula.__init__ = _formula_str_ctor ...@@ -80,6 +80,46 @@ formula.__init__ = _formula_str_ctor
formula.to_str = _formula_to_str formula.to_str = _formula_to_str
formula.show_ast = _render_formula_as_svg formula.show_ast = _render_formula_as_svg
def _tgba_to_str(a, format='hoa', opt=None):
format = format.lower()
if format == 'hoa':
ostr = ostringstream()
hoa_reachable(ostr, a, opt)
return ostr.str()
if format == 'dot':
ostr = ostringstream()
dotty_reachable(ostr, a, opt)
return ostr.str()
if format == 'spin':
ostr = ostringstream()
never_claim_reachable(ostr, a, opt)
return ostr.str()
if format == 'lbtt':
ostr = ostringstream()
lbtt_reachable(ostr, a, bool(opt))
return ostr.str()
raise ValueError("unknown string format: " + format)
def _tgba_save(a, filename, format='hoa', opt=None, append=False):
with open(filename, 'a' if append else 'w') as f:
s = a.to_str(format, opt)
f.write(s)
if s[-1] != '\n':
f.write('\n')
return a
tgba.to_str = _tgba_to_str
tgba.save = _tgba_save
def automata(filename):
p = hoa_stream_parser(filename, True)
while True:
a = p.parse_strict(_bdd_dict)
if a == None:
return
yield a
def translate(formula, output='tgba', pref='small', level='high', def translate(formula, output='tgba', pref='small', level='high',
complete=False): complete=False):
"""Translate a formula into an automaton. """Translate a formula into an automaton.
......
...@@ -74,6 +74,7 @@ namespace std { ...@@ -74,6 +74,7 @@ namespace std {
#include <sstream> #include <sstream>
#include <signal.h> #include <signal.h>
#include "misc/common.hh"
#include "misc/version.hh" #include "misc/version.hh"
#include "misc/minato.hh" #include "misc/minato.hh"
#include "misc/optionmap.hh" #include "misc/optionmap.hh"
...@@ -135,6 +136,7 @@ namespace std { ...@@ -135,6 +136,7 @@ namespace std {
#include "tgbaalgos/postproc.hh" #include "tgbaalgos/postproc.hh"
#include "tgbaalgos/stutter.hh" #include "tgbaalgos/stutter.hh"
#include "tgbaalgos/translate.hh" #include "tgbaalgos/translate.hh"
#include "tgbaalgos/hoa.hh"
#include "hoaparse/public.hh" #include "hoaparse/public.hh"
...@@ -182,7 +184,7 @@ using namespace spot; ...@@ -182,7 +184,7 @@ using namespace spot;
try { try {
$action $action
} }
catch (const spot::ltl::parse_error& e) catch (const spot::parse_error& e)
{ {
std::string er("\n"); std::string er("\n");
er += e.what(); er += e.what();
...@@ -278,6 +280,7 @@ namespace spot { ...@@ -278,6 +280,7 @@ namespace spot {
%include "tgbaalgos/postproc.hh" %include "tgbaalgos/postproc.hh"
%include "tgbaalgos/stutter.hh" %include "tgbaalgos/stutter.hh"
%include "tgbaalgos/translate.hh" %include "tgbaalgos/translate.hh"
%include "tgbaalgos/hoa.hh"
%include "hoaparse/public.hh" %include "hoaparse/public.hh"
......
...@@ -33,6 +33,7 @@ check_SCRIPTS = run ...@@ -33,6 +33,7 @@ check_SCRIPTS = run
TESTS = \ TESTS = \
alarm.py \ alarm.py \
automata.ipynb \ automata.ipynb \
automata-io.ipynb \
bddnqueen.py \ bddnqueen.py \
formulas.ipynb \ formulas.ipynb \
implies.py \ implies.py \
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment