diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 16a5e1338..578b76a4c 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -547,18 +547,22 @@ digraph G { I [label="", style=invis, height=0] I -> 1 subgraph cluster_0 { + color=green label="" 0 [label="0"] } subgraph cluster_1 { + color=green label="" 3 [label="3"] } subgraph cluster_2 { + color=red label="" 4 [label="4"] } subgraph cluster_3 { + color=green label="" 1 [label="1"] 2 [label="2"] @@ -586,40 +590,77 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/' #+RESULTS: oaut-dot2 #+begin_example digraph G { - label="(Gb | F!a) W c\\nInf(0)" + rankdir=LR + label="Fin(2) & (Inf(0)&Inf(1))" labelloc="t" node [shape="circle"] - I [label="", style=invis, height=0] + I [label="", style=invis, width=0] I -> 1 subgraph cluster_0 { + color=grey + label="" + 5 [label="5"] + 6 [label="6"] + } + subgraph cluster_1 { + color=orange label="" 0 [label="0"] } - subgraph cluster_1 { - label="" - 3 [label="3"] - } subgraph cluster_2 { + color=orange + label="" + 9 [label="9"] + 10 [label="10"] + } + subgraph cluster_3 { + color=green + label="" + 8 [label="8"] + } + subgraph cluster_4 { + color=green + label="" + 7 [label="7"] + } + subgraph cluster_5 { + color=black + label="" + 2 [label="2"] + } + subgraph cluster_6 { + color=red label="" 4 [label="4"] } - subgraph cluster_3 { + subgraph cluster_7 { + color=green label="" 1 [label="1"] - 2 [label="2"] + 3 [label="3"] } - 0 -> 0 [label="b\\n{0}"] - 1 -> 0 [label="a & b & !c"] - 1 -> 1 [label="!a & !c\\n{0}"] - 1 -> 2 [label="a & !c"] - 1 -> 3 [label="c"] - 2 -> 1 [label="!a & !c\\n{0}"] - 2 -> 2 [label="a & !c"] - 2 -> 3 [label="!a & c"] - 2 -> 4 [label="a & c"] - 3 -> 3 [label="1\\n{0}"] - 4 -> 3 [label="!a"] - 4 -> 4 [label="a"] + 0 -> 0 [label="a & b\\n{0,1,2}"] + 0 -> 0 [label="!a & !b\\n{2}"] + 0 -> 5 [label="a\\n{2}"] + 1 -> 4 [label="b"] + 1 -> 3 [label="a & !b"] + 2 -> 0 [label="a"] + 2 -> 7 [label="b"] + 3 -> 1 [label="a & b\\n{0,1}"] + 4 -> 4 [label="!b\\n{1,2}"] + 4 -> 2 [label="b"] + 5 -> 6 [label="1"] + 6 -> 5 [label="1"] + 7 -> 7 [label="!a & b\\n{0,1}"] + 7 -> 7 [label="a & b\\n{0,2}"] + 7 -> 8 [label="1"] + 8 -> 8 [label="!a & b\\n{0,2}"] + 8 -> 8 [label="a & b\\n{0,1}"] + 8 -> 9 [label="1"] + 9 -> 9 [label="!a & b\\n{0,2}"] + 9 -> 10 [label="a & b\\n{0,1}"] + 10 -> 9 [label="!a & b\\n{0,1}"] + 10 -> 10 [label="a & b\\n{0,2}"] } #+end_example @@ -634,6 +675,134 @@ The acceptance condition is displayed in the same way as in the [[http://adl.git format]]. Here =Inf(0)= means that runs are accepting if and only if they visit some the transitions in the set #0 infinitely often. +The strongly connected components are displayed using the following colors: +- *green* components contain an accepting cycle +- *red* components contain no accepting cycle +- *orange* components may or may not contain an accepting cycle. Such an indecision occur only when using =Fin= acceptance primitive, deciding that would require a better algorithm than what the output routine is using. +- *black* components are trivial (i.e., they contain no cycle) +- *gray* components are useless (i.e., they are non-accepting, and are only followed by non-accepting components) + +Here is an example involving all colors: + +#+NAME: oaut-dot3 +#+BEGIN_SRC sh :results verbatim :exports none +autfilt --dot=cas < 1 + subgraph cluster_0 { + color=grey + label="" + 5 [label="5"] + 6 [label="6"] + } + subgraph cluster_1 { + color=orange + label="" + 0 [label="0"] + } + subgraph cluster_2 { + color=orange + label="" + 8 [label="8"] + 9 [label="9"] + } + subgraph cluster_3 { + color=green + label="" + 7 [label="7"] + } + subgraph cluster_4 { + color=black + label="" + 2 [label="2"] + } + subgraph cluster_5 { + color=red + label="" + 4 [label="4"] + } + subgraph cluster_6 { + color=green + label="" + 1 [label="1"] + 3 [label="3"] + } + 0 -> 0 [label="a & b\\n{0,1,2}"] + 0 -> 0 [label="!a & !b\\n{2}"] + 0 -> 5 [label="a\\n{2}"] + 1 -> 4 [label="b"] + 1 -> 3 [label="a & !b"] + 2 -> 0 [label="a"] + 2 -> 7 [label="b"] + 3 -> 1 [label="a & b\\n{0,1}"] + 4 -> 4 [label="!b\\n{1,2}"] + 4 -> 2 [label="b"] + 5 -> 6 [label="1\\n{1}"] + 6 -> 5 [label="1"] + 7 -> 7 [label="!a & b\\n{0,2}"] + 7 -> 7 [label="a & b\\n{0,1}"] + 7 -> 8 [label="1"] + 8 -> 8 [label="!a & b\\n{0,2}"] + 8 -> 9 [label="a & b\\n{0,1}"] + 9 -> 8 [label="!a & b\\n{0,1}"] + 9 -> 9 [label="a & b\\n{0,2}"] +} +#+end_example + +#+BEGIN_SRC dot :file oaut-dot3.png :cmdline -Tpng :var txt=oaut-dot3 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:oaut-dot3.png]] + * Statistics The =--stats= option takes format string parameter to specify what and diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 38c30176f..d4ebef7c4 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -673,7 +673,7 @@ namespace st->nondeterministic = st->nondetstates != 0; for (unsigned n = 0; n < c; ++n) { - if (!m.is_accepting_scc(n)) + if (m.is_rejecting_scc(n)) ++st->nonacc_scc; else if (is_terminal_scc(m, n)) ++st->terminal_scc; diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 669e8627b..b1ca42a65 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -189,6 +189,47 @@ namespace spot return false; } + static bool + inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + { + auto sub = pos - pos->size; + while (sub < pos) + { + --pos; + if (!inf_eval(inf, pos)) + return false; + pos -= pos->size; + } + return true; + } + case acc_cond::acc_op::Or: + { + auto sub = pos - pos->size; + while (sub < pos) + { + --pos; + if (inf_eval(inf, pos)) + return true; + pos -= pos->size; + } + return false; + } + case acc_cond::acc_op::Inf: + return (pos[-1].mark & inf) == pos[-1].mark; + case acc_cond::acc_op::Fin: + return true; + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + } + SPOT_UNREACHABLE(); + return false; + } + static acc_cond::mark_t eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos) { @@ -243,6 +284,13 @@ namespace spot return eval(inf, &code_.back()); } + bool acc_cond::inf_satisfiable(mark_t inf) const + { + if (code_.empty()) + return true; + return inf_eval(inf, &code_.back()); + } + acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const { if (uses_fin_acceptance()) diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 76b4ad70a..3e6734b64 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -843,6 +843,11 @@ namespace spot } bool accepting(mark_t inf) const; + + // Assume all Fin(x) in the condition a true. Would the resulting + // condition (involving only Inf(y)) be satisfiable? + bool inf_satisfiable(mark_t inf) const; + mark_t accepting_sets(mark_t inf) const; std::ostream& format(std::ostream& os, mark_t m) const diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 12788bc9d..c7c7793f9 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -164,10 +164,25 @@ namespace spot for (unsigned i = 0; i < sccs; ++i) { os_ << " subgraph cluster_" << i << " {\n"; + + // Color the SCC to indicate whether is it accepting. + if (!si->is_useful_scc(i)) + os_ << " color=grey\n"; + else if (si->is_trivial(i)) + os_ << " color=black\n"; + else if (si->is_accepting_scc(i)) + os_ << " color=green\n"; + else if (si->is_rejecting_scc(i)) + os_ << " color=red\n"; + else + os_ << " color=orange\n"; + if (name_ || opt_show_acc_) - // Reset the label, otherwise the graph label would - // be inherited by the cluster. - os_ << " label=\"\"\n"; + { + // Reset the label, otherwise the graph label would + // be inherited by the cluster. + os_ << " label=\"\"\n"; + } for (auto s: si->states_of(i)) process_state(s); os_ << " }\n"; diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index b90caecc0..f4bd3f08f 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -136,7 +136,7 @@ namespace spot { acc_cond::mark_t acc = 0U; unsigned scc = si.scc_of(src); - if (!si.is_accepting_scc(scc) && !si.is_trivial(scc)) + if (si.is_rejecting_scc(scc) && !si.is_trivial(scc)) acc = all_acc; // Keep track of all conditions on transition leaving state diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 849be2468..4ee43a9a2 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -80,9 +80,8 @@ namespace spot bool is_weak_scc(scc_info& map, unsigned scc) { - // If no cycle is accepting, the SCC is weak. - if (!map.is_accepting_scc(scc) - && !map.get_aut()->acc().uses_fin_acceptance()) + // Rejecting SCCs are weak. + if (map.is_rejecting_scc(scc)) return true; // If all transitions use the same acceptance set, the SCC is weak. return map.used_acc_of(scc).size() == 1; diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc index 4a9c3742a..b391fabee 100644 --- a/src/tgbaalgos/remfin.cc +++ b/src/tgbaalgos/remfin.cc @@ -292,6 +292,9 @@ namespace spot res->new_transition(s, t.dst, t.cond, (t.acc & main_sets) | main_add); + if (si.is_rejecting_scc(n)) + continue; + // Create clones for (unsigned i = 0; i < cs; ++i) if (m & rem[i]) diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 72127c239..5d8db0524 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -40,8 +40,12 @@ namespace spot for (auto& scc: *si) { - if (!scc.is_accepting()) + if (scc.is_rejecting()) continue; + // Non-rejecting SCCs should necessarily be accepting, because + // with only one self loop, there should be no ambiguity. + if (!scc.is_accepting()) + return false; // Accepting SCCs should have only one state. auto& st = scc.states(); if (st.size() != 1) diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index f2026cef2..cdda763d1 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -115,7 +115,7 @@ namespace spot // the destination in not in an accepting SCC, // or if we are between SCC with early_susp unset. unsigned u = this->si->scc_of(dst); - if (!this->si->is_accepting_scc(u) + if (this->si->is_rejecting_scc(u) || (!early_susp && (u != this->si->scc_of(src)))) cond = bdd_exist(cond, suspvars); } @@ -147,7 +147,7 @@ namespace spot unsigned u = this->si->scc_of(src); // If the transition is between two SCCs, or in a // non-accepting SCC. Remove the acceptance sets. - if (!this->si->is_accepting_scc(u) || u != this->si->scc_of(dst)) + if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst)) acc = 0U; } @@ -173,7 +173,7 @@ namespace spot std::tie(keep, cond, acc) = this->next_filter::trans(src, dst, cond, acc); - if (!this->si->is_accepting_scc(this->si->scc_of(dst))) + if (this->si->is_rejecting_scc(this->si->scc_of(dst))) acc = 0U; return filtered_trans(keep, cond, acc); } @@ -206,7 +206,7 @@ namespace spot unsigned max = 0; // Max number of useful sets for (unsigned n = 0; n < scc_count; ++n) { - if (!this->si->is_accepting_scc(n)) + if (this->si->is_rejecting_scc(n)) continue; strip_[n] = acc.useless(used_acc[n].begin(), used_acc[n].end()); cnt[n] = acc.num_sets() - strip_[n].count(); @@ -218,7 +218,7 @@ namespace spot // that do not have enough. for (unsigned n = 0; n < scc_count; ++n) { - if (!this->si->is_accepting_scc(n)) + if (this->si->is_rejecting_scc(n)) continue; if (cnt[n] < max) strip_[n].remove_some(max - cnt[n]); @@ -237,7 +237,7 @@ namespace spot { unsigned u = this->si->scc_of(dst); - if (!this->si->is_accepting_scc(u)) + if (this->si->is_rejecting_scc(u)) acc = 0U; else acc = acc.strip(strip_[u]); diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index 9e5f1289e..8dc82c935 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -120,7 +120,10 @@ namespace spot node_.emplace_back(acc, triv); std::swap(node_.back().succ_, root_.front().node.succ_); std::swap(node_.back().states_, root_.front().node.states_); - node_.back().accepting_ = !triv && aut->acc().accepting(acc); + node_.back().accepting_ = + !triv && root_.front().node.accepting_; + node_.back().rejecting_ = + triv || !aut->acc().inf_satisfiable(acc); root_.pop_front(); // Record the transition between the SCC being popped // and the previous SCC. @@ -177,7 +180,7 @@ namespace spot // non-dead SCC has necessarily been crossed by our path to // this state: there is a state S2 in our path which belongs // to this SCC too. We are going to merge all states between - // this S1 and S2 into this SCC. + // this S1 and S2 into this SCC.. // // This merge is easy to do because the order of the SCC in // ROOT is descending: we just have to merge all SCCs from the @@ -186,17 +189,24 @@ namespace spot int threshold = spi; std::list states; scc_succs succs; + bool is_accepting = false; + // If this is a self-loop, check its acceptance alone. + if (dest == succ->src) + is_accepting = aut->acc().accepting(acc); + + assert(!root_.empty()); while (threshold > root_.front().index) { - assert(!root_.empty()); acc |= root_.front().node.acc_; acc |= root_.front().in_acc; + is_accepting |= root_.front().node.accepting_; states.splice(states.end(), root_.front().node.states_); succs.insert(succs.end(), root_.front().node.succ_.begin(), root_.front().node.succ_.end()); root_.pop_front(); + assert(!root_.empty()); } // Note that we do not always have @@ -207,6 +217,8 @@ namespace spot // Accumulate all acceptance conditions, states, SCC // successors, and conditions into the merged SCC. root_.front().node.acc_ |= acc; + root_.front().node.accepting_ |= is_accepting + || aut->acc().accepting(root_.front().node.acc_); root_.front().node.states_.splice(root_.front().node.states_.end(), states); root_.front().node.succ_.insert(root_.front().node.succ_.end(), @@ -215,12 +227,12 @@ namespace spot root_.front().node.trivial_ = false; } - // An SCC is useful if it is accepting or it has a successor SCC - // that is useful. + // An SCC is useful if it is not rejecting or it has a successor + // SCC that is useful. unsigned scccount = scc_count(); for (unsigned i = 0; i < scccount; ++i) { - if (node_[i].is_accepting()) + if (!node_[i].is_rejecting()) { node_[i].useful_ = true; continue; @@ -253,7 +265,7 @@ namespace spot for (unsigned src = 0; src < n; ++src) { unsigned src_scc = scc_of(src); - if (src_scc == -1U || !is_accepting_scc(src_scc)) + if (src_scc == -1U || is_rejecting_scc(src_scc)) continue; auto& s = result[src_scc]; for (auto& t: aut_->out(src)) @@ -272,7 +284,7 @@ namespace spot std::vector result(scc_count()); auto acc = used_acc(); for (unsigned s = 0; s < n; ++s) - result[s] = !is_accepting_scc(s) || acc[s].size() == 1; + result[s] = is_rejecting_scc(s) || acc[s].size() == 1; return result; } diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 1d209312c..648f139e7 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -48,11 +48,13 @@ namespace spot acc_cond::mark_t acc_; std::list states_; // States of the component bool trivial_:1; - bool accepting_:1; + bool accepting_:1; // Necessarily accepting + bool rejecting_:1; // Necessarily rejecting bool useful_:1; public: scc_node(): - acc_(0U), trivial_(true), accepting_(false), useful_(false) + acc_(0U), trivial_(true), accepting_(false), + rejecting_(false), useful_(false) { } @@ -66,11 +68,24 @@ namespace spot return trivial_; } + /// \brief True if we are sure that the SCC is accepting + /// + /// Note that both is_accepting() and is_rejecting() may return + /// false if an SCC interesects a mix of Fin and Inf sets. bool is_accepting() const { return accepting_; } + // True if we are sure that the SCC is rejecting + /// + /// Note that both is_accepting() and is_rejecting() may return + /// false if an SCC interesects a mix of Fin and Inf sets. + bool is_rejecting() const + { + return rejecting_; + } + bool is_useful() const { return useful_; @@ -179,6 +194,11 @@ namespace spot return node(scc).is_accepting(); } + bool is_rejecting_scc(unsigned scc) const + { + return node(scc).is_rejecting(); + } + bool is_useful_scc(unsigned scc) const { return node(scc).is_useful(); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 546c395f3..37ebe2f86 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -98,6 +98,7 @@ TESTS = \ randomize.test \ lbttparse.test \ scc.test \ + sccdot.test \ sccsimpl.test \ dbacomp.test \ obligation.test \ diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index bbca2c11d..376961805 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -332,10 +332,12 @@ digraph G { I [label="", style=invis, width=0] I -> 0 subgraph cluster_0 { + color=green label="" 1 [label="1", peripheries=2] } subgraph cluster_1 { + color=red label="" 0 [label="0"] } diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 84b20350b..49fc0d20d 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -314,12 +314,15 @@ digraph G { I [label="", style=invis, height=0] I -> 3 subgraph cluster_0 { + color=green 1 [label="s1", peripheries=2] } subgraph cluster_1 { + color=green 0 [label="s0", peripheries=2] } subgraph cluster_2 { + color=black 3 [label="s3"] } 0 -> 0 [label="b"] diff --git a/src/tgbatest/sccdot.test b/src/tgbatest/sccdot.test new file mode 100755 index 000000000..1a291e386 --- /dev/null +++ b/src/tgbatest/sccdot.test @@ -0,0 +1,149 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# l'Epita +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +set -e + +# Check the scc_info categorization of SCCs as accepting/rejecting +# by looking at the dot output. +cat < in.hoa +HOA: v1 +States: 11 +Start: 1 +AP: 2 "a" "b" +acc-name: generalized-Buchi 2 +Acceptance: 3 Inf(0)&Inf(1)&Fin(2) +--BODY-- +State: 0 {2} +[0&1] 0 {0 1} +[!0&!1] 0 +[0] 5 +State: 1 +[1] 4 +[0&!1] 3 +State: 4 +[!1] 4 {1 2} +[1] 2 +State: 2 +[0] 0 +[1] 7 +State: 3 +[0&1] 1 {1 0} +State: 5 +[t] 6 +State: 6 +[t] 5 +State: 7 +[!0&1] 7 {0 1} /* This state and the next one differs by */ +[0&1] 7 {0 2} /* the order of the self loops. */ +[t] 8 +State: 8 +[!0&1] 8 {0 2} +[0&1] 8 {0 1} +[t] 9 +State: 9 +[!0&1] 9 {0 2} +[0&1] 10 {0 1} +State: 10 +[!0&1] 9 {0 1} +[0&1] 10 {0 2} +--END-- +EOF + +run 0 ../../bin/autfilt --dot=as in.hoa > out.dot + +# The important stuff is the color=xxx lines +cat <expected +digraph G { + rankdir=LR + label="Fin(2) & (Inf(0)&Inf(1))" + labelloc="t" + I [label="", style=invis, width=0] + I -> 1 + subgraph cluster_0 { + color=grey + label="" + 5 [label="5"] + 6 [label="6"] + } + subgraph cluster_1 { + color=orange + label="" + 0 [label="0"] + } + subgraph cluster_2 { + color=orange + label="" + 9 [label="9"] + 10 [label="10"] + } + subgraph cluster_3 { + color=green + label="" + 8 [label="8"] + } + subgraph cluster_4 { + color=green + label="" + 7 [label="7"] + } + subgraph cluster_5 { + color=black + label="" + 2 [label="2"] + } + subgraph cluster_6 { + color=red + label="" + 4 [label="4"] + } + subgraph cluster_7 { + color=green + label="" + 1 [label="1"] + 3 [label="3"] + } + 0 -> 0 [label="a & b\n{0,1,2}"] + 0 -> 0 [label="!a & !b\n{2}"] + 0 -> 5 [label="a\n{2}"] + 1 -> 4 [label="b"] + 1 -> 3 [label="a & !b"] + 2 -> 0 [label="a"] + 2 -> 7 [label="b"] + 3 -> 1 [label="a & b\n{0,1}"] + 4 -> 4 [label="!b\n{1,2}"] + 4 -> 2 [label="b"] + 5 -> 6 [label="1"] + 6 -> 5 [label="1"] + 7 -> 7 [label="!a & b\n{0,1}"] + 7 -> 7 [label="a & b\n{0,2}"] + 7 -> 8 [label="1"] + 8 -> 8 [label="!a & b\n{0,2}"] + 8 -> 8 [label="a & b\n{0,1}"] + 8 -> 9 [label="1"] + 9 -> 9 [label="!a & b\n{0,2}"] + 9 -> 10 [label="a & b\n{0,1}"] + 10 -> 9 [label="!a & b\n{0,1}"] + 10 -> 10 [label="a & b\n{0,2}"] +} +EOF + +diff out.dot expected