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

acd: fix typeness checks, and add options for those

Browse source 
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Here.
* tests/python/zlktree.ipynb, tests/python/zlktree.py: Add tests
and examples.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-24 11:10:12 +02:00
parent 406bc8ed17
commit 043a1dc394
4 changed files with 365 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

96
spot/twaalgos/zlktree.cc
View file

@ -23,6 +23,7 @@
#include <spot/twaalgos/zlktree.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>
using namespace std::string_literals;
namespace spot
{
@ -188,7 +189,7 @@ namespace spot
std::pair<unsigned, unsigned>
zielonka_tree::step(unsigned branch, acc_cond::mark_t colors) const
{
if (SPOT_UNLIKELY(nodes_.size() < branch || nodes_[branch].first_child))
if (SPOT_UNLIKELY(nodes_.size() <= branch || nodes_[branch].first_child))
throw std::runtime_error
("zielonka_tree::step(): incorrect branch number");
@ -345,14 +346,26 @@ namespace spot
+ " is too large");
}
acd::acd(const const_twa_graph_ptr& aut)
: si_(new scc_info(aut)), own_si_(true), trees_(si_->scc_count())
void acd::report_need_opt(const char* opt)
{
throw std::runtime_error("ACD should be built with option "s + opt);
}
void acd::report_empty_acd(const char* fn)
{
throw
std::runtime_error(std::string(fn) +
"(): ACD is empty, did you use ABORT_WRONG_SHAPE?");
}
acd::acd(const const_twa_graph_ptr& aut, acd_options opt)
: si_(new scc_info(aut)), own_si_(true), opt_(opt), trees_(si_->scc_count())
{
build_();
}
acd::acd(const scc_info& si)
: si_(&si), own_si_(false), trees_(si_->scc_count())
acd::acd(const scc_info& si, acd_options opt)
: si_(&si), own_si_(false), opt_(opt), trees_(si_->scc_count())
{
build_();
}
@ -507,10 +520,39 @@ namespace spot
}
else if (children > 1)
{
if (accepting_node)
has_rabin_shape_ = false;
else
has_streett_shape_ = false;
// Check the shape if requested.
if ((has_rabin_shape_
&& !!(opt_ & acd_options::CHECK_RABIN)
&& accepting_node)
|| (has_streett_shape_
&& !!(opt_ & acd_options::CHECK_STREETT)
&& !accepting_node))
{
std::unique_ptr<bitvect> seen(make_bitvect(nstates));
std::unique_ptr<bitvect> cur(make_bitvect(nstates));
for (const auto& [sz, bv]: out)
{
cur->clear_all();
bv->foreach_set_index([&aut, &cur](unsigned e)
{
cur->set(aut->edge_storage(e).src);
});
if (cur->intersects(*seen))
{
if (accepting_node)
has_rabin_shape_ = false;
else
has_streett_shape_ = false;
if (!!(opt_ & acd_options::ABORT_WRONG_SHAPE))
{
nodes_.clear();
return;
}
break;
}
*seen |= *cur;
}
}
}
}
// Now we decide if the ACD corresponds to a "min even" or "max
@ -565,11 +607,14 @@ namespace spot
unsigned acd::first_branch(unsigned s) const
{
if (SPOT_UNLIKELY(aut_->num_states() < s))
throw std::runtime_error("first_branch(): unknown state " +
throw std::runtime_error("acd::first_branch(): unknown state " +
std::to_string(s));
unsigned scc = si_->scc_of(s);
if (trees_[scc].trivial) // the branch is irrelevant for transiant SCCs
return 0;
if (SPOT_UNLIKELY(nodes_.empty()))
// make sure we do not complain about this if all SCCs are trivial.
report_empty_acd("acd::first_branch");
unsigned n = trees_[scc].root;
assert(nodes_[n].states.get(s));
return leftmost_branch_(n, s);
@ -579,7 +624,7 @@ namespace spot
std::pair<unsigned, unsigned>
acd::step(unsigned branch, unsigned edge) const
{
if (SPOT_UNLIKELY(nodes_.size() < branch))
if (SPOT_UNLIKELY(nodes_.size() <= branch))
throw std::runtime_error("acd::step(): incorrect branch number");
if (SPOT_UNLIKELY(nodes_[branch].edges.size() < edge))
throw std::runtime_error("acd::step(): incorrect edge number");
@ -622,13 +667,13 @@ namespace spot
void acd::dot(std::ostream& os, const char* id) const
{
unsigned ns = nodes_.size();
os << "digraph acd {\n labelloc=\"t\"\n label=\"\n"
<< (is_even_ ? "min even\"" : "min odd\"\n");
<< (ns ? (is_even_ ? "min even\"" : "min odd\"") : "empty ACD\"");
if (id)
escape_str(os << " id=\"", id)
// fill the node so that the entire node is clickable
<< "\"\n node [id=\"N\\N\", style=filled, fillcolor=white]\n";
unsigned ns = nodes_.size();
for (unsigned n = 0; n < ns; ++n)
{
acc_cond::mark_t m = {};
@ -736,14 +781,14 @@ namespace spot
bool acd::node_acceptance(unsigned n) const
{
if (SPOT_UNLIKELY(nodes_.size() < n))
if (SPOT_UNLIKELY(nodes_.size() <= n))
throw std::runtime_error("acd::node_acceptance(): unknown node");
return (nodes_[n].level & 1) ^ is_even_;
}
std::vector<unsigned> acd::edges_of_node(unsigned n) const
{
if (SPOT_UNLIKELY(nodes_.size() < n))
if (SPOT_UNLIKELY(nodes_.size() <= n))
throw std::runtime_error("acd::edges_of_node(): unknown node");
std::vector<unsigned> res;
unsigned scc = nodes_[n].scc;
@ -755,6 +800,27 @@ namespace spot
return res;
}
bool acd::has_rabin_shape() const
{
if (!(opt_ & acd_options::CHECK_RABIN))
report_need_opt("CHECK_RABIN");
return has_rabin_shape_;
}
bool acd::has_streett_shape() const
{
if (!(opt_ & acd_options::CHECK_STREETT))
report_need_opt("CHECK_STREETT");
return has_streett_shape_;
}
bool acd::has_parity_shape() const
{
if ((opt_ & acd_options::CHECK_PARITY) != acd_options::CHECK_PARITY)
report_need_opt("CHECK_PARITY");
return has_streett_shape_ && has_rabin_shape_;
}
twa_graph_ptr
acd_transform(const const_twa_graph_ptr& a, bool colored)
{

80
spot/twaalgos/zlktree.hh
View file

@ -151,6 +151,48 @@ namespace spot
twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut);
/// \ingroup twa_acc_transform
/// \brief Options to alter the behavior of acd
enum class acd_options
{
/// Build the ACD, without checking its shape.
NONE = 0,
/// Check if the ACD has Rabin shape.
CHECK_RABIN = 1,
/// Check if the ACD has Streett shape.
CHECK_STREETT = 2,
/// Check if the ACD has Parity shape
CHECK_PARITY = CHECK_RABIN | CHECK_STREETT,
/// Abort the construction of the ACD if it does not have the
/// shape that is tested. When that happens, node_count() is set
/// to 0.
ABORT_WRONG_SHAPE = 4,
};
#ifndef SWIG
inline
bool operator!(acd_options me)
{
return me == acd_options::NONE;
}
inline
acd_options operator&(acd_options left, acd_options right)
{
typedef std::underlying_type_t<acd_options> ut;
return static_cast<acd_options>(static_cast<ut>(left)
& static_cast<ut>(right));
}
inline
acd_options operator|(acd_options left, acd_options right)
{
typedef std::underlying_type_t<acd_options> ut;
return static_cast<acd_options>(static_cast<ut>(left)
| static_cast<ut>(right));
}
#endif
/// \ingroup twa_acc_transform
/// \brief Alternating Cycle Decomposition implementation
///
@ -164,8 +206,8 @@ namespace spot
{
public:
/// \brief Build a Alternating Cycle Decomposition an SCC decomposition
acd(const scc_info& si);
acd(const const_twa_graph_ptr& aut);
acd(const scc_info& si, acd_options opt = acd_options::NONE);
acd(const const_twa_graph_ptr& aut, acd_options opt = acd_options::NONE);
~acd();
@ -229,29 +271,24 @@ namespace spot
/// \brief Whether the ACD has Rabin shape.
///
/// The ACD has Rabin shape of all accepting (round) nodes have
/// at most one child.
bool has_rabin_shape() const
{
return has_rabin_shape_;
}
/// The ACD has Rabin shape if all accepting (round) nodes have no
/// children with a state in common. The acd should be built with
/// option CHECK_RABIN or CHECK_PARITY for this function to work.
bool has_rabin_shape() const;
/// \brief Whether the ACD has Streett shape.
///
/// The ACD has Streett shape of all rejecting (square) nodes have
/// at most one child.
bool has_streett_shape() const
{
return has_streett_shape_;
}
/// The ACD has Streett shape if all rejecting (square) nodes have no
/// children with a state in common. The acd should be built with
/// option CHECK_STREETT or CHECK_PARITY for this function to work.
bool has_streett_shape() const;
/// \brief Whether the ACD has parity shape.
/// \brief Whether the ACD has Streett shape.
///
/// The ACD has parity shape of all nodes have at most one child.
bool has_parity_shape() const
{
return has_streett_shape() && has_rabin_shape();
}
/// The ACD has Streett shape if all nodes have no
/// children with a state in common. The acd should be built with
/// option CHECK_PARITY for this function to work.
bool has_parity_shape() const;
/// \brief Return the automaton on which the ACD is defined.
const const_twa_graph_ptr get_aut() const
@ -268,6 +305,7 @@ namespace spot
private:
const scc_info* si_;
bool own_si_ = false;
acd_options opt_;
// This structure is used to represent one node in the ACD forest.
// The tree use a left-child / right-sibling representation
@ -335,6 +373,8 @@ namespace spot
#ifndef SWIG
[[noreturn]] static
void report_invalid_scc_number(unsigned num, const char* fn);
[[noreturn]] static void report_need_opt(const char* opt);
[[noreturn]] static void report_empty_acd(const char* fn);
#endif
};

186
tests/python/zlktree.ipynb
View file

File diff suppressed because one or more lines are too long

90
tests/python/zlktree.py
View file

@ -27,3 +27,93 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3}
b = spot.zielonka_tree_transform(a)
assert spot.are_equivalent(a, b)
assert b.acc().is_buchi()
def report_missing_exception():
raise RuntimeError("missing exception")
a = spot.automaton("""
HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" acc-name: Rabin 3
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) &
Inf(5)) properties: trans-labels explicit-labels trans-acc --BODY--
State: 0 [0&!1] 0 {1 2 3} [!0&!1] 8 [0&1] 4 State: 1 [0&1] 1 {2}
State: 2 [0&1] 8 {3} [0&1] 2 {1} [!0&1] 4 {3 4} [!0&!1] 3 {2 5} State:
3 [!0&!1] 5 [0&1] 8 {1 2} [!0&!1] 9 {1} State: 4 [0&!1] 3 {0 2} [!0&1]
5 {1} State: 5 [!0&!1] 6 [!0&!1] 7 {2} [0&!1] 3 {1} [!0&1] 5 State: 6
[!0&!1] 1 [!0&!1] 2 {4} [0&!1] 0 {1 3 4} [0&1] 5 [!0&!1] 3 State: 7
[0&1] 4 {0} [0&1] 5 [0&1] 0 {3} [0&1] 1 {2 4} State: 8 [0&!1] 6 {0 4
5} [!0&!1] 7 {4} [0&!1] 2 {1 3} [0&1] 0 {0 1 4} State: 9 [!0&1] 6 {4}
[!0&!1] 2 {5} [!0&!1] 0 {3} [!0&!1] 5 --END--""")
aa = spot.acd(a)
try:
assert aa.has_rabin_shape()
except RuntimeError as e:
assert 'CHECK_RABIN' in str(e)
else:
report_missing_exception()
try:
assert not aa.has_streett_shape()
except RuntimeError as e:
assert 'CHECK_STREETT' in str(e)
else:
report_missing_exception()
try:
assert not aa.has_parity_shape()
except RuntimeError as e:
assert 'CHECK_PARITY' in str(e)
else:
report_missing_exception()
aa = spot.acd(a, spot.acd_options_CHECK_RABIN)
assert aa.has_rabin_shape()
assert aa.node_count() == 13
try:
assert not aa.has_streett_shape()
except RuntimeError as e:
assert 'CHECK_STREETT' in str(e)
else:
report_missing_exception()
try:
assert aa.has_parity_shape()
except RuntimeError as e:
assert 'CHECK_PARITY' in str(e)
else:
report_missing_exception()
aa = spot.acd(a, (spot.acd_options_CHECK_PARITY |
spot.acd_options_ABORT_WRONG_SHAPE))
assert aa.has_rabin_shape()
assert not aa.has_streett_shape()
assert not aa.has_parity_shape()
assert aa.node_count() == 0
try:
aa.first_branch(0)
except RuntimeError as e:
assert 'ABORT_WRONG_SHAPE' in str(e)
else:
report_missing_exception()
try:
aa.step(0, 0)
except RuntimeError as e:
assert 'incorrect branch number' in str(e)
else:
report_missing_exception()
try:
aa.node_acceptance(0)
except RuntimeError as e:
assert 'unknown node' in str(e)
else:
report_missing_exception()
try:
aa.edges_of_node(0)
except RuntimeError as e:
assert 'unknown node' in str(e)
else:
report_missing_exception()