Commit cdfe78f1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

twa_graph: do not order BDDs by IDs in merge_edges()

Fixes #282.

* spot/misc/bddlt.hh (bdd_less_than_stable): New function.
* spot/twa/twagraph.cc (merge_edges): Use it.
* tests/core/complement.test, tests/core/degenid.test,
tests/core/ltldo.test, tests/core/prodor.test,
tests/core/readsave.test, tests/core/sbacc.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/dualize.py,
tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
tests/python/product.ipynb, tests/python/simstate.py,
tests/python/tra2tba.py: Adjust all expected outputs.
* NEWS: Mention the bug.
parent bd34f3c6
......@@ -2,6 +2,14 @@ New in spot 2.4.0.dev (not yet released)
Nothing yet.
Bugs fixed:
- The twa_graph::mege_edges() function relied on BDD IDs to sort
edges. This in turn caused some algorithm (like the
degeneralization) to produce slighltly different outputs (but
still correct outputs) depending on the BDD operations performed
before.
New in spot 2.4 (2017-09-06)
Build:
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2011, 2014, 2017 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -29,6 +29,10 @@ namespace spot
{
/// \ingroup misc_tools
/// \brief Comparison functor for BDDs.
///
/// This comparison function use BDD ids for efficiency. An
/// algorithm depending on this order may return different results
/// depending on how the BDD library has been used before.
struct bdd_less_than :
public std::binary_function<const bdd&, const bdd&, bool>
{
......@@ -39,6 +43,43 @@ namespace spot
}
};
/// \ingroup misc_tools
/// \brief Comparison functor for BDDs.
///
/// This comparison function actually check for BDD variables, so as
/// long as the variable order is the same, the output of this
/// comparison will be stable and independent on previous BDD
/// operations.
struct bdd_less_than_stable :
public std::binary_function<const bdd&, const bdd&, bool>
{
bool
operator()(const bdd& left, const bdd& right) const
{
int li = left.id();
int ri = right.id();
if (li == ri)
return false;
if (li <= 1 || ri <= 1)
return li < ri;
{
int vl = bdd_var(left);
int vr = bdd_var(right);
if (vl != vr)
return vl < vr;
}
// We check the high side before low, this way
// !a&b comes before a&!b and a&b
{
bdd hl = bdd_high(left);
bdd hr = bdd_high(right);
if (hl != hr)
return operator()(hl, hr);
return operator()(bdd_low(left), bdd_low(right));
}
}
};
/// \ingroup misc_tools
/// \brief Hash functor for BDDs.
struct bdd_hash :
......
......@@ -19,6 +19,7 @@
#include <spot/twa/twagraph.hh>
#include <spot/tl/print.hh>
#include <spot/misc/bddlt.hh>
#include <vector>
#include <deque>
......@@ -79,11 +80,11 @@ namespace spot
delete namer;
}
/// \brief Merge universal destinations
///
/// If several states have the same universal destination, merge
/// them all. Also remove unused destination, and any redundant
/// state in each destination.
/// \brief Merge universal destinations
///
/// If several states have the same universal destination, merge
/// them all. Also remove unused destination, and any redundant
/// state in each destination.
void twa_graph::merge_univ_dests()
{
auto& g = get_graph();
......@@ -198,7 +199,8 @@ namespace spot
return true;
if (lhs.dst > rhs.dst)
return false;
return lhs.cond.id() < rhs.cond.id();
bdd_less_than_stable lt;
return lt(lhs.cond, rhs.cond);
// Do not sort on acceptance, we'll merge
// them.
});
......
......@@ -62,10 +62,10 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0&1] 0 {0 1}
[!0&!1] 0
[!0&1] 0 {1}
[0&!1] 0 {0}
[0&1] 0 {0 1}
--END--
HOA: v1
States: 4
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2011, 2013, 2014, 2015, 2017 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -242,15 +242,15 @@ State: 0
[0] 1
State: 1 {0}
[1&2] 1
[!1&2] 2
[!2] 3
[!2] 2
[!1&2] 3
State: 2
[1] 1
[!1] 2
State: 3
[1&2] 1
[!1&2] 2
[!2] 3
[!2] 2
[!1&2] 3
State: 3
[1] 1
[!1] 3
--END--
EOF
diff out expected
......@@ -82,8 +82,8 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 0 {0}
[!0] 0
[0] 0 {0}
--END--
EOF
diff output expected
......@@ -103,8 +103,8 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 0 {0}
[!0] 0
[0] 0 {0}
--END--
EOF
diff output expected
......@@ -124,8 +124,8 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0 {0}
[!0] 0
[0] 0 {0}
--END--
EOF
diff output expected
......
......@@ -65,18 +65,18 @@ properties: trans-labels explicit-labels trans-acc complete
properties: stutter-invariant
--BODY--
State: 0
[0] 0 {1}
[!0] 0
[0&1] 1 {1}
[0] 0 {1}
[!0&1] 1
[0&1] 1 {1}
State: 1
[0&1] 1 {0 1}
[!0&1] 1 {0}
[0&!1] 2 {0 1}
[0&1] 1 {0 1}
[!0&!1] 2 {0}
[0&!1] 2 {0 1}
State: 2
[0] 2 {1}
[!0] 2
[0] 2 {1}
--END--
EOF
diff por.hoa exp
......@@ -96,13 +96,13 @@ Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[0] 0 {1}
[!0] 0
[0&1] 1 {1}
[0] 0 {1}
[!0&1] 1
[0&1] 1 {1}
State: 1
[0&1] 1 {0 1}
[!0&1] 1 {0}
[0&1] 1 {0 1}
--END--
EOF
diff pand.hoa exp
......
......@@ -363,10 +363,10 @@ digraph G {
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="a & b\n{0,1}"]
0 -> 0 [label="!a & !b"]
0 -> 0 [label="!a & b\n{1}"]
0 -> 0 [label="a & !b\n{0}"]
0 -> 0 [label="a & b\n{0,1}"]
}
EOF
diff output expected
......@@ -382,10 +382,10 @@ digraph G {
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="a & b\n⓿❶"]
0 -> 0 [label="!a & !b"]
0 -> 0 [label="!a & b\n❶"]
0 -> 0 [label="a & !b\n⓿"]
0 -> 0 [label="a & b\n⓿❶"]
}
EOF
diff output expected
......@@ -407,10 +407,10 @@ digraph G {
I [label="", style=invis, width=0]
I -> 0
0 [label=<0>]
0 -> 0 [label=<a &amp; b<br/>$zero$one>]
0 -> 0 [label=<!a &amp; !b>]
0 -> 0 [label=<!a &amp; b<br/>$one>]
0 -> 0 [label=<a &amp; !b<br/>$zero>]
0 -> 0 [label=<a &amp; b<br/>$zero$one>]
}
EOF
diff output expected
......
......@@ -37,26 +37,26 @@ Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 {0}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 1 {0 1}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 2
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 3 {1}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 0 {0 1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 1
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 2 {1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 3 {0}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
--END--
EOF
......
......@@ -140,29 +140,29 @@
"<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M166.467,-136.153C166.078,-145.539 166.922,-154 169,-154 170.526,-154 171.387,-149.437 171.582,-143.295\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"171.533,-136.153 174.731,-143.131 171.557,-139.653 171.581,-143.153 171.581,-143.153 171.581,-143.153 171.557,-139.653 168.431,-143.174 171.533,-136.153 171.533,-136.153\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-172.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M165.104,-135.577C162.424,-156.718 163.723,-184 169,-184 173.7,-184 175.244,-162.36 173.633,-142.691\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"172.896,-135.577 176.75,-142.215 173.257,-139.059 173.617,-142.54 173.617,-142.54 173.617,-142.54 173.257,-139.059 170.484,-142.864 172.896,-135.577 172.896,-135.577\"/>\n",
"<text text-anchor=\"start\" x=\"148.5\" y=\"-187.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M164.828,-135.699C162.523,-152.996 163.914,-172 169,-172 173.371,-172 175.012,-157.965 173.925,-143.04\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"173.172,-135.699 177.02,-142.341 173.529,-139.181 173.886,-142.663 173.886,-142.663 173.886,-142.663 173.529,-139.181 170.753,-142.984 173.172,-135.699 173.172,-135.699\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-175.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M164.049,-135.467C158.901,-163.149 160.551,-202 169,-202 176.756,-202 178.783,-169.261 175.081,-142.477\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"173.951,-135.467 178.174,-141.877 174.508,-138.923 175.065,-142.378 175.065,-142.378 175.065,-142.378 174.508,-138.923 171.955,-142.879 173.951,-135.467 173.951,-135.467\"/>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-219.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-220.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M163.463,-135.36C155.342,-171.623 157.188,-230 169,-230 180.074,-230 182.389,-178.692 175.943,-142.399\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"174.537,-135.36 178.997,-141.607 175.223,-138.792 175.908,-142.224 175.908,-142.224 175.908,-142.224 175.223,-138.792 172.819,-142.841 174.537,-135.36 174.537,-135.36\"/>\n",
"<text text-anchor=\"start\" x=\"150.5\" y=\"-248.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"<text text-anchor=\"start\" x=\"161\" y=\"-233.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M163.519,-135.237C155.333,-171.922 157.16,-232 169,-232 180.1,-232 182.399,-179.197 175.898,-142.369\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"174.481,-135.237 178.935,-141.488 175.163,-138.669 175.845,-142.102 175.845,-142.102 175.845,-142.102 175.163,-138.669 172.756,-142.716 174.481,-135.237 174.481,-135.237\"/>\n",
"<text text-anchor=\"start\" x=\"152\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
"<text text-anchor=\"start\" x=\"153\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"<text text-anchor=\"start\" x=\"169\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;2 -->\n",
"<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
......@@ -176,7 +176,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7ffb2c16a630> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d2406cc00> >"
]
}
],
......
This diff is collapsed.
......@@ -212,7 +212,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e720> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc5466510> >"
]
}
],
......@@ -330,7 +330,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e6f0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca420> >"
]
}
],
......@@ -472,7 +472,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e5d0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca1b0> >"
]
}
],
......@@ -563,7 +563,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e600> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc5466330> >"
]
}
],
......@@ -628,20 +628,20 @@
"<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M52.7643,-51.7817C52.2144,-61.3149 53.293,-70 56,-70 57.988,-70 59.0977,-65.3161 59.3292,-59.0521\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"59.2357,-51.7817 62.4756,-58.7406 59.2808,-55.2814 59.3258,-58.7812 59.3258,-58.7812 59.3258,-58.7812 59.2808,-55.2814 56.1761,-58.8217 59.2357,-51.7817 59.2357,-51.7817\"/>\n",
"<text text-anchor=\"start\" x=\"38\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
"<text text-anchor=\"start\" x=\"36\" y=\"-88.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"<text text-anchor=\"start\" x=\"48\" y=\"-73.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M50.6841,-51.4203C47.6538,-68.791 49.4258,-88 56,-88 61.7011,-88 63.7908,-73.5545 62.2691,-58.3894\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"61.3159,-51.4203 65.3856,-57.9288 61.7902,-54.888 62.2646,-58.3557 62.2646,-58.3557 62.2646,-58.3557 61.7902,-54.888 59.1437,-58.7826 61.3159,-51.4203 61.3159,-51.4203\"/>\n",
"<text text-anchor=\"start\" x=\"36\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"<text text-anchor=\"start\" x=\"48\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M50.9906,-51.5771C47.5451,-72.718 49.2148,-100 56,-100 62.043,-100 64.0285,-78.3596 61.9564,-58.6907\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"61.0094,-51.5771 65.0556,-58.1002 61.4713,-55.0465 61.9332,-58.5159 61.9332,-58.5159 61.9332,-58.5159 61.4713,-55.0465 58.8107,-58.9316 61.0094,-51.5771 61.0094,-51.5771\"/>\n",
"<text text-anchor=\"start\" x=\"38\" y=\"-103.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !c</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef60> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca180> >"
]
}
],
......@@ -758,7 +758,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e540> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca360> >"
]
},
{
......@@ -883,7 +883,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e5a0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca120> >"
]
},
{
......@@ -1027,7 +1027,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e450> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca390> >"
]
}
],
......@@ -1433,7 +1433,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d4b0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec1e0> >"
]
}
],
......@@ -1759,7 +1759,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d480> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca450> >"
]
},
{
......@@ -1957,7 +1957,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062eed0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca360> >"
]
},
{
......@@ -2138,7 +2138,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e450> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bcac30> >"
]
}
],
......@@ -2474,7 +2474,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e376f660> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc5466300> >"
]
}
],
......@@ -2619,7 +2619,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d540> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bcac90> >"
]
},
{
......@@ -2739,7 +2739,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef00> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca270> >"
]
},
{
......@@ -2920,7 +2920,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e480> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca120> >"
]
}
],
......@@ -3278,7 +3278,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d480> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec2d0> >"
]
}
],
......@@ -3569,7 +3569,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d540> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bcac30> >"
]
},
{
......@@ -3722,7 +3722,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca330> >"
]
},
{
......@@ -3860,7 +3860,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef00> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca120> >"
]
}
],
......@@ -4164,7 +4164,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d5d0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec540> >"
]
}
],
......@@ -4276,7 +4276,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d810> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca270> >"
]
}
],
......@@ -4369,7 +4369,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064da20> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bcac30> >"
]
},
{
......@@ -4436,7 +4436,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bcac30> >"
]
}
],
......@@ -4523,7 +4523,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064da80> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec870> >"
]
}
],
......@@ -4679,7 +4679,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064db40> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec270> >"
]
}
],
......@@ -4809,7 +4809,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064dc00> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bca2d0> >"
]
},
{
......@@ -4898,7 +4898,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec630> >"
]
},
{
......@@ -5016,7 +5016,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064dcc0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4bec930> >"
]
}
],
......@@ -5200,7 +5200,7 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e05e74b0> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7effc4b87210> >"