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

contains: generalize second argument to a twa

Browse source 
This was triggered by a question from Pierre Ganty on the mailing
list.

* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc (contains):
Generalize second argument to const_twa_ptr instead of
const_twa_graph_ptr.
* NEWS: Mention this.
* tests/python/ltsmin-pml.ipynb: Show that it work.
* THANKS: Mention Pierre.
This commit is contained in:
Alexandre Duret-Lutz 2022-06-22 23:43:07 +02:00
parent be28365db4
commit 288b1c7958
5 changed files with 56 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -108,6 +108,11 @@ New in spot 2.10.6.dev (not yet released)
run with additional option to abort when the tree as an unwanted
shape, or to turn the tree into a DAG.
- contains() can now take a twa as a second argument, not just a
twa_graph. This allows for instance to do contains(ltl, kripke)
to obtain a simple model checker (that returns true or false,
without counterexample).
New in spot 2.10.6 (2022-05-18)
Bugs fixed:

1
THANKS
View file

@ -44,6 +44,7 @@ Ming-Hsien Tsai
Nikos Gorogiannis
Ondřej Lengál
Paul Guénézan
Pierre Ganty
Reuben Rowe
Roei Nahum
Rüdiger Ehlers

6
spot/twaalgos/contains.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
// Copyright (C) 2018, 2019, 2022 Laboratoire de Recherche et Développement de
// l'Epita.
//
// This file is part of Spot, a model checking library.
@ -34,7 +34,7 @@ namespace spot
}
}
bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right)
bool contains(const_twa_graph_ptr left, const_twa_ptr right)
{
return !complement(left)->intersects(right);
}
@ -44,7 +44,7 @@ namespace spot
return contains(left, translate(right, left->get_dict()));
}
bool contains(formula left, const_twa_graph_ptr right)
bool contains(formula left, const_twa_ptr right)
{
return !translate(formula::Not(left), right->get_dict())->intersects(right);
}

11
spot/twaalgos/contains.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2018 Laboratoire de Recherche et Développement de
// Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de
// l'Epita.
//
// This file is part of Spot, a model checking library.
@ -38,10 +38,15 @@ namespace spot
/// associated to the complement of \a left. It helps if \a left
/// is a deterministic automaton or a formula (because in both cases
/// complementation is easier).
///
/// Complementation is only supported on twa_graph automata, so that
/// is the reason \a left must be a twa_graph. Right will be
/// explored on-the-fly if it is not a twa_graph.
///
/// @{
SPOT_API bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right);
SPOT_API bool contains(const_twa_graph_ptr left, const_twa_ptr right);
SPOT_API bool contains(const_twa_graph_ptr left, formula right);
SPOT_API bool contains(formula left, const_twa_graph_ptr right);
SPOT_API bool contains(formula left, const_twa_ptr right);
SPOT_API bool contains(formula left, formula right);
/// @}

51
tests/python/ltsmin-pml.ipynb
View file

@ -40,8 +40,8 @@
"SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n",
"(C) University of Twente, Formal Methods and Tools group\n",
"\n",
"Parsing tmprn9_nun3.pml...\n",
"Parsing tmprn9_nun3.pml done (0.1 sec)\n",
"Parsing tmpwot5yb9c.pml...\n",
"Parsing tmpwot5yb9c.pml done (0.0 sec)\n",
"\n",
"Optimizing graphs...\n",
" StateMerging changed 0 states/transitions.\n",
@ -84,8 +84,8 @@
" Found 2 / 2 (100.0%) Commuting actions \n",
"Generating guard dependency matrices done (0.0 sec)\n",
"\n",
"Written C code to /home/adl/git/spot/tests/python/tmprn9_nun3.pml.spins.c\n",
"Compiled C code to PINS library tmprn9_nun3.pml.spins\n",
"Written C code to /home/adl/git/spot/tests/python/tmpwot5yb9c.pml.spins.c\n",
"Compiled C code to PINS library tmpwot5yb9c.pml.spins\n",
"\n"
]
}
@ -419,7 +419,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fb7d8049450> >"
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f7f9849ee20> >"
]
},
"execution_count": 4,
@ -1120,6 +1120,33 @@
"k.show('.1K')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Since a kripke structure is a `twa`, can be used on the right-hand side of `contains`. Here we show that every path of `k` contains a step where `P_0.a < 2`."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains('F\"P_0.a < 2\"', k)"
]
},
{
"cell_type": "markdown",
"metadata": {},
@ -1132,7 +1159,7 @@
},
{
"cell_type": "code",
"execution_count": 7,
"execution_count": 8,
"metadata": {},
"outputs": [],
"source": [
@ -1141,7 +1168,7 @@
},
{
"cell_type": "code",
"execution_count": 8,
"execution_count": 9,
"metadata": {},
"outputs": [
{
@ -1173,7 +1200,7 @@
},
{
"cell_type": "code",
"execution_count": 9,
"execution_count": 10,
"metadata": {},
"outputs": [
{
@ -1239,7 +1266,7 @@
},
{
"cell_type": "code",
"execution_count": 10,
"execution_count": 11,
"metadata": {},
"outputs": [
{
@ -1251,7 +1278,7 @@
" P_0.b: int"
]
},
"execution_count": 10,
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@ -1262,7 +1289,7 @@
},
{
"cell_type": "code",
"execution_count": 11,
"execution_count": 12,
"metadata": {},
"outputs": [],
"source": [
@ -1286,7 +1313,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.2"
"version": "3.10.5"
}
},
"nbformat": 4,