acc: introduce fin_one_extract()
* spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::fin_one_extract, acc_code::acc_cond::fin_one_extract): New methods. * python/spot/impl.i: Add support for the return type. * tests/python/acc_cond.ipynb: Test them.
This commit is contained in:
Alexandre Duret-Lutz
parent
2d1cb0ddcd
commit
7fedb3dc61
4 changed files with 246 additions and 16 deletions
|
|
@ -468,6 +468,8 @@ namespace std {
|
|||
%template(liststr) list<std::string>;
|
||||
%template(pairunsigned) pair<unsigned, unsigned>;
|
||||
%template(pairmark_t) pair<spot::acc_cond::mark_t, spot::acc_cond::mark_t>;
|
||||
%template(pairintacccode) pair<int, spot::acc_cond::acc_code>;
|
||||
%template(pairintacccond) pair<int, spot::acc_cond>;
|
||||
%template(vectorformula) vector<spot::formula>;
|
||||
%template(vectorunsigned) vector<unsigned>;
|
||||
%template(vectorpairunsigned) vector<pair<unsigned, unsigned>>;
|
||||
|
|
|
|||
112
spot/twa/acc.cc
112
spot/twa/acc.cc
|
|
@ -2644,6 +2644,118 @@ namespace spot
|
|||
return -1;
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
int has_top_fin(const acc_cond::acc_word* pos, bool top = true)
|
||||
{
|
||||
if (pos->sub.op == acc_cond::acc_op::Fin)
|
||||
{
|
||||
acc_cond::mark_t m = pos[-1].mark;
|
||||
if (top || m.is_singleton())
|
||||
return m.min_set() - 1;
|
||||
}
|
||||
else if (pos->sub.op == acc_cond::acc_op::And)
|
||||
{
|
||||
auto sub = pos - pos->sub.size;
|
||||
do
|
||||
{
|
||||
--pos;
|
||||
if (int f = has_top_fin(pos, false); f >= 0)
|
||||
return f;
|
||||
pos -= pos->sub.size;
|
||||
}
|
||||
while (sub < pos);
|
||||
}
|
||||
else if (top && pos->sub.op == acc_cond::acc_op::Or)
|
||||
{
|
||||
auto sub = pos - pos->sub.size;
|
||||
do
|
||||
{
|
||||
--pos;
|
||||
if (int f = has_top_fin(pos); f >= 0)
|
||||
return f;
|
||||
pos -= pos->sub.size;
|
||||
}
|
||||
while (sub < pos);
|
||||
}
|
||||
return -1;
|
||||
}
|
||||
|
||||
bool uses_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f)
|
||||
{
|
||||
auto sub = pos - pos->sub.size;
|
||||
do
|
||||
{
|
||||
switch (pos->sub.op)
|
||||
{
|
||||
case acc_cond::acc_op::And:
|
||||
case acc_cond::acc_op::Or:
|
||||
--pos;
|
||||
break;
|
||||
case acc_cond::acc_op::Fin:
|
||||
if (pos[-1].mark & f)
|
||||
return true;
|
||||
SPOT_FALLTHROUGH;
|
||||
case acc_cond::acc_op::Inf:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
pos -= 2;
|
||||
break;
|
||||
}
|
||||
}
|
||||
while (sub < pos);
|
||||
return false;
|
||||
}
|
||||
|
||||
acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos,
|
||||
acc_cond::mark_t f)
|
||||
{
|
||||
auto start = pos - pos->sub.size;
|
||||
switch (pos->sub.op)
|
||||
{
|
||||
case acc_cond::acc_op::And:
|
||||
case acc_cond::acc_op::Fin:
|
||||
case acc_cond::acc_op::Inf:
|
||||
return pos;
|
||||
case acc_cond::acc_op::Or:
|
||||
{
|
||||
--pos;
|
||||
auto res = acc_cond::acc_code::f();
|
||||
do
|
||||
{
|
||||
if (uses_fin(pos, f))
|
||||
{
|
||||
acc_cond::acc_code tmp(pos);
|
||||
tmp |= std::move(res);
|
||||
std::swap(tmp, res);
|
||||
}
|
||||
pos -= pos->sub.size + 1;
|
||||
}
|
||||
while (pos > start);
|
||||
return res;
|
||||
}
|
||||
case acc_cond::acc_op::FinNeg:
|
||||
case acc_cond::acc_op::InfNeg:
|
||||
SPOT_UNREACHABLE();
|
||||
return {};
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
return {};
|
||||
}
|
||||
}
|
||||
|
||||
std::pair<int, acc_cond::acc_code>
|
||||
acc_cond::acc_code::fin_one_extract() const
|
||||
{
|
||||
if (is_t() || is_f())
|
||||
return {-1, *this};
|
||||
const acc_cond::acc_word* pos = &back();
|
||||
int selected_fin = has_top_fin(pos);
|
||||
if (selected_fin < 0)
|
||||
selected_fin = fin_one();
|
||||
return {selected_fin, extract_fin(pos, {(unsigned) selected_fin})};
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
bool
|
||||
|
|
|
|||
|
|
@ -1251,12 +1251,6 @@ namespace spot
|
|||
/// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
|
||||
mark_t fin_unit() const;
|
||||
|
||||
/// \brief Return one acceptance set i that appear as `Fin(i)`
|
||||
/// in the condition.
|
||||
///
|
||||
/// Return -1 if no such set exist.
|
||||
int fin_one() const;
|
||||
|
||||
/// \brief Find a `Inf(i)` that is a unit clause.
|
||||
///
|
||||
/// This return a mark_t `{i}` such that `Inf(i)` appears as a
|
||||
|
|
@ -1270,6 +1264,31 @@ namespace spot
|
|||
/// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`.
|
||||
mark_t inf_unit() const;
|
||||
|
||||
/// \brief Return one acceptance set i that appears as `Fin(i)`
|
||||
/// in the condition.
|
||||
///
|
||||
/// Return -1 if no such set exist.
|
||||
int fin_one() const;
|
||||
|
||||
/// \brief Return one acceptance set i that appears as `Fin(i)`
|
||||
/// in the condition, and all disjuncts containing it.
|
||||
///
|
||||
/// If the condition is a disjunction and one of the disjunct
|
||||
/// has the shape `...&Fin(i)&...`, then `i` will be prefered
|
||||
/// over any arbitrary Fin.
|
||||
///
|
||||
/// The second element of the pair, is the same acceptance
|
||||
/// condition in which all top-level disjunct not featuring
|
||||
/// `Fin(i)` have been removed.
|
||||
///
|
||||
/// For example on
|
||||
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))`
|
||||
/// the output would be the pair
|
||||
/// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`.
|
||||
/// On that example `Fin(1)` is prefered to `Fin(7)` because
|
||||
/// it appears at the top-level.
|
||||
std::pair<int, acc_code> fin_one_extract() const;
|
||||
|
||||
/// \brief Help closing accepting or rejecting cycle.
|
||||
///
|
||||
/// Assuming you have a partial cycle visiting all acceptance
|
||||
|
|
@ -2157,15 +2176,6 @@ namespace spot
|
|||
return code_.fin_unit();
|
||||
}
|
||||
|
||||
/// \brief Return one acceptance set i that appear as `Fin(i)`
|
||||
/// in the condition.
|
||||
///
|
||||
/// Return -1 if no such set exist.
|
||||
int fin_one() const
|
||||
{
|
||||
return code_.fin_one();
|
||||
}
|
||||
|
||||
/// \brief Find a `Inf(i)` that is a unit clause.
|
||||
///
|
||||
/// This return a mark_t `{i}` such that `Inf(i)` appears as a
|
||||
|
|
@ -2182,6 +2192,38 @@ namespace spot
|
|||
return code_.inf_unit();
|
||||
}
|
||||
|
||||
/// \brief Return one acceptance set i that appear as `Fin(i)`
|
||||
/// in the condition.
|
||||
///
|
||||
/// Return -1 if no such set exist.
|
||||
int fin_one() const
|
||||
{
|
||||
return code_.fin_one();
|
||||
}
|
||||
|
||||
/// \brief Return one acceptance set i that appears as `Fin(i)`
|
||||
/// in the condition, and all disjuncts containing it.
|
||||
///
|
||||
/// If the condition is a disjunction and one of the disjunct
|
||||
/// has the shape `...&Fin(i)&...`, then `i` will be prefered
|
||||
/// over any arbitrary Fin.
|
||||
///
|
||||
/// The second element of the pair, is the same acceptance
|
||||
/// condition in which all top-level disjunct not featuring
|
||||
/// `Fin(i)` have been removed.
|
||||
///
|
||||
/// For example on
|
||||
/// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))`
|
||||
/// the output would be the pair
|
||||
/// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`.
|
||||
/// On that example `Fin(1)` is prefered to `Fin(7)` because
|
||||
/// it appears at the top-level.
|
||||
std::pair<int, acc_cond> fin_one_extract() const
|
||||
{
|
||||
auto [f, c] = code_.fin_one_extract();
|
||||
return {f, {num_sets(), std::move(c)}};
|
||||
}
|
||||
|
||||
/// \brief Return the top-level disjuncts.
|
||||
///
|
||||
/// For instance, if the formula is
|
||||
|
|
|
|||
|
|
@ -1409,6 +1409,80 @@
|
|||
"print(acc.top_disjuncts())\n",
|
||||
"print(acc.top_conjuncts())"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"`fin_one()` return the number of one color `x` that appears as `Fin(x)` in the formula, or `-1` if the formula is Fin-less.\n",
|
||||
"\n",
|
||||
"The variant `fin_one_extract()` consider the acceptance condition as a disjunction (if the top-level operator is not a disjunction, we just assume the formula is a disjunction with only one disjunct), and return a pair `(x,c)` where `c` is the disjunction of all disjuncts of the original formula where `Fin(x)` appear. Also this function tries to choose an `x` such that one of the disjunct has the form `...&Fin(x)&...` if possible: this is visible in the third example, where 5 is prefered to 2."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 55,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))\n",
|
||||
"0\n",
|
||||
"(0, spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\"))\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"print(acc)\n",
|
||||
"print(acc.fin_one())\n",
|
||||
"print(acc.fin_one_extract())"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 56,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(6, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)))\n",
|
||||
"0\n",
|
||||
"(0, spot.acc_cond(6, \"Fin(0) & Inf(1)\"))\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"acc2 = spot.acc_cond('Rabin 3')\n",
|
||||
"print(acc2)\n",
|
||||
"print(acc2.fin_one())\n",
|
||||
"print(acc2.fin_one_extract())"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 57,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(6, (Inf(0) & (Fin(2) | Inf(3))) | (Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5))))\n",
|
||||
"2\n",
|
||||
"(5, spot.acc_cond(6, \"(Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5)))\"))\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"acc3 = spot.acc_cond('Inf(0)&(Fin(2)|Inf(3)) | Inf(4)&Fin(5) | Inf(0)&Inf(5)&(Fin(5)|Fin(0))')\n",
|
||||
"print(acc3)\n",
|
||||
"print(acc3.fin_one())\n",
|
||||
"print(acc3.fin_one_extract())"
|
||||
]
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
|
|
@ -1427,7 +1501,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.7.3rc1"
|
||||
"version": "3.9.2"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue