diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index a3cde0f6e..8ce477a2d 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -19,9 +19,44 @@ #include #include +#include namespace spot { + + std::string twa_graph::format_state(unsigned n) const + { + if (is_univ_dest(n)) + { + std::stringstream ss; + bool notfirst = false; + for (unsigned d: univ_dests(n)) + { + if (notfirst) + ss << '&'; + notfirst = true; + ss << format_state(d); + } + return ss.str(); + } + + auto named = get_named_prop>("state-names"); + if (named && n < named->size()) + return (*named)[n]; + + auto prod = get_named_prop + >>("product-states"); + if (prod && n < prod->size()) + { + auto& p = (*prod)[n]; + std::stringstream ss; + ss << p.first << ',' << p.second; + return ss.str(); + } + + return std::to_string(n); + } + void twa_graph::release_formula_namer(namer* namer, bool keep_names) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 7c30331ed..1c41db02f 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -336,26 +336,7 @@ namespace spot return &g_.state_data(n); } - std::string format_state(unsigned n) const - { - std::stringstream ss; - if (is_univ_dest(n)) - { - bool notfirst = false; - for (unsigned d: univ_dests(n)) - { - if (notfirst) - ss << '&'; - notfirst = true; - ss << d; - } - } - else - { - ss << n; - } - return ss.str(); - } + std::string format_state(unsigned n) const; virtual std::string format_state(const state* st) const override { diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 04b9c5699..861e2282c 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3rc1" + "version": "3.5.3" }, "name": "" }, @@ -254,7 +254,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0b5ab70> >" + " *' at 0x7f304c67b690> >" ] } ], @@ -356,7 +356,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb270> >" + " *' at 0x7f304c60b2d0> >" ] } ], @@ -571,7 +571,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f304c60b150> >" ] } ], @@ -750,7 +750,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f304c60b150> >" ] } ], @@ -830,7 +830,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f304c60b870> >" ] }, { @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f304c60b840> >" ] } ], @@ -962,7 +962,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f304c60b8a0> >" ] } ], @@ -983,10 +983,10 @@ "prompt_number": 13, "text": [ "Prefix:\n", - " 0\n", + " 1,0\n", " | a & b\t{1}\n", "Cycle:\n", - " 1\n", + " 0,0\n", " | a\t{0,1}" ] } @@ -1087,7 +1087,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f304c60b8a0> >" ] }, { @@ -1144,7 +1144,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f304c60b870> >" ] }, { @@ -1190,7 +1190,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f304c60b840> >" ] } ], @@ -1397,7 +1397,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb750> >" + " *' at 0x7f304c60b6f0> >" ] }, { @@ -1471,7 +1471,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb630> >" + " *' at 0x7f304c60b690> >" ] }, { @@ -1555,7 +1555,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb2d0> >" + " *' at 0x7f304c60b810> >" ] } ], @@ -1701,7 +1701,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f304c60bab0> >" ] } ], @@ -1846,7 +1846,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f304c60bab0> >" ] } ], @@ -1989,7 +1989,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f304c60bab0> >" ] }, { @@ -2218,7 +2218,7 @@ "0\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "a\n", @@ -2229,7 +2229,7 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a & !b\n", @@ -2240,7 +2240,7 @@ "3\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "!a & b\n", @@ -2263,7 +2263,7 @@ "6\n", "\n", "\n", - "4->6\n", + "4->6\n", "\n", "\n", "!c\n", @@ -2274,69 +2274,69 @@ "7\n", "\n", "\n", - "4->7\n", + "4->7\n", "\n", "\n", "c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "!b\n", "\u2776\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "b & !c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "b & c\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "b\n", "\u2776\n", "\n", "\n", - "7->6\n", + "7->6\n", "\n", "\n", "!b & !c\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "!b & c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "a\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "a\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!a & !b\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "!a & b & !c\n", @@ -2347,25 +2347,25 @@ "5\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "!a & b & c\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "a\n", "\n", "\n", - "5->2\n", + "5->2\n", "\n", "\n", "!a & !b\n", "\n", "\n", - "5->3\n", + "5->3\n", "\n", "\n", "!a & b\n",