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

replace sba_explicit_* by tgba_digraph, and use tgba_digraph is postproc

Browse source 
This is a huge patch.  tgba_digraph are equiped with some boolean
properties that can be used to indicate whether they represent SBA
(and will carry more informations later).  All algorithms that produce
or use sba_explicit_* automata are changed to use tgba_digraph.
postproc has been rewritten using only tgba_digraph, and this required
changing the return types of many algorithms from tgba* to
tgba_digraph*.

* src/bin/dstar2tgba.cc, src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc,
src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/postproc.cc,
src/tgbaalgos/postproc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/stripacc.cc,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.cc,
src/tgbaalgos/translate.hh, src/tgbatest/ltl2tgba.cc,
wrap/python/spot.i: Update.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-11 19:08:14 +02:00
parent 637aeff2d3
commit 6c9d5e4bb3
26 changed files with 296 additions and 257 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/bin/dstar2tgba.cc
View file

@ -307,8 +307,8 @@ namespace
const xtime_t before = gethrxtime();
spot::tgba* nba = spot::dstar_to_tgba(daut);
const spot::tgba* aut = post.run(nba, 0);
auto nba = spot::dstar_to_tgba(daut);
auto aut = post.run(nba, 0);
const xtime_t after = gethrxtime();
const double prec = XTIME_PRECISION;

4
src/bin/ltlfilt.cc
View file

@ -548,8 +548,8 @@ namespace
// other reasons.
if (matched && obligation)
{
spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict());
spot::tgba* min = minimize_obligation(aut, f);
auto aut = ltl_to_tgba_fm(f, simpl.get_dict());
auto min = minimize_obligation(aut, f);
assert(min);
if (aut == min)
{

4
src/dstarparse/dra2ba.cc
View file

@ -49,7 +49,7 @@ namespace spot
// This function is defined in nra2nba.cc, and used only here.
SPOT_LOCAL
tgba* nra_to_nba(const dstar_aut* nra, const tgba* aut);
tgba_digraph* nra_to_nba(const dstar_aut* nra, const tgba* aut);
namespace
{
@ -320,7 +320,7 @@ namespace spot
}
tgba* dra_to_ba(const dstar_aut* dra, bool* dba)
tgba_digraph* dra_to_ba(const dstar_aut* dra, bool* dba)
{
assert(dra->type == Rabin);

2
src/dstarparse/dstar2tgba.cc
View file

@ -21,7 +21,7 @@
namespace spot
{
tgba*
tgba_digraph*
dstar_to_tgba(const dstar_aut* daut)
{
switch (daut->type)

4
src/dstarparse/nra2nba.cc
View file

@ -122,7 +122,7 @@ namespace spot
// In dra_to_dba() we call this function with a second argument
// that is a masked version of nra->aut.
SPOT_LOCAL
tgba* nra_to_nba(const dstar_aut* nra, const tgba* aut)
tgba_digraph* nra_to_nba(const dstar_aut* nra, const tgba* aut)
{
assert(nra->type == Rabin);
nra_to_nba_worker w(nra, aut);
@ -134,7 +134,7 @@ namespace spot
}
SPOT_API
tgba* nra_to_nba(const dstar_aut* nra)
tgba_digraph* nra_to_nba(const dstar_aut* nra)
{
return nra_to_nba(nra, nra->aut);
}

2
src/dstarparse/nsa2tgba.cc
View file

@ -99,7 +99,7 @@ namespace spot
}
SPOT_API
tgba* nsa_to_tgba(const dstar_aut* nsa)
tgba_digraph* nsa_to_tgba(const dstar_aut* nsa)
{
assert(nsa->type == Streett);
tgba_digraph* a = nsa->aut;

10
src/dstarparse/public.hh
View file

@ -106,14 +106,14 @@ namespace spot
/// \brief Convert a non-deterministic Rabin automaton into a
/// non-deterministic Büchi automaton.
SPOT_API tgba*
SPOT_API tgba_digraph*
nra_to_nba(const dstar_aut* nra);
/// \brief Convert a non-deterministic Rabin automaton into a
/// non-deterministic Büchi automaton.
///
/// This version simply ignores all states in \a ignore.
SPOT_API tgba*
SPOT_API tgba_digraph*
nra_to_nba(const dstar_aut* nra, const state_set* ignore);
/// \brief Convert a deterministic Rabin automaton into a
@ -132,18 +132,18 @@ namespace spot
/// If the optional \a dba_output argument is non-null, the
/// pointed Boolean will be updated to indicate whether the
/// returned Büchi automaton is deterministic.
SPOT_API tgba*
SPOT_API tgba_digraph*
dra_to_ba(const dstar_aut* dra, bool* dba_output = 0);
/// \brief Convert a non-deterministic Streett automaton into a
/// non-deterministic tgba.
SPOT_API tgba*
SPOT_API tgba_digraph*
nsa_to_tgba(const dstar_aut* nra);
/// \brief Convert a Rabin or Streett automaton into a TGBA.
///
/// This function calls dra_to_ba() or nsa_to_tgba().
SPOT_API tgba*
SPOT_API tgba_digraph*
dstar_to_tgba(const dstar_aut* dstar);

42
src/tgba/tgbagraph.hh
View file

@ -411,6 +411,48 @@ namespace spot
}
g_.defrag();
}
protected:
unsigned bprops_ = 0;
public:
enum bprop {
StateBasedAcc = 1,
SingleAccSet = 2,
SBA = StateBasedAcc | SingleAccSet,
};
bool get_bprop(bprop p) const
{
return (bprops_ & p) == p;
}
void set_bprop(bprop p)
{
bprops_ |= p;
}
void clear_bprop(bprop p)
{
bprops_ &= ~p;
}
bool state_is_accepting(unsigned s) const
{
assert(get_bprop(StateBasedAcc));
for (auto& t: g_.out(s))
// Stop at the first transition, since the remaining should be
// labeled identically.
return t.acc == all_acceptance_conditions_;
return false;
}
bool state_is_accepting(const state* s) const
{
return state_is_accepting(state_number(s));
}
};
}

20
src/tgba/tgbasafracomplement.cc
View file

@ -34,7 +34,6 @@
#include "ltlast/constant.hh"
#include "tgbaalgos/dotty.hh"
#include "tgba/tgbasafracomplement.hh"
#include "tgba/sba.hh"
#include "tgbaalgos/degen.hh"
namespace spot
@ -54,7 +53,7 @@ namespace spot
/// \brief Automaton with Safra's tree as states.
struct safra_tree_automaton
{
safra_tree_automaton(const tgba* sba);
safra_tree_automaton(const tgba_digraph* sba);
~safra_tree_automaton();
typedef std::map<bdd, const safra_tree*, bdd_less_than> transition_list;
typedef
@ -67,14 +66,14 @@ namespace spot
int get_nb_acceptance_pairs() const;
safra_tree* get_initial_state() const;
void set_initial_state(safra_tree* s);
const tgba* get_sba(void) const
const tgba_digraph* get_sba(void) const
{
return a_;
}
private:
mutable int max_nb_pairs_;
safra_tree* initial_state;
const tgba* a_;
const tgba_digraph* a_;
};
/// \brief A Safra tree, used as state during the determinization
@ -112,7 +111,7 @@ namespace spot
int max_name() const;
// Operations to get successors of a tree.
safra_tree* branch_accepting(const sba& a);
safra_tree* branch_accepting(const tgba_digraph& a);
safra_tree* succ_create(const bdd& condition,
cache_t& cache_transition);
safra_tree* normalize_siblings();
@ -316,7 +315,7 @@ namespace spot
/// is inserted with the set of all accepting states of \c nodes
/// as label and an unused name.
safra_tree*
safra_tree::branch_accepting(const sba& a)
safra_tree::branch_accepting(const tgba_digraph& a)
{
for (auto c: children)
c->branch_accepting(a);
@ -574,7 +573,8 @@ namespace spot
private:
typedef std::set<int> atomic_list_t;
typedef std::set<bdd, bdd_less_than> conjunction_list_t;
static void retrieve_atomics(const safra_tree* node, sba* sba_aut,
static void retrieve_atomics(const safra_tree* node,
tgba_digraph* sba_aut,
safra_tree::cache_t& cache,
atomic_list_t& atomic_list);
static void set_atomic_list(atomic_list_t& list, bdd condition);
@ -587,7 +587,7 @@ namespace spot
safra_determinisation::create_safra_automaton(const tgba* a)
{
// initialization.
sba* sba_aut = degeneralize(a);
auto sba_aut = degeneralize(a);
safra_tree_automaton* st = new safra_tree_automaton(sba_aut);
@ -664,7 +664,7 @@ namespace spot
/// of the states in the label of the node.
void
safra_determinisation::retrieve_atomics(const safra_tree* node,
sba* sba_aut,
tgba_digraph* sba_aut,
safra_tree::cache_t& cache,
atomic_list_t& atomic_list)
{
@ -1031,7 +1031,7 @@ namespace spot
// safra_tree_automaton
////////////////////////
safra_tree_automaton::safra_tree_automaton(const tgba* a)
safra_tree_automaton::safra_tree_automaton(const tgba_digraph* a)
: max_nb_pairs_(-1), initial_state(0), a_(a)
{
a->get_dict()->register_all_variables_of(a, this);

13
src/tgbaalgos/compsusp.cc
View file

@ -349,7 +349,7 @@ namespace spot
}
tgba*
tgba_digraph*
compsusp(const ltl::formula* f, bdd_dict* dict,
bool no_wdba, bool no_simulation,
bool early_susp, bool no_susp_product, bool wdba_smaller,
@ -371,18 +371,11 @@ namespace spot
if (!no_wdba)
{
tgba* min = minimize_obligation(res, g, 0, wdba_smaller);
tgba_digraph* min = minimize_obligation(res, g, 0, wdba_smaller);
if (min != res)
{
delete res;
// FIXME: minimize_obligation does not yet return a
// tgba_digraph, so we convert the result using dupexp.
// Once minimize_obligation is fixed, we should remove the
// call to dupexp.
assert(dynamic_cast<tgba_digraph*>(min) == nullptr);
res = tgba_dupexp_dfs(min);
delete min;
//res = min;
res = min;
no_simulation = true;
}
}

3
src/tgbaalgos/compsusp.hh
View file

@ -21,6 +21,7 @@
# define SPOT_TGBAALGOS_COMPSUSP_HH
#include "ltlast/formula.hh"
#include "tgba/tgbagraph.hh"
namespace spot
{
@ -49,7 +50,7 @@ namespace spot
/// This interface is subject to change, and clients aiming for
/// long-term stability should better use the services of the
/// spot::translator class instead.
SPOT_API tgba*
SPOT_API tgba_digraph*
compsusp(const ltl::formula* f, bdd_dict* dict,
bool no_wdba = false, bool no_simulation = false,
bool early_susp = false, bool no_susp_product = false,

50
src/tgbaalgos/degen.cc
View file

@ -19,7 +19,7 @@
#include "degen.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbagraph.hh"
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include "ltlast/constant.hh"
@ -251,7 +251,7 @@ namespace spot
};
}
sba*
tgba_digraph*
degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{
@ -259,8 +259,9 @@ namespace spot
bdd_dict* dict = a->get_dict();
// The result (degeneralized) automaton uses numbered states.
sba_explicit_number* res = new sba_explicit_number(dict);
// The result automaton is an SBA.
auto res = new tgba_digraph(dict);
res->set_bprop(tgba_digraph::SBA);
// We use the same BDD variables as the input, except for the
// acceptance.
@ -314,7 +315,7 @@ namespace spot
// (dest*2+acc) where dest is the destination state number, and
// acc is 1 iff the transition is accepting. The source
// is always that of the current iteration.
typedef std::map<int, state_explicit_number::transition*> tr_cache_t;
typedef std::map<int, unsigned> tr_cache_t;
tr_cache_t tr_cache;
// State level cache
@ -355,16 +356,7 @@ namespace spot
}
}
#ifdef DEGEN_DEBUG
std::map<const state*, int>names;
names[s.first] = 1;
ds2num[s] =
10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first);
#else
ds2num[s] = 0;
#endif
ds2num[s] = res->new_state();
todo.push_back(s);
// If use_lvl_cache is on insert initial state to level cache
@ -557,11 +549,7 @@ namespace spot
}
else
{
#ifdef DEGEN_DEBUG
dest = 10000 * names[d.first] + 100 * d.second + scc;
#else
dest = ds2num.size();
#endif
dest = res->new_state();
ds2num[d] = dest;
todo.push_back(d);
// Insert new state to cache
@ -582,24 +570,24 @@ namespace spot
}
}
state_explicit_number::transition*& t =
tr_cache[dest * 2 + is_acc];
unsigned& t = tr_cache[dest * 2 + is_acc];
if (t == 0)
{
// Actually create the transition.
t = res->create_transition(src, dest);
t->condition = i->current_condition();
// If the source state is accepting, we have to put
// degen_acc on all outgoing transitions. (We are still
// building a TGBA; we only assure that it can be used as
// an SBA.)
// Actually create the transition. If the source
// state is accepting, we have to put degen_acc on all
// outgoing transitions. (We are still building a
// TGBA; we only assure that it can be used as an
// SBA.)
bdd acc = bddfalse;
if (is_acc)
t->acceptance_conditions = degen_acc;
acc = degen_acc;
t = res->new_transition(src, dest,
i->current_condition(), acc);
}
else
{
t->condition |= i->current_condition();
res->trans_data(t).cond |= i->current_condition();
}
}
tr_cache.clear();

7
src/tgbaalgos/degen.hh
View file

@ -20,13 +20,10 @@
#ifndef SPOT_TGBAALGOS_DEGEN_HH
# define SPOT_TGBAALGOS_DEGEN_HH
# include "misc/common.hh"
# include "tgba/tgbagraph.hh"
namespace spot
{
class sba;
class tgba;
/// \ingroup tgba_misc
/// \brief Degeneralize a spot::tgba into an equivalent sba with
/// only one acceptance condition.
@ -52,7 +49,7 @@ namespace spot
/// \a a to be computed prior to its actual degeneralization.
///
/// \see tgba_sba_proxy, tgba_tba_proxy
SPOT_API sba*
SPOT_API tgba_digraph*
degeneralize(const tgba* a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
int use_lvl_cache = 1,

5
src/tgbaalgos/dotty.cc
View file

@ -28,7 +28,7 @@
#include "tgba/bddprint.hh"
#include "reachiter.hh"
#include "misc/escape.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbagraph.hh"
#include "tgba/formula2bdd.hh"
namespace spot
@ -130,6 +130,9 @@ namespace spot
{
if (!dd)
dd = dotty_decorator::instance();
if (const tgba_digraph* gd = dynamic_cast<const tgba_digraph*>(g))
assume_sba |= gd->get_bprop(tgba_digraph::StateBasedAcc);
dotty_bfs d(os, g, assume_sba, dd);
d.run();
return os;

73
src/tgbaalgos/minimize.cc
View file

@ -48,7 +48,6 @@
#include "tgbaalgos/bfssteps.hh"
#include "tgbaalgos/isdet.hh"
#include "tgbaalgos/dtgbacomp.hh"
#include "priv/countstates.hh"
namespace spot
{
@ -115,30 +114,43 @@ namespace spot
// From the base automaton and the list of sets, build the minimal
// resulting automaton
sba_explicit_number* build_result(const tgba* a,
std::list<hash_set*>& sets,
hash_set* final)
tgba_digraph* build_result(const tgba* a,
std::list<hash_set*>& sets,
hash_set* final)
{
auto dict = a->get_dict();
auto res = new tgba_digraph(dict);
dict->register_all_variables_of(a, res);
dict->unregister_all_typed_variables(bdd_dict::acc, res);
res->set_bprop(tgba_digraph::StateBasedAcc);
// For each set, create a state in the resulting automaton.
// For a state s, state_num[s] is the number of the state in the minimal
// automaton.
hash_map state_num;
std::list<hash_set*>::iterator sit;
unsigned num = 0;
for (sit = sets.begin(); sit != sets.end(); ++sit)
{
hash_set::iterator hit;
hash_set* h = *sit;
unsigned num = res->new_state();
for (hit = h->begin(); hit != h->end(); ++hit)
state_num[*hit] = num;
++num;
}
typedef state_explicit_number::transition trs;
sba_explicit_number* res = new sba_explicit_number(a->get_dict());
// For each transition in the initial automaton, add the corresponding
// transition in res.
bdd allacc = bddfalse;
if (!final->empty())
res->declare_acceptance_condition(ltl::constant::true_instance());
{
res->set_bprop(tgba_digraph::SingleAccSet);
int accvar =
dict->register_acceptance_variable(ltl::constant::true_instance(),
res);
allacc = bdd_ithvar(accvar);
res->set_acceptance_conditions(allacc);
}
for (sit = sets.begin(); sit != sets.end(); ++sit)
{
hash_set::iterator hit;
@ -157,17 +169,21 @@ namespace spot
dst->destroy();
if (i == state_num.end()) // Ignore useless destinations.
continue;
trs* t = res->create_transition(src_num, i->second);
res->add_conditions(t, succit->current_condition());
bdd acc = bddfalse;
if (accepting)
res->add_acceptance_condition(t, ltl::constant::true_instance());
acc = allacc;
res->new_transition(src_num, i->second,
succit->current_condition(), acc);
}
}
res->merge_transitions();
const state* init_state = a->get_init_state();
unsigned init_num = state_num[init_state];
init_state->destroy();
res->set_init_state(init_num);
if (res->num_states() > 0)
{
const state* init_state = a->get_init_state();
unsigned init_num = state_num[init_state];
init_state->destroy();
res->set_init_state(init_num);
}
return res;
}
@ -212,6 +228,7 @@ namespace spot
wdba_scc_is_accepting(const tgba_digraph* det_a, unsigned scc_n,
const tgba* orig_a, scc_map& sm, power_map& pm)
{
// Get some state from the SCC #n.
const state* start = sm.one_state_of(scc_n)->clone();
@ -272,8 +289,8 @@ namespace spot
}
sba_explicit_number* minimize_dfa(const tgba_digraph* det_a,
hash_set* final, hash_set* non_final)
tgba_digraph* minimize_dfa(const tgba_digraph* det_a,
hash_set* final, hash_set* non_final)
{
typedef std::list<hash_set*> partition_t;
partition_t cur_run;
@ -460,7 +477,7 @@ namespace spot
#endif
// Build the result.
sba_explicit_number* res = build_result(det_a, done, final_copy);
auto* res = build_result(det_a, done, final_copy);
// Free all the allocated memory.
delete final_copy;
@ -479,7 +496,7 @@ namespace spot
}
sba_explicit_number* minimize_monitor(const tgba* a)
tgba_digraph* minimize_monitor(const tgba* a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
@ -497,7 +514,7 @@ namespace spot
return minimize_dfa(det_a, final, non_final);
}
sba_explicit_number* minimize_wdba(const tgba* a)
tgba_digraph* minimize_wdba(const tgba* a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
@ -596,21 +613,21 @@ namespace spot
return minimize_dfa(det_a, final, non_final);
}
tgba*
minimize_obligation(const tgba* aut_f,
tgba_digraph*
minimize_obligation(const tgba_digraph* aut_f,
const ltl::formula* f, const tgba* aut_neg_f,
bool reject_bigger)
{
sba_explicit_number* min_aut_f = minimize_wdba(aut_f);
auto min_aut_f = minimize_wdba(aut_f);
if (reject_bigger)
{
// Abort if min_aut_f has more states than aut_f.
unsigned orig_states = count_states(aut_f);
unsigned orig_states = aut_f->num_states();
if (orig_states < min_aut_f->num_states())
{
delete min_aut_f;
return const_cast<tgba*>(aut_f);
return const_cast<tgba_digraph*>(aut_f);
}
}
@ -653,7 +670,7 @@ namespace spot
{
// Otherwise, we cannot check if the minimization is safe.
delete min_aut_f;
return 0;
return nullptr;
}
}
@ -705,6 +722,6 @@ namespace spot
if (ok)
return min_aut_f;
delete min_aut_f;
return const_cast<tgba*>(aut_f);
return const_cast<tgba_digraph*>(aut_f);
}
}

18
src/tgbaalgos/minimize.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_MINIMIZE_HH
# define SPOT_TGBAALGOS_MINIMIZE_HH
# include "tgba/tgbaexplicit.hh"
# include "tgba/tgbagraph.hh"
# include "ltlast/formula.hh"
namespace spot
@ -57,7 +57,7 @@ namespace spot
/// \param a the automaton to convert into a minimal deterministic monitor
/// \pre Dead SCCs should have been removed from \a a before
/// calling this function.
SPOT_API sba_explicit_number* minimize_monitor(const tgba* a);
SPOT_API tgba_digraph* minimize_monitor(const tgba* a);
/// \brief Minimize a Büchi automaton in the WDBA class.
///
@ -93,7 +93,7 @@ namespace spot
month = oct
}
\endverbatim */
SPOT_API sba_explicit_number* minimize_wdba(const tgba* a);
SPOT_API tgba_digraph* minimize_wdba(const tgba* a);
/// \brief Minimize an automaton if it represents an obligation property.
///
@ -150,10 +150,10 @@ namespace spot
/// determinization step during minimize_wdba().) Note that
/// checking the size of the minimized WDBA occurs before ensuring
/// that the minimized WDBA is correct.
SPOT_API tgba* minimize_obligation(const tgba* aut_f,
const ltl::formula* f = 0,
const tgba* aut_neg_f = 0,
bool reject_bigger = false);
SPOT_API tgba_digraph* minimize_obligation(const tgba_digraph* aut_f,
const ltl::formula* f = 0,
const tgba* aut_neg_f = 0,
bool reject_bigger = false);
/// @}
}

59
src/tgbaalgos/postproc.cc
View file

@ -75,7 +75,7 @@ namespace spot
}
}
const tgba* postprocessor::do_simul(const tgba* a, int opt)
const tgba_digraph* postprocessor::do_simul(const tgba_digraph* a, int opt)
{
switch (opt)
{
@ -95,7 +95,8 @@ namespace spot
}
}
const tgba* postprocessor::do_ba_simul(const tgba* a, int opt)
const tgba_digraph* postprocessor::do_ba_simul(const tgba_digraph* a,
int opt)
{
switch (opt)
{
@ -112,18 +113,16 @@ namespace spot
}
const tgba* postprocessor::do_degen(const tgba* a)
const tgba_digraph* postprocessor::do_degen(const tgba_digraph* a)
{
const tgba* d = degeneralize(a,
degen_reset_,
degen_order_,
degen_cache_,
degen_lskip_);
auto d = degeneralize(a,
degen_reset_, degen_order_,
degen_cache_, degen_lskip_);
delete a;
if (ba_simul_ <= 0)
return d;
const tgba* s = do_ba_simul(d, ba_simul_);
auto s = do_ba_simul(d, ba_simul_);
if (s != d)
delete d;
@ -133,7 +132,8 @@ namespace spot
#define PREF_ (pref_ & (Small | Deterministic))
#define COMP_ (pref_ & Complete)
const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
const tgba_digraph*
postprocessor::run(const tgba_digraph* a, const ltl::formula* f)
{
if (type_ == TGBA && PREF_ == Any && level_ == Low)
return a;
@ -154,13 +154,13 @@ namespace spot
{
// Do not bother about acceptance conditions, they will be
// ignored.
const tgba* s = scc_filter_states(a);
auto s = scc_filter_states(a);
delete a;
a = s;
}
else if (scc_filter_ > 0)
{
const tgba* s = scc_filter(a, scc_filter_ > 1);
auto s = scc_filter(a, scc_filter_ > 1);
delete a;
a = s;
}
@ -169,20 +169,18 @@ namespace spot
{
if (PREF_ == Deterministic)
{
const tgba* m = minimize_monitor(a);
auto m = minimize_monitor(a);
delete a;
return m;
}
else
{
const tgba* m = strip_acceptance(a);
delete a;
a = m;
strip_acceptance_here(const_cast<tgba_digraph*>(a));
}
if (PREF_ == Any)
return a;
const tgba* sim = do_simul(a, simul_);
auto sim = do_simul(a, simul_);
if (a == sim)
// simulation was disabled.
return a;
@ -193,9 +191,9 @@ namespace spot
}
// For Small,High we return the smallest between the output of
// the simulation, and that of the deterministic minimization.
const tgba* m = minimize_monitor(a);
auto m = minimize_monitor(a);
delete a;
if (count_states(m) > count_states(sim))
if (m->num_states() > sim->num_states())
{
delete m;
}
@ -206,7 +204,7 @@ namespace spot
}
if (COMP_ == Complete)
{
const tgba* s = tgba_complete(sim);
auto s = tgba_complete(sim);
delete sim;
sim = s;
}
@ -222,8 +220,8 @@ namespace spot
bool dba_is_wdba = false;
bool dba_is_minimal = false;
const tgba* dba = 0;
const tgba* sim = 0;
const tgba_digraph* dba = 0;
const tgba_digraph* sim = 0;
// (Small,Low) is the only configuration where we do not run
// WDBA-minimization.
@ -231,7 +229,7 @@ namespace spot
{
bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, 0, reject_bigger);
if (dba == a) // Minimization failed.
if (dba == a || dba == 0) // Minimization failed.
dba = 0;
else
dba_is_minimal = dba_is_wdba = true;
@ -243,7 +241,6 @@ namespace spot
if (!dba || (level_ == High && PREF_ == Small))
{
sim = do_simul(a, simul_);
if (sim != a)
delete a;
@ -363,8 +360,8 @@ namespace spot
in = dba;
}
const tgba* cmp = tgba_complete(in);
const tgba* res = 0;
const tgba_digraph* cmp = tgba_complete(in);
const tgba_digraph* res = 0;
if (target_acc == 1)
{
if (sat_states_ != -1)
@ -408,14 +405,14 @@ namespace spot
&& !(dba_is_minimal && state_based_
&& dba->number_of_acceptance_conditions() == 1))
{
const tgba* d = degeneralize(dba);
auto d = degeneralize(dba);
delete dba;
dba = d;
}
if (dba && sim)
{
if (count_states(dba) > count_states(sim))
if (dba->num_states() > sim->num_states())
{
delete dba;
dba = 0;
@ -432,14 +429,14 @@ namespace spot
{
if (dba && !dba_is_minimal) // WDBA is already clean.
{
const tgba* s = scc_filter(dba, true);
auto s = scc_filter(dba, true);
delete dba;
assert(!sim);
dba = s;
}
else if (sim)
{
const tgba* s = scc_filter(sim, true);
auto s = scc_filter(sim, true);
delete sim;
assert(!dba);
sim = s;
@ -450,7 +447,7 @@ namespace spot
if (COMP_ == Complete)
{
const tgba* s = tgba_complete(sim);
auto s = tgba_complete(sim);
delete sim;
sim = s;
}

11
src/tgbaalgos/postproc.hh
View file

@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_POSTPROC_HH
# define SPOT_TGBAALGOS_POSTPROC_HH
#include "tgba/tgba.hh"
#include "tgba/tgbagraph.hh"
namespace spot
{
@ -97,12 +97,13 @@ namespace spot
}
/// Return the optimized automaton and delete \a input_disown.
const tgba* run(const tgba* input_disown, const ltl::formula* f);
const tgba_digraph* run(const tgba_digraph* input_disown,
const ltl::formula* f);
protected:
const tgba* do_simul(const tgba* input, int opt);
const tgba* do_ba_simul(const tgba* input, int opt);
const tgba* do_degen(const tgba* input);
const tgba_digraph* do_simul(const tgba_digraph* input, int opt);
const tgba_digraph* do_ba_simul(const tgba_digraph* input, int opt);
const tgba_digraph* do_degen(const tgba_digraph* input);
output_type type_;
int pref_;

62
src/tgbaalgos/sccfilter.cc
View file

@ -20,8 +20,8 @@
#include "tgba/tgbaexplicit.hh"
#include "sccfilter.hh"
#include "reachiter.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
#include "scc.hh"
#include "sccinfo.hh"
namespace spot
{
@ -903,7 +903,8 @@ namespace spot
if (keep && acc != bddfalse)
{
unsigned u = this->si->scc_of(src);
unsigned u = this->si->scc_of(dst);
auto i = remap_[u].find(acc.id());
if (i != remap_[u].end())
acc = i->second;
@ -920,6 +921,12 @@ namespace spot
tgba_digraph* scc_filter_apply(const tgba_digraph* aut,
scc_info* given_si, Args&&... args)
{
bdd_dict* bd = aut->get_dict();
tgba_digraph* filtered = new tgba_digraph(bd);
unsigned in_n = aut->num_states(); // Number of input states.
if (in_n == 0) // Nothing to filter.
return filtered;
// Compute scc_info if not supplied.
scc_info* si = given_si;
if (!si)
@ -928,7 +935,6 @@ namespace spot
F filter(si, std::forward<Args>(args)...);
// Renumber all useful states.
unsigned in_n = aut->num_states(); // Number of input states.
unsigned out_n = 0; // Number of output states.
std::vector<unsigned> inout; // Associate old states to new ones.
inout.reserve(in_n);
@ -938,8 +944,6 @@ namespace spot
else
inout.push_back(-1U);
bdd_dict* bd = aut->get_dict();
tgba_digraph* filtered = new tgba_digraph(bd);
bd->register_all_variables_of(aut, filtered);
{
bdd all = aut->all_acceptance_conditions();
@ -989,14 +993,17 @@ namespace spot
scc_filter(const tgba_digraph* aut, bool remove_all_useless,
scc_info* given_si)
{
tgba_digraph* res;
if (remove_all_useless)
return scc_filter_apply<state_filter
<acc_filter_all
<acc_filter_simplify<>>>>(aut, given_si);
res = scc_filter_apply<state_filter
<acc_filter_all
<acc_filter_simplify<>>>>(aut, given_si);
else
return scc_filter_apply<state_filter
<acc_filter_some
<acc_filter_simplify<>>>>(aut, given_si);
res = scc_filter_apply<state_filter
<acc_filter_some
<acc_filter_simplify<>>>>(aut, given_si);
res->merge_transitions();
return res;
}
tgba_digraph*
@ -1004,22 +1011,25 @@ namespace spot
bdd suspvars, bdd ignoredvars, bool early_susp,
scc_info* given_si)
{
tgba_digraph* res;
if (remove_all_useless)
return scc_filter_apply<susp_filter
<state_filter
<acc_filter_all
<acc_filter_simplify<>>>>>(aut, given_si,
suspvars,
ignoredvars,
early_susp);
res = scc_filter_apply<susp_filter
<state_filter
<acc_filter_all
<acc_filter_simplify<>>>>>(aut, given_si,
suspvars,
ignoredvars,
early_susp);
else
return scc_filter_apply<susp_filter
<state_filter
<acc_filter_some
<acc_filter_simplify<>>>>>(aut, given_si,
suspvars,
ignoredvars,
early_susp);
res = scc_filter_apply<susp_filter
<state_filter
<acc_filter_some
<acc_filter_simplify<>>>>>(aut, given_si,
suspvars,
ignoredvars,
early_susp);
res->merge_transitions();
return res;
}
}

17
src/tgbaalgos/sccinfo.cc
View file

@ -76,13 +76,14 @@ namespace spot
// Setup depth-first search from the initial state.
{
unsigned init = aut->get_init_state_number();
num_ = -1;
h_[init] = num_;
root_.emplace_front(num_, bddfalse, bddfalse);
todo_.emplace(init, aut->out(init).begin());
}
if (n > 0)
{
unsigned init = aut->get_init_state_number();
num_ = -1;
h_[init] = num_;
root_.emplace_front(num_, bddfalse, bddfalse);
todo_.emplace(init, aut->out(init).begin());
}
while (!todo_.empty())
{
@ -237,7 +238,7 @@ namespace spot
for (unsigned src = 0; src < n; ++src)
{
unsigned src_scc = scc_of(src);
if (!is_accepting_scc(src_scc))
if (src_scc == -1U || !is_accepting_scc(src_scc))
continue;
for (auto& t: aut_->out(src))
{

47
src/tgbaalgos/stripacc.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -22,42 +22,13 @@
namespace spot
{
namespace
void strip_acceptance_here(tgba_digraph* a)
{
class strip_iter: public tgba_reachable_iterator_depth_first
{
public:
strip_iter(const tgba* a)
: tgba_reachable_iterator_depth_first(a),
out_(new sba_explicit_number(a->get_dict()))
{
}
sba_explicit_number*
result()
{
return out_;
}
void
process_link(const state*, int in,
const state*, int out,
const tgba_succ_iterator* si)
{
state_explicit_number::transition* t = out_->create_transition(in, out);
out_->add_conditions(t, si->current_condition());
}
private:
sba_explicit_number* out_;
};
}
sba_explicit_number*
strip_acceptance(const tgba* a)
{
strip_iter si(a);
si.run();
return si.result();
unsigned n = a->num_states();
for (unsigned s = 0; s < n; ++s)
for (auto& t: a->out(s))
t.acc = bddfalse;
a->set_acceptance_conditions(bddfalse);
a->get_dict()->unregister_all_typed_variables(bdd_dict::acc, a);
}
}

12
src/tgbaalgos/stripacc.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -20,16 +20,16 @@
#ifndef SPOT_TGBAALGOS_STRIPACC_HH
# define SPOT_TGBAALGOS_STRIPACC_HH
# include "tgba/tgbaexplicit.hh"
# include "tgba/tgbagraph.hh"
namespace spot
{
/// \ingroup tgba_misc
/// \brief Duplicate automaton \a a, removing all acceptance sets.
/// \brief Remove all acceptance sets from a tgba_digraph.
///
/// This is equivalent to marking all states/transitions as accepting.
SPOT_API sba_explicit_number*
strip_acceptance(const tgba* a);
SPOT_API void
strip_acceptance_here(tgba_digraph* a);
}
#endif // SPOT_TGBAALGOS_STRIPACC_HH

10
src/tgbaalgos/translate.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -61,7 +61,7 @@ namespace spot
simpl_owned_ = simpl_ = new ltl::ltl_simplifier(options, dict);
}
const tgba* translator::run(const ltl::formula** f)
const tgba_digraph* translator::run(const ltl::formula** f)
{
const ltl::formula* r = simpl_->simplify(*f);
(*f)->destroy();
@ -71,7 +71,7 @@ namespace spot
// natural way (improving the degeneralization).
simpl_->clear_as_bdd_cache();
const tgba* aut;
const tgba_digraph* aut;
if (comp_susp_ > 0)
{
int skel_wdba = skel_wdba_;
@ -91,10 +91,10 @@ namespace spot
return aut;
}
const tgba* translator::run(const ltl::formula* f)
const tgba_digraph* translator::run(const ltl::formula* f)
{
f->clone();
const tgba* aut = run(&f);
auto aut = run(&f);
f->destroy();
return aut;
}

8
src/tgbaalgos/translate.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -103,14 +103,14 @@ namespace spot
///
/// The formula \a f is simplified internally, but it is not
/// not destroyed (this is the responsibility of the caller).
const tgba* run(const ltl::formula* f);
const tgba_digraph* run(const ltl::formula* f);
/// \brief Convert \a f into an automaton, and update f.
///
/// The formula <code>*f</code> is destroyed, and replaced
/// by the simplified version, which should be destroyed by
/// the caller.
const tgba* run(const ltl::formula** f);
const tgba_digraph* run(const ltl::formula** f);
protected:
void setup_opt(const option_map* opt);

51
src/tgbatest/ltl2tgba.cc
View file

@ -1003,7 +1003,6 @@ main(int argc, char** argv)
if (from_file)
{
spot::tgba_explicit_string* e = 0;
switch (readformat)
{
case ReadSpot:
@ -1113,9 +1112,6 @@ main(int argc, char** argv)
}
break;
}
if (e)
e->merge_transitions();
}
else
{
@ -1204,19 +1200,36 @@ main(int argc, char** argv)
const spot::tgba* aut_scc = 0;
if (scc_filter)
{
auto aa = dynamic_cast<const spot::tgba_digraph*>(a);
bool freeit = false;
if (!aa)
{
freeit = true;
aa = tgba_dupexp_dfs(a);
}
assert(aa);
tm.start("SCC-filter");
aut_scc = a = spot::scc_filter(a, scc_filter_all);
aut_scc = a = spot::scc_filter(aa, scc_filter_all);
tm.stop("SCC-filter");
assume_sba = false;
if (freeit)
delete aa;
}
const spot::tgba* degeneralized = 0;
spot::tgba* minimized = 0;
spot::tgba_digraph* minimized = 0;
if (opt_minimize)
{
tm.start("obligation minimization");
minimized = minimize_obligation(a, f, 0, reject_bigger);
auto aa = dynamic_cast<const spot::tgba_digraph*>(a);
bool freeit = false;
if (!aa)
{
freeit = true;
aa = tgba_dupexp_dfs(a);
}
minimized = minimize_obligation(aa, f, 0, reject_bigger);
tm.stop("obligation minimization");
if (minimized == 0)
@ -1229,7 +1242,7 @@ main(int argc, char** argv)
exit(2);
}
}
else if (minimized == a)
else if (minimized == aa)
{
minimized = 0;
}
@ -1244,6 +1257,8 @@ main(int argc, char** argv)
reduction_iterated_sim = false;
assume_sba = true;
}
if (freeit)
delete aa;
}
if (reduction_dir_sim && !reduction_iterated_sim)
@ -1302,8 +1317,10 @@ main(int argc, char** argv)
if (scc_filter)
{
auto aa = down_cast<const spot::tgba_digraph*>(a);
assert(aa);
tm.start("SCC-filter on don't care");
a = spot::scc_filter(a, true);
a = spot::scc_filter(aa, true);
delete temp_dont_care_sim;
temp_dont_care_sim = a;
tm.stop("SCC-filter on don't care");
@ -1438,8 +1455,10 @@ main(int argc, char** argv)
{
tm.start("SCC-filter post-sim");
delete aut_scc;
auto aa = down_cast<const spot::tgba_digraph*>(a);
assert(aa);
// Do not filter_all for SBA
aut_scc = a = spot::scc_filter(a, assume_sba ?
aut_scc = a = spot::scc_filter(aa, assume_sba ?
false : scc_filter_all);
tm.stop("SCC-filter post-sim");
}
@ -1448,7 +1467,7 @@ main(int argc, char** argv)
if (opt_monitor)
{
tm.start("Monitor minimization");
minimized = a = minimize_monitor(a);
a = minimized = minimize_monitor(a);
tm.stop("Monitor minimization");
assume_sba = false; // All states are accepting, so double
// circles in the dot output are
@ -1612,16 +1631,6 @@ 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();
else if (spot::sba_explicit_formula* sef =
dynamic_cast<spot::sba_explicit_formula*>(a))
sef->enable_utf8();
}
if (output != -1)
{
tm.start("producing output");

15
wrap/python/spot.i
View file

@ -378,13 +378,22 @@ namespace std {
%inline %{
// A variant of minimize_obligation() that always return a new object.
const spot::tgba*
const spot::tgba_digraph*
minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f)
{
const tgba* res = spot::minimize_obligation(a, f);
auto aa = dynamic_cast<const spot::tgba_digraph*>(a);
bool freeit = false;
if (!aa)
{
freeit = true;
aa = tgba_dupexp_dfs(a);
}
auto res = spot::minimize_obligation(aa, f);
// Return 0 if the output is the same as the input, otherwise
// it is hard for swig to know if the output is "new" or not.
if (res == a)
if (freeit)
delete aa;
if (res == aa)
return 0;
else
return res;