Make it possible to output UTF-8 for dotty().
* src/tgba/tgbaexplicit.hh: Rerganize a bit to allow different functions to be used to format states. Add an enabled_utf8() method to tgba_explicit_formula. * src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc: Simplify the interface by not depending on dotty_decorator explicitely. * src/tgba/bddprint.hh (enable_utf8): New function. * src/tgba/bddprint.cc (enable_utf8): Implement it and use the global utf8 flag in other functions. * src/tgbatest/ltl2tgba.cc: Add an -8 option for UTF-8 outpout. * wrap/python/spot.i: Adjust for tgbexplicit.hh changes.
This commit is contained in:
Alexandre Duret-Lutz
parent
f082700fb2
commit
e93ceebafe
7 changed files with 235 additions and 101 deletions
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2009, 2012 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
|
||||
|
|
@ -36,6 +36,19 @@ namespace spot
|
|||
/// Global flag to enable Acc[x] output (instead of `x').
|
||||
static bool want_acc;
|
||||
|
||||
/// Global flag to enable UTF-8 output.
|
||||
static bool utf8;
|
||||
|
||||
static
|
||||
std::ostream& print_ltl(const ltl::formula* f, std::ostream& o)
|
||||
{
|
||||
if (utf8)
|
||||
ltl::to_utf8_string(f, o);
|
||||
else
|
||||
ltl::to_string(f, o);
|
||||
return o;
|
||||
}
|
||||
|
||||
/// Stream handler used by Buddy to display BDD variables.
|
||||
static void
|
||||
print_handler(std::ostream& o, int var)
|
||||
|
|
@ -52,12 +65,12 @@ namespace spot
|
|||
if (want_acc)
|
||||
{
|
||||
o << "Acc[";
|
||||
to_string(isi->second, o) << "]";
|
||||
print_ltl(isi->second, o) << "]";
|
||||
}
|
||||
else
|
||||
{
|
||||
o << "\"";
|
||||
to_string(isi->second, o) << "\"";
|
||||
print_ltl(isi->second, o) << "\"";
|
||||
}
|
||||
}
|
||||
else
|
||||
|
|
@ -65,14 +78,16 @@ namespace spot
|
|||
isi = dict->now_formula_map.find(var);
|
||||
if (isi != dict->now_formula_map.end())
|
||||
{
|
||||
o << "Now["; to_string(isi->second, o) << "]";
|
||||
o << "Now[";
|
||||
print_ltl(isi->second, o) << "]";
|
||||
}
|
||||
else
|
||||
{
|
||||
isi = dict->now_formula_map.find(var - 1);
|
||||
if (isi != dict->now_formula_map.end())
|
||||
{
|
||||
o << "Next["; to_string(isi->second, o) << "]";
|
||||
o << "Next[";
|
||||
print_ltl(isi->second, o) << "]";
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -202,7 +217,7 @@ namespace spot
|
|||
bdd_print_formula(std::ostream& os, const bdd_dict* d, bdd b)
|
||||
{
|
||||
const ltl::formula* f = bdd_to_formula(b, d);
|
||||
to_string(f, os);
|
||||
print_ltl(f, os);
|
||||
f->destroy();
|
||||
return os;
|
||||
}
|
||||
|
|
@ -237,4 +252,9 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
void
|
||||
enable_utf8()
|
||||
{
|
||||
utf8 = true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// Copyright (C) 2003, 2004, 2012 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -113,6 +113,8 @@ namespace spot
|
|||
std::ostream& bdd_print_table(std::ostream& os,
|
||||
const bdd_dict* dict, bdd b);
|
||||
|
||||
/// \brief Enable UTF-8 output for bdd printers.
|
||||
void enable_utf8();
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBA_BDDPRINT_HH
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
typedef Label Label_t;
|
||||
typedef Label label_t;
|
||||
typedef label_hash label_hash_t;
|
||||
|
||||
struct transition
|
||||
|
|
@ -154,12 +154,6 @@ namespace spot
|
|||
}
|
||||
|
||||
static const int default_val;
|
||||
static std::string to_string(int l)
|
||||
{
|
||||
std::stringstream ss;
|
||||
ss << l;
|
||||
return ss.str();
|
||||
}
|
||||
};
|
||||
|
||||
/// States labeled by a string
|
||||
|
|
@ -183,10 +177,6 @@ namespace spot
|
|||
}
|
||||
|
||||
static const std::string default_val;
|
||||
static std::string to_string(const std::string& l)
|
||||
{
|
||||
return l;
|
||||
}
|
||||
};
|
||||
|
||||
/// States labeled by a formula
|
||||
|
|
@ -210,10 +200,6 @@ namespace spot
|
|||
}
|
||||
|
||||
static const ltl::formula* default_val;
|
||||
static std::string to_string(const ltl::formula* l)
|
||||
{
|
||||
return ltl::to_string(l);
|
||||
}
|
||||
};
|
||||
|
||||
/// Successor iterators used by spot::tgba_explicit.
|
||||
|
|
@ -280,19 +266,22 @@ namespace spot
|
|||
bdd all_acceptance_conditions_;
|
||||
};
|
||||
|
||||
/// Graph implementation for automata representation
|
||||
/// Graph implementation for explicit automgon
|
||||
/// \ingroup tgba_representation
|
||||
template<typename State, typename Type>
|
||||
class explicit_graph: public Type
|
||||
{
|
||||
public:
|
||||
typedef typename State::label_t label_t;
|
||||
typedef typename State::label_hash_t label_hash_t;
|
||||
typedef typename State::transitions_t transitions_t;
|
||||
typedef typename State::transition transition;
|
||||
typedef State state;
|
||||
protected:
|
||||
typedef Sgi::hash_map<typename State::Label_t, State,
|
||||
typename State::label_hash_t> ls_map;
|
||||
typedef Sgi::hash_map<const State*, typename State::Label_t,
|
||||
ptr_hash<State> > sl_map;
|
||||
typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map;
|
||||
typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map;
|
||||
|
||||
public:
|
||||
typedef typename State::transition transition;
|
||||
|
||||
explicit_graph(bdd_dict* dict)
|
||||
: ls_(),
|
||||
|
|
@ -319,15 +308,14 @@ namespace spot
|
|||
t.condition = bddtrue;
|
||||
t.acceptance_conditions = bddfalse;
|
||||
|
||||
typename State::transitions_t::iterator i =
|
||||
typename transitions_t::iterator i =
|
||||
source->successors.insert(source->successors.end(), t);
|
||||
|
||||
return &*i;
|
||||
}
|
||||
|
||||
transition*
|
||||
create_transition(const typename State::Label_t& source,
|
||||
const typename State::Label_t& dest)
|
||||
create_transition(const label_t& source, const label_t& dest)
|
||||
{
|
||||
// It's important that the source be created before the
|
||||
// destination, so the first source encountered becomes the
|
||||
|
|
@ -361,19 +349,19 @@ namespace spot
|
|||
}
|
||||
|
||||
//old tgba explicit labelled interface
|
||||
bool has_state(const typename State::Label_t& name)
|
||||
bool has_state(const label_t& name)
|
||||
{
|
||||
return ls_.find(name) != ls_.end();
|
||||
}
|
||||
|
||||
const typename State::Label_t& get_label(const State* s) const
|
||||
const label_t& get_label(const State* s) const
|
||||
{
|
||||
typename sl_map::const_iterator i = sl_.find(s);
|
||||
assert(i != sl_.end());
|
||||
return i->second;
|
||||
}
|
||||
|
||||
const typename State::Label_t& get_label(const spot::state* s) const
|
||||
const label_t& get_label(const spot::state* s) const
|
||||
{
|
||||
const State* se = down_cast<const State*>(s);
|
||||
assert(se);
|
||||
|
|
@ -381,8 +369,7 @@ namespace spot
|
|||
}
|
||||
|
||||
transition*
|
||||
create_trainsition(const typename State::Label_t& source,
|
||||
const typename State::Label_t& dest)
|
||||
create_trainsition(const label_t& source, const label_t& dest)
|
||||
{
|
||||
// It's important that the source be created before the
|
||||
// destination, so the first source encountered becomes the
|
||||
|
|
@ -398,7 +385,7 @@ namespace spot
|
|||
typename ls_map::iterator i;
|
||||
for (i = ls_.begin(); i != ls_.end(); ++i)
|
||||
{
|
||||
typename State::transitions_t::iterator i2;
|
||||
typename transitions_t::iterator i2;
|
||||
for (i2 = i->second.successors.begin();
|
||||
i2 != i->second.successors.end(); ++i2)
|
||||
i2->acceptance_conditions = all - i2->acceptance_conditions;
|
||||
|
|
@ -411,21 +398,20 @@ namespace spot
|
|||
typename ls_map::iterator i;
|
||||
for (i = ls_.begin(); i != ls_.end(); ++i)
|
||||
{
|
||||
typename State::transitions_t::iterator t1;
|
||||
typename transitions_t::iterator t1;
|
||||
for (t1 = i->second.successors.begin();
|
||||
t1 != i->second.successors.end(); ++t1)
|
||||
{
|
||||
bdd acc = t1->acceptance_conditions;
|
||||
const state_explicit<typename State::Label_t,
|
||||
typename State::label_hash_t>* dest = t1->dest;
|
||||
const state_explicit<label_t, label_hash_t>* dest = t1->dest;
|
||||
|
||||
// Find another transition with the same destination and
|
||||
// acceptance conditions.
|
||||
typename State::transitions_t::iterator t2 = t1;
|
||||
typename transitions_t::iterator t2 = t1;
|
||||
++t2;
|
||||
while (t2 != i->second.successors.end())
|
||||
{
|
||||
typename State::transitions_t::iterator t2copy = t2++;
|
||||
typename transitions_t::iterator t2copy = t2++;
|
||||
if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
|
||||
{
|
||||
t1->condition |= t2copy->condition;
|
||||
|
|
@ -438,7 +424,7 @@ namespace spot
|
|||
|
||||
/// Return the state_explicit for \a name, creating the state if
|
||||
/// it does not exist.
|
||||
State* add_state(const typename State::Label_t& name)
|
||||
State* add_state(const label_t& name)
|
||||
{
|
||||
typename ls_map::iterator i = ls_.find(name);
|
||||
if (i == ls_.end())
|
||||
|
|
@ -458,7 +444,7 @@ namespace spot
|
|||
}
|
||||
|
||||
State*
|
||||
set_init_state(const typename State::Label_t& state)
|
||||
set_init_state(const label_t& state)
|
||||
{
|
||||
State* s = add_state(state);
|
||||
init_ = s;
|
||||
|
|
@ -472,14 +458,14 @@ namespace spot
|
|||
|
||||
while (i != ls_.end())
|
||||
{
|
||||
typename State::Label_t s = i->first;
|
||||
label_t s = i->first;
|
||||
|
||||
// Do not erase the same state twice(Because of possible aliases).
|
||||
if (sl_.erase(&(i->second)))
|
||||
i->second.destroy();
|
||||
|
||||
++i;
|
||||
destroy_key<typename State::Label_t> dest;
|
||||
destroy_key<label_t> dest;
|
||||
dest.destroy(s);
|
||||
}
|
||||
|
||||
|
|
@ -515,21 +501,33 @@ namespace spot
|
|||
->all_acceptance_conditions());
|
||||
}
|
||||
|
||||
//no need?
|
||||
|
||||
typedef std::string (*to_string_func_t)(const label_t& t);
|
||||
|
||||
void set_to_string_func(to_string_func_t f)
|
||||
{
|
||||
to_string_func_ = f;
|
||||
}
|
||||
|
||||
to_string_func_t get_to_string_func() const
|
||||
{
|
||||
return to_string_func_;
|
||||
}
|
||||
|
||||
virtual std::string format_state(const spot::state* state) const
|
||||
{
|
||||
const State* se = down_cast<const State*>(state);
|
||||
assert(se);
|
||||
typename sl_map::const_iterator i = sl_.find(se);
|
||||
assert(i != sl_.end());
|
||||
return State::to_string(i->second);
|
||||
assert(to_string_func_);
|
||||
return to_string_func_(i->second);
|
||||
}
|
||||
|
||||
/// old implementation in tgba_explicit_string
|
||||
/// Create an alias for a state. Any reference to \a alias_name
|
||||
/// will act as a reference to \a real_name.
|
||||
void add_state_alias(const typename State::Label_t& alias,
|
||||
const typename State::Label_t& real)
|
||||
void add_state_alias(const label_t& alias, const label_t& real)
|
||||
{
|
||||
ls_[alias] = *(add_state(real));
|
||||
}
|
||||
|
|
@ -614,7 +612,7 @@ namespace spot
|
|||
typename explicit_graph<State, tgba>::ls_map::iterator i;
|
||||
for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
|
||||
{
|
||||
typename State::transitions_t::iterator i2;
|
||||
typename transitions_t::iterator i2;
|
||||
for (i2 = i->second.successors.begin();
|
||||
i2 != i->second.successors.end(); ++i2)
|
||||
i2->acceptance_conditions &= neg;
|
||||
|
|
@ -639,11 +637,11 @@ namespace spot
|
|||
{
|
||||
const State* s = down_cast<const State*>(in);
|
||||
assert(s);
|
||||
const typename State::transitions_t& st = s->successors;
|
||||
const transitions_t& st = s->successors;
|
||||
|
||||
bdd res = bddfalse;
|
||||
|
||||
typename State::transitions_t::const_iterator i;
|
||||
typename transitions_t::const_iterator i;
|
||||
for (i = st.begin(); i != st.end(); ++i)
|
||||
res |= i->condition;
|
||||
|
||||
|
|
@ -654,11 +652,11 @@ namespace spot
|
|||
{
|
||||
const State* s = down_cast<const State*>(in);
|
||||
assert(s);
|
||||
const typename State::transitions_t& st = s->successors;
|
||||
const transitions_t& st = s->successors;
|
||||
|
||||
bdd res = bddtrue;
|
||||
|
||||
typename State::transitions_t::const_iterator i;
|
||||
typename transitions_t::const_iterator i;
|
||||
for (i = st.begin(); i != st.end(); ++i)
|
||||
res &= bdd_support(i->condition);
|
||||
|
||||
|
|
@ -674,17 +672,14 @@ namespace spot
|
|||
mutable bdd all_acceptance_conditions_;
|
||||
mutable bool all_acceptance_conditions_computed_;
|
||||
bdd neg_acceptance_conditions_;
|
||||
to_string_func_t to_string_func_;
|
||||
};
|
||||
|
||||
template <typename State>
|
||||
class tgba_explicit: public explicit_graph<State, tgba>
|
||||
{
|
||||
public:
|
||||
typedef typename State::transition transition;
|
||||
typedef State state;
|
||||
|
||||
tgba_explicit(bdd_dict* dict):
|
||||
explicit_graph<State,tgba>(dict)
|
||||
tgba_explicit(bdd_dict* dict): explicit_graph<State,tgba>(dict)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -702,11 +697,7 @@ namespace spot
|
|||
class sba_explicit: public explicit_graph<State, sba>
|
||||
{
|
||||
public:
|
||||
typedef typename State::transition transition;
|
||||
typedef State state;
|
||||
|
||||
sba_explicit(bdd_dict* dict):
|
||||
explicit_graph<State, sba>(dict)
|
||||
sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -741,15 +732,90 @@ namespace spot
|
|||
};
|
||||
|
||||
|
||||
// It is tempting to write
|
||||
//
|
||||
// template<template<typename T>class graph, typename Type>
|
||||
// class explicit_conf: public graph<T>
|
||||
//
|
||||
// to simplify the typedefs at the end of the file, however swig
|
||||
// cannot parse this syntax.
|
||||
|
||||
/// Configuration of graph automata
|
||||
/// \ingroup tgba_representation
|
||||
template<class graph, typename Type>
|
||||
class explicit_conf: public graph
|
||||
{
|
||||
public:
|
||||
explicit_conf(bdd_dict* d): graph(d)
|
||||
{
|
||||
set_to_string_func(to_string);
|
||||
};
|
||||
|
||||
static std::string to_string(const typename Type::label_t& l)
|
||||
{
|
||||
std::stringstream ss;
|
||||
ss << l;
|
||||
return ss.str();
|
||||
}
|
||||
};
|
||||
|
||||
template<class graph>
|
||||
class explicit_conf<graph, state_explicit_string>: public graph
|
||||
{
|
||||
public:
|
||||
explicit_conf(bdd_dict* d): graph(d)
|
||||
{
|
||||
set_to_string_func(to_string);
|
||||
};
|
||||
|
||||
static std::string to_string(const std::string& l)
|
||||
{
|
||||
return l;
|
||||
}
|
||||
};
|
||||
|
||||
template<class graph>
|
||||
class explicit_conf<graph, state_explicit_formula>: public graph
|
||||
{
|
||||
public:
|
||||
explicit_conf(bdd_dict* d): graph(d)
|
||||
{
|
||||
set_to_string_func(to_string);
|
||||
};
|
||||
|
||||
// Enable UTF8 output for the formulae that label states.
|
||||
void enable_utf8()
|
||||
{
|
||||
set_to_string_func(to_utf8_string);
|
||||
}
|
||||
|
||||
static std::string to_string(const ltl::formula* const& l)
|
||||
{
|
||||
return ltl::to_string(l);
|
||||
}
|
||||
|
||||
static std::string to_utf8_string(const ltl::formula* const& l)
|
||||
{
|
||||
return ltl::to_utf8_string(l);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
// Typedefs for tgba
|
||||
typedef tgba_explicit<state_explicit_string> tgba_explicit_string;
|
||||
typedef tgba_explicit<state_explicit_formula> tgba_explicit_formula;
|
||||
typedef tgba_explicit<state_explicit_number> tgba_explicit_number;
|
||||
typedef explicit_conf<tgba_explicit<state_explicit_string>,
|
||||
state_explicit_string> tgba_explicit_string;
|
||||
typedef explicit_conf<tgba_explicit<state_explicit_formula>,
|
||||
state_explicit_formula> tgba_explicit_formula;
|
||||
typedef explicit_conf<tgba_explicit<state_explicit_number>,
|
||||
state_explicit_number> tgba_explicit_number;
|
||||
|
||||
// Typedefs for sba
|
||||
typedef sba_explicit<state_explicit_string> sba_explicit_string;
|
||||
typedef sba_explicit<state_explicit_formula> sba_explicit_formula;
|
||||
typedef sba_explicit<state_explicit_number> sba_explicit_number;
|
||||
typedef explicit_conf<sba_explicit<state_explicit_string>,
|
||||
state_explicit_string> sba_explicit_string;
|
||||
typedef explicit_conf<sba_explicit<state_explicit_formula>,
|
||||
state_explicit_formula> sba_explicit_formula;
|
||||
typedef explicit_conf<sba_explicit<state_explicit_number>,
|
||||
state_explicit_number> sba_explicit_number;
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBA_TGBAEXPLICIT_HH
|
||||
|
|
|
|||
|
|
@ -24,10 +24,12 @@
|
|||
#include <ostream>
|
||||
#include "tgba/tgba.hh"
|
||||
#include "dotty.hh"
|
||||
#include "dottydec.hh"
|
||||
#include "tgba/bddprint.hh"
|
||||
#include "reachiter.hh"
|
||||
#include "misc/escape.hh"
|
||||
#include "tgba/tgbatba.hh"
|
||||
#include "tgba/formula2bdd.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -126,6 +128,8 @@ namespace spot
|
|||
dotty_reachable(std::ostream& os, const tgba* g,
|
||||
bool assume_sba, dotty_decorator* dd)
|
||||
{
|
||||
if (!dd)
|
||||
dd = dotty_decorator::instance();
|
||||
dotty_bfs d(os, g, assume_sba, dd);
|
||||
d.run();
|
||||
return os;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,7 @@
|
|||
// Copyright (C) 2003, 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// -*- coding: utf-
|
||||
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement 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
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -22,27 +25,29 @@
|
|||
#ifndef SPOT_TGBAALGOS_DOTTY_HH
|
||||
# define SPOT_TGBAALGOS_DOTTY_HH
|
||||
|
||||
#include "dottydec.hh"
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class tgba;
|
||||
class dotty_decorator;
|
||||
|
||||
/// \brief Print reachable states in dot format.
|
||||
/// \ingroup tgba_io
|
||||
///
|
||||
/// If assume_sba is set, this assumes that the automaton
|
||||
/// If \a assume_sba is set, this assumes that the automaton
|
||||
/// is an SBA and use double elipse to mark accepting states.
|
||||
///
|
||||
/// The \a dd argument allows to customize the output in various
|
||||
/// ways. See \ref tgba_dotty "this page" for a list of available
|
||||
/// decorators.
|
||||
/// decorators. If no decorator is specified, the dotty_decorator
|
||||
/// is used.
|
||||
/// labels the transitions are encoded in UTF-8.
|
||||
std::ostream&
|
||||
dotty_reachable(std::ostream& os,
|
||||
const tgba* g,
|
||||
bool assume_sba = false,
|
||||
dotty_decorator* dd = dotty_decorator::instance());
|
||||
dotty_decorator* dd = 0);
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBAALGOS_DOTTY_HH
|
||||
|
|
|
|||
|
|
@ -266,6 +266,7 @@ syntax(char* prog)
|
|||
<< "Miscellaneous options:" << std::endl
|
||||
<< " -0 produce minimal output dedicated to the paper"
|
||||
<< std::endl
|
||||
<< " -8 output UTF-8 formulae" << std::endl
|
||||
<< " -d turn on traces during parsing" << std::endl
|
||||
<< " -T time the different phases of the translation"
|
||||
<< std::endl
|
||||
|
|
@ -281,6 +282,7 @@ main(int argc, char** argv)
|
|||
|
||||
bool debug_opt = false;
|
||||
bool paper_opt = false;
|
||||
bool utf8_opt = false;
|
||||
enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
|
||||
enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
|
||||
enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
|
||||
|
|
@ -304,7 +306,7 @@ main(int argc, char** argv)
|
|||
spot::ltl::ltl_simplifier_options redopt(false, false, false, false, false);
|
||||
bool scc_filter_all = false;
|
||||
bool symbolic_scc_pruning = false;
|
||||
bool display_reduce_form = false;
|
||||
bool display_reduced_form = false;
|
||||
bool post_branching = false;
|
||||
bool fair_loop_approx = false;
|
||||
bool graph_run_opt = false;
|
||||
|
|
@ -339,6 +341,11 @@ main(int argc, char** argv)
|
|||
{
|
||||
paper_opt = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-8"))
|
||||
{
|
||||
utf8_opt = true;
|
||||
spot::enable_utf8();
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-a"))
|
||||
{
|
||||
output = 2;
|
||||
|
|
@ -609,7 +616,7 @@ main(int argc, char** argv)
|
|||
}
|
||||
else if (!strcmp(argv[formula_index], "-rd"))
|
||||
{
|
||||
display_reduce_form = true;
|
||||
display_reduced_form = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-RDS"))
|
||||
{
|
||||
|
|
@ -772,9 +779,9 @@ main(int argc, char** argv)
|
|||
|
||||
if (f || from_file)
|
||||
{
|
||||
const spot::tgba_bdd_concrete* concrete = 0;
|
||||
spot::tgba_bdd_concrete* concrete = 0;
|
||||
const spot::tgba* to_free = 0;
|
||||
const spot::tgba* a = 0;
|
||||
spot::tgba* a = 0;
|
||||
|
||||
if (from_file)
|
||||
{
|
||||
|
|
@ -822,9 +829,14 @@ main(int argc, char** argv)
|
|||
f->destroy();
|
||||
tm.stop("reducing formula");
|
||||
f = t;
|
||||
if (display_reduce_form)
|
||||
if (display_reduced_form)
|
||||
{
|
||||
if (utf8_opt)
|
||||
std::cout << spot::ltl::to_utf8_string(f) << std::endl;
|
||||
else
|
||||
std::cout << spot::ltl::to_string(f) << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
if (f->is_psl_formula()
|
||||
&& !f->is_ltl_formula()
|
||||
|
|
@ -900,14 +912,13 @@ main(int argc, char** argv)
|
|||
if (scc_filter)
|
||||
{
|
||||
tm.start("reducing A_f w/ SCC");
|
||||
a = aut_scc = spot::scc_filter(a, scc_filter_all);
|
||||
aut_scc = a = spot::scc_filter(a, scc_filter_all);
|
||||
tm.stop("reducing A_f w/ SCC");
|
||||
}
|
||||
|
||||
const spot::tgba_tba_proxy* degeneralized = 0;
|
||||
const spot::tgba_sgba_proxy* state_labeled = 0;
|
||||
const spot::tgba* degeneralized = 0;
|
||||
|
||||
const spot::tgba* minimized = 0;
|
||||
spot::tgba* minimized = 0;
|
||||
if (opt_minimize)
|
||||
{
|
||||
tm.start("obligation minimization");
|
||||
|
|
@ -961,39 +972,39 @@ main(int argc, char** argv)
|
|||
{
|
||||
if (degeneralize_opt == DegenTBA)
|
||||
{
|
||||
a = degeneralized = new spot::tgba_tba_proxy(a);
|
||||
degeneralized = a = new spot::tgba_tba_proxy(a);
|
||||
}
|
||||
else if (degeneralize_opt == DegenSBA)
|
||||
{
|
||||
a = degeneralized = new spot::tgba_sba_proxy(a);
|
||||
degeneralized = a = new spot::tgba_sba_proxy(a);
|
||||
assume_sba = true;
|
||||
}
|
||||
else if (labeling_opt == StateLabeled)
|
||||
{
|
||||
a = state_labeled = new spot::tgba_sgba_proxy(a);
|
||||
degeneralized = a = new spot::tgba_sgba_proxy(a);
|
||||
}
|
||||
}
|
||||
|
||||
if (opt_monitor)
|
||||
{
|
||||
tm.start("Monitor minimization");
|
||||
a = minimized = minimize_monitor(a);
|
||||
minimized = a = minimize_monitor(a);
|
||||
tm.stop("Monitor minimization");
|
||||
assume_sba = false; // All states are accepting, so double
|
||||
// circles in the dot output are
|
||||
// pointless.
|
||||
}
|
||||
|
||||
const spot::tgba_explicit_string* expl = 0;
|
||||
const spot::tgba* expl = 0;
|
||||
switch (dupexp)
|
||||
{
|
||||
case NoneDup:
|
||||
break;
|
||||
case BFS:
|
||||
a = expl = tgba_dupexp_bfs(a);
|
||||
expl = a = tgba_dupexp_bfs(a);
|
||||
break;
|
||||
case DFS:
|
||||
a = expl = tgba_dupexp_dfs(a);
|
||||
expl = a = tgba_dupexp_dfs(a);
|
||||
break;
|
||||
}
|
||||
|
||||
|
|
@ -1001,7 +1012,7 @@ main(int argc, char** argv)
|
|||
|
||||
if (system)
|
||||
{
|
||||
a = product = product_to_free = new spot::tgba_product(system, a);
|
||||
product = product_to_free = a = new spot::tgba_product(system, a);
|
||||
|
||||
assume_sba = false;
|
||||
|
||||
|
|
@ -1013,12 +1024,12 @@ main(int argc, char** argv)
|
|||
degeneralize_opt = DegenTBA;
|
||||
if (degeneralize_opt == DegenTBA)
|
||||
{
|
||||
a = product = product_degeneralized =
|
||||
product = product_degeneralized = a =
|
||||
new spot::tgba_tba_proxy(product);
|
||||
}
|
||||
else if (degeneralize_opt == DegenSBA)
|
||||
{
|
||||
a = product = product_degeneralized =
|
||||
product = product_degeneralized = a =
|
||||
new spot::tgba_sba_proxy(product);
|
||||
assume_sba = true;
|
||||
}
|
||||
|
|
@ -1047,6 +1058,11 @@ main(int argc, char** argv)
|
|||
a = new spot::future_conditions_collector(a, true);
|
||||
}
|
||||
|
||||
if (utf8_opt)
|
||||
if (spot::tgba_explicit_formula* tef =
|
||||
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
||||
tef->enable_utf8();
|
||||
|
||||
if (output != -1)
|
||||
{
|
||||
tm.start("producing output");
|
||||
|
|
@ -1266,7 +1282,7 @@ main(int argc, char** argv)
|
|||
{
|
||||
spot::tgba* ar =
|
||||
spot::tgba_run_to_tgba(a, run);
|
||||
spot::dotty_reachable(std::cout, ar);
|
||||
spot::dotty_reachable(std::cout, ar, false);
|
||||
delete ar;
|
||||
}
|
||||
else
|
||||
|
|
@ -1301,7 +1317,6 @@ main(int argc, char** argv)
|
|||
delete minimized;
|
||||
delete degeneralized;
|
||||
delete aut_scc;
|
||||
delete state_labeled;
|
||||
delete to_free;
|
||||
delete echeck_inst;
|
||||
delete temp_dir_sim;
|
||||
|
|
|
|||
|
|
@ -213,9 +213,23 @@ using namespace spot;
|
|||
spot::explicit_graph<state_explicit_number, tgba>;
|
||||
%template(explicit_graph__formula_tgba)
|
||||
spot::explicit_graph<state_explicit_formula, tgba>;
|
||||
%template(tgba_explicit__string) spot::tgba_explicit<state_explicit_string>;
|
||||
%template(tgba_explicit__number) spot::tgba_explicit<state_explicit_number>;
|
||||
%template(tgba_explicit__formula) spot::tgba_explicit<state_explicit_formula>;
|
||||
|
||||
%template(explicit_string_tgba)
|
||||
spot::explicit_graph<state_explicit_string, tgba>;
|
||||
%template(explicit_number_tgba)
|
||||
spot::tgba_explicit<state_explicit_formula>;
|
||||
%template(explicit__number_tgba)
|
||||
spot::tgba_explicit<state_explicit_number>;
|
||||
|
||||
%template(explicit_string__tgba)
|
||||
spot::explicit_conf<tgba_explicit<state_explicit_string>,
|
||||
state_explicit_string>;
|
||||
%template(explicit_number__tgba)
|
||||
spot::explicit_conf<tgba_explicit<state_explicit_number>,
|
||||
state_explicit_number>;
|
||||
%template(explicit_formula__tgba)
|
||||
spot::explicit_conf<tgba_explicit<state_explicit_formula>,
|
||||
state_explicit_formula>;
|
||||
|
||||
%include "tgbaalgos/dottydec.hh"
|
||||
%include "tgbaalgos/dotty.hh"
|
||||
|
|
@ -302,6 +316,14 @@ minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f)
|
|||
return res;
|
||||
}
|
||||
|
||||
void
|
||||
tgba_enable_utf8(spot::tgba* a)
|
||||
{
|
||||
if (spot::tgba_explicit_formula* tef =
|
||||
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
||||
tef->enable_utf8();
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list
|
||||
empty_parse_error_list()
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue