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

acc: introduce top_conjuncts() and top_disjuncts()

Browse source 
* spot/twa/acc.cc, spot/twa/acc.hh: Add the new functions.
* python/spot/impl.i: Add bindings.
* tests/python/acc_cond.ipynb: Add tests.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2019-03-22 13:50:05 +01:00
parent 55c50c65c8
commit 510a18b156
5 changed files with 202 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -20,6 +20,10 @@ 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 |.
Bugs fixed:
- When processing CSV files with MSDOS-style \r\n line endings,

1
python/spot/impl.i
View file

@ -473,6 +473,7 @@ namespace std {
%template(vectorformula) vector<spot::formula>;
%template(vectorunsigned) vector<unsigned>;
%template(vectorpairunsigned) vector<pair<unsigned, unsigned>>;
%template(vectoracccode) vector<spot::acc_cond::acc_code>;
%template(vectorbool) vector<bool>;
%template(vectorbdd) vector<bdd>;
%template(vectorstring) vector<string>;

70
spot/twa/acc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -1232,6 +1232,74 @@ namespace spot
return rescode;
}
namespace
{
static std::vector<acc_cond::acc_code>
top_clauses(const acc_cond::acc_code& code,
acc_cond::acc_op connect, acc_cond::acc_op inf_fin)
{
std::vector<acc_cond::acc_code> res;
if (!code.empty())
{
auto pos = &code.back();
auto start = &code.front();
assert(pos - pos->sub.size == start);
if (pos->sub.op == connect)
{
do
{
--pos;
if (pos->sub.op == inf_fin)
{
for (unsigned d: pos[-1].mark.sets())
{
acc_cond::acc_code tmp;
tmp.resize(2);
tmp[0].mark = {d};
tmp[1].sub.op = inf_fin;
tmp[1].sub.size = 1;
res.emplace_back(tmp);
}
}
else
{
res.emplace_back(pos);
}
pos -= pos->sub.size;
}
while (pos > start);
return res;
}
if (pos->sub.op == inf_fin)
{
for (unsigned d: pos[-1].mark.sets())
{
acc_cond::acc_code tmp;
tmp.resize(2);
tmp[0].mark = {d};
tmp[1].sub.op = inf_fin;
tmp[1].sub.size = 1;
res.emplace_back(tmp);
}
return res;
}
}
res.emplace_back(code);
return res;
}
}
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> acc_cond::acc_code::top_conjuncts() const
{
return top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf);
}
std::pair<bool, acc_cond::mark_t>
acc_cond::sat_unsat_mark(bool sat) const
{

23
spot/twa/acc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -1120,6 +1120,27 @@ namespace spot
/// This implementation is the dual of `to_dnf()`.
acc_code to_cnf() const;
/// \brief Return the top-level disjuncts.
///
/// For instance, if the formula is
/// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns
/// [Fin(0), Fin(1), 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_code> top_disjuncts() const;
/// \brief Return the top-level conjuncts.
///
/// For instance, if the formula is
/// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns
/// [Fin(0), Fin(1), 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_code> top_conjuncts() const;
/// \brief Complement an acceptance formula.
///
/// Also known as "dualizing the acceptance condition" since

177
tests/python/acc_cond.ipynb
View file

@ -821,14 +821,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"# `acc_cond`\n",
"\n",
"Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
"This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets. We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
"\n",
"It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1. The extra two sets will have no impact on the language, even if they are used in the automaton.\n",
"\n",
"The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that. But for the purpose of this notebook, let's do it:"
"If the top-level operators is a conjunct or disjunct, the following methods returns lists of clauses."
]
},
{
@ -837,26 +830,40 @@
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 33,
"metadata": {},
"output_type": "execute_result"
"name": "stdout",
"output_type": "stream",
"text": [
"spot.acc_code(\"(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))\")\n",
"(spot.acc_code(\"Fin(0)\"), spot.acc_code(\"Fin(3)\"), spot.acc_code(\"Inf(1) & Fin(2)\"))\n",
"spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\")\n",
"(spot.acc_code(\"Inf(0)\"), spot.acc_code(\"Inf(1)\"), spot.acc_code(\"Fin(2)|Fin(3)\"))\n",
"(spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\"),)\n"
]
}
],
"source": [
"acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
"acc"
"c = spot.acc_code('Fin(0)|(Inf(1)&Fin(2))|Fin(3)')\n",
"print(repr(c))\n",
"print(c.top_disjuncts())\n",
"c = spot.acc_code('Inf(0)&Inf(1)&(Fin(2)|Fin(3))')\n",
"print(repr(c))\n",
"print(c.top_conjuncts())\n",
"# Nothing to split here as the top operator is not a disjunction\n",
"print(c.top_disjuncts())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For convenience, you can pass the string directly:"
"# `acc_cond`\n",
"\n",
"Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
"This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets. We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
"\n",
"It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1. The extra two sets will have no impact on the language, even if they are used in the automaton.\n",
"\n",
"The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that. But for the purpose of this notebook, let's do it:"
]
},
{
@ -876,10 +883,17 @@
}
],
"source": [
"acc = spot.acc_cond(4, 'Rabin 2')\n",
"acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For convenience, you can pass the string directly:"
]
},
{
"cell_type": "code",
"execution_count": 35,
@ -888,7 +902,7 @@
{
"data": {
"text/plain": [
"4"
"spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 35,
@ -897,7 +911,8 @@
}
],
"source": [
"acc.num_sets()"
"acc = spot.acc_cond(4, 'Rabin 2')\n",
"acc"
]
},
{
@ -908,7 +923,7 @@
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
"4"
]
},
"execution_count": 36,
@ -916,6 +931,26 @@
"output_type": "execute_result"
}
],
"source": [
"acc.num_sets()"
]
},
{
"cell_type": "code",
"execution_count": 37,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
]
},
"execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc.get_acceptance()"
]
@ -929,7 +964,7 @@
},
{
"cell_type": "code",
"execution_count": 37,
"execution_count": 38,
"metadata": {},
"outputs": [
{
@ -938,7 +973,7 @@
"spot.acc_cond(4, \"t\")"
]
},
"execution_count": 37,
"execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@ -950,7 +985,7 @@
},
{
"cell_type": "code",
"execution_count": 38,
"execution_count": 39,
"metadata": {},
"outputs": [
{
@ -959,7 +994,7 @@
"spot.acc_cond(6, \"t\")"
]
},
"execution_count": 38,
"execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@ -971,7 +1006,7 @@
},
{
"cell_type": "code",
"execution_count": 39,
"execution_count": 40,
"metadata": {},
"outputs": [
{
@ -980,7 +1015,7 @@
"spot.acc_cond(6, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 39,
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@ -997,34 +1032,6 @@
"Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:"
]
},
{
"cell_type": "code",
"execution_count": 40,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond('Streett 2')\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above is in fact just syntactic sugar for:"
]
},
{
"cell_type": "code",
"execution_count": 41,
@ -1041,6 +1048,34 @@
"output_type": "execute_result"
}
],
"source": [
"acc = spot.acc_cond('Streett 2')\n",
"acc"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above is in fact just syntactic sugar for:"
]
},
{
"cell_type": "code",
"execution_count": 42,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
]
},
"execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"code = spot.acc_code('Streett 2')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
@ -1056,7 +1091,7 @@
},
{
"cell_type": "code",
"execution_count": 42,
"execution_count": 43,
"metadata": {},
"outputs": [
{
@ -1065,7 +1100,7 @@
"spot.acc_cond(4, \"Inf(0)&Inf(1)&Inf(2)&Inf(3)\")"
]
},
"execution_count": 42,
"execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@ -1085,7 +1120,7 @@
},
{
"cell_type": "code",
"execution_count": 43,
"execution_count": 44,
"metadata": {},
"outputs": [
{
@ -1118,7 +1153,7 @@
},
{
"cell_type": "code",
"execution_count": 44,
"execution_count": 45,
"metadata": {},
"outputs": [
{
@ -1147,7 +1182,7 @@
},
{
"cell_type": "code",
"execution_count": 45,
"execution_count": 46,
"metadata": {},
"outputs": [
{
@ -1179,7 +1214,7 @@
},
{
"cell_type": "code",
"execution_count": 46,
"execution_count": 47,
"metadata": {},
"outputs": [
{
@ -1209,7 +1244,7 @@
},
{
"cell_type": "code",
"execution_count": 47,
"execution_count": 48,
"metadata": {},
"outputs": [
{
@ -1234,7 +1269,7 @@
},
{
"cell_type": "code",
"execution_count": 48,
"execution_count": 49,
"metadata": {},
"outputs": [
{
@ -1243,7 +1278,7 @@
"spot.mark_t([0, 1, 2, 3])"
]
},
"execution_count": 48,
"execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@ -1262,7 +1297,7 @@
},
{
"cell_type": "code",
"execution_count": 49,
"execution_count": 50,
"metadata": {},
"outputs": [
{
@ -1292,7 +1327,7 @@
},
{
"cell_type": "code",
"execution_count": 50,
"execution_count": 51,
"metadata": {},
"outputs": [
{
@ -1311,7 +1346,7 @@
},
{
"cell_type": "code",
"execution_count": 51,
"execution_count": 52,
"metadata": {},
"outputs": [
{
@ -1331,7 +1366,7 @@
},
{
"cell_type": "code",
"execution_count": 52,
"execution_count": 53,
"metadata": {},
"outputs": [
{
@ -1366,7 +1401,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.7"
"version": "3.7.3rc1"
}
},
"nbformat": 4,