mark_t: sets() no longer returns a vector
spot::mark_t::sets() was modified so that it now returns an iterable object rather than an std::vector<unsigned>. * NEWS: Mention the modification. * python/spot/impl.i: Declares mark_container as iterable to SWIG. * spot/parseaut/parseaut.yy: Adapts to the modification. * spot/twa/acc.hh: Implement the modification. * tests/python/acc_cond.ipynb: Adapts to the modification.
This commit is contained in:
parent
9377db2e5e
commit
cc3bdfcd2e
5 changed files with 113 additions and 21 deletions
3
NEWS
3
NEWS
|
|
@ -48,6 +48,9 @@ New in spot 2.3.3.dev (not yet released)
|
||||||
synonym for spot::twa::prop_universal() to help backward
|
synonym for spot::twa::prop_universal() to help backward
|
||||||
compatibility.
|
compatibility.
|
||||||
|
|
||||||
|
- spot::acc_cond::mark_t::sets() now returns an internal iterable
|
||||||
|
object instead of an std::vector<unsigned>.
|
||||||
|
|
||||||
Deprecation notice:
|
Deprecation notice:
|
||||||
|
|
||||||
- spot::dtwa_complement() used to work only on deterministic
|
- spot::dtwa_complement() used to work only on deterministic
|
||||||
|
|
|
||||||
|
|
@ -787,6 +787,14 @@ def state_is_accepting(self, src) -> "bool":
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
%extend spot::internal::mark_container {
|
||||||
|
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
|
||||||
|
{
|
||||||
|
return swig::make_forward_iterator_np(self->begin(), self->begin(),
|
||||||
|
self->end(), *PYTHON_SELF);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
%extend spot::twa_graph {
|
%extend spot::twa_graph {
|
||||||
unsigned new_univ_edge(unsigned src, const std::vector<unsigned>& v,
|
unsigned new_univ_edge(unsigned src, const std::vector<unsigned>& v,
|
||||||
bdd cond, acc_cond::mark_t acc = 0U)
|
bdd cond, acc_cond::mark_t acc = 0U)
|
||||||
|
|
|
||||||
|
|
@ -2173,14 +2173,18 @@ static void fix_acceptance(result_& r)
|
||||||
unsigned base = 0;
|
unsigned base = 0;
|
||||||
if (both)
|
if (both)
|
||||||
{
|
{
|
||||||
auto v = both.sets();
|
base = acc.add_sets(both.count());
|
||||||
auto vs = v.size();
|
|
||||||
base = acc.add_sets(vs);
|
|
||||||
for (auto& t: r.h->aut->edge_vector())
|
for (auto& t: r.h->aut->edge_vector())
|
||||||
if ((t.acc & both) != both)
|
{
|
||||||
for (unsigned i = 0; i < vs; ++i)
|
unsigned i = 0;
|
||||||
if (!t.acc.has(v[i]))
|
if ((t.acc & both) != both)
|
||||||
t.acc |= acc.mark(base + i);
|
for (unsigned v : both.sets())
|
||||||
|
{
|
||||||
|
if (!t.acc.has(v))
|
||||||
|
t.acc |= acc.mark(base + i);
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (onlyneg || both)
|
if (onlyneg || both)
|
||||||
|
|
|
||||||
|
|
@ -28,6 +28,10 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
namespace internal
|
||||||
|
{
|
||||||
|
class mark_container;
|
||||||
|
}
|
||||||
class SPOT_API acc_cond
|
class SPOT_API acc_cond
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
|
|
@ -297,13 +301,8 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// FIXME: Return some iterable object without building a vector.
|
// Returns some iterable object that contains the used sets.
|
||||||
std::vector<unsigned> sets() const
|
spot::internal::mark_container sets() const;
|
||||||
{
|
|
||||||
std::vector<unsigned> res;
|
|
||||||
fill(std::back_inserter(res));
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
SPOT_API
|
SPOT_API
|
||||||
friend std::ostream& operator<<(std::ostream& os, mark_t m);
|
friend std::ostream& operator<<(std::ostream& os, mark_t m);
|
||||||
|
|
@ -1243,6 +1242,85 @@ namespace spot
|
||||||
|
|
||||||
SPOT_API
|
SPOT_API
|
||||||
std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
|
std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
|
||||||
|
|
||||||
|
namespace internal
|
||||||
|
{
|
||||||
|
class SPOT_API mark_iterator
|
||||||
|
{
|
||||||
|
public:
|
||||||
|
typedef unsigned value_type;
|
||||||
|
typedef const value_type& reference;
|
||||||
|
typedef const value_type* pointer;
|
||||||
|
typedef std::ptrdiff_t difference_type;
|
||||||
|
typedef std::forward_iterator_tag iterator_category;
|
||||||
|
|
||||||
|
mark_iterator() noexcept
|
||||||
|
: m_(0U)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
mark_iterator(acc_cond::mark_t m) noexcept
|
||||||
|
: m_(m)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator==(mark_iterator m) const
|
||||||
|
{
|
||||||
|
return m_ == m.m_;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator!=(mark_iterator m) const
|
||||||
|
{
|
||||||
|
return m_ != m.m_;
|
||||||
|
}
|
||||||
|
|
||||||
|
value_type operator*() const
|
||||||
|
{
|
||||||
|
SPOT_ASSERT(m_);
|
||||||
|
return m_.min_set() - 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
mark_iterator operator++()
|
||||||
|
{
|
||||||
|
m_.id &= m_.id - 1;
|
||||||
|
return *this;
|
||||||
|
}
|
||||||
|
|
||||||
|
mark_iterator operator++(int)
|
||||||
|
{
|
||||||
|
mark_iterator it = *this;
|
||||||
|
++(*this);
|
||||||
|
return it;
|
||||||
|
}
|
||||||
|
private:
|
||||||
|
acc_cond::mark_t m_;
|
||||||
|
};
|
||||||
|
|
||||||
|
class SPOT_API mark_container
|
||||||
|
{
|
||||||
|
public:
|
||||||
|
mark_container(spot::acc_cond::mark_t m) noexcept
|
||||||
|
: m_(m)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
mark_iterator begin() const
|
||||||
|
{
|
||||||
|
return {m_};
|
||||||
|
}
|
||||||
|
mark_iterator end() const
|
||||||
|
{
|
||||||
|
return {};
|
||||||
|
}
|
||||||
|
private:
|
||||||
|
spot::acc_cond::mark_t m_;
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
inline spot::internal::mark_container acc_cond::mark_t::sets() const
|
||||||
|
{
|
||||||
|
return {*this};
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace std
|
namespace std
|
||||||
|
|
|
||||||
|
|
@ -15,10 +15,9 @@
|
||||||
"name": "python",
|
"name": "python",
|
||||||
"nbconvert_exporter": "python",
|
"nbconvert_exporter": "python",
|
||||||
"pygments_lexer": "ipython3",
|
"pygments_lexer": "ipython3",
|
||||||
"version": "3.4.3+"
|
"version": "3.5.3"
|
||||||
},
|
},
|
||||||
"name": "",
|
"name": ""
|
||||||
"signature": "sha256:9abaa081794db5d5479c8c9c179c8518aa52b60abdb4b7a106045646e277d43a"
|
|
||||||
},
|
},
|
||||||
"nbformat": 3,
|
"nbformat": 3,
|
||||||
"nbformat_minor": 0,
|
"nbformat_minor": 0,
|
||||||
|
|
@ -338,7 +337,7 @@
|
||||||
"collapsed": false,
|
"collapsed": false,
|
||||||
"input": [
|
"input": [
|
||||||
"print(x)\n",
|
"print(x)\n",
|
||||||
"print(x.sets())\n",
|
"print(list(x.sets()))\n",
|
||||||
"for s in x.sets():\n",
|
"for s in x.sets():\n",
|
||||||
" print(s)"
|
" print(s)"
|
||||||
],
|
],
|
||||||
|
|
@ -350,7 +349,7 @@
|
||||||
"stream": "stdout",
|
"stream": "stdout",
|
||||||
"text": [
|
"text": [
|
||||||
"{0,2,5}\n",
|
"{0,2,5}\n",
|
||||||
"(0, 2, 5)\n",
|
"[0, 2, 5]\n",
|
||||||
"0\n",
|
"0\n",
|
||||||
"2\n",
|
"2\n",
|
||||||
"5\n"
|
"5\n"
|
||||||
|
|
@ -1435,7 +1434,7 @@
|
||||||
"language": "python",
|
"language": "python",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"outputs": [],
|
"outputs": [],
|
||||||
"prompt_number": 52
|
"prompt_number": null
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"metadata": {}
|
"metadata": {}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue