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

Replace most uses of scc_map by scc_info.

Browse source 
This involves reimplementing some algorithms using tgba_digraph, and
implementing an explicit product that takes two tgba_digraphs and
produces a tgba_digraph.

* src/tgbaalgos/product.cc, src/tgbaalgos/product.hh: New files.
* src/tgbaalgos/Makefile.am: Adjust.
* src/bin/ltlcross.cc, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc: Update to use scc_info and/or tgba_digraph.
This commit is contained in:
Alexandre Duret-Lutz 2014-10-07 18:21:37 +02:00
parent b6745482af
commit 2fb436a174
27 changed files with 497 additions and 394 deletions
Download patch file Download diff file Expand all files Collapse all files

85
src/bin/ltlcross.cc
View file

@ -46,12 +46,10 @@
#include "ltlvisit/mutation.hh"
#include "ltlvisit/relabel.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/product.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/isweakscc.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
@ -880,7 +878,7 @@ namespace
string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
}
spot::const_tgba_ptr
spot::const_tgba_digraph_ptr
translate(unsigned int translator_num, char l, statistics_formula* fstats,
bool& problem)
{
@ -900,7 +898,7 @@ namespace
const char* status_str = 0;
spot::const_tgba_ptr res = 0;
spot::const_tgba_digraph_ptr res = 0;
if (timed_out)
{
// This is not considered to be a global error.
@ -1059,15 +1057,14 @@ namespace
st->edges = s.transitions;
st->transitions = s.sub_transitions;
st->acc = res->acc().num_sets();
spot::scc_map m(res);
m.build_map();
spot::scc_info m(res);
unsigned c = m.scc_count();
st->scc = c;
st->nondetstates = spot::count_nondet_states(res);
st->nondeterministic = st->nondetstates != 0;
for (unsigned n = 0; n < c; ++n)
{
if (!m.accepting(n))
if (!m.is_accepting_scc(n))
++st->nonacc_scc;
else if (is_terminal_scc(m, n))
++st->terminal_scc;
@ -1090,8 +1087,8 @@ namespace
};
static bool
check_empty_prod(const spot::const_tgba_ptr& aut_i,
const spot::const_tgba_ptr& aut_j,
check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i,
const spot::const_tgba_digraph_ptr& aut_j,
size_t i, size_t j, bool icomp, bool jcomp)
{
auto prod = spot::product(aut_i, aut_j);
@ -1145,7 +1142,7 @@ namespace
}
static bool
cross_check(const std::vector<spot::scc_map*>& maps, char l, unsigned p)
cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
{
size_t m = maps.size();
if (verbose)
@ -1167,13 +1164,17 @@ namespace
unsigned verified = 0;
unsigned violated = 0;
for (size_t i = 0; i < m; ++i)
if (spot::scc_map* m = maps[i])
if (spot::scc_info* m = maps[i])
{
// r == true iff the automaton i is accepting.
bool r = false;
unsigned c = m->scc_count();
for (unsigned j = 0; (j < c) && !r; ++j)
r |= m->accepting(j);
for (unsigned j = 0; j < c; ++j)
if (m->is_accepting_scc(j))
{
r = true;
break;
}
res[i] = r;
if (r)
++verified;
@ -1216,41 +1217,34 @@ namespace
return false;
}
typedef std::set<spot::state*, spot::state_ptr_less_than> state_set;
typedef std::set<unsigned> state_set;
// Collect all the states of SSPACE that appear in the accepting SCCs
// of PROD.
// of PROD. (Trivial SCCs are considered accepting.)
static void
states_in_acc(const spot::scc_map* m,
const spot::const_tgba_ptr& sspace,
states_in_acc(const spot::scc_info* m,
state_set& s)
{
auto aut = m->get_aut();
auto ps = static_cast<const spot::product_states*>
(aut->get_named_prop("product-states"));
unsigned c = m->scc_count();
for (unsigned n = 0; n < c; ++n)
if (m->accepting(n))
if (m->is_accepting_scc(n) || m->is_trivial(n))
for (auto i: m->states_of(n))
{
spot::state* x = aut->project_state(i, sspace);
assert(x);
if (!s.insert(x).second)
x->destroy();
}
// Get the projection on sspace.
s.insert((*ps)[i].second);
}
static bool
consistency_check(const spot::scc_map* pos, const spot::scc_map* neg,
const spot::const_tgba_ptr& sspace)
consistency_check(const spot::scc_info* pos, const spot::scc_info* neg)
{
// the states of SSPACE should appear in the accepting SCC of at
// least one of POS or NEG. Maybe both.
state_set s;
states_in_acc(pos, sspace, s);
states_in_acc(neg, sspace, s);
bool res = s.size() == states;
for (auto i: s)
i->destroy();
return res;
states_in_acc(pos, s);
states_in_acc(neg, s);
return s.size() == states;
}
typedef
@ -1423,12 +1417,12 @@ namespace
// These store the result of the translation of the positive and
// negative formulas.
size_t m = translators.size();
std::vector<spot::const_tgba_ptr> pos(m);
std::vector<spot::const_tgba_ptr> neg(m);
std::vector<spot::const_tgba_digraph_ptr> pos(m);
std::vector<spot::const_tgba_digraph_ptr> neg(m);
// These store the complement of the above results, when we can
// compute it easily.
std::vector<spot::const_tgba_ptr> comp_pos(m);
std::vector<spot::const_tgba_ptr> comp_neg(m);
std::vector<spot::const_tgba_digraph_ptr> comp_pos(m);
std::vector<spot::const_tgba_digraph_ptr> comp_neg(m);
unsigned n = vstats.size();
@ -1577,19 +1571,18 @@ namespace
auto statespace = spot::random_graph(states, density, ap, dict);
// Products of the state space with the positive automata.
std::vector<spot::const_tgba_ptr> pos_prod(m);
std::vector<spot::const_tgba_digraph_ptr> pos_prod(m);
// Products of the state space with the negative automata.
std::vector<spot::const_tgba_ptr> neg_prod(m);
std::vector<spot::const_tgba_digraph_ptr> neg_prod(m);
// Associated SCC maps.
std::vector<spot::scc_map*> pos_map(m);
std::vector<spot::scc_map*> neg_map(m);
std::vector<spot::scc_info*> pos_map(m);
std::vector<spot::scc_info*> neg_map(m);
for (size_t i = 0; i < m; ++i)
if (pos[i])
{
auto p = spot::product(pos[i], statespace);
pos_prod[i] = p;
spot::scc_map* sm = new spot::scc_map(p);
sm->build_map();
auto sm = new spot::scc_info(p);
pos_map[i] = sm;
// Statistics
@ -1608,8 +1601,7 @@ namespace
{
auto p = spot::product(neg[i], statespace);
neg_prod[i] = p;
spot::scc_map* sm = new spot::scc_map(p);
sm->build_map();
auto sm = new spot::scc_info(p);
neg_map[i] = sm;
// Statistics
@ -1636,8 +1628,7 @@ namespace
std::cerr << "info: consistency_check (P" << i
<< ",N" << i << "), state-space #"
<< p << '/' << products << '\n';
if (!(consistency_check(pos_map[i], neg_map[i],
statespace)))
if (!(consistency_check(pos_map[i], neg_map[i])))
{
++problems;

31
src/tgba/tgba.cc
View file

@ -22,6 +22,7 @@
#include "tgba.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include <utility>
namespace spot
{
@ -38,6 +39,10 @@ namespace spot
if (last_support_conditions_input_)
last_support_conditions_input_->destroy();
delete iter_cache_;
// Destroy all named properties.
for (auto& np: named_prop_)
np.second.second(np.second.first);
}
bdd
@ -78,4 +83,30 @@ namespace spot
return !couvreur99(shared_from_this())->check();
}
void
tgba::set_named_prop(std::string s,
void* val, std::function<void(void*)> destructor)
{
auto p = named_prop_.emplace(std::piecewise_construct,
std::forward_as_tuple(s),
std::forward_as_tuple(val, destructor));
if (!p.second)
{
p.first->second.second(p.first->second.first);
p.first->second = std::make_pair(val, destructor);
}
}
void*
tgba::get_named_prop(std::string s) const
{
auto i = named_prop_.find(s);
if (i == named_prop_.end())
return nullptr;
return i->second.first;
}
}

14
src/tgba/tgba.hh
View file

@ -27,6 +27,8 @@
#include "acc.hh"
#include <cassert>
#include <memory>
#include <unordered_map>
#include <functional>
#include "misc/casts.hh"
#include "misc/hash.hh"
@ -657,8 +659,20 @@ namespace spot
bprop is;
};
#ifndef SWIG
// Dynamic properties, are given with a name and a destructor function.
std::unordered_map<std::string,
std::pair<void*,
std::function<void(void*)>>> named_prop_;
#endif
public:
#ifndef SWIG
void set_named_prop(std::string s,
void* val, std::function<void(void*)> destructor);
void* get_named_prop(std::string s) const;
#endif
bool has_single_acc_set() const
{
return is.single_acc_set;

7
src/tgba/tgbasafracomplement.cc
View file

@ -570,7 +570,7 @@ namespace spot
{
public:
static safra_tree_automaton*
create_safra_automaton(const const_tgba_ptr& a);
create_safra_automaton(const const_tgba_digraph_ptr& a);
private:
typedef std::set<int> atomic_list_t;
typedef std::set<bdd, bdd_less_than> conjunction_list_t;
@ -585,7 +585,8 @@ namespace spot
/// \brief The body of Safra's construction.
safra_tree_automaton*
safra_determinisation::create_safra_automaton(const const_tgba_ptr& a)
safra_determinisation::create_safra_automaton
(const const_tgba_digraph_ptr& a)
{
// initialization.
auto sba_aut = degeneralize(a);
@ -1074,7 +1075,7 @@ namespace spot
// tgba_safra_complement
//////////////////////////
tgba_safra_complement::tgba_safra_complement(const const_tgba_ptr& a)
tgba_safra_complement::tgba_safra_complement(const const_tgba_digraph_ptr& a)
: tgba(a->get_dict()), automaton_(a),
safra_(safra_determinisation::create_safra_automaton(a))
{

6
src/tgba/tgbasafracomplement.hh
View file

@ -50,7 +50,7 @@ namespace spot
class SPOT_API tgba_safra_complement : public tgba
{
public:
tgba_safra_complement(const const_tgba_ptr& a);
tgba_safra_complement(const const_tgba_digraph_ptr& a);
virtual ~tgba_safra_complement();
// tgba interface.
@ -67,7 +67,7 @@ namespace spot
protected:
virtual bdd compute_support_conditions(const state* state) const;
private:
const_tgba_ptr automaton_;
const_tgba_digraph_ptr automaton_;
void* safra_;
#if TRANSFORM_TO_TBA
acc_cond::mark_t the_acceptance_cond_;
@ -82,7 +82,7 @@ namespace spot
typedef std::shared_ptr<const tgba_safra_complement>
const_tgba_safra_complement_ptr;
inline tgba_safra_complement_ptr
make_safra_complement(const const_tgba_ptr& a)
make_safra_complement(const const_tgba_digraph_ptr& a)
{
return std::make_shared<tgba_safra_complement>(a);
}

2
src/tgbaalgos/Makefile.am
View file

@ -53,6 +53,7 @@ tgbaalgos_HEADERS = \
neverclaim.hh \
postproc.hh \
powerset.hh \
product.hh \
projrun.hh \
randomgraph.hh \
reachiter.hh \
@ -100,6 +101,7 @@ libtgbaalgos_la_SOURCES = \
neverclaim.cc \
postproc.cc \
powerset.cc \
product.cc \
projrun.cc \
randomgraph.cc \
reachiter.cc \

7
src/tgbaalgos/cycles.cc
View file

@ -22,7 +22,7 @@
namespace spot
{
enumerate_cycles::enumerate_cycles(const scc_map& map)
enumerate_cycles::enumerate_cycles(const scc_info& map)
: aut_(map.get_aut()), sm_(map)
{
}
@ -84,12 +84,13 @@ namespace spot
dfs_.push_back(e);
}
// FIXME: Recode this algorithm using unsigned states.
void
enumerate_cycles::run(unsigned scc)
{
bool keep_going = true;
push_state(tag_state(sm_.one_state_of(scc)->clone()));
push_state(tag_state(aut_->state_from_number(sm_.one_state_of(scc))));
while (keep_going && !dfs_.empty())
{
@ -109,7 +110,7 @@ namespace spot
// Ignore those that are not on the SCC, or destination
// that have been "virtually" deleted from A(v).
state* s = cur.succ->current_state();
if ((sm_.scc_of_state(s) != scc)
if ((sm_.scc_of(aut_->state_number(s)) != scc)
|| (cur.ts->second.del.find(s) != cur.ts->second.del.end()))
{
s->destroy();

20
src/tgbaalgos/cycles.hh
View file

@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_CYCLES_HH
# define SPOT_TGBAALGOS_CYCLES_HH
#include "scc.hh"
#include "sccinfo.hh"
#include "misc/hash.hh"
#include <deque>
@ -62,13 +62,11 @@ namespace spot
/// dfs_ stack. Only the last portion of this stack may form a
/// cycle.
///
/// The class constructor takes an scc_map that should already have
/// been built for its automaton. Calling <code>run(n)</code> will
/// enumerate all elementary cycles in SCC <code>n</code>. Each
/// time an SCC is found, the method cycle_found(s) is called with
/// the initial state s of the cycle: the cycle is constituted from
/// all the states that are on the \c dfs_ stack after \c s
/// (including \c s).
/// Calling <code>run(n)</code> will enumerate all elementary cycles
/// in SCC <code>n</code>. Each time an SCC is found, the method
/// cycle_found(s) is called with the initial state s of the cycle:
/// the cycle is constituted from all the states that are on the \c
/// dfs_ stack after \c s (including \c s).
///
/// You should inherit from this class and redefine the
/// cycle_found() method to perform any work you would like to do on
@ -112,9 +110,9 @@ namespace spot
typedef hash_type::iterator tagged_state;
// The automaton we are working on.
const_tgba_ptr aut_;
const_tgba_digraph_ptr aut_;
// The SCC map built for aut_.
const scc_map& sm_;
const scc_info& sm_;
// The DFS stack. Each entry contains a tagged state, an iterator
// on the transitions leaving that state, and a Boolean f
@ -131,7 +129,7 @@ namespace spot
dfs_stack dfs_;
public:
enumerate_cycles(const scc_map& map);
enumerate_cycles(const scc_info& map);
virtual ~enumerate_cycles() {}
/// \brief Run in SCC scc, and call \a cycle_found() for any new

214
src/tgbaalgos/degen.cc
View file

@ -26,7 +26,7 @@
#include <vector>
#include <algorithm>
#include <iterator>
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgba/bddprint.hh"
//#define DEGEN_DEBUG
@ -38,32 +38,19 @@ namespace spot
// A state in the degenalized automaton corresponds to a state in
// the TGBA associated to a level. The level is just an index in
// the list of acceptance sets.
typedef std::pair<const state*, unsigned> degen_state;
typedef std::pair<unsigned, unsigned> degen_state;
struct degen_state_hash
{
size_t
operator()(const degen_state& s) const
{
return s.first->hash() & wang32_hash(s.second);
}
};
struct degen_state_equal
{
bool
operator()(const degen_state& left,
const degen_state& right) const
{
if (left.second != right.second)
return false;
return left.first->compare(right.first) == 0;
return wang32_hash(s.first ^ wang32_hash(s.second));
}
};
// Associate the degeneralized state to its number.
typedef std::unordered_map<degen_state, int,
degen_state_hash, degen_state_equal> ds2num_map;
typedef std::unordered_map<degen_state, int, degen_state_hash> ds2num_map;
// Queue of state to be processed.
typedef std::deque<degen_state> queue_t;
@ -72,96 +59,64 @@ namespace spot
// SCC -- we do not care about the other) of some state.
class outgoing_acc
{
const_tgba_ptr a_;
typedef std::pair<acc_cond::mark_t, acc_cond::mark_t> cache_entry;
typedef std::unordered_map<const state*, cache_entry,
state_ptr_hash, state_ptr_equal> cache_t;
cache_t cache_;
const scc_map* sm_;
const_tgba_digraph_ptr a_;
typedef std::tuple<acc_cond::mark_t,
acc_cond::mark_t,
bool> cache_entry;
std::vector<cache_entry> cache_;
const scc_info* sm_;
public:
outgoing_acc(const const_tgba_ptr& a, const scc_map* sm): a_(a), sm_(sm)
void fill_cache(unsigned s)
{
}
cache_t::const_iterator fill_cache(const state* s)
{
unsigned s1 = sm_ ? sm_->scc_of_state(s) : 0;
unsigned s1 = sm_ ? sm_->scc_of(s) : 0;
acc_cond::mark_t common = a_->acc().all_sets();
acc_cond::mark_t union_ = 0U;
for (auto it: a_->succ(s))
bool has_acc_self_loop = false;
for (auto& t: a_->out(s))
{
// Ignore transitions that leave the SCC of s.
const state* d = it->current_state();
unsigned s2 = sm_ ? sm_->scc_of_state(d) : 0;
d->destroy();
unsigned d = t.dst;
unsigned s2 = sm_ ? sm_->scc_of(d) : 0;
if (s2 != s1)
continue;
acc_cond::mark_t set = it->current_acceptance_conditions();
common &= set;
union_ |= set;
common &= t.acc;
union_ |= t.acc;
// an accepting self-loop?
has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
}
cache_entry e(common, union_);
return cache_.emplace(s, e).first;
cache_[s] = std::make_tuple(common, union_, has_acc_self_loop);
}
public:
outgoing_acc(const const_tgba_digraph_ptr& a, const scc_info* sm):
a_(a), cache_(a->num_states()), sm_(sm)
{
unsigned n = a->num_states();
for (unsigned s = 0; s < n; ++s)
fill_cache(s);
}
// Intersection of all outgoing acceptance sets
acc_cond::mark_t common_acc(const state* s)
acc_cond::mark_t common_acc(unsigned s)
{
cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end())
i = fill_cache(s);
return i->second.first;
assert(s < cache_.size());
return std::get<0>(cache_[s]);
}
// Union of all outgoing acceptance sets
acc_cond::mark_t union_acc(const state* s)
{
cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end())
i = fill_cache(s);
return i->second.second;
}
};
// Check whether a state has an accepting self-loop, with a catch.
class has_acc_loop
{
const_tgba_ptr a_;
typedef std::unordered_map<const state*, bool,
state_ptr_hash, state_ptr_equal> cache_t;
cache_t cache_;
state_unicity_table& uniq_;
public:
has_acc_loop(const const_tgba_ptr& a, state_unicity_table& uniq):
a_(a),
uniq_(uniq)
acc_cond::mark_t union_acc(unsigned s)
{
assert(s < cache_.size());
return std::get<1>(cache_[s]);
}
bool check(const state* s)
// Has an accepting self-loop
bool has_acc_selfloop(unsigned s)
{
auto p = cache_.emplace(s, false);
if (p.second)
{
for (auto it: a_->succ(s))
{
// Look only for transitions that are accepting.
if (!a_->acc().accepting(it->current_acceptance_conditions()))
continue;
// Look only for self-loops.
const state* dest = uniq_(it->current_state());
if (dest == s)
{
p.first->second = true;
break;
}
}
}
return p.first->second;
assert(s < cache_.size());
return std::get<2>(cache_[s]);
}
};
@ -196,7 +151,6 @@ namespace spot
void
print(int scc)
{
std::vector<bdd>::iterator i;
std::cout << "Order_" << scc << ":\t";
for (auto i: order_)
std::cout << i << ", ";
@ -234,7 +188,7 @@ namespace spot
template<bool want_sba>
tgba_digraph_ptr
degeneralize_aux(const const_tgba_ptr& a, bool use_z_lvl,
degeneralize_aux(const const_tgba_digraph_ptr& a, bool use_z_lvl,
bool use_cust_acc_orders, int use_lvl_cache,
bool skip_levels)
{
@ -274,14 +228,6 @@ namespace spot
// Initialize scc_orders
scc_orders orders(a->acc(), skip_levels);
// Make sure we always use the same pointer for identical states
// from the input automaton.
state_unicity_table uniq;
// Accepting loop checker, for some heuristics.
has_acc_loop acc_loop(a, uniq);
// These maps make it possible to convert degen_state to number
// and vice-versa.
ds2num_map ds2num;
@ -293,27 +239,27 @@ namespace spot
typedef std::map<int, unsigned> tr_cache_t;
tr_cache_t tr_cache;
// State level cache
typedef std::map<const state*, unsigned> lvl_cache_t;
lvl_cache_t lvl_cache;
// Read this early, because it might create a state if the
// automaton is empty.
degen_state s(a->get_init_state_number(), 0);
// State->level cache
std::vector<std::pair<unsigned, bool>> lvl_cache(a->num_states());
// Compute SCCs in order to use any optimization.
scc_map m(a);
scc_info* m = nullptr;
if (use_scc)
m.build_map();
m = new scc_info(a);
// Cache for common outgoing acceptances.
outgoing_acc outgoing(a, use_scc ? &m : 0);
outgoing_acc outgoing(a, m);
queue_t todo;
const state* s0 = uniq(a->get_init_state());
degen_state s(s0, 0);
// As a heuristic for building SBA, if the initial state has at
// least one accepting self-loop, start the degeneralization on
// the accepting level.
if (want_sba && acc_loop.check(s0))
if (want_sba && outgoing.has_acc_selfloop(s.first))
s.second = order.size();
// Otherwise, check for acceptance conditions common to all
// outgoing transitions, and assume we have already seen these and
@ -322,7 +268,7 @@ namespace spot
{
auto set = outgoing.common_acc(s.first);
if (use_cust_acc_orders)
s.second = orders.next_level(m.initial(), s.second, set);
s.second = orders.next_level(m->initial(), s.second, set);
else
while (s.second < order.size()
&& set.has(order[s.second]))
@ -345,7 +291,7 @@ namespace spot
// If such state exists level from chache is used.
// If not, a new level (starting with 0) is computed.
if (use_lvl_cache)
lvl_cache[s.first] = s.second;
lvl_cache[s.first] = std::make_pair(s.second, true);
while (!todo.empty())
{
@ -363,19 +309,19 @@ namespace spot
// Check SCC for state s
int s_scc = -1;
if (use_scc)
s_scc = m.scc_of_state(s.first);
s_scc = m->scc_of(s.first);
for (auto i: a->succ(s.first))
for (auto& i: a->out(s.first))
{
degen_state d(uniq(i->current_state()), 0);
degen_state d(i.dst, 0);
// Check whether the target SCC is accepting
bool is_scc_acc;
int scc;
if (use_scc)
{
scc = m.scc_of_state(d.first);
is_scc_acc = m.accepting(scc);
scc = m->scc_of(d.first);
is_scc_acc = m->is_accepting_scc(scc);
}
else
{
@ -386,7 +332,7 @@ namespace spot
}
// The old level is slevel. What should be the new one?
auto acc = i->current_acceptance_conditions();
auto acc = i.acc;
auto otheracc = outgoing.common_acc(d.first);
if (want_sba && is_acc)
@ -459,9 +405,9 @@ namespace spot
// If lvl_cache is used and switching SCCs, use level
// from cache
if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end())
&& lvl_cache[d.first].second)
{
d.second = lvl_cache[d.first];
d.second = lvl_cache[d.first].first;
}
else
{
@ -490,7 +436,8 @@ namespace spot
// state that has at least one accepting
// self-loop, start the degeneralization on
// the accepting level.
if (s_scc != scc && acc_loop.check(d.first))
if (s_scc != scc
&& outgoing.has_acc_selfloop(d.first))
{
d.second = order.size();
}
@ -558,50 +505,47 @@ namespace spot
if (use_lvl_cache)
{
auto res = lvl_cache.emplace(d.first, d.second);
if (!res.second)
auto lvl = d.second;
if (lvl_cache[d.first].second)
{
if (use_lvl_cache == 3)
res.first->second =
std::max(res.first->second, d.second);
lvl = std::max(lvl_cache[d.first].first, lvl);
else if (use_lvl_cache == 2)
res.first->second =
std::min(res.first->second, d.second);
lvl = std::min(lvl_cache[d.first].first, lvl);
}
lvl_cache[d.first] = std::make_pair(lvl, true);
}
}
unsigned& t = tr_cache[dest * 2 + is_acc];
if (t == 0) // Create transition.
t = res->new_acc_transition(src, dest,
i->current_condition(), is_acc);
t = res->new_acc_transition(src, dest, i.cond, is_acc);
else // Update existing transition.
res->trans_data(t).cond |= i->current_condition();
res->trans_data(t).cond |= i.cond;
}
tr_cache.clear();
}
#ifdef DEGEN_DEBUG
std::vector<bdd>::iterator i;
std::cout << "Orig. order: \t";
for (i = order.begin(); i != order.end(); i++)
for (auto i: order)
{
bdd_print_acc(std::cout, dict, *i);
std::cout << ", ";
std::cout << i << ", ";
}
std::cout << std::endl;
orders.print(dict);
std::cout << '\n';
orders.print();
#endif
delete m;
res->merge_transitions();
return res;
}
}
tgba_digraph_ptr
degeneralize(const const_tgba_ptr& a,
degeneralize(const const_tgba_digraph_ptr& a,
bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{
@ -616,7 +560,7 @@ namespace spot
}
tgba_digraph_ptr
degeneralize_tba(const const_tgba_ptr& a,
degeneralize_tba(const const_tgba_digraph_ptr& a,
bool use_z_lvl, bool use_cust_acc_orders,
int use_lvl_cache, bool skip_levels)
{

4
src/tgbaalgos/degen.hh
View file

@ -49,13 +49,13 @@ namespace spot
/// with transition-based acceptance.
/// \@{
SPOT_API tgba_digraph_ptr
degeneralize(const const_tgba_ptr& a, bool use_z_lvl = true,
degeneralize(const const_tgba_digraph_ptr& a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
int use_lvl_cache = 1,
bool skip_levels = true);
SPOT_API tgba_digraph_ptr
degeneralize_tba(const const_tgba_ptr& a, bool use_z_lvl = true,
degeneralize_tba(const const_tgba_digraph_ptr& a, bool use_z_lvl = true,
bool use_cust_acc_orders = false,
int use_lvl_cache = 1,
bool skip_levels = true);

46
src/tgbaalgos/isweakscc.cc
View file

@ -31,7 +31,7 @@ namespace spot
public:
bool result;
weak_checker(const scc_map& map)
weak_checker(const scc_info& map)
: enumerate_cycles(map), result(true)
{
}
@ -65,10 +65,10 @@ namespace spot
}
bool
is_inherently_weak_scc(scc_map& map, unsigned scc)
is_inherently_weak_scc(scc_info& map, unsigned scc)
{
// If no cycle is accepting, the SCC is weak.
if (!map.accepting(scc))
if (!map.is_accepting_scc(scc))
return true;
// If the SCC is accepting, but one cycle is not, the SCC is not
// weak.
@ -78,57 +78,43 @@ namespace spot
}
bool
is_weak_scc(scc_map& map, unsigned scc)
is_weak_scc(scc_info& map, unsigned scc)
{
// If no cycle is accepting, the SCC is weak.
if (!map.accepting(scc))
if (!map.is_accepting_scc(scc))
return true;
// If all transitions use the same acceptance set, the SCC is weak.
return map.useful_acc_of(scc).size() == 1;
return map.used_acc_of(scc).size() == 1;
}
bool
is_complete_scc(scc_map& map, unsigned scc)
is_complete_scc(scc_info& map, unsigned scc)
{
auto a = map.get_aut();
for (auto s: map.states_of(scc))
{
tgba_succ_iterator* it = a->succ_iter(s);
// If a state has no successors, the SCC is not complete.
if (!it->first())
{
a->release_iter(it);
return false;
}
// Sum guards on all outgoing transitions.
bool has_succ = false;
bdd sumall = bddfalse;
do
for (auto& t: a->out(s))
{
const state *next = it->current_state();
// check it's the same scc
if (map.scc_of_state(next) == scc)
sumall |= it->current_condition();
next->destroy();
has_succ = true;
if (map.scc_of(t.dst) == scc)
sumall |= t.cond;
if (sumall == bddtrue)
break;
}
while (it->next());
a->release_iter(it);
if (sumall != bddtrue)
if (!has_succ || sumall != bddtrue)
return false;
}
return true;
}
bool
is_terminal_scc(scc_map& map, unsigned scc)
is_terminal_scc(scc_info& map, unsigned scc)
{
// If all transitions use all acceptance conditions, the SCC is weak.
return (map.accepting(scc)
&& map.useful_acc_of(scc).size() == 1
return (map.is_accepting_scc(scc)
&& map.used_acc_of(scc).size() == 1
&& is_complete_scc(map, scc));
}
}

29
src/tgbaalgos/isweakscc.hh
View file

@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_ISWEAKSCC_HH
# define SPOT_TGBAALGOS_ISWEAKSCC_HH
#include "scc.hh"
#include "sccinfo.hh"
namespace spot
{
@ -36,15 +36,14 @@ namespace spot
/// Note the terminal SCCs are also inherently weak with that
/// definition.
///
/// The scc_map \a map should have been built already. The absence
/// of accepting cycle is easy to check (the scc_map can tell
/// whether the SCC is non-accepting already). Similarly, an SCC in
/// which all transitions belong to all acceptance sets is
/// necessarily weak.
/// For other accepting SCCs, this function enumerates all cycles in
/// the given SCC (it stops if it find a non-accepting cycle).
/// The absence of accepting cycle is easy to check (the scc_info
/// object can tell whether the SCC is non-accepting already).
/// Similarly, an SCC in which all transitions belong to all
/// acceptance sets is necessarily weak. For other accepting SCCs,
/// this function enumerates all cycles in the given SCC (it stops
/// if it find a non-accepting cycle).
SPOT_API bool
is_inherently_weak_scc(scc_map& map, unsigned scc);
is_inherently_weak_scc(scc_info& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is weak.
///
@ -52,27 +51,21 @@ namespace spot
/// are fully accepting (i.e., the belong to all acceptance sets).
///
/// Note that terminal SCCs are also weak with that definition.
///
/// The scc_map \a map should have been built already.
SPOT_API bool
is_weak_scc(scc_map& map, unsigned scc);
is_weak_scc(scc_info& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is complete.
///
/// An SCC is complete iff for all states and all label there exists
/// a transition that stays into this SCC.
///
/// The scc_map \a map should have been built already.
SPOT_API bool
is_complete_scc(scc_map& map, unsigned scc);
is_complete_scc(scc_info& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is terminal.
///
/// An SCC is terminal if it is weak, complete, and accepting.
///
/// The scc_map \a map should have been built already.
SPOT_API bool
is_terminal_scc(scc_map& map, unsigned scc);
is_terminal_scc(scc_info& map, unsigned scc);
/// @}
}

37
src/tgbaalgos/minimize.cc
View file

@ -41,7 +41,7 @@
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/safety.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/bfssteps.hh"
#include "tgbaalgos/isdet.hh"
@ -183,7 +183,7 @@ namespace spot
struct wdba_search_acc_loop : public bfs_steps
{
wdba_search_acc_loop(const const_tgba_ptr& det_a,
unsigned scc_n, scc_map& sm,
unsigned scc_n, scc_info& sm,
power_map& pm, const state* dest)
: bfs_steps(det_a), scc_n(scc_n), sm(sm), pm(pm), dest(dest)
{
@ -194,7 +194,8 @@ namespace spot
filter(const state* s)
{
s = seen(s);
if (sm.scc_of_state(s) != scc_n)
if (sm.scc_of(std::static_pointer_cast<const tgba_digraph>(a_)
->state_number(s)) != scc_n)
return 0;
return s;
}
@ -206,7 +207,7 @@ namespace spot
}
unsigned scc_n;
scc_map& sm;
scc_info& sm;
power_map& pm;
const state* dest;
state_unicity_table seen;
@ -215,12 +216,12 @@ namespace spot
bool
wdba_scc_is_accepting(const const_tgba_digraph_ptr& det_a, unsigned scc_n,
const const_tgba_ptr& orig_a, scc_map& sm,
const const_tgba_ptr& orig_a, scc_info& sm,
power_map& pm)
{
// Get some state from the SCC #n.
const state* start = sm.one_state_of(scc_n)->clone();
const state* start = det_a->state_from_number(sm.one_state_of(scc_n));
// Find a loop around START in SCC #n.
wdba_search_acc_loop wsal(det_a, scc_n, sm, pm, start);
@ -478,7 +479,7 @@ namespace spot
}
tgba_digraph_ptr minimize_monitor(const const_tgba_ptr& a)
tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
@ -498,7 +499,7 @@ namespace spot
return res;
}
tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a)
tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a)
{
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
@ -520,8 +521,7 @@ namespace spot
// We also keep track of whether an SCC is useless
// (i.e., it is not the start of any accepting word).
scc_map sm(det_a);
sm.build_map();
scc_info sm(det_a);
unsigned scc_count = sm.scc_count();
// SCC that have been marked as useless.
std::vector<bool> useless(scc_count);
@ -537,8 +537,8 @@ namespace spot
for (unsigned m = 0; m < scc_count; ++m)
{
bool is_useless = true;
bool transient = sm.trivial(m);
const scc_map::succ_type& succ = sm.succ(m);
bool transient = sm.is_trivial(m);
auto& succ = sm.succ(m);
if (transient && succ.empty())
{
@ -552,11 +552,10 @@ namespace spot
// Also SCCs are useless if all their successor are
// useless.
unsigned l = k;
for (scc_map::succ_type::const_iterator j = succ.begin();
j != succ.end(); ++j)
for (auto& j: succ)
{
is_useless &= useless[j->first];
unsigned dj = d[j->first];
is_useless &= useless[j.dst];
unsigned dj = d[j.dst];
if (dj < l)
l = dj;
}
@ -586,10 +585,8 @@ namespace spot
if (!is_useless)
{
hash_set* dest_set = (d[m] & 1) ? non_final : final;
const std::list<const state*>& l = sm.states_of(m);
std::list<const state*>::const_iterator il;
for (il = l.begin(); il != l.end(); ++il)
dest_set->insert((*il)->clone());
for (auto s: sm.states_of(m))
dest_set->insert(det_a->state_from_number(s));
}
}
}

4
src/tgbaalgos/minimize.hh
View file

@ -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 tgba_digraph_ptr minimize_monitor(const const_tgba_ptr& a);
SPOT_API tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a);
/// \brief Minimize a Büchi automaton in the WDBA class.
///
@ -93,7 +93,7 @@ namespace spot
month = oct
}
\endverbatim */
SPOT_API tgba_digraph_ptr minimize_wdba(const const_tgba_ptr& a);
SPOT_API tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a);
/// \brief Minimize an automaton if it represents an obligation property.
///

23
src/tgbaalgos/powerset.cc
View file

@ -28,7 +28,7 @@
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
#include "bdd.h"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/cycles.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgba/tgbaproduct.hh"
@ -42,8 +42,9 @@
namespace spot
{
// FIXME: Redo this algorithm using the tgba_digraph interface.
tgba_digraph_ptr
tgba_powerset(const const_tgba_ptr& aut, power_map& pm, bool merge)
tgba_powerset(const const_tgba_digraph_ptr& aut, power_map& pm, bool merge)
{
typedef power_map::power_state power_state;
typedef std::map<power_map::power_state, int> power_set;
@ -112,7 +113,7 @@ namespace spot
}
tgba_digraph_ptr
tgba_powerset(const const_tgba_ptr& aut)
tgba_powerset(const const_tgba_digraph_ptr& aut)
{
power_map pm;
return tgba_powerset(aut, pm);
@ -130,7 +131,7 @@ namespace spot
typedef std::set<trans*> trans_set;
typedef std::vector<trans_set> set_set;
protected:
const_tgba_ptr ref_;
const_tgba_digraph_ptr ref_;
power_map& refmap_;
trans_set reject_; // set of rejecting transitions
set_set accept_; // set of cycles that are accepting
@ -139,7 +140,7 @@ namespace spot
unsigned cycles_left_; // count of cycles left to explore
public:
fix_scc_acceptance(const scc_map& sm, const_tgba_ptr ref,
fix_scc_acceptance(const scc_info& sm, const_tgba_digraph_ptr ref,
power_map& refmap, unsigned threshold)
: enumerate_cycles(sm), ref_(ref), refmap_(refmap),
threshold_(threshold)
@ -173,8 +174,7 @@ namespace spot
bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
{
auto a = std::static_pointer_cast<tgba_digraph>
(std::const_pointer_cast<tgba>(aut_));
auto a = std::const_pointer_cast<tgba_digraph>(aut_);
// Build an automaton representing this loop.
auto loop_a = make_tgba_digraph(aut_->get_dict());
@ -268,20 +268,19 @@ namespace spot
static bool
fix_dba_acceptance(tgba_digraph_ptr det,
const_tgba_ptr ref, power_map& refmap,
const_tgba_digraph_ptr ref, power_map& refmap,
unsigned threshold)
{
det->copy_acceptance_conditions_of(ref);
scc_map sm(det);
sm.build_map();
scc_info sm(det);
unsigned scc_count = sm.scc_count();
fix_scc_acceptance fsa(sm, ref, refmap, threshold);
for (unsigned m = 0; m < scc_count; ++m)
if (!sm.trivial(m))
if (!sm.is_trivial(m))
if (fsa.fix_scc(m))
return true;
return false;
@ -289,7 +288,7 @@ namespace spot
}
tgba_digraph_ptr
tba_determinize(const const_tgba_ptr& aut,
tba_determinize(const const_tgba_digraph_ptr& aut,
unsigned threshold_states, unsigned threshold_cycles)
{
power_map pm;

7
src/tgbaalgos/powerset.hh
View file

@ -65,9 +65,10 @@ namespace spot
/// transitions.
//@{
SPOT_API tgba_digraph_ptr
tgba_powerset(const const_tgba_ptr& aut, power_map& pm, bool merge = true);
tgba_powerset(const const_tgba_digraph_ptr& aut,
power_map& pm, bool merge = true);
SPOT_API tgba_digraph_ptr
tgba_powerset(const const_tgba_ptr& aut);
tgba_powerset(const const_tgba_digraph_ptr& aut);
//@}
@ -107,7 +108,7 @@ namespace spot
/// whenever an SCC of the constructed automaton has more than \a
/// threshold_cycles cycles.
SPOT_API tgba_digraph_ptr
tba_determinize(const const_tgba_ptr& aut,
tba_determinize(const const_tgba_digraph_ptr& aut,
unsigned threshold_states = 0,
unsigned threshold_cycles = 0);

108
src/tgbaalgos/product.cc Normal file
View file

@ -0,0 +1,108 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include "product.hh"
#include "tgba/tgbagraph.hh"
#include <deque>
#include <unordered_map>
#include "misc/hash.hh"
namespace spot
{
namespace
{
typedef std::pair<unsigned, unsigned> product_state;
struct product_state_hash
{
size_t
operator()(product_state s) const
{
return wang32_hash(s.first ^ wang32_hash(s.second));
}
};
}
tgba_digraph_ptr product(const const_tgba_digraph_ptr& left,
const const_tgba_digraph_ptr& right,
unsigned left_state,
unsigned right_state)
{
std::unordered_map<product_state, unsigned, product_state_hash> s2n;
std::deque<std::pair<product_state, unsigned>> todo;
assert(left->get_dict() == right->get_dict());
auto res = make_tgba_digraph(left->get_dict());
res->copy_ap_of(left);
res->copy_ap_of(right);
res->set_acceptance_conditions(left->acc().num_sets()
+ right->acc().num_sets());
auto v = new product_states;
res->set_named_prop("product-states", v, [](void* vv) {
delete static_cast<product_states*>(vv);
});
auto new_state =
[&](unsigned left_state, unsigned right_state) -> unsigned
{
product_state x(left_state, right_state);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
p.first->second = res->new_state();
todo.emplace_back(x, p.first->second);
assert(p.first->second == v->size());
v->push_back(x);
}
return p.first->second;
};
new_state(left_state, right_state);
while (!todo.empty())
{
auto top = todo.front();
todo.pop_front();
for (auto& l: left->out(top.first.first))
for (auto& r: right->out(top.first.second))
{
auto cond = l.cond & r.cond;
if (cond == bddfalse)
continue;
auto dst = new_state(l.dst, r.dst);
res->new_transition(top.second, dst, cond,
res->acc().join(left->acc(), l.acc,
right->acc(), r.acc));
// If right is deterministic, we can abort immediately!
}
}
return res;
}
tgba_digraph_ptr product(const const_tgba_digraph_ptr& left,
const const_tgba_digraph_ptr& right)
{
return product(left, right,
left->get_init_state_number(),
right->get_init_state_number());
}
}

45
src/tgbaalgos/product.hh Normal file
View file

@ -0,0 +1,45 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBAALGOS_PRODUCT_HH
# define SPOT_TGBAALGOS_PRODUCT_HH
#include "misc/common.hh"
#include "tgba/fwd.hh"
#include <vector>
#include <utility>
namespace spot
{
// The tgba constructed by product() below contain property named
// "product-states" with type product_states.
typedef std::vector<std::pair<unsigned, unsigned>> product_states;
SPOT_API
tgba_digraph_ptr product(const const_tgba_digraph_ptr& left,
const const_tgba_digraph_ptr& right);
SPOT_API
tgba_digraph_ptr product(const const_tgba_digraph_ptr& left,
const const_tgba_digraph_ptr& right,
unsigned left_state,
unsigned right_state);
}
#endif // SPOT_TGBAALGOS_PRODUCT_HH

67
src/tgbaalgos/safety.cc
View file

@ -24,26 +24,23 @@
namespace spot
{
bool
is_guarantee_automaton(const const_tgba_ptr& aut, const scc_map* sm)
is_guarantee_automaton(const const_tgba_digraph_ptr& aut,
const scc_info* sm)
{
// Create an scc_map of the user did not give one to us.
// Create an scc_info if the user did not give one to us.
bool need_sm = !sm;
if (need_sm)
{
scc_map* x = new scc_map(aut);
x->build_map();
sm = x;
}
sm = new scc_info(aut);
bool result = true;
unsigned scc_count = sm->scc_count();
for (unsigned scc = 0; (scc < scc_count) && result; ++scc)
for (unsigned scc = 0; scc < scc_count; ++scc)
{
if (!sm->accepting(scc))
if (!sm->is_accepting_scc(scc))
continue;
// Accepting SCCs should have only one state.
const std::list<const state*>& st = sm->states_of(scc);
auto& st = sm->states_of(scc);
if (st.size() != 1)
{
result = false;
@ -51,50 +48,28 @@ namespace spot
}
// The state should have only one transition that is a
// self-loop labelled by true.
const state* s = *st.begin();
tgba_succ_iterator* it = aut->succ_iter(s);
it->first();
assert(!it->done());
state* dest = it->current_state();
bdd cond = it->current_condition();
result = (!it->next()) && (cond == bddtrue) && (!dest->compare(s));
dest->destroy();
aut->release_iter(it);
auto src = st.front();
auto out = aut->out(src);
auto it = out.begin();
assert(it != out.end());
result =
(it->cond == bddtrue) && (it->dst == src) && (++it == out.end());
if (!result)
break;
}
// Free the scc_map if we created it.
if (need_sm)
delete sm;
return result;
}
bool is_safety_mwdba(const const_tgba_ptr& aut)
bool is_safety_mwdba(const const_tgba_digraph_ptr& aut)
{
state_unicity_table seen; // States already seen.
std::deque<const state*> todo; // A queue of states yet to explore.
todo.push_back(seen(aut->get_init_state()));
bool all_accepting = true;
while (all_accepting && !todo.empty())
{
const state* s = todo.front();
todo.pop_front();
for (auto it: aut->succ(s))
{
auto acc = it->current_acceptance_conditions();
if (!aut->acc().accepting(acc))
{
all_accepting = false;
break;
}
if (const state* d = seen.is_new(it->current_state()))
todo.push_back(d);
}
}
return all_accepting;
for (auto& t: aut->transitions())
if (!aut->is_dead_transition(t))
if (!aut->acc().accepting(t.acc))
return false;
return true;
}

14
src/tgbaalgos/safety.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
// Copyright (C) 2010, 2011, 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_SAFETY_HH
# define SPOT_TGBAALGOS_SAFETY_HH
#include "scc.hh"
#include "sccinfo.hh"
namespace spot
{
@ -43,11 +43,11 @@ namespace spot
///
/// \param aut the automaton to check
///
/// \param sm an scc_map of the automaton if available (it will be
/// built otherwise. If you supply an scc_map you should call
/// build_map() before passing it to this function.
/// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise).
SPOT_API bool
is_guarantee_automaton(const const_tgba_ptr& aut, const scc_map* sm = 0);
is_guarantee_automaton(const const_tgba_digraph_ptr& aut,
const scc_info* sm = 0);
/// \brief Whether a minimized WDBA represents a safety property.
///
@ -57,7 +57,7 @@ namespace spot
///
/// \param aut the automaton to check
SPOT_API bool
is_safety_mwdba(const const_tgba_ptr& aut);
is_safety_mwdba(const const_tgba_digraph_ptr& aut);
}

12
src/tgbaalgos/sccinfo.cc
View file

@ -121,7 +121,7 @@ namespace spot
node_.emplace_back(acc, triv);
std::swap(node_.back().succ, root_.front().node.succ);
std::swap(node_.back().states, root_.front().node.states);
node_.back().accepting = aut->acc().accepting(acc);
node_.back().accepting = !triv && aut->acc().accepting(acc);
root_.pop_front();
// Record the transition between the SCC being popped
// and the previous SCC.
@ -229,6 +229,16 @@ namespace spot
}
std::set<acc_cond::mark_t> scc_info::used_acc_of(unsigned scc) const
{
std::set<acc_cond::mark_t> res;
for (auto src: states_of(scc))
for (auto& t: aut_->out(src))
if (scc_of(t.dst) == scc)
res.insert(t.acc);
return res;
}
std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
{
unsigned n = aut_->num_states();

19
src/tgbaalgos/sccinfo.hh
View file

@ -45,12 +45,12 @@ namespace spot
struct scc_node
{
scc_node():
acc(0U), trivial(true)
acc(0U), trivial(true), accepting(false), useful(false)
{
}
scc_node(acc_cond::mark_t acc, bool trivial):
acc(acc), trivial(trivial)
acc(acc), trivial(trivial), accepting(false), useful(false)
{
}
@ -104,6 +104,18 @@ namespace spot
return node(scc).states;
}
unsigned one_state_of(unsigned scc) const
{
return states_of(scc).front();
}
/// \brief Get number of the SCC containing the initial state.
unsigned initial() const
{
assert(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
return scc_count() - 1;
}
const scc_succs& succ(unsigned scc) const
{
return node(scc).succ;
@ -138,6 +150,9 @@ namespace spot
/// each accepting SCC.
std::vector<std::set<acc_cond::mark_t>> used_acc() const;
std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
std::vector<bool> weak_sccs() const;
bdd scc_ap_support(unsigned scc) const;

27
src/tgbatest/complementation.cc
View file

@ -122,7 +122,7 @@ int main(int argc, char* argv[])
{
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
spot::tgba_ptr a = spot::tgba_parse(file, pel, dict, env);
spot::tgba_digraph_ptr a = spot::tgba_parse(file, pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, file, pel))
return 2;
@ -147,15 +147,13 @@ int main(int argc, char* argv[])
}
else if (print_formula)
{
spot::tgba_ptr a;
spot::ltl::parse_error_list p1;
const spot::ltl::formula* f1 = spot::ltl::parse(file, p1);
if (spot::ltl::format_parse_errors(std::cerr, file, p1))
return 2;
a = spot::ltl_to_tgba_fm(f1, dict);
auto a = spot::ltl_to_tgba_fm(f1, dict);
spot::tgba_ptr complement = 0;
complement = spot::make_safra_complement(a);
@ -164,7 +162,7 @@ int main(int argc, char* argv[])
}
else if (stats)
{
spot::tgba_ptr a;
spot::tgba_digraph_ptr a;
const spot::ltl::formula* f1 = 0;
if (formula)
@ -211,10 +209,8 @@ int main(int argc, char* argv[])
if (formula)
{
const spot::ltl::formula* nf1 =
spot::ltl::unop::instance(spot::ltl::unop::Not,
f1->clone());
spot::tgba_ptr a2 = spot::ltl_to_tgba_fm(nf1, dict);
auto nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone());
auto a2 = spot::ltl_to_tgba_fm(nf1, dict);
spot::tgba_statistics a_size = spot::stats_reachable(a2);
std::cout << "Not Formula: "
<< a_size.states << ", "
@ -234,14 +230,11 @@ int main(int argc, char* argv[])
if (spot::ltl::format_parse_errors(std::cerr, file, p1))
return 2;
spot::tgba_ptr Af = spot::ltl_to_tgba_fm(f1, dict);
const spot::ltl::formula* nf1 =
spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone());
spot::tgba_ptr Anf = spot::ltl_to_tgba_fm(nf1, dict);
spot::tgba_ptr nAf = spot::make_safra_complement(Af);
spot::tgba_ptr nAnf = spot::make_safra_complement(Anf);
auto Af = spot::ltl_to_tgba_fm(f1, dict);
auto nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone());
auto Anf = spot::ltl_to_tgba_fm(nf1, dict);
auto nAf = spot::make_safra_complement(Af);
auto nAnf = spot::make_safra_complement(Anf);
auto ec = spot::couvreur99(spot::product(nAf, nAnf));
auto res = ec->check();
spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton());

2
src/tgbatest/emptchk.cc
View file

@ -103,7 +103,7 @@ main(int argc, char** argv)
{
auto a = spot::ltl_to_taa(f, d);
aut[0] = a;
aut[1] = spot::degeneralize_tba(a);
aut[1] = spot::degeneralize_tba(spot::tgba_dupexp_bfs(a));
}
{
auto a = spot::ltl_to_tgba_fm(f, d);

14
src/tgbatest/ltl2ta.test
View file

@ -400,15 +400,15 @@ in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)
-TA -lv -sp | 45 | 676 | 9
-TA -lv -sp -RT | 35 | 566 | 4
-TA -DS | 54 | 722 | 26
-TA -DS -RT | 42 | 608 | 18
-TA -DS -RT | 38 | 534 | 17
-TA -DS -lv | 55 | 800 | 19
-TA -DS -lv -RT | 44 | 702 | 13
-TA -DS -lv -RT | 39 | 608 | 11
-TA -DS -sp | 54 | 776 | 18
-TA -DS -sp -RT | 43 | 678 | 12
-TA -DS -sp -RT | 38 | 586 | 10
-TA -DS -lv -sp | 55 | 800 | 19
-TA -DS -lv -sp -RT | 44 | 702 | 13
-x -TA -DS -in | 55 | 694 | 11
-x -TA -DS -in -RT | 41 | 597 | 8
-TA -DS -lv -sp -RT | 39 | 608 | 11
-x -TA -DS -in | 55 | 696 | 11
-x -TA -DS -in -RT | 42 | 603 | 8
in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))
-TGTA | 69 | 1539 | XXX
-TGTA -RT | 49 | 935 | XXX
@ -429,7 +429,7 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))
-TA -DS -lv -sp | 125 | 3028 | 42
-TA -DS -lv -sp -RT | 97 | 2149 | 40
-x -TA -DS -in | 125 | 1838 | 25
-x -TA -DS -in -RT | 87 | 1296 | 25
-x -TA -DS -in -RT | 90 | 1368 | 25
EOF
sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt

33
src/tgbatest/ltl2tgba.cc
View file

@ -54,7 +54,7 @@
#include "tgbaalgos/gtec/gtec.hh"
#include "misc/timer.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/emptiness_stats.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/sccinfo.hh"
@ -1286,14 +1286,14 @@ checked_main(int argc, char** argv)
{
if (degeneralize_opt == DegenTBA)
{
a = spot::degeneralize_tba(a, degen_reset, degen_order,
degen_cache);
a = spot::degeneralize_tba(ensure_digraph(a),
degen_reset, degen_order, degen_cache);
}
else if (degeneralize_opt == DegenSBA)
{
tm.start("degeneralization");
a = spot::degeneralize(a, degen_reset, degen_order,
degen_cache);
a = spot::degeneralize(ensure_digraph(a),
degen_reset, degen_order, degen_cache);
tm.stop("degeneralization");
assume_sba = true;
}
@ -1303,7 +1303,8 @@ checked_main(int argc, char** argv)
&& (!f || f->is_syntactic_recurrence()))
{
tm.start("determinization 2");
auto determinized = tba_determinize(a, 0, opt_determinize_threshold);
auto determinized = tba_determinize(ensure_digraph(a), 0,
opt_determinize_threshold);
tm.stop("determinization 2");
if (determinized)
a = determinized;
@ -1312,7 +1313,7 @@ checked_main(int argc, char** argv)
if (opt_monitor)
{
tm.start("Monitor minimization");
a = minimize_monitor(a);
a = minimize_monitor(ensure_digraph(a));
tm.stop("Monitor minimization");
assume_sba = false; // All states are accepting, so double
// circles in the dot output are
@ -1397,7 +1398,7 @@ checked_main(int argc, char** argv)
if (opt_monitor)
{
tm.start("Monitor minimization");
a = minimize_monitor(a);
a = minimize_monitor(ensure_digraph(a));
tm.stop("Monitor minimization");
assume_sba = false; // All states are accepting, so double
// circles in the dot output are
@ -1509,7 +1510,7 @@ checked_main(int argc, char** argv)
if (degeneralize_opt == DegenTBA)
{
tm.start("degeneralize product");
a = spot::degeneralize_tba(a,
a = spot::degeneralize_tba(ensure_digraph(a),
degen_reset,
degen_order,
degen_cache);
@ -1518,7 +1519,7 @@ checked_main(int argc, char** argv)
else if (degeneralize_opt == DegenSBA)
{
tm.start("degeneralize product");
a = spot::degeneralize(a,
a = spot::degeneralize(ensure_digraph(a),
degen_reset,
degen_order,
degen_cache);
@ -1572,7 +1573,7 @@ checked_main(int argc, char** argv)
// It is possible that we have applied other
// operations to the automaton since its initial
// degeneralization. Let's degeneralize again!
auto s = spot::degeneralize(a, degen_reset,
auto s = spot::degeneralize(ensure_digraph(a), degen_reset,
degen_order, degen_cache);
spot::never_claim_reachable(std::cout, s, f, spin_comments);
}
@ -1621,8 +1622,8 @@ checked_main(int argc, char** argv)
}
else
{
bool g = is_guarantee_automaton(a);
bool s = is_safety_mwdba(a);
bool g = is_guarantee_automaton(ensure_digraph(a));
bool s = is_safety_mwdba(ensure_digraph(a));
if (g && !s)
{
std::cout << "this is a guarantee property (hence, "
@ -1649,8 +1650,7 @@ checked_main(int argc, char** argv)
break;
case 15:
{
spot::scc_map m(a);
m.build_map();
spot::scc_info m(ensure_digraph(a));
spot::enumerate_cycles c(m);
unsigned max = m.scc_count();
for (unsigned n = 0; n < max; ++n)
@ -1662,8 +1662,7 @@ checked_main(int argc, char** argv)
}
case 16:
{
spot::scc_map m(a);
m.build_map();
spot::scc_info m(ensure_digraph(a));
unsigned max = m.scc_count();
for (unsigned n = 0; n < max; ++n)
{

14
src/tgbatest/randtgba.cc
View file

@ -46,7 +46,7 @@
#include "misc/random.hh"
#include "misc/optionmap.hh"
#include "tgbaalgos/degen.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/product.hh"
#include "misc/timer.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
@ -85,8 +85,8 @@ const char* default_algos[] = {
std::vector<ec_algo> ec_algos;
spot::emptiness_check_ptr
cons_emptiness_check(int num, spot::const_tgba_ptr a,
const spot::const_tgba_ptr& degen,
cons_emptiness_check(int num, spot::const_tgba_digraph_ptr a,
const spot::const_tgba_digraph_ptr& degen,
unsigned int n_acc)
{
auto inst = ec_algos[num].inst;
@ -579,8 +579,8 @@ main(int argc, char** argv)
bool stop_on_first_difference = false;
spot::tgba_ptr formula = nullptr;
spot::tgba_ptr product = nullptr;
spot::tgba_digraph_ptr formula = nullptr;
spot::tgba_digraph_ptr product = nullptr;
spot::option_map options;
@ -906,7 +906,7 @@ main(int argc, char** argv)
spot::srand(opt_ec_seed);
spot::tgba_ptr a =
spot::tgba_digraph_ptr a =
spot::random_graph(opt_n, opt_d, apf, dict,
opt_n_acc, opt_a, opt_t);
if (formula)
@ -925,7 +925,7 @@ main(int argc, char** argv)
}
else
{
spot::tgba_ptr degen = nullptr;
spot::tgba_digraph_ptr degen = nullptr;
if (opt_degen && real_n_acc > 1)
degen = degeneralize_tba(a);