Commit 0d9c81a6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

acc: extend top_disjuncts and top_conjuncts to acc_cond as well

* spot/twa/acc.hh, spot/twa/acc.cc: Implement the new methods.
* python/spot/impl.i: Add bindings for vectors of acc_cond.
* tests/python/acc_cond.ipynb: Test the two methods.
* NEWS: Adjust.
parent 01edf4f8
......@@ -20,9 +20,9 @@ New in spot 2.7.2.dev (not yet released)
'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
state instead of 4.)
- acc_cond::acc_code::top_disjuncts() and
acc_cond::acc_code::top_conjuncts() can be used to split an
acceptance condition on the top-level & or |.
- acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be
used to split an acceptance condition on the top-level & or |.
These methods also exist in acc_cond::acc_code.
- minimize_obligation() learned to work on very weak automata even
if the formula or negated automaton are not supplied. (This
......
......@@ -473,6 +473,7 @@ namespace std {
%template(vectorformula) vector<spot::formula>;
%template(vectorunsigned) vector<unsigned>;
%template(vectorpairunsigned) vector<pair<unsigned, unsigned>>;
%template(vectoracccond) vector<spot::acc_cond>;
%template(vectoracccode) vector<spot::acc_cond::acc_code>;
%template(vectorbool) vector<bool>;
%template(vectorbdd) vector<bdd>;
......
......@@ -1234,12 +1234,12 @@ namespace spot
namespace
{
static std::vector<acc_cond::acc_code>
template<typename Fun>
static void
top_clauses(const acc_cond::acc_code& code,
acc_cond::acc_op connect, acc_cond::acc_op inf_fin)
acc_cond::acc_op connect, acc_cond::acc_op inf_fin,
Fun store)
{
std::vector<acc_cond::acc_code> res;
if (!code.empty())
{
auto pos = &code.back();
......@@ -1259,17 +1259,17 @@ namespace spot
tmp[0].mark = {d};
tmp[1].sub.op = inf_fin;
tmp[1].sub.size = 1;
res.emplace_back(tmp);
store(tmp);
}
}
else
{
res.emplace_back(pos);
store(pos);
}
pos -= pos->sub.size;
}
while (pos > start);
return res;
return;
}
if (pos->sub.op == inf_fin)
{
......@@ -1280,24 +1280,48 @@ namespace spot
tmp[0].mark = {d};
tmp[1].sub.op = inf_fin;
tmp[1].sub.size = 1;
res.emplace_back(tmp);
store(tmp);
}
return res;
return;
}
}
res.emplace_back(code);
return res;
store(code);
return;
}
}
std::vector<acc_cond::acc_code> acc_cond::acc_code::top_disjuncts() const
{
return top_clauses(*this, acc_cond::acc_op::Or, acc_cond::acc_op::Fin);
std::vector<acc_cond::acc_code> res;
top_clauses(*this, acc_cond::acc_op::Or, acc_cond::acc_op::Fin,
[&](const acc_cond::acc_code& c) { res.emplace_back(c); });
return res;
}
std::vector<acc_cond::acc_code> acc_cond::acc_code::top_conjuncts() const
{
return top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf);
std::vector<acc_cond::acc_code> res;
top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf,
[&](const acc_cond::acc_code& c) { res.emplace_back(c); });
return res;
}
std::vector<acc_cond> acc_cond::top_disjuncts() const
{
std::vector<acc_cond> res;
top_clauses(code_, acc_cond::acc_op::Or, acc_cond::acc_op::Fin,
[&](const acc_cond::acc_code& c)
{ res.emplace_back(num_, c); });
return res;
}
std::vector<acc_cond> acc_cond::top_conjuncts() const
{
std::vector<acc_cond> res;
top_clauses(code_, acc_cond::acc_op::And, acc_cond::acc_op::Inf,
[&](const acc_cond::acc_code& c)
{ res.emplace_back(num_, c); });
return res;
}
std::pair<bool, acc_cond::mark_t>
......
......@@ -1978,6 +1978,26 @@ namespace spot
return code_.fin_one();
}
/// \brief Return the top-level disjuncts.
///
/// For instance, if the formula is
/// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns
/// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))].
///
/// If the formula is not a disjunction, this returns
/// a vector with the formula as only element.
std::vector<acc_cond> top_disjuncts() const;
/// \brief Return the top-level conjuncts.
///
/// For instance, if the formula is
/// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns
/// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))].
///
/// If the formula is not a conjunction, this returns
/// a vector with the formula as only element.
std::vector<acc_cond> top_conjuncts() const;
protected:
mark_t all_sets_() const
{
......
......@@ -1383,6 +1383,32 @@
"print(acc)\n",
"print(acc.unsat_mark())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`top_conjuncts` and `top_disjuncts` also work on `acc_cond`. In this case they return tuple of `acc_cond` with the same number of sets."
]
},
{
"cell_type": "code",
"execution_count": 54,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\"),)\n",
"(spot.acc_cond(4, \"Fin(0) | Inf(1)\"), spot.acc_cond(4, \"Fin(2) | Inf(3)\"))\n"
]
}
],
"source": [
"print(acc.top_disjuncts())\n",
"print(acc.top_conjuncts())"
]
}
],
"metadata": {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment