graph: rename num_transitions() as num_edges()
And in fact, rename most "trans*" as "edges*", because that what they really are. * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc, src/dstarparse/dstarparse.yy, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc, src/graph/graph.hh, src/graph/ngraph.hh, src/ltlvisit/exclusive.cc, src/parseaut/parseaut.yy, src/tests/complementation.cc, src/tests/graph.cc, src/tests/ltl2tgba.cc, src/tests/ngraph.cc, src/tests/twagraph.cc, src/twa/twagraph.cc, src/twa/twagraph.hh, src/twa/twamask.hh, src/twaalgos/are_isomorphic.cc, src/twaalgos/are_isomorphic.hh, src/twaalgos/canonicalize.cc, src/twaalgos/cleanacc.cc, src/twaalgos/complete.cc, src/twaalgos/compsusp.cc, src/twaalgos/cycles.cc, src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc, src/twaalgos/dtgbacomp.cc, src/twaalgos/dtgbasat.cc, src/twaalgos/dupexp.cc, src/twaalgos/emptiness.cc, src/twaalgos/isunamb.cc, src/twaalgos/isweakscc.cc, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/mask.hh, src/twaalgos/minimize.cc, src/twaalgos/postproc.cc, src/twaalgos/powerset.cc, src/twaalgos/product.cc, src/twaalgos/randomgraph.cc, src/twaalgos/randomize.cc, src/twaalgos/randomize.hh, src/twaalgos/relabel.cc, src/twaalgos/remfin.cc, src/twaalgos/safety.cc, src/twaalgos/sbacc.cc, src/twaalgos/sccfilter.cc, src/twaalgos/sepsets.cc, src/twaalgos/simulation.cc, src/twaalgos/stutter.cc, src/twaalgos/totgba.cc: Rename these.
This commit is contained in:
Alexandre Duret-Lutz
parent
a1ba0a89c5
commit
af8634d8c4
53 changed files with 685 additions and 693 deletions
|
|
@ -216,7 +216,7 @@ static const struct argp_child children[] =
|
||||||
{ 0, 0, 0, 0 }
|
{ 0, 0, 0, 0 }
|
||||||
};
|
};
|
||||||
|
|
||||||
typedef spot::twa_graph::graph_t::trans_storage_t tr_t;
|
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
|
||||||
typedef std::set<std::vector<tr_t>> unique_aut_t;
|
typedef std::set<std::vector<tr_t>> unique_aut_t;
|
||||||
static long int match_count = 0;
|
static long int match_count = 0;
|
||||||
static spot::option_map extra_options;
|
static spot::option_map extra_options;
|
||||||
|
|
@ -502,7 +502,7 @@ namespace
|
||||||
|
|
||||||
// If --stats or --name is used, duplicate the automaton so we
|
// If --stats or --name is used, duplicate the automaton so we
|
||||||
// never modify the original automaton (e.g. with
|
// never modify the original automaton (e.g. with
|
||||||
// merge_transitions()) and the statistics about it make sense.
|
// merge_edges()) and the statistics about it make sense.
|
||||||
auto aut = ((automaton_format == Stats) || opt_name)
|
auto aut = ((automaton_format == Stats) || opt_name)
|
||||||
? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
|
? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
|
||||||
: haut->aut;
|
: haut->aut;
|
||||||
|
|
@ -512,7 +512,7 @@ namespace
|
||||||
if (opt_stripacc)
|
if (opt_stripacc)
|
||||||
spot::strip_acceptance_here(aut);
|
spot::strip_acceptance_here(aut);
|
||||||
if (opt_merge)
|
if (opt_merge)
|
||||||
aut->merge_transitions();
|
aut->merge_edges();
|
||||||
if (opt_clean_acc || opt_rem_fin)
|
if (opt_clean_acc || opt_rem_fin)
|
||||||
cleanup_acceptance_here(aut);
|
cleanup_acceptance_here(aut);
|
||||||
if (opt_sep_sets)
|
if (opt_sep_sets)
|
||||||
|
|
@ -534,7 +534,7 @@ namespace
|
||||||
bool matched = true;
|
bool matched = true;
|
||||||
|
|
||||||
matched &= opt_states.contains(aut->num_states());
|
matched &= opt_states.contains(aut->num_states());
|
||||||
matched &= opt_edges.contains(aut->num_transitions());
|
matched &= opt_edges.contains(aut->num_edges());
|
||||||
matched &= opt_accsets.contains(aut->acc().num_sets());
|
matched &= opt_accsets.contains(aut->acc().num_sets());
|
||||||
if (opt_is_complete)
|
if (opt_is_complete)
|
||||||
matched &= is_complete(aut);
|
matched &= is_complete(aut);
|
||||||
|
|
@ -602,8 +602,8 @@ namespace
|
||||||
auto tmp =
|
auto tmp =
|
||||||
spot::canonicalize(make_twa_graph(aut,
|
spot::canonicalize(make_twa_graph(aut,
|
||||||
spot::twa::prop_set::all()));
|
spot::twa::prop_set::all()));
|
||||||
if (!opt->uniq->emplace(tmp->transition_vector().begin() + 1,
|
if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
|
||||||
tmp->transition_vector().end()).second)
|
tmp->edge_vector().end()).second)
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -681,7 +681,7 @@ main(int argc, char** argv)
|
||||||
if (opt->are_isomorphic)
|
if (opt->are_isomorphic)
|
||||||
{
|
{
|
||||||
if (opt_merge)
|
if (opt_merge)
|
||||||
opt->are_isomorphic->merge_transitions();
|
opt->are_isomorphic->merge_edges();
|
||||||
opt->isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>
|
opt->isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>
|
||||||
(new spot::isomorphism_checker(opt->are_isomorphic));
|
(new spot::isomorphism_checker(opt->are_isomorphic));
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1151,7 +1151,7 @@ namespace
|
||||||
if (x[i]->acc().uses_fin_acceptance()) \
|
if (x[i]->acc().uses_fin_acceptance()) \
|
||||||
{ \
|
{ \
|
||||||
auto st = x[i]->num_states(); \
|
auto st = x[i]->num_states(); \
|
||||||
auto tr = x[i]->num_transitions(); \
|
auto tr = x[i]->num_edges(); \
|
||||||
auto ac = x[i]->acc().num_sets(); \
|
auto ac = x[i]->acc().num_sets(); \
|
||||||
x[i] = remove_fin(x[i]); \
|
x[i] = remove_fin(x[i]); \
|
||||||
if (verbose) \
|
if (verbose) \
|
||||||
|
|
@ -1161,7 +1161,7 @@ namespace
|
||||||
<< tr << " ed., " \
|
<< tr << " ed., " \
|
||||||
<< ac << " sets) -> (" \
|
<< ac << " sets) -> (" \
|
||||||
<< x[i]->num_states() << " st., " \
|
<< x[i]->num_states() << " st., " \
|
||||||
<< x[i]->num_transitions() << " ed., " \
|
<< x[i]->num_edges() << " ed., " \
|
||||||
<< x[i]->acc().num_sets() << " sets)\n"; \
|
<< x[i]->acc().num_sets() << " sets)\n"; \
|
||||||
} \
|
} \
|
||||||
}
|
}
|
||||||
|
|
@ -1246,7 +1246,7 @@ namespace
|
||||||
|
|
||||||
if (verbose)
|
if (verbose)
|
||||||
std::cerr << "info: state-space has "
|
std::cerr << "info: state-space has "
|
||||||
<< statespace->num_transitions()
|
<< statespace->num_edges()
|
||||||
<< " edges\n";
|
<< " edges\n";
|
||||||
|
|
||||||
// Products of the state space with the positive automata.
|
// Products of the state space with the positive automata.
|
||||||
|
|
@ -1263,7 +1263,7 @@ namespace
|
||||||
std::cerr << ("info: building product between state-space and"
|
std::cerr << ("info: building product between state-space and"
|
||||||
" P") << i
|
" P") << i
|
||||||
<< " (" << pos[i]->num_states() << " st., "
|
<< " (" << pos[i]->num_states() << " st., "
|
||||||
<< pos[i]->num_transitions() << " ed.)\n";
|
<< pos[i]->num_edges() << " ed.)\n";
|
||||||
auto p = spot::product(pos[i], statespace);
|
auto p = spot::product(pos[i], statespace);
|
||||||
pos_prod[i] = p;
|
pos_prod[i] = p;
|
||||||
auto sm = new spot::scc_info(p);
|
auto sm = new spot::scc_info(p);
|
||||||
|
|
@ -1287,7 +1287,7 @@ namespace
|
||||||
std::cerr << ("info: building product between state-space and"
|
std::cerr << ("info: building product between state-space and"
|
||||||
" N") << i
|
" N") << i
|
||||||
<< " (" << neg[i]->num_states() << " st., "
|
<< " (" << neg[i]->num_states() << " st., "
|
||||||
<< neg[i]->num_transitions() << " ed.)\n";
|
<< neg[i]->num_edges() << " ed.)\n";
|
||||||
|
|
||||||
auto p = spot::product(neg[i], statespace);
|
auto p = spot::product(neg[i], statespace);
|
||||||
neg_prod[i] = p;
|
neg_prod[i] = p;
|
||||||
|
|
|
||||||
|
|
@ -63,7 +63,7 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\n\
|
||||||
\n\
|
\n\
|
||||||
Build 3 random, complete, and deterministic Rabin automata\n\
|
Build 3 random, complete, and deterministic Rabin automata\n\
|
||||||
with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\
|
with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\
|
||||||
a high density of transitions, and 3 to 4 atomic propositions:\n\
|
a high density of edges, and 3 to 4 atomic propositions:\n\
|
||||||
% randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\
|
% randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\
|
||||||
";
|
";
|
||||||
|
|
||||||
|
|
@ -79,15 +79,15 @@ static const argp_option options[] =
|
||||||
{ "acceptance", 'A', "ACCEPTANCE", 0,
|
{ "acceptance", 'A', "ACCEPTANCE", 0,
|
||||||
"specify the acceptance type of the automaton", 0 },
|
"specify the acceptance type of the automaton", 0 },
|
||||||
{ "acc-probability", 'a', "FLOAT", 0,
|
{ "acc-probability", 'a', "FLOAT", 0,
|
||||||
"probability that a transition belong to one acceptance set (0.2)", 0 },
|
"probability that an edge belongs to one acceptance set (0.2)", 0 },
|
||||||
{ "automata", 'n', "INT", 0, "number of automata to output (1)\n"\
|
{ "automata", 'n', "INT", 0, "number of automata to output (1)\n"\
|
||||||
"use a negative value for unbounded generation", 0 },
|
"use a negative value for unbounded generation", 0 },
|
||||||
{ "ba", 'B', 0, 0,
|
{ "ba", 'B', 0, 0,
|
||||||
"build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 },
|
"build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 },
|
||||||
{ "colored", OPT_COLORED, 0, 0,
|
{ "colored", OPT_COLORED, 0, 0,
|
||||||
"build an automaton in which each transition (or state if combined with "
|
"build an automaton in which each edge (or state if combined with "
|
||||||
"-S) belong to a single acceptance set", 0 },
|
"-S) belong to a single acceptance set", 0 },
|
||||||
{ "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 },
|
{ "density", 'd', "FLOAT", 0, "density of the edges (0.2)", 0 },
|
||||||
{ "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ",
|
{ "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ",
|
||||||
0 },
|
0 },
|
||||||
{ "unique", 'u', 0, 0,
|
{ "unique", 'u', 0, 0,
|
||||||
|
|
@ -133,7 +133,7 @@ static const struct argp_child children[] =
|
||||||
};
|
};
|
||||||
|
|
||||||
static const char* opt_acceptance = nullptr;
|
static const char* opt_acceptance = nullptr;
|
||||||
typedef spot::twa_graph::graph_t::trans_storage_t tr_t;
|
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
|
||||||
typedef std::set<std::vector<tr_t>> unique_aut_t;
|
typedef std::set<std::vector<tr_t>> unique_aut_t;
|
||||||
static spot::ltl::atomic_prop_set aprops;
|
static spot::ltl::atomic_prop_set aprops;
|
||||||
static range ap_count_given = {-1, -2}; // Must be two different negative val
|
static range ap_count_given = {-1, -2}; // Must be two different negative val
|
||||||
|
|
@ -364,8 +364,8 @@ main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
auto tmp = spot::canonicalize
|
auto tmp = spot::canonicalize
|
||||||
(make_twa_graph(aut, spot::twa::prop_set::all()));
|
(make_twa_graph(aut, spot::twa::prop_set::all()));
|
||||||
std::vector<tr_t> trans(tmp->transition_vector().begin() + 1,
|
std::vector<tr_t> trans(tmp->edge_vector().begin() + 1,
|
||||||
tmp->transition_vector().end());
|
tmp->edge_vector().end());
|
||||||
if (!opt_uniq->emplace(trans).second)
|
if (!opt_uniq->emplace(trans).second)
|
||||||
{
|
{
|
||||||
--trials;
|
--trials;
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
|
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -247,12 +247,12 @@ namespace spot
|
||||||
unsigned in_scc = sm_.scc_of_state(sin);
|
unsigned in_scc = sm_.scc_of_state(sin);
|
||||||
|
|
||||||
bdd cond = si->current_condition();
|
bdd cond = si->current_condition();
|
||||||
unsigned t = out_->new_transition(in, out, cond);
|
unsigned t = out_->new_edge(in, out, cond);
|
||||||
|
|
||||||
if (realizable_[in_scc])
|
if (realizable_[in_scc])
|
||||||
{
|
{
|
||||||
if (final_.find(sin) != final_.end())
|
if (final_.find(sin) != final_.end())
|
||||||
out_->trans_data(t).acc = acc_;
|
out_->edge_data(t).acc = acc_;
|
||||||
}
|
}
|
||||||
else if (sm_.scc_of_state(sout) == in_scc)
|
else if (sm_.scc_of_state(sout) == in_scc)
|
||||||
{
|
{
|
||||||
|
|
@ -278,12 +278,11 @@ namespace spot
|
||||||
// implementation create more transitions than needed:
|
// implementation create more transitions than needed:
|
||||||
// we do not need more than one transition per
|
// we do not need more than one transition per
|
||||||
// accepting cycle.
|
// accepting cycle.
|
||||||
out_->new_transition(in, out + shift, cond);
|
out_->new_edge(in, out + shift, cond);
|
||||||
|
|
||||||
// Acceptance transitions are those in the Li
|
// Acceptance transitions are those in the Li
|
||||||
// set. (Löding's Fi set.)
|
// set. (Löding's Fi set.)
|
||||||
out_->new_acc_transition(in + shift, out + shift, cond,
|
out_->new_acc_edge(in + shift, out + shift, cond, l.get(i));
|
||||||
l.get(i));
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -275,7 +275,7 @@ states:
|
||||||
{
|
{
|
||||||
for (map_t::const_iterator i = result.dest_map.begin();
|
for (map_t::const_iterator i = result.dest_map.begin();
|
||||||
i != result.dest_map.end(); ++i)
|
i != result.dest_map.end(); ++i)
|
||||||
result.d->aut->new_transition(result.cur_state, i->first, i->second);
|
result.d->aut->new_edge(result.cur_state, i->first, i->second);
|
||||||
}
|
}
|
||||||
%%
|
%%
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -70,7 +70,7 @@ namespace spot
|
||||||
int out = d_->aut->state_number(sout);
|
int out = d_->aut->state_number(sout);
|
||||||
|
|
||||||
bdd cond = si->current_condition();
|
bdd cond = si->current_condition();
|
||||||
out_->new_transition(in, out, cond);
|
out_->new_edge(in, out, cond);
|
||||||
|
|
||||||
// Create one clone of the automaton per accepting pair,
|
// Create one clone of the automaton per accepting pair,
|
||||||
// removing states from the Ui part of the (Li, Ui) pairs.
|
// removing states from the Ui part of the (Li, Ui) pairs.
|
||||||
|
|
@ -94,12 +94,11 @@ namespace spot
|
||||||
// implementation create more transitions than needed:
|
// implementation create more transitions than needed:
|
||||||
// we do not need more than one transition per
|
// we do not need more than one transition per
|
||||||
// accepting cycle.
|
// accepting cycle.
|
||||||
out_->new_transition(in, out + shift, cond);
|
out_->new_edge(in, out + shift, cond);
|
||||||
|
|
||||||
// A transition is accepting if it is in the Li
|
// A transition is accepting if it is in the Li
|
||||||
// set. (Löding's Fi set.)
|
// set. (Löding's Fi set.)
|
||||||
out_->new_acc_transition(in + shift, out + shift, cond,
|
out_->new_acc_edge(in + shift, out + shift, cond, l.get(i));
|
||||||
l.get(i));
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -155,7 +155,7 @@ namespace spot
|
||||||
dest = dres.first->second = res->new_state();
|
dest = dres.first->second = res->new_state();
|
||||||
todo.push_back(d);
|
todo.push_back(d);
|
||||||
}
|
}
|
||||||
res->new_transition(src, dest, t.cond, acc);
|
res->new_edge(src, dest, t.cond, acc);
|
||||||
|
|
||||||
// Jump to level ∅
|
// Jump to level ∅
|
||||||
if (s.pend == 0)
|
if (s.pend == 0)
|
||||||
|
|
@ -175,7 +175,7 @@ namespace spot
|
||||||
dest = dres.first->second = res->new_state();
|
dest = dres.first->second = res->new_state();
|
||||||
todo.push_back(d);
|
todo.push_back(d);
|
||||||
}
|
}
|
||||||
res->new_transition(src, dest, t.cond);
|
res->new_edge(src, dest, t.cond);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -30,7 +30,7 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
template <typename State_Data, typename Trans_Data, bool Alternating = false>
|
template <typename State_Data, typename Edge_Data, bool Alternating = false>
|
||||||
class SPOT_API digraph;
|
class SPOT_API digraph;
|
||||||
|
|
||||||
namespace internal
|
namespace internal
|
||||||
|
|
@ -144,12 +144,12 @@ namespace spot
|
||||||
// We have two implementations, one with attached State_Data, and
|
// We have two implementations, one with attached State_Data, and
|
||||||
// one without.
|
// one without.
|
||||||
|
|
||||||
template <typename Transition, typename State_Data>
|
template <typename Edge, typename State_Data>
|
||||||
struct SPOT_API distate_storage final: public State_Data
|
struct SPOT_API distate_storage final: public State_Data
|
||||||
{
|
{
|
||||||
Transition succ = 0; // First outgoing transition (used when iterating)
|
Edge succ = 0; // First outgoing edge (used when iterating)
|
||||||
Transition succ_tail = 0; // Last outgoing transition (used for
|
Edge succ_tail = 0; // Last outgoing edge (used for
|
||||||
// appending new transitions)
|
// appending new edges)
|
||||||
|
|
||||||
template <typename... Args,
|
template <typename... Args,
|
||||||
typename = typename std::enable_if<
|
typename = typename std::enable_if<
|
||||||
|
|
@ -161,36 +161,36 @@ namespace spot
|
||||||
};
|
};
|
||||||
|
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
// Transition storage
|
// Edge storage
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
|
|
||||||
// Again two implementation: one with label, and one without.
|
// Again two implementation: one with label, and one without.
|
||||||
|
|
||||||
template <typename StateIn,
|
template <typename StateIn,
|
||||||
typename StateOut, typename Transition, typename Trans_Data>
|
typename StateOut, typename Edge, typename Edge_Data>
|
||||||
struct SPOT_API trans_storage final: public Trans_Data
|
struct SPOT_API edge_storage final: public Edge_Data
|
||||||
{
|
{
|
||||||
typedef Transition transition;
|
typedef Edge edge;
|
||||||
|
|
||||||
StateOut dst; // destination
|
StateOut dst; // destination
|
||||||
Transition next_succ; // next outgoing transition with same
|
Edge next_succ; // next outgoing edge with same
|
||||||
// source, or 0
|
// source, or 0
|
||||||
StateIn src; // source
|
StateIn src; // source
|
||||||
|
|
||||||
explicit trans_storage()
|
explicit edge_storage()
|
||||||
: Trans_Data{}
|
: Edge_Data{}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
trans_storage(StateOut dst, Transition next_succ,
|
edge_storage(StateOut dst, Edge next_succ,
|
||||||
StateIn src, Args&&... args)
|
StateIn src, Args&&... args)
|
||||||
: Trans_Data{std::forward<Args>(args)...},
|
: Edge_Data{std::forward<Args>(args)...},
|
||||||
dst(dst), next_succ(next_succ), src(src)
|
dst(dst), next_succ(next_succ), src(src)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator<(const trans_storage& other) const
|
bool operator<(const edge_storage& other) const
|
||||||
{
|
{
|
||||||
if (src < other.src)
|
if (src < other.src)
|
||||||
return true;
|
return true;
|
||||||
|
|
@ -204,7 +204,7 @@ namespace spot
|
||||||
return this->data() < other.data();
|
return this->data() < other.data();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator==(const trans_storage& other) const
|
bool operator==(const edge_storage& other) const
|
||||||
{
|
{
|
||||||
return src == other.src &&
|
return src == other.src &&
|
||||||
dst == other.dst &&
|
dst == other.dst &&
|
||||||
|
|
@ -213,46 +213,46 @@ namespace spot
|
||||||
};
|
};
|
||||||
|
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
// Transition iterator
|
// Edge iterator
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
|
|
||||||
// This holds a graph and a transition number that is the start of
|
// This holds a graph and a edge number that is the start of
|
||||||
// a list, and it iterates over all the trans_storage_t elements
|
// a list, and it iterates over all the edge_storage_t elements
|
||||||
// of that list.
|
// of that list.
|
||||||
|
|
||||||
template <typename Graph>
|
template <typename Graph>
|
||||||
class SPOT_API trans_iterator:
|
class SPOT_API edge_iterator:
|
||||||
std::iterator<std::forward_iterator_tag,
|
std::iterator<std::forward_iterator_tag,
|
||||||
typename
|
typename
|
||||||
std::conditional<std::is_const<Graph>::value,
|
std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_storage_t,
|
const typename Graph::edge_storage_t,
|
||||||
typename Graph::trans_storage_t>::type>
|
typename Graph::edge_storage_t>::type>
|
||||||
{
|
{
|
||||||
typedef
|
typedef
|
||||||
std::iterator<std::forward_iterator_tag,
|
std::iterator<std::forward_iterator_tag,
|
||||||
typename
|
typename
|
||||||
std::conditional<std::is_const<Graph>::value,
|
std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_storage_t,
|
const typename Graph::edge_storage_t,
|
||||||
typename Graph::trans_storage_t>::type>
|
typename Graph::edge_storage_t>::type>
|
||||||
super;
|
super;
|
||||||
public:
|
public:
|
||||||
typedef typename Graph::transition transition;
|
typedef typename Graph::edge edge;
|
||||||
|
|
||||||
trans_iterator()
|
edge_iterator()
|
||||||
: g_(nullptr), t_(0)
|
: g_(nullptr), t_(0)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_iterator(Graph* g, transition t): g_(g), t_(t)
|
edge_iterator(Graph* g, edge t): g_(g), t_(t)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator==(trans_iterator o) const
|
bool operator==(edge_iterator o) const
|
||||||
{
|
{
|
||||||
return t_ == o.t_;
|
return t_ == o.t_;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator!=(trans_iterator o) const
|
bool operator!=(edge_iterator o) const
|
||||||
{
|
{
|
||||||
return t_ != o.t_;
|
return t_ != o.t_;
|
||||||
}
|
}
|
||||||
|
|
@ -260,24 +260,24 @@ namespace spot
|
||||||
typename super::reference
|
typename super::reference
|
||||||
operator*()
|
operator*()
|
||||||
{
|
{
|
||||||
return g_->trans_storage(t_);
|
return g_->edge_storage(t_);
|
||||||
}
|
}
|
||||||
|
|
||||||
typename super::pointer
|
typename super::pointer
|
||||||
operator->()
|
operator->()
|
||||||
{
|
{
|
||||||
return &g_->trans_storage(t_);
|
return &g_->edge_storage(t_);
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_iterator operator++()
|
edge_iterator operator++()
|
||||||
{
|
{
|
||||||
t_ = operator*().next_succ;
|
t_ = operator*().next_succ;
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_iterator operator++(int)
|
edge_iterator operator++(int)
|
||||||
{
|
{
|
||||||
trans_iterator ti = *this;
|
edge_iterator ti = *this;
|
||||||
t_ = operator*().next_succ;
|
t_ = operator*().next_succ;
|
||||||
return ti;
|
return ti;
|
||||||
}
|
}
|
||||||
|
|
@ -287,52 +287,52 @@ namespace spot
|
||||||
return t_;
|
return t_;
|
||||||
}
|
}
|
||||||
|
|
||||||
transition trans() const
|
edge trans() const
|
||||||
{
|
{
|
||||||
return t_;
|
return t_;
|
||||||
}
|
}
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
Graph* g_;
|
Graph* g_;
|
||||||
transition t_;
|
edge t_;
|
||||||
};
|
};
|
||||||
|
|
||||||
template <typename Graph>
|
template <typename Graph>
|
||||||
class SPOT_API killer_trans_iterator: public trans_iterator<Graph>
|
class SPOT_API killer_edge_iterator: public edge_iterator<Graph>
|
||||||
{
|
{
|
||||||
typedef trans_iterator<Graph> super;
|
typedef edge_iterator<Graph> super;
|
||||||
public:
|
public:
|
||||||
typedef typename Graph::state_storage_t state_storage_t;
|
typedef typename Graph::state_storage_t state_storage_t;
|
||||||
typedef typename Graph::transition transition;
|
typedef typename Graph::edge edge;
|
||||||
|
|
||||||
killer_trans_iterator(Graph* g, transition t, state_storage_t& src):
|
killer_edge_iterator(Graph* g, edge t, state_storage_t& src):
|
||||||
super(g, t), src_(src), prev_(0)
|
super(g, t), src_(src), prev_(0)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
killer_trans_iterator operator++()
|
killer_edge_iterator operator++()
|
||||||
{
|
{
|
||||||
prev_ = this->t_;
|
prev_ = this->t_;
|
||||||
this->t_ = this->operator*().next_succ;
|
this->t_ = this->operator*().next_succ;
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
killer_trans_iterator operator++(int)
|
killer_edge_iterator operator++(int)
|
||||||
{
|
{
|
||||||
killer_trans_iterator ti = *this;
|
killer_edge_iterator ti = *this;
|
||||||
++*this;
|
++*this;
|
||||||
return ti;
|
return ti;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Erase the current transition and advance the iterator.
|
// Erase the current edge and advance the iterator.
|
||||||
void erase()
|
void erase()
|
||||||
{
|
{
|
||||||
transition next = this->operator*().next_succ;
|
edge next = this->operator*().next_succ;
|
||||||
|
|
||||||
// Update source state and previous transitions
|
// Update source state and previous edges
|
||||||
if (prev_)
|
if (prev_)
|
||||||
{
|
{
|
||||||
this->g_->trans_storage(prev_).next_succ = next;
|
this->g_->edge_storage(prev_).next_succ = next;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
@ -345,18 +345,18 @@ namespace spot
|
||||||
assert(next == 0);
|
assert(next == 0);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Erased transitions have themselves as next_succ.
|
// Erased edges have themselves as next_succ.
|
||||||
this->operator*().next_succ = this->t_;
|
this->operator*().next_succ = this->t_;
|
||||||
|
|
||||||
// Advance iterator to next transition.
|
// Advance iterator to next edge.
|
||||||
this->t_ = next;
|
this->t_ = next;
|
||||||
|
|
||||||
++this->g_->killed_trans_;
|
++this->g_->killed_edge_;
|
||||||
}
|
}
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
state_storage_t& src_;
|
state_storage_t& src_;
|
||||||
transition prev_;
|
edge prev_;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -364,36 +364,36 @@ namespace spot
|
||||||
// State OUT
|
// State OUT
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
|
|
||||||
// Fake container listing the outgoing transitions of a state.
|
// Fake container listing the outgoing edges of a state.
|
||||||
|
|
||||||
template <typename Graph>
|
template <typename Graph>
|
||||||
class SPOT_API state_out
|
class SPOT_API state_out
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
typedef typename Graph::transition transition;
|
typedef typename Graph::edge edge;
|
||||||
state_out(Graph* g, transition t):
|
state_out(Graph* g, edge t):
|
||||||
g_(g), t_(t)
|
g_(g), t_(t)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_iterator<Graph> begin()
|
edge_iterator<Graph> begin()
|
||||||
{
|
{
|
||||||
return {g_, t_};
|
return {g_, t_};
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_iterator<Graph> end()
|
edge_iterator<Graph> end()
|
||||||
{
|
{
|
||||||
return {};
|
return {};
|
||||||
}
|
}
|
||||||
|
|
||||||
void recycle(transition t)
|
void recycle(edge t)
|
||||||
{
|
{
|
||||||
t_ = t;
|
t_ = t;
|
||||||
}
|
}
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
Graph* g_;
|
Graph* g_;
|
||||||
transition t_;
|
edge t_;
|
||||||
};
|
};
|
||||||
|
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
|
|
@ -401,24 +401,24 @@ namespace spot
|
||||||
//////////////////////////////////////////////////
|
//////////////////////////////////////////////////
|
||||||
|
|
||||||
template <typename Graph>
|
template <typename Graph>
|
||||||
class SPOT_API all_trans_iterator:
|
class SPOT_API all_edge_iterator:
|
||||||
std::iterator<std::forward_iterator_tag,
|
std::iterator<std::forward_iterator_tag,
|
||||||
typename
|
typename
|
||||||
std::conditional<std::is_const<Graph>::value,
|
std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_storage_t,
|
const typename Graph::edge_storage_t,
|
||||||
typename Graph::trans_storage_t>::type>
|
typename Graph::edge_storage_t>::type>
|
||||||
{
|
{
|
||||||
typedef
|
typedef
|
||||||
std::iterator<std::forward_iterator_tag,
|
std::iterator<std::forward_iterator_tag,
|
||||||
typename
|
typename
|
||||||
std::conditional<std::is_const<Graph>::value,
|
std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_storage_t,
|
const typename Graph::edge_storage_t,
|
||||||
typename Graph::trans_storage_t>::type>
|
typename Graph::edge_storage_t>::type>
|
||||||
super;
|
super;
|
||||||
|
|
||||||
typedef typename std::conditional<std::is_const<Graph>::value,
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_vector,
|
const typename Graph::edge_vector_t,
|
||||||
typename Graph::trans_vector>::type
|
typename Graph::edge_vector_t>::type
|
||||||
tv_t;
|
tv_t;
|
||||||
|
|
||||||
unsigned t_;
|
unsigned t_;
|
||||||
|
|
@ -433,36 +433,36 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
public:
|
public:
|
||||||
all_trans_iterator(unsigned pos, tv_t& tv)
|
all_edge_iterator(unsigned pos, tv_t& tv)
|
||||||
: t_(pos), tv_(tv)
|
: t_(pos), tv_(tv)
|
||||||
{
|
{
|
||||||
skip_();
|
skip_();
|
||||||
}
|
}
|
||||||
|
|
||||||
all_trans_iterator(tv_t& tv)
|
all_edge_iterator(tv_t& tv)
|
||||||
: t_(tv.size()), tv_(tv)
|
: t_(tv.size()), tv_(tv)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
all_trans_iterator& operator++()
|
all_edge_iterator& operator++()
|
||||||
{
|
{
|
||||||
skip_();
|
skip_();
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
all_trans_iterator operator++(int)
|
all_edge_iterator operator++(int)
|
||||||
{
|
{
|
||||||
all_trans_iterator old = *this;
|
all_edge_iterator old = *this;
|
||||||
++*this;
|
++*this;
|
||||||
return old;
|
return old;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator==(all_trans_iterator o) const
|
bool operator==(all_edge_iterator o) const
|
||||||
{
|
{
|
||||||
return t_ == o.t_;
|
return t_ == o.t_;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator!=(all_trans_iterator o) const
|
bool operator!=(all_edge_iterator o) const
|
||||||
{
|
{
|
||||||
return t_ != o.t_;
|
return t_ != o.t_;
|
||||||
}
|
}
|
||||||
|
|
@ -485,10 +485,10 @@ namespace spot
|
||||||
class SPOT_API all_trans
|
class SPOT_API all_trans
|
||||||
{
|
{
|
||||||
typedef typename std::conditional<std::is_const<Graph>::value,
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||||
const typename Graph::trans_vector,
|
const typename Graph::edge_vector_t,
|
||||||
typename Graph::trans_vector>::type
|
typename Graph::edge_vector_t>::type
|
||||||
tv_t;
|
tv_t;
|
||||||
typedef all_trans_iterator<Graph> iter_t;
|
typedef all_edge_iterator<Graph> iter_t;
|
||||||
tv_t& tv_;
|
tv_t& tv_;
|
||||||
public:
|
public:
|
||||||
|
|
||||||
|
|
@ -513,69 +513,69 @@ namespace spot
|
||||||
|
|
||||||
// The actual graph implementation
|
// The actual graph implementation
|
||||||
|
|
||||||
template <typename State_Data, typename Trans_Data, bool Alternating>
|
template <typename State_Data, typename Edge_Data, bool Alternating>
|
||||||
class digraph
|
class digraph
|
||||||
{
|
{
|
||||||
friend class internal::trans_iterator<digraph>;
|
friend class internal::edge_iterator<digraph>;
|
||||||
friend class internal::trans_iterator<const digraph>;
|
friend class internal::edge_iterator<const digraph>;
|
||||||
friend class internal::killer_trans_iterator<digraph>;
|
friend class internal::killer_edge_iterator<digraph>;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
typedef internal::trans_iterator<digraph> iterator;
|
typedef internal::edge_iterator<digraph> iterator;
|
||||||
typedef internal::trans_iterator<const digraph> const_iterator;
|
typedef internal::edge_iterator<const digraph> const_iterator;
|
||||||
|
|
||||||
static constexpr bool alternating()
|
static constexpr bool alternating()
|
||||||
{
|
{
|
||||||
return Alternating;
|
return Alternating;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Extra data to store on each state or transition.
|
// Extra data to store on each state or edge.
|
||||||
typedef State_Data state_data_t;
|
typedef State_Data state_data_t;
|
||||||
typedef Trans_Data trans_data_t;
|
typedef Edge_Data edge_data_t;
|
||||||
|
|
||||||
// State and transitions are identified by their indices in some
|
// State and edges are identified by their indices in some
|
||||||
// vector.
|
// vector.
|
||||||
typedef unsigned state;
|
typedef unsigned state;
|
||||||
typedef unsigned transition;
|
typedef unsigned edge;
|
||||||
|
|
||||||
// The type of an output state (when seen from a transition)
|
// The type of an output state (when seen from a edge)
|
||||||
// depends on the kind of graph we build
|
// depends on the kind of graph we build
|
||||||
typedef typename std::conditional<Alternating,
|
typedef typename std::conditional<Alternating,
|
||||||
std::vector<state>,
|
std::vector<state>,
|
||||||
state>::type out_state;
|
state>::type out_state;
|
||||||
|
|
||||||
typedef internal::distate_storage<transition,
|
typedef internal::distate_storage<edge,
|
||||||
internal::boxed_label<State_Data>>
|
internal::boxed_label<State_Data>>
|
||||||
state_storage_t;
|
state_storage_t;
|
||||||
typedef internal::trans_storage<state, out_state, transition,
|
typedef internal::edge_storage<state, out_state, edge,
|
||||||
internal::boxed_label<Trans_Data>>
|
internal::boxed_label<Edge_Data>>
|
||||||
trans_storage_t;
|
edge_storage_t;
|
||||||
typedef std::vector<state_storage_t> state_vector;
|
typedef std::vector<state_storage_t> state_vector;
|
||||||
typedef std::vector<trans_storage_t> trans_vector;
|
typedef std::vector<edge_storage_t> edge_vector_t;
|
||||||
protected:
|
protected:
|
||||||
state_vector states_;
|
state_vector states_;
|
||||||
trans_vector transitions_;
|
edge_vector_t edges_;
|
||||||
// Number of erased transitions.
|
// Number of erased edges.
|
||||||
unsigned killed_trans_;
|
unsigned killed_edge_;
|
||||||
public:
|
public:
|
||||||
/// \brief construct an empty graph
|
/// \brief construct an empty graph
|
||||||
///
|
///
|
||||||
/// Construct an empty graph, and reserve space for \a max_states
|
/// Construct an empty graph, and reserve space for \a max_states
|
||||||
/// states and \a max_trans transitions. These are not hard
|
/// states and \a max_trans edges. These are not hard
|
||||||
/// limits, but just hints to pre-allocate a data structure that
|
/// limits, but just hints to pre-allocate a data structure that
|
||||||
/// may hold that much items.
|
/// may hold that much items.
|
||||||
digraph(unsigned max_states = 10, unsigned max_trans = 0)
|
digraph(unsigned max_states = 10, unsigned max_trans = 0)
|
||||||
: killed_trans_(0)
|
: killed_edge_(0)
|
||||||
{
|
{
|
||||||
states_.reserve(max_states);
|
states_.reserve(max_states);
|
||||||
if (max_trans == 0)
|
if (max_trans == 0)
|
||||||
max_trans = max_states * 2;
|
max_trans = max_states * 2;
|
||||||
transitions_.reserve(max_trans + 1);
|
edges_.reserve(max_trans + 1);
|
||||||
// Transition number 0 is not used, because we use this index
|
// Edge number 0 is not used, because we use this index
|
||||||
// to mark the absence of a transition.
|
// to mark the absence of a edge.
|
||||||
transitions_.resize(1);
|
edges_.resize(1);
|
||||||
// This causes transition 0 to be considered as dead.
|
// This causes edge 0 to be considered as dead.
|
||||||
transitions_[0].next_succ = 0;
|
edges_[0].next_succ = 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned num_states() const
|
unsigned num_states() const
|
||||||
|
|
@ -583,17 +583,17 @@ namespace spot
|
||||||
return states_.size();
|
return states_.size();
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned num_transitions() const
|
unsigned num_edges() const
|
||||||
{
|
{
|
||||||
return transitions_.size() - killed_trans_ - 1;
|
return edges_.size() - killed_edge_ - 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool valid_trans(transition t) const
|
bool valid_trans(edge t) const
|
||||||
{
|
{
|
||||||
// Erased transitions have their next_succ pointing to
|
// Erased edges have their next_succ pointing to
|
||||||
// themselves.
|
// themselves.
|
||||||
return (t < transitions_.size() &&
|
return (t < edges_.size() &&
|
||||||
transitions_[t].next_succ != t);
|
edges_[t].next_succ != t);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
|
|
@ -645,49 +645,49 @@ namespace spot
|
||||||
return states_[s].data();
|
return states_[s].data();
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_storage_t&
|
edge_storage_t&
|
||||||
trans_storage(transition s)
|
edge_storage(edge s)
|
||||||
{
|
{
|
||||||
assert(s < transitions_.size());
|
assert(s < edges_.size());
|
||||||
return transitions_[s];
|
return edges_[s];
|
||||||
}
|
}
|
||||||
|
|
||||||
const trans_storage_t&
|
const edge_storage_t&
|
||||||
trans_storage(transition s) const
|
edge_storage(edge s) const
|
||||||
{
|
{
|
||||||
assert(s < transitions_.size());
|
assert(s < edges_.size());
|
||||||
return transitions_[s];
|
return edges_[s];
|
||||||
}
|
}
|
||||||
|
|
||||||
typename trans_storage_t::data_t&
|
typename edge_storage_t::data_t&
|
||||||
trans_data(transition s)
|
edge_data(edge s)
|
||||||
{
|
{
|
||||||
assert(s < transitions_.size());
|
assert(s < edges_.size());
|
||||||
return transitions_[s].data();
|
return edges_[s].data();
|
||||||
}
|
}
|
||||||
|
|
||||||
const typename trans_storage_t::data_t&
|
const typename edge_storage_t::data_t&
|
||||||
trans_data(transition s) const
|
edge_data(edge s) const
|
||||||
{
|
{
|
||||||
assert(s < transitions_.size());
|
assert(s < edges_.size());
|
||||||
return transitions_[s].data();
|
return edges_[s].data();
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
transition
|
edge
|
||||||
new_transition(state src, out_state dst, Args&&... args)
|
new_edge(state src, out_state dst, Args&&... args)
|
||||||
{
|
{
|
||||||
assert(src < states_.size());
|
assert(src < states_.size());
|
||||||
|
|
||||||
transition t = transitions_.size();
|
edge t = edges_.size();
|
||||||
transitions_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
|
edges_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
|
||||||
|
|
||||||
transition st = states_[src].succ_tail;
|
edge st = states_[src].succ_tail;
|
||||||
assert(st < t || !st);
|
assert(st < t || !st);
|
||||||
if (!st)
|
if (!st)
|
||||||
states_[src].succ = t;
|
states_[src].succ = t;
|
||||||
else
|
else
|
||||||
transitions_[st].next_succ = t;
|
edges_[st].next_succ = t;
|
||||||
states_[src].succ_tail = t;
|
states_[src].succ_tail = t;
|
||||||
return t;
|
return t;
|
||||||
}
|
}
|
||||||
|
|
@ -698,10 +698,10 @@ namespace spot
|
||||||
return &ss - &states_.front();
|
return &ss - &states_.front();
|
||||||
}
|
}
|
||||||
|
|
||||||
transition index_of_transition(const trans_storage_t& tt) const
|
edge index_of_edge(const edge_storage_t& tt) const
|
||||||
{
|
{
|
||||||
assert(!transitions_.empty());
|
assert(!edges_.empty());
|
||||||
return &tt - &transitions_.front();
|
return &tt - &edges_.front();
|
||||||
}
|
}
|
||||||
|
|
||||||
internal::state_out<digraph>
|
internal::state_out<digraph>
|
||||||
|
|
@ -728,13 +728,13 @@ namespace spot
|
||||||
return out(index_of_state(src));
|
return out(index_of_state(src));
|
||||||
}
|
}
|
||||||
|
|
||||||
internal::killer_trans_iterator<digraph>
|
internal::killer_edge_iterator<digraph>
|
||||||
out_iteraser(state_storage_t& src)
|
out_iteraser(state_storage_t& src)
|
||||||
{
|
{
|
||||||
return {this, src.succ, src};
|
return {this, src.succ, src};
|
||||||
}
|
}
|
||||||
|
|
||||||
internal::killer_trans_iterator<digraph>
|
internal::killer_edge_iterator<digraph>
|
||||||
out_iteraser(state src)
|
out_iteraser(state src)
|
||||||
{
|
{
|
||||||
return out_iteraser(state_storage(src));
|
return out_iteraser(state_storage(src));
|
||||||
|
|
@ -750,52 +750,52 @@ namespace spot
|
||||||
return states_;
|
return states_;
|
||||||
}
|
}
|
||||||
|
|
||||||
internal::all_trans<const digraph> transitions() const
|
internal::all_trans<const digraph> edges() const
|
||||||
{
|
{
|
||||||
return transitions_;
|
return edges_;
|
||||||
}
|
}
|
||||||
|
|
||||||
internal::all_trans<digraph> transitions()
|
internal::all_trans<digraph> edges()
|
||||||
{
|
{
|
||||||
return transitions_;
|
return edges_;
|
||||||
}
|
}
|
||||||
|
|
||||||
// When using this method, beware that the first entry (transition
|
// When using this method, beware that the first entry (edge
|
||||||
// #0) is not a real transition, and that any transition with
|
// #0) is not a real edge, and that any edge with
|
||||||
// next_succ pointing to itself is an erased transition.
|
// next_succ pointing to itself is an erased edge.
|
||||||
//
|
//
|
||||||
// You should probably use transitions() instead.
|
// You should probably use edges() instead.
|
||||||
const trans_vector& transition_vector() const
|
const edge_vector_t& edge_vector() const
|
||||||
{
|
{
|
||||||
return transitions_;
|
return edges_;
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_vector& transition_vector()
|
edge_vector_t& edge_vector()
|
||||||
{
|
{
|
||||||
return transitions_;
|
return edges_;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_dead_transition(unsigned t) const
|
bool is_dead_edge(unsigned t) const
|
||||||
{
|
{
|
||||||
return transitions_[t].next_succ == t;
|
return edges_[t].next_succ == t;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_dead_transition(const trans_storage_t& t) const
|
bool is_dead_edge(const edge_storage_t& t) const
|
||||||
{
|
{
|
||||||
return t.next_succ == index_of_transition(t);
|
return t.next_succ == index_of_edge(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// To help debugging
|
// To help debugging
|
||||||
void dump_storage(std::ostream& o) const
|
void dump_storage(std::ostream& o) const
|
||||||
{
|
{
|
||||||
unsigned tend = transitions_.size();
|
unsigned tend = edges_.size();
|
||||||
for (unsigned t = 1; t < tend; ++t)
|
for (unsigned t = 1; t < tend; ++t)
|
||||||
{
|
{
|
||||||
o << 't' << t << ": (s"
|
o << 't' << t << ": (s"
|
||||||
<< transitions_[t].src << ", s"
|
<< edges_[t].src << ", s"
|
||||||
<< transitions_[t].dst << ") t"
|
<< edges_[t].dst << ") t"
|
||||||
<< transitions_[t].next_succ << '\n';
|
<< edges_[t].next_succ << '\n';
|
||||||
}
|
}
|
||||||
unsigned send = states_.size();
|
unsigned send = states_.size();
|
||||||
for (unsigned s = 0; s < send; ++s)
|
for (unsigned s = 0; s < send; ++s)
|
||||||
|
|
@ -806,49 +806,49 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Remove all dead transitions. The transitions_ vector is left
|
// Remove all dead edges. The edges_ vector is left
|
||||||
// in a state that is incorrect and should eventually be fixed by
|
// in a state that is incorrect and should eventually be fixed by
|
||||||
// a call to chain_transitions_() before any iteration on the
|
// a call to chain_edges_() before any iteration on the
|
||||||
// successor of a state is performed.
|
// successor of a state is performed.
|
||||||
void remove_dead_transitions_()
|
void remove_dead_edges_()
|
||||||
{
|
{
|
||||||
if (killed_trans_ == 0)
|
if (killed_edge_ == 0)
|
||||||
return;
|
return;
|
||||||
auto i = std::remove_if(transitions_.begin() + 1, transitions_.end(),
|
auto i = std::remove_if(edges_.begin() + 1, edges_.end(),
|
||||||
[this](const trans_storage_t& t) {
|
[this](const edge_storage_t& t) {
|
||||||
return this->is_dead_transition(t);
|
return this->is_dead_edge(t);
|
||||||
});
|
});
|
||||||
transitions_.erase(i, transitions_.end());
|
edges_.erase(i, edges_.end());
|
||||||
killed_trans_ = 0;
|
killed_edge_ = 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
// This will invalidate all iterators, and also destroy transition
|
// This will invalidate all iterators, and also destroy edge
|
||||||
// chains. Call chain_transitions_() immediately afterwards
|
// chains. Call chain_edges_() immediately afterwards
|
||||||
// unless you know what you are doing.
|
// unless you know what you are doing.
|
||||||
template<class Predicate = std::less<trans_storage_t>>
|
template<class Predicate = std::less<edge_storage_t>>
|
||||||
void sort_transitions_(Predicate p = Predicate())
|
void sort_edges_(Predicate p = Predicate())
|
||||||
{
|
{
|
||||||
//std::cerr << "\nbefore\n";
|
//std::cerr << "\nbefore\n";
|
||||||
//dump_storage(std::cerr);
|
//dump_storage(std::cerr);
|
||||||
std::stable_sort(transitions_.begin() + 1, transitions_.end(), p);
|
std::stable_sort(edges_.begin() + 1, edges_.end(), p);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Should be called only when it is known that all transitions
|
// Should be called only when it is known that all edges
|
||||||
// with the same destination are consecutive in the vector.
|
// with the same destination are consecutive in the vector.
|
||||||
void chain_transitions_()
|
void chain_edges_()
|
||||||
{
|
{
|
||||||
state last_src = -1U;
|
state last_src = -1U;
|
||||||
transition tend = transitions_.size();
|
edge tend = edges_.size();
|
||||||
for (transition t = 1; t < tend; ++t)
|
for (edge t = 1; t < tend; ++t)
|
||||||
{
|
{
|
||||||
state src = transitions_[t].src;
|
state src = edges_[t].src;
|
||||||
if (src != last_src)
|
if (src != last_src)
|
||||||
{
|
{
|
||||||
states_[src].succ = t;
|
states_[src].succ = t;
|
||||||
if (last_src != -1U)
|
if (last_src != -1U)
|
||||||
{
|
{
|
||||||
states_[last_src].succ_tail = t - 1;
|
states_[last_src].succ_tail = t - 1;
|
||||||
transitions_[t - 1].next_succ = 0;
|
edges_[t - 1].next_succ = 0;
|
||||||
}
|
}
|
||||||
while (++last_src != src)
|
while (++last_src != src)
|
||||||
{
|
{
|
||||||
|
|
@ -858,13 +858,13 @@ namespace spot
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
transitions_[t - 1].next_succ = t;
|
edges_[t - 1].next_succ = t;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (last_src != -1U)
|
if (last_src != -1U)
|
||||||
{
|
{
|
||||||
states_[last_src].succ_tail = tend - 1;
|
states_[last_src].succ_tail = tend - 1;
|
||||||
transitions_[tend - 1].next_succ = 0;
|
edges_[tend - 1].next_succ = 0;
|
||||||
}
|
}
|
||||||
unsigned send = states_.size();
|
unsigned send = states_.size();
|
||||||
while (++last_src != send)
|
while (++last_src != send)
|
||||||
|
|
@ -876,18 +876,18 @@ namespace spot
|
||||||
//dump_storage(std::cerr);
|
//dump_storage(std::cerr);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Rename all the states in the transition vector. The
|
// Rename all the states in the edge vector. The
|
||||||
// transitions_ vector is left in a state that is incorrect and
|
// edges_ vector is left in a state that is incorrect and
|
||||||
// should eventually be fixed by a call to chain_transitions_()
|
// should eventually be fixed by a call to chain_edges_()
|
||||||
// before any iteration on the successor of a state is performed.
|
// before any iteration on the successor of a state is performed.
|
||||||
void rename_states_(const std::vector<unsigned>& newst)
|
void rename_states_(const std::vector<unsigned>& newst)
|
||||||
{
|
{
|
||||||
assert(newst.size() == states_.size());
|
assert(newst.size() == states_.size());
|
||||||
unsigned tend = transitions_.size();
|
unsigned tend = edges_.size();
|
||||||
for (unsigned t = 1; t < tend; t++)
|
for (unsigned t = 1; t < tend; t++)
|
||||||
{
|
{
|
||||||
transitions_[t].dst = newst[transitions_[t].dst];
|
edges_[t].dst = newst[edges_[t].dst];
|
||||||
transitions_[t].src = newst[transitions_[t].src];
|
edges_[t].src = newst[edges_[t].src];
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -908,40 +908,40 @@ namespace spot
|
||||||
continue;
|
continue;
|
||||||
if (dst == -1U)
|
if (dst == -1U)
|
||||||
{
|
{
|
||||||
// This is an erased state. Mark all its transitions as
|
// This is an erased state. Mark all its edges as
|
||||||
// dead (i.e., t.next_succ should point to t for each of
|
// dead (i.e., t.next_succ should point to t for each of
|
||||||
// them).
|
// them).
|
||||||
auto t = states_[s].succ;
|
auto t = states_[s].succ;
|
||||||
while (t)
|
while (t)
|
||||||
std::swap(t, transitions_[t].next_succ);
|
std::swap(t, edges_[t].next_succ);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
states_[dst] = std::move(states_[s]);
|
states_[dst] = std::move(states_[s]);
|
||||||
}
|
}
|
||||||
states_.resize(used_states);
|
states_.resize(used_states);
|
||||||
|
|
||||||
// Shift all transitions in transitions_. The algorithm is
|
// Shift all edges in edges_. The algorithm is
|
||||||
// similar to remove_if, but it also keeps the correspondence
|
// similar to remove_if, but it also keeps the correspondence
|
||||||
// between the old and new index as newidx[old] = new.
|
// between the old and new index as newidx[old] = new.
|
||||||
unsigned tend = transitions_.size();
|
unsigned tend = edges_.size();
|
||||||
std::vector<transition> newidx(tend);
|
std::vector<edge> newidx(tend);
|
||||||
unsigned dest = 1;
|
unsigned dest = 1;
|
||||||
for (transition t = 1; t < tend; ++t)
|
for (edge t = 1; t < tend; ++t)
|
||||||
{
|
{
|
||||||
if (is_dead_transition(t))
|
if (is_dead_edge(t))
|
||||||
continue;
|
continue;
|
||||||
if (t != dest)
|
if (t != dest)
|
||||||
transitions_[dest] = std::move(transitions_[t]);
|
edges_[dest] = std::move(edges_[t]);
|
||||||
newidx[t] = dest;
|
newidx[t] = dest;
|
||||||
++dest;
|
++dest;
|
||||||
}
|
}
|
||||||
transitions_.resize(dest);
|
edges_.resize(dest);
|
||||||
killed_trans_ = 0;
|
killed_edge_ = 0;
|
||||||
|
|
||||||
// Adjust next_succ and dst pointers in all transitions.
|
// Adjust next_succ and dst pointers in all edges.
|
||||||
for (transition t = 1; t < dest; ++t)
|
for (edge t = 1; t < dest; ++t)
|
||||||
{
|
{
|
||||||
auto& tr = transitions_[t];
|
auto& tr = edges_[t];
|
||||||
tr.next_succ = newidx[tr.next_succ];
|
tr.next_succ = newidx[tr.next_succ];
|
||||||
tr.dst = newst[tr.dst];
|
tr.dst = newst[tr.dst];
|
||||||
tr.src = newst[tr.src];
|
tr.src = newst[tr.src];
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// l'Epita.
|
// de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -36,7 +36,7 @@ namespace spot
|
||||||
public:
|
public:
|
||||||
|
|
||||||
typedef typename Graph::state state;
|
typedef typename Graph::state state;
|
||||||
typedef typename Graph::transition transition;
|
typedef typename Graph::edge edge;
|
||||||
typedef State_Name name;
|
typedef State_Name name;
|
||||||
|
|
||||||
typedef std::unordered_map<name, state,
|
typedef std::unordered_map<name, state,
|
||||||
|
|
@ -90,13 +90,13 @@ namespace spot
|
||||||
auto old = p.first->second;
|
auto old = p.first->second;
|
||||||
p.first->second = s;
|
p.first->second = s;
|
||||||
// Add the successor of OLD to those of S.
|
// Add the successor of OLD to those of S.
|
||||||
auto& trans = g_.transition_vector();
|
auto& trans = g_.edge_vector();
|
||||||
auto& states = g_.states();
|
auto& states = g_.states();
|
||||||
trans[states[s].succ_tail].next_succ = states[old].succ;
|
trans[states[s].succ_tail].next_succ = states[old].succ;
|
||||||
states[s].succ_tail = states[old].succ_tail;
|
states[s].succ_tail = states[old].succ_tail;
|
||||||
states[old].succ = 0;
|
states[old].succ = 0;
|
||||||
states[old].succ_tail = 0;
|
states[old].succ_tail = 0;
|
||||||
// Remove all references to old in transitions:
|
// Remove all references to old in edges:
|
||||||
unsigned tend = trans.size();
|
unsigned tend = trans.size();
|
||||||
for (unsigned t = 1; t < tend; ++t)
|
for (unsigned t = 1; t < tend; ++t)
|
||||||
{
|
{
|
||||||
|
|
@ -130,35 +130,34 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
transition
|
edge
|
||||||
new_transition(name src, name dst, Args&&... args)
|
new_edge(name src, name dst, Args&&... args)
|
||||||
{
|
{
|
||||||
return g_.new_transition(get_state(src), get_state(dst),
|
return g_.new_edge(get_state(src), get_state(dst),
|
||||||
std::forward<Args>(args)...);
|
std::forward<Args>(args)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
transition
|
edge
|
||||||
new_transition(name src,
|
new_edge(name src, const std::vector<State_Name>& dst, Args&&... args)
|
||||||
const std::vector<State_Name>& dst, Args&&... args)
|
|
||||||
{
|
{
|
||||||
std::vector<State_Name> d;
|
std::vector<State_Name> d;
|
||||||
d.reserve(dst.size());
|
d.reserve(dst.size());
|
||||||
for (auto n: dst)
|
for (auto n: dst)
|
||||||
d.push_back(get_state(n));
|
d.push_back(get_state(n));
|
||||||
return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
|
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
||||||
}
|
}
|
||||||
|
|
||||||
template <typename... Args>
|
template <typename... Args>
|
||||||
transition
|
edge
|
||||||
new_transition(name src,
|
new_edge(name src,
|
||||||
const std::initializer_list<State_Name>& dst, Args&&... args)
|
const std::initializer_list<State_Name>& dst, Args&&... args)
|
||||||
{
|
{
|
||||||
std::vector<state> d;
|
std::vector<state> d;
|
||||||
d.reserve(dst.size());
|
d.reserve(dst.size());
|
||||||
for (auto n: dst)
|
for (auto n: dst)
|
||||||
d.push_back(get_state(n));
|
d.push_back(get_state(n));
|
||||||
return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
|
return g_.new_edge(get_state(src), d, std::forward<Args>(args)...);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -168,7 +168,7 @@ namespace spot
|
||||||
bdd support = bddtrue;
|
bdd support = bddtrue;
|
||||||
{
|
{
|
||||||
std::set<int> bdd_seen;
|
std::set<int> bdd_seen;
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
if (bdd_seen.insert(t.cond.id()).second)
|
if (bdd_seen.insert(t.cond.id()).second)
|
||||||
support &= bdd_support(t.cond);
|
support &= bdd_support(t.cond);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1021,16 +1021,14 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt
|
||||||
"(previous edge is labeled)");
|
"(previous edge is labeled)");
|
||||||
else
|
else
|
||||||
cond = res.state_label;
|
cond = res.state_label;
|
||||||
res.h->aut->new_transition(res.cur_state, $1,
|
res.h->aut->new_edge(res.cur_state, $1,
|
||||||
cond,
|
cond, $2 | res.acc_state);
|
||||||
$2 | res.acc_state);
|
|
||||||
}
|
}
|
||||||
labeled-edge: trans-label checked-state-num trans-acc_opt
|
labeled-edge: trans-label checked-state-num trans-acc_opt
|
||||||
{
|
{
|
||||||
if (res.cur_label != bddfalse)
|
if (res.cur_label != bddfalse)
|
||||||
res.h->aut->new_transition(res.cur_state, $2,
|
res.h->aut->new_edge(res.cur_state, $2,
|
||||||
res.cur_label,
|
res.cur_label, $3 | res.acc_state);
|
||||||
$3 | res.acc_state);
|
|
||||||
}
|
}
|
||||||
| trans-label state-conj-2 trans-acc_opt
|
| trans-label state-conj-2 trans-acc_opt
|
||||||
{
|
{
|
||||||
|
|
@ -1067,7 +1065,7 @@ unlabeled-edge: checked-state-num trans-acc_opt
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (cond != bddfalse)
|
if (cond != bddfalse)
|
||||||
res.h->aut->new_transition(res.cur_state, $1,
|
res.h->aut->new_edge(res.cur_state, $1,
|
||||||
cond, $2 | res.acc_state);
|
cond, $2 | res.acc_state);
|
||||||
}
|
}
|
||||||
| state-conj-2 trans-acc_opt
|
| state-conj-2 trans-acc_opt
|
||||||
|
|
@ -1097,7 +1095,7 @@ never: "never" { res.namer = res.h->aut->create_namer<std::string>();
|
||||||
if (res.accept_all_needed && !res.accept_all_seen)
|
if (res.accept_all_needed && !res.accept_all_seen)
|
||||||
{
|
{
|
||||||
unsigned n = res.namer->new_state("accept_all");
|
unsigned n = res.namer->new_state("accept_all");
|
||||||
res.h->aut->new_acc_transition(n, n, bddtrue);
|
res.h->aut->new_acc_edge(n, n, bddtrue);
|
||||||
}
|
}
|
||||||
// If we aliased existing state, we have some unreachable
|
// If we aliased existing state, we have some unreachable
|
||||||
// states to remove.
|
// states to remove.
|
||||||
|
|
@ -1172,7 +1170,7 @@ nc-state:
|
||||||
|
|
||||||
auto acc = !strncmp("accept", $1->c_str(), 6) ?
|
auto acc = !strncmp("accept", $1->c_str(), 6) ?
|
||||||
res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
|
res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
|
||||||
res.namer->new_transition(*$1, *$1, bddtrue, acc);
|
res.namer->new_edge(*$1, *$1, bddtrue, acc);
|
||||||
delete $1;
|
delete $1;
|
||||||
}
|
}
|
||||||
| nc-ident-list { delete $1; }
|
| nc-ident-list { delete $1; }
|
||||||
|
|
@ -1185,7 +1183,7 @@ nc-state:
|
||||||
{
|
{
|
||||||
bdd c = bdd_from_int(p.first);
|
bdd c = bdd_from_int(p.first);
|
||||||
bdd_delref(p.first);
|
bdd_delref(p.first);
|
||||||
res.namer->new_transition(*$1, *p.second, c, acc);
|
res.namer->new_edge(*$1, *p.second, c, acc);
|
||||||
delete p.second;
|
delete p.second;
|
||||||
}
|
}
|
||||||
delete $1;
|
delete $1;
|
||||||
|
|
@ -1445,7 +1443,7 @@ lbtt-transitions:
|
||||||
{
|
{
|
||||||
res.states_map.emplace(dst, dst);
|
res.states_map.emplace(dst, dst);
|
||||||
}
|
}
|
||||||
res.h->aut->new_transition(res.cur_state, dst,
|
res.h->aut->new_edge(res.cur_state, dst,
|
||||||
res.cur_label,
|
res.cur_label,
|
||||||
res.acc_state | $3);
|
res.acc_state | $3);
|
||||||
}
|
}
|
||||||
|
|
@ -1563,7 +1561,7 @@ static void fix_acceptance(result_& r)
|
||||||
auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
|
auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
|
||||||
if (onlyneg)
|
if (onlyneg)
|
||||||
{
|
{
|
||||||
for (auto& t: r.h->aut->transition_vector())
|
for (auto& t: r.h->aut->edge_vector())
|
||||||
t.acc ^= onlyneg;
|
t.acc ^= onlyneg;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1579,7 +1577,7 @@ static void fix_acceptance(result_& r)
|
||||||
auto v = acc.sets(both);
|
auto v = acc.sets(both);
|
||||||
auto vs = v.size();
|
auto vs = v.size();
|
||||||
base = acc.add_sets(vs);
|
base = acc.add_sets(vs);
|
||||||
for (auto& t: r.h->aut->transition_vector())
|
for (auto& t: r.h->aut->edge_vector())
|
||||||
if ((t.acc & both) != both)
|
if ((t.acc & both) != both)
|
||||||
for (unsigned i = 0; i < vs; ++i)
|
for (unsigned i = 0; i < vs; ++i)
|
||||||
if (!t.acc.has(v[i]))
|
if (!t.acc.has(v[i]))
|
||||||
|
|
@ -1631,7 +1629,7 @@ static void fix_initial_state(result_& r)
|
||||||
// unless one of the actual initial state has no incoming edge.
|
// unless one of the actual initial state has no incoming edge.
|
||||||
auto& aut = r.h->aut;
|
auto& aut = r.h->aut;
|
||||||
std::vector<unsigned> has_incoming(aut->num_states(), 0);
|
std::vector<unsigned> has_incoming(aut->num_states(), 0);
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
has_incoming[t.dst] = true;
|
has_incoming[t.dst] = true;
|
||||||
|
|
||||||
bool found = false;
|
bool found = false;
|
||||||
|
|
@ -1649,7 +1647,7 @@ static void fix_initial_state(result_& r)
|
||||||
for (auto p: start)
|
for (auto p: start)
|
||||||
if (p != init)
|
if (p != init)
|
||||||
for (auto& t: aut->out(p))
|
for (auto& t: aut->out(p))
|
||||||
aut->new_transition(init, t.dst, t.cond);
|
aut->new_edge(init, t.dst, t.cond);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -198,7 +198,7 @@ int main(int argc, char* argv[])
|
||||||
auto buchi = spot::degeneralize(a);
|
auto buchi = spot::degeneralize(a);
|
||||||
std::cout << "Buchi: "
|
std::cout << "Buchi: "
|
||||||
<< buchi->num_states()
|
<< buchi->num_states()
|
||||||
<< buchi->num_transitions()
|
<< buchi->num_edges()
|
||||||
<< buchi->acc().num_sets()
|
<< buchi->acc().num_sets()
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// l'Epita.
|
// de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -89,12 +89,12 @@ bool f1()
|
||||||
auto s1 = g.new_state();
|
auto s1 = g.new_state();
|
||||||
auto s2 = g.new_state();
|
auto s2 = g.new_state();
|
||||||
auto s3 = g.new_state();
|
auto s3 = g.new_state();
|
||||||
g.new_transition(s1, s2);
|
g.new_edge(s1, s2);
|
||||||
g.new_transition(s1, s3);
|
g.new_edge(s1, s3);
|
||||||
g.new_transition(s2, s3);
|
g.new_edge(s2, s3);
|
||||||
g.new_transition(s3, s1);
|
g.new_edge(s3, s1);
|
||||||
g.new_transition(s3, s2);
|
g.new_edge(s3, s2);
|
||||||
g.new_transition(s3, s3);
|
g.new_edge(s3, s3);
|
||||||
|
|
||||||
dot(std::cout, g);
|
dot(std::cout, g);
|
||||||
|
|
||||||
|
|
@ -118,10 +118,10 @@ bool f2()
|
||||||
auto s1 = g.new_state(1);
|
auto s1 = g.new_state(1);
|
||||||
auto s2 = g.new_state(2);
|
auto s2 = g.new_state(2);
|
||||||
auto s3 = g.new_state(3);
|
auto s3 = g.new_state(3);
|
||||||
g.new_transition(s1, s2);
|
g.new_edge(s1, s2);
|
||||||
g.new_transition(s1, s3);
|
g.new_edge(s1, s3);
|
||||||
g.new_transition(s2, s3);
|
g.new_edge(s2, s3);
|
||||||
g.new_transition(s3, s2);
|
g.new_edge(s3, s2);
|
||||||
|
|
||||||
dot(std::cout, g);
|
dot(std::cout, g);
|
||||||
|
|
||||||
|
|
@ -140,10 +140,10 @@ bool f3()
|
||||||
auto s1 = g.new_state();
|
auto s1 = g.new_state();
|
||||||
auto s2 = g.new_state();
|
auto s2 = g.new_state();
|
||||||
auto s3 = g.new_state();
|
auto s3 = g.new_state();
|
||||||
g.new_transition(s1, s2, 1);
|
g.new_edge(s1, s2, 1);
|
||||||
g.new_transition(s1, s3, 2);
|
g.new_edge(s1, s3, 2);
|
||||||
g.new_transition(s2, s3, 3);
|
g.new_edge(s2, s3, 3);
|
||||||
g.new_transition(s3, s2, 4);
|
g.new_edge(s3, s2, 4);
|
||||||
|
|
||||||
dot(std::cout, g);
|
dot(std::cout, g);
|
||||||
|
|
||||||
|
|
@ -162,10 +162,10 @@ bool f4()
|
||||||
auto s1 = g.new_state(2);
|
auto s1 = g.new_state(2);
|
||||||
auto s2 = g.new_state(3);
|
auto s2 = g.new_state(3);
|
||||||
auto s3 = g.new_state(4);
|
auto s3 = g.new_state(4);
|
||||||
g.new_transition(s1, s2, 1);
|
g.new_edge(s1, s2, 1);
|
||||||
g.new_transition(s1, s3, 2);
|
g.new_edge(s1, s3, 2);
|
||||||
g.new_transition(s2, s3, 3);
|
g.new_edge(s2, s3, 3);
|
||||||
g.new_transition(s3, s2, 4);
|
g.new_edge(s3, s2, 4);
|
||||||
|
|
||||||
dot(std::cout, g);
|
dot(std::cout, g);
|
||||||
|
|
||||||
|
|
@ -184,10 +184,10 @@ bool f5()
|
||||||
auto s1 = g.new_state();
|
auto s1 = g.new_state();
|
||||||
auto s2 = g.new_state();
|
auto s2 = g.new_state();
|
||||||
auto s3 = g.new_state();
|
auto s3 = g.new_state();
|
||||||
g.new_transition(s1, s2, std::make_pair(1, 1.2f));
|
g.new_edge(s1, s2, std::make_pair(1, 1.2f));
|
||||||
g.new_transition(s1, s3, std::make_pair(2, 1.3f));
|
g.new_edge(s1, s3, std::make_pair(2, 1.3f));
|
||||||
g.new_transition(s2, s3, std::make_pair(3, 1.4f));
|
g.new_edge(s2, s3, std::make_pair(3, 1.4f));
|
||||||
g.new_transition(s3, s2, std::make_pair(4, 1.5f));
|
g.new_edge(s3, s2, std::make_pair(4, 1.5f));
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
float h = 0;
|
float h = 0;
|
||||||
|
|
@ -206,10 +206,10 @@ bool f6()
|
||||||
auto s1 = g.new_state();
|
auto s1 = g.new_state();
|
||||||
auto s2 = g.new_state();
|
auto s2 = g.new_state();
|
||||||
auto s3 = g.new_state();
|
auto s3 = g.new_state();
|
||||||
g.new_transition(s1, s2, 1, 1.2f);
|
g.new_edge(s1, s2, 1, 1.2f);
|
||||||
g.new_transition(s1, s3, 2, 1.3f);
|
g.new_edge(s1, s3, 2, 1.3f);
|
||||||
g.new_transition(s2, s3, 3, 1.4f);
|
g.new_edge(s2, s3, 3, 1.4f);
|
||||||
g.new_transition(s3, s2, 4, 1.5f);
|
g.new_edge(s3, s2, 4, 1.5f);
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
float h = 0;
|
float h = 0;
|
||||||
|
|
@ -227,10 +227,10 @@ bool f7()
|
||||||
auto s1 = g.new_state(2);
|
auto s1 = g.new_state(2);
|
||||||
auto s2 = g.new_state(3);
|
auto s2 = g.new_state(3);
|
||||||
auto s3 = g.new_state(4);
|
auto s3 = g.new_state(4);
|
||||||
g.new_transition(s1, {s2, s3}, 1);
|
g.new_edge(s1, {s2, s3}, 1);
|
||||||
g.new_transition(s1, {s3}, 2);
|
g.new_edge(s1, {s3}, 2);
|
||||||
g.new_transition(s2, {s3}, 3);
|
g.new_edge(s2, {s3}, 3);
|
||||||
g.new_transition(s3, {s2}, 4);
|
g.new_edge(s3, {s2}, 4);
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
for (auto& t: g.out(s1))
|
for (auto& t: g.out(s1))
|
||||||
|
|
@ -273,10 +273,10 @@ bool f8()
|
||||||
auto s1 = g.new_state(2, 4);
|
auto s1 = g.new_state(2, 4);
|
||||||
auto s2 = g.new_state(3, 6);
|
auto s2 = g.new_state(3, 6);
|
||||||
auto s3 = g.new_state(4, 8);
|
auto s3 = g.new_state(4, 8);
|
||||||
g.new_transition(s1, s2, 1, 3);
|
g.new_edge(s1, s2, 1, 3);
|
||||||
g.new_transition(s1, s3, 2, 5);
|
g.new_edge(s1, s3, 2, 5);
|
||||||
g.new_transition(s2, s3, 3, 7);
|
g.new_edge(s2, s3, 3, 7);
|
||||||
g.new_transition(s3, s2, 4, 9);
|
g.new_edge(s3, s2, 4, 9);
|
||||||
|
|
||||||
dot(std::cout, g);
|
dot(std::cout, g);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -613,7 +613,7 @@ checked_main(int argc, char** argv)
|
||||||
if (spot::format_parse_aut_errors(std::cerr,
|
if (spot::format_parse_aut_errors(std::cerr,
|
||||||
argv[formula_index] + 2, pel))
|
argv[formula_index] + 2, pel))
|
||||||
return 2;
|
return 2;
|
||||||
daut->aut->merge_transitions();
|
daut->aut->merge_edges();
|
||||||
system_aut = daut->aut;
|
system_aut = daut->aut;
|
||||||
tm.stop("reading -P's argument");
|
tm.stop("reading -P's argument");
|
||||||
}
|
}
|
||||||
|
|
@ -1018,7 +1018,7 @@ checked_main(int argc, char** argv)
|
||||||
tm.stop("parsing hoa");
|
tm.stop("parsing hoa");
|
||||||
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
||||||
return 2;
|
return 2;
|
||||||
daut->aut->merge_transitions();
|
daut->aut->merge_edges();
|
||||||
a = daut->aut;
|
a = daut->aut;
|
||||||
assume_sba = a->is_sba();
|
assume_sba = a->is_sba();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// l'Epita.
|
// de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -128,12 +128,12 @@ bool f1()
|
||||||
auto s1 = gg.new_state("s1");
|
auto s1 = gg.new_state("s1");
|
||||||
auto s2 = gg.new_state("s2");
|
auto s2 = gg.new_state("s2");
|
||||||
auto s3 = gg.new_state("s3");
|
auto s3 = gg.new_state("s3");
|
||||||
gg.new_transition("s1", "s2");
|
gg.new_edge("s1", "s2");
|
||||||
gg.new_transition("s1", "s3");
|
gg.new_edge("s1", "s3");
|
||||||
gg.new_transition("s2", "s3");
|
gg.new_edge("s2", "s3");
|
||||||
gg.new_transition("s3", "s1");
|
gg.new_edge("s3", "s1");
|
||||||
gg.new_transition("s3", "s2");
|
gg.new_edge("s3", "s2");
|
||||||
gg.new_transition("s3", "s3");
|
gg.new_edge("s3", "s3");
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
@ -158,10 +158,10 @@ bool f2()
|
||||||
auto s1 = gg.new_state("s1", 1);
|
auto s1 = gg.new_state("s1", 1);
|
||||||
gg.new_state("s2", 2);
|
gg.new_state("s2", 2);
|
||||||
gg.new_state("s3", 3);
|
gg.new_state("s3", 3);
|
||||||
gg.new_transition("s1", "s2");
|
gg.new_edge("s1", "s2");
|
||||||
gg.new_transition("s1", "s3");
|
gg.new_edge("s1", "s3");
|
||||||
gg.new_transition("s2", "s3");
|
gg.new_edge("s2", "s3");
|
||||||
gg.new_transition("s3", "s2");
|
gg.new_edge("s3", "s2");
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
@ -181,10 +181,10 @@ bool f3()
|
||||||
auto s1 = gg.new_state("s1");
|
auto s1 = gg.new_state("s1");
|
||||||
gg.new_state("s2");
|
gg.new_state("s2");
|
||||||
gg.new_state("s3");
|
gg.new_state("s3");
|
||||||
gg.new_transition("s1", "s2", 1);
|
gg.new_edge("s1", "s2", 1);
|
||||||
gg.new_transition("s1", "s3", 2);
|
gg.new_edge("s1", "s3", 2);
|
||||||
gg.new_transition("s2", "s3", 3);
|
gg.new_edge("s2", "s3", 3);
|
||||||
gg.new_transition("s3", "s2", 4);
|
gg.new_edge("s3", "s2", 4);
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
@ -204,10 +204,10 @@ bool f4()
|
||||||
auto s1 = gg.new_state("s1", 2);
|
auto s1 = gg.new_state("s1", 2);
|
||||||
gg.new_state("s2", 3);
|
gg.new_state("s2", 3);
|
||||||
gg.new_state("s3", 4);
|
gg.new_state("s3", 4);
|
||||||
gg.new_transition("s1", "s2", 1);
|
gg.new_edge("s1", "s2", 1);
|
||||||
gg.new_transition("s1", "s3", 2);
|
gg.new_edge("s1", "s3", 2);
|
||||||
gg.new_transition("s2", "s3", 3);
|
gg.new_edge("s2", "s3", 3);
|
||||||
gg.new_transition("s3", "s2", 4);
|
gg.new_edge("s3", "s2", 4);
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
@ -228,10 +228,10 @@ bool f5()
|
||||||
auto s1 = gg.new_state("s1");
|
auto s1 = gg.new_state("s1");
|
||||||
gg.new_state("s2");
|
gg.new_state("s2");
|
||||||
gg.new_state("s3");
|
gg.new_state("s3");
|
||||||
gg.new_transition("s1", "s2", std::make_pair(1, 1.2f));
|
gg.new_edge("s1", "s2", std::make_pair(1, 1.2f));
|
||||||
gg.new_transition("s1", "s3", std::make_pair(2, 1.3f));
|
gg.new_edge("s1", "s3", std::make_pair(2, 1.3f));
|
||||||
gg.new_transition("s2", "s3", std::make_pair(3, 1.4f));
|
gg.new_edge("s2", "s3", std::make_pair(3, 1.4f));
|
||||||
gg.new_transition("s3", "s2", std::make_pair(4, 1.5f));
|
gg.new_edge("s3", "s2", std::make_pair(4, 1.5f));
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
float h = 0;
|
float h = 0;
|
||||||
|
|
@ -252,10 +252,10 @@ bool f6()
|
||||||
auto s1 = gg.new_state("s1");
|
auto s1 = gg.new_state("s1");
|
||||||
gg.new_state("s2");
|
gg.new_state("s2");
|
||||||
gg.new_state("s3");
|
gg.new_state("s3");
|
||||||
gg.new_transition("s1", "s2", 1, 1.2f);
|
gg.new_edge("s1", "s2", 1, 1.2f);
|
||||||
gg.new_transition("s1", "s3", 2, 1.3f);
|
gg.new_edge("s1", "s3", 2, 1.3f);
|
||||||
gg.new_transition("s2", "s3", 3, 1.4f);
|
gg.new_edge("s2", "s3", 3, 1.4f);
|
||||||
gg.new_transition("s3", "s2", 4, 1.5f);
|
gg.new_edge("s3", "s2", 4, 1.5f);
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
float h = 0;
|
float h = 0;
|
||||||
|
|
@ -276,10 +276,10 @@ bool f7()
|
||||||
auto s1 = gg.new_state("s1", 2);
|
auto s1 = gg.new_state("s1", 2);
|
||||||
gg.new_state("s2", 3);
|
gg.new_state("s2", 3);
|
||||||
gg.new_state("s3", 4);
|
gg.new_state("s3", 4);
|
||||||
gg.new_transition("s1", {"s2", "s3"}, 1);
|
gg.new_edge("s1", {"s2", "s3"}, 1);
|
||||||
gg.new_transition("s1", {"s3"}, 2);
|
gg.new_edge("s1", {"s3"}, 2);
|
||||||
gg.new_transition("s2", {"s3"}, 3);
|
gg.new_edge("s2", {"s3"}, 3);
|
||||||
gg.new_transition("s3", {"s2"}, 4);
|
gg.new_edge("s3", {"s2"}, 4);
|
||||||
|
|
||||||
int f = 0;
|
int f = 0;
|
||||||
for (auto& t: g.out(s1))
|
for (auto& t: g.out(s1))
|
||||||
|
|
@ -324,10 +324,10 @@ bool f8()
|
||||||
auto s1 = gg.new_state("s1", 2, 4);
|
auto s1 = gg.new_state("s1", 2, 4);
|
||||||
gg.new_state("s2", 3, 6);
|
gg.new_state("s2", 3, 6);
|
||||||
gg.new_state("s3", 4, 8);
|
gg.new_state("s3", 4, 8);
|
||||||
gg.new_transition("s1", "s2", 1, 3);
|
gg.new_edge("s1", "s2", 1, 3);
|
||||||
gg.new_transition("s1", "s3", 2, 5);
|
gg.new_edge("s1", "s3", 2, 5);
|
||||||
gg.new_transition("s2", "s3", 3, 7);
|
gg.new_edge("s2", "s3", 3, 7);
|
||||||
gg.new_transition("s3", "s2", 4, 9);
|
gg.new_edge("s3", "s2", 4, 9);
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
@ -392,10 +392,10 @@ bool f9()
|
||||||
auto s3 = gg.new_state("s3");
|
auto s3 = gg.new_state("s3");
|
||||||
gg.alias_state(s3, "s3b");
|
gg.alias_state(s3, "s3b");
|
||||||
|
|
||||||
gg.new_transition("s1", "s2", 1, 3);
|
gg.new_edge("s1", "s2", 1, 3);
|
||||||
gg.new_transition("s1", "s3", 2, 5);
|
gg.new_edge("s1", "s3", 2, 5);
|
||||||
gg.new_transition("s2", "s3b", 3, 7);
|
gg.new_edge("s2", "s3b", 3, 7);
|
||||||
gg.new_transition("s3", "s2", 4, 9);
|
gg.new_edge("s3", "s2", 4, 9);
|
||||||
|
|
||||||
dot(std::cout, gg);
|
dot(std::cout, gg);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// l'Epita.
|
// de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -42,13 +42,13 @@ void f1()
|
||||||
auto s1 = tg->new_state();
|
auto s1 = tg->new_state();
|
||||||
auto s2 = tg->new_state();
|
auto s2 = tg->new_state();
|
||||||
auto s3 = tg->new_state();
|
auto s3 = tg->new_state();
|
||||||
tg->new_transition(s1, s1, bddfalse, 0U);
|
tg->new_edge(s1, s1, bddfalse, 0U);
|
||||||
tg->new_transition(s1, s2, p1, 0U);
|
tg->new_edge(s1, s2, p1, 0U);
|
||||||
tg->new_transition(s1, s3, p2, tg->acc().mark(1));
|
tg->new_edge(s1, s3, p2, tg->acc().mark(1));
|
||||||
tg->new_transition(s2, s3, p1 & p2, tg->acc().mark(0));
|
tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0));
|
||||||
tg->new_transition(s3, s1, p1 | p2, tg->acc().marks({0, 1}));
|
tg->new_edge(s3, s1, p1 | p2, tg->acc().marks({0, 1}));
|
||||||
tg->new_transition(s3, s2, p1 >> p2, 0U);
|
tg->new_edge(s3, s2, p1 >> p2, 0U);
|
||||||
tg->new_transition(s3, s3, bddtrue, tg->acc().marks({0, 1}));
|
tg->new_edge(s3, s3, bddtrue, tg->acc().marks({0, 1}));
|
||||||
|
|
||||||
spot::print_dot(std::cout, tg);
|
spot::print_dot(std::cout, tg);
|
||||||
|
|
||||||
|
|
@ -69,19 +69,19 @@ void f1()
|
||||||
}
|
}
|
||||||
|
|
||||||
auto all = tg->acc().marks({0, 1});
|
auto all = tg->acc().marks({0, 1});
|
||||||
tg->new_transition(s3, s1, p1 | p2, all);
|
tg->new_edge(s3, s1, p1 | p2, all);
|
||||||
tg->new_transition(s3, s2, p1 >> p2, 0U);
|
tg->new_edge(s3, s2, p1 >> p2, 0U);
|
||||||
tg->new_transition(s3, s1, bddtrue, all);
|
tg->new_edge(s3, s1, bddtrue, all);
|
||||||
|
|
||||||
std::cerr << tg->num_transitions() << '\n';
|
std::cerr << tg->num_edges() << '\n';
|
||||||
assert(tg->num_transitions() == 7);
|
assert(tg->num_edges() == 7);
|
||||||
|
|
||||||
spot::print_dot(std::cout, tg);
|
spot::print_dot(std::cout, tg);
|
||||||
tg->merge_transitions();
|
tg->merge_edges();
|
||||||
spot::print_dot(std::cout, tg);
|
spot::print_dot(std::cout, tg);
|
||||||
|
|
||||||
std::cerr << tg->num_transitions() << '\n';
|
std::cerr << tg->num_edges() << '\n';
|
||||||
assert(tg->num_transitions() == 5);
|
assert(tg->num_edges() == 5);
|
||||||
|
|
||||||
// Add enough states so that the state vector is reallocated.
|
// Add enough states so that the state vector is reallocated.
|
||||||
for (unsigned i = 0; i < 100; ++i)
|
for (unsigned i = 0; i < 100; ++i)
|
||||||
|
|
|
||||||
|
|
@ -53,12 +53,12 @@ namespace spot
|
||||||
delete namer;
|
delete namer;
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::merge_transitions()
|
void twa_graph::merge_edges()
|
||||||
{
|
{
|
||||||
g_.remove_dead_transitions_();
|
g_.remove_dead_edges_();
|
||||||
|
|
||||||
typedef graph_t::trans_storage_t tr_t;
|
typedef graph_t::edge_storage_t tr_t;
|
||||||
g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
|
g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
|
||||||
{
|
{
|
||||||
if (lhs.src < rhs.src)
|
if (lhs.src < rhs.src)
|
||||||
return true;
|
return true;
|
||||||
|
|
@ -73,11 +73,11 @@ namespace spot
|
||||||
// them.
|
// them.
|
||||||
});
|
});
|
||||||
|
|
||||||
auto& trans = this->transition_vector();
|
auto& trans = this->edge_vector();
|
||||||
unsigned tend = trans.size();
|
unsigned tend = trans.size();
|
||||||
unsigned out = 0;
|
unsigned out = 0;
|
||||||
unsigned in = 1;
|
unsigned in = 1;
|
||||||
// Skip any leading false transition.
|
// Skip any leading false edge.
|
||||||
while (in < tend && trans[in].cond == bddfalse)
|
while (in < tend && trans[in].cond == bddfalse)
|
||||||
++in;
|
++in;
|
||||||
if (in < tend)
|
if (in < tend)
|
||||||
|
|
@ -87,11 +87,11 @@ namespace spot
|
||||||
trans[out] = trans[in];
|
trans[out] = trans[in];
|
||||||
for (++in; in < tend; ++in)
|
for (++in; in < tend; ++in)
|
||||||
{
|
{
|
||||||
if (trans[in].cond == bddfalse) // Unusable transition
|
if (trans[in].cond == bddfalse) // Unusable edge
|
||||||
continue;
|
continue;
|
||||||
// Merge transitions with the same source, destination, and
|
// Merge edges with the same source, destination, and
|
||||||
// acceptance. (We test the source last, because this is the
|
// acceptance. (We test the source last, because this is the
|
||||||
// most likely test to be true as transitions are ordered by
|
// most likely test to be true as edges are ordered by
|
||||||
// sources and then destinations.)
|
// sources and then destinations.)
|
||||||
if (trans[out].dst == trans[in].dst
|
if (trans[out].dst == trans[in].dst
|
||||||
&& trans[out].acc == trans[in].acc
|
&& trans[out].acc == trans[in].acc
|
||||||
|
|
@ -113,14 +113,14 @@ namespace spot
|
||||||
tend = out;
|
tend = out;
|
||||||
out = in = 2;
|
out = in = 2;
|
||||||
|
|
||||||
// FIXME: We could should also merge transitions when using
|
// FIXME: We could should also merge edges when using
|
||||||
// fin_acceptance, but the rule for Fin sets are different than
|
// fin_acceptance, but the rule for Fin sets are different than
|
||||||
// those for Inf sets, (and we need to be careful if a set is used
|
// those for Inf sets, (and we need to be careful if a set is used
|
||||||
// both as Inf and Fin)
|
// both as Inf and Fin)
|
||||||
if ((in < tend) && !acc().uses_fin_acceptance())
|
if ((in < tend) && !acc().uses_fin_acceptance())
|
||||||
{
|
{
|
||||||
typedef graph_t::trans_storage_t tr_t;
|
typedef graph_t::edge_storage_t tr_t;
|
||||||
g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
|
g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
|
||||||
{
|
{
|
||||||
if (lhs.src < rhs.src)
|
if (lhs.src < rhs.src)
|
||||||
return true;
|
return true;
|
||||||
|
|
@ -137,7 +137,7 @@ namespace spot
|
||||||
|
|
||||||
for (; in < tend; ++in)
|
for (; in < tend; ++in)
|
||||||
{
|
{
|
||||||
// Merge transitions with the same source, destination,
|
// Merge edges with the same source, destination,
|
||||||
// and conditions. (We test the source last, for the
|
// and conditions. (We test the source last, for the
|
||||||
// same reason as above.)
|
// same reason as above.)
|
||||||
if (trans[out].dst == trans[in].dst
|
if (trans[out].dst == trans[in].dst
|
||||||
|
|
@ -157,7 +157,7 @@ namespace spot
|
||||||
trans.resize(out);
|
trans.resize(out);
|
||||||
}
|
}
|
||||||
|
|
||||||
g_.chain_transitions_();
|
g_.chain_edges_();
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::purge_unreachable_states()
|
void twa_graph::purge_unreachable_states()
|
||||||
|
|
@ -228,7 +228,7 @@ namespace spot
|
||||||
order.push_back(src);
|
order.push_back(src);
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
auto& t = g_.trans_storage(tid);
|
auto& t = g_.edge_storage(tid);
|
||||||
todo.back().second = t.next_succ;
|
todo.back().second = t.next_succ;
|
||||||
unsigned dst = t.dst;
|
unsigned dst = t.dst;
|
||||||
if (useful[dst] != 1)
|
if (useful[dst] != 1)
|
||||||
|
|
@ -246,13 +246,13 @@ namespace spot
|
||||||
bool useless = true;
|
bool useless = true;
|
||||||
while (t)
|
while (t)
|
||||||
{
|
{
|
||||||
// Erase any transition to a useless state.
|
// Erase any edge to a useless state.
|
||||||
if (!useful[t->dst])
|
if (!useful[t->dst])
|
||||||
{
|
{
|
||||||
t.erase();
|
t.erase();
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
// if we have a transition to a useful state, then the
|
// if we have a edge to a useful state, then the
|
||||||
// state is useful.
|
// state is useful.
|
||||||
useless = false;
|
useless = false;
|
||||||
++t;
|
++t;
|
||||||
|
|
|
||||||
|
|
@ -73,22 +73,22 @@ namespace spot
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
struct SPOT_API twa_graph_trans_data
|
struct SPOT_API twa_graph_edge_data
|
||||||
{
|
{
|
||||||
bdd cond;
|
bdd cond;
|
||||||
acc_cond::mark_t acc;
|
acc_cond::mark_t acc;
|
||||||
|
|
||||||
explicit twa_graph_trans_data()
|
explicit twa_graph_edge_data()
|
||||||
: cond(bddfalse), acc(0)
|
: cond(bddfalse), acc(0)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
twa_graph_trans_data(bdd cond, acc_cond::mark_t acc = 0U)
|
twa_graph_edge_data(bdd cond, acc_cond::mark_t acc = 0U)
|
||||||
: cond(cond), acc(acc)
|
: cond(cond), acc(acc)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator<(const twa_graph_trans_data& other) const
|
bool operator<(const twa_graph_edge_data& other) const
|
||||||
{
|
{
|
||||||
if (cond.id() < other.cond.id())
|
if (cond.id() < other.cond.id())
|
||||||
return true;
|
return true;
|
||||||
|
|
@ -97,7 +97,7 @@ namespace spot
|
||||||
return acc < other.acc;
|
return acc < other.acc;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool operator==(const twa_graph_trans_data& other) const
|
bool operator==(const twa_graph_edge_data& other) const
|
||||||
{
|
{
|
||||||
return cond.id() == other.cond.id() &&
|
return cond.id() == other.cond.id() &&
|
||||||
acc == other.acc;
|
acc == other.acc;
|
||||||
|
|
@ -110,19 +110,19 @@ namespace spot
|
||||||
public twa_succ_iterator
|
public twa_succ_iterator
|
||||||
{
|
{
|
||||||
private:
|
private:
|
||||||
typedef typename Graph::transition transition;
|
typedef typename Graph::edge edge;
|
||||||
typedef typename Graph::state_data_t state;
|
typedef typename Graph::state_data_t state;
|
||||||
const Graph* g_;
|
const Graph* g_;
|
||||||
transition t_;
|
edge t_;
|
||||||
transition p_;
|
edge p_;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
twa_graph_succ_iterator(const Graph* g, transition t)
|
twa_graph_succ_iterator(const Graph* g, edge t)
|
||||||
: g_(g), t_(t)
|
: g_(g), t_(t)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void recycle(transition t)
|
virtual void recycle(edge t)
|
||||||
{
|
{
|
||||||
t_ = t;
|
t_ = t;
|
||||||
}
|
}
|
||||||
|
|
@ -135,7 +135,7 @@ namespace spot
|
||||||
|
|
||||||
virtual bool next()
|
virtual bool next()
|
||||||
{
|
{
|
||||||
p_ = g_->trans_storage(p_).next_succ;
|
p_ = g_->edge_storage(p_).next_succ;
|
||||||
return p_;
|
return p_;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -148,22 +148,22 @@ namespace spot
|
||||||
{
|
{
|
||||||
assert(!done());
|
assert(!done());
|
||||||
return const_cast<twa_graph_state*>
|
return const_cast<twa_graph_state*>
|
||||||
(&g_->state_data(g_->trans_storage(p_).dst));
|
(&g_->state_data(g_->edge_storage(p_).dst));
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual bdd current_condition() const
|
virtual bdd current_condition() const
|
||||||
{
|
{
|
||||||
assert(!done());
|
assert(!done());
|
||||||
return g_->trans_data(p_).cond;
|
return g_->edge_data(p_).cond;
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual acc_cond::mark_t current_acceptance_conditions() const
|
virtual acc_cond::mark_t current_acceptance_conditions() const
|
||||||
{
|
{
|
||||||
assert(!done());
|
assert(!done());
|
||||||
return g_->trans_data(p_).acc;
|
return g_->edge_data(p_).acc;
|
||||||
}
|
}
|
||||||
|
|
||||||
transition pos() const
|
edge pos() const
|
||||||
{
|
{
|
||||||
return p_;
|
return p_;
|
||||||
}
|
}
|
||||||
|
|
@ -173,8 +173,8 @@ namespace spot
|
||||||
class SPOT_API twa_graph final: public twa
|
class SPOT_API twa_graph final: public twa
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
typedef digraph<twa_graph_state, twa_graph_trans_data> graph_t;
|
typedef digraph<twa_graph_state, twa_graph_edge_data> graph_t;
|
||||||
typedef graph_t::trans_storage_t trans_storage_t;
|
typedef graph_t::edge_storage_t edge_storage_t;
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
graph_t g_;
|
graph_t g_;
|
||||||
|
|
@ -248,9 +248,9 @@ namespace spot
|
||||||
return g_.num_states();
|
return g_.num_states();
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned num_transitions() const
|
unsigned num_edges() const
|
||||||
{
|
{
|
||||||
return g_.num_transitions();
|
return g_.num_edges();
|
||||||
}
|
}
|
||||||
|
|
||||||
void set_init_state(graph_t::state s)
|
void set_init_state(graph_t::state s)
|
||||||
|
|
@ -323,49 +323,49 @@ namespace spot
|
||||||
return format_state(state_number(st));
|
return format_state(state_number(st));
|
||||||
}
|
}
|
||||||
|
|
||||||
twa_graph_trans_data& trans_data(const twa_succ_iterator* it)
|
twa_graph_edge_data& edge_data(const twa_succ_iterator* it)
|
||||||
{
|
{
|
||||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||||
return g_.trans_data(i->pos());
|
return g_.edge_data(i->pos());
|
||||||
}
|
}
|
||||||
|
|
||||||
twa_graph_trans_data& trans_data(unsigned t)
|
twa_graph_edge_data& edge_data(unsigned t)
|
||||||
{
|
{
|
||||||
return g_.trans_data(t);
|
return g_.edge_data(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
const twa_graph_trans_data& trans_data(const twa_succ_iterator* it) const
|
const twa_graph_edge_data& edge_data(const twa_succ_iterator* it) const
|
||||||
{
|
{
|
||||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||||
return g_.trans_data(i->pos());
|
return g_.edge_data(i->pos());
|
||||||
}
|
}
|
||||||
|
|
||||||
const twa_graph_trans_data& trans_data(unsigned t) const
|
const twa_graph_edge_data& edge_data(unsigned t) const
|
||||||
{
|
{
|
||||||
return g_.trans_data(t);
|
return g_.edge_data(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_storage_t& trans_storage(const twa_succ_iterator* it)
|
edge_storage_t& edge_storage(const twa_succ_iterator* it)
|
||||||
{
|
{
|
||||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||||
return g_.trans_storage(i->pos());
|
return g_.edge_storage(i->pos());
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_storage_t& trans_storage(unsigned t)
|
edge_storage_t& edge_storage(unsigned t)
|
||||||
{
|
{
|
||||||
return g_.trans_storage(t);
|
return g_.edge_storage(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
const trans_storage_t
|
const edge_storage_t
|
||||||
trans_storage(const twa_succ_iterator* it) const
|
edge_storage(const twa_succ_iterator* it) const
|
||||||
{
|
{
|
||||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||||
return g_.trans_storage(i->pos());
|
return g_.edge_storage(i->pos());
|
||||||
}
|
}
|
||||||
|
|
||||||
const trans_storage_t trans_storage(unsigned t) const
|
const edge_storage_t edge_storage(unsigned t) const
|
||||||
{
|
{
|
||||||
return g_.trans_storage(t);
|
return g_.edge_storage(t);
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned new_state()
|
unsigned new_state()
|
||||||
|
|
@ -378,19 +378,19 @@ namespace spot
|
||||||
return g_.new_states(n);
|
return g_.new_states(n);
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned new_transition(unsigned src, unsigned dst,
|
unsigned new_edge(unsigned src, unsigned dst,
|
||||||
bdd cond, acc_cond::mark_t acc = 0U)
|
bdd cond, acc_cond::mark_t acc = 0U)
|
||||||
{
|
{
|
||||||
return g_.new_transition(src, dst, cond, acc);
|
return g_.new_edge(src, dst, cond, acc);
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned new_acc_transition(unsigned src, unsigned dst,
|
unsigned new_acc_edge(unsigned src, unsigned dst,
|
||||||
bdd cond, bool acc = true)
|
bdd cond, bool acc = true)
|
||||||
{
|
{
|
||||||
if (acc)
|
if (acc)
|
||||||
return g_.new_transition(src, dst, cond, acc_.all_sets());
|
return g_.new_edge(src, dst, cond, acc_.all_sets());
|
||||||
else
|
else
|
||||||
return g_.new_transition(src, dst, cond);
|
return g_.new_edge(src, dst, cond);
|
||||||
}
|
}
|
||||||
|
|
||||||
#ifndef SWIG
|
#ifndef SWIG
|
||||||
|
|
@ -404,18 +404,18 @@ namespace spot
|
||||||
auto states()
|
auto states()
|
||||||
SPOT_RETURN(g_.states());
|
SPOT_RETURN(g_.states());
|
||||||
|
|
||||||
auto transitions() const
|
auto edges() const
|
||||||
SPOT_RETURN(g_.transitions());
|
SPOT_RETURN(g_.edges());
|
||||||
auto transitions()
|
auto edges()
|
||||||
SPOT_RETURN(g_.transitions());
|
SPOT_RETURN(g_.edges());
|
||||||
|
|
||||||
auto transition_vector() const
|
auto edge_vector() const
|
||||||
SPOT_RETURN(g_.transition_vector());
|
SPOT_RETURN(g_.edge_vector());
|
||||||
auto transition_vector()
|
auto edge_vector()
|
||||||
SPOT_RETURN(g_.transition_vector());
|
SPOT_RETURN(g_.edge_vector());
|
||||||
|
|
||||||
auto is_dead_transition(const graph_t::trans_storage_t& t) const
|
auto is_dead_edge(const graph_t::edge_storage_t& t) const
|
||||||
SPOT_RETURN(g_.is_dead_transition(t));
|
SPOT_RETURN(g_.is_dead_edge(t));
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
virtual bdd compute_support_conditions(const state* s) const
|
virtual bdd compute_support_conditions(const state* s) const
|
||||||
|
|
@ -426,9 +426,9 @@ namespace spot
|
||||||
return sum;
|
return sum;
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Iterate over all transitions, and merge those with compatible
|
/// Iterate over all edges, and merge those with compatible
|
||||||
/// extremities and acceptance.
|
/// extremities and acceptance.
|
||||||
void merge_transitions();
|
void merge_edges();
|
||||||
|
|
||||||
/// Remove all states without successors.
|
/// Remove all states without successors.
|
||||||
void purge_dead_states();
|
void purge_dead_states();
|
||||||
|
|
@ -440,7 +440,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
assert(has_state_based_acc() || num_sets() == 0);
|
assert(has_state_based_acc() || num_sets() == 0);
|
||||||
for (auto& t: g_.out(s))
|
for (auto& t: g_.out(s))
|
||||||
// Stop at the first transition, since the remaining should be
|
// Stop at the first edge, since the remaining should be
|
||||||
// labeled identically.
|
// labeled identically.
|
||||||
return t.acc;
|
return t.acc;
|
||||||
return 0U;
|
return 0U;
|
||||||
|
|
@ -450,7 +450,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
assert(has_state_based_acc() || num_sets() == 0);
|
assert(has_state_based_acc() || num_sets() == 0);
|
||||||
for (auto& t: g_.out(s))
|
for (auto& t: g_.out(s))
|
||||||
// Stop at the first transition, since the remaining should be
|
// Stop at the first edge, since the remaining should be
|
||||||
// labeled identically.
|
// labeled identically.
|
||||||
return acc_.accepting(t.acc);
|
return acc_.accepting(t.acc);
|
||||||
return false;
|
return false;
|
||||||
|
|
@ -464,11 +464,11 @@ namespace spot
|
||||||
bool operator==(const twa_graph& aut) const
|
bool operator==(const twa_graph& aut) const
|
||||||
{
|
{
|
||||||
if (num_states() != aut.num_states() ||
|
if (num_states() != aut.num_states() ||
|
||||||
num_transitions() != aut.num_transitions() ||
|
num_edges() != aut.num_edges() ||
|
||||||
num_sets() != aut.num_sets())
|
num_sets() != aut.num_sets())
|
||||||
return false;
|
return false;
|
||||||
auto& trans1 = transition_vector();
|
auto& trans1 = edge_vector();
|
||||||
auto& trans2 = aut.transition_vector();
|
auto& trans2 = aut.edge_vector();
|
||||||
return std::equal(trans1.begin() + 1, trans1.end(),
|
return std::equal(trans1.begin() + 1, trans1.end(),
|
||||||
trans2.begin() + 1);
|
trans2.begin() + 1);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
|
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
|
||||||
|
|
@ -29,7 +29,7 @@
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
typedef spot::twa_graph::graph_t::trans_storage_t tr_t;
|
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
|
||||||
bool
|
bool
|
||||||
tr_t_less_than(const tr_t& t1, const tr_t& t2)
|
tr_t_less_than(const tr_t& t1, const tr_t& t2)
|
||||||
{
|
{
|
||||||
|
|
@ -101,7 +101,7 @@ namespace
|
||||||
const spot::const_twa_graph_ptr aut2)
|
const spot::const_twa_graph_ptr aut2)
|
||||||
{
|
{
|
||||||
return aut1->num_states() != aut2->num_states() ||
|
return aut1->num_states() != aut2->num_states() ||
|
||||||
aut1->num_transitions() != aut2->num_transitions() ||
|
aut1->num_edges() != aut2->num_edges() ||
|
||||||
// FIXME: At some point, it would be nice to support reordering
|
// FIXME: At some point, it would be nice to support reordering
|
||||||
// of acceptance sets (issue #58).
|
// of acceptance sets (issue #58).
|
||||||
aut1->acc().get_acceptance() != aut2->acc().get_acceptance();
|
aut1->acc().get_acceptance() != aut2->acc().get_acceptance();
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -49,6 +49,5 @@ namespace spot
|
||||||
twa_graph_ptr ref_;
|
twa_graph_ptr ref_;
|
||||||
bool ref_deterministic_ = false;
|
bool ref_deterministic_ = false;
|
||||||
unsigned nondet_states_ = 0;
|
unsigned nondet_states_ = 0;
|
||||||
std::vector<twa_graph::graph_t::trans_storage_t> reftrans_;
|
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
|
||||||
// Developpement de l Epita (LRDE).
|
// Developpement de l Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -24,13 +24,13 @@
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
typedef std::pair<spot::twa_graph::graph_t::trans_data_t, unsigned>
|
typedef std::pair<spot::twa_graph::graph_t::edge_data_t, unsigned>
|
||||||
trans_sig_t;
|
edge_sig_t;
|
||||||
|
|
||||||
struct signature_t
|
struct signature_t
|
||||||
{
|
{
|
||||||
std::vector<trans_sig_t> ingoing;
|
std::vector<edge_sig_t> ingoing;
|
||||||
std::vector<trans_sig_t> outgoing;
|
std::vector<edge_sig_t> outgoing;
|
||||||
unsigned classnum;
|
unsigned classnum;
|
||||||
|
|
||||||
bool
|
bool
|
||||||
|
|
@ -49,7 +49,7 @@ namespace
|
||||||
{
|
{
|
||||||
std::vector<signature_t> signature(aut->num_states(), signature_t());
|
std::vector<signature_t> signature(aut->num_states(), signature_t());
|
||||||
|
|
||||||
for (auto& t : aut->transitions())
|
for (auto& t : aut->edges())
|
||||||
{
|
{
|
||||||
signature[t.dst].ingoing.emplace_back(t.data(), state2class[t.src]);
|
signature[t.dst].ingoing.emplace_back(t.data(), state2class[t.src]);
|
||||||
signature[t.src].outgoing.emplace_back(t.data(), state2class[t.dst]);
|
signature[t.src].outgoing.emplace_back(t.data(), state2class[t.dst]);
|
||||||
|
|
@ -102,8 +102,8 @@ namespace spot
|
||||||
auto& g = aut->get_graph();
|
auto& g = aut->get_graph();
|
||||||
g.rename_states_(state2class);
|
g.rename_states_(state2class);
|
||||||
aut->set_init_state(state2class[aut->get_init_state_number()]);
|
aut->set_init_state(state2class[aut->get_init_state_number()]);
|
||||||
g.sort_transitions_();
|
g.sort_edges_();
|
||||||
g.chain_transitions_();
|
g.chain_edges_();
|
||||||
return aut;
|
return aut;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -31,7 +31,7 @@ namespace spot
|
||||||
acc_cond::mark_t used_in_cond = c.used_sets();
|
acc_cond::mark_t used_in_cond = c.used_sets();
|
||||||
|
|
||||||
acc_cond::mark_t used_in_aut = 0U;
|
acc_cond::mark_t used_in_aut = 0U;
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
used_in_aut |= t.acc;
|
used_in_aut |= t.acc;
|
||||||
|
|
||||||
auto useful = used_in_aut & used_in_cond;
|
auto useful = used_in_aut & used_in_cond;
|
||||||
|
|
@ -42,7 +42,7 @@ namespace spot
|
||||||
return aut;
|
return aut;
|
||||||
|
|
||||||
// Remove useless marks from the automaton
|
// Remove useless marks from the automaton
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
t.acc = t.acc.strip(useless);
|
t.acc = t.acc.strip(useless);
|
||||||
|
|
||||||
// Remove useless marks from the acceptance condition
|
// Remove useless marks from the acceptance condition
|
||||||
|
|
|
||||||
|
|
@ -35,7 +35,7 @@ namespace spot
|
||||||
// We cannot safely complete an automaton if its
|
// We cannot safely complete an automaton if its
|
||||||
// acceptance is always satisfiable.
|
// acceptance is always satisfiable.
|
||||||
auto acc = aut->set_buchi();
|
auto acc = aut->set_buchi();
|
||||||
for (auto& t: aut->transition_vector())
|
for (auto& t: aut->edge_vector())
|
||||||
t.acc = acc;
|
t.acc = acc;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -67,7 +67,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned t = aut->num_transitions();
|
unsigned t = aut->num_edges();
|
||||||
|
|
||||||
// Now complete all states (excluding any newly added the sink).
|
// Now complete all states (excluding any newly added the sink).
|
||||||
for (unsigned i = 0; i < n; ++i)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
|
|
@ -80,39 +80,39 @@ namespace spot
|
||||||
// FIXME: This is ugly.
|
// FIXME: This is ugly.
|
||||||
//
|
//
|
||||||
// In case the automaton uses state-based acceptance, we
|
// In case the automaton uses state-based acceptance, we
|
||||||
// need to put the new transition in the same set as all
|
// need to put the new edge in the same set as all
|
||||||
// the other.
|
// the other.
|
||||||
//
|
//
|
||||||
// In case the automaton uses transition-based acceptance,
|
// In case the automaton uses edge-based acceptance,
|
||||||
// it does not matter what acceptance set we put the new
|
// it does not matter what acceptance set we put the new
|
||||||
// transition into.
|
// edge into.
|
||||||
//
|
//
|
||||||
// So in both cases, we put the transition in the same
|
// So in both cases, we put the edge in the same
|
||||||
// acceptance sets as the last outgoing transition of the
|
// acceptance sets as the last outgoing edge of the
|
||||||
// state.
|
// state.
|
||||||
acc = t.acc;
|
acc = t.acc;
|
||||||
}
|
}
|
||||||
// If the state has incomplete successors, we need to add a
|
// If the state has incomplete successors, we need to add a
|
||||||
// transition to some sink state.
|
// edge to some sink state.
|
||||||
if (missingcond != bddfalse)
|
if (missingcond != bddfalse)
|
||||||
{
|
{
|
||||||
// If we haven't found any sink, simply add one.
|
// If we haven't found any sink, simply add one.
|
||||||
if (sink == -1U)
|
if (sink == -1U)
|
||||||
{
|
{
|
||||||
sink = aut->new_state();
|
sink = aut->new_state();
|
||||||
aut->new_transition(sink, sink, bddtrue, um.second);
|
aut->new_edge(sink, sink, bddtrue, um.second);
|
||||||
}
|
}
|
||||||
// In case the automaton use state-based acceptance, propagate
|
// In case the automaton use state-based acceptance, propagate
|
||||||
// the acceptance of the first transition to the one we add.
|
// the acceptance of the first edge to the one we add.
|
||||||
aut->new_transition(i, sink, missingcond, acc);
|
aut->new_edge(i, sink, missingcond, acc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Get rid of any named property if the automaton changed.
|
// Get rid of any named property if the automaton changed.
|
||||||
if (t < aut->num_transitions())
|
if (t < aut->num_edges())
|
||||||
aut->release_named_properties();
|
aut->release_named_properties();
|
||||||
else
|
else
|
||||||
assert(t == aut->num_transitions());
|
assert(t == aut->num_edges());
|
||||||
|
|
||||||
return sink;
|
return sink;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -266,7 +266,7 @@ namespace spot
|
||||||
p.second = ris;
|
p.second = ris;
|
||||||
}
|
}
|
||||||
|
|
||||||
// This loops over all the right transitions
|
// This loops over all the right edges
|
||||||
// if RI is defined. Otherwise this just makes
|
// if RI is defined. Otherwise this just makes
|
||||||
// one iteration as if the right automaton was
|
// one iteration as if the right automaton was
|
||||||
// looping in state 0 with "true".
|
// looping in state 0 with "true".
|
||||||
|
|
@ -277,7 +277,7 @@ namespace spot
|
||||||
if (ri)
|
if (ri)
|
||||||
{
|
{
|
||||||
cond = lc & ri->current_condition();
|
cond = lc & ri->current_condition();
|
||||||
// Skip incompatible transitions.
|
// Skip incompatible edges.
|
||||||
if (cond == bddfalse)
|
if (cond == bddfalse)
|
||||||
{
|
{
|
||||||
ri->next();
|
ri->next();
|
||||||
|
|
@ -303,7 +303,7 @@ namespace spot
|
||||||
acc_cond::mark_t a =
|
acc_cond::mark_t a =
|
||||||
res->acc().join(la, li->current_acceptance_conditions(),
|
res->acc().join(la, li->current_acceptance_conditions(),
|
||||||
ra, racc);
|
ra, racc);
|
||||||
res->new_transition(src, dest, bdd_exist(cond, v), a);
|
res->new_edge(src, dest, bdd_exist(cond, v), a);
|
||||||
|
|
||||||
if (ri)
|
if (ri)
|
||||||
ri->next();
|
ri->next();
|
||||||
|
|
|
||||||
|
|
@ -88,14 +88,14 @@ namespace spot
|
||||||
if (cur.succ == 0)
|
if (cur.succ == 0)
|
||||||
cur.succ = aut_->get_graph().state_storage(cur.s).succ;
|
cur.succ = aut_->get_graph().state_storage(cur.s).succ;
|
||||||
else
|
else
|
||||||
cur.succ = aut_->trans_storage(cur.succ).next_succ;
|
cur.succ = aut_->edge_storage(cur.succ).next_succ;
|
||||||
if (cur.succ)
|
if (cur.succ)
|
||||||
{
|
{
|
||||||
// Explore one successor.
|
// Explore one successor.
|
||||||
|
|
||||||
// Ignore those that are not on the SCC, or destination
|
// Ignore those that are not on the SCC, or destination
|
||||||
// that have been "virtually" deleted from A(v).
|
// that have been "virtually" deleted from A(v).
|
||||||
unsigned s = aut_->trans_storage(cur.succ).dst;
|
unsigned s = aut_->edge_storage(cur.succ).dst;
|
||||||
|
|
||||||
if ((sm_.scc_of(s) != scc) || (info_[cur.s].del[s]))
|
if ((sm_.scc_of(s) != scc) || (info_[cur.s].del[s]))
|
||||||
continue;
|
continue;
|
||||||
|
|
|
||||||
|
|
@ -55,7 +55,7 @@ namespace spot
|
||||||
// Queue of state to be processed.
|
// Queue of state to be processed.
|
||||||
typedef std::deque<degen_state> queue_t;
|
typedef std::deque<degen_state> queue_t;
|
||||||
|
|
||||||
// Acceptance set common to all outgoing transitions (of the same
|
// Acceptance set common to all outgoing edges (of the same
|
||||||
// SCC -- we do not care about the other) of some state.
|
// SCC -- we do not care about the other) of some state.
|
||||||
class outgoing_acc
|
class outgoing_acc
|
||||||
{
|
{
|
||||||
|
|
@ -75,7 +75,7 @@ namespace spot
|
||||||
bool seen = false;
|
bool seen = false;
|
||||||
for (auto& t: a_->out(s))
|
for (auto& t: a_->out(s))
|
||||||
{
|
{
|
||||||
// Ignore transitions that leave the SCC of s.
|
// Ignore edges that leave the SCC of s.
|
||||||
unsigned d = t.dst;
|
unsigned d = t.dst;
|
||||||
unsigned s2 = sm_ ? sm_->scc_of(d) : 0;
|
unsigned s2 = sm_ ? sm_->scc_of(d) : 0;
|
||||||
if (s2 != s1)
|
if (s2 != s1)
|
||||||
|
|
@ -237,10 +237,10 @@ namespace spot
|
||||||
// and vice-versa.
|
// and vice-versa.
|
||||||
ds2num_map ds2num;
|
ds2num_map ds2num;
|
||||||
|
|
||||||
// This map is used to find transitions that go to the same
|
// This map is used to find edges that go to the same
|
||||||
// destination with the same acceptance. The integer key is
|
// destination with the same acceptance. The integer key is
|
||||||
// (dest*2+acc) where dest is the destination state number, and
|
// (dest*2+acc) where dest is the destination state number, and
|
||||||
// acc is 1 iff the transition is accepting. The source
|
// acc is 1 iff the edge is accepting. The source
|
||||||
// is always that of the current iteration.
|
// is always that of the current iteration.
|
||||||
typedef std::map<int, unsigned> tr_cache_t;
|
typedef std::map<int, unsigned> tr_cache_t;
|
||||||
tr_cache_t tr_cache;
|
tr_cache_t tr_cache;
|
||||||
|
|
@ -268,7 +268,7 @@ namespace spot
|
||||||
if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first))
|
if (want_sba && !ignaccsl && outgoing.has_acc_selfloop(s.first))
|
||||||
s.second = order.size();
|
s.second = order.size();
|
||||||
// Otherwise, check for acceptance conditions common to all
|
// Otherwise, check for acceptance conditions common to all
|
||||||
// outgoing transitions, and assume we have already seen these and
|
// outgoing edges, and assume we have already seen these and
|
||||||
// start on the associated level.
|
// start on the associated level.
|
||||||
if (s.second == 0)
|
if (s.second == 0)
|
||||||
{
|
{
|
||||||
|
|
@ -345,12 +345,12 @@ namespace spot
|
||||||
{
|
{
|
||||||
// Ignore the last expected acceptance set (the value of
|
// Ignore the last expected acceptance set (the value of
|
||||||
// prev below) if it is common to all other outgoing
|
// prev below) if it is common to all other outgoing
|
||||||
// transitions (of the current state) AND if it is not
|
// edges (of the current state) AND if it is not
|
||||||
// used by any outgoing transition of the destination
|
// used by any outgoing edge of the destination
|
||||||
// state.
|
// state.
|
||||||
//
|
//
|
||||||
// 1) It's correct to do that, because this acceptance
|
// 1) It's correct to do that, because this acceptance
|
||||||
// set is common to other outgoing transitions.
|
// set is common to other outgoing edges.
|
||||||
// Therefore if we make a cycle to this state we
|
// Therefore if we make a cycle to this state we
|
||||||
// will eventually see that acceptance set thanks
|
// will eventually see that acceptance set thanks
|
||||||
// to the "pulling" of the common acceptance sets
|
// to the "pulling" of the common acceptance sets
|
||||||
|
|
@ -360,7 +360,7 @@ namespace spot
|
||||||
// degeneralization idempotent (up to a renaming
|
// degeneralization idempotent (up to a renaming
|
||||||
// of states). Consider the following automaton
|
// of states). Consider the following automaton
|
||||||
// where 1 is initial and => marks accepting
|
// where 1 is initial and => marks accepting
|
||||||
// transitions: 1=>1, 1=>2, 2->2, 2->1. This is
|
// edges: 1=>1, 1=>2, 2->2, 2->1. This is
|
||||||
// already an SBA, with 1 as accepting state.
|
// already an SBA, with 1 as accepting state.
|
||||||
// However if you try degeralize it without
|
// However if you try degeralize it without
|
||||||
// ignoring *prev, you'll get two copies of state
|
// ignoring *prev, you'll get two copies of state
|
||||||
|
|
@ -389,9 +389,9 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// A transition in the SLEVEL acceptance set should
|
// A edge in the SLEVEL acceptance set should
|
||||||
// be directed to the next acceptance set. If the
|
// be directed to the next acceptance set. If the
|
||||||
// current transition is also in the next acceptance
|
// current edge is also in the next acceptance
|
||||||
// set, then go to the one after, etc.
|
// set, then go to the one after, etc.
|
||||||
//
|
//
|
||||||
// See Denis Oddoux's PhD thesis for a nice
|
// See Denis Oddoux's PhD thesis for a nice
|
||||||
|
|
@ -419,7 +419,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// Complete (or replace) the acceptance sets of
|
// Complete (or replace) the acceptance sets of
|
||||||
// this link with the acceptance sets common to
|
// this link with the acceptance sets common to
|
||||||
// all transitions leaving the destination state.
|
// all edges leaving the destination state.
|
||||||
if (s_scc == scc)
|
if (s_scc == scc)
|
||||||
acc |= otheracc;
|
acc |= otheracc;
|
||||||
else
|
else
|
||||||
|
|
@ -452,7 +452,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// Consider both the current acceptance
|
// Consider both the current acceptance
|
||||||
// sets, and the acceptance sets common to
|
// sets, and the acceptance sets common to
|
||||||
// the outgoing transitions of the
|
// the outgoing edges of the
|
||||||
// destination state. But don't do
|
// destination state. But don't do
|
||||||
// that if the state is accepting and we
|
// that if the state is accepting and we
|
||||||
// are not skipping levels.
|
// are not skipping levels.
|
||||||
|
|
@ -471,12 +471,12 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
// In case we are building a TBA is_acc has to be
|
// In case we are building a TBA is_acc has to be
|
||||||
// set differently for each transition, and
|
// set differently for each edge, and
|
||||||
// we do not need to stay use final level.
|
// we do not need to stay use final level.
|
||||||
if (!want_sba)
|
if (!want_sba)
|
||||||
{
|
{
|
||||||
is_acc = d.second == order.size();
|
is_acc = d.second == order.size();
|
||||||
if (is_acc) // The transition is accepting
|
if (is_acc) // The edge is accepting
|
||||||
{
|
{
|
||||||
d.second = 0; // Make it go to the first level.
|
d.second = 0; // Make it go to the first level.
|
||||||
// Skip levels as much as possible.
|
// Skip levels as much as possible.
|
||||||
|
|
@ -526,10 +526,10 @@ namespace spot
|
||||||
|
|
||||||
unsigned& t = tr_cache[dest * 2 + is_acc];
|
unsigned& t = tr_cache[dest * 2 + is_acc];
|
||||||
|
|
||||||
if (t == 0) // Create transition.
|
if (t == 0) // Create edge.
|
||||||
t = res->new_acc_transition(src, dest, i.cond, is_acc);
|
t = res->new_acc_edge(src, dest, i.cond, is_acc);
|
||||||
else // Update existing transition.
|
else // Update existing edge.
|
||||||
res->trans_data(t).cond |= i.cond;
|
res->edge_data(t).cond |= i.cond;
|
||||||
}
|
}
|
||||||
tr_cache.clear();
|
tr_cache.clear();
|
||||||
}
|
}
|
||||||
|
|
@ -546,7 +546,7 @@ namespace spot
|
||||||
|
|
||||||
delete m;
|
delete m;
|
||||||
|
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -427,7 +427,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(const twa_graph::trans_storage_t& t, int number)
|
process_link(const twa_graph::edge_storage_t& t, int number)
|
||||||
{
|
{
|
||||||
std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
|
std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
|
||||||
os_ << " " << t.src << " -> " << t.dst;
|
os_ << " " << t.src << " -> " << t.dst;
|
||||||
|
|
|
||||||
|
|
@ -302,7 +302,7 @@ namespace spot
|
||||||
|
|
||||||
// Compute the AP used in the hard way.
|
// Compute the AP used in the hard way.
|
||||||
bdd ap = bddtrue;
|
bdd ap = bddtrue;
|
||||||
for (auto& t: ref->transitions())
|
for (auto& t: ref->edges())
|
||||||
ap &= bdd_support(t.cond);
|
ap &= bdd_support(t.cond);
|
||||||
|
|
||||||
// Count the number of atomic propositions
|
// Count the number of atomic propositions
|
||||||
|
|
@ -679,7 +679,7 @@ namespace spot
|
||||||
&& acc_states.find(t->second.src) != acc_states.end();
|
&& acc_states.find(t->second.src) != acc_states.end();
|
||||||
|
|
||||||
last_aut_trans =
|
last_aut_trans =
|
||||||
a->new_acc_transition(t->second.src, t->second.dst,
|
a->new_acc_edge(t->second.src, t->second.dst,
|
||||||
t->second.cond, accept);
|
t->second.cond, accept);
|
||||||
last_sat_trans = &t->second;
|
last_sat_trans = &t->second;
|
||||||
|
|
||||||
|
|
@ -697,7 +697,7 @@ namespace spot
|
||||||
assert(!state_based);
|
assert(!state_based);
|
||||||
// This assumes that the SAT solvers output
|
// This assumes that the SAT solvers output
|
||||||
// variables in increasing order.
|
// variables in increasing order.
|
||||||
a->trans_data(last_aut_trans).acc = acc;
|
a->edge_data(last_aut_trans).acc = acc;
|
||||||
}
|
}
|
||||||
else if (state_based)
|
else if (state_based)
|
||||||
{
|
{
|
||||||
|
|
@ -733,7 +733,7 @@ namespace spot
|
||||||
else
|
else
|
||||||
dout << -pit.second << "\t¬" << pit.first << "C\n";
|
dout << -pit.second << "\t¬" << pit.first << "C\n";
|
||||||
#endif
|
#endif
|
||||||
a->merge_transitions();
|
a->merge_edges();
|
||||||
return a;
|
return a;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -51,27 +51,27 @@ namespace spot
|
||||||
res->new_states(num_sets * n + 1);
|
res->new_states(num_sets * n + 1);
|
||||||
unsigned sink = res->num_states() - 1;
|
unsigned sink = res->num_states() - 1;
|
||||||
// The sink state has an accepting self-loop.
|
// The sink state has an accepting self-loop.
|
||||||
res->new_acc_transition(sink, sink, bddtrue);
|
res->new_acc_edge(sink, sink, bddtrue);
|
||||||
|
|
||||||
for (unsigned src = 0; src < n; ++src)
|
for (unsigned src = 0; src < n; ++src)
|
||||||
{
|
{
|
||||||
// Keep track of all conditions on transition leaving state
|
// Keep track of all conditions on edge leaving state
|
||||||
// SRC, so we can complete it.
|
// SRC, so we can complete it.
|
||||||
bdd missingcond = bddtrue;
|
bdd missingcond = bddtrue;
|
||||||
for (auto& t: res->out(src))
|
for (auto& t: res->out(src))
|
||||||
{
|
{
|
||||||
if (t.dst >= n) // Ignore transitions we added.
|
if (t.dst >= n) // Ignore edges we added.
|
||||||
break;
|
break;
|
||||||
missingcond -= t.cond;
|
missingcond -= t.cond;
|
||||||
acc_cond::mark_t curacc = t.acc;
|
acc_cond::mark_t curacc = t.acc;
|
||||||
// The original transition must not accept anymore.
|
// The original edge must not accept anymore.
|
||||||
t.acc = 0U;
|
t.acc = 0U;
|
||||||
|
|
||||||
// Transition that were fully accepting are never cloned.
|
// Edge that were fully accepting are never cloned.
|
||||||
if (oldacc.accepting(curacc))
|
if (oldacc.accepting(curacc))
|
||||||
continue;
|
continue;
|
||||||
// Save t.cond and t.dst as the reference to t
|
// Save t.cond and t.dst as the reference to t
|
||||||
// is invalided by calls to new_transition().
|
// is invalided by calls to new_edge().
|
||||||
unsigned dst = t.dst;
|
unsigned dst = t.dst;
|
||||||
bdd cond = t.cond;
|
bdd cond = t.cond;
|
||||||
|
|
||||||
|
|
@ -84,30 +84,30 @@ namespace spot
|
||||||
add += n;
|
add += n;
|
||||||
if (!oldacc.has(curacc, set))
|
if (!oldacc.has(curacc, set))
|
||||||
{
|
{
|
||||||
// Clone the transition
|
// Clone the edge
|
||||||
res->new_acc_transition(src + add, dst + add, cond);
|
res->new_acc_edge(src + add, dst + add, cond);
|
||||||
assert(dst + add < sink);
|
assert(dst + add < sink);
|
||||||
// Using `t' is disallowed from now on as it is a
|
// Using `t' is disallowed from now on as it is a
|
||||||
// reference to a transition that may have been
|
// reference to a edge that may have been
|
||||||
// reallocated.
|
// reallocated.
|
||||||
|
|
||||||
// At least one transition per cycle should have a
|
// At least one edge per cycle should have a
|
||||||
// nondeterministic copy from the original clone.
|
// nondeterministic copy from the original clone.
|
||||||
// We use state numbers to select it, as any cycle
|
// We use state numbers to select it, as any cycle
|
||||||
// is guaranteed to have at least one transition
|
// is guaranteed to have at least one edge
|
||||||
// with dst <= src. FIXME: Computing a feedback
|
// with dst <= src. FIXME: Computing a feedback
|
||||||
// arc set would be better.
|
// arc set would be better.
|
||||||
if (dst <= src)
|
if (dst <= src)
|
||||||
res->new_transition(src, dst + add, cond);
|
res->new_edge(src, dst + add, cond);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
assert(add == num_sets * n);
|
assert(add == num_sets * n);
|
||||||
}
|
}
|
||||||
// Complete the original automaton.
|
// Complete the original automaton.
|
||||||
if (missingcond != bddfalse)
|
if (missingcond != bddfalse)
|
||||||
res->new_transition(src, sink, missingcond);
|
res->new_edge(src, sink, missingcond);
|
||||||
}
|
}
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
res->purge_dead_states();
|
res->purge_dead_states();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
@ -137,7 +137,7 @@ namespace spot
|
||||||
if (si.is_rejecting_scc(scc) && !si.is_trivial(scc))
|
if (si.is_rejecting_scc(scc) && !si.is_trivial(scc))
|
||||||
acc = all_acc;
|
acc = all_acc;
|
||||||
|
|
||||||
// Keep track of all conditions on transition leaving state
|
// Keep track of all conditions on edge leaving state
|
||||||
// SRC, so we can complete it.
|
// SRC, so we can complete it.
|
||||||
bdd missingcond = bddtrue;
|
bdd missingcond = bddtrue;
|
||||||
for (auto& t: res->out(src))
|
for (auto& t: res->out(src))
|
||||||
|
|
@ -151,12 +151,12 @@ namespace spot
|
||||||
if (res->num_states() == sink)
|
if (res->num_states() == sink)
|
||||||
{
|
{
|
||||||
res->new_state();
|
res->new_state();
|
||||||
res->new_acc_transition(sink, sink, bddtrue);
|
res->new_acc_edge(sink, sink, bddtrue);
|
||||||
}
|
}
|
||||||
res->new_transition(src, sink, missingcond);
|
res->new_edge(src, sink, missingcond);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
//res->merge_transitions();
|
//res->merge_edges();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -613,7 +613,7 @@ namespace spot
|
||||||
|
|
||||||
// Compute the AP used in the hard way.
|
// Compute the AP used in the hard way.
|
||||||
bdd ap = bddtrue;
|
bdd ap = bddtrue;
|
||||||
for (auto& t: ref->transitions())
|
for (auto& t: ref->edges())
|
||||||
ap &= bdd_support(t.cond);
|
ap &= bdd_support(t.cond);
|
||||||
|
|
||||||
// Count the number of atomic propositions
|
// Count the number of atomic propositions
|
||||||
|
|
@ -1033,10 +1033,9 @@ namespace spot
|
||||||
acc = i->second;
|
acc = i->second;
|
||||||
}
|
}
|
||||||
|
|
||||||
last_aut_trans = a->new_transition(t->second.src,
|
last_aut_trans = a->new_edge(t->second.src,
|
||||||
t->second.dst,
|
t->second.dst,
|
||||||
t->second.cond,
|
t->second.cond, acc);
|
||||||
acc);
|
|
||||||
last_sat_trans = &t->second;
|
last_sat_trans = &t->second;
|
||||||
|
|
||||||
dout << v << '\t' << t->second << "δ\n";
|
dout << v << '\t' << t->second << "δ\n";
|
||||||
|
|
@ -1058,7 +1057,7 @@ namespace spot
|
||||||
ta->second.dst == last_sat_trans->dst)
|
ta->second.dst == last_sat_trans->dst)
|
||||||
{
|
{
|
||||||
assert(!state_based);
|
assert(!state_based);
|
||||||
auto& v = a->trans_data(last_aut_trans).acc;
|
auto& v = a->edge_data(last_aut_trans).acc;
|
||||||
v |= ta->second.acc;
|
v |= ta->second.acc;
|
||||||
}
|
}
|
||||||
else if (state_based)
|
else if (state_based)
|
||||||
|
|
@ -1076,7 +1075,7 @@ namespace spot
|
||||||
dout << pit.second << '\t' << pit.first << "C\n";
|
dout << pit.second << '\t' << pit.first << "C\n";
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
a->merge_transitions();
|
a->merge_edges();
|
||||||
return a;
|
return a;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -64,7 +64,7 @@ namespace spot
|
||||||
const state*, int out,
|
const state*, int out,
|
||||||
const twa_succ_iterator* si)
|
const twa_succ_iterator* si)
|
||||||
{
|
{
|
||||||
out_->new_transition
|
out_->new_edge
|
||||||
(in - 1, out - 1, si->current_condition(),
|
(in - 1, out - 1, si->current_condition(),
|
||||||
si->current_acceptance_conditions());
|
si->current_acceptance_conditions());
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
|
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||||
// et Développement de l'Epita (LRDE).
|
// Recherche et Développement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
// et Marie Curie.
|
// et Marie Curie.
|
||||||
|
|
@ -369,7 +369,7 @@ namespace spot
|
||||||
p.first->second = res->new_state();
|
p.first->second = res->new_state();
|
||||||
dst = p.first->second;
|
dst = p.first->second;
|
||||||
|
|
||||||
res->new_transition(src, dst, label, acc);
|
res->new_edge(src, dst, label, acc);
|
||||||
src = dst;
|
src = dst;
|
||||||
|
|
||||||
// Sum acceptance conditions.
|
// Sum acceptance conditions.
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,7 @@ namespace spot
|
||||||
auto prod = product(clean_a, clean_a);
|
auto prod = product(clean_a, clean_a);
|
||||||
auto clean_p = scc_filter_states(prod);
|
auto clean_p = scc_filter_states(prod);
|
||||||
return clean_a->num_states() == clean_p->num_states()
|
return clean_a->num_states() == clean_p->num_states()
|
||||||
&& clean_a->num_transitions() == clean_p->num_transitions();
|
&& clean_a->num_edges() == clean_p->num_edges();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool check_unambiguous(const twa_graph_ptr& aut)
|
bool check_unambiguous(const twa_graph_ptr& aut)
|
||||||
|
|
|
||||||
|
|
@ -43,7 +43,7 @@ namespace spot
|
||||||
acc_cond::mark_t acc = 0U;
|
acc_cond::mark_t acc = 0U;
|
||||||
for (;;)
|
for (;;)
|
||||||
{
|
{
|
||||||
acc |= aut_->trans_storage(i->succ).acc;
|
acc |= aut_->edge_storage(i->succ).acc;
|
||||||
if (i->s == start)
|
if (i->s == start)
|
||||||
break;
|
break;
|
||||||
++i;
|
++i;
|
||||||
|
|
|
||||||
|
|
@ -1160,7 +1160,7 @@ namespace spot
|
||||||
dest->destroy();
|
dest->destroy();
|
||||||
}
|
}
|
||||||
|
|
||||||
namer->new_transition(now, dest, label);
|
namer->new_edge(now, dest, label);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -2553,7 +2553,7 @@ namespace spot
|
||||||
namer->new_state(t.dest);
|
namer->new_state(t.dest);
|
||||||
}
|
}
|
||||||
|
|
||||||
namer->new_transition(now, t.dest, t.cond,
|
namer->new_edge(now, t.dest, t.cond,
|
||||||
d.bdd_to_mark(t.prom));
|
d.bdd_to_mark(t.prom));
|
||||||
if (seen)
|
if (seen)
|
||||||
t.dest->destroy();
|
t.dest->destroy();
|
||||||
|
|
|
||||||
|
|
@ -25,7 +25,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Clone and mask an automaton.
|
/// \brief Clone and mask an automaton.
|
||||||
///
|
///
|
||||||
/// Copy the transition of the automaton \a old, into the automaton
|
/// Copy the edge of the automaton \a old, into the automaton
|
||||||
/// \a cpy, creating new states at the same time. The argument \a
|
/// \a cpy, creating new states at the same time. The argument \a
|
||||||
/// trans should behave as a function with the following prototype:
|
/// trans should behave as a function with the following prototype:
|
||||||
/// <code>
|
/// <code>
|
||||||
|
|
@ -33,9 +33,9 @@ namespace spot
|
||||||
/// unsigned dst)
|
/// unsigned dst)
|
||||||
/// </code>
|
/// </code>
|
||||||
/// It can modify either the condition or the acceptance sets of
|
/// It can modify either the condition or the acceptance sets of
|
||||||
/// the transitions. Set the condition to bddfalse to remove it
|
/// the edges. Set the condition to bddfalse to remove it
|
||||||
/// (this will also remove the destination state and its descendants
|
/// (this will also remove the destination state and its descendants
|
||||||
/// if they are not reachable by another transition).
|
/// if they are not reachable by another edge).
|
||||||
/// \param init The optional new initial state.
|
/// \param init The optional new initial state.
|
||||||
|
|
||||||
template<typename Trans>
|
template<typename Trans>
|
||||||
|
|
@ -75,14 +75,14 @@ namespace spot
|
||||||
trans(t.src, cond, acc, t.dst);
|
trans(t.src, cond, acc, t.dst);
|
||||||
|
|
||||||
if (cond != bddfalse)
|
if (cond != bddfalse)
|
||||||
cpy->new_transition(new_src,
|
cpy->new_edge(new_src,
|
||||||
new_state(t.dst),
|
new_state(t.dst),
|
||||||
cond, acc);
|
cond, acc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Copy an automaton and update each transitions.
|
/// \brief Copy an automaton and update each edge.
|
||||||
///
|
///
|
||||||
/// Copy the states of the automaton \a old, into the automaton
|
/// Copy the states of the automaton \a old, into the automaton
|
||||||
/// \a cpy. Each state in \a cpy will have the same id as the ones in \a old.
|
/// \a cpy. Each state in \a cpy will have the same id as the ones in \a old.
|
||||||
|
|
@ -93,7 +93,7 @@ namespace spot
|
||||||
/// unsigned dst)
|
/// unsigned dst)
|
||||||
/// </code>
|
/// </code>
|
||||||
/// It can modify either the condition or the acceptance sets of
|
/// It can modify either the condition or the acceptance sets of
|
||||||
/// the transitions. Set the condition to bddfalse to remove it. Note that
|
/// the edges. Set the condition to bddfalse to remove it. Note that
|
||||||
/// all transtions will be processed.
|
/// all transtions will be processed.
|
||||||
/// \param init The optional new initial state.
|
/// \param init The optional new initial state.
|
||||||
template<typename Trans>
|
template<typename Trans>
|
||||||
|
|
@ -105,7 +105,7 @@ namespace spot
|
||||||
cpy->new_states(old->num_states());
|
cpy->new_states(old->num_states());
|
||||||
cpy->set_init_state(init);
|
cpy->set_init_state(init);
|
||||||
|
|
||||||
for (auto& t: old->transitions())
|
for (auto& t: old->edges())
|
||||||
{
|
{
|
||||||
bdd cond = t.cond;
|
bdd cond = t.cond;
|
||||||
acc_cond::mark_t acc = t.acc;
|
acc_cond::mark_t acc = t.acc;
|
||||||
|
|
@ -114,7 +114,7 @@ namespace spot
|
||||||
// equivilent in old and cpy.
|
// equivilent in old and cpy.
|
||||||
assert(t.src < cpy->num_states() && t.dst < cpy->num_states());
|
assert(t.src < cpy->num_states() && t.dst < cpy->num_states());
|
||||||
if (cond != bddfalse)
|
if (cond != bddfalse)
|
||||||
cpy->new_transition(t.src, t.dst, cond, acc);
|
cpy->new_edge(t.src, t.dst, cond, acc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -133,7 +133,7 @@ namespace spot
|
||||||
transform_copy(old, cpy, trans, old->get_init_state_number());
|
transform_copy(old, cpy, trans, old->get_init_state_number());
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Remove all transitions that are in some given acceptance sets.
|
/// \brief Remove all edges that are in some given acceptance sets.
|
||||||
SPOT_API
|
SPOT_API
|
||||||
twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in,
|
twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in,
|
||||||
acc_cond::mark_t to_remove);
|
acc_cond::mark_t to_remove);
|
||||||
|
|
|
||||||
|
|
@ -160,11 +160,11 @@ namespace spot
|
||||||
dst->destroy();
|
dst->destroy();
|
||||||
if (i == state_num.end()) // Ignore useless destinations.
|
if (i == state_num.end()) // Ignore useless destinations.
|
||||||
continue;
|
continue;
|
||||||
res->new_acc_transition(src_num, i->second,
|
res->new_acc_edge(src_num, i->second,
|
||||||
succit->current_condition(), accepting);
|
succit->current_condition(), accepting);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
if (res->num_states() > 0)
|
if (res->num_states() > 0)
|
||||||
{
|
{
|
||||||
const state* init_state = a->get_init_state();
|
const state* init_state = a->get_init_state();
|
||||||
|
|
@ -236,11 +236,11 @@ namespace spot
|
||||||
int n;
|
int n;
|
||||||
for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
|
for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i)
|
||||||
{
|
{
|
||||||
loop_a->new_transition(n - 1, n, i->label);
|
loop_a->new_edge(n - 1, n, i->label);
|
||||||
i->s->destroy();
|
i->s->destroy();
|
||||||
}
|
}
|
||||||
assert(i != loop.end());
|
assert(i != loop.end());
|
||||||
loop_a->new_transition(n - 1, 0, i->label);
|
loop_a->new_edge(n - 1, 0, i->label);
|
||||||
i->s->destroy();
|
i->s->destroy();
|
||||||
assert(++i == loop.end());
|
assert(++i == loop.end());
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -44,7 +44,7 @@ namespace spot
|
||||||
if (a->num_sets() == 0)
|
if (a->num_sets() == 0)
|
||||||
{
|
{
|
||||||
auto m = a->set_buchi();
|
auto m = a->set_buchi();
|
||||||
for (auto& t: a->transitions())
|
for (auto& t: a->edges())
|
||||||
t.acc = m;
|
t.acc = m;
|
||||||
}
|
}
|
||||||
return a;
|
return a;
|
||||||
|
|
|
||||||
|
|
@ -93,7 +93,7 @@ namespace spot
|
||||||
typedef std::set<bdd, bdd_less_than> sup_map;
|
typedef std::set<bdd, bdd_less_than> sup_map;
|
||||||
sup_map sup;
|
sup_map sup;
|
||||||
// Record occurrences of all guards
|
// Record occurrences of all guards
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
sup.emplace(t.cond);
|
sup.emplace(t.cond);
|
||||||
for (auto& i: sup)
|
for (auto& i: sup)
|
||||||
allap &= bdd_support(i);
|
allap &= bdd_support(i);
|
||||||
|
|
@ -206,14 +206,14 @@ namespace spot
|
||||||
assert(pm.map_.size() == dst_num);
|
assert(pm.map_.size() == dst_num);
|
||||||
pm.map_.emplace_back(std::move(ps));
|
pm.map_.emplace_back(std::move(ps));
|
||||||
}
|
}
|
||||||
res->new_transition(src_num, dst_num, num2bdd[c]);
|
res->new_edge(src_num, dst_num, num2bdd[c]);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
for (auto v: toclean)
|
for (auto v: toclean)
|
||||||
delete v;
|
delete v;
|
||||||
if (merge)
|
if (merge)
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -232,15 +232,15 @@ namespace spot
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
typedef dfs_stack::const_iterator cycle_iter;
|
typedef dfs_stack::const_iterator cycle_iter;
|
||||||
typedef twa_graph_trans_data trans;
|
typedef twa_graph_edge_data trans;
|
||||||
typedef std::set<trans*> trans_set;
|
typedef std::set<trans*> edge_set;
|
||||||
typedef std::vector<trans_set> set_set;
|
typedef std::vector<edge_set> set_set;
|
||||||
protected:
|
protected:
|
||||||
const_twa_graph_ptr ref_;
|
const_twa_graph_ptr ref_;
|
||||||
power_map& refmap_;
|
power_map& refmap_;
|
||||||
trans_set reject_; // set of rejecting transitions
|
edge_set reject_; // set of rejecting edges
|
||||||
set_set accept_; // set of cycles that are accepting
|
set_set accept_; // set of cycles that are accepting
|
||||||
trans_set all_; // all non rejecting transitions
|
edge_set all_; // all non rejecting edges
|
||||||
unsigned threshold_; // maximum count of enumerated cycles
|
unsigned threshold_; // maximum count of enumerated cycles
|
||||||
unsigned cycles_left_; // count of cycles left to explore
|
unsigned cycles_left_; // count of cycles left to explore
|
||||||
|
|
||||||
|
|
@ -277,7 +277,7 @@ namespace spot
|
||||||
return threshold_ != 0 && cycles_left_ == 0;
|
return threshold_ != 0 && cycles_left_ == 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const
|
bool is_cycle_accepting(cycle_iter begin, edge_set& ts) const
|
||||||
{
|
{
|
||||||
auto a = std::const_pointer_cast<twa_graph>(aut_);
|
auto a = std::const_pointer_cast<twa_graph>(aut_);
|
||||||
|
|
||||||
|
|
@ -289,8 +289,8 @@ namespace spot
|
||||||
cycle_iter i;
|
cycle_iter i;
|
||||||
for (n = 1, i = begin; n <= loop_size; ++n, ++i)
|
for (n = 1, i = begin; n <= loop_size; ++n, ++i)
|
||||||
{
|
{
|
||||||
trans* t = &a->trans_data(i->succ);
|
trans* t = &a->edge_data(i->succ);
|
||||||
loop_a->new_transition(n - 1, n % loop_size, t->cond);
|
loop_a->new_edge(n - 1, n % loop_size, t->cond);
|
||||||
if (reject_.find(t) == reject_.end())
|
if (reject_.find(t) == reject_.end())
|
||||||
ts.insert(t);
|
ts.insert(t);
|
||||||
}
|
}
|
||||||
|
|
@ -318,7 +318,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
print_set(std::ostream& o, const trans_set& s) const
|
print_set(std::ostream& o, const edge_set& s) const
|
||||||
{
|
{
|
||||||
o << "{ ";
|
o << "{ ";
|
||||||
for (auto i: s)
|
for (auto i: s)
|
||||||
|
|
@ -333,7 +333,7 @@ namespace spot
|
||||||
cycle_iter i = dfs_.begin();
|
cycle_iter i = dfs_.begin();
|
||||||
while (i->s != start)
|
while (i->s != start)
|
||||||
++i;
|
++i;
|
||||||
trans_set ts;
|
edge_set ts;
|
||||||
bool is_acc = is_cycle_accepting(i, ts);
|
bool is_acc = is_cycle_accepting(i, ts);
|
||||||
do
|
do
|
||||||
++i;
|
++i;
|
||||||
|
|
@ -387,7 +387,7 @@ namespace spot
|
||||||
unsigned threshold_states, unsigned threshold_cycles)
|
unsigned threshold_states, unsigned threshold_cycles)
|
||||||
{
|
{
|
||||||
power_map pm;
|
power_map pm;
|
||||||
// Do not merge transitions in the deterministic automaton. If we
|
// Do not merge edges in the deterministic automaton. If we
|
||||||
// add two self-loops labeled by "a" and "!a", we do not want
|
// add two self-loops labeled by "a" and "!a", we do not want
|
||||||
// these to be merged as "1" before the acceptance has been fixed.
|
// these to be merged as "1" before the acceptance has been fixed.
|
||||||
auto det = tgba_powerset(aut, pm, false);
|
auto det = tgba_powerset(aut, pm, false);
|
||||||
|
|
@ -397,7 +397,7 @@ namespace spot
|
||||||
return nullptr;
|
return nullptr;
|
||||||
if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
|
if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
|
||||||
return nullptr;
|
return nullptr;
|
||||||
det->merge_transitions();
|
det->merge_edges();
|
||||||
return det;
|
return det;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -92,7 +92,7 @@ namespace spot
|
||||||
if (cond == bddfalse)
|
if (cond == bddfalse)
|
||||||
continue;
|
continue;
|
||||||
auto dst = new_state(l.dst, r.dst);
|
auto dst = new_state(l.dst, r.dst);
|
||||||
res->new_transition(top.second, dst, cond,
|
res->new_edge(top.second, dst, cond,
|
||||||
res->acc().join(left->acc(), l.acc,
|
res->acc().join(left->acc(), l.acc,
|
||||||
right->acc(), r.acc));
|
right->acc(), r.acc));
|
||||||
// If right is deterministic, we can abort immediately!
|
// If right is deterministic, we can abort immediately!
|
||||||
|
|
|
||||||
|
|
@ -184,7 +184,7 @@ namespace spot
|
||||||
labels = random_deterministic_labels(props, props_n, nsucc);
|
labels = random_deterministic_labels(props, props_n, nsucc);
|
||||||
|
|
||||||
// if nsucc > 2^props_n, we cannot produce nsucc deterministic
|
// if nsucc > 2^props_n, we cannot produce nsucc deterministic
|
||||||
// transitions so we set it to labels.size()
|
// edges so we set it to labels.size()
|
||||||
nsucc = labels.size();
|
nsucc = labels.size();
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
@ -214,7 +214,7 @@ namespace spot
|
||||||
std::advance(i, index);
|
std::advance(i, index);
|
||||||
|
|
||||||
// Link it from src.
|
// Link it from src.
|
||||||
res->new_transition(src, *i, l, m);
|
res->new_edge(src, *i, l, m);
|
||||||
nodes_to_process.insert(*i);
|
nodes_to_process.insert(*i);
|
||||||
unreachable_nodes.erase(*i);
|
unreachable_nodes.erase(*i);
|
||||||
break;
|
break;
|
||||||
|
|
@ -229,7 +229,7 @@ namespace spot
|
||||||
state_randomizer[index] = state_randomizer[possibilities];
|
state_randomizer[index] = state_randomizer[possibilities];
|
||||||
state_randomizer[possibilities] = dst;
|
state_randomizer[possibilities] = dst;
|
||||||
|
|
||||||
res->new_transition(src, dst, l, m);
|
res->new_edge(src, dst, l, m);
|
||||||
auto j = unreachable_nodes.find(dst);
|
auto j = unreachable_nodes.find(dst);
|
||||||
if (j != unreachable_nodes.end())
|
if (j != unreachable_nodes.end())
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -27,9 +27,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
void
|
void
|
||||||
randomize(twa_graph_ptr& aut, bool randomize_states,
|
randomize(twa_graph_ptr& aut, bool randomize_states,
|
||||||
bool randomize_transitions)
|
bool randomize_edges)
|
||||||
{
|
{
|
||||||
if (!randomize_states && !randomize_transitions)
|
if (!randomize_states && !randomize_edges)
|
||||||
return;
|
return;
|
||||||
auto& g = aut->get_graph();
|
auto& g = aut->get_graph();
|
||||||
if (randomize_states)
|
if (randomize_states)
|
||||||
|
|
@ -51,16 +51,16 @@ namespace spot
|
||||||
aut->set_named_prop("state-names", nn);
|
aut->set_named_prop("state-names", nn);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (randomize_transitions)
|
if (randomize_edges)
|
||||||
{
|
{
|
||||||
g.remove_dead_transitions_();
|
g.remove_dead_edges_();
|
||||||
auto& v = g.transition_vector();
|
auto& v = g.edge_vector();
|
||||||
mrandom_shuffle(v.begin() + 1, v.end());
|
mrandom_shuffle(v.begin() + 1, v.end());
|
||||||
}
|
}
|
||||||
|
|
||||||
typedef twa_graph::graph_t::trans_storage_t tr_t;
|
typedef twa_graph::graph_t::edge_storage_t tr_t;
|
||||||
g.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
|
g.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
|
||||||
{ return lhs.src < rhs.src; });
|
{ return lhs.src < rhs.src; });
|
||||||
g.chain_transitions_();
|
g.chain_edges_();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014 Laboratoire de Recherche et
|
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -25,10 +25,10 @@ namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Randomize a TGBA
|
/// \brief Randomize a TGBA
|
||||||
///
|
///
|
||||||
/// Make a random permutation of the state, and of the transitions
|
/// Make a random permutation of the state, and of the edges
|
||||||
/// leaving this state.
|
/// leaving this state.
|
||||||
SPOT_API void
|
SPOT_API void
|
||||||
randomize(twa_graph_ptr& aut,
|
randomize(twa_graph_ptr& aut,
|
||||||
bool randomize_states = true,
|
bool randomize_states = true,
|
||||||
bool randomize_transitions = true);
|
bool randomize_edges = true);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -35,7 +35,7 @@ namespace spot
|
||||||
bdd_setpair(pairs, oldv, newv);
|
bdd_setpair(pairs, oldv, newv);
|
||||||
vars.push_back(oldv);
|
vars.push_back(oldv);
|
||||||
}
|
}
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
t.cond = bdd_replace(t.cond, pairs);
|
t.cond = bdd_replace(t.cond, pairs);
|
||||||
for (auto v: vars)
|
for (auto v: vars)
|
||||||
d->unregister_variable(v, aut);
|
d->unregister_variable(v, aut);
|
||||||
|
|
|
||||||
|
|
@ -289,8 +289,7 @@ namespace spot
|
||||||
// Create the main copy
|
// Create the main copy
|
||||||
for (auto s: states)
|
for (auto s: states)
|
||||||
for (auto& t: aut->out(s))
|
for (auto& t: aut->out(s))
|
||||||
res->new_transition(s, t.dst, t.cond,
|
res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add);
|
||||||
(t.acc & main_sets) | main_add);
|
|
||||||
|
|
||||||
if (si.is_rejecting_scc(n))
|
if (si.is_rejecting_scc(n))
|
||||||
continue;
|
continue;
|
||||||
|
|
@ -314,16 +313,16 @@ namespace spot
|
||||||
if ((t.acc & r) || si.scc_of(t.dst) != n)
|
if ((t.acc & r) || si.scc_of(t.dst) != n)
|
||||||
continue;
|
continue;
|
||||||
auto nd = state_map[t.dst];
|
auto nd = state_map[t.dst];
|
||||||
res->new_transition(ns, nd, t.cond, (t.acc & k) | a);
|
res->new_edge(ns, nd, t.cond, (t.acc & k) | a);
|
||||||
// We need only one non-deterministic jump per
|
// We need only one non-deterministic jump per
|
||||||
// cycle. As an approximation, we only do
|
// cycle. As an approximation, we only do
|
||||||
// them on back-links.
|
// them on back-links.
|
||||||
//
|
//
|
||||||
// The acceptance marks on these transition
|
// The acceptance marks on these edge
|
||||||
// are useless, but we keep them to preserve
|
// are useless, but we keep them to preserve
|
||||||
// state-based acceptance if any.
|
// state-based acceptance if any.
|
||||||
if (t.dst <= s)
|
if (t.dst <= s)
|
||||||
res->new_transition(s, nd, t.cond,
|
res->new_edge(s, nd, t.cond,
|
||||||
(t.acc & main_sets) | main_add);
|
(t.acc & main_sets) | main_add);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -46,7 +46,7 @@ namespace spot
|
||||||
result = false;
|
result = false;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
// The state should have only one transition that is a
|
// The state should have only one edge that is a
|
||||||
// self-loop labelled by true.
|
// self-loop labelled by true.
|
||||||
auto src = st.front();
|
auto src = st.front();
|
||||||
auto out = aut->out(src);
|
auto out = aut->out(src);
|
||||||
|
|
@ -69,7 +69,7 @@ namespace spot
|
||||||
throw std::runtime_error
|
throw std::runtime_error
|
||||||
("is_safety_mwdba() should be called on a Buchi automaton");
|
("is_safety_mwdba() should be called on a Buchi automaton");
|
||||||
|
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
if (!aut->acc().accepting(t.acc))
|
if (!aut->acc().accepting(t.acc))
|
||||||
return false;
|
return false;
|
||||||
return true;
|
return true;
|
||||||
|
|
|
||||||
|
|
@ -54,11 +54,11 @@ namespace spot
|
||||||
return p.first->second;
|
return p.first->second;
|
||||||
};
|
};
|
||||||
|
|
||||||
// Find any transition going into the initial state, and use its
|
// Find any edge going into the initial state, and use its
|
||||||
// acceptance as mark.
|
// acceptance as mark.
|
||||||
acc_cond::mark_t init_acc = 0U;
|
acc_cond::mark_t init_acc = 0U;
|
||||||
unsigned old_init = old->get_init_state_number();
|
unsigned old_init = old->get_init_state_number();
|
||||||
for (auto& t: old->transitions())
|
for (auto& t: old->edges())
|
||||||
if (t.dst == old_init)
|
if (t.dst == old_init)
|
||||||
{
|
{
|
||||||
init_acc = t.acc;
|
init_acc = t.acc;
|
||||||
|
|
@ -71,7 +71,7 @@ namespace spot
|
||||||
auto one = todo.back();
|
auto one = todo.back();
|
||||||
todo.pop_back();
|
todo.pop_back();
|
||||||
for (auto& t: old->out(one.first.first))
|
for (auto& t: old->out(one.first.first))
|
||||||
res->new_transition(one.second,
|
res->new_edge(one.second,
|
||||||
new_state(t.dst, t.acc),
|
new_state(t.dst, t.acc),
|
||||||
t.cond,
|
t.cond,
|
||||||
one.first.second);
|
one.first.second);
|
||||||
|
|
|
||||||
|
|
@ -36,7 +36,7 @@ namespace spot
|
||||||
// state(src) return true iff s should be kept
|
// state(src) return true iff s should be kept
|
||||||
// trans(src, dst, cond, acc) returns a triplet
|
// trans(src, dst, cond, acc) returns a triplet
|
||||||
// (keep, cond2, acc2) where keep is a Boolean stating if the
|
// (keep, cond2, acc2) where keep is a Boolean stating if the
|
||||||
// transition should be kept, and cond2/acc2
|
// edge should be kept, and cond2/acc2
|
||||||
// give replacement values for cond/acc
|
// give replacement values for cond/acc
|
||||||
struct id_filter
|
struct id_filter
|
||||||
{
|
{
|
||||||
|
|
@ -57,7 +57,7 @@ namespace spot
|
||||||
out->copy_acceptance_of(this->si->get_aut());
|
out->copy_acceptance_of(this->si->get_aut());
|
||||||
}
|
}
|
||||||
|
|
||||||
// Accept all transitions, unmodified
|
// Accept all edges, unmodified
|
||||||
filtered_trans trans(unsigned, unsigned, bdd cond, acc_cond::mark_t acc)
|
filtered_trans trans(unsigned, unsigned, bdd cond, acc_cond::mark_t acc)
|
||||||
{
|
{
|
||||||
return filtered_trans{true, cond, acc};
|
return filtered_trans{true, cond, acc};
|
||||||
|
|
@ -124,7 +124,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
// Remove acceptance conditions from all transitions outside of
|
// Remove acceptance conditions from all edges outside of
|
||||||
// non-accepting SCCs.
|
// non-accepting SCCs.
|
||||||
template <class next_filter = id_filter>
|
template <class next_filter = id_filter>
|
||||||
struct acc_filter_all: next_filter
|
struct acc_filter_all: next_filter
|
||||||
|
|
@ -145,7 +145,7 @@ namespace spot
|
||||||
if (keep)
|
if (keep)
|
||||||
{
|
{
|
||||||
unsigned u = this->si->scc_of(src);
|
unsigned u = this->si->scc_of(src);
|
||||||
// If the transition is between two SCCs, or in a
|
// If the edge is between two SCCs, or in a
|
||||||
// non-accepting SCC. Remove the acceptance sets.
|
// non-accepting SCC. Remove the acceptance sets.
|
||||||
if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst))
|
if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst))
|
||||||
acc = 0U;
|
acc = 0U;
|
||||||
|
|
@ -155,7 +155,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
// Remove acceptance conditions from all transitions whose
|
// Remove acceptance conditions from all edges whose
|
||||||
// destination is not an accepting SCCs.
|
// destination is not an accepting SCCs.
|
||||||
template <class next_filter = id_filter>
|
template <class next_filter = id_filter>
|
||||||
struct acc_filter_some: next_filter
|
struct acc_filter_some: next_filter
|
||||||
|
|
@ -296,7 +296,7 @@ namespace spot
|
||||||
std::tie(want, cond, acc) =
|
std::tie(want, cond, acc) =
|
||||||
filter.trans(isrc, t.dst, t.cond, t.acc);
|
filter.trans(isrc, t.dst, t.cond, t.acc);
|
||||||
if (want)
|
if (want)
|
||||||
filtered->new_transition(osrc, odst, cond, acc);
|
filtered->new_edge(osrc, odst, cond, acc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (!given_si)
|
if (!given_si)
|
||||||
|
|
@ -346,7 +346,7 @@ namespace spot
|
||||||
res = scc_filter_apply<state_filter
|
res = scc_filter_apply<state_filter
|
||||||
<acc_filter_some<>>>(aut, given_si);
|
<acc_filter_some<>>>(aut, given_si);
|
||||||
}
|
}
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
res->prop_copy(aut,
|
res->prop_copy(aut,
|
||||||
{ false, // state-based acceptance is not preserved
|
{ false, // state-based acceptance is not preserved
|
||||||
true,
|
true,
|
||||||
|
|
@ -378,7 +378,7 @@ namespace spot
|
||||||
suspvars,
|
suspvars,
|
||||||
ignoredvars,
|
ignoredvars,
|
||||||
early_susp);
|
early_susp);
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
res->prop_copy(aut,
|
res->prop_copy(aut,
|
||||||
{ false, // state-based acceptance is not preserved
|
{ false, // state-based acceptance is not preserved
|
||||||
true,
|
true,
|
||||||
|
|
|
||||||
|
|
@ -84,8 +84,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Fix the transitions
|
// Fix the edges
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->edges())
|
||||||
{
|
{
|
||||||
if ((t.acc & common) == 0U)
|
if ((t.acc & common) == 0U)
|
||||||
continue;
|
continue;
|
||||||
|
|
|
||||||
|
|
@ -38,12 +38,12 @@
|
||||||
// the format of the acceptance condition, it doesn't allow easy
|
// the format of the acceptance condition, it doesn't allow easy
|
||||||
// simplification. Instead of encoding them as: "a!b!c + !ab!c", we
|
// simplification. Instead of encoding them as: "a!b!c + !ab!c", we
|
||||||
// use them as: "ab". We complement them because we want a
|
// use them as: "ab". We complement them because we want a
|
||||||
// simplification if the condition of the transition A implies the
|
// simplification if the condition of the edge A implies the
|
||||||
// transition of B, and if the acceptance condition of A is included
|
// edge of B, and if the acceptance condition of A is included
|
||||||
// in the acceptance condition of B. To let the bdd makes the job, we
|
// in the acceptance condition of B. To let the bdd makes the job, we
|
||||||
// revert them.
|
// revert them.
|
||||||
|
|
||||||
// Then, to check if a transition i-dominates another, we'll use the bdd:
|
// Then, to check if a edge i-dominates another, we'll use the bdd:
|
||||||
// "sig(transA) = cond(trans) & acc(trans) & implied(class(trans->state))"
|
// "sig(transA) = cond(trans) & acc(trans) & implied(class(trans->state))"
|
||||||
// Idem for sig(transB). The 'implied'
|
// Idem for sig(transB). The 'implied'
|
||||||
// (represented by a hash table 'relation_' in the implementation) is
|
// (represented by a hash table 'relation_' in the implementation) is
|
||||||
|
|
@ -65,8 +65,8 @@
|
||||||
// 3. Rename the class (to actualize the name in the previous_class and
|
// 3. Rename the class (to actualize the name in the previous_class and
|
||||||
// in relation_).
|
// in relation_).
|
||||||
// 4. Building an automaton with the result, with the condition:
|
// 4. Building an automaton with the result, with the condition:
|
||||||
// "a transition in the original automaton appears in the simulated one
|
// "a edge in the original automaton appears in the simulated one
|
||||||
// iff this transition is included in the set of i-maximal neighbour."
|
// iff this edge is included in the set of i-maximal neighbour."
|
||||||
// This function is `build_output'.
|
// This function is `build_output'.
|
||||||
// The automaton simulated is recomplemented to come back to its initial
|
// The automaton simulated is recomplemented to come back to its initial
|
||||||
// state when the object Simulation is destroyed.
|
// state when the object Simulation is destroyed.
|
||||||
|
|
@ -96,13 +96,13 @@ namespace spot
|
||||||
struct automaton_size
|
struct automaton_size
|
||||||
{
|
{
|
||||||
automaton_size()
|
automaton_size()
|
||||||
: transitions(0),
|
: edges(0),
|
||||||
states(0)
|
states(0)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
automaton_size(const twa_graph_ptr& a)
|
automaton_size(const twa_graph_ptr& a)
|
||||||
: transitions(a->num_transitions()),
|
: edges(a->num_edges()),
|
||||||
states(a->num_states())
|
states(a->num_states())
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -110,12 +110,12 @@ namespace spot
|
||||||
void set_size(const twa_graph_ptr& a)
|
void set_size(const twa_graph_ptr& a)
|
||||||
{
|
{
|
||||||
states = a->num_states();
|
states = a->num_states();
|
||||||
transitions = a->num_transitions();
|
edges = a->num_edges();
|
||||||
}
|
}
|
||||||
|
|
||||||
inline bool operator!=(const automaton_size& r)
|
inline bool operator!=(const automaton_size& r)
|
||||||
{
|
{
|
||||||
return transitions != r.transitions || states != r.states;
|
return edges != r.edges || states != r.states;
|
||||||
}
|
}
|
||||||
|
|
||||||
inline bool operator<(const automaton_size& r)
|
inline bool operator<(const automaton_size& r)
|
||||||
|
|
@ -125,9 +125,9 @@ namespace spot
|
||||||
if (states > r.states)
|
if (states > r.states)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
if (transitions < r.transitions)
|
if (edges < r.edges)
|
||||||
return true;
|
return true;
|
||||||
if (transitions > r.transitions)
|
if (edges > r.edges)
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
return false;
|
return false;
|
||||||
|
|
@ -140,15 +140,15 @@ namespace spot
|
||||||
if (states > r.states)
|
if (states > r.states)
|
||||||
return true;
|
return true;
|
||||||
|
|
||||||
if (transitions < r.transitions)
|
if (edges < r.edges)
|
||||||
return false;
|
return false;
|
||||||
if (transitions > r.transitions)
|
if (edges > r.edges)
|
||||||
return true;
|
return true;
|
||||||
|
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
int transitions;
|
int edges;
|
||||||
int states;
|
int states;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
@ -207,7 +207,7 @@ namespace spot
|
||||||
all_inf_ = all_inf;
|
all_inf_ = all_inf;
|
||||||
|
|
||||||
// Replace all the acceptance conditions by their complements.
|
// Replace all the acceptance conditions by their complements.
|
||||||
// (In the case of Cosimulation, we also flip the transitions.)
|
// (In the case of Cosimulation, we also flip the edges.)
|
||||||
if (Cosimulation)
|
if (Cosimulation)
|
||||||
{
|
{
|
||||||
a_ = make_twa_graph(in->get_dict());
|
a_ = make_twa_graph(in->get_dict());
|
||||||
|
|
@ -239,7 +239,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
acc = t.acc ^ all_inf;
|
acc = t.acc ^ all_inf;
|
||||||
}
|
}
|
||||||
a_->new_transition(t.dst, s, t.cond, acc);
|
a_->new_edge(t.dst, s, t.cond, acc);
|
||||||
}
|
}
|
||||||
a_->set_init_state(init_state_number);
|
a_->set_init_state(init_state_number);
|
||||||
}
|
}
|
||||||
|
|
@ -247,7 +247,7 @@ namespace spot
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
a_ = make_twa_graph(in, twa::prop_set::all());
|
a_ = make_twa_graph(in, twa::prop_set::all());
|
||||||
for (auto& t: a_->transitions())
|
for (auto& t: a_->edges())
|
||||||
t.acc ^= all_inf;
|
t.acc ^= all_inf;
|
||||||
}
|
}
|
||||||
assert(a_->num_states() == size_a_);
|
assert(a_->num_states() == size_a_);
|
||||||
|
|
@ -309,11 +309,11 @@ namespace spot
|
||||||
for (auto& p: bdd_lstate_)
|
for (auto& p: bdd_lstate_)
|
||||||
{
|
{
|
||||||
// If the signature of a state is bddfalse (no
|
// If the signature of a state is bddfalse (no
|
||||||
// transitions) the class of this state is bddfalse
|
// edges) the class of this state is bddfalse
|
||||||
// instead of an anonymous variable. It allows
|
// instead of an anonymous variable. It allows
|
||||||
// simplifications in the signature by removing a
|
// simplifications in the signature by removing a
|
||||||
// transition which has as a destination a state with
|
// edge which has as a destination a state with
|
||||||
// no outgoing transition.
|
// no outgoing edge.
|
||||||
if (p.first == bddfalse)
|
if (p.first == bddfalse)
|
||||||
for (auto s: p.second)
|
for (auto s: p.second)
|
||||||
previous_class_[s] = bddfalse;
|
previous_class_[s] = bddfalse;
|
||||||
|
|
@ -360,7 +360,7 @@ namespace spot
|
||||||
bdd acc = mark_to_bdd(t.acc);
|
bdd acc = mark_to_bdd(t.acc);
|
||||||
|
|
||||||
// to_add is a conjunction of the acceptance condition,
|
// to_add is a conjunction of the acceptance condition,
|
||||||
// the label of the transition and the class of the
|
// the label of the edge and the class of the
|
||||||
// destination and all the class it implies.
|
// destination and all the class it implies.
|
||||||
bdd to_add = acc & t.cond & relation_[previous_class_[t.dst]];
|
bdd to_add = acc & t.cond & relation_[previous_class_[t.dst]];
|
||||||
|
|
||||||
|
|
@ -426,11 +426,11 @@ namespace spot
|
||||||
for (auto& p: bdd_lstate_)
|
for (auto& p: bdd_lstate_)
|
||||||
{
|
{
|
||||||
// If the signature of a state is bddfalse (no
|
// If the signature of a state is bddfalse (no
|
||||||
// transitions) the class of this state is bddfalse
|
// edges) the class of this state is bddfalse
|
||||||
// instead of an anonymous variable. It allows
|
// instead of an anonymous variable. It allows
|
||||||
// simplifications in the signature by removing a
|
// simplifications in the signature by removing a
|
||||||
// transition which has as a destination a state with
|
// edge which has as a destination a state with
|
||||||
// no outgoing transition.
|
// no outgoing edge.
|
||||||
bdd acc = bddfalse;
|
bdd acc = bddfalse;
|
||||||
if (p.first != bddfalse)
|
if (p.first != bddfalse)
|
||||||
acc = *it_bdd;
|
acc = *it_bdd;
|
||||||
|
|
@ -511,14 +511,14 @@ namespace spot
|
||||||
accst.resize(res->num_states(), 0U);
|
accst.resize(res->num_states(), 0U);
|
||||||
|
|
||||||
stat.states = bdd_lstate_.size();
|
stat.states = bdd_lstate_.size();
|
||||||
stat.transitions = 0;
|
stat.edges = 0;
|
||||||
|
|
||||||
unsigned nb_satoneset = 0;
|
unsigned nb_satoneset = 0;
|
||||||
unsigned nb_minato = 0;
|
unsigned nb_minato = 0;
|
||||||
|
|
||||||
auto all_inf = all_inf_;
|
auto all_inf = all_inf_;
|
||||||
// For each class, we will create
|
// For each class, we will create
|
||||||
// all the transitions between the states.
|
// all the edges between the states.
|
||||||
for (auto& p: bdd_lstate_)
|
for (auto& p: bdd_lstate_)
|
||||||
{
|
{
|
||||||
// All states in p.second have the same class, so just
|
// All states in p.second have the same class, so just
|
||||||
|
|
@ -565,11 +565,11 @@ namespace spot
|
||||||
bdd cond_acc_dest;
|
bdd cond_acc_dest;
|
||||||
while ((cond_acc_dest = isop.next()) != bddfalse)
|
while ((cond_acc_dest = isop.next()) != bddfalse)
|
||||||
{
|
{
|
||||||
++stat.transitions;
|
++stat.edges;
|
||||||
|
|
||||||
++nb_minato;
|
++nb_minato;
|
||||||
|
|
||||||
// Take the transition, and keep only the variable which
|
// Take the edge, and keep only the variable which
|
||||||
// are used to represent the class.
|
// are used to represent the class.
|
||||||
bdd dst = bdd_existcomp(cond_acc_dest,
|
bdd dst = bdd_existcomp(cond_acc_dest,
|
||||||
all_class_var_);
|
all_class_var_);
|
||||||
|
|
@ -584,7 +584,7 @@ namespace spot
|
||||||
|
|
||||||
// Because we have complemented all the Inf
|
// Because we have complemented all the Inf
|
||||||
// acceptance conditions on the input automaton,
|
// acceptance conditions on the input automaton,
|
||||||
// we must revert them to create a new transition.
|
// we must revert them to create a new edge.
|
||||||
acc ^= all_inf;
|
acc ^= all_inf;
|
||||||
|
|
||||||
if (Cosimulation)
|
if (Cosimulation)
|
||||||
|
|
@ -592,18 +592,18 @@ namespace spot
|
||||||
if (Sba)
|
if (Sba)
|
||||||
{
|
{
|
||||||
// acc should be attached to src, or rather,
|
// acc should be attached to src, or rather,
|
||||||
// in our transition-based representation)
|
// in our edge-based representation)
|
||||||
// to all transitions leaving src. As we
|
// to all edges leaving src. As we
|
||||||
// can't do this here, store this in a table
|
// can't do this here, store this in a table
|
||||||
// so we can fix it later.
|
// so we can fix it later.
|
||||||
accst[gb->get_state(src.id())] = acc;
|
accst[gb->get_state(src.id())] = acc;
|
||||||
acc = 0U;
|
acc = 0U;
|
||||||
}
|
}
|
||||||
gb->new_transition(dst.id(), src.id(), cond, acc);
|
gb->new_edge(dst.id(), src.id(), cond, acc);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
gb->new_transition(src.id(), dst.id(), cond, acc);
|
gb->new_edge(src.id(), dst.id(), cond, acc);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -612,7 +612,7 @@ namespace spot
|
||||||
res->set_init_state(gb->get_state(previous_class_
|
res->set_init_state(gb->get_state(previous_class_
|
||||||
[a_->get_init_state_number()].id()));
|
[a_->get_init_state_number()].id()));
|
||||||
|
|
||||||
res->merge_transitions(); // FIXME: is this really needed?
|
res->merge_edges(); // FIXME: is this really needed?
|
||||||
|
|
||||||
// Mark all accepting state in a second pass, when
|
// Mark all accepting state in a second pass, when
|
||||||
// dealing with SBA in cosimulation.
|
// dealing with SBA in cosimulation.
|
||||||
|
|
|
||||||
|
|
@ -286,7 +286,7 @@ namespace spot
|
||||||
get_all_ap(const const_twa_graph_ptr& a)
|
get_all_ap(const const_twa_graph_ptr& a)
|
||||||
{
|
{
|
||||||
bdd res = bddtrue;
|
bdd res = bddtrue;
|
||||||
for (auto& i: a->transitions())
|
for (auto& i: a->edges())
|
||||||
res &= bdd_support(i.cond);
|
res &= bdd_support(i.cond);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
@ -360,8 +360,8 @@ namespace spot
|
||||||
(void)u;
|
(void)u;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Create the transition.
|
// Create the edge.
|
||||||
res->new_transition(src, dest, one, t.acc);
|
res->new_edge(src, dest, one, t.acc);
|
||||||
|
|
||||||
if (src == dest)
|
if (src == dest)
|
||||||
self_loop_needed = false;
|
self_loop_needed = false;
|
||||||
|
|
@ -369,9 +369,9 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
if (self_loop_needed && s.second != bddfalse)
|
if (self_loop_needed && s.second != bddfalse)
|
||||||
res->new_transition(src, src, s.second, 0U);
|
res->new_edge(src, src, s.second, 0U);
|
||||||
}
|
}
|
||||||
res->merge_transitions();
|
res->merge_edges();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -381,18 +381,18 @@ namespace spot
|
||||||
if (atomic_propositions == bddfalse)
|
if (atomic_propositions == bddfalse)
|
||||||
atomic_propositions = get_all_ap(a);
|
atomic_propositions = get_all_ap(a);
|
||||||
unsigned num_states = a->num_states();
|
unsigned num_states = a->num_states();
|
||||||
unsigned num_transitions = a->num_transitions();
|
unsigned num_edges = a->num_edges();
|
||||||
std::vector<bdd> selfloops(num_states, bddfalse);
|
std::vector<bdd> selfloops(num_states, bddfalse);
|
||||||
std::map<std::pair<unsigned, int>, unsigned> newstates;
|
std::map<std::pair<unsigned, int>, unsigned> newstates;
|
||||||
// Record all the conditions for which we can selfloop on each
|
// Record all the conditions for which we can selfloop on each
|
||||||
// state.
|
// state.
|
||||||
for (auto& t: a->transitions())
|
for (auto& t: a->edges())
|
||||||
if (t.src == t.dst)
|
if (t.src == t.dst)
|
||||||
selfloops[t.src] |= t.cond;
|
selfloops[t.src] |= t.cond;
|
||||||
for (unsigned t = 1; t <= num_transitions; ++t)
|
for (unsigned t = 1; t <= num_edges; ++t)
|
||||||
{
|
{
|
||||||
auto& td = a->trans_storage(t);
|
auto& td = a->edge_storage(t);
|
||||||
if (a->is_dead_transition(td))
|
if (a->is_dead_edge(td))
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
unsigned src = td.src;
|
unsigned src = td.src;
|
||||||
|
|
@ -401,11 +401,11 @@ namespace spot
|
||||||
{
|
{
|
||||||
bdd all = td.cond;
|
bdd all = td.cond;
|
||||||
// If there is a self-loop with the whole condition on
|
// If there is a self-loop with the whole condition on
|
||||||
// either end of the transition, do not bother with it.
|
// either end of the edge, do not bother with it.
|
||||||
if (bdd_implies(all, selfloops[src])
|
if (bdd_implies(all, selfloops[src])
|
||||||
|| bdd_implies(all, selfloops[dst]))
|
|| bdd_implies(all, selfloops[dst]))
|
||||||
continue;
|
continue;
|
||||||
// Do not use td in the loop because the new_transition()
|
// Do not use td in the loop because the new_edge()
|
||||||
// might invalidate it.
|
// might invalidate it.
|
||||||
auto acc = td.acc;
|
auto acc = td.acc;
|
||||||
while (all != bddfalse)
|
while (all != bddfalse)
|
||||||
|
|
@ -420,13 +420,13 @@ namespace spot
|
||||||
if (p.second)
|
if (p.second)
|
||||||
p.first->second = a->new_state();
|
p.first->second = a->new_state();
|
||||||
unsigned tmp = p.first->second; // intermediate state
|
unsigned tmp = p.first->second; // intermediate state
|
||||||
unsigned i = a->new_transition(src, tmp, one, acc);
|
unsigned i = a->new_edge(src, tmp, one, acc);
|
||||||
assert(i > num_transitions);
|
assert(i > num_edges);
|
||||||
i = a->new_transition(tmp, tmp, one, 0U);
|
i = a->new_edge(tmp, tmp, one, 0U);
|
||||||
assert(i > num_transitions);
|
assert(i > num_edges);
|
||||||
// No acceptance here to preserve the state-based property.
|
// No acceptance here to preserve the state-based property.
|
||||||
i = a->new_transition(tmp, dst, one, 0U);
|
i = a->new_edge(tmp, dst, one, 0U);
|
||||||
assert(i > num_transitions);
|
assert(i > num_edges);
|
||||||
(void)i;
|
(void)i;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -437,7 +437,7 @@ namespace spot
|
||||||
false, // deterministic
|
false, // deterministic
|
||||||
false, // stutter inv.
|
false, // stutter inv.
|
||||||
});
|
});
|
||||||
a->merge_transitions();
|
a->merge_edges();
|
||||||
return a;
|
return a;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -474,7 +474,7 @@ namespace spot
|
||||||
|
|
||||||
while (!todo.empty())
|
while (!todo.empty())
|
||||||
{
|
{
|
||||||
auto t1 = a->trans_storage(todo.back());
|
auto t1 = a->edge_storage(todo.back());
|
||||||
todo.pop_back();
|
todo.pop_back();
|
||||||
|
|
||||||
for (auto& t2 : a->out(t1.dst))
|
for (auto& t2 : a->out(t1.dst))
|
||||||
|
|
@ -486,7 +486,7 @@ namespace spot
|
||||||
acc_cond::mark_t acc = t1.acc | t2.acc;
|
acc_cond::mark_t acc = t1.acc | t2.acc;
|
||||||
for (auto& t: dst2trans[t2.dst])
|
for (auto& t: dst2trans[t2.dst])
|
||||||
{
|
{
|
||||||
auto& ts = a->trans_storage(t);
|
auto& ts = a->edge_storage(t);
|
||||||
if (acc == ts.acc)
|
if (acc == ts.acc)
|
||||||
{
|
{
|
||||||
if (!bdd_implies(cond, ts.cond))
|
if (!bdd_implies(cond, ts.cond))
|
||||||
|
|
@ -516,9 +516,9 @@ namespace spot
|
||||||
if (need_new_trans)
|
if (need_new_trans)
|
||||||
{
|
{
|
||||||
// Load t2.dst first, because t2 can be
|
// Load t2.dst first, because t2 can be
|
||||||
// invalidated by new_transition().
|
// invalidated by new_edge().
|
||||||
auto dst = t2.dst;
|
auto dst = t2.dst;
|
||||||
auto i = a->new_transition(state, dst, cond, acc);
|
auto i = a->new_edge(state, dst, cond, acc);
|
||||||
dst2trans[dst].push_back(i);
|
dst2trans[dst].push_back(i);
|
||||||
todo.push_back(i);
|
todo.push_back(i);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -95,7 +95,7 @@ namespace spot
|
||||||
assert(nterms > 0);
|
assert(nterms > 0);
|
||||||
res->set_generalized_buchi(nterms);
|
res->set_generalized_buchi(nterms);
|
||||||
|
|
||||||
for (auto& t: res->transitions())
|
for (auto& t: res->edges())
|
||||||
{
|
{
|
||||||
acc_cond::mark_t cur_m = t.acc;
|
acc_cond::mark_t cur_m = t.acc;
|
||||||
acc_cond::mark_t new_m = 0U;
|
acc_cond::mark_t new_m = 0U;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue