From 5e07e8384d859587b19a75c1312ad3c0a43ebf22 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Oct 2015 16:45:39 +0200 Subject: [PATCH] tgba_complete: rename as complete and export in Python * src/twaalgos/complete.cc, src/twaalgos/complete.hh (tgba_complete, tgba_complete_here): Rename as... (complete, complete_here): ... these. Also fix useless output of acceptance marks on transition leading to the sink when the automaton does not use state-based acceptance. * src/tests/ikwiad.cc, src/twaalgos/dtgbacomp.cc, src/twaalgos/dtgbasat.cc, src/twaalgos/postproc.cc, src/twaalgos/product.cc: Adjust. * wrap/python/spot_impl.i: Export these function. * wrap/python/tests/automata.ipynb: Test spot.complete(). --- src/tests/ikwiad.cc | 6 +- src/twaalgos/complete.cc | 8 +- src/twaalgos/complete.hh | 14 +- src/twaalgos/dtgbacomp.cc | 2 +- src/twaalgos/dtgbasat.cc | 2 +- src/twaalgos/postproc.cc | 10 +- src/twaalgos/product.cc | 4 +- wrap/python/spot_impl.i | 2 + wrap/python/tests/automata.ipynb | 246 +++++++++++++++++++++++++++++-- 9 files changed, 257 insertions(+), 37 deletions(-) diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index ebd7e3041..e326272d4 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -1178,9 +1178,9 @@ checked_main(int argc, char** argv) if (opt_complete) { - tm.start("determinization"); - a = tgba_complete(a); - tm.stop("determinization"); + tm.start("completion"); + a = complete(a); + tm.stop("completion"); } if (opt_dtbasat >= 0) diff --git a/src/twaalgos/complete.cc b/src/twaalgos/complete.cc index 13e722862..01d103837 100644 --- a/src/twaalgos/complete.cc +++ b/src/twaalgos/complete.cc @@ -21,7 +21,7 @@ namespace spot { - unsigned tgba_complete_here(twa_graph_ptr aut) + unsigned complete_here(twa_graph_ptr aut) { unsigned n = aut->num_states(); unsigned sink = -1U; @@ -104,6 +104,8 @@ namespace spot } // In case the automaton use state-based acceptance, propagate // the acceptance of the first edge to the one we add. + if (!aut->has_state_based_acc()) + acc = 0U; aut->new_edge(i, sink, missingcond, acc); } } @@ -117,7 +119,7 @@ namespace spot return sink; } - twa_graph_ptr tgba_complete(const const_twa_ptr& aut) + twa_graph_ptr complete(const const_twa_ptr& aut) { auto res = make_twa_graph(aut, { true, // state based @@ -125,7 +127,7 @@ namespace spot true, // deterministic true, // stutter inv. }); - tgba_complete_here(res); + complete_here(res); return res; } diff --git a/src/twaalgos/complete.hh b/src/twaalgos/complete.hh index e44840ad4..d03e0a8da 100644 --- a/src/twaalgos/complete.hh +++ b/src/twaalgos/complete.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -25,15 +25,15 @@ namespace spot { /// \brief Complete a twa_graph in place. /// - /// If the tgba has no acceptance set, one will be added. The + /// If the TωA has no acceptance set, one will be added. The /// returned value is the number of the sink state (it can be a new /// state added for completion, or an existing non-accepting state /// that has been reused as sink state because it had no outgoing /// transitions apart from self-loops.) - SPOT_API unsigned tgba_complete_here(twa_graph_ptr aut); + SPOT_API unsigned complete_here(twa_graph_ptr aut); - /// \brief Clone a tgba and complete it. + /// \brief Clone a twa and complete it. /// - /// If the tgba has no acceptance set, one will be added. - SPOT_API twa_graph_ptr tgba_complete(const const_twa_ptr& aut); + /// If the twa has no acceptance set, one will be added. + SPOT_API twa_graph_ptr complete(const const_twa_ptr& aut); } diff --git a/src/twaalgos/dtgbacomp.cc b/src/twaalgos/dtgbacomp.cc index 2c02e05c6..2edb181dc 100644 --- a/src/twaalgos/dtgbacomp.cc +++ b/src/twaalgos/dtgbacomp.cc @@ -178,7 +178,7 @@ namespace spot { // Simply complete the automaton, and complement its // acceptance. - auto res = cleanup_acceptance_here(tgba_complete(aut)); + auto res = cleanup_acceptance_here(complete(aut)); res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); return res; diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 6548abeba..643cc5136 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -1339,7 +1339,7 @@ namespace spot } else { - tgba_complete_here(a); + complete_here(a); } if (states == -1 && max_states == -1) diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index fb3e3f0f6..1a7d2cfef 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -156,7 +156,7 @@ namespace spot || (type_ == Monitor && a->num_sets() == 0)) { if (COMP_) - a = tgba_complete(a); + a = complete(a); if (SBACC_) a = sbacc(a); return a; @@ -207,7 +207,7 @@ namespace spot a = m; } if (COMP_) - a = tgba_complete(a); + a = complete(a); return a; } @@ -216,7 +216,7 @@ namespace spot if (type_ == BA) a = do_degen(a); if (COMP_) - a = tgba_complete(a); + a = complete(a); if (SBACC_) a = sbacc(a); return a; @@ -380,7 +380,7 @@ namespace spot in = dba; } - const_twa_graph_ptr res = tgba_complete(in); + const_twa_graph_ptr res = complete(in); if (target_acc == 1) { if (sat_states_ != -1) @@ -457,7 +457,7 @@ namespace spot sim = dba ? dba : sim; if (COMP_) - sim = tgba_complete(sim); + sim = complete(sim); if (SBACC_) sim = sbacc(sim); diff --git a/src/twaalgos/product.cc b/src/twaalgos/product.cc index 158e4cb0d..9b6bb78c3 100644 --- a/src/twaalgos/product.cc +++ b/src/twaalgos/product.cc @@ -136,8 +136,8 @@ namespace spot unsigned left_state, unsigned right_state) { - return product_aux(tgba_complete(left), - tgba_complete(right), + return product_aux(complete(left), + complete(right), left_state, right_state, false); } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 459de7b1c..6fc2926ac 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -111,6 +111,7 @@ #include "twaalgos/dot.hh" #include "twaalgos/degen.hh" #include "twaalgos/copy.hh" +#include "twaalgos/complete.hh" #include "twaalgos/emptiness.hh" #include "twaalgos/gtec/gtec.hh" #include "twaalgos/lbtt.hh" @@ -255,6 +256,7 @@ namespace std { %include "twaalgos/degen.hh" %include "twaalgos/dot.hh" %include "twaalgos/copy.hh" +%include "twaalgos/complete.hh" %include "twaalgos/emptiness.hh" %include "twaalgos/gtec/gtec.hh" %include "twaalgos/lbtt.hh" diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index fe1028a36..d863de9a5 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -17,7 +17,8 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "" + "name": "", + "signature": "sha256:6b034a8346695a3f327fd50e8c768209ea3d931598b99d5d80508685976c255e" }, "nbformat": 3, "nbformat_minor": 0, @@ -176,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c07cf30> >" + " *' at 0x7f2998ab6540> >" ] } ], @@ -315,7 +316,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -468,7 +469,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -568,7 +569,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c065360> >" + " *' at 0x7f2998a8be40> >" ] } ], @@ -638,7 +639,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c0654b0> >" + " *' at 0x7f2998a8bed0> >" ] } ], @@ -714,7 +715,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c065270> >" + " *' at 0x7f2998a8b840> >" ] } ], @@ -837,7 +838,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1027,7 +1028,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1174,7 +1175,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c0652d0> >" + " *' at 0x7f2998a280f0> >" ] } ], @@ -1275,7 +1276,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c065150> >" + " *' at 0x7f2998a28120> >" ] } ], @@ -1393,7 +1394,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c0651e0> >" + " *' at 0x7f2998a28150> >" ] } ], @@ -1493,7 +1494,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c065300> >" + " *' at 0x7f2998a28180> >" ] } ], @@ -1967,7 +1968,7 @@ "\n" ], "text": [ - " *' at 0x7fe49c04ad80> >" + " *' at 0x7f2998a8bde0> >" ] } ], @@ -2170,7 +2171,7 @@ "\n" ], "text": [ - " *' at 0x7fe49f10ec90> >" + " *' at 0x7f2998a8bfc0> >" ] } ], @@ -2186,6 +2187,221 @@ "metadata": {}, "outputs": [], "prompt_number": 20 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.complete(a)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 21, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\u2778\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\u2778\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\u2777\n", + "\u2778\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f2998a8bea0> >" + ] + } + ], + "prompt_number": 21 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.complete(spot.translate('Ga'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 22, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f2998a281e0> >" + ] + } + ], + "prompt_number": 22 } ], "metadata": {}