26ef5458eb
This uses the same trick as discussed in issue #566 and issue #568. * spot/twaalgos/determinize.cc (safra_support): Use a basis if it is smaller than 2^|support| for the current Safra state. * tests/core/568.test: Add some tests. * NEWS: Mention the optimization.
1114 lines
34 KiB
C++
1114 lines
34 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
|
|
//
|
|
// This file is part of Spot, a model checking library.
|
|
//
|
|
// Spot is free software; you can redistribute it and/or modify it
|
|
// under the terms of the GNU General Public License as published by
|
|
// the Free Software Foundation; either version 3 of the License, or
|
|
// (at your option) any later version.
|
|
//
|
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
// License for more details.
|
|
//
|
|
// You should have received a copy of the GNU General Public License
|
|
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
#include "config.h"
|
|
#include <algorithm>
|
|
#include <deque>
|
|
#include <stack>
|
|
#include <utility>
|
|
#include <set>
|
|
#include <map>
|
|
#include <cmath>
|
|
#include <spot/misc/clz.hh>
|
|
#include <spot/misc/bddlt.hh>
|
|
#include <spot/twaalgos/sccinfo.hh>
|
|
#include <spot/twaalgos/determinize.hh>
|
|
#include <spot/twaalgos/degen.hh>
|
|
#include <spot/twaalgos/sccfilter.hh>
|
|
#include <spot/twaalgos/simulation.hh>
|
|
#include <spot/twaalgos/isdet.hh>
|
|
#include <spot/twaalgos/parity.hh>
|
|
#include <spot/twaalgos/split.hh>
|
|
#include <spot/priv/robin_hood.hh>
|
|
|
|
namespace spot
|
|
{
|
|
namespace
|
|
{
|
|
// forward declaration
|
|
struct safra_build;
|
|
class compute_succs;
|
|
}
|
|
|
|
class safra_state final
|
|
{
|
|
public:
|
|
// a helper method to check invariants
|
|
void
|
|
check() const
|
|
{
|
|
// do not refer to braces that do not exist
|
|
for (const auto& p : nodes_)
|
|
if (p.second >= 0)
|
|
if (((unsigned)p.second) >= braces_.size())
|
|
assert(false);
|
|
|
|
// braces_ describes the parenthood relation, -1 meaning toplevel
|
|
// so braces_[b] < b always, and -1 is the only negative number allowed
|
|
for (int b : braces_)
|
|
{
|
|
if (b < 0 && b != -1)
|
|
assert(false);
|
|
if (b >= 0 && braces_[b] > b)
|
|
assert(false);
|
|
}
|
|
|
|
// no unused braces
|
|
std::set<int> used_braces;
|
|
for (const auto& n : nodes_)
|
|
{
|
|
int b = n.second;
|
|
while (b >= 0)
|
|
{
|
|
used_braces.insert(b);
|
|
b = braces_[b];
|
|
}
|
|
}
|
|
assert(used_braces.size() == braces_.size());
|
|
}
|
|
|
|
public:
|
|
using state_t = unsigned;
|
|
using safra_node_t = std::pair<state_t, std::vector<int>>;
|
|
|
|
bool operator<(const safra_state&) const;
|
|
bool operator==(const safra_state&) const;
|
|
size_t hash() const;
|
|
|
|
// Print the number of states in each brace
|
|
// default constructor
|
|
safra_state();
|
|
safra_state(state_t state_number, bool acceptance_scc = false);
|
|
safra_state(const safra_build& s, const compute_succs& cs, unsigned& color,
|
|
unsigned topbrace);
|
|
// Compute successor for transition ap
|
|
safra_state
|
|
compute_succ(const compute_succs& cs, const bdd& ap, unsigned& color) const;
|
|
void
|
|
merge_redundant_states(const std::vector<std::vector<char>>& implies);
|
|
unsigned
|
|
finalize_construction(const std::vector<int>& buildbraces,
|
|
const compute_succs& cs, unsigned topbrace);
|
|
|
|
// each brace points to its parent.
|
|
// braces_[i] is the parent of i
|
|
// Note that braces_[i] < i, -1 stands for "no parent" (top-level)
|
|
std::vector<int> braces_;
|
|
std::vector<std::pair<state_t, int>> nodes_;
|
|
};
|
|
|
|
namespace
|
|
{
|
|
struct hash_safra
|
|
{
|
|
size_t
|
|
operator()(const safra_state& s) const noexcept
|
|
{
|
|
return s.hash();
|
|
}
|
|
};
|
|
|
|
template<class T>
|
|
struct ref_wrap_equal
|
|
{
|
|
bool
|
|
operator()(const std::reference_wrapper<T>& x,
|
|
const std::reference_wrapper<T>& y) const
|
|
{
|
|
return std::equal_to<T>()(x.get(), y.get());
|
|
}
|
|
};
|
|
|
|
using power_set =
|
|
robin_hood::unordered_node_map<safra_state, unsigned, hash_safra>;
|
|
|
|
std::string
|
|
nodes_to_string(const const_twa_graph_ptr& aut,
|
|
const safra_state& states);
|
|
|
|
// Returns true if lhs has a smaller nesting pattern than rhs
|
|
// If lhs and rhs are the same, return false.
|
|
// NB the nesting patterns are backwards.
|
|
bool nesting_cmp(const std::vector<int>& lhs,
|
|
const std::vector<int>& rhs)
|
|
{
|
|
unsigned m = std::min(lhs.size(), rhs.size());
|
|
auto lit = lhs.rbegin();
|
|
auto rit = rhs.rbegin();
|
|
for (unsigned i = 0; i != m; ++i)
|
|
{
|
|
if (*lit != *rit)
|
|
return *lit < *rit;
|
|
}
|
|
return lhs.size() > rhs.size();
|
|
}
|
|
|
|
// a helper class for building the successor of a safra_state
|
|
struct safra_build final
|
|
{
|
|
std::vector<int> braces_;
|
|
std::map<unsigned, int> nodes_;
|
|
|
|
bool
|
|
compare_braces(int a, int b)
|
|
{
|
|
std::vector<int> a_pattern;
|
|
std::vector<int> b_pattern;
|
|
a_pattern.reserve(a+1);
|
|
b_pattern.reserve(b+1);
|
|
while (a != b)
|
|
{
|
|
if (a > b)
|
|
{
|
|
a_pattern.emplace_back(a);
|
|
a = braces_[a];
|
|
}
|
|
else
|
|
{
|
|
b_pattern.emplace_back(b);
|
|
b = braces_[b];
|
|
}
|
|
}
|
|
return nesting_cmp(a_pattern, b_pattern);
|
|
}
|
|
|
|
// Used when creating the list of successors
|
|
// 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(int brace, unsigned dst, const acc_cond::mark_t& acc)
|
|
{
|
|
int newb = brace;
|
|
if (acc)
|
|
{
|
|
assert(acc.has(0) && acc.is_singleton() && "Only TBA are accepted");
|
|
// Accepting edges generate new braces: step A1
|
|
newb = braces_.size();
|
|
braces_.emplace_back(brace);
|
|
}
|
|
auto i = nodes_.emplace(dst, newb);
|
|
if (!i.second) // dst already exists
|
|
{
|
|
// Step A2: Only keep the smallest nesting pattern.
|
|
// Use nesting_cmp to compare nesting patterns.
|
|
if (compare_braces(newb, i.first->second))
|
|
{
|
|
i.first->second = newb;
|
|
}
|
|
else
|
|
{
|
|
if (newb != brace) // new brace was created but is not needed
|
|
braces_.pop_back();
|
|
}
|
|
}
|
|
}
|
|
|
|
// Same as above, specialized for brace == -1
|
|
// Acceptance parameter is passed as a template parameter to improve
|
|
// performance.
|
|
// If a node for dst already existed, the newly inserted node has smaller
|
|
// nesting pattern iff is_acc == true AND nodes_[dst] == -1
|
|
template<bool is_acc>
|
|
void
|
|
update_succ_toplevel(unsigned dst)
|
|
{
|
|
if (is_acc)
|
|
{
|
|
// Accepting edges generate new braces: step A1
|
|
int newb = braces_.size();
|
|
auto i = nodes_.emplace(dst, newb);
|
|
if (i.second || i.first->second == -1)
|
|
{
|
|
braces_.emplace_back(-1);
|
|
i.first->second = newb;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
nodes_.emplace(dst, -1);
|
|
}
|
|
}
|
|
|
|
};
|
|
|
|
// Given a certain transition_label, compute all the successors of a
|
|
// safra_state under that label, and return the new nodes in res.
|
|
class compute_succs final
|
|
{
|
|
friend class spot::safra_state;
|
|
|
|
const safra_state* src;
|
|
const std::vector<bdd>* all_bdds;
|
|
const const_twa_graph_ptr& aut;
|
|
const power_set& seen;
|
|
const scc_info& scc;
|
|
const std::vector<std::vector<char>>& implies;
|
|
bool use_scc;
|
|
bool use_simulation;
|
|
bool use_stutter;
|
|
|
|
// work vectors for safra_state::finalize_construction()
|
|
mutable std::vector<char> empty_green;
|
|
mutable std::vector<int> highest_green_ancestor;
|
|
mutable std::vector<unsigned> decr_by;
|
|
mutable safra_build ss;
|
|
|
|
public:
|
|
compute_succs(const const_twa_graph_ptr& aut,
|
|
const power_set& seen,
|
|
const scc_info& scc,
|
|
const std::vector<std::vector<char>>& implies,
|
|
bool use_scc,
|
|
bool use_simulation,
|
|
bool use_stutter)
|
|
: src(nullptr)
|
|
, all_bdds(nullptr)
|
|
, aut(aut)
|
|
, seen(seen)
|
|
, scc(scc)
|
|
, implies(implies)
|
|
, use_scc(use_scc)
|
|
, use_simulation(use_simulation)
|
|
, use_stutter(use_stutter)
|
|
{}
|
|
|
|
void
|
|
set(const safra_state& s, const std::vector<bdd>& v)
|
|
{
|
|
src = &s;
|
|
all_bdds = &v;
|
|
}
|
|
|
|
struct iterator
|
|
{
|
|
const compute_succs& cs_;
|
|
std::vector<bdd>::const_iterator bddit;
|
|
safra_state ss;
|
|
unsigned color_;
|
|
|
|
iterator(const compute_succs& c, std::vector<bdd>::const_iterator it)
|
|
: cs_(c)
|
|
, bddit(it)
|
|
{
|
|
compute_();
|
|
}
|
|
|
|
bool
|
|
operator!=(const iterator& other) const
|
|
{
|
|
return bddit != other.bddit;
|
|
}
|
|
|
|
iterator&
|
|
operator++()
|
|
{
|
|
++bddit;
|
|
compute_();
|
|
return *this;
|
|
}
|
|
// no need to implement postfix increment
|
|
|
|
const bdd&
|
|
cond() const
|
|
{
|
|
return *bddit;
|
|
}
|
|
|
|
const safra_state&
|
|
operator*() const
|
|
{
|
|
return ss;
|
|
}
|
|
const safra_state*
|
|
operator->() const
|
|
{
|
|
return &ss;
|
|
}
|
|
|
|
private:
|
|
std::vector<safra_state> stutter_path_;
|
|
|
|
void
|
|
compute_()
|
|
{
|
|
if (bddit == cs_.all_bdds->end())
|
|
return;
|
|
|
|
const bdd& ap = *bddit;
|
|
|
|
// In stutter-invariant automata, every time we follow a
|
|
// transition labeled by L, we can actually stutter the L
|
|
// label and jump further away. The following code performs
|
|
// this stuttering until a cycle is found, and select one
|
|
// state of the cycle as the destination to jump to.
|
|
if (cs_.use_stutter && cs_.aut->prop_stutter_invariant())
|
|
{
|
|
ss = *cs_.src;
|
|
// The path is usually quite small (3-4 states), so it's
|
|
// not worth setting up a hash table to detect a cycle.
|
|
stutter_path_.clear();
|
|
std::vector<safra_state>::iterator cycle_seed;
|
|
unsigned mincolor = -1U;
|
|
// stutter forward until we cycle
|
|
for (;;)
|
|
{
|
|
// any duplicate value, if any, is usually close to
|
|
// the end, so search backward.
|
|
auto it = std::find(stutter_path_.rbegin(),
|
|
stutter_path_.rend(), ss);
|
|
if (it != stutter_path_.rend())
|
|
{
|
|
cycle_seed = (it + 1).base();
|
|
break;
|
|
}
|
|
stutter_path_.emplace_back(std::move(ss));
|
|
ss = stutter_path_.back().compute_succ(cs_, ap, color_);
|
|
mincolor = std::min(color_, mincolor);
|
|
}
|
|
bool in_seen = cs_.seen.find(*cycle_seed) != cs_.seen.end();
|
|
for (auto it = cycle_seed + 1; it < stutter_path_.end(); ++it)
|
|
{
|
|
if (in_seen)
|
|
{
|
|
// if *cycle_seed is already in seen, replace
|
|
// it with a smaller state also in seen.
|
|
if (cs_.seen.find(*it) != cs_.seen.end()
|
|
&& *it < *cycle_seed)
|
|
cycle_seed = it;
|
|
}
|
|
else
|
|
{
|
|
// if *cycle_seed is not in seen, replace it
|
|
// either with a state in seen or with a smaller
|
|
// state
|
|
if (cs_.seen.find(*it) != cs_.seen.end())
|
|
{
|
|
cycle_seed = it;
|
|
in_seen = true;
|
|
}
|
|
else if (*it < *cycle_seed)
|
|
{
|
|
cycle_seed = it;
|
|
}
|
|
}
|
|
}
|
|
ss = std::move(*cycle_seed);
|
|
color_ = mincolor;
|
|
}
|
|
else
|
|
{
|
|
ss = cs_.src->compute_succ(cs_, ap, color_);
|
|
}
|
|
}
|
|
};
|
|
|
|
iterator
|
|
begin() const
|
|
{
|
|
return iterator(*this, all_bdds->begin());
|
|
}
|
|
iterator
|
|
end() const
|
|
{
|
|
return iterator(*this, all_bdds->end());
|
|
}
|
|
};
|
|
|
|
const char* const sub[10] =
|
|
{
|
|
"\u2080",
|
|
"\u2081",
|
|
"\u2082",
|
|
"\u2083",
|
|
"\u2084",
|
|
"\u2085",
|
|
"\u2086",
|
|
"\u2087",
|
|
"\u2088",
|
|
"\u2089",
|
|
};
|
|
|
|
std::string subscript(unsigned start)
|
|
{
|
|
std::string res;
|
|
do
|
|
{
|
|
res = sub[start % 10] + res;
|
|
start /= 10;
|
|
}
|
|
while (start);
|
|
return res;
|
|
}
|
|
|
|
struct compare
|
|
{
|
|
bool
|
|
operator() (const safra_state::safra_node_t& lhs,
|
|
const safra_state::safra_node_t& rhs) const
|
|
{
|
|
return lhs.second < rhs.second;
|
|
}
|
|
};
|
|
|
|
// Return the nodes sorted in ascending order
|
|
std::vector<safra_state::safra_node_t>
|
|
sorted_nodes(const safra_state& s)
|
|
{
|
|
std::vector<safra_state::safra_node_t> res;
|
|
for (const auto& n: s.nodes_)
|
|
{
|
|
// First, count the number of braces.
|
|
unsigned nbraces = 0;
|
|
for (int brace = n.second; brace >= 0; brace = s.braces_[brace])
|
|
++nbraces;
|
|
// Then list them in reverse order. Since we know the
|
|
// number of braces, we can allocate exactly what we need.
|
|
if (nbraces > 0)
|
|
{
|
|
std::vector<int> tmp(nbraces, 0);
|
|
for (int brace = n.second; brace >= 0; brace = s.braces_[brace])
|
|
tmp[--nbraces] = brace;
|
|
res.emplace_back(n.first, std::move(tmp));
|
|
}
|
|
else
|
|
{
|
|
res.emplace_back(n.first, std::vector<int>{});
|
|
}
|
|
}
|
|
std::sort(res.begin(), res.end(), compare());
|
|
return res;
|
|
}
|
|
|
|
std::string
|
|
nodes_to_string(const const_twa_graph_ptr& aut,
|
|
const safra_state& states)
|
|
{
|
|
auto copy = sorted_nodes(states);
|
|
std::ostringstream os;
|
|
std::stack<int> s;
|
|
bool first = true;
|
|
for (const auto& n: copy)
|
|
{
|
|
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.second.begin(), n.second.end(),
|
|
s.top());
|
|
if (it == n.second.end() || *it != s.top())
|
|
{
|
|
os << subscript(s.top()) << '}';
|
|
s.pop();
|
|
}
|
|
else
|
|
{
|
|
if (*it == s.top())
|
|
++it;
|
|
break;
|
|
}
|
|
}
|
|
// Add new braces
|
|
while (it != n.second.end())
|
|
{
|
|
os << '{' << subscript(*it);
|
|
s.push(*it);
|
|
++it;
|
|
first = true;
|
|
}
|
|
if (!first)
|
|
os << ' ';
|
|
os << aut->format_state(n.first);
|
|
first = false;
|
|
}
|
|
// Finish unwinding stack to print last braces
|
|
while (!s.empty())
|
|
{
|
|
os << subscript(s.top()) << '}';
|
|
s.pop();
|
|
}
|
|
return os.str();
|
|
}
|
|
|
|
std::vector<std::string>*
|
|
print_debug(const const_twa_graph_ptr& aut,
|
|
const power_set& states)
|
|
{
|
|
auto res = new std::vector<std::string>(states.size());
|
|
for (const auto& p: states)
|
|
(*res)[p.second] = nodes_to_string(aut, p.first);
|
|
return res;
|
|
}
|
|
|
|
std::vector<unsigned>*
|
|
classify(const power_set& states,
|
|
const std::vector<unsigned>* original_class)
|
|
{
|
|
unsigned sz = states.size();
|
|
auto classes = new std::vector<unsigned>(sz);
|
|
std::vector<std::set<unsigned>> state_sets(sz);
|
|
for (const auto& p: states)
|
|
{
|
|
// Get the set of original stats of this
|
|
std::set<unsigned> s;
|
|
for (auto& n: p.first.nodes_)
|
|
{
|
|
unsigned st = n.first;
|
|
if (original_class)
|
|
st = (*original_class)[st];
|
|
s.insert(st);
|
|
}
|
|
state_sets[p.second] = std::move(s);
|
|
}
|
|
std::map<std::set<unsigned>, unsigned> seensets;
|
|
for (unsigned s = 0; s < sz; ++s)
|
|
{
|
|
auto p = seensets.emplace(state_sets[s], s);
|
|
(*classes)[s] = p.first->second;
|
|
}
|
|
return classes;
|
|
}
|
|
|
|
class safra_support
|
|
{
|
|
const std::vector<bdd>& state_supports;
|
|
robin_hood::unordered_flat_map<bdd, std::vector<bdd>, bdd_hash> cache;
|
|
std::vector<bdd> basis;
|
|
unsigned log_basis_size = 0;
|
|
public:
|
|
safra_support(const std::vector<bdd>& s,
|
|
const const_twa_graph_ptr& orig_aut)
|
|
: state_supports(s)
|
|
{
|
|
unsigned nap = orig_aut->ap().size();
|
|
if (nap > 5)
|
|
{
|
|
edge_separator es;
|
|
// Gather all labels, but stop if we see too many. The
|
|
// threshold below is arbitrary: adjust if you know better.
|
|
if (es.add_to_basis(orig_aut, 256 * nap))
|
|
{
|
|
basis = es.basis();
|
|
auto sz = basis.size();
|
|
log_basis_size = CHAR_BIT*sizeof(sz) - clz(sz);
|
|
}
|
|
}
|
|
}
|
|
|
|
const std::vector<bdd>&
|
|
get(const safra_state& s)
|
|
{
|
|
bdd supp = bddtrue;
|
|
for (const auto& n : s.nodes_)
|
|
supp &= state_supports[n.first];
|
|
auto i = cache.emplace(supp, std::vector<bdd>());
|
|
if (i.second) // insertion took place
|
|
{
|
|
std::vector<bdd>& res = i.first->second;
|
|
// If we have a basis, we probably want to use it.
|
|
// But we should do that only if 2^|supp| is larger.
|
|
if (log_basis_size)
|
|
{
|
|
// Compute the size of the support
|
|
bdd s = supp;
|
|
unsigned sz = log_basis_size;
|
|
while (sz && s != bddtrue)
|
|
{
|
|
--sz;
|
|
s = bdd_high(s);
|
|
}
|
|
if (s != bddtrue)
|
|
return res = basis;
|
|
}
|
|
for (bdd one: minterms_of(bddtrue, supp))
|
|
res.emplace_back(one);
|
|
}
|
|
return i.first->second;
|
|
}
|
|
};
|
|
}
|
|
|
|
std::vector<char> find_scc_paths(const scc_info& scc);
|
|
|
|
safra_state
|
|
safra_state::compute_succ(const compute_succs& cs,
|
|
const bdd& ap, unsigned& color) const
|
|
{
|
|
safra_build& ss = cs.ss;
|
|
ss.braces_ = braces_; // copy
|
|
ss.nodes_.clear();
|
|
unsigned topbrace = braces_.size();
|
|
for (const auto& node: nodes_)
|
|
{
|
|
for (const auto& t: cs.aut->out(node.first))
|
|
{
|
|
if (!bdd_implies(ap, t.cond))
|
|
continue;
|
|
// Check if we are leaving the SCC, if so we delete all the
|
|
// braces as no cycles can be found with that node
|
|
if (cs.use_scc && cs.scc.scc_of(node.first) != cs.scc.scc_of(t.dst))
|
|
if (cs.scc.is_accepting_scc(cs.scc.scc_of(t.dst)))
|
|
// Entering accepting SCC so add brace
|
|
ss.update_succ_toplevel<true>(t.dst);
|
|
else
|
|
// When entering non accepting SCC don't create any braces
|
|
ss.update_succ_toplevel<false>(t.dst);
|
|
else
|
|
ss.update_succ(node.second, t.dst, t.acc);
|
|
}
|
|
}
|
|
return safra_state(ss, cs, color, topbrace);
|
|
}
|
|
|
|
// When a node a implies a node b, remove the node a.
|
|
void
|
|
safra_state::merge_redundant_states(
|
|
const std::vector<std::vector<char>>& implies)
|
|
{
|
|
auto it1 = nodes_.begin();
|
|
while (it1 != nodes_.end())
|
|
{
|
|
const auto& imp1 = implies[it1->first];
|
|
auto old_it1 = it1++;
|
|
if (imp1.empty())
|
|
continue;
|
|
for (auto it2 = nodes_.begin(); it2 != nodes_.end(); ++it2)
|
|
{
|
|
if (old_it1 == it2)
|
|
continue;
|
|
if (imp1[it2->first])
|
|
{
|
|
it1 = nodes_.erase(old_it1);
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
// Return the emitted color, red or green
|
|
unsigned
|
|
safra_state::finalize_construction(const std::vector<int>& buildbraces,
|
|
const compute_succs& cs, unsigned topbrace)
|
|
{
|
|
unsigned red = -1U;
|
|
unsigned green = -1U;
|
|
// use std::vector<char> to avoid std::vector<bool>
|
|
// a char encodes several bools:
|
|
// * first bit says whether the brace is empty and red
|
|
// * second bit says whether the brace is green
|
|
// brackets removed from green pairs can be safely be marked as red,
|
|
// because their enclosing green has a lower number
|
|
// beware of pairs marked both as red and green: they are actually empty
|
|
constexpr char is_empty = 1;
|
|
constexpr char is_green = 2;
|
|
cs.empty_green.assign(buildbraces.size(), is_empty | is_green);
|
|
|
|
for (const auto& n : nodes_)
|
|
if (n.second >= 0)
|
|
{
|
|
int brace = n.second;
|
|
// Step A4: For a brace to be green it must not contain states
|
|
// on its own.
|
|
cs.empty_green[brace] &= ~is_green;
|
|
while (brace >= 0 && (cs.empty_green[brace] & is_empty))
|
|
{
|
|
cs.empty_green[brace] &= ~is_empty;
|
|
brace = buildbraces[brace];
|
|
}
|
|
}
|
|
|
|
// Step A4 Remove brackets within green pairs
|
|
// for each bracket, find its highest green ancestor
|
|
// 0 cannot be in a green pair, its highest green ancestor is itself
|
|
// Also find red and green signals to emit
|
|
// And compute the number of braces to remove for renumbering
|
|
cs.highest_green_ancestor.assign(buildbraces.size(), 0);
|
|
cs.decr_by.assign(buildbraces.size(), 0);
|
|
unsigned decr = 0;
|
|
for (unsigned b = 0; b != buildbraces.size(); ++b)
|
|
{
|
|
cs.highest_green_ancestor[b] = b;
|
|
const int& ancestor = buildbraces[b];
|
|
// Note that ancestor < b
|
|
if (ancestor >= 0
|
|
&& (cs.highest_green_ancestor[ancestor] != ancestor
|
|
|| (cs.empty_green[ancestor] & is_green)))
|
|
{
|
|
cs.highest_green_ancestor[b] = cs.highest_green_ancestor[ancestor];
|
|
cs.empty_green[b] |= is_empty; // mark brace for removal
|
|
}
|
|
|
|
if (cs.empty_green[b] & is_empty)
|
|
{
|
|
// Step A5 renumber braces
|
|
++decr;
|
|
|
|
// Any brace above topbrace was added while constructing
|
|
// this successor, so it should not emit any red.
|
|
if (b < topbrace)
|
|
// Step A3 emit red
|
|
red = std::min(red, 2*b);
|
|
}
|
|
else if (cs.empty_green[b] & is_green)
|
|
{
|
|
assert(b < topbrace);
|
|
// Step A4 emit green
|
|
green = std::min(green, 2*b+1);
|
|
}
|
|
|
|
cs.decr_by[b] = decr;
|
|
}
|
|
|
|
// Update nodes with new braces numbers
|
|
braces_ = std::vector<int>(buildbraces.size() - decr, -1);
|
|
for (auto& n : nodes_)
|
|
{
|
|
if (n.second >= 0)
|
|
{
|
|
unsigned i = cs.highest_green_ancestor[n.second];
|
|
int j = buildbraces[i] >=0
|
|
? buildbraces[i] - cs.decr_by[buildbraces[i]]
|
|
: -1;
|
|
n.second = i - cs.decr_by[i];
|
|
braces_[n.second] = j;
|
|
}
|
|
}
|
|
|
|
return std::min(red, green);
|
|
}
|
|
|
|
safra_state::safra_state()
|
|
: nodes_{std::make_pair(0, -1)}
|
|
{}
|
|
|
|
// Called only to initialize first state
|
|
safra_state::safra_state(state_t val, bool accepting_scc)
|
|
: nodes_{std::make_pair(val, -1)}
|
|
{
|
|
if (accepting_scc)
|
|
{
|
|
braces_.emplace_back(-1);
|
|
nodes_.back().second = 0;
|
|
}
|
|
}
|
|
|
|
safra_state::safra_state(const safra_build& s,
|
|
const compute_succs& cs,
|
|
unsigned& color,
|
|
unsigned topbrace)
|
|
: nodes_(s.nodes_.begin(), s.nodes_.end())
|
|
{
|
|
if (cs.use_simulation)
|
|
merge_redundant_states(cs.implies);
|
|
color = finalize_construction(s.braces_, cs, topbrace);
|
|
}
|
|
|
|
bool
|
|
safra_state::operator<(const safra_state& other) const
|
|
{
|
|
// FIXME: what is the right, if any, comparison to perform?
|
|
return braces_ == other.braces_ ? nodes_ < other.nodes_
|
|
: braces_ < other.braces_;
|
|
}
|
|
size_t
|
|
safra_state::hash() const
|
|
{
|
|
size_t res = 0;
|
|
//std::cerr << this << " [";
|
|
for (const auto& p : nodes_)
|
|
{
|
|
res ^= (res << 3) ^ p.first;
|
|
res ^= (res << 3) ^ p.second;
|
|
// std::cerr << '(' << p.first << ',' << p.second << ')';
|
|
}
|
|
// std::cerr << "][ ";
|
|
for (const auto& b : braces_)
|
|
{
|
|
res ^= (res << 3) ^ b;
|
|
// std::cerr << b << ' ';
|
|
}
|
|
// std::cerr << "]: " << std::hex << res << std::dec << '\n';
|
|
return res;
|
|
}
|
|
|
|
bool
|
|
safra_state::operator==(const safra_state& other) const
|
|
{
|
|
return nodes_ == other.nodes_ && braces_ == other.braces_;
|
|
}
|
|
|
|
namespace
|
|
{
|
|
class reachability_matrix final
|
|
{
|
|
// Store a lower triangular matrix.
|
|
// (j can reach i) <=> (i<=j and m[j*(j+1)/2 + i]==1)
|
|
std::vector<char> m;
|
|
public:
|
|
reachability_matrix(const scc_info& scc)
|
|
{
|
|
unsigned scccount = scc.scc_count();
|
|
m.resize(scccount * (scccount + 1) / 2, 0);
|
|
for (unsigned i = 0; i < scccount; ++i)
|
|
m[(i * (i + 1) / 2) + i] = 1;
|
|
for (unsigned i = 1; i < scccount; ++i)
|
|
{
|
|
unsigned ibase = i * (i + 1) / 2;
|
|
for (unsigned d: scc.succ(i))
|
|
{
|
|
// we necessarily have d < i because of the way SCCs are
|
|
// numbered, so we can build the transitive closure by
|
|
// just ORing any SCC reachable from d.
|
|
unsigned dbase = d * (d + 1) / 2;
|
|
for (unsigned j = 0; j <= d; ++j)
|
|
m[ibase + j] |= m[dbase + j];
|
|
}
|
|
}
|
|
}
|
|
|
|
bool operator()(unsigned j, unsigned i) const
|
|
{
|
|
return i <= j && m[(j * (j + 1) / 2) + i];
|
|
}
|
|
};
|
|
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
tgba_determinize(const const_twa_graph_ptr& a,
|
|
bool pretty_print, bool use_scc,
|
|
bool use_simulation, bool use_stutter,
|
|
const output_aborter* aborter,
|
|
int trans_pruning,
|
|
bool want_classes)
|
|
{
|
|
if (!a->is_existential())
|
|
throw std::runtime_error
|
|
("tgba_determinize() does not support alternation");
|
|
if (is_universal(a))
|
|
return std::const_pointer_cast<twa_graph>(a);
|
|
|
|
// Degeneralize
|
|
const_twa_graph_ptr aut;
|
|
std::vector<bdd> implications;
|
|
{
|
|
twa_graph_ptr aut_tmp = spot::degeneralize_tba(a);
|
|
if (pretty_print)
|
|
aut_tmp->copy_state_names_from(a);
|
|
if (use_simulation)
|
|
{
|
|
aut_tmp = spot::scc_filter(aut_tmp, true, nullptr, true);
|
|
auto aut2 = simulation(aut_tmp, &implications, trans_pruning);
|
|
if (pretty_print)
|
|
aut2->copy_state_names_from(aut_tmp);
|
|
aut_tmp = aut2;
|
|
}
|
|
aut = aut_tmp;
|
|
}
|
|
scc_info_options scc_opt = scc_info_options::TRACK_SUCCS;
|
|
// We do need to track states in SCC for stutter invariance (see below how
|
|
// supports are computed in this case)
|
|
if (use_stutter && aut->prop_stutter_invariant())
|
|
scc_opt = scc_info_options::TRACK_SUCCS | scc_info_options::TRACK_STATES;
|
|
scc_info scc = scc_info(aut, scc_opt);
|
|
|
|
// If we have too many SCCs, disable simulation-based checks, as
|
|
// computations to index the matrix would overflow. (Issue #541.)
|
|
if (scc.scc_count() >= (1 << 16))
|
|
{
|
|
use_simulation = false;
|
|
implications.clear();
|
|
}
|
|
|
|
// If use_simulation is false, implications is empty, so nothing is built
|
|
std::vector<std::vector<char>> implies(
|
|
implications.size(),
|
|
std::vector<char>(implications.size(), 0));
|
|
if (use_simulation)
|
|
{
|
|
reachability_matrix scc_can_reach(scc);
|
|
bool something_implies_something = false;
|
|
for (unsigned i = 0; i != implications.size(); ++i)
|
|
{
|
|
// NB spot::simulation() does not remove unreachable states, as it
|
|
// would invalidate the contents of 'implications'.
|
|
// so we need to explicitly test for unreachable states
|
|
// FIXME: based on the scc_info, we could remove the unreachable
|
|
// states, both in the input automaton and in 'implications'
|
|
// to reduce the size of 'implies'.
|
|
if (!scc.reachable_state(i))
|
|
continue;
|
|
unsigned scc_of_i = scc.scc_of(i);
|
|
bool i_implies_something = false;
|
|
for (unsigned j = 0; j != implications.size(); ++j)
|
|
{
|
|
if (!scc.reachable_state(j))
|
|
continue;
|
|
|
|
bool i_implies_j = !scc_can_reach(scc.scc_of(j), scc_of_i)
|
|
&& bdd_implies(implications[i], implications[j]);
|
|
implies[i][j] = i_implies_j;
|
|
i_implies_something |= i_implies_j;
|
|
}
|
|
// Clear useless lines.
|
|
if (!i_implies_something)
|
|
implies[i].clear();
|
|
else
|
|
something_implies_something = true;
|
|
}
|
|
if (!something_implies_something)
|
|
{
|
|
implies.clear();
|
|
use_simulation = false;
|
|
}
|
|
}
|
|
|
|
// Compute the support of each state
|
|
std::vector<bdd> support(aut->num_states());
|
|
if (use_stutter && aut->prop_stutter_invariant())
|
|
{
|
|
// FIXME: this could be improved
|
|
// supports of states should account for possible stuttering if we plan
|
|
// to use stuttering invariance
|
|
for (unsigned c = 0; c != scc.scc_count(); ++c)
|
|
{
|
|
bdd c_supp = scc.scc_ap_support(c);
|
|
for (const auto& su: scc.succ(c))
|
|
c_supp &= support[scc.one_state_of(su)];
|
|
for (unsigned st: scc.states_of(c))
|
|
support[st] = c_supp;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
for (unsigned i = 0; i != aut->num_states(); ++i)
|
|
{
|
|
bdd res = bddtrue;
|
|
for (const auto& e : aut->out(i))
|
|
res &= bdd_support(e.cond);
|
|
support[i] = res;
|
|
}
|
|
}
|
|
|
|
safra_support safra2letters(support, aut);
|
|
|
|
auto res = make_twa_graph(aut->get_dict());
|
|
res->copy_ap_of(aut);
|
|
res->prop_copy(aut,
|
|
{ false, // state based
|
|
false, // inherently_weak
|
|
false, false, // deterministic
|
|
false, // complete
|
|
true // stutter inv
|
|
});
|
|
// completeness can only be improved.
|
|
if (aut->prop_complete().is_true())
|
|
res->prop_complete(true);
|
|
|
|
// Given a safra_state get its associated state in output automata.
|
|
// Required to create new edges from 2 safra-state
|
|
power_set seen;
|
|
// As per the standard, references to elements in a std::unordered_set or
|
|
// std::unordered_map are invalidated by erasure only.
|
|
std::deque<std::reference_wrapper<power_set::value_type>> todo;
|
|
auto get_state = [&res, &seen, &todo](const safra_state& s) -> unsigned
|
|
{
|
|
auto it = seen.find(s);
|
|
if (it == seen.end())
|
|
{
|
|
unsigned dst_num = res->new_state();
|
|
it = seen.emplace(s, dst_num).first;
|
|
todo.emplace_back(*it);
|
|
}
|
|
return it->second;
|
|
};
|
|
|
|
{
|
|
unsigned init_state = aut->get_init_state_number();
|
|
bool start_accepting =
|
|
!use_scc || scc.is_accepting_scc(scc.scc_of(init_state));
|
|
safra_state init(init_state, start_accepting);
|
|
unsigned num = get_state(init); // inserts both in seen and in todo
|
|
res->set_init_state(num);
|
|
}
|
|
unsigned sets = 0;
|
|
|
|
compute_succs succs(aut, seen, scc, implies, use_scc, use_simulation,
|
|
use_stutter);
|
|
// The main loop
|
|
while (!todo.empty())
|
|
{
|
|
if (aborter && aborter->too_large(res))
|
|
return nullptr;
|
|
const safra_state& curr = todo.front().get().first;
|
|
unsigned src_num = todo.front().get().second;
|
|
todo.pop_front();
|
|
succs.set(curr, safra2letters.get(curr));
|
|
for (auto s = succs.begin(); s != succs.end(); ++s)
|
|
{
|
|
// Don't construct sink state as complete does a better job at this
|
|
if (s->nodes_.empty())
|
|
continue;
|
|
unsigned dst_num = get_state(*s);
|
|
if (s.color_ != -1U)
|
|
{
|
|
res->new_edge(src_num, dst_num, s.cond(), {s.color_});
|
|
sets = std::max(s.color_ + 1, sets);
|
|
}
|
|
else
|
|
res->new_edge(src_num, dst_num, s.cond());
|
|
}
|
|
}
|
|
// Green and red colors work in pairs, so the number of parity conditions is
|
|
// necessarily even.
|
|
sets += sets & 1;
|
|
// Acceptance is now min(odd) since we can emit Red on paths 0 with new opti
|
|
res->set_acceptance(sets, acc_cond::acc_code::parity_min_odd(sets));
|
|
res->prop_universal(true);
|
|
res->prop_state_acc(false);
|
|
|
|
cleanup_parity_here(res);
|
|
|
|
if (pretty_print)
|
|
res->set_named_prop("state-names", print_debug(aut, seen));
|
|
|
|
if (want_classes)
|
|
{
|
|
auto* ptr =
|
|
aut->get_named_prop<std::vector<unsigned>>("original-states");
|
|
if (ptr && ptr->size() != aut->num_states())
|
|
throw std::runtime_error("tgba_determinize(): "
|
|
"input's \"original-states\" property "
|
|
"has unexpected size");
|
|
if (!ptr)
|
|
{
|
|
ptr =
|
|
aut->get_named_prop<std::vector<unsigned>>("original-classes");
|
|
if (ptr && ptr->size() != aut->num_states())
|
|
throw std::runtime_error("tgba_determinize(): "
|
|
"input's \"original-classes\" property "
|
|
"has unexpected size");
|
|
}
|
|
res->set_named_prop("original-classes", classify(seen, ptr));
|
|
}
|
|
|
|
return res;
|
|
}
|
|
}
|