diff --git a/NEWS b/NEWS
index 6b1fe88b9..220250133 100644
--- a/NEWS
+++ b/NEWS
@@ -1,29 +1,4 @@
-New in spot 2.9.0.dev (not yet released)
-
- Command-line tools:
-
- - 'ltl2tgba -G -D' is now better at handling formulas that use
- '<->' and 'xor' operators at the top level. For instance
- ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
- now produces a 16-state automaton (instead of 31 in Spot 2.9).
-
- - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
- It can now take three values:
- 0: never attempt this optimization,
- 1: always try to determinize and minimize automata as WDBA,
- and check (if needed) that the result is correct,
- 2: determinize and minimize automata as WDBA only if it is known
- beforehand (by cheap syntactic means) that the result will be
- correct (e.g., the input formula is a syntactic obligation).
- The default is 1 in "--high" mode, 2 in "--medium" mode or in
- "--deterministic --low" mode, and 0 in other "--low" modes.
-
- - ltlsynt learned --algo=ps to use the default conversion to
- deterministic parity automata (the same as ltl2tgba -DP'max odd').
-
- - ltlsynt now has a -x option to fine-tune the translation. See the
- spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
- to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
+New in spot 2.9.1.dev (not yet released)
Library:
@@ -62,8 +37,37 @@ New in spot 2.9.0.dev (not yet released)
file. With this refactoring, we can retrieve both a kripke or a
kripkecube from a PINS file.
+New in spot 2.9.1 (2020-07-15)
+
+ Command-line tools:
+
+ - 'ltl2tgba -G -D' is now better at handling formulas that use
+ '<->' and 'xor' operators at the top level. For instance
+ ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
+ now produces a 16-state automaton (instead of 31 in Spot 2.9).
+
+ - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
+ It can now take three values:
+ 0: never attempt this optimization,
+ 1: always try to determinize and minimize automata as WDBA,
+ and check (if needed) that the result is correct,
+ 2: determinize and minimize automata as WDBA only if it is known
+ beforehand (by cheap syntactic means) that the result will be
+ correct (e.g., the input formula is a syntactic obligation).
+ The default is 1 in "--high" mode, 2 in "--medium" mode or in
+ "--deterministic --low" mode, and 0 in other "--low" modes.
+
+ - ltlsynt learned --algo=ps to use the default conversion to
+ deterministic parity automata (the same as ltl2tgba -DP'max odd').
+
+ - ltlsynt now has a -x option to fine-tune the translation. See the
+ spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
+ to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
+
+ Library:
+
- product_xor() and product_xnor() are two new versions of the
- synchronized product. The only work with operands that are
+ synchronized product. They only work with operands that are
deterministic automata, and build automata whose language are
respectively the symmetric difference of the operands, and the
complement of that.
@@ -101,6 +105,14 @@ New in spot 2.9.0.dev (not yet released)
issues in intersecting_run(), exclusive_run(),
intersecting_word(), exclusive_word(), which all call reduce().
+ - ltlcross used to crash with "Too many acceptance sets used. The
+ limit is 32." when complementing an automaton would require more
+ acceptance sets than supported by Spot. This is now diagnosed
+ with --verbose, but does not prevent ltlcross from continuing.
+
+ - scc_info::edges_of() and scc_info::inner_edges_of() now correctly
+ honor any filter passed to scc_info.
+
New in spot 2.9 (2020-04-30)
Command-line tools:
diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index a7f9fa1da..fd8deb228 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -1336,25 +1336,37 @@ namespace
&& !spot::is_universal(from[i]))
missing_complement = true;
else
- to[i] = spot::complement(from[i], aborter);
- if (verbose)
- {
- if (to[i])
- {
- std::cerr << "\t(";
- printsize(from[i]);
- std::cerr << ") -> (";
- printsize(to[i]);
- std::cerr << ")\tComp(" << prefix << i << ")\n";
- }
- else
- {
- std::cerr << "\tnot complemented";
- if (aborter)
- aborter->print_reason(std::cerr << " (") << ')';
- std::cerr << '\n';
- }
- }
+ try
+ {
+ to[i] = spot::complement(from[i], aborter);
+ if (verbose)
+ {
+ if (to[i])
+ {
+ std::cerr << "\t(";
+ printsize(from[i]);
+ std::cerr << ") -> (";
+ printsize(to[i]);
+ std::cerr << ")\tComp(" << prefix
+ << i << ")\n";
+ }
+ else
+ {
+ std::cerr << "\tnot complemented";
+ if (aborter)
+ aborter->print_reason(std::cerr
+ << " (") << ')';
+ std::cerr << '\n';
+ }
+ }
+ }
+ catch (const std::runtime_error& re)
+ {
+ missing_complement = true;
+ if (verbose)
+ std::cerr << "\tnot complemented ("
+ << re.what() << ")\n";
+ }
}
};
missing_complement = false;
diff --git a/configure.ac b/configure.ac
index 84e7be90e..ac0bd0ee8 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
# along with this program. If not, see .
AC_PREREQ([2.63])
-AC_INIT([spot], [2.9.0.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.9.1.dev], [spot@lrde.epita.fr])
AC_CONFIG_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/setup.org b/doc/org/setup.org
index ad0283119..d94c663e7 100644
--- a/doc/org/setup.org
+++ b/doc/org/setup.org
@@ -1,10 +1,10 @@
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
#+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html
-#+MACRO: SPOTVERSION 2.9
-#+MACRO: LASTRELEASE 2.9
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz][=spot-2.9.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9/NEWS][summary of the changes]]
+#+MACRO: SPOTVERSION 2.9.1
+#+MACRO: LASTRELEASE 2.9.1
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz][=spot-2.9.1.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-1/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2020-04-30
#+ATTR_HTML: :id spotlogo
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index 38774f60b..647675610 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -38,22 +38,6 @@ namespace spot
{
namespace
{
- using EdgeMask = std::vector;
-
- template< typename Edges, typename Apply >
- void for_each_edge(const const_twa_graph_ptr& aut,
- const Edges& edges,
- const EdgeMask& mask,
- Apply apply)
- {
- for (const auto& e: edges)
- {
- unsigned edge_id = aut->edge_number(e);
- if (mask[edge_id])
- apply(edge_id);
- }
- }
-
// Transforms automaton from transition based acceptance to state based
// acceptance.
void make_state_acc(twa_graph_ptr & aut)
@@ -87,7 +71,6 @@ namespace spot
bool is_scc_tba_type(const_twa_graph_ptr aut,
const scc_info& si,
const unsigned scc,
- const std::vector& keep,
const rs_pairs_view& aut_pairs,
std::vector& final)
{
@@ -101,10 +84,8 @@ namespace spot
auto aut_fin_alone = aut_pairs.fins_alone();
if ((scc_acc & aut_fin_alone) != aut_fin_alone)
{
- for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e)
- {
- final[e] = true;
- });
+ for (auto& e: si.edges_of(scc))
+ final[aut->edge_number(e)] = true;
return true;
}
@@ -126,14 +107,14 @@ namespace spot
// final. Otherwise we do not know: it is possible that there is
// a non-accepting cycle in the SCC that does not visit Fᵢ.
std::set unknown;
- for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e)
+ for (auto& ed: si.inner_edges_of(scc))
{
- const auto& ed = aut->edge_data(e);
+ unsigned e = aut->edge_number(ed);
if (ed.acc & scc_infs_alone)
- final[e] = true;
+ final[e] = true;
else
- unknown.insert(e);
- });
+ unknown.insert(e);
+ }
// Erase edges that cannot belong to a cycle, i.e., the edges
// whose 'dst' is not 'src' of any unknown edges.
@@ -182,13 +163,11 @@ namespace spot
for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc)
{
- for_each_edge(aut, si.edges_of(uscc), keep, [&](unsigned e)
- {
- unknown.erase(e);
- });
+ for (auto& e: si.edges_of(uscc))
+ unknown.erase(aut->edge_number(e));
if (si.is_rejecting_scc(uscc))
continue;
- if (!is_scc_tba_type(aut, si, uscc, keep, aut_pairs, final))
+ if (!is_scc_tba_type(aut, si, uscc, aut_pairs, final))
return false;
}
}
@@ -229,10 +208,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector scc_is_tba_type(si.scc_count(), false);
std::vector final(aut->edge_vector().size(), false);
- std::vector keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
- scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep,
+ scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc,
aut_pairs, final);
auto res = make_twa_graph(aut->get_dict());
@@ -804,10 +782,9 @@ namespace spot
// if is TBA type
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector final(aut->edge_vector().size(), false);
- std::vector keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
- if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
+ if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return false;
return true;
@@ -827,10 +804,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector final(aut->edge_vector().size(), false);
- std::vector keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
- if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
+ if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return nullptr;
auto res = make_twa_graph(aut, twa::prop_set::all());
diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh
index 3c31c3dcd..a76ca3612 100644
--- a/spot/twaalgos/sccinfo.hh
+++ b/spot/twaalgos/sccinfo.hh
@@ -27,6 +27,38 @@ namespace spot
{
class scc_info;
+ /// @{
+ /// \ingroup twa_misc
+ /// \brief An edge_filter may be called on each edge to decide what
+ /// to do with it.
+ ///
+ /// The edge filter is called with an edge and a destination. (In
+ /// existential automata the destination is already given by the
+ /// edge, but in alternating automata, one edge may have several
+ /// destinations, and in this case the filter will be called for
+ /// each destination.) The filter should return a value from
+ /// edge_filter_choice.
+ ///
+ /// \c keep means to use the edge normally, as if no filter had
+ /// been given. \c ignore means to pretend the edge does not
+ /// exist (if the destination is only reachable through this edge,
+ /// it will not be visited). \c cut also ignores the edge, but
+ /// it remembers to visit the destination state (as if it were an
+ /// initial state) in case it is not reachable otherwise.
+ ///
+ /// Note that successors between SCCs can only be maintained for
+ /// edges that are kept. If some edges are ignored or cut, the
+ /// SCC graph that you can explore with scc_info::initial() and
+ /// scc_info::succ() will be restricted to the portion reachable
+ /// with "keep" edges. Additionally SCCs might be created when
+ /// edges are cut, but those will not be reachable from
+ /// scc_info::initial()..
+ enum class edge_filter_choice { keep, ignore, cut };
+ typedef edge_filter_choice
+ (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
+ void* filter_data);
+ /// @}
+
namespace internal
{
struct keep_all
@@ -100,6 +132,9 @@ namespace spot
dv_t* dv_;
Filter filt_;
+ edge_filter efilter_;
+ void* efilter_data_;
+
void inc_state_maybe_()
{
@@ -113,21 +148,49 @@ namespace spot
inc_state_maybe_();
}
+ // Do we ignore the current transition?
bool ignore_current()
{
unsigned dst = (*this)->dst;
if ((int)dst >= 0)
- // Non-universal branching => a single destination.
- return !filt_(&(*this)->dst, 1 + &(*this)->dst);
- // Universal branching => multiple destinations.
- const unsigned* d = dv_->data() + ~dst;
- return !filt_(d + 1, d + *d + 1);
+ {
+ // Non-universal branching => a single destination.
+ if (!filt_(&(*this)->dst, 1 + &(*this)->dst))
+ return true;
+ if (efilter_)
+ return efilter_((*tv_)[t_], dst, efilter_data_)
+ != edge_filter_choice::keep;
+ return false;
+ }
+ else
+ {
+ // Universal branching => multiple destinations.
+ const unsigned* d = dv_->data() + ~dst;
+ if (!filt_(d + 1, d + *d + 1))
+ return true;
+ if (efilter_)
+ {
+ // Keep the transition if at least one destination
+ // is not filtered.
+ const unsigned* end = d + *d + 1;
+ for (const unsigned* i = d + 1; i != end; ++i)
+ {
+ if (efilter_((*tv_)[t_], *i, efilter_data_)
+ == edge_filter_choice::keep)
+ return false;
+ return true;
+ }
+ }
+ return false;
+ }
}
public:
scc_edge_iterator(state_iterator begin, state_iterator end,
- tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
- : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
+ tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
+ edge_filter efilter, void* efilter_data) noexcept
+ : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
+ efilter_(efilter), efilter_data_(efilter_data)
{
if (pos_ == end_)
return;
@@ -191,22 +254,26 @@ namespace spot
sv_t* sv_;
dv_t* dv_;
Filter filt_;
+ edge_filter efilter_;
+ void* efilter_data_;
public:
scc_edges(state_iterator begin, state_iterator end,
- tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept
- : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt)
+ tv_t* tv, sv_t* sv, dv_t* dv, Filter filt,
+ edge_filter efilter, void* efilter_data) noexcept
+ : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt),
+ efilter_(efilter), efilter_data_(efilter_data)
{
}
iter_t begin() const
{
- return {begin_, end_, tv_, sv_, dv_, filt_};
+ return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_};
}
iter_t end() const
{
- return {end_, end_, nullptr, nullptr, nullptr, filt_};
+ return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr};
}
};
}
@@ -378,36 +445,10 @@ namespace spot
// support that yet.
typedef scc_info_node scc_node;
typedef scc_info_node::scc_succs scc_succs;
- /// @{
- /// \brief An edge_filter may be called on each edge to decide what
- /// to do with it.
- ///
- /// The edge filter is called with an edge and a destination. (In
- /// existential automata the destination is already given by the
- /// edge, but in alternating automata, one edge may have several
- /// destinations, and in this case the filter will be called for
- /// each destination.) The filter should return a value from
- /// edge_filter_choice.
- ///
- /// \c keep means to use the edge normally, as if no filter had
- /// been given. \c ignore means to pretend the edge does not
- /// exist (if the destination is only reachable through this edge,
- /// it will not be visited). \c cut also ignores the edge, but
- /// it remembers to visit the destination state (as if it were an
- /// initial state) in case it is not reachable otherwise.
- ///
- /// Note that successors between SCCs can only be maintained for
- /// edges that are kept. If some edges are ignored or cut, the
- /// SCC graph that you can explore with scc_info::initial() and
- /// scc_info::succ() will be restricted to the portion reachable
- /// with "keep" edges. Additionally SCCs might be created when
- /// edges are cut, but those will not be reachable from
- /// scc_info::initial()..
- enum class edge_filter_choice { keep, ignore, cut };
- typedef edge_filter_choice
- (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
- void* filter_data);
- /// @}
+
+ // These types used to be defined here in Spot up to 2.9.
+ typedef spot::edge_filter_choice edge_filter_choice;
+ typedef spot::edge_filter edge_filter;
protected:
@@ -559,7 +600,7 @@ namespace spot
return {states.begin(), states.end(),
&aut_->edge_vector(), &aut_->states(),
&aut_->get_graph().dests_vector(),
- internal::keep_all()};
+ internal::keep_all(), filter_, const_cast(filter_data_)};
}
/// \brief A fake container to iterate over all edges between
@@ -576,7 +617,8 @@ namespace spot
return {states.begin(), states.end(),
&aut_->edge_vector(), &aut_->states(),
&aut_->get_graph().dests_vector(),
- internal::keep_inner_scc(sccof_, scc)};
+ internal::keep_inner_scc(sccof_, scc), filter_,
+ const_cast(filter_data_)};
}
unsigned one_state_of(unsigned scc) const
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 803b6ba22..e8db7e94b 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -320,6 +320,7 @@ TESTS_twa = \
core/ltlcross.test \
core/spotlbtt2.test \
core/ltlcross2.test \
+ core/ltlcross6.test \
core/autcross.test \
core/autcross2.test \
core/autcross3.test \
diff --git a/tests/core/ltlcross6.test b/tests/core/ltlcross6.test
new file mode 100755
index 000000000..4b0a4b188
--- /dev/null
+++ b/tests/core/ltlcross6.test
@@ -0,0 +1,314 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2020 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
+#
+# 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
+
+cat >fake <<\EOF
+#!/bin/sh
+cat <<\FOO
+HOA: v1 States: 137 Start: 0 AP: 4 "a" "b" "c" "d" acc-name: Buchi
+Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc
+--BODY-- State: 0 [!0&!1&!2&!3] 0 [!0&!1&!2&!3] 1 [!0&!1&!2&!3] 2
+[0&!1&!2&!3] 0 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&!1&!2&!3] 5 [0&!1&!2&!3] 6
+[0&!1&!2&!3] 7 [0&!1&!2&!3] 8 [0&!1&!2&!3] 9 [!0&1&!2&!3] 0 [!0&1&!2&!3]
+10 [!0&1&!2&!3] 11 [!0&1&!2&!3] 12 [0&1&!2&!3] 0 [0&1&!2&!3] 13
+[0&1&!2&!3] 14 [0&1&!2&!3] 15 [0&1&!2&!3] 16 [0&1&!2&!3] 17 [0&1&!2&!3] 18
+[0&1&!2&!3] 19 [!0&!1&2&!3] 0 [!0&!1&2&!3] 20 [!0&!1&2&!3] 21 [0&!1&2&!3]
+0 [0&!1&2&!3] 22 [0&!1&2&!3] 23 [0&!1&2&!3] 24 [0&!1&2&!3] 25 [0&!1&2&!3]
+26 [0&!1&2&!3] 27 [!0&1&2&!3] 0 [!0&1&2&!3] 28 [!0&1&2&!3] 29 [!0&1&2&!3]
+30 [0&1&2&!3] 0 [0&1&2&!3] 31 [0&1&2&!3] 32 [0&1&2&!3] 33 [0&1&2&!3] 34
+[0&1&2&!3] 35 [0&1&2&!3] 36 [0&1&2&!3] 37 [!0&!1&!2&3] 0 [!0&!1&!2&3] 38
+[!0&!1&!2&3] 39 [!0&!1&!2&3] 40 [0&!1&!2&3] 0 [0&!1&!2&3] 41 [0&!1&!2&3]
+42 [0&!1&!2&3] 43 [0&!1&!2&3] 44 [0&!1&!2&3] 45 [0&!1&!2&3] 46 [0&!1&!2&3]
+47 [0&!1&!2&3] 48 [0&!1&!2&3] 49 [!0&1&!2&3] 0 [!0&1&!2&3] 50 [!0&1&!2&3]
+51 [0&1&!2&3] 0 [0&1&!2&3] 52 [0&1&!2&3] 53 [0&1&!2&3] 54 [0&1&!2&3] 55
+[0&1&!2&3] 56 [0&1&!2&3] 57 [0&1&!2&3] 58 [0&1&!2&3] 59 [0&1&!2&3] 60
+[0&1&!2&3] 61 [!0&!1&2&3] 0 [!0&!1&2&3] 62 [!0&!1&2&3] 63 [!0&!1&2&3]
+64 [0&!1&2&3] 0 [0&!1&2&3] 65 [0&!1&2&3] 66 [0&!1&2&3] 67 [0&!1&2&3]
+68 [0&!1&2&3] 69 [0&!1&2&3] 70 [0&!1&2&3] 71 [0&!1&2&3] 72 [0&!1&2&3]
+73 [!0&1&2&3] 0 [!0&1&2&3] 74 [!0&1&2&3] 75 [0&1&2&3] 0 [0&1&2&3] 76
+[0&1&2&3] 77 [0&1&2&3] 78 [0&1&2&3] 79 [0&1&2&3] 80 [0&1&2&3] 81 [0&1&2&3]
+82 [0&1&2&3] 83 State: 1 [!0&!1&!2&3] 1 [0&!1&!2&3] 1 [!0&!1&2&3] 20
+[0&!1&2&3] 20 State: 2 [!0&!1&!2&3] 2 [0&!1&!2&3] 2 [!0&!1&2&3] 21
+[0&!1&2&3] 21 State: 3 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3] 3
+[0&1&!2&!3] 4 [0&!1&2&!3] 3 [0&!1&2&!3] 4 [0&1&2&!3] 3 [0&1&2&!3] 4
+[0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 3 [0&1&!2&3] 4 [0&!1&2&3] 84
+[0&1&2&3] 3 [0&1&2&3] 4 State: 4 {0} [0&!1&!2&!3] 3 [0&1&!2&!3] 13
+[0&!1&2&!3] 22 [0&1&2&!3] 31 [0&!1&!2&3] 41 [0&1&!2&3] 52 [0&!1&2&3]
+65 [0&1&2&3] 76 State: 5 [!0&!1&!2&3] 1 [0&!1&!2&3] 5 [!0&!1&2&3]
+20 [0&!1&2&3] 23 State: 6 [!0&!1&!2&3] 2 [0&!1&!2&3] 6 [!0&!1&2&3]
+21 [0&!1&2&3] 24 State: 7 [0&!1&!2&!3] 7 [0&1&!2&!3] 7 [0&!1&2&!3] 7
+[0&1&2&!3] 7 [0&!1&!2&3] 7 [0&1&!2&3] 7 [0&!1&2&3] 25 [0&1&2&3] 7 State:
+8 [0&!1&!2&!3] 8 [0&1&!2&!3] 8 [0&!1&2&!3] 8 [0&1&2&!3] 8 [0&!1&!2&3] 8
+[0&1&!2&3] 8 [0&!1&2&3] 85 [0&!1&2&3] 86 [0&1&2&3] 8 State: 9 [0&!1&!2&!3]
+9 [0&1&!2&!3] 9 [0&!1&2&!3] 9 [0&1&2&!3] 9 [0&!1&!2&3] 9 [0&1&!2&3]
+9 [0&!1&2&3] 27 [0&1&2&3] 9 State: 10 [!0&!1&!2&!3] 1 [0&!1&!2&!3] 1
+[!0&1&!2&!3] 10 [!0&1&!2&!3] 11 [0&1&!2&!3] 10 [0&1&!2&!3] 11 [!0&!1&2&!3]
+20 [0&!1&2&!3] 20 [!0&1&2&!3] 28 [0&1&2&!3] 28 [!0&1&!2&3] 10 [!0&1&!2&3]
+11 [0&1&!2&3] 10 [0&1&!2&3] 11 [!0&1&2&3] 28 [0&1&2&3] 28 State: 11 {0}
+[!0&!1&!2&!3] 1 [0&!1&!2&!3] 5 [!0&1&!2&!3] 10 [0&1&!2&!3] 14 [!0&!1&2&!3]
+20 [0&!1&2&!3] 23 [!0&1&2&!3] 28 [0&1&2&!3] 32 State: 12 [!0&!1&!2&!3] 2
+[0&!1&!2&!3] 2 [!0&1&!2&!3] 12 [0&1&!2&!3] 12 [!0&!1&2&!3] 21 [0&!1&2&!3]
+21 [!0&1&2&!3] 29 [!0&1&2&!3] 30 [0&1&2&!3] 29 [0&1&2&!3] 30 [!0&1&!2&3]
+12 [0&1&!2&3] 12 [!0&1&2&3] 29 [!0&1&2&3] 30 [0&1&2&3] 29 [0&1&2&3]
+30 State: 13 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3] 13 [0&!1&2&!3]
+22 [0&1&2&!3] 31 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 13 [0&!1&2&3]
+22 [0&1&2&3] 31 State: 14 [!0&!1&!2&!3] 1 [0&!1&!2&!3] 5 [!0&1&!2&!3] 10
+[!0&1&!2&!3] 11 [0&1&!2&!3] 14 [!0&!1&2&!3] 20 [0&!1&2&!3] 23 [!0&1&2&!3]
+28 [0&1&2&!3] 32 [!0&1&!2&3] 10 [!0&1&!2&3] 11 [0&1&!2&3] 14 [!0&1&2&3]
+28 [0&1&2&3] 32 State: 15 [!0&!1&!2&!3] 2 [0&!1&!2&!3] 6 [!0&1&!2&!3] 12
+[0&1&!2&!3] 15 [!0&!1&2&!3] 21 [0&!1&2&!3] 24 [!0&1&2&!3] 29 [!0&1&2&!3]
+30 [0&1&2&!3] 33 [!0&1&!2&3] 12 [0&1&!2&3] 15 [!0&1&2&3] 29 [!0&1&2&3]
+30 [0&1&2&3] 33 State: 16 [0&!1&!2&!3] 7 [0&1&!2&!3] 16 [0&1&!2&!3] 17
+[0&!1&2&!3] 25 [0&1&2&!3] 34 [0&!1&!2&3] 7 [0&1&!2&3] 16 [0&1&!2&3] 17
+[0&!1&2&3] 7 [0&1&2&3] 34 State: 17 {0} [0&!1&!2&!3] 7 [0&1&!2&!3] 16
+[0&!1&2&!3] 25 [0&1&2&!3] 34 [0&!1&!2&3] 45 [0&1&!2&3] 54 [0&!1&2&3]
+68 [0&1&2&3] 77 State: 18 [0&!1&!2&!3] 8 [0&1&!2&!3] 18 [0&!1&2&!3]
+26 [0&1&2&!3] 35 [0&!1&!2&3] 8 [0&1&!2&3] 18 [0&!1&2&3] 26 [0&1&2&3]
+35 State: 19 [0&!1&!2&!3] 9 [0&1&!2&!3] 19 [0&!1&2&!3] 27 [0&1&2&!3]
+36 [0&1&2&!3] 37 [0&!1&!2&3] 9 [0&1&!2&3] 19 [0&!1&2&3] 9 [0&1&2&3]
+36 [0&1&2&3] 37 State: 20 [!0&!1&!2&3] 1 [0&!1&!2&3] 1 [!0&1&!2&3] 10
+[!0&1&!2&3] 11 [0&1&!2&3] 10 [0&1&!2&3] 11 [!0&!1&2&3] 20 [0&!1&2&3]
+20 [!0&1&2&3] 28 [0&1&2&3] 28 State: 21 [!0&!1&!2&3] 2 [0&!1&!2&3] 2
+[!0&1&!2&3] 12 [0&1&!2&3] 12 [!0&!1&2&3] 21 [0&!1&2&3] 21 [!0&1&2&3]
+29 [!0&1&2&3] 30 [0&1&2&3] 29 [0&1&2&3] 30 State: 22 [0&!1&!2&!3] 3
+[0&!1&!2&!3] 4 [0&1&!2&!3] 3 [0&1&!2&!3] 4 [0&!1&2&!3] 3 [0&!1&2&!3]
+4 [0&1&2&!3] 3 [0&1&2&!3] 4 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3]
+13 [0&!1&2&3] 84 [0&1&2&3] 31 State: 23 [!0&!1&!2&3] 1 [0&!1&!2&3] 5
+[!0&1&!2&3] 10 [!0&1&!2&3] 11 [0&1&!2&3] 14 [!0&!1&2&3] 20 [0&!1&2&3]
+23 [!0&1&2&3] 28 [0&1&2&3] 32 State: 24 [!0&!1&!2&3] 2 [0&!1&!2&3] 6
+[!0&1&!2&3] 12 [0&1&!2&3] 15 [!0&!1&2&3] 21 [0&!1&2&3] 24 [!0&1&2&3]
+29 [!0&1&2&3] 30 [0&1&2&3] 33 State: 25 [0&!1&!2&!3] 7 [0&1&!2&!3]
+7 [0&!1&2&!3] 7 [0&1&2&!3] 7 [0&!1&!2&3] 7 [0&1&!2&3] 16 [0&1&!2&3]
+17 [0&!1&2&3] 25 [0&1&2&3] 34 State: 26 [0&!1&!2&!3] 8 [0&1&!2&!3]
+8 [0&!1&2&!3] 8 [0&1&2&!3] 8 [0&!1&!2&3] 8 [0&1&!2&3] 18 [0&!1&2&3]
+85 [0&!1&2&3] 86 [0&1&2&3] 35 State: 27 [0&!1&!2&!3] 9 [0&1&!2&!3]
+9 [0&!1&2&!3] 9 [0&1&2&!3] 9 [0&!1&!2&3] 9 [0&1&!2&3] 19 [0&!1&2&3]
+27 [0&1&2&3] 36 [0&1&2&3] 37 State: 28 [!0&!1&!2&!3] 1 [0&!1&!2&!3] 1
+[!0&1&!2&!3] 10 [!0&1&!2&!3] 11 [0&1&!2&!3] 10 [0&1&!2&!3] 11 [!0&!1&2&!3]
+20 [0&!1&2&!3] 20 [!0&1&2&!3] 28 [0&1&2&!3] 28 State: 29 [!0&!1&!2&!3] 2
+[0&!1&!2&!3] 2 [!0&1&!2&!3] 12 [0&1&!2&!3] 12 [!0&!1&2&!3] 21 [0&!1&2&!3]
+21 [!0&1&2&!3] 29 [!0&1&2&!3] 30 [0&1&2&!3] 29 [0&1&2&!3] 30 State:
+30 {0} [!0&!1&!2&!3] 2 [0&!1&!2&!3] 6 [!0&1&!2&!3] 12 [0&1&!2&!3] 15
+[!0&!1&2&!3] 21 [0&!1&2&!3] 24 [!0&1&2&!3] 29 [0&1&2&!3] 33 State: 31
+[0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3] 13 [0&!1&2&!3] 22 [0&1&2&!3]
+31 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 3 [0&1&!2&3] 4 [0&!1&2&3]
+22 [0&1&2&3] 3 [0&1&2&3] 4 State: 32 [!0&!1&!2&!3] 1 [0&!1&!2&!3] 5
+[!0&1&!2&!3] 10 [!0&1&!2&!3] 11 [0&1&!2&!3] 14 [!0&!1&2&!3] 20 [0&!1&2&!3]
+23 [!0&1&2&!3] 28 [0&1&2&!3] 32 State: 33 [!0&!1&!2&!3] 2 [0&!1&!2&!3] 6
+[!0&1&!2&!3] 12 [0&1&!2&!3] 15 [!0&!1&2&!3] 21 [0&!1&2&!3] 24 [!0&1&2&!3]
+29 [!0&1&2&!3] 30 [0&1&2&!3] 33 State: 34 [0&!1&!2&!3] 7 [0&1&!2&!3] 16
+[0&1&!2&!3] 17 [0&!1&2&!3] 25 [0&1&2&!3] 34 [0&!1&!2&3] 7 [0&1&!2&3]
+7 [0&!1&2&3] 7 [0&1&2&3] 7 State: 35 [0&!1&!2&!3] 8 [0&1&!2&!3] 18
+[0&!1&2&!3] 26 [0&1&2&!3] 35 [0&!1&!2&3] 8 [0&1&!2&3] 8 [0&!1&2&3] 26
+[0&1&2&3] 8 State: 36 [0&!1&!2&!3] 9 [0&1&!2&!3] 19 [0&!1&2&!3] 27
+[0&1&2&!3] 36 [0&1&2&!3] 37 [0&!1&!2&3] 9 [0&1&!2&3] 9 [0&!1&2&3] 9
+[0&1&2&3] 9 State: 37 {0} [0&!1&!2&!3] 9 [0&1&!2&!3] 19 [0&!1&2&!3] 27
+[0&1&2&!3] 36 [0&!1&!2&3] 48 [0&1&!2&3] 59 [0&!1&2&3] 72 [0&1&2&3] 81
+State: 38 [!0&!1&!2&3] 38 [!0&!1&!2&3] 39 [0&!1&!2&3] 38 [0&!1&!2&3] 39
+[!0&!1&2&3] 62 [0&!1&2&3] 62 State: 39 {0} [!0&!1&!2&3] 38 [0&!1&!2&3]
+42 [!0&!1&2&3] 62 [0&!1&2&3] 66 State: 40 [!0&!1&!2&3] 40 [0&!1&!2&3]
+40 [!0&!1&2&3] 63 [!0&!1&2&3] 64 [0&!1&2&3] 63 [0&!1&2&3] 64 State: 41
+[0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3] 3 [0&1&!2&!3] 4 [0&!1&2&!3]
+3 [0&!1&2&!3] 4 [0&1&2&!3] 3 [0&1&2&!3] 4 [0&!1&!2&3] 41 [0&1&!2&3] 3
+[0&1&!2&3] 4 [0&!1&2&3] 65 [0&1&2&3] 3 [0&1&2&3] 4 State: 42 [!0&!1&!2&3]
+38 [!0&!1&!2&3] 39 [0&!1&!2&3] 42 [!0&!1&2&3] 62 [0&!1&2&3] 66 State: 43
+[0&!1&!2&3] 43 [0&!1&!2&3] 44 [0&!1&2&3] 67 State: 44 {0} [0&!1&!2&3]
+43 [0&!1&2&3] 67 State: 45 [0&!1&!2&!3] 7 [0&1&!2&!3] 7 [0&!1&2&!3]
+7 [0&1&2&!3] 7 [0&!1&!2&3] 45 [0&1&!2&3] 7 [0&!1&2&3] 87 [0&1&2&3]
+7 State: 46 [!0&!1&!2&3] 40 [0&!1&!2&3] 46 [!0&!1&2&3] 63 [!0&!1&2&3]
+64 [0&!1&2&3] 69 State: 47 [0&!1&!2&!3] 8 [0&1&!2&!3] 8 [0&!1&2&!3] 8
+[0&1&2&!3] 8 [0&!1&!2&3] 47 [0&1&!2&3] 8 [0&!1&2&3] 70 [0&1&2&3] 8 State:
+48 [0&!1&!2&!3] 9 [0&1&!2&!3] 9 [0&!1&2&!3] 9 [0&1&2&!3] 9 [0&!1&!2&3]
+48 [0&1&!2&3] 9 [0&!1&2&3] 88 [0&1&2&3] 9 State: 49 [0&!1&!2&3] 49
+[0&!1&2&3] 71 [0&!1&2&3] 73 State: 50 [!0&!1&!2&!3] 89 [0&!1&!2&!3]
+89 [!0&1&!2&!3] 50 [0&1&!2&!3] 50 [!0&!1&2&!3] 90 [!0&!1&2&!3] 91
+[0&!1&2&!3] 90 [0&!1&2&!3] 91 [!0&1&2&!3] 74 [0&1&2&!3] 74 [!0&1&!2&3]
+50 [0&1&!2&3] 50 [!0&1&2&3] 74 [0&1&2&3] 74 State: 51 [!0&!1&!2&!3] 92
+[0&!1&!2&!3] 92 [!0&1&!2&!3] 94 [!0&1&!2&!3] 95 [0&1&!2&!3] 94 [0&1&!2&!3]
+95 [!0&!1&2&!3] 93 [0&!1&2&!3] 93 [!0&1&2&!3] 75 [0&1&2&!3] 75 [!0&1&!2&3]
+51 [0&1&!2&3] 51 [!0&1&2&3] 75 [0&1&2&3] 75 State: 52 [0&!1&!2&!3] 41
+[0&1&!2&!3] 52 [0&!1&2&!3] 96 [0&1&2&!3] 76 [0&!1&!2&3] 3 [0&!1&!2&3]
+4 [0&1&!2&3] 52 [0&!1&2&3] 22 [0&1&2&3] 76 State: 53 [0&!1&!2&!3] 97
+[0&1&!2&!3] 99 [0&1&!2&!3] 100 [0&!1&2&!3] 98 [0&1&2&!3] 82 [0&1&!2&3]
+53 [0&1&2&3] 82 State: 54 [0&!1&!2&!3] 45 [0&1&!2&!3] 54 [0&!1&2&!3]
+87 [0&1&2&!3] 77 [0&!1&!2&3] 7 [0&1&!2&3] 54 [0&!1&2&3] 7 [0&1&2&3] 77
+State: 55 [!0&!1&!2&!3] 89 [0&!1&!2&!3] 101 [!0&1&!2&!3] 50 [0&1&!2&!3]
+55 [!0&!1&2&!3] 90 [!0&!1&2&!3] 91 [0&!1&2&!3] 102 [!0&1&2&!3] 74
+[0&1&2&!3] 78 [!0&1&!2&3] 50 [0&1&!2&3] 55 [!0&1&2&3] 74 [0&1&2&3] 78
+State: 56 [!0&!1&!2&!3] 92 [0&!1&!2&!3] 103 [!0&1&!2&!3] 94 [!0&1&!2&!3]
+95 [0&1&!2&!3] 104 [!0&!1&2&!3] 93 [0&!1&2&!3] 105 [!0&1&2&!3] 75
+[0&1&2&!3] 79 [!0&1&!2&3] 51 [0&1&!2&3] 56 [!0&1&2&3] 75 [0&1&2&3] 79
+State: 57 [0&!1&!2&!3] 106 [0&1&!2&!3] 57 [0&!1&2&!3] 107 [0&!1&2&!3]
+108 [0&1&2&!3] 83 [0&1&!2&3] 57 [0&1&2&3] 83 State: 58 [0&!1&!2&!3] 47
+[0&1&!2&!3] 58 [0&!1&2&!3] 70 [0&1&2&!3] 80 [0&!1&!2&3] 8 [0&1&!2&3]
+58 [0&!1&2&3] 8 [0&1&2&3] 80 State: 59 [0&!1&!2&!3] 48 [0&1&!2&!3] 59
+[0&!1&2&!3] 72 [0&1&2&!3] 81 [0&!1&!2&3] 9 [0&1&!2&3] 59 [0&!1&2&3]
+109 [0&1&2&3] 81 State: 60 [0&1&!2&3] 60 [0&1&!2&3] 61 State: 61 {0}
+[0&1&!2&3] 60 State: 62 [!0&!1&!2&3] 38 [!0&!1&!2&3] 39 [0&!1&!2&3] 38
+[0&!1&!2&3] 39 [!0&1&!2&3] 110 [0&1&!2&3] 110 [!0&!1&2&3] 62 [0&!1&2&3]
+62 [!0&1&2&3] 111 [0&1&2&3] 111 State: 63 [!0&!1&!2&3] 40 [0&!1&!2&3] 40
+[!0&1&!2&3] 112 [0&1&!2&3] 112 [!0&!1&2&3] 63 [!0&!1&2&3] 64 [0&!1&2&3]
+63 [0&!1&2&3] 64 [!0&1&2&3] 113 [0&1&2&3] 113 State: 64 {0} [!0&!1&!2&3]
+40 [0&!1&!2&3] 46 [!0&!1&2&3] 63 [0&!1&2&3] 69 State: 65 [0&!1&!2&!3]
+3 [0&!1&!2&!3] 4 [0&1&!2&!3] 3 [0&1&!2&!3] 4 [0&!1&2&!3] 3 [0&!1&2&!3]
+4 [0&1&2&!3] 3 [0&1&2&!3] 4 [0&!1&!2&3] 41 [0&1&!2&3] 114 [0&!1&2&3] 65
+[0&1&2&3] 115 State: 66 [!0&!1&!2&3] 38 [!0&!1&!2&3] 39 [0&!1&!2&3] 42
+[!0&1&!2&3] 110 [0&1&!2&3] 116 [!0&!1&2&3] 62 [0&!1&2&3] 66 [!0&1&2&3]
+111 [0&1&2&3] 117 State: 67 [0&!1&!2&3] 43 [0&!1&!2&3] 44 [0&1&!2&3]
+118 [0&!1&2&3] 67 [0&1&2&3] 119 State: 68 [0&!1&!2&!3] 7 [0&1&!2&!3] 7
+[0&!1&2&!3] 7 [0&1&2&!3] 7 [0&!1&!2&3] 45 [0&1&!2&3] 120 [0&!1&2&3] 87
+[0&1&2&3] 121 State: 69 [!0&!1&!2&3] 40 [0&!1&!2&3] 46 [!0&1&!2&3] 112
+[0&1&!2&3] 122 [!0&!1&2&3] 63 [!0&!1&2&3] 64 [0&!1&2&3] 69 [!0&1&2&3]
+113 [0&1&2&3] 123 State: 70 [0&!1&!2&!3] 8 [0&1&!2&!3] 8 [0&!1&2&!3]
+8 [0&1&2&!3] 8 [0&!1&!2&3] 47 [0&1&!2&3] 58 [0&!1&2&3] 70 [0&1&2&3]
+80 State: 71 {0} [0&!1&!2&3] 49 [0&!1&2&3] 73 State: 72 [0&!1&!2&!3]
+9 [0&1&!2&!3] 9 [0&!1&2&!3] 9 [0&1&2&!3] 9 [0&!1&!2&3] 48 [0&1&!2&3]
+59 [0&!1&2&3] 88 [0&1&2&3] 81 State: 73 [0&!1&!2&3] 49 [0&1&!2&3] 124
+[0&!1&2&3] 71 [0&!1&2&3] 73 [0&1&2&3] 125 State: 74 [!0&!1&!2&!3]
+89 [0&!1&!2&!3] 89 [!0&1&!2&!3] 50 [0&1&!2&!3] 50 [!0&!1&2&!3] 90
+[!0&!1&2&!3] 91 [0&!1&2&!3] 90 [0&!1&2&!3] 91 [!0&1&2&!3] 74 [0&1&2&!3] 74
+State: 75 [!0&!1&!2&!3] 92 [0&!1&!2&!3] 92 [!0&1&!2&!3] 94 [!0&1&!2&!3] 95
+[0&1&!2&!3] 94 [0&1&!2&!3] 95 [!0&!1&2&!3] 93 [0&!1&2&!3] 93 [!0&1&2&!3]
+75 [0&1&2&!3] 75 State: 76 [0&!1&!2&!3] 41 [0&1&!2&!3] 52 [0&!1&2&!3]
+96 [0&1&2&!3] 76 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 3 [0&1&!2&3]
+4 [0&!1&2&3] 22 [0&1&2&3] 3 [0&1&2&3] 4 State: 77 [0&!1&!2&!3] 45
+[0&1&!2&!3] 54 [0&!1&2&!3] 87 [0&1&2&!3] 77 [0&!1&!2&3] 7 [0&1&!2&3]
+7 [0&!1&2&3] 7 [0&1&2&3] 7 State: 78 [!0&!1&!2&!3] 89 [0&!1&!2&!3] 101
+[!0&1&!2&!3] 50 [0&1&!2&!3] 55 [!0&!1&2&!3] 90 [!0&!1&2&!3] 91 [0&!1&2&!3]
+102 [!0&1&2&!3] 74 [0&1&2&!3] 78 State: 79 [!0&!1&!2&!3] 92 [0&!1&!2&!3]
+103 [!0&1&!2&!3] 94 [!0&1&!2&!3] 95 [0&1&!2&!3] 104 [!0&!1&2&!3] 93
+[0&!1&2&!3] 105 [!0&1&2&!3] 75 [0&1&2&!3] 79 State: 80 [0&!1&!2&!3] 47
+[0&1&!2&!3] 58 [0&!1&2&!3] 70 [0&1&2&!3] 80 [0&!1&!2&3] 8 [0&1&!2&3]
+8 [0&!1&2&3] 8 [0&1&2&3] 8 State: 81 [0&!1&!2&!3] 48 [0&1&!2&!3] 59
+[0&!1&2&!3] 72 [0&1&2&!3] 81 [0&!1&!2&3] 9 [0&1&!2&3] 9 [0&!1&2&3] 109
+[0&1&2&3] 9 State: 82 [0&!1&!2&!3] 97 [0&1&!2&!3] 99 [0&1&!2&!3] 100
+[0&!1&2&!3] 98 [0&1&2&!3] 82 State: 83 [0&!1&!2&!3] 106 [0&1&!2&!3] 57
+[0&!1&2&!3] 107 [0&!1&2&!3] 108 [0&1&2&!3] 83 State: 84 [0&!1&!2&!3] 3
+[0&!1&!2&!3] 4 [0&1&!2&!3] 3 [0&1&!2&!3] 4 [0&!1&2&!3] 3 [0&!1&2&!3] 4
+[0&1&2&!3] 3 [0&1&2&!3] 4 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 127
+[0&!1&2&3] 84 [0&1&2&3] 126 State: 85 [0&!1&!2&!3] 8 [0&1&!2&!3] 8
+[0&!1&2&!3] 8 [0&1&2&!3] 8 [0&!1&!2&3] 8 [0&1&!2&3] 128 [0&!1&2&3] 85
+[0&!1&2&3] 86 [0&1&2&3] 129 State: 86 {0} [0&!1&!2&!3] 8 [0&1&!2&!3] 18
+[0&!1&2&!3] 26 [0&1&2&!3] 35 [0&!1&!2&3] 47 [0&1&!2&3] 58 [0&!1&2&3]
+70 [0&1&2&3] 80 State: 87 [0&!1&!2&!3] 7 [0&1&!2&!3] 7 [0&!1&2&!3]
+7 [0&1&2&!3] 7 [0&!1&!2&3] 45 [0&1&!2&3] 54 [0&!1&2&3] 87 [0&1&2&3]
+77 State: 88 [0&!1&!2&!3] 9 [0&1&!2&!3] 9 [0&!1&2&!3] 9 [0&1&2&!3] 9
+[0&!1&!2&3] 48 [0&1&!2&3] 130 [0&!1&2&3] 88 [0&1&2&3] 131 State: 89
+[!0&!1&!2&3] 89 [0&!1&!2&3] 89 [!0&!1&2&3] 90 [!0&!1&2&3] 91 [0&!1&2&3]
+90 [0&!1&2&3] 91 State: 90 [!0&!1&!2&3] 89 [0&!1&!2&3] 89 [!0&1&!2&3]
+50 [0&1&!2&3] 50 [!0&!1&2&3] 90 [!0&!1&2&3] 91 [0&!1&2&3] 90 [0&!1&2&3]
+91 [!0&1&2&3] 74 [0&1&2&3] 74 State: 91 {0} [!0&1&!2&3] 50 [0&1&!2&3]
+55 [!0&1&2&3] 74 [0&1&2&3] 78 State: 92 [!0&!1&!2&3] 92 [0&!1&!2&3] 92
+[!0&!1&2&3] 93 [0&!1&2&3] 93 State: 93 [!0&!1&!2&3] 92 [0&!1&!2&3] 92
+[!0&1&!2&3] 94 [!0&1&!2&3] 95 [0&1&!2&3] 94 [0&1&!2&3] 95 [!0&!1&2&3]
+93 [0&!1&2&3] 93 [!0&1&2&3] 75 [0&1&2&3] 75 State: 94 [!0&!1&!2&!3]
+92 [0&!1&!2&!3] 92 [!0&1&!2&!3] 94 [!0&1&!2&!3] 95 [0&1&!2&!3] 94
+[0&1&!2&!3] 95 [!0&!1&2&!3] 93 [0&!1&2&!3] 93 [!0&1&2&!3] 75 [0&1&2&!3]
+75 [!0&1&!2&3] 94 [!0&1&!2&3] 95 [0&1&!2&3] 94 [0&1&!2&3] 95 [!0&1&2&3]
+75 [0&1&2&3] 75 State: 95 {0} [!0&1&!2&3] 51 [0&1&!2&3] 56 [!0&1&2&3]
+75 [0&1&2&3] 79 State: 96 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3]
+3 [0&1&!2&!3] 4 [0&!1&2&!3] 3 [0&!1&2&!3] 4 [0&1&2&!3] 3 [0&1&2&!3]
+4 [0&!1&!2&3] 41 [0&1&!2&3] 52 [0&!1&2&3] 65 [0&1&2&3] 76 State: 97
+[0&!1&!2&3] 97 [0&!1&2&3] 98 State: 98 [0&!1&!2&3] 97 [0&1&!2&3] 99
+[0&1&!2&3] 100 [0&!1&2&3] 98 [0&1&2&3] 82 State: 99 [0&!1&!2&!3] 97
+[0&1&!2&!3] 99 [0&1&!2&!3] 100 [0&!1&2&!3] 98 [0&1&2&!3] 82 [0&1&!2&3]
+99 [0&1&!2&3] 100 [0&1&2&3] 82 State: 100 {0} [0&1&!2&3] 53 [0&1&2&3]
+82 State: 101 [!0&!1&!2&3] 89 [0&!1&!2&3] 101 [!0&!1&2&3] 90 [!0&!1&2&3]
+91 [0&!1&2&3] 102 State: 102 [!0&!1&!2&3] 89 [0&!1&!2&3] 101 [!0&1&!2&3]
+50 [0&1&!2&3] 55 [!0&!1&2&3] 90 [!0&!1&2&3] 91 [0&!1&2&3] 102 [!0&1&2&3]
+74 [0&1&2&3] 78 State: 103 [!0&!1&!2&3] 92 [0&!1&!2&3] 103 [!0&!1&2&3] 93
+[0&!1&2&3] 105 State: 104 [!0&!1&!2&!3] 92 [0&!1&!2&!3] 103 [!0&1&!2&!3]
+94 [!0&1&!2&!3] 95 [0&1&!2&!3] 104 [!0&!1&2&!3] 93 [0&!1&2&!3] 105
+[!0&1&2&!3] 75 [0&1&2&!3] 79 [!0&1&!2&3] 94 [!0&1&!2&3] 95 [0&1&!2&3] 104
+[!0&1&2&3] 75 [0&1&2&3] 79 State: 105 [!0&!1&!2&3] 92 [0&!1&!2&3] 103
+[!0&1&!2&3] 94 [!0&1&!2&3] 95 [0&1&!2&3] 104 [!0&!1&2&3] 93 [0&!1&2&3]
+105 [!0&1&2&3] 75 [0&1&2&3] 79 State: 106 [0&!1&!2&3] 106 [0&!1&2&3]
+107 [0&!1&2&3] 108 State: 107 [0&!1&!2&3] 106 [0&1&!2&3] 57 [0&!1&2&3]
+107 [0&!1&2&3] 108 [0&1&2&3] 83 State: 108 {0} [0&1&!2&3] 57 [0&1&2&3]
+83 State: 109 [0&!1&!2&!3] 9 [0&1&!2&!3] 9 [0&!1&2&!3] 9 [0&1&2&!3] 9
+[0&!1&!2&3] 9 [0&1&!2&3] 132 [0&!1&2&3] 27 [0&1&2&3] 133 State: 110
+[!0&!1&!2&!3] 38 [!0&!1&!2&!3] 39 [0&!1&!2&!3] 38 [0&!1&!2&!3]
+39 [!0&1&!2&!3] 110 [0&1&!2&!3] 110 [!0&!1&2&!3] 62 [0&!1&2&!3]
+62 [!0&1&2&!3] 111 [0&1&2&!3] 111 [!0&1&!2&3] 110 [0&1&!2&3] 110
+[!0&1&2&3] 111 [0&1&2&3] 111 State: 111 [!0&!1&!2&!3] 38 [!0&!1&!2&!3]
+39 [0&!1&!2&!3] 38 [0&!1&!2&!3] 39 [!0&1&!2&!3] 110 [0&1&!2&!3] 110
+[!0&!1&2&!3] 62 [0&!1&2&!3] 62 [!0&1&2&!3] 111 [0&1&2&!3] 111 State:
+112 [!0&!1&!2&!3] 40 [0&!1&!2&!3] 40 [!0&1&!2&!3] 112 [0&1&!2&!3]
+112 [!0&!1&2&!3] 63 [!0&!1&2&!3] 64 [0&!1&2&!3] 63 [0&!1&2&!3]
+64 [!0&1&2&!3] 113 [0&1&2&!3] 113 [!0&1&!2&3] 112 [0&1&!2&3] 112
+[!0&1&2&3] 113 [0&1&2&3] 113 State: 113 [!0&!1&!2&!3] 40 [0&!1&!2&!3]
+40 [!0&1&!2&!3] 112 [0&1&!2&!3] 112 [!0&!1&2&!3] 63 [!0&!1&2&!3] 64
+[0&!1&2&!3] 63 [0&!1&2&!3] 64 [!0&1&2&!3] 113 [0&1&2&!3] 113 State:
+114 [0&!1&!2&!3] 41 [0&1&!2&!3] 114 [0&!1&2&!3] 65 [0&1&2&!3] 115
+[0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 114 [0&!1&2&3] 3 [0&!1&2&3] 4
+[0&1&2&3] 115 State: 115 [0&!1&!2&!3] 41 [0&1&!2&!3] 114 [0&!1&2&!3]
+65 [0&1&2&!3] 115 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 3 [0&1&!2&3] 4
+[0&!1&2&3] 3 [0&!1&2&3] 4 [0&1&2&3] 3 [0&1&2&3] 4 State: 116 [!0&!1&!2&!3]
+38 [!0&!1&!2&!3] 39 [0&!1&!2&!3] 42 [!0&1&!2&!3] 110 [0&1&!2&!3] 116
+[!0&!1&2&!3] 62 [0&!1&2&!3] 66 [!0&1&2&!3] 111 [0&1&2&!3] 117 [!0&1&!2&3]
+110 [0&1&!2&3] 116 [!0&1&2&3] 111 [0&1&2&3] 117 State: 117 [!0&!1&!2&!3]
+38 [!0&!1&!2&!3] 39 [0&!1&!2&!3] 42 [!0&1&!2&!3] 110 [0&1&!2&!3] 116
+[!0&!1&2&!3] 62 [0&!1&2&!3] 66 [!0&1&2&!3] 111 [0&1&2&!3] 117 State:
+118 [0&!1&!2&!3] 43 [0&!1&!2&!3] 44 [0&1&!2&!3] 118 [0&!1&2&!3] 67
+[0&1&2&!3] 119 [0&1&!2&3] 118 [0&1&2&3] 119 State: 119 [0&!1&!2&!3] 43
+[0&!1&!2&!3] 44 [0&1&!2&!3] 118 [0&!1&2&!3] 67 [0&1&2&!3] 119 State: 120
+[0&!1&!2&!3] 45 [0&1&!2&!3] 120 [0&!1&2&!3] 68 [0&1&2&!3] 121 [0&!1&!2&3]
+7 [0&1&!2&3] 120 [0&!1&2&3] 134 [0&1&2&3] 121 State: 121 [0&!1&!2&!3] 45
+[0&1&!2&!3] 120 [0&!1&2&!3] 68 [0&1&2&!3] 121 [0&!1&!2&3] 7 [0&1&!2&3]
+7 [0&!1&2&3] 134 [0&1&2&3] 7 State: 122 [!0&!1&!2&!3] 40 [0&!1&!2&!3]
+46 [!0&1&!2&!3] 112 [0&1&!2&!3] 122 [!0&!1&2&!3] 63 [!0&!1&2&!3] 64
+[0&!1&2&!3] 69 [!0&1&2&!3] 113 [0&1&2&!3] 123 [!0&1&!2&3] 112 [0&1&!2&3]
+122 [!0&1&2&3] 113 [0&1&2&3] 123 State: 123 [!0&!1&!2&!3] 40 [0&!1&!2&!3]
+46 [!0&1&!2&!3] 112 [0&1&!2&!3] 122 [!0&!1&2&!3] 63 [!0&!1&2&!3] 64
+[0&!1&2&!3] 69 [!0&1&2&!3] 113 [0&1&2&!3] 123 State: 124 [0&!1&!2&!3] 49
+[0&1&!2&!3] 124 [0&!1&2&!3] 71 [0&!1&2&!3] 73 [0&1&2&!3] 125 [0&1&!2&3]
+124 [0&1&2&3] 125 State: 125 [0&!1&!2&!3] 49 [0&1&!2&!3] 124 [0&!1&2&!3]
+71 [0&!1&2&!3] 73 [0&1&2&!3] 125 State: 126 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4
+[0&1&!2&!3] 127 [0&!1&2&!3] 84 [0&1&2&!3] 126 [0&!1&!2&3] 3 [0&!1&!2&3] 4
+[0&1&!2&3] 3 [0&1&!2&3] 4 [0&!1&2&3] 3 [0&!1&2&3] 4 [0&1&2&3] 3 [0&1&2&3]
+4 State: 127 [0&!1&!2&!3] 3 [0&!1&!2&!3] 4 [0&1&!2&!3] 127 [0&!1&2&!3]
+84 [0&1&2&!3] 126 [0&!1&!2&3] 3 [0&!1&!2&3] 4 [0&1&!2&3] 127 [0&!1&2&3]
+3 [0&!1&2&3] 4 [0&1&2&3] 126 State: 128 [0&!1&!2&!3] 8 [0&1&!2&!3] 128
+[0&!1&2&!3] 85 [0&!1&2&!3] 86 [0&1&2&!3] 129 [0&!1&!2&3] 8 [0&1&!2&3]
+128 [0&!1&2&3] 8 [0&1&2&3] 129 State: 129 [0&!1&!2&!3] 8 [0&1&!2&!3] 128
+[0&!1&2&!3] 85 [0&!1&2&!3] 86 [0&1&2&!3] 129 [0&!1&!2&3] 8 [0&1&!2&3]
+8 [0&!1&2&3] 8 [0&1&2&3] 8 State: 130 [0&!1&!2&!3] 48 [0&1&!2&!3] 130
+[0&!1&2&!3] 88 [0&1&2&!3] 131 [0&!1&!2&3] 9 [0&1&!2&3] 130 [0&!1&2&3]
+9 [0&1&2&3] 131 State: 131 [0&!1&!2&!3] 48 [0&1&!2&!3] 130 [0&!1&2&!3]
+88 [0&1&2&!3] 131 [0&!1&!2&3] 9 [0&1&!2&3] 9 [0&!1&2&3] 9 [0&1&2&3]
+9 State: 132 [0&!1&!2&!3] 9 [0&1&!2&!3] 132 [0&!1&2&!3] 109 [0&1&2&!3]
+133 [0&!1&!2&3] 9 [0&1&!2&3] 132 [0&!1&2&3] 109 [0&1&2&3] 133 State: 133
+[0&!1&!2&!3] 9 [0&1&!2&!3] 132 [0&!1&2&!3] 109 [0&1&2&!3] 133 [0&!1&!2&3]
+9 [0&1&!2&3] 9 [0&!1&2&3] 109 [0&1&2&3] 9 State: 134 [0&!1&!2&!3] 7
+[0&1&!2&!3] 7 [0&!1&2&!3] 7 [0&1&2&!3] 7 [0&!1&!2&3] 7 [0&1&!2&3] 135
+[0&!1&2&3] 25 [0&1&2&3] 136 State: 135 [0&!1&!2&!3] 7 [0&1&!2&!3] 135
+[0&!1&2&!3] 134 [0&1&2&!3] 136 [0&!1&!2&3] 7 [0&1&!2&3] 135 [0&!1&2&3]
+134 [0&1&2&3] 136 State: 136 [0&!1&!2&!3] 7 [0&1&!2&!3] 135 [0&!1&2&!3]
+134 [0&1&2&!3] 136 [0&!1&!2&3] 7 [0&1&!2&3] 7 [0&!1&2&3] 134 [0&1&2&3]
+7 --END--
+FOO
+EOF
+
+chmod +x fake
+
+ltlcross -f 1 "./fake %f >%O" --verbose --csv=out.csv && exit 1
+test 2 = `grep '"ok"' out.csv | wc -l`
diff --git a/tests/core/sccif.test b/tests/core/sccif.test
index 2ee7f314c..2f3441f66 100755
--- a/tests/core/sccif.test
+++ b/tests/core/sccif.test
@@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -79,7 +79,7 @@ SCC#1
succs: 0
SCC#2
states: 2
- edges: 2->2
+ edges:
succs: 0 1
EOF