From 288b1c79586472828d31e74dfd2de0708c0ce86a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jun 2022 23:43:07 +0200 Subject: [PATCH] contains: generalize second argument to a twa 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. --- NEWS | 5 ++++ THANKS | 1 + spot/twaalgos/contains.cc | 6 ++--- spot/twaalgos/contains.hh | 11 +++++--- tests/python/ltsmin-pml.ipynb | 51 ++++++++++++++++++++++++++--------- 5 files changed, 56 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index 307cc4a3a..a1e2361f5 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/THANKS b/THANKS index 8a9c1b630..c53a0aafb 100644 --- a/THANKS +++ b/THANKS @@ -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 diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index 6c76249d5..cf2680d01 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -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); } diff --git a/spot/twaalgos/contains.hh b/spot/twaalgos/contains.hh index 61c53076a..a1d64f1b1 100644 --- a/spot/twaalgos/contains.hh +++ b/spot/twaalgos/contains.hh @@ -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); /// @} diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb index 120ab11f5..5d25b207f 100644 --- a/tests/python/ltsmin-pml.ipynb +++ b/tests/python/ltsmin-pml.ipynb @@ -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 @@ "\n" ], "text/plain": [ - " *' at 0x7fb7d8049450> >" + " *' 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,