diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index bf093e168e12daccfb5fe92b4709de6d94691eb3..865a45ef688d54684e3d6b16efa7236eed63f63f 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -318,10 +318,15 @@ namespace spot return format_state(state_number(st)); } - twa_graph_edge_data& edge_data(const twa_succ_iterator* it) + unsigned edge_number(const twa_succ_iterator* it) const { auto* i = down_cast*>(it); - return g_.edge_data(i->pos()); + return i->pos(); + } + + twa_graph_edge_data& edge_data(const twa_succ_iterator* it) + { + return g_.edge_data(edge_number(it)); } twa_graph_edge_data& edge_data(unsigned t) @@ -331,8 +336,7 @@ namespace spot const twa_graph_edge_data& edge_data(const twa_succ_iterator* it) const { - auto* i = down_cast*>(it); - return g_.edge_data(i->pos()); + return g_.edge_data(edge_number(it)); } const twa_graph_edge_data& edge_data(unsigned t) const @@ -342,8 +346,7 @@ namespace spot edge_storage_t& edge_storage(const twa_succ_iterator* it) { - auto* i = down_cast*>(it); - return g_.edge_storage(i->pos()); + return g_.edge_storage(edge_number(it)); } edge_storage_t& edge_storage(unsigned t) @@ -354,8 +357,7 @@ namespace spot const edge_storage_t edge_storage(const twa_succ_iterator* it) const { - auto* i = down_cast*>(it); - return g_.edge_storage(i->pos()); + return g_.edge_storage(edge_number(it)); } const edge_storage_t edge_storage(unsigned t) const diff --git a/spot/twaalgos/copy.cc b/spot/twaalgos/copy.cc index d4ec62aa1c6fc6f4a66c7055b5b00d5c2e15f124..9461411d752e50c1ff713803b3375e6be1d7293b 100644 --- a/spot/twaalgos/copy.cc +++ b/spot/twaalgos/copy.cc @@ -34,12 +34,36 @@ namespace spot out->copy_acceptance_of(aut); out->copy_ap_of(aut); out->prop_copy(aut, p); + std::vector* names = nullptr; std::set* incomplete = nullptr; + + // Old highlighting maps + typedef std::map hmap; + hmap* ohstates = nullptr; + hmap* ohedges = nullptr; + const_twa_graph_ptr aut_g = nullptr; + // New highlighting maps + hmap* nhstates = nullptr; + hmap* nhedges = nullptr; + if (preserve_names) { names = new std::vector; out->set_named_prop("state-names", names); + + // If the input is a twa_graph and we were asked to preserve + // names, also preserve highlights. + aut_g = std::dynamic_pointer_cast(aut); + if (aut_g) + { + ohstates = aut->get_named_prop("highlight-states"); + if (ohstates) + nhstates = out->get_or_set_named_prop("highlight-states"); + ohedges = aut->get_named_prop("highlight-edges"); + if (ohedges) + nhedges = out->get_or_set_named_prop("highlight-edges"); + } } // States already seen. @@ -56,6 +80,12 @@ namespace spot todo.push_back(p.first); if (names) names->push_back(aut->format_state(s)); + if (ohstates) + { + auto q = ohstates->find(aut_g->state_number(s)); + if (q != ohstates->end()) + nhstates->emplace(p.first->second, q->second); + } } else { @@ -73,6 +103,7 @@ namespace spot todo.pop_front(); for (auto* t: aut->succ(src1)) { + unsigned edgenum = 0; if (SPOT_UNLIKELY(max_states < out->num_states())) { // If we have reached the max number of state, never try @@ -85,11 +116,18 @@ namespace spot incomplete->insert(src2); continue; } - out->new_edge(src2, i->second, t->cond(), t->acc()); + edgenum = out->new_edge(src2, i->second, t->cond(), t->acc()); } else { - out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc()); + edgenum = + out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc()); + } + if (ohedges) + { + auto q = ohedges->find(aut_g->edge_number(t)); + if (q != ohedges->end()) + nhedges->emplace(edgenum, q->second); } } } diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 49703bf95c841dd5bcdbc3748e1fcad8a51c1384..4f79a6fcae7c87ec9d5fdfbf3ebf8dc9fd65dd99 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:f8755e90b26b56799cf6192d76999196f60eefa8307d0d104b73f476904754cc" + "signature": "sha256:024df96495fac2f6862d63f78750ad9279a60f4e73ad02643779e5dc6a1f1982" }, "nbformat": 3, "nbformat_minor": 0, @@ -155,7 +155,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -255,7 +255,7 @@ "\n" ], "text": [ - " *' at 0x7f859c0838a0> >" + " *' at 0x7fe2a40ed8a0> >" ] } ], @@ -357,7 +357,7 @@ "\n" ], "text": [ - " *' at 0x7f8595d88f60> >" + " *' at 0x7fe2a4061f90> >" ] } ], @@ -367,7 +367,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Saving the HOA 1.1\n", + "# Saving to HOA 1.1\n", "\n", "When saving to HOA format, the highlighting is only output if version 1.1 of the format is selected, because the headers `spot.highlight.edges` and `spot.highlight.states` contain dots, which are disallowed in version 1. Compare these two outputs:" ] @@ -572,7 +572,7 @@ "\n" ], "text": [ - " *' at 0x7f8595d88fc0> >" + " *' at 0x7fe2a8edf0f0> >" ] } ], @@ -751,7 +751,7 @@ "\n" ], "text": [ - " *' at 0x7f8595d88fc0> >" + " *' at 0x7fe2a8edf0f0> >" ] } ], @@ -831,7 +831,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e090> >" + " *' at 0x7fe2a8edf090> >" ] }, { @@ -877,7 +877,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e060> >" + " *' at 0x7fe2a8edf030> >" ] } ], @@ -963,7 +963,7 @@ "\n" ], "text": [ - " *' at 0x7f8595d88d20> >" + " *' at 0x7fe2a4061fc0> >" ] } ], @@ -1088,7 +1088,7 @@ "\n" ], "text": [ - " *' at 0x7f8595d88d20> >" + " *' at 0x7fe2a4061fc0> >" ] }, { @@ -1145,7 +1145,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e090> >" + " *' at 0x7fe2a8edf090> >" ] }, { @@ -1191,7 +1191,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e060> >" + " *' at 0x7fe2a8edf030> >" ] } ], @@ -1398,7 +1398,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e120> >" + " *' at 0x7fe2a8edf150> >" ] }, { @@ -1472,7 +1472,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e0f0> >" + " *' at 0x7fe2a8edf120> >" ] }, { @@ -1556,7 +1556,7 @@ "\n" ], "text": [ - " *' at 0x7f85a187e150> >" + " *' at 0x7fe2a8edf180> >" ] } ], @@ -1702,11 +1702,186 @@ "\n" ], "text": [ - " *' at 0x7f85a187e240> >" + " *' at 0x7fe2a8edf270> >" ] } ], "prompt_number": 17 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Highlighting with partial output\n", + "\n", + "For simplicity, rendering of partial automata is actually implemented by copying the original automaton and marking some states as \"incomplete\". This also allows the same display code to work with automata generated on-the-fly. However since there is a copy, propagating the highlighting information requires extra work. Let's make sure it has been done:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "display(b.show('.<4'), b.show('.<2'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "u1\n", + "\n", + "...\n", + "\n", + "\n", + "1->u1\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", + "2->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "u1\n", + "\n", + "...\n", + "\n", + "\n", + "1->u1\n", + "\n", + "\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 18 } ], "metadata": {}