Fixes #495
Monitors can now be split AND completed at the same time. Split can be called on games without providing "synthesis-outputs" - relying on named prop. * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Here * tests/python/_synthesis.ipynb: Testing
This commit is contained in:
philipp
parent
20bcc216a0
commit
7cefe30d97
3 changed files with 824 additions and 22 deletions
|
|
@ -447,16 +447,28 @@ namespace spot
|
|||
const bdd& output_bdd, bool complete_env)
|
||||
{
|
||||
auto split = make_twa_graph(aut->get_dict());
|
||||
|
||||
auto [has_unsat, unsat_mark] = aut->acc().unsat_mark();
|
||||
|
||||
split->copy_ap_of(aut);
|
||||
split->copy_acceptance_of(aut);
|
||||
split->new_states(aut->num_states());
|
||||
split->set_init_state(aut->get_init_state_number());
|
||||
split->set_named_prop<bdd>("synthesis-outputs", new bdd(output_bdd));
|
||||
set_synthesis_outputs(split, output_bdd);
|
||||
|
||||
auto [is_unsat, unsat_mark] = aut->acc().unsat_mark();
|
||||
if (!is_unsat && complete_env)
|
||||
throw std::runtime_error("split_2step(): Cannot complete arena for "
|
||||
"env as there is no unsat mark.");
|
||||
const auto use_color = has_unsat;
|
||||
if (has_unsat)
|
||||
split->copy_acceptance_of(aut);
|
||||
else
|
||||
{
|
||||
if (complete_env)
|
||||
{
|
||||
split->set_co_buchi(); // Fin(0)
|
||||
unsat_mark = acc_cond::mark_t({0});
|
||||
has_unsat = true;
|
||||
}
|
||||
else
|
||||
split->acc().set_acceptance(acc_cond::acc_code::t());
|
||||
}
|
||||
|
||||
bdd input_bdd = bddtrue;
|
||||
{
|
||||
|
|
@ -504,9 +516,10 @@ namespace spot
|
|||
unsigned sink_con = -1u;
|
||||
unsigned sink_env = -1u;
|
||||
auto get_sink_con_state = [&split, &sink_con, &sink_env,
|
||||
um = unsat_mark]
|
||||
um = unsat_mark, hu = has_unsat]
|
||||
(bool create = true)
|
||||
{
|
||||
assert(hu);
|
||||
if (SPOT_UNLIKELY((sink_con == -1u) && create))
|
||||
{
|
||||
sink_con = split->new_state();
|
||||
|
|
@ -518,7 +531,8 @@ namespace spot
|
|||
};
|
||||
|
||||
// Loop over all states
|
||||
for (unsigned src = 0; src < aut->num_states(); ++src)
|
||||
const auto n_states = aut->num_states();
|
||||
for (unsigned src = 0; src < n_states; ++src)
|
||||
{
|
||||
env_edge_hash.clear();
|
||||
e_cache.clear();
|
||||
|
|
@ -579,11 +593,16 @@ namespace spot
|
|||
auto out = split->out(i);
|
||||
if (std::equal(out.begin(), out.end(),
|
||||
dests.begin(), dests.end(),
|
||||
[](const twa_graph::edge_storage_t& x,
|
||||
[uc = use_color]
|
||||
(const twa_graph::edge_storage_t& x,
|
||||
const e_info_t* y)
|
||||
{
|
||||
// If there is no unsat -> we do not care
|
||||
// about color
|
||||
// todo further optim?
|
||||
return x.dst == y->dst
|
||||
&& x.acc == y->acc
|
||||
&& (!uc
|
||||
|| x.acc == y->acc)
|
||||
&& x.cond.id() == y->econdout.id();
|
||||
}))
|
||||
{
|
||||
|
|
@ -592,6 +611,7 @@ namespace spot
|
|||
if (it != env_edge_hash.end())
|
||||
it->second.second |= one_letter;
|
||||
else
|
||||
// Uncolored
|
||||
env_edge_hash.emplace(i,
|
||||
eeh_t(split->new_edge(src, i, bddtrue), one_letter));
|
||||
break;
|
||||
|
|
@ -605,7 +625,8 @@ namespace spot
|
|||
env_hash.emplace(h, d);
|
||||
env_edge_hash.emplace(d, eeh_t(n_e, one_letter));
|
||||
for (const auto &t: dests)
|
||||
split->new_edge(d, t->dst, t->econdout, t->acc);
|
||||
split->new_edge(d, t->dst, t->econdout,
|
||||
use_color ? t->acc : acc_cond::mark_t({}));
|
||||
}
|
||||
} // letters
|
||||
// save locally stored condition
|
||||
|
|
@ -619,21 +640,34 @@ namespace spot
|
|||
// The named property
|
||||
// compute the owners
|
||||
// env is equal to false
|
||||
std::vector<bool>* owner =
|
||||
new std::vector<bool>(split->num_states(), false);
|
||||
auto owner = std::vector<bool>(split->num_states(), false);
|
||||
// All "new" states belong to the player
|
||||
std::fill(owner->begin()+aut->num_states(), owner->end(), true);
|
||||
std::fill(owner.begin()+aut->num_states(), owner.end(), true);
|
||||
// Check if sinks have been created
|
||||
if (sink_env != -1u)
|
||||
owner->at(sink_env) = false;
|
||||
split->set_named_prop("state-player", owner);
|
||||
split->set_named_prop("synthesis-outputs",
|
||||
new bdd(output_bdd));
|
||||
owner.at(sink_env) = false;
|
||||
|
||||
// !use_color -> all words accepted
|
||||
// complete_env && sink_env == -1u
|
||||
// complet. for env demanded but already
|
||||
// satisfied -> split is also all true
|
||||
if (complete_env && sink_env == -1u && !use_color)
|
||||
split->acc() = acc_cond::acc_code::t();
|
||||
|
||||
set_state_players(split, std::move(owner));
|
||||
|
||||
// Done
|
||||
return split;
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
split_2step(const const_twa_graph_ptr& aut, bool complete_env)
|
||||
{
|
||||
return split_2step(aut,
|
||||
get_synthesis_outputs(aut),
|
||||
complete_env);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
unsplit_2step(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -52,11 +52,17 @@ namespace spot
|
|||
/// \param complete_env Whether the automaton should be complete for the
|
||||
/// environment, i.e. the player of inputs
|
||||
/// \note This function also computes the state players
|
||||
/// \note If the automaton is to be completed for both env and player
|
||||
/// then egdes between the sinks will be added
|
||||
/// \note If the automaton is to be completed, sink states will
|
||||
/// be added for both env and player if necessary
|
||||
SPOT_API twa_graph_ptr
|
||||
split_2step(const const_twa_graph_ptr& aut,
|
||||
const bdd& output_bdd, bool complete_env);
|
||||
const bdd& output_bdd, bool complete_env = true);
|
||||
|
||||
/// \ingroup synthesis
|
||||
/// \brief Like split_2step but relying on the named property
|
||||
/// 'synthesis-outputs'
|
||||
SPOT_API twa_graph_ptr
|
||||
split_2step(const const_twa_graph_ptr& aut, bool complete_env = true);
|
||||
|
||||
/// \ingroup synthesis
|
||||
/// \brief the inverse of split_2step
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"import spot\n",
|
||||
"import spot, buddy\n",
|
||||
"spot.setup()"
|
||||
]
|
||||
},
|
||||
|
|
@ -389,6 +389,768 @@
|
|||
"assert(mmus3.equivalent_to(msep3))\n",
|
||||
"assert(mmus3.equivalent_to(mus3))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Testing related to #495"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 6,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(0, t)\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"244pt\" height=\"115pt\"\n",
|
||||
" viewBox=\"0.00 0.00 244.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 240,-111 240,4 -4,4\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"115\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"107\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->1 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>1->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M74.12,-18C102.48,-18 159.32,-18 192.12,-18\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"199.52,-18 192.52,-21.15 196.02,-18 192.52,-18 192.52,-18 192.52,-18 196.02,-18 192.52,-14.85 199.52,-18 199.52,-18\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">(!i & !o) | (i & o)</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M205.29,-31.29C199.86,-42.4 204.09,-54 218,-54 229.08,-54 234.02,-46.63 232.82,-38.02\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"230.71,-31.29 235.81,-37.03 231.76,-34.63 232.81,-37.97 232.81,-37.97 232.81,-37.97 231.76,-34.63 229.8,-38.91 230.71,-31.29 230.71,-31.29\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"218\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f7b0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 6,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"a = spot.translate(\"i<->o\", \"parity\")\n",
|
||||
"print(a.acc())\n",
|
||||
"a"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 7,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"206pt\" height=\"85pt\"\n",
|
||||
" viewBox=\"0.00 0.00 205.50 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 81)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-81 201.5,-81 201.5,4 -4,4\"/>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->1 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"175\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"175\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>1->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M74.01,-18C93.94,-18 127.11,-18 149.73,-18\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"156.97,-18 149.97,-21.15 153.47,-18 149.97,-18 149.97,-18 149.97,-18 153.47,-18 149.97,-14.85 156.97,-18 156.97,-18\"/>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-41 94.5,-60 105.5,-60 105.5,-41 94.5,-41\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"96.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"109.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-41 120.5,-60 137.5,-60 137.5,-41 120.5,-41\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"122.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-20 94.5,-39 105.5,-39 105.5,-20 94.5,-20\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"99.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"109.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-20 120.5,-39 137.5,-39 137.5,-20 120.5,-20\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"122.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->0 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M165.19,-33.17C162.21,-43.66 165.48,-54 175,-54 182.29,-54 185.91,-47.94 185.87,-40.39\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"184.81,-33.17 188.95,-39.63 185.32,-36.63 185.83,-40.09 185.83,-40.09 185.83,-40.09 185.32,-36.63 182.71,-40.55 184.81,-33.17 184.81,-33.17\"/>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"155,-55.5 155,-74.5 168,-74.5 168,-55.5 155,-55.5\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"157\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"172\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"183,-55.5 183,-74.5 196,-74.5 196,-55.5 183,-55.5\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"185\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f7b0> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 7,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"spot.set_synthesis_outputs(a, buddy.bdd_ithvar(a.register_ap(\"o\")))\n",
|
||||
"a"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 8,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(0, t)\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"363pt\" height=\"136pt\"\n",
|
||||
" viewBox=\"0.00 0.00 363.00 136.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 132)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-132 359,-132 359,4 -4,4\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"174.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"166.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->1 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-45C2.79,-45 17.15,-45 30.63,-45\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-45 30.94,-48.15 34.44,-45 30.94,-45 30.94,-45 30.94,-45 34.44,-45 30.94,-41.85 37.94,-45 37.94,-45\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3 -->\n",
|
||||
"<g id=\"node5\" class=\"node\">\n",
|
||||
"<title>3</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-90 117,-72 144,-54 171,-72 144,-90\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"144\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->3 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>1->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M73.58,-50.21C86.33,-54.21 104.15,-59.8 118.53,-64.32\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-66.44 117.66,-67.35 121.95,-65.39 118.61,-64.34 118.61,-64.34 118.61,-64.34 121.95,-65.39 119.55,-61.34 125.29,-66.44 125.29,-66.44\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4 -->\n",
|
||||
"<g id=\"node6\" class=\"node\">\n",
|
||||
"<title>4</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-36 117,-18 144,0 171,-18 144,-36\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"144\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->4 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\">\n",
|
||||
"<title>1->4</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M73.58,-39.79C86.33,-35.79 104.15,-30.2 118.53,-25.68\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-23.56 119.55,-28.66 121.95,-24.61 118.61,-25.66 118.61,-25.66 118.61,-25.66 121.95,-24.61 117.66,-22.65 125.29,-23.56 125.29,-23.56\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"93.5\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"238\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"238\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g id=\"node4\" class=\"node\">\n",
|
||||
"<title>2</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"328,-63 301,-45 328,-27 355,-45 328,-63\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"328\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->2 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M256.39,-45C267.02,-45 280.98,-45 293.68,-45\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"300.97,-45 293.97,-48.15 297.47,-45 293.97,-45 293.97,-45 293.97,-45 297.47,-45 293.97,-41.85 300.97,-45 300.97,-45\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"278.5\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2->0 -->\n",
|
||||
"<g id=\"edge5\" class=\"edge\">\n",
|
||||
"<title>2->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M314.15,-35.81C303.54,-29.35 288.02,-22.44 274,-26 269.14,-27.23 264.22,-29.3 259.67,-31.62\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"253.31,-35.13 257.91,-28.99 256.37,-33.44 259.44,-31.74 259.44,-31.74 259.44,-31.74 256.37,-33.44 260.96,-34.5 253.31,-35.13 253.31,-35.13\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"278.5\" y=\"-29.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3->0 -->\n",
|
||||
"<g id=\"edge6\" class=\"edge\">\n",
|
||||
"<title>3->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M163.18,-66.67C177.62,-62.43 197.92,-56.47 213.58,-51.87\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-49.87 214.58,-54.86 217.05,-50.86 213.69,-51.84 213.69,-51.84 213.69,-51.84 217.05,-50.86 212.8,-48.82 220.41,-49.87 220.41,-49.87\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"189\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4->0 -->\n",
|
||||
"<g id=\"edge7\" class=\"edge\">\n",
|
||||
"<title>4->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M163.18,-23.33C177.62,-27.57 197.92,-33.53 213.58,-38.13\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-40.13 212.8,-41.18 217.05,-39.14 213.69,-38.16 213.69,-38.16 213.69,-38.16 217.05,-39.14 214.58,-35.14 220.41,-40.13 220.41,-40.13\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"191\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f630> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 8,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"a_s = spot.split_2step(a, True)\n",
|
||||
"print(a.acc())\n",
|
||||
"a_s"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 9,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"326pt\" height=\"108pt\"\n",
|
||||
" viewBox=\"0.00 0.00 326.00 108.23\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 104.23)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-104.23 322,-104.23 322,4 -4,4\"/>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->0 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-42.23C2.79,-42.23 17.15,-42.23 30.63,-42.23\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-42.23 30.94,-45.38 34.44,-42.23 30.94,-42.23 30.94,-42.23 30.94,-42.23 34.44,-42.23 30.94,-39.08 37.94,-42.23 37.94,-42.23\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"176\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"176\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->1 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M72.74,-48.86C78.67,-51.03 85.54,-53.15 92,-54.23 113.04,-57.73 118.96,-57.73 140,-54.23 144.14,-53.54 148.45,-52.42 152.57,-51.13\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"159.26,-48.86 153.64,-54.09 155.94,-49.99 152.63,-51.11 152.63,-51.11 152.63,-51.11 155.94,-49.99 151.62,-48.13 159.26,-48.86 159.26,-48.86\"/>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-79.23 94,-98.23 110,-98.23 110,-79.23 94,-79.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"96\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"114\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-79.23 125,-98.23 138,-98.23 138,-79.23 125,-79.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"127\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"108\" y=\"-64.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->0 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>1->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M165.21,-27.48C159.03,-19.57 150.28,-10.57 140,-6.23 120.35,2.08 111.65,2.08 92,-6.23 84.13,-9.55 77.16,-15.61 71.55,-21.81\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"66.79,-27.48 68.88,-20.1 69.04,-24.8 71.29,-22.12 71.29,-22.12 71.29,-22.12 69.04,-24.8 73.7,-24.14 66.79,-27.48 66.79,-27.48\"/>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-29.23 94,-48.23 110,-48.23 110,-29.23 94,-29.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"96\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">i1</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"114\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-29.23 125,-48.23 138,-48.23 138,-29.23 125,-29.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"127\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"108\" y=\"-14.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g id=\"node4\" class=\"node\">\n",
|
||||
"<title>2</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"300\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"300\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->2 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\">\n",
|
||||
"<title>1->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M194.22,-42.23C215.2,-42.23 250.79,-42.23 274.59,-42.23\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"281.87,-42.23 274.87,-45.38 278.37,-42.23 274.87,-42.23 274.87,-42.23 274.87,-42.23 278.37,-42.23 274.87,-39.08 281.87,-42.23 281.87,-42.23\"/>\n",
|
||||
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"214,-65.23 214,-84.23 230,-84.23 230,-65.23 214,-65.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"216\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"234\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
|
||||
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"245,-65.23 245,-84.23 262,-84.23 262,-65.23 245,-65.23\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"247\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"230\" y=\"-50.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee36703f60> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 9,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"a = spot.make_twa_graph()\n",
|
||||
"a.acc().set_acceptance(spot.acc_code.t())\n",
|
||||
"i0 = buddy.bdd_ithvar(a.register_ap('i0'))\n",
|
||||
"i1 = buddy.bdd_ithvar(a.register_ap('i1'))\n",
|
||||
"o = buddy.bdd_ithvar(a.register_ap('o'))\n",
|
||||
"tt = buddy.bddtrue\n",
|
||||
"a0 = spot.mark_t([0])\n",
|
||||
"a.new_states(3)\n",
|
||||
"a.new_edge(0,1,i0&o,a0)\n",
|
||||
"a.new_edge(1,0,i1,a0)\n",
|
||||
"a.new_edge(1,2,i0&(buddy.bdd_not(o)),a0)\n",
|
||||
"spot.set_synthesis_outputs(a, o)\n",
|
||||
"a"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 10,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(0, t)\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"484pt\" height=\"198pt\"\n",
|
||||
" viewBox=\"0.00 0.00 484.00 198.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 194)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-194 480,-194 480,4 -4,4\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"235\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"227\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-80\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->0 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-80C2.79,-80 17.15,-80 30.63,-80\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-80 30.94,-83.15 34.44,-80 30.94,-80 30.94,-80 30.94,-80 34.44,-80 30.94,-76.85 37.94,-80 37.94,-80\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>3</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-98 122,-80 149,-62 176,-80 149,-98\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"149\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->3 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M74.12,-80C85.52,-80 100.87,-80 114.63,-80\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"121.65,-80 114.65,-83.15 118.15,-80 114.65,-80 114.65,-80 114.65,-80 118.15,-80 114.65,-76.85 121.65,-80 121.65,-80\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node4\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-80\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"239\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3->1 -->\n",
|
||||
"<g id=\"edge6\" class=\"edge\">\n",
|
||||
"<title>3->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M176.4,-80C188.2,-80 202.01,-80 213.57,-80\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"220.79,-80 213.79,-83.15 217.29,-80 213.79,-80 213.79,-80 213.79,-80 217.29,-80 213.79,-76.85 220.79,-80 220.79,-80\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"194\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4 -->\n",
|
||||
"<g id=\"node5\" class=\"node\">\n",
|
||||
"<title>4</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->4 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>1->4</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M255.26,-71.53C261.37,-68.19 268.49,-64.36 275,-61 297.28,-49.51 323.09,-37 340.97,-28.44\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"347.64,-25.26 342.68,-31.12 344.48,-26.77 341.32,-28.27 341.32,-28.27 341.32,-28.27 344.48,-26.77 339.97,-25.43 347.64,-25.26 347.64,-25.26\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"275\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 & i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 5 -->\n",
|
||||
"<g id=\"node6\" class=\"node\">\n",
|
||||
"<title>5</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-98 337,-80 364,-62 391,-80 364,-98\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->5 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\">\n",
|
||||
"<title>1->5</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M257.1,-80C275.77,-80 306.11,-80 329.55,-80\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"336.58,-80 329.58,-83.15 333.08,-80 329.58,-80 329.58,-80 329.58,-80 333.08,-80 329.58,-76.85 336.58,-80 336.58,-80\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"275\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0 & !i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 6 -->\n",
|
||||
"<g id=\"node7\" class=\"node\">\n",
|
||||
"<title>6</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-152 337,-134 364,-116 391,-134 364,-152\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->6 -->\n",
|
||||
"<g id=\"edge5\" class=\"edge\">\n",
|
||||
"<title>1->6</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M255.65,-87.24C261.68,-90.01 268.65,-93.18 275,-96 297.15,-105.84 322.59,-116.79 340.39,-124.39\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"347.06,-127.24 339.38,-127.39 343.84,-125.86 340.62,-124.49 340.62,-124.49 340.62,-124.49 343.84,-125.86 341.86,-121.59 347.06,-127.24 347.06,-127.24\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"277\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">i0 & i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4->0 -->\n",
|
||||
"<g id=\"edge7\" class=\"edge\">\n",
|
||||
"<title>4->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M338.99,-19.5C295.19,-22.67 199.65,-31.6 122,-53 107.19,-57.08 91.25,-63.67 78.86,-69.31\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"72.37,-72.33 77.39,-66.52 75.55,-70.85 78.72,-69.38 78.72,-69.38 78.72,-69.38 75.55,-70.85 80.05,-72.23 72.37,-72.33 72.37,-72.33\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g id=\"node8\" class=\"node\">\n",
|
||||
"<title>2</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"458\" cy=\"-107\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"458\" y=\"-103.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 5->2 -->\n",
|
||||
"<g id=\"edge8\" class=\"edge\">\n",
|
||||
"<title>5->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M385.52,-83.87C396.46,-86.14 410.08,-89.28 422,-93 426.08,-94.27 430.36,-95.81 434.47,-97.39\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"441.16,-100.05 433.49,-100.39 437.91,-98.76 434.66,-97.46 434.66,-97.46 434.66,-97.46 437.91,-98.76 435.82,-94.54 441.16,-100.05 441.16,-100.05\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"409\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 6->0 -->\n",
|
||||
"<g id=\"edge9\" class=\"edge\">\n",
|
||||
"<title>6->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M338.67,-135.14C320.98,-135.69 296.46,-135.88 275,-134 206.21,-127.98 189.42,-121.91 122,-107 108.53,-104.02 104.82,-104.11 92,-99 87.43,-97.18 82.69,-94.9 78.23,-92.56\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"71.95,-89.13 79.61,-89.72 75.03,-90.81 78.1,-92.49 78.1,-92.49 78.1,-92.49 75.03,-90.81 76.59,-95.25 71.95,-89.13 71.95,-89.13\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"198.5\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 6->2 -->\n",
|
||||
"<g id=\"edge10\" class=\"edge\">\n",
|
||||
"<title>6->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M383.18,-128.67C397.62,-124.43 417.92,-118.47 433.58,-113.87\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"440.41,-111.87 434.58,-116.86 437.05,-112.86 433.69,-113.84 433.69,-113.84 433.69,-113.84 437.05,-112.86 432.8,-110.82 440.41,-111.87 440.41,-111.87\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"409\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716f930> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 10,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"a_snc = spot.split_2step(a, False)\n",
|
||||
"print(a_snc.acc())\n",
|
||||
"a_snc"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 11,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"(1, Fin(0))\n"
|
||||
]
|
||||
},
|
||||
{
|
||||
"data": {
|
||||
"image/svg+xml": [
|
||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
|
||||
"<!-- Generated by graphviz version 2.43.0 (0)\n",
|
||||
" -->\n",
|
||||
"<!-- Pages: 1 -->\n",
|
||||
"<svg width=\"706pt\" height=\"269pt\"\n",
|
||||
" viewBox=\"0.00 0.00 706.00 269.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
||||
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 265)\">\n",
|
||||
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-265 702,-265 702,4 -4,4\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"327.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"350.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"366.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"317.5\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">[co-Büchi]</text>\n",
|
||||
"<!-- I -->\n",
|
||||
"<!-- 0 -->\n",
|
||||
"<g id=\"node2\" class=\"node\">\n",
|
||||
"<title>0</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-59\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"56\" y=\"-55.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- I->0 -->\n",
|
||||
"<g id=\"edge1\" class=\"edge\">\n",
|
||||
"<title>I->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-59C2.79,-59 17.15,-59 30.63,-59\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-59 30.94,-62.15 34.44,-59 30.94,-59 30.94,-59 30.94,-59 34.44,-59 30.94,-55.85 37.94,-59 37.94,-59\"/>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3 -->\n",
|
||||
"<g id=\"node3\" class=\"node\">\n",
|
||||
"<title>3</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"583,-190 556,-172 583,-154 610,-172 583,-190\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"583\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->3 -->\n",
|
||||
"<g id=\"edge2\" class=\"edge\">\n",
|
||||
"<title>0->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M59.28,-76.91C65.47,-116.91 86.48,-210 148,-210 148,-210 148,-210 494,-210 519.79,-210 546.6,-196.08 563.75,-185.08\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"569.61,-181.2 565.52,-187.69 566.69,-183.13 563.78,-185.07 563.78,-185.07 563.78,-185.07 566.69,-183.13 562.04,-182.44 569.61,-181.2 569.61,-181.2\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"289\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">!i0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 5 -->\n",
|
||||
"<g id=\"node4\" class=\"node\">\n",
|
||||
"<title>5</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-108 122,-90 149,-72 176,-90 149,-108\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"149\" y=\"-86.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 0->5 -->\n",
|
||||
"<g id=\"edge3\" class=\"edge\">\n",
|
||||
"<title>0->5</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M73.27,-64.54C87.28,-69.31 107.7,-76.27 123.65,-81.71\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"130.63,-84.08 122.99,-84.81 127.32,-82.95 124.01,-81.83 124.01,-81.83 124.01,-81.83 127.32,-82.95 125.02,-78.84 130.63,-84.08 130.63,-84.08\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"92\" y=\"-77.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4 -->\n",
|
||||
"<g id=\"node10\" class=\"node\">\n",
|
||||
"<title>4</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"680\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"680\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 3->4 -->\n",
|
||||
"<g id=\"edge9\" class=\"edge\">\n",
|
||||
"<title>3->4</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M605.09,-175.35C616.59,-176.77 631.07,-177.92 644,-177 647.49,-176.75 651.16,-176.37 654.76,-175.92\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"661.96,-174.93 655.46,-179 658.49,-175.4 655.03,-175.88 655.03,-175.88 655.03,-175.88 658.49,-175.4 654.6,-172.76 661.96,-174.93 661.96,-174.93\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"631.5\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"628\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1 -->\n",
|
||||
"<g id=\"node5\" class=\"node\">\n",
|
||||
"<title>1</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-104\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"239\" y=\"-100.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 5->1 -->\n",
|
||||
"<g id=\"edge11\" class=\"edge\">\n",
|
||||
"<title>5->1</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M171.3,-93.39C184.18,-95.44 200.62,-98.05 213.96,-100.18\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"221.01,-101.3 213.61,-103.31 217.56,-100.75 214.1,-100.2 214.1,-100.2 214.1,-100.2 217.56,-100.75 214.6,-97.09 221.01,-101.3 221.01,-101.3\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"194\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->3 -->\n",
|
||||
"<g id=\"edge4\" class=\"edge\">\n",
|
||||
"<title>1->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M249.03,-119.4C255.17,-128.4 264.14,-139.12 275,-145 321.53,-170.19 479.42,-172.57 548.82,-172.35\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"556.04,-172.32 549.06,-175.5 552.54,-172.34 549.04,-172.35 549.04,-172.35 549.04,-172.35 552.54,-172.34 549.03,-169.2 556.04,-172.32 556.04,-172.32\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"409\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 & !i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 6 -->\n",
|
||||
"<g id=\"node6\" class=\"node\">\n",
|
||||
"<title>6</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-90 337,-72 364,-54 391,-72 364,-90\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->6 -->\n",
|
||||
"<g id=\"edge5\" class=\"edge\">\n",
|
||||
"<title>1->6</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M256.59,-99.68C277.36,-94.28 313.15,-84.97 337.44,-78.65\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"344.26,-76.87 338.28,-81.69 340.88,-77.76 337.49,-78.64 337.49,-78.64 337.49,-78.64 340.88,-77.76 336.7,-75.59 344.26,-76.87 344.26,-76.87\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"275\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 & i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 7 -->\n",
|
||||
"<g id=\"node7\" class=\"node\">\n",
|
||||
"<title>7</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-144 337,-126 364,-108 391,-126 364,-144\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->7 -->\n",
|
||||
"<g id=\"edge6\" class=\"edge\">\n",
|
||||
"<title>1->7</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M255.24,-112.42C261.23,-115.33 268.26,-118.29 275,-120 293.02,-124.57 313.74,-126.16 330.55,-126.56\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"337.97,-126.67 330.92,-129.71 334.47,-126.62 330.97,-126.57 330.97,-126.57 330.97,-126.57 334.47,-126.62 331.02,-123.42 337.97,-126.67 337.97,-126.67\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"275\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">i0 & !i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 8 -->\n",
|
||||
"<g id=\"node8\" class=\"node\">\n",
|
||||
"<title>8</title>\n",
|
||||
"<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 1->8 -->\n",
|
||||
"<g id=\"edge7\" class=\"edge\">\n",
|
||||
"<title>1->8</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M250.63,-89.89C257.09,-81.94 265.84,-72.19 275,-65 295.27,-49.1 321.69,-35.81 340.28,-27.47\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"346.74,-24.62 341.6,-30.32 343.54,-26.03 340.33,-27.44 340.33,-27.44 340.33,-27.44 343.54,-26.03 339.06,-24.56 346.74,-24.62 346.74,-24.62\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"277\" y=\"-68.8\" font-family=\"Lato\" font-size=\"14.00\">i0 & i1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 6->0 -->\n",
|
||||
"<g id=\"edge12\" class=\"edge\">\n",
|
||||
"<title>6->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M350.67,-62.68C342.25,-56.92 330.55,-50.05 319,-47 233.55,-24.42 127.04,-42.98 80.55,-53.28\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"73.61,-54.85 79.74,-50.23 77.03,-54.08 80.44,-53.3 80.44,-53.3 80.44,-53.3 77.03,-54.08 81.14,-56.37 73.61,-54.85 73.61,-54.85\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2 -->\n",
|
||||
"<g id=\"node9\" class=\"node\">\n",
|
||||
"<title>2</title>\n",
|
||||
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"493\" cy=\"-126\" rx=\"18\" ry=\"18\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"493\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 7->2 -->\n",
|
||||
"<g id=\"edge13\" class=\"edge\">\n",
|
||||
"<title>7->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M391.01,-126C413.57,-126 445.96,-126 467.93,-126\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"474.95,-126 467.95,-129.15 471.45,-126 467.95,-126 467.95,-126 467.95,-126 471.45,-126 467.95,-122.85 474.95,-126 474.95,-126\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"426.5\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 8->0 -->\n",
|
||||
"<g id=\"edge14\" class=\"edge\">\n",
|
||||
"<title>8->0</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M339.67,-16.08C306.97,-13.79 245.73,-10.98 194,-17 161.34,-20.8 153.63,-25.01 122,-34 108.48,-37.84 105.14,-39.01 92,-44 87.96,-45.54 83.71,-47.26 79.6,-48.99\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"72.92,-51.85 78.11,-46.2 76.13,-50.47 79.35,-49.1 79.35,-49.1 79.35,-49.1 76.13,-50.47 80.59,-51.99 72.92,-51.85 72.92,-51.85\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"198.5\" y=\"-20.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 8->2 -->\n",
|
||||
"<g id=\"edge15\" class=\"edge\">\n",
|
||||
"<title>8->2</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M376.72,-27.97C398.76,-46.71 446.53,-87.34 473.14,-109.96\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"478.8,-114.77 471.42,-112.64 476.13,-112.51 473.47,-110.24 473.47,-110.24 473.47,-110.24 476.13,-112.51 475.51,-107.84 478.8,-114.77 478.8,-114.77\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"426.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 2->3 -->\n",
|
||||
"<g id=\"edge8\" class=\"edge\">\n",
|
||||
"<title>2->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M510.25,-131.34C518.71,-134.35 529.12,-138.42 538,-143 546.64,-147.45 555.69,-153.2 563.32,-158.41\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"569.35,-162.61 561.81,-161.2 566.48,-160.61 563.61,-158.61 563.61,-158.61 563.61,-158.61 566.48,-160.61 565.41,-156.03 569.35,-162.61 569.35,-162.61\"/>\n",
|
||||
"<text text-anchor=\"middle\" x=\"533.5\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"</g>\n",
|
||||
"<!-- 4->3 -->\n",
|
||||
"<g id=\"edge10\" class=\"edge\">\n",
|
||||
"<title>4->3</title>\n",
|
||||
"<path fill=\"none\" stroke=\"black\" d=\"M667.4,-158.86C661.16,-152.78 652.91,-146.21 644,-143 637.31,-140.59 634.81,-140.96 628,-143 618.42,-145.87 608.99,-151.59 601.34,-157.19\"/>\n",
|
||||
"<polygon fill=\"black\" stroke=\"black\" points=\"595.36,-161.8 598.98,-155.03 598.13,-159.66 600.9,-157.52 600.9,-157.52 600.9,-157.52 598.13,-159.66 602.82,-160.02 595.36,-161.8 595.36,-161.8\"/>\n",
|
||||
"<text text-anchor=\"start\" x=\"631.5\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
|
||||
"<text text-anchor=\"start\" x=\"628\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
|
||||
"</g>\n",
|
||||
"</g>\n",
|
||||
"</svg>\n"
|
||||
],
|
||||
"text/plain": [
|
||||
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fee3716fa20> >"
|
||||
]
|
||||
},
|
||||
"execution_count": 11,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"a_s = spot.split_2step(a, True)\n",
|
||||
"print(a_s.acc())\n",
|
||||
"a_s"
|
||||
]
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue