From fb59cab09f39c12344a79c9d460ceb586ab256d3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 20 Jan 2017 16:33:30 +0100 Subject: [PATCH] emptiness: allow twa_run::as_twa to preserve names * spot/twaalgos/emptiness.cc, spot/twaalgos/emptiness.hh: Here. * tests/python/ltsmin-dve.ipynb: Add a test. * NEWS: Mention the change. --- NEWS | 4 + spot/twaalgos/emptiness.cc | 25 ++- spot/twaalgos/emptiness.hh | 9 +- tests/python/ltsmin-dve.ipynb | 348 ++++++++++++++++++++++++---------- 4 files changed, 276 insertions(+), 110 deletions(-) diff --git a/NEWS b/NEWS index fcbc50fbc..03cd9f9b6 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,10 @@ New in spot 2.3.0.dev (not yet released) will select the best output automaton for each formula translated. See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples. + Library: + + - spot::twa_run::as_twa() has an option to preserve state names. + Bugs fixed: - spot::otf_product() was incorrectly registering atomic diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 23fa84692..606c6d3ab 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -752,13 +752,20 @@ namespace spot } twa_graph_ptr - twa_run::as_twa() const + twa_run::as_twa(bool preserve_names) const { auto d = aut->get_dict(); auto res = make_twa_graph(d); res->copy_ap_of(aut); res->copy_acceptance_of(aut); + std::vector* names= nullptr; + if (preserve_names) + { + names = new std::vector; + res->set_named_prop("state-names", names); + } + const state* s = aut->get_init_state(); unsigned src; unsigned dst; @@ -777,6 +784,8 @@ namespace spot assert(s->compare(i->s) == 0); src = res->new_state(); seen.emplace(i->s, src); + if (names) + names->push_back(aut->format_state(s)); for (; i != l->end();) { @@ -826,7 +835,15 @@ namespace spot auto p = seen.emplace(next, 0); if (p.second) - p.first->second = res->new_state(); + { + unsigned ns = res->new_state(); + p.first->second = ns; + if (names) + { + assert(ns = names->size()); + names->push_back(aut->format_state(next)); + } + } dst = p.first->second; res->new_edge(src, dst, label, acc); diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index a9ce377b6..bbbed6390 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de +// Recherche et Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -438,7 +438,10 @@ namespace spot /// \brief Return a twa_graph_ptr corresponding to \a run /// /// Identical states are merged. - twa_graph_ptr as_twa() const; + /// + /// If \a preserve_names is set, the created states are named + /// using the format_state() result from the original state. + twa_graph_ptr as_twa(bool preserve_names = false) const; /// \brief Display a twa_run. /// diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb index 25260f98c..d08e61ef5 100644 --- a/tests/python/ltsmin-dve.ipynb +++ b/tests/python/ltsmin-dve.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.1" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:6d5d45c42cb1493863ed37f13f9c8679e93f026fa8d3b50cb87fba6914a4475f" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -276,8 +275,8 @@ "\n", "0\n", "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", @@ -287,8 +286,8 @@ "\n", "1\n", "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", @@ -298,8 +297,8 @@ "\n", "2\n", "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", @@ -309,8 +308,8 @@ "\n", "3\n", "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", @@ -320,8 +319,8 @@ "\n", "4\n", "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", @@ -336,8 +335,8 @@ "\n", "5\n", "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", @@ -347,8 +346,8 @@ "\n", "6\n", "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", @@ -358,8 +357,8 @@ "\n", "7\n", "\n", - "a=2, b=1, Q=0\n", - "...\n", + "a=2, b=1, Q=0\n", + "...\n", "\n", "\n", "3->7\n", @@ -374,8 +373,8 @@ "\n", "8\n", "\n", - "a=1, b=2, Q=0\n", - "...\n", + "a=1, b=2, Q=0\n", + "...\n", "\n", "\n", "4->8\n", @@ -400,8 +399,8 @@ "\n", "9\n", "\n", - "a=0, b=3, Q=0\n", - "...\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", "5->9\n", @@ -447,7 +446,7 @@ "\n" ], "text": [ - " *' at 0x7f2d78243480> >" + " *' at 0x7f402430f9c0> >" ] } ], @@ -475,8 +474,8 @@ "\n", "0\n", "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", @@ -486,8 +485,8 @@ "\n", "1\n", "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", @@ -497,8 +496,8 @@ "\n", "2\n", "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", @@ -508,8 +507,8 @@ "\n", "3\n", "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", @@ -519,8 +518,8 @@ "\n", "4\n", "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", @@ -535,8 +534,8 @@ "\n", "5\n", "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", @@ -546,8 +545,8 @@ "\n", "6\n", "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", @@ -557,8 +556,8 @@ "\n", "7\n", "\n", - "a=2, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", @@ -573,8 +572,8 @@ "\n", "8\n", "\n", - "a=1, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", @@ -589,8 +588,8 @@ "\n", "9\n", "\n", - "a=0, b=3, Q=0\n", - "...\n", + "a=0, b=3, Q=0\n", + "...\n", "\n", "\n", "5->9\n", @@ -600,8 +599,8 @@ "\n", "10\n", "\n", - "a=0, b=2, Q=1\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", @@ -616,8 +615,8 @@ "\n", "11\n", "\n", - "a=3, b=1, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", @@ -627,8 +626,8 @@ "\n", "12\n", "\n", - "a=2, b=2, Q=0\n", - "...\n", + "a=2, b=2, Q=0\n", + "...\n", "\n", "\n", "7->12\n", @@ -643,8 +642,8 @@ "\n", "13\n", "\n", - "a=1, b=3, Q=0\n", - "...\n", + "a=1, b=3, Q=0\n", + "...\n", "\n", "\n", "8->13\n", @@ -654,8 +653,8 @@ "\n", "14\n", "\n", - "a=1, b=2, Q=1\n", - "...\n", + "a=1, b=2, Q=1\n", + "...\n", "\n", "\n", "8->14\n", @@ -726,7 +725,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -754,8 +753,8 @@ "\n", "0\n", "\n", - "a=0, b=0, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=0, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "I->0\n", @@ -765,8 +764,8 @@ "\n", "1\n", "\n", - "a=1, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "0->1\n", @@ -776,8 +775,8 @@ "\n", "2\n", "\n", - "a=0, b=1, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=1, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "0->2\n", @@ -787,8 +786,8 @@ "\n", "3\n", "\n", - "a=2, b=0, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=0, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->3\n", @@ -798,8 +797,8 @@ "\n", "4\n", "\n", - "a=1, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "1->4\n", @@ -814,8 +813,8 @@ "\n", "5\n", "\n", - "a=0, b=2, Q=0\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=2, Q=0\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "2->5\n", @@ -825,8 +824,8 @@ "\n", "6\n", "\n", - "a=3, b=0, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "a=3, b=0, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "3->6\n", @@ -836,8 +835,8 @@ "\n", "7\n", "\n", - "a=2, b=1, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=1, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "3->7\n", @@ -852,8 +851,8 @@ "\n", "8\n", "\n", - "a=1, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "4->8\n", @@ -868,8 +867,8 @@ "\n", "9\n", "\n", - "a=0, b=3, Q=0\n", - ""a<1" & "b>2" & !dead\n", + "a=0, b=3, Q=0\n", + ""a<1" & "b>2" & !dead\n", "\n", "\n", "5->9\n", @@ -879,8 +878,8 @@ "\n", "10\n", "\n", - "a=0, b=2, Q=1\n", - ""a<1" & !"b>2" & !dead\n", + "a=0, b=2, Q=1\n", + ""a<1" & !"b>2" & !dead\n", "\n", "\n", "5->10\n", @@ -895,8 +894,8 @@ "\n", "11\n", "\n", - "a=3, b=1, Q=0\n", - "!"a<1" & !"b>2" & dead\n", + "a=3, b=1, Q=0\n", + "!"a<1" & !"b>2" & dead\n", "\n", "\n", "7->11\n", @@ -906,8 +905,8 @@ "\n", "12\n", "\n", - "a=2, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "7->12\n", @@ -922,8 +921,8 @@ "\n", "13\n", "\n", - "a=1, b=3, Q=0\n", - "!"a<1" & "b>2" & !dead\n", + "a=1, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "8->13\n", @@ -933,8 +932,8 @@ "\n", "14\n", "\n", - "a=1, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "a=1, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "8->14\n", @@ -944,8 +943,8 @@ "\n", "15\n", "\n", - "a=0, b=3, Q=1\n", - ""a<1" & "b>2" & dead\n", + "a=0, b=3, Q=1\n", + ""a<1" & "b>2" & dead\n", "\n", "\n", "9->15\n", @@ -970,8 +969,8 @@ "\n", "16\n", "\n", - "a=3, b=2, Q=0\n", - "!"a<1" & !"b>2" & !dead\n", + "a=3, b=2, Q=0\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->16\n", @@ -981,8 +980,8 @@ "\n", "17\n", "\n", - "a=2, b=3, Q=0\n", - "!"a<1" & "b>2" & !dead\n", + "a=2, b=3, Q=0\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "12->17\n", @@ -992,8 +991,8 @@ "\n", "18\n", "\n", - "a=2, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "a=2, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "12->18\n", @@ -1003,8 +1002,8 @@ "\n", "19\n", "\n", - "a=1, b=3, Q=1\n", - "!"a<1" & "b>2" & dead\n", + "a=1, b=3, Q=1\n", + "!"a<1" & "b>2" & dead\n", "\n", "\n", "13->19\n", @@ -1029,8 +1028,8 @@ "\n", "20\n", "\n", - "a=3, b=2, Q=1\n", - "!"a<1" & !"b>2" & !dead\n", + "a=3, b=2, Q=1\n", + "!"a<1" & !"b>2" & !dead\n", "\n", "\n", "16->20\n", @@ -1040,8 +1039,8 @@ "\n", "21\n", "\n", - "a=2, b=3, Q=1\n", - "!"a<1" & "b>2" & !dead\n", + "a=2, b=3, Q=1\n", + "!"a<1" & "b>2" & !dead\n", "\n", "\n", "17->21\n", @@ -1082,7 +1081,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1152,7 +1151,7 @@ "\n" ], "text": [ - " *' at 0x7f2d78197fc0> >" + " *' at 0x7f4024027150> >" ] } ], @@ -1314,7 +1313,7 @@ "\n" ], "text": [ - " *' at 0x7f2d78243360> >" + " *' at 0x7f402430ffc0> >" ] } ], @@ -1384,9 +1383,152 @@ } ], "prompt_number": 16 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Instead of `otf_product(x, y).is_empty()` we prefer to call `!x.intersects(y)`. There is also `x.intersecting_run(y)` that can be used to return a counterexample." + ] + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "def model_debug(f, m):\n", + " f = spot.formula(f)\n", + " ss = m.kripke(spot.atomic_prop_collect(f))\n", + " nf = spot.formula_Not(f).translate()\n", + " return ss.intersecting_run(nf)" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 21 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "run = model_debug('\"a<1\" R \"b > 1\"', m); run" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 23, + "text": [ + "Prefix:\n", + " a=0, b=0, Q=0\n", + " | \"a<1\" & !\"b > 1\" & !dead\n", + " a=1, b=0, Q=0\n", + " | !\"a<1\" & !\"b > 1\" & !dead\n", + " a=2, b=0, Q=0\n", + " | !\"a<1\" & !\"b > 1\" & !dead\n", + "Cycle:\n", + " a=3, b=0, Q=0\n", + " | !\"a<1\" & !\"b > 1\" & dead" + ] + } + ], + "prompt_number": 23 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This accepting run can be represented as an automaton (the `True` argument requires the state names to be preserved). This can be more readable." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "run.as_twa(True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 24, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "a=0, b=0, Q=0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "a=1, b=0, Q=0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + ""a<1" & !"b > 1" & !dead\n", + "\n", + "\n", + "2\n", + "\n", + "a=2, b=0, Q=0\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!"a<1" & !"b > 1" & !dead\n", + "\n", + "\n", + "3\n", + "\n", + "a=3, b=0, Q=0\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!"a<1" & !"b > 1" & !dead\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!"a<1" & !"b > 1" & dead\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f4024027720> >" + ] + } + ], + "prompt_number": 24 } ], "metadata": {} } ] -} \ No newline at end of file +}