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

safra: handle single accepting set

Browse source 
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Here.
This commit is contained in:
Alexandre Lewkowicz 2015-05-13 19:43:11 +02:00 • committed by Alexandre Duret-Lutz
parent 496083b14a
commit f2fa92004c
2 changed files with 151 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

167
src/twaalgos/safra.cc
View file

@ -43,10 +43,11 @@ namespace spot
safra_state empty_state = safra_state(nb_braces_.size());
idx = res.size();
res.push_back(std::make_pair(empty_state, t.cond));
std::cerr << "Created inner node: " << idx << std::endl;
}
safra_state& ss = res[idx].first;
assert(ss.nb_braces_.size() == ss.is_green_.size());
ss.update_succ(node, t.dst, t.acc);
assert(ss.nb_braces_.size() == ss.is_green_.size());
}
}
for (auto& s: res)
@ -59,53 +60,158 @@ namespace spot
void safra_state::finalize_construction()
{
// TODO this is a dirty hack to have two comparision functions depending on
// wether or not we are still construction the safra_stata
// Ideally I'd like to have this done statically but not sure how to do it
for (unsigned i = 0; i < nb_braces_.size(); ++i)
std::vector<unsigned> rem_succ_of;
assert(is_green_.size() == nb_braces_.size());
for (unsigned i = 0; i < is_green_.size(); ++i)
{
if (nb_braces_[i] == 0)
{
// TODO We also emit Red = min(red, i)
// Step A3: Brackets that do not contain any nodes emit red
is_green_[i] = false;
}
else if (is_green_[i])
{
// Step A4 Emit green
rem_succ_of.emplace_back(i);
}
}
for (auto& n: nodes_)
{
node& nn = const_cast<node&>(n);
// Step A4 Remove all brackets inside each green pair
nn.truncate_braces(rem_succ_of, nb_braces_);
}
// Step A5 define the rem variable
std::vector<unsigned> decr_by(nb_braces_.size());
unsigned decr = 0;
for (unsigned i = 0; i < nb_braces_.size(); ++i)
{
// Step A5 renumber braces
nb_braces_[i - decr] = nb_braces_[i];
if (nb_braces_[i] == 0)
{
++decr;
}
// Step A5, renumber braces
decr_by[i] = decr;
}
nb_braces_.resize(nb_braces_.size() - decr);
for (auto& n: nodes_)
{
node& nn = const_cast<node&>(n);
nn.renumber(decr_by);
// TODO this is a dirty hack to have two comparision functions depending
// on wether or not we are still construction the safra_stata
// Ideally I'd like to have this done statically but not sure how to do
// it
nn.disable_construction();
}
}
void safra_state::node::renumber(const std::vector<unsigned>& decr_by)
{
for (unsigned idx = 0; idx < braces_.size(); ++idx)
{
braces_[idx] -= decr_by[braces_[idx]];
}
}
// TODO FINISH TRUNCATE
void
safra_state::node::truncate_braces(const std::vector<unsigned>& rem_succ_of,
std::vector<size_t>& nb_braces)
{
assert(in_construction_ && "Only allowed to do this during construction");
for (unsigned idx = 0; idx < braces_.size(); ++idx)
{
bool found = false;
// find first brace that matches rem_succ_of
for (auto s: rem_succ_of)
{
found |= braces_[idx] == s;
}
if (found)
{
assert(idx < braces_.size() - 1);
// For each deleted brace, decrement elements of nb_braces
// This corresponds to A4 step
for (unsigned i = idx + 1; i < braces_.size(); ++i)
{
--nb_braces[braces_[i]];
}
braces_.resize(idx + 1);
break;
}
}
}
void safra_state::update_succ(const node& src, unsigned dst,
const acc_cond::mark_t acc)
{
(void) acc; // TODO
unsigned last_brace = src.braces_.back();
// Check if there already is a node named dst in current macro_state
auto i = nodes_.find(node(dst));
if (i != nodes_.end())
{
// Todo need to handle acc and create new braces
if (src.braces_ > i->braces_)
// Step A2: Remove all occurrences whos nesting pattern (i-e braces_)
// is smaller
if (src.braces_ > i->braces_ ||
(acc.count() && src.braces_ == i->braces_))
{
std::cerr << "Replacing braces of: " << dst << std::endl;
node& dst = const_cast<node&>(*i);
for (auto b: dst.braces_)
nb_braces_[b]--;
dst.braces_ = src.braces_;
auto copy = src.braces_;
// TODO handle multiple accepting transition
if (acc.count())
{
// Accepting transition generate new braces: step A1
last_brace = nb_braces_.size();
copy.emplace_back(nb_braces_.size());
nb_braces_.emplace_back(1);
// Newly created braces cannot emit green as they won't have
// any braces inside them (by construction)
is_green_.emplace_back(false);
}
{
// Remove brace count of removed node
node& dst = const_cast<node&>(*i);
for (auto b: dst.braces_)
--nb_braces_[b];
}
{
// Affect new value of braces
node& dst = const_cast<node&>(*i);
for (auto b: copy)
++nb_braces_[b];
dst.braces_ = std::move(copy);
}
}
// Node already exists and has bigger values
else
// Node already exists and has bigger nesting pattern value
return;
}
else
{
// Todo need to handle acc and create new braces
nodes_.emplace(dst, src.braces_);
// TODO need to handle multiple acc sets
auto copy = src.braces_;
if (acc.count())
{
last_brace = nb_braces_.size();
copy.emplace_back(nb_braces_.size());
// Step A4 Newly created braces cannot emit green as they won't have
// any braces inside them (by construction)
is_green_.emplace_back(false);
nb_braces_.emplace_back(0);
}
for (auto b: copy)
++nb_braces_[b];
nodes_.emplace(dst, std::move(copy));
}
for (auto b: src.braces_)
nb_braces_[b]++;
// If brace has no right-hand-side brace than it cannot emit any green color
is_green_[src.braces_[src.braces_.size() - 1]] = false;
// Step A4: For a brace to emit green it must surround other braces.
// Therefore, the last brace cannot emit green as it is the most inside
// brace.
is_green_[last_brace] = false;
}
// Comparison is needed when for a set of safra_state
@ -131,7 +237,7 @@ namespace spot
{
unsigned nb_braces = val;
// One brace set
is_green_.assign(true, nb_braces);
is_green_.assign(nb_braces, true);
// First brace has init_state hence one state inside the first braces.
nb_braces_.assign(nb_braces, 0);
}
@ -156,6 +262,21 @@ namespace spot
return false;
}
void safra_state::print_debug(unsigned state_id)
{
std::cerr << "State: " << state_id << "{ ";
for (auto& n: nodes_)
{
std::cerr << n.id_ << " [";
for (auto& b: n.braces_)
{
std::cerr << b << ' ';
}
std::cerr << "], ";
}
std::cerr << "}\n";
}
twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& aut)
{
@ -196,12 +317,10 @@ namespace spot
else
{
dst_num = res->new_state();
std::cerr << "New state " << dst_num << std::endl;
s.first.print_debug(dst_num);
todo.push_back(s.first);
seen.insert(std::make_pair(s.first, dst_num));
}
std::cerr << "Tr: " << src_num << " -> " << dst_num << "["
<< s.second << "]" << std::endl;
res->new_transition(src_num, dst_num, s.second);
}
}

9
src/twaalgos/safra.hh
View file

@ -36,6 +36,9 @@ namespace spot
bool operator==(const node& other) const;
bool operator<(const node& other) const;
void disable_construction() { in_construction_ = false; }
void truncate_braces(const std::vector<unsigned>& rem_succ_of,
std::vector<size_t>& nb_braces);
void renumber(const std::vector<unsigned>& decr_by);
node(unsigned id)
: id_(id), in_construction_(true) {}
node(unsigned id, brace_t b_id, bool in_construction = true)
@ -57,12 +60,16 @@ namespace spot
public:
typedef std::vector<std::pair<safra_state, bdd>> succs_t;
bool operator<(const safra_state& other) const;
// Print each sub-state with their associated braces of a safra state
void print_debug(unsigned state_id);
safra_state(unsigned state_number, bool init_state = false);
// Given a certain transition_label, compute all the successors of that
// label, and return that new node.
succs_t compute_succs(const const_twa_graph_ptr& aut) const;
// Used when creating the list of successors
void update_succ(const node& src, unsigned dst, const acc_cond::mark_t);
// 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 node& src, unsigned dst, const acc_cond::mark_t acc);
void finalize_construction();
// A list of nodes similar to the ones of a
// safra tree. These are constructed in the same way as the powerset