python: better bindings for testing automata
* src/taalgos/dotty.cc, src/taalgos/dotty.hh: Add an interface similar to that of tgba/dotty.hh, even if we have to ignore most options. * src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh: Add an option to display the intermediate automaton with explicit stuttering transitions, for the purpose of making demonstrations. * src/tgba/tgbagraph.hh: Tweak the file so that SWIG can read it. * wrap/python/spot.py: Add wrappers for testing automata. * wrap/python/spot_impl.i: Fix support for atomic_prop_collect_as_bdd, and include a few more files. * wrap/python/tests/testingaut.ipynb: New file. * wrap/python/tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz
parent
7bb183b929
commit
16204e8e61
9 changed files with 796 additions and 31 deletions
|
|
@ -23,6 +23,8 @@
|
|||
#include "reachiter.hh"
|
||||
#include "misc/escape.hh"
|
||||
#include "misc/bareword.hh"
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -30,10 +32,83 @@ namespace spot
|
|||
{
|
||||
class dotty_bfs : public ta_reachable_iterator_breadth_first
|
||||
{
|
||||
void
|
||||
parse_opts(const char* options)
|
||||
{
|
||||
const char* orig = options;
|
||||
while (char c = *options++)
|
||||
switch (c)
|
||||
{
|
||||
case '.':
|
||||
{
|
||||
// Copy the value in a string, so future calls to
|
||||
// parse_opts do not fail if the environment has
|
||||
// changed. (This matters particularly in an ipython
|
||||
// notebook, where it is tempting to redefine
|
||||
// SPOT_DOTDEFAULT.)
|
||||
static std::string def = []()
|
||||
{
|
||||
auto s = getenv("SPOT_DOTDEFAULT");
|
||||
return s ? s : "";
|
||||
}();
|
||||
// Prevent infinite recursions...
|
||||
if (orig == def.c_str())
|
||||
throw std::runtime_error
|
||||
(std::string("SPOT_DOTDEFAULT should not contain '.'"));
|
||||
if (!def.empty())
|
||||
parse_opts(def.c_str());
|
||||
break;
|
||||
}
|
||||
case 'A':
|
||||
opt_hide_sets_ = true;
|
||||
break;
|
||||
case 'c':
|
||||
opt_circles_ = true;
|
||||
break;
|
||||
case 'h':
|
||||
opt_horizontal_ = true;
|
||||
break;
|
||||
case 'f':
|
||||
if (*options != '(')
|
||||
throw std::runtime_error
|
||||
(std::string("invalid font specification for dotty()"));
|
||||
{
|
||||
auto* end = strchr(++options, ')');
|
||||
if (!end)
|
||||
throw std::runtime_error
|
||||
(std::string("invalid font specification for dotty()"));
|
||||
opt_font_ = std::string(options, end - options);
|
||||
options = end + 1;
|
||||
}
|
||||
break;
|
||||
case 'v':
|
||||
opt_horizontal_ = false;
|
||||
break;
|
||||
case 'a':
|
||||
case 'b':
|
||||
case 'n':
|
||||
case 'N':
|
||||
case 'r':
|
||||
case 'R':
|
||||
case 's':
|
||||
case 't':
|
||||
// All these options are implemented by dotty() on TGBA,
|
||||
// but are not implemented here. We simply ignore them,
|
||||
// because raising an exception if they are in
|
||||
// SPOT_DEFAULT would be annoying.
|
||||
break;
|
||||
default:
|
||||
throw std::runtime_error
|
||||
(std::string("unknown option for dotty(): ") + c);
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
dotty_bfs(std::ostream& os, const const_ta_ptr& a) :
|
||||
dotty_bfs(std::ostream& os, const const_ta_ptr& a,
|
||||
const char* opt) :
|
||||
ta_reachable_iterator_breadth_first(a), os_(os)
|
||||
{
|
||||
parse_opts(opt ? opt : ".");
|
||||
}
|
||||
|
||||
void
|
||||
|
|
@ -41,6 +116,16 @@ namespace spot
|
|||
{
|
||||
os_ << "digraph G {\n";
|
||||
|
||||
if (opt_horizontal_)
|
||||
os_ << " rankdir=LR\n";
|
||||
if (opt_circles_)
|
||||
os_ << " node [shape=\"circle\"]\n";
|
||||
if (!opt_font_.empty())
|
||||
os_ << " fontname=\"" << opt_font_
|
||||
<< "\"\n node [fontname=\"" << opt_font_
|
||||
<< "\"]\n edge [fontname=\"" << opt_font_
|
||||
<< "\"]\n";
|
||||
|
||||
// Always copy the environment variable into a static string,
|
||||
// so that we (1) look it up once, but (2) won't crash if the
|
||||
// environment is changed.
|
||||
|
|
@ -120,8 +205,12 @@ namespace spot
|
|||
if (label.empty())
|
||||
label = "{}";
|
||||
|
||||
label += "\n";
|
||||
label += t_automata_->acc().format(si->current_acceptance_conditions());
|
||||
if (!opt_hide_sets_)
|
||||
{
|
||||
label += "\n";
|
||||
label += t_automata_->acc().
|
||||
format(si->current_acceptance_conditions());
|
||||
}
|
||||
|
||||
os_ << " " << in << " -> " << out << " [label=\"";
|
||||
escape_str(os_, label);
|
||||
|
|
@ -131,14 +220,19 @@ namespace spot
|
|||
private:
|
||||
std::ostream& os_;
|
||||
spot::state* artificial_initial_state_;
|
||||
|
||||
bool opt_horizontal_ = true;
|
||||
bool opt_circles_ = false;
|
||||
bool opt_hide_sets_ = false;
|
||||
std::string opt_font_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
dotty_reachable(std::ostream& os, const const_ta_ptr& a)
|
||||
dotty_reachable(std::ostream& os, const const_ta_ptr& a, const char* opt)
|
||||
{
|
||||
dotty_bfs d(os, a);
|
||||
dotty_bfs d(os, a, opt);
|
||||
d.run();
|
||||
return os;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2013, 2014 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2010, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -25,5 +25,6 @@
|
|||
namespace spot
|
||||
{
|
||||
SPOT_API std::ostream&
|
||||
dotty_reachable(std::ostream& os, const const_ta_ptr& a);
|
||||
dotty_reachable(std::ostream& os, const const_ta_ptr& a,
|
||||
const char* opt = nullptr);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -410,7 +410,8 @@ namespace spot
|
|||
build_ta(const ta_explicit_ptr& ta, bdd atomic_propositions_set_,
|
||||
bool degeneralized,
|
||||
bool single_pass_emptiness_check,
|
||||
bool artificial_livelock_state_mode)
|
||||
bool artificial_livelock_state_mode,
|
||||
bool no_livelock)
|
||||
{
|
||||
|
||||
std::stack<state_ta_explicit*> todo;
|
||||
|
|
@ -517,6 +518,9 @@ namespace spot
|
|||
delete tgba_succ_it;
|
||||
}
|
||||
|
||||
if (no_livelock)
|
||||
return ta;
|
||||
|
||||
state_ta_explicit* artificial_livelock_acc_state = 0;
|
||||
|
||||
trace << "*** build_ta: artificial_livelock_acc_state_mode = ***"
|
||||
|
|
@ -541,8 +545,10 @@ namespace spot
|
|||
|
||||
ta_explicit_ptr
|
||||
tgba_to_ta(const const_tgba_ptr& tgba_, bdd atomic_propositions_set_,
|
||||
bool degeneralized, bool artificial_initial_state_mode,
|
||||
bool single_pass_emptiness_check, bool artificial_livelock_state_mode)
|
||||
bool degeneralized, bool artificial_initial_state_mode,
|
||||
bool single_pass_emptiness_check,
|
||||
bool artificial_livelock_state_mode,
|
||||
bool no_livelock)
|
||||
{
|
||||
ta_explicit_ptr ta;
|
||||
|
||||
|
|
@ -563,7 +569,8 @@ namespace spot
|
|||
|
||||
// build ta automaton
|
||||
build_ta(ta, atomic_propositions_set_, degeneralized,
|
||||
single_pass_emptiness_check, artificial_livelock_state_mode);
|
||||
single_pass_emptiness_check, artificial_livelock_state_mode,
|
||||
no_livelock);
|
||||
|
||||
// (degeneralized=true) => TA
|
||||
if (degeneralized)
|
||||
|
|
@ -607,7 +614,7 @@ namespace spot
|
|||
// build a Generalized TA automaton involving a single_pass_emptiness_check
|
||||
// (without an artificial livelock state):
|
||||
auto ta = tgta->get_ta();
|
||||
build_ta(ta, atomic_propositions_set_, false, true, false);
|
||||
build_ta(ta, atomic_propositions_set_, false, true, false, false);
|
||||
|
||||
trace << "***tgba_to_tgbta: POST build_ta***" << std::endl;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -75,6 +75,9 @@ namespace spot
|
|||
/// Buchi-accepting state, then s has no successors. A STA product requires
|
||||
/// only one-pass emptiness check algorithm (see spot::ta_check::check)
|
||||
///
|
||||
/// \param no_livelock when set, this disable the replacement of
|
||||
/// stuttering components by livelock states. Use this flag to
|
||||
/// demonstrate an intermediate step of the construction.
|
||||
///
|
||||
/// \return A spot::ta_explicit that recognizes the same language as the
|
||||
/// TGBA \a tgba_to_convert.
|
||||
|
|
@ -83,7 +86,8 @@ namespace spot
|
|||
bool degeneralized = true,
|
||||
bool artificial_initial_state_mode = true,
|
||||
bool single_pass_emptiness_check = false,
|
||||
bool artificial_livelock_state_mode = false);
|
||||
bool artificial_livelock_state_mode = false,
|
||||
bool no_livelock = false);
|
||||
|
||||
/// \ingroup tgba_ta
|
||||
/// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue