diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 8cabf0772..35b71ed6a 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -23,6 +23,8 @@ #include "reachiter.hh" #include "misc/escape.hh" #include "misc/bareword.hh" +#include +#include namespace spot { @@ -30,10 +32,83 @@ namespace spot { class dotty_bfs : public ta_reachable_iterator_breadth_first { + void + parse_opts(const char* options) + { + const char* orig = options; + while (char c = *options++) + switch (c) + { + case '.': + { + // Copy the value in a string, so future calls to + // parse_opts do not fail if the environment has + // changed. (This matters particularly in an ipython + // notebook, where it is tempting to redefine + // SPOT_DOTDEFAULT.) + static std::string def = []() + { + auto s = getenv("SPOT_DOTDEFAULT"); + return s ? s : ""; + }(); + // Prevent infinite recursions... + if (orig == def.c_str()) + throw std::runtime_error + (std::string("SPOT_DOTDEFAULT should not contain '.'")); + if (!def.empty()) + parse_opts(def.c_str()); + break; + } + case 'A': + opt_hide_sets_ = true; + break; + case 'c': + opt_circles_ = true; + break; + case 'h': + opt_horizontal_ = true; + break; + case 'f': + if (*options != '(') + throw std::runtime_error + (std::string("invalid font specification for dotty()")); + { + auto* end = strchr(++options, ')'); + if (!end) + throw std::runtime_error + (std::string("invalid font specification for dotty()")); + opt_font_ = std::string(options, end - options); + options = end + 1; + } + break; + case 'v': + opt_horizontal_ = false; + break; + case 'a': + case 'b': + case 'n': + case 'N': + case 'r': + case 'R': + case 's': + case 't': + // All these options are implemented by dotty() on TGBA, + // but are not implemented here. We simply ignore them, + // because raising an exception if they are in + // SPOT_DEFAULT would be annoying. + break; + default: + throw std::runtime_error + (std::string("unknown option for dotty(): ") + c); + } + } + public: - dotty_bfs(std::ostream& os, const const_ta_ptr& a) : + dotty_bfs(std::ostream& os, const const_ta_ptr& a, + const char* opt) : ta_reachable_iterator_breadth_first(a), os_(os) { + parse_opts(opt ? opt : "."); } void @@ -41,6 +116,16 @@ namespace spot { os_ << "digraph G {\n"; + if (opt_horizontal_) + os_ << " rankdir=LR\n"; + if (opt_circles_) + os_ << " node [shape=\"circle\"]\n"; + if (!opt_font_.empty()) + os_ << " fontname=\"" << opt_font_ + << "\"\n node [fontname=\"" << opt_font_ + << "\"]\n edge [fontname=\"" << opt_font_ + << "\"]\n"; + // Always copy the environment variable into a static string, // so that we (1) look it up once, but (2) won't crash if the // environment is changed. @@ -120,8 +205,12 @@ namespace spot if (label.empty()) label = "{}"; - label += "\n"; - label += t_automata_->acc().format(si->current_acceptance_conditions()); + if (!opt_hide_sets_) + { + label += "\n"; + label += t_automata_->acc(). + format(si->current_acceptance_conditions()); + } os_ << " " << in << " -> " << out << " [label=\""; escape_str(os_, label); @@ -131,14 +220,19 @@ namespace spot private: std::ostream& os_; spot::state* artificial_initial_state_; + + bool opt_horizontal_ = true; + bool opt_circles_ = false; + bool opt_hide_sets_ = false; + std::string opt_font_; }; } std::ostream& - dotty_reachable(std::ostream& os, const const_ta_ptr& a) + dotty_reachable(std::ostream& os, const const_ta_ptr& a, const char* opt) { - dotty_bfs d(os, a); + dotty_bfs d(os, a, opt); d.run(); return os; } diff --git a/src/taalgos/dotty.hh b/src/taalgos/dotty.hh index f66faaefa..ee4a538a7 100644 --- a/src/taalgos/dotty.hh +++ b/src/taalgos/dotty.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -25,5 +25,6 @@ namespace spot { SPOT_API std::ostream& - dotty_reachable(std::ostream& os, const const_ta_ptr& a); + dotty_reachable(std::ostream& os, const const_ta_ptr& a, + const char* opt = nullptr); } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 727797b72..fc38d3808 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -410,7 +410,8 @@ namespace spot build_ta(const ta_explicit_ptr& ta, bdd atomic_propositions_set_, bool degeneralized, bool single_pass_emptiness_check, - bool artificial_livelock_state_mode) + bool artificial_livelock_state_mode, + bool no_livelock) { std::stack todo; @@ -517,6 +518,9 @@ namespace spot delete tgba_succ_it; } + if (no_livelock) + return ta; + state_ta_explicit* artificial_livelock_acc_state = 0; trace << "*** build_ta: artificial_livelock_acc_state_mode = ***" @@ -541,8 +545,10 @@ namespace spot ta_explicit_ptr tgba_to_ta(const const_tgba_ptr& tgba_, bdd atomic_propositions_set_, - bool degeneralized, bool artificial_initial_state_mode, - bool single_pass_emptiness_check, bool artificial_livelock_state_mode) + bool degeneralized, bool artificial_initial_state_mode, + bool single_pass_emptiness_check, + bool artificial_livelock_state_mode, + bool no_livelock) { ta_explicit_ptr ta; @@ -563,7 +569,8 @@ namespace spot // build ta automaton build_ta(ta, atomic_propositions_set_, degeneralized, - single_pass_emptiness_check, artificial_livelock_state_mode); + single_pass_emptiness_check, artificial_livelock_state_mode, + no_livelock); // (degeneralized=true) => TA if (degeneralized) @@ -607,7 +614,7 @@ namespace spot // build a Generalized TA automaton involving a single_pass_emptiness_check // (without an artificial livelock state): auto ta = tgta->get_ta(); - build_ta(ta, atomic_propositions_set_, false, true, false); + build_ta(ta, atomic_propositions_set_, false, true, false, false); trace << "***tgba_to_tgbta: POST build_ta***" << std::endl; diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index 9bf23d607..8ad671c3f 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -75,6 +75,9 @@ namespace spot /// Buchi-accepting state, then s has no successors. A STA product requires /// only one-pass emptiness check algorithm (see spot::ta_check::check) /// + /// \param no_livelock when set, this disable the replacement of + /// stuttering components by livelock states. Use this flag to + /// demonstrate an intermediate step of the construction. /// /// \return A spot::ta_explicit that recognizes the same language as the /// TGBA \a tgba_to_convert. @@ -83,7 +86,8 @@ namespace spot bool degeneralized = true, bool artificial_initial_state_mode = true, bool single_pass_emptiness_check = false, - bool artificial_livelock_state_mode = false); + bool artificial_livelock_state_mode = false, + bool no_livelock = false); /// \ingroup tgba_ta /// \brief Build a spot::tgta_explicit* (TGTA) from an LTL formula. diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 958083efc..dd99099ce 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -381,6 +381,7 @@ namespace spot return g_.new_transition(src, dst, cond); } +#ifndef SWIG auto out(unsigned src) const SPOT_RETURN(g_.out(src)); auto out(unsigned src) @@ -403,6 +404,7 @@ namespace spot auto is_dead_transition(const graph_t::trans_storage_t& t) const SPOT_RETURN(g_.is_dead_transition(t)); +#endif virtual bdd compute_support_conditions(const state* s) const { diff --git a/wrap/python/spot.py b/wrap/python/spot.py index e9c60254c..3427be03d 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -46,6 +46,7 @@ def _render_automaton_as_svg(a, opt=None): return _ostream_to_svg(ostr) tgba._repr_svg_ = _render_automaton_as_svg +ta._repr_svg_ = _render_automaton_as_svg def _render_formula_as_svg(a): # Load the SVG function only if we need it. This way the bindings @@ -56,13 +57,14 @@ def _render_formula_as_svg(a): dotty(ostr, a) return SVG(_ostream_to_svg(ostr)) -def _render_tgba_as_svg(a, opt=None): +def _return_automaton_as_svg(a, opt=None): # Load the SVG function only if we need it. This way the bindings # can still be used outside of IPython if IPython is not # installed. from IPython.display import SVG return SVG(_render_automaton_as_svg(a, opt)) -tgba.show = _render_tgba_as_svg +tgba.show = _return_automaton_as_svg +ta.show = _return_automaton_as_svg def _formula_str_ctor(self, str): self.this = parse_formula(str) diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index dff3566f8..65928e6f2 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -135,6 +135,7 @@ namespace std { #include "tgbaalgos/isdet.hh" #include "tgbaalgos/simulation.hh" #include "tgbaalgos/postproc.hh" +#include "tgbaalgos/product.hh" #include "tgbaalgos/stutter.hh" #include "tgbaalgos/translate.hh" #include "tgbaalgos/hoa.hh" @@ -225,7 +226,14 @@ using namespace spot; %include "ltlparse/public.hh" + /* these must come before apcollect.hh */ %include "tgba/bdddict.hh" +%include "tgba/bddprint.hh" +%include "tgba/fwd.hh" +%feature("flatnested") spot::acc_cond::mark_t; +%feature("flatnested") spot::acc_cond::acc_code; +%include "tgba/acc.hh" +%include "tgba/tgba.hh" %include "ltlvisit/apcollect.hh" %include "ltlvisit/dotty.hh" @@ -243,21 +251,9 @@ using namespace spot; // Help SWIG with namespace lookups. #define ltl spot::ltl -%include "tgba/bddprint.hh" -%include "tgba/fwd.hh" -%feature("flatnested") spot::acc_cond::mark_t; -%include "tgba/acc.hh" -%include "tgba/tgba.hh" %include "tgba/taatgba.hh" %include "tgba/tgbaproduct.hh" - -// We won't parse tgba_digraph, so just pretend it is a subclass of tgba. -%nodefaultctor spot::tgba_digraph; -namespace spot { - class tgba_digraph: public tgba - { - }; -} +%include "tgba/tgbagraph.hh" // Should come after the definition of tgba_digraph @@ -280,6 +276,7 @@ namespace spot { %include "tgbaalgos/isdet.hh" %include "tgbaalgos/simulation.hh" %include "tgbaalgos/postproc.hh" +%include "tgbaalgos/product.hh" %include "tgbaalgos/stutter.hh" %include "tgbaalgos/translate.hh" %include "tgbaalgos/hoa.hh" diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 477fdc79d..7dc5e3117 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -47,4 +47,5 @@ TESTS = \ piperead.ipynb \ randaut.ipynb \ randltl.ipynb \ - setxor.py + setxor.py \ + testingaut.ipynb diff --git a/wrap/python/tests/testingaut.ipynb b/wrap/python/tests/testingaut.ipynb new file mode 100644 index 000000000..804cbf41f --- /dev/null +++ b/wrap/python/tests/testingaut.ipynb @@ -0,0 +1,657 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:89d455537d395ae2842b209c6c14a262e15747fd501a731df0cd235f8c95011f" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import os\n", + "from IPython.display import display, HTML\n", + "# Note that Spot (loaded by the kernel) will store a copy of\n", + "# the environment variables the first time it reads them, so\n", + "# if you change those variables, the new values will be ignored\n", + "# until you restart the kernel.\n", + "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n", + "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n", + "import spot" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To translate a formula into a Testing Automaton\n", + "\n", + "Start by building a Buchi automaton" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.formula('a U Gb')\n", + "a = f.translate('ba')\n", + "a" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1eb80416f0> >" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Then, gather all the atomic proposition in the formula, and create an automaton with changesets" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "propset = spot.atomic_prop_collect_as_bdd(f, a)\n", + "ta = spot.tgba_to_ta(a, propset, True, True, False, False, True)\n", + "ta.show('.A')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "init\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1\n", + "!a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3\n", + "\n", + "1\n", + "a & b\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "1\n", + "a & !b\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "0\n", + "a & b\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "0\n", + "!a & b\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "0\n", + "a & !b\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "0\n", + "!a & !b\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "3->8\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "9\n", + "\n", + "1\n", + "!a & !b\n", + "\n", + "\n", + "3->9\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "4->9\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "{}\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by `{}`), marking as *livelock accepting* (rectangles) any states from which there exists a an accepting path labeled by `{}`." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "ta = spot.tgba_to_ta(a, propset, True, True, False, False, False)\n", + "ta.show('.A')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "init\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1\n", + "!a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3\n", + "\n", + "1\n", + "a & b\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "1\n", + "a & !b\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "0\n", + "a & b\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "0\n", + "!a & b\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Finally, use bisimulation to minimize the number of states." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.minimize_ta(ta).show('.A')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "init\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "1\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "{a, b}\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "{b}\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "{a}\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [] + } + ], + "metadata": {} + } + ] +} \ No newline at end of file