Export tgba_parse() to the python interface.
* src/tgbaparse/public.hh: Hide tgba_parse_errorlist to SWIG. * wrap/python/spot.i: Export tgba_parse. * wrap/python/tests/parsetgba.py: New file. * wrap/python/tests/Makefile.am: Add it.
This commit is contained in:
parent
ebf4d2585d
commit
9559799637
5 changed files with 88 additions and 7 deletions
2
NEWS
2
NEWS
|
|
@ -16,6 +16,8 @@ New in spot 0.9a:
|
||||||
- Promises generated for formula of the form P(a U (b U c))
|
- Promises generated for formula of the form P(a U (b U c))
|
||||||
are reduced into P(c), avoiding the introduction of many
|
are reduced into P(c), avoiding the introduction of many
|
||||||
promises that imply each other.
|
promises that imply each other.
|
||||||
|
* The tgba_parse() function is now available via the Python
|
||||||
|
bindings.
|
||||||
* Bug fixes:
|
* Bug fixes:
|
||||||
- The random SERE generator was using the wrong operators
|
- The random SERE generator was using the wrong operators
|
||||||
for "and" and "or", mistaking And/Or with AndRat/OrRat.
|
for "and" and "or", mistaking And/Or with AndRat/OrRat.
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,9 @@
|
||||||
// Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire
|
// -*- coding: utf-8 -*-
|
||||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
|
||||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
// de l'Epita.
|
||||||
|
// 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.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -38,10 +41,15 @@ namespace spot
|
||||||
/// \addtogroup tgba_io
|
/// \addtogroup tgba_io
|
||||||
/// @{
|
/// @{
|
||||||
|
|
||||||
|
#ifndef SWIG
|
||||||
/// \brief A parse diagnostic with its location.
|
/// \brief A parse diagnostic with its location.
|
||||||
typedef std::pair<tgbayy::location, std::string> tgba_parse_error;
|
typedef std::pair<tgbayy::location, std::string> tgba_parse_error;
|
||||||
/// \brief A list of parser diagnostics, as filled by parse.
|
/// \brief A list of parser diagnostics, as filled by parse.
|
||||||
typedef std::list<tgba_parse_error> tgba_parse_error_list;
|
typedef std::list<tgba_parse_error> tgba_parse_error_list;
|
||||||
|
#else
|
||||||
|
// Turn parse_error_list into an opaque type for Swig.
|
||||||
|
struct tgba_parse_error_list {};
|
||||||
|
#endif
|
||||||
|
|
||||||
/// \brief Build a spot::tgba_explicit from a text file.
|
/// \brief Build a spot::tgba_explicit from a text file.
|
||||||
/// \param filename The name of the file to parse.
|
/// \param filename The name of the file to parse.
|
||||||
|
|
|
||||||
|
|
@ -107,6 +107,8 @@ namespace std {
|
||||||
#include "tgbaalgos/stats.hh"
|
#include "tgbaalgos/stats.hh"
|
||||||
#include "tgbaalgos/simulation.hh"
|
#include "tgbaalgos/simulation.hh"
|
||||||
|
|
||||||
|
#include "tgbaparse/public.hh"
|
||||||
|
|
||||||
using namespace spot::ltl;
|
using namespace spot::ltl;
|
||||||
using namespace spot;
|
using namespace spot;
|
||||||
%}
|
%}
|
||||||
|
|
@ -191,6 +193,8 @@ using namespace spot;
|
||||||
%feature("new") spot::tgba::succ_iter;
|
%feature("new") spot::tgba::succ_iter;
|
||||||
%feature("new") spot::tgba_succ_iterator::current_state;
|
%feature("new") spot::tgba_succ_iterator::current_state;
|
||||||
%feature("new") spot::simulation;
|
%feature("new") spot::simulation;
|
||||||
|
%feature("new") spot::tgba_parse;
|
||||||
|
|
||||||
// Help SWIG with namespace lookups.
|
// Help SWIG with namespace lookups.
|
||||||
#define ltl spot::ltl
|
#define ltl spot::ltl
|
||||||
%include "tgba/bdddict.hh"
|
%include "tgba/bdddict.hh"
|
||||||
|
|
@ -215,11 +219,11 @@ using namespace spot;
|
||||||
spot::explicit_graph<state_explicit_formula, tgba>;
|
spot::explicit_graph<state_explicit_formula, tgba>;
|
||||||
|
|
||||||
%template(explicit_string_tgba)
|
%template(explicit_string_tgba)
|
||||||
spot::explicit_graph<state_explicit_string, tgba>;
|
spot::tgba_explicit<state_explicit_string>;
|
||||||
%template(explicit_number_tgba)
|
|
||||||
spot::tgba_explicit<state_explicit_formula>;
|
|
||||||
%template(explicit__number_tgba)
|
%template(explicit__number_tgba)
|
||||||
spot::tgba_explicit<state_explicit_number>;
|
spot::tgba_explicit<state_explicit_number>;
|
||||||
|
%template(explicit_formula_tgba)
|
||||||
|
spot::tgba_explicit<state_explicit_formula>;
|
||||||
|
|
||||||
%template(explicit_string__tgba)
|
%template(explicit_string__tgba)
|
||||||
spot::explicit_conf<tgba_explicit<state_explicit_string>,
|
spot::explicit_conf<tgba_explicit<state_explicit_string>,
|
||||||
|
|
@ -249,6 +253,9 @@ using namespace spot;
|
||||||
%include "tgbaalgos/sccfilter.hh"
|
%include "tgbaalgos/sccfilter.hh"
|
||||||
%include "tgbaalgos/stats.hh"
|
%include "tgbaalgos/stats.hh"
|
||||||
%include "tgbaalgos/simulation.hh"
|
%include "tgbaalgos/simulation.hh"
|
||||||
|
|
||||||
|
%include "tgbaparse/public.hh"
|
||||||
|
|
||||||
#undef ltl
|
#undef ltl
|
||||||
|
|
||||||
%extend spot::ltl::formula {
|
%extend spot::ltl::formula {
|
||||||
|
|
@ -331,6 +338,13 @@ empty_parse_error_list()
|
||||||
return l;
|
return l;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
spot::tgba_parse_error_list
|
||||||
|
empty_tgba_parse_error_list()
|
||||||
|
{
|
||||||
|
tgba_parse_error_list l;
|
||||||
|
return l;
|
||||||
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
get_cout()
|
get_cout()
|
||||||
{
|
{
|
||||||
|
|
@ -381,3 +395,13 @@ __nonzero__()
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
%extend spot::tgba_parse_error_list {
|
||||||
|
|
||||||
|
bool
|
||||||
|
__nonzero__()
|
||||||
|
{
|
||||||
|
return !self->empty();
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
## Copyright (C) 2010 Labortatoire de Recherche et Développement de
|
## Copyright (C) 2010, 2012 Labortatoire de Recherche et Développement de
|
||||||
## l'EPITA.
|
## l'EPITA.
|
||||||
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
|
|
@ -38,4 +38,5 @@ TESTS = \
|
||||||
minato.py \
|
minato.py \
|
||||||
modgray.py \
|
modgray.py \
|
||||||
optionmap.py \
|
optionmap.py \
|
||||||
|
parsetgba.py \
|
||||||
setxor.py
|
setxor.py
|
||||||
|
|
|
||||||
46
wrap/python/tests/parsetgba.py
Executable file
46
wrap/python/tests/parsetgba.py
Executable file
|
|
@ -0,0 +1,46 @@
|
||||||
|
# -*- mode: python; coding: utf-8 -*-
|
||||||
|
# Copyright (C) 2012 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 2 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 Spot; see the file COPYING. If not, write to the Free
|
||||||
|
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
# 02111-1307, USA.
|
||||||
|
|
||||||
|
import os
|
||||||
|
import spot
|
||||||
|
|
||||||
|
contents = '''
|
||||||
|
acc = "b";
|
||||||
|
"a U b", "1", "b", "b";
|
||||||
|
"a U b", "a U b", "a & !b",;
|
||||||
|
"1", "1", "1", "b";
|
||||||
|
'''
|
||||||
|
|
||||||
|
filename = 'parsetgba.out'
|
||||||
|
|
||||||
|
out = open(filename, 'w+')
|
||||||
|
out.write(contents)
|
||||||
|
out.close()
|
||||||
|
|
||||||
|
d = spot.bdd_dict()
|
||||||
|
p = spot.empty_tgba_parse_error_list()
|
||||||
|
a = spot.tgba_parse(filename, p, d)
|
||||||
|
|
||||||
|
assert not p
|
||||||
|
|
||||||
|
spot.dotty_reachable(spot.get_cout(), a)
|
||||||
|
|
||||||
|
os.unlink(filename)
|
||||||
Loading…
Add table
Add a link
Reference in a new issue