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

acc_cond: rename is_tt/is_ff as is_t/is_f and add printer

Browse source 
* spot/twa/acc.cc, spot/twa/acc.hh: Here.
* spot/parseaut/parseaut.yy, spot/twa/acc.hh,
spot/twaalgos/gtec/gtec.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/neverclaim.cc, spot/twaalgos/product.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc: Adjust.
* NEWS: Mention the changes.
* wrap/python/spot_impl.i: Bind acc_cond the printer.
* wrap/python/tests/acc_cond.ipynb: Add more examples.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-17 08:42:34 +01:00
parent 2927cf38ac
commit 94cca9de3d
12 changed files with 259 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

15
NEWS
View file

@ -37,17 +37,22 @@ New in spot 1.99.6a (not yet released)
shift_left() have been replaced by operators |=, &=, <<=, and for
completeness the operators |, &, and << have been added.
* Several methods have been removed from the acc_cond class because
they were simply redundant with the methods of acc_cond::mark_t,
and more complex to use.
* Several methods have been removed from the acc_cond
class because they were simply redundant with the methods of
acc_cond::mark_t, and more complex to use.
acc_cond::marks(...) -> use acc_cond::mark_t(...) directly
acc_cond::marks(...) -> use acc_cond::mark_t(...)
acc_cond::sets(m) -> use m.sets()
acc_cond::has(m, u) -> use m.has(u) directly
acc_cond::has(m, u) -> use m.has(u)
acc_cond::cup(l, r) -> use l | r
acc_cond::cap(l, r) -> use l & r
acc_cond::set_minus(l, r) -> use l - r
Additionally, the following methods have been renamed:
acc_cond::is_tt() -> acc_cond::is_t()
acc_cond::is_ff() -> acc_cond::is_f()
Python:
* Iterating over the transitions leaving a state (the

2
spot/parseaut/parseaut.yy
View file

@ -572,7 +572,7 @@ header-item: "States:" INT
res.ignore_more_acc = true;
// Not setting the acceptance in case of error will
// force it to be true.
if (res.opts.want_kripke && (!$4->is_tt() || $2 > 0))
if (res.opts.want_kripke && (!$4->is_t() || $2 > 0))
error(@2 + @4,
"the acceptance for Kripke structure must be '0 t'");
else

27
spot/twa/acc.cc
View file

@ -51,6 +51,11 @@ namespace spot
return os;
}
std::ostream& operator<<(std::ostream& os, const acc_cond& acc)
{
return os << '(' << acc.num_sets() << ", " << acc.get_acceptance() << ')';
}
namespace
{
void default_set_printer(std::ostream& os, int v)
@ -411,9 +416,9 @@ namespace spot
int acc_cond::is_rabin() const
{
if (code_.is_ff())
if (code_.is_f())
return num_ == 0 ? 0 : -1;
if ((num_ & 1) || code_.is_tt())
if ((num_ & 1) || code_.is_t())
return -1;
if (is_rs(code_, acc_op::Or, acc_op::And, all_sets()))
@ -424,9 +429,9 @@ namespace spot
int acc_cond::is_streett() const
{
if (code_.is_tt())
if (code_.is_t())
return num_ == 0 ? 0 : -1;
if ((num_ & 1) || code_.is_ff())
if ((num_ & 1) || code_.is_f())
return -1;
if (is_rs(code_, acc_op::And, acc_op::Or, all_sets()))
@ -444,7 +449,7 @@ namespace spot
pairs.resize(num_);
return true;
}
if (code_.is_tt()
if (code_.is_t()
|| code_.back().op != acc_op::Or)
return false;
@ -670,7 +675,7 @@ namespace spot
if (sets == 0)
{
max = true;
odd = is_tt();
odd = is_t();
return true;
}
acc_cond::mark_t u_inf;
@ -857,7 +862,7 @@ namespace spot
std::pair<bool, acc_cond::mark_t>
acc_cond::unsat_mark() const
{
if (is_tt())
if (is_t())
return {false, 0U};
if (!uses_fin_acceptance())
return {true, 0U};
@ -1105,7 +1110,7 @@ namespace spot
acc_cond::acc_code acc_cond::acc_code::complement() const
{
if (is_tt())
if (is_t())
return acc_cond::acc_code::f();
return complement_rec(&back());
}
@ -1165,7 +1170,7 @@ namespace spot
acc_cond::acc_code
acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const
{
if (is_tt() || is_ff())
if (is_t() || is_f())
return *this;
return strip_rec(&back(), rem, missing);
}
@ -1173,7 +1178,7 @@ namespace spot
acc_cond::mark_t
acc_cond::acc_code::used_sets() const
{
if (is_tt() || is_ff())
if (is_t() || is_f())
return 0U;
acc_cond::mark_t used_in_cond = 0U;
auto pos = &back();
@ -1201,7 +1206,7 @@ namespace spot
std::pair<acc_cond::mark_t, acc_cond::mark_t>
acc_cond::acc_code::used_inf_fin_sets() const
{
if (is_tt() || is_ff())
if (is_t() || is_f())
return {0U, 0U};
acc_cond::mark_t used_fin = 0U;

38
spot/twa/acc.hh
View file

@ -395,14 +395,14 @@ namespace spot
return !(*this == other);
}
bool is_tt() const
bool is_t() const
{
unsigned s = size();
return s == 0
|| ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
}
bool is_ff() const
bool is_f() const
{
unsigned s = size();
return s > 1
@ -557,12 +557,12 @@ namespace spot
acc_code& operator&=(acc_code&& r)
{
if (is_tt() || r.is_ff())
if (is_t() || r.is_f())
{
*this = std::move(r);
return *this;
}
if (is_ff() || r.is_tt())
if (is_f() || r.is_t())
return *this;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
@ -649,12 +649,12 @@ namespace spot
acc_code& operator&=(const acc_code& r)
{
if (is_tt() || r.is_ff())
if (is_t() || r.is_f())
{
*this = r;
return *this;
}
if (is_ff() || r.is_tt())
if (is_f() || r.is_t())
return *this;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
@ -754,9 +754,9 @@ namespace spot
acc_code& operator|=(acc_code&& r)
{
if (is_tt() || r.is_ff())
if (is_t() || r.is_f())
return *this;
if (is_ff() || r.is_tt())
if (is_f() || r.is_t())
{
*this = std::move(r);
return *this;
@ -930,14 +930,24 @@ namespace spot
return uses_fin_acceptance_;
}
bool is_tt() const
bool is_t() const
{
return code_.is_tt();
return code_.is_t();
}
bool is_ff() const
bool is_all() const
{
return code_.is_ff();
return num_ == 0 && is_t();
}
bool is_f() const
{
return code_.is_f();
}
bool is_none() const
{
return num_ == 0 && is_f();
}
bool is_buchi() const
@ -1158,6 +1168,7 @@ namespace spot
mark_t::value_t all_;
acc_code code_;
bool uses_fin_acceptance_ = false;
};
/// \brief Parse a string into an acc_code
@ -1179,6 +1190,9 @@ namespace spot
///
/// A spot::parse_error is thrown on syntax error.
SPOT_API acc_cond::acc_code parse_acc_code(const char* input);
SPOT_API
std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
}
namespace std

4
spot/twaalgos/gtec/gtec.cc
View file

@ -133,7 +133,7 @@ namespace spot
{
{
auto acc = ecs_->aut->acc();
if (acc.get_acceptance().is_ff())
if (acc.get_acceptance().is_f())
return nullptr;
if (acc.uses_fin_acceptance())
throw std::runtime_error
@ -395,7 +395,7 @@ namespace spot
{
{
auto acc = ecs_->aut->acc();
if (acc.get_acceptance().is_ff())
if (acc.get_acceptance().is_f())
return nullptr;
if (acc.uses_fin_acceptance())
throw std::runtime_error

4
spot/twaalgos/hoa.cc
View file

@ -313,7 +313,7 @@ namespace spot
acc_cond::acc_code acc_c = aut->acc().get_acceptance();
if (aut->acc().is_generalized_buchi())
{
if (aut->acc().is_tt())
if (aut->acc().is_all())
os << "acc-name: all";
else if (aut->acc().is_buchi())
os << "acc-name: Buchi";
@ -323,7 +323,7 @@ namespace spot
}
else if (aut->acc().is_generalized_co_buchi())
{
if (aut->acc().is_ff())
if (aut->acc().is_none())
os << "acc-name: none";
else if (aut->acc().is_co_buchi())
os << "acc-name: co-Buchi";

2
spot/twaalgos/neverclaim.cc
View file

@ -205,7 +205,7 @@ namespace spot
print_never_claim(std::ostream& os, const const_twa_ptr& g,
const char* options)
{
if (!(g->acc().is_buchi() || g->acc().is_tt()))
if (!(g->acc().is_buchi() || g->acc().is_all()))
throw std::runtime_error
("Never claim output only supports Büchi acceptance");
never_claim_output d(os, options);

2
spot/twaalgos/product.cc
View file

@ -80,7 +80,7 @@ namespace spot
};
res->set_init_state(new_state(left_state, right_state));
if (right_acc.is_ff())
if (right_acc.is_f())
// Do not bother doing any work if the resulting acceptance is
// false.
return res;

4
spot/twaalgos/remfin.cc
View file

@ -312,7 +312,7 @@ namespace spot
auto code = aut->get_acceptance();
if (code.is_tt())
if (code.is_t())
return nullptr;
acc_cond::mark_t inf_pairs = 0U;
@ -640,7 +640,7 @@ namespace spot
auto c = acc.inf(m);
for (unsigned i = 0; i < sz; ++i)
{
if (!code[i].is_tt())
if (!code[i].is_t())
continue;
add[i] = m;
code[i] &= std::move(c);

2
spot/twaalgos/strength.cc
View file

@ -126,7 +126,7 @@ namespace spot
bool is_safety_mwdba(const const_twa_graph_ptr& aut)
{
if (!(aut->acc().is_buchi() || aut->acc().is_tt()))
if (!(aut->acc().is_buchi() || aut->acc().is_all()))
throw std::runtime_error
("is_safety_mwdba() should be called on a Buchi automaton");

18
wrap/python/spot_impl.i
View file

@ -485,19 +485,35 @@ namespace std {
return new spot::acc_cond::mark_t(f.begin(), f.end());
}
std::string __str__()
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::acc_cond {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::twa_run {

185
wrap/python/tests/acc_cond.ipynb
View file

@ -1,7 +1,23 @@
{
"metadata": {
"name": "",
"signature": "sha256:f11212c3a17ce302ae81974af32b21c1ebda4aa54d8930f03787ce7ed1c9e5f5"
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.4.3+"
},
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
@ -920,7 +936,7 @@
"output_type": "pyout",
"prompt_number": 34,
"text": [
"<spot_impl.acc_cond; proxy of <Swig Object of type 'spot::acc_cond *' at 0x7f19407487e0> >"
"(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))"
]
}
],
@ -970,17 +986,176 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"To be continued..."
"The `acc_cond` object can also be constructed using only a number of sets. In that case, the acceptance condition defaults to `t`, and it can be changed to something else later (using `set_acceptance()`). The number of acceptance sets can also be augmented with `add_sets()`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(4)\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 37,
"text": [
"(4, t)"
]
}
],
"prompt_number": 37
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc.add_sets(2)\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 38,
"text": [
"(6, t)"
]
}
],
"prompt_number": 38
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc.set_acceptance(spot.parse_acc_code('Streett 2'))\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 39,
"text": [
"(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
]
}
],
"prompt_number": 39
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The common scenario of setting generalized B\u00fcchi acceptance can be achieved more efficiently as follows:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(4)\n",
"acc.set_generalized_buchi()\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 40,
"text": [
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))"
]
}
],
"prompt_number": 40
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `acc_cond` class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, `Inf(0)&Inf(1)&Inf(2)&Inf(3)` is only called generalized B\u00fcchi if exactly for acceptance sets are used. So the following behavior should not be a surprise:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(acc)\n",
"print(acc.is_generalized_buchi())\n",
"acc.add_sets(1)\n",
"print(acc)\n",
"print(acc.is_generalized_buchi())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"True\n",
"(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"False\n"
]
}
],
"prompt_number": 41
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Similar methods like `is_t()`, `is_f()`, `is_buchi()`, `is_co_buchi()`, `is_generalized_co_buchi()` all return a Boolean.\n",
"\n",
"The `is_rabin()` and `is_streett()` methods, however, return a number of pairs. The number of pairs is always `num_sets()/2` on success, or -1 on failure."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"code = spot.parse_acc_code('Rabin 2')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
"print(acc)\n",
"print(acc.is_rabin())\n",
"print(acc.is_streett())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
"2\n",
"-1\n"
]
}
],
"prompt_number": 42
},
{
"cell_type": "code",
"collapsed": true,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 36
"prompt_number": null
}
],
"metadata": {}