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

safra: Give more explicit names to types

Browse source 
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.
This commit is contained in:
Alexandre Lewkowicz 2015-09-24 07:40:40 +02:00 • committed by Alexandre Duret-Lutz
parent 18396e5973
commit b59b31f806
2 changed files with 28 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/twaalgos/safra.cc
View file

@ -87,20 +87,20 @@ namespace spot
struct compare
{
bool
operator() (std::pair<std::vector<node_helper::brace_t>, unsigned>& lhs,
std::pair<std::vector<node_helper::brace_t>, unsigned>& rhs)
operator() (const safra_state::safra_node_t& lhs,
const safra_state::safra_node_t& rhs)
{
return lhs.first < rhs.first;
return lhs.second < rhs.second;
}
};
// Return the sorteds nodes in ascending order
std::vector<std::pair<std::vector<node_helper::brace_t>, unsigned>>
std::vector<safra_state::safra_node_t>
sorted_nodes(const safra_state::nodes_t& nodes)
{
std::vector<std::pair<std::vector<node_helper::brace_t>, unsigned>> res;
std::vector<safra_state::safra_node_t> res;
for (auto& n: nodes)
res.emplace_back(n.second, n.first);
res.emplace_back(n.first, n.second);
std::sort(res.begin(), res.end(), compare());
return res;
}
@ -114,15 +114,15 @@ namespace spot
bool first = true;
for (auto& n: copy)
{
auto it = n.first.begin();
auto it = n.second.begin();
// Find brace on top of stack in vector
// If brace is not present, then we close it as no other ones of that
// type will be found since we ordered our vector
while (!s.empty())
{
it = std::lower_bound(n.first.begin(), n.first.end(),
it = std::lower_bound(n.second.begin(), n.second.end(),
s.top());
if (it == n.first.end() || *it != s.top())
if (it == n.second.end() || *it != s.top())
{
os << subscript(s.top()) << '}';
s.pop();
@ -135,7 +135,7 @@ namespace spot
}
}
// Add new braces
while (it != n.first.end())
while (it != n.second.end())
{
os << '{' << subscript(*it);
s.push(*it);
@ -144,7 +144,7 @@ namespace spot
}
if (!first)
os << ' ';
os << n.second;
os << n.first;
first = false;
}
// Finish unwinding stack to print last braces
@ -169,7 +169,7 @@ namespace spot
void
safra_state::compute_succs(const const_twa_graph_ptr& aut,
const std::vector<unsigned>& bddnums,
const std::vector<bdd_id_t>& bddnums,
std::unordered_map<bdd,
std::pair<unsigned, unsigned>,
bdd_hash>& deltas,
@ -230,7 +230,7 @@ namespace spot
}
}
unsigned safra_state::finalize_construction()
safra_state::color_t safra_state::finalize_construction()
{
unsigned red = -1U;
unsigned green = -1U;
@ -320,7 +320,7 @@ namespace spot
}
void safra_state::update_succ(const std::vector<node_helper::brace_t>& braces,
unsigned dst, const acc_cond::mark_t acc)
state_t dst, const acc_cond::mark_t acc)
{
std::vector<node_helper::brace_t> copy = braces;
if (acc.count())
@ -356,7 +356,7 @@ namespace spot
}
// Called only to initialize first state
safra_state::safra_state(unsigned val, bool init_state, bool accepting_scc)
safra_state::safra_state(state_t val, bool init_state, bool accepting_scc)
{
if (init_state)
{
@ -439,7 +439,7 @@ namespace spot
// Nedded for compute succs
// Used to convert large bdd to indexes
std::unordered_map<bdd, std::pair<unsigned, unsigned>, bdd_hash> deltas;
std::vector<unsigned> bddnums;
std::vector<safra_state::bdd_id_t> bddnums;
for (auto& t: aut->edges())
{
auto it = deltas.find(t.cond);

19
src/twaalgos/safra.hh
View file

@ -41,16 +41,21 @@ namespace spot
class safra_state
{
public:
using nodes_t = std::map<unsigned, std::vector<node_helper::brace_t>>;
using succs_t = std::vector<std::pair<safra_state, unsigned>>;
using state_t = unsigned;
using color_t = unsigned;
using bdd_id_t = unsigned;
using nodes_t = std::map<state_t, std::vector<node_helper::brace_t>>;
using succs_t = std::vector<std::pair<safra_state, bdd_id_t>>;
using safra_node_t = std::pair<state_t, std::vector<node_helper::brace_t>>;
bool operator<(const safra_state& other) const;
// Printh the number of states in each brace
safra_state(unsigned state_number, bool init_state = false,
safra_state(state_t state_number, bool init_state = false,
bool acceptance_scc = false);
// Given a certain transition_label, compute all the successors of that
// label, and return that new node.
void compute_succs(const const_twa_graph_ptr& aut,
const std::vector<unsigned>& bddnums,
const std::vector<bdd_id_t>& bddnums,
std::unordered_map<bdd,
std::pair<unsigned, unsigned>,
bdd_hash>& deltas,
@ -63,9 +68,9 @@ namespace spot
// A new intermediate node is created with src's braces and with dst as id
// A merge is done if dst already existed in *this
void update_succ(const std::vector<node_helper::brace_t>& braces,
unsigned dst, const acc_cond::mark_t acc);
state_t dst, const acc_cond::mark_t acc);
// Return the emitted color, red or green
unsigned finalize_construction();
color_t finalize_construction();
// A list of nodes similar to the ones of a
// safra tree. These are constructed in the same way as the powerset
// algorithm.
@ -75,7 +80,7 @@ namespace spot
std::vector<size_t> nb_braces_;
// A bitfield to know if a brace can emit green.
std::vector<bool> is_green_;
unsigned color_;
color_t color_;
};
SPOT_API twa_graph_ptr