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

python: better binding for is_parity()

Browse source 
* wrap/python/spot_impl.i: Here.
* wrap/python/tests/acc_cond.ipynb: Document it.
* spot/twa/acc.cc (is_parity): Always initialize max.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-17 11:46:46 +01:00
parent fd6ad9913f
commit 15131e74f2
3 changed files with 124 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

5
spot/twa/acc.cc
View file

@ -685,7 +685,10 @@ namespace spot
odd = !u_inf.has(0);
for (auto s: u_inf.sets())
if ((s & 1) != odd)
return false;
{
max = false; // just so the value is not uninitialized
return false;
}
auto max_code = acc_code::parity(true, odd, sets);
if (max_code == code_)

26
wrap/python/spot_impl.i
View file

@ -221,8 +221,9 @@ namespace swig
// For spot::emptiness_check_instantiator::construct and any other
// function that return errors via a "char **err" argument.
%typemap(in, numinputs=0) char** OUTPUT (char* temp)
"$1 = &temp;";
%typemap(in, numinputs=0) char** OUTPUT (char* temp) {
$1 = &temp;
}
%typemap(argout) char** OUTPUT {
PyObject *obj = SWIG_FromCharPtr(*$1);
if (!$result) {
@ -239,13 +240,32 @@ namespace swig
$result = PyList_New(1);
PyList_SetItem($result, 0, o2);
}
PyList_Append($result,obj);
PyList_Append($result, obj);
Py_DECREF(obj);
}
};
%apply char** OUTPUT { char** err };
// This is mainly for acc_cond::is_parity()
%typemap(in, numinputs=0) bool& (bool temp) {
$1 = &temp;
};
%typemap(argout) bool& {
PyObject *obj = SWIG_From_bool(*$1);
if (!$result) {
$result = obj;
} else {
if (!PyList_Check($result)) {
PyObject *o2 = $result;
$result = PyList_New(1);
PyList_SetItem($result, 0, o2);
}
PyList_Append($result, obj);
Py_DECREF(obj);
}
};
// Allow None to be passed for formula. Some functions like
// postprocessor::run() take an optional formula that defaults to
// nullptr. So it make sense to have function that take formulas that

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

@ -17,7 +17,8 @@
"pygments_lexer": "ipython3",
"version": "3.4.3+"
},
"name": ""
"name": "",
"signature": "sha256:bcc334639d07643d72b406a76d5aa91c5accb4e05a55128c0f909ad73b4b2491"
},
"nbformat": 3,
"nbformat_minor": 0,
@ -1085,7 +1086,7 @@
"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:"
"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 4 acceptance sets are used. So the following behavior should not be surprising:"
]
},
{
@ -1148,17 +1149,108 @@
],
"prompt_number": 42
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The check for parity acceptance returns three Boolean in a list of the form `[matched, max?, odd?]`. If `matched` is `False`, the other values should be ignored."
]
},
{
"cell_type": "code",
"collapsed": true,
"collapsed": false,
"input": [
"code = spot.parse_acc_code('parity min odd 4')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
"print(acc)\n",
"print(acc.is_parity())\n",
"acc.set_generalized_buchi()\n",
"print(acc)\n",
"print(acc.is_parity())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"(4, Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))\n",
"[True, False, True]\n",
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
"[False, False, False]\n"
]
}
],
"prompt_number": 43
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`acc_cond` contains a few function for manipulating `mark_t` instances, these are typically functions that require known the total number of accepting sets declared.\n",
"\n",
"For instance complementing a `mark_t`:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"m = spot.mark_t([1, 3])\n",
"print(acc.comp(m))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"{0,2}\n"
]
}
],
"prompt_number": 44
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`all_sets()` returns a `mark_t` listing all the declared sets: "
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc.all_sets()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 45,
"text": [
"{0,1,2,3}"
]
}
],
"prompt_number": 45
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": null
"prompt_number": 45
}
],
"metadata": {}
}
]
}
}