diff --git a/NEWS b/NEWS
index fa154b72c61911629e0d4066ed60c771fd803308..17619300b16255a8c20c78435f90991617bb26d8 100644
--- a/NEWS
+++ b/NEWS
@@ -6,6 +6,10 @@ New in spot 1.1.4a (not relased)
* ltlcross has a new option --color to color its output. It is enabled
by default when the output is a terminal.
+ * ltlcross will give an example of infinite word accepted by the
+ two automata when the product between a positive automaton and
+ a negative automaton is non-empty.
+
* Environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
temporary files are created and if they should be erased. Read
the man page of ltlcross for detail.
diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org
index 05ba2e0ea694d38095261d2788bdd1dd7dcbc897..af2ef4aa2b9e84457ea0012cb7677eba68d8fb45 100644
--- a/doc/org/ltlcross.org
+++ b/doc/org/ltlcross.org
@@ -396,28 +396,32 @@ positive and negative formulas by the ith translator).
A single failing translator might generate a lot of lines of
the form:
- : error: P0*N1 is nonempty
- : error: P1*N0 is nonempty
- : error: P1*N1 is nonempty
- : error: P1*N2 is nonempty
- : error: P1*N3 is nonempty
- : error: P1*N4 is nonempty
- : error: P1*N5 is nonempty
- : error: P1*N6 is nonempty
- : error: P1*N7 is nonempty
- : error: P1*N8 is nonempty
- : error: P1*N9 is nonempty
- : error: P2*N1 is nonempty
- : error: P3*N1 is nonempty
- : error: P4*N1 is nonempty
- : error: P5*N1 is nonempty
- : error: P6*N1 is nonempty
- : error: P7*N1 is nonempty
- : error: P8*N1 is nonempty
- : error: P9*N1 is nonempty
+ : error: P0*N1 is nonempty; both automata accept the infinite word
+ : cycle{p0 & !p1}
+ : error: P1*N0 is nonempty; both automata accept the infinite word
+ : p0; !p1; cycle{p0 & p1}
+ : error: P1*N1 is nonempty; both automata accept the infinite word
+ : p0; cycle{!p1 & !p0}
+ : error: P1*N2 is nonempty; both automata accept the infinite word
+ : p0; !p1; cycle{p0 & p1}
+ : error: P1*N3 is nonempty; both automata accept the infinite word
+ : p0; !p1; cycle{p0 & p1}
+ : error: P1*N4 is nonempty; both automata accept the infinite word
+ : p0; cycle{!p1 & !p0}
+ : error: P2*N1 is nonempty; both automata accept the infinite word
+ : p0; !p1; !p0; cycle{!p1 & !p0; p0 & !p1; !p1; !p1; p0 & !p1}
+ : error: P3*N1 is nonempty; both automata accept the infinite word
+ : p0; !p1; !p1 & !p0; cycle{p0 & !p1}
+ : error: P4*N1 is nonempty; both automata accept the infinite word
+ : p0; !p1; !p1 & !p0; cycle{p0 & !p1}
In this example, translator number =1= looks clearly faulty
- (at least the other 9 translators do not contradict each other).
+ (at least the other 4 translators do not contradict each other).
+
+ Examples of infinite words that are accepted by both automata
+ always have the form of a lasso: a (possibly empty) finite prefix
+ followed by a cycle that should be repeated infinitely often.
+ The cycle part is denoted by =cycle{...}=.
- Cross-comparison checks: for some state-space $S$,
all $P_i\otimes S$ are either all empty, or all non-empty.
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 7c349a6583dcd8eef57f776177ba45e3005136f3..827f81d87e16c63c477482a4402b80581b664284 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -50,6 +50,8 @@
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/isweakscc.hh"
+#include "tgbaalgos/reducerun.hh"
+#include "tgbaalgos/word.hh"
#include "misc/formater.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
@@ -175,6 +177,7 @@ ARGMATCH_VERIFY(color_args, color_types);
color_type color_opt = color_if_tty;
const char* bright_red = "\033[01;31m";
const char* bright_white = "\033[01;37m";
+const char* bright_yellow = "\033[01;33m";
const char* reset_color = "\033[m";
unsigned states = 200;
@@ -201,6 +204,15 @@ global_error()
return std::cerr;
}
+static std::ostream&
+example()
+{
+ if (color_opt)
+ std::cerr << bright_yellow;
+ return std::cerr;
+}
+
+
static void
end_error()
{
@@ -796,14 +808,40 @@ namespace
}
};
- static bool
- is_empty(const spot::tgba* aut)
+ static void
+ check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j,
+ size_t i, size_t j)
{
- spot::emptiness_check* ec = spot::couvreur99(aut);
+ spot::tgba_product* prod = new spot::tgba_product(aut_i, aut_j);
+ spot::emptiness_check* ec = spot::couvreur99(prod);
spot::emptiness_check_result* res = ec->check();
+
+ if (res)
+ {
+ global_error() << "error: P" << i << "*N" << j
+ << " is nonempty";
+
+ spot::tgba_run* run = res->accepting_run();
+ if (run)
+ {
+ const spot::tgba_run* runmin = reduce_run(prod, run);
+ delete run;
+ std::cerr << "; both automata accept the infinite word\n"
+ << " ";
+ spot::tgba_word w(runmin);
+ w.simplify();
+ w.print(example(), prod->get_dict()) << "\n";
+ delete runmin;
+ }
+ else
+ {
+ std::cerr << "\n";
+ }
+ end_error();
+ }
delete res;
delete ec;
- return !res;
+ delete prod;
}
static void
@@ -1038,17 +1076,7 @@ namespace
if (pos[i])
for (size_t j = 0; j < m; ++j)
if (neg[j])
- {
- spot::tgba_product* prod =
- new spot::tgba_product(pos[i], neg[j]);
- if (!is_empty(prod))
- {
- global_error() << "error: P" << i << "*N" << j
- << " is nonempty\n";
- end_error();
- }
- delete prod;
- }
+ check_empty_prod(pos[i], neg[j], i, j);
}
else
{
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index dcbc871c77b4b24d90b73b4192def5d8a7f7aaba..e24f4dfb66d4e7894f23b8edd0b8161d96afe919 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -68,7 +68,8 @@ tgbaalgos_HEADERS = \
tau03.hh \
tau03opt.hh \
translate.hh \
- reductgba_sim.hh
+ reductgba_sim.hh \
+ word.hh
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
@@ -114,6 +115,7 @@ libtgbaalgos_la_SOURCES = \
translate.cc \
reductgba_sim.cc \
weight.cc \
- weight.hh
+ weight.hh \
+ word.cc
libtgbaalgos_la_LIBADD = gtec/libgtec.la
diff --git a/src/tgbaalgos/word.cc b/src/tgbaalgos/word.cc
new file mode 100644
index 0000000000000000000000000000000000000000..1b8d9e3b4c21fb9397b42aa12d367de167482ecd
--- /dev/null
+++ b/src/tgbaalgos/word.cc
@@ -0,0 +1,110 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 .
+
+#include "word.hh"
+#include "tgba/bddprint.hh"
+#include "tgba/bdddict.hh"
+
+namespace spot
+{
+ tgba_word::tgba_word(const tgba_run* run)
+ {
+ for (tgba_run::steps::const_iterator i = run->prefix.begin();
+ i != run->prefix.end(); ++i)
+ prefix.push_back(i->label);
+ for (tgba_run::steps::const_iterator i = run->cycle.begin();
+ i != run->cycle.end(); ++i)
+ cycle.push_back(i->label);
+ }
+
+ void
+ tgba_word::simplify()
+ {
+ // If all the formulas on the cycle are compatible, reduce the
+ // cycle to a simple conjunction.
+ //
+ // For instance
+ // !a|!b; b; a&b; cycle{a; b; a&b}
+ // can be reduced to
+ // !a|!b; b; a&b; cycle{a&b}
+ {
+ bdd all = bddtrue;
+ for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
+ all &= *i;
+ if (all != bddfalse)
+ {
+ cycle.clear();
+ cycle.push_back(all);
+ }
+ }
+ // If the last formula of the prefix is compatible with the
+ // last formula of the cycle, we can shift the cycle and
+ // reduce the prefix.
+ //
+ // For instance
+ // !a|!b; b; a&b; cycle{a&b}
+ // can be reduced to
+ // !a|!b; cycle{a&b}
+ while (!prefix.empty())
+ {
+ bdd a = prefix.back() & cycle.back();
+ if (a == bddfalse)
+ break;
+ prefix.pop_back();
+ cycle.pop_back();
+ cycle.push_front(a);
+ }
+ // Get rid of any disjunction.
+ //
+ // For instance
+ // !a|!b; cycle{a&b}
+ // can be reduced to
+ // !a&!b; cycle{a&b}
+ for (seq_t::iterator i = prefix.begin(); i != prefix.end(); ++i)
+ *i = bdd_satone(*i);
+ for (seq_t::iterator i = cycle.begin(); i != cycle.end(); ++i)
+ *i = bdd_satone(*i);
+
+ }
+
+ std::ostream&
+ tgba_word::print(std::ostream& os, bdd_dict* d) const
+ {
+ if (!prefix.empty())
+ for (seq_t::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
+ {
+ bdd_print_formula(os, d, *i);
+ os << "; ";
+ }
+ assert(!cycle.empty());
+ bool notfirst = false;
+ os << "cycle{";
+ for (seq_t::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
+ {
+ if (notfirst)
+ os << "; ";
+ notfirst = true;
+ bdd_print_formula(os, d, *i);
+ }
+ os << "}";
+ return os;
+ }
+
+
+}
diff --git a/src/tgbaalgos/word.hh b/src/tgbaalgos/word.hh
new file mode 100644
index 0000000000000000000000000000000000000000..af3f5f51e587664359dc963baf881e2b15940529
--- /dev/null
+++ b/src/tgbaalgos/word.hh
@@ -0,0 +1,43 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 .
+
+#ifndef SPOT_TGBAALGOS_WORD_HH
+# define SPOT_TGBAALGOS_WORD_HH
+
+# include "emptiness.hh"
+
+namespace spot
+{
+ class bdd_dict;
+
+ /// \brief An infinite word stored as a lasso.
+ struct SPOT_API tgba_word
+ {
+ tgba_word(const tgba_run* run);
+ void simplify();
+ std::ostream& print(std::ostream& os, bdd_dict* d) const;
+
+ typedef std::list seq_t;
+ seq_t prefix;
+ seq_t cycle;
+ };
+
+}
+
+#endif // SPOT_TGBAALGOS_WORD_HH
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 00cc920a398f6cd6d39801498100674b9667273c..07346785108569d359ec11d0a2ad940c803246de 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -108,6 +108,7 @@ TESTS = \
emptchk.test \
emptchke.test \
dfs.test \
+ ltlcrossce.test \
emptchkr.test \
ltlcounter.test \
basimul.test \
diff --git a/src/tgbatest/ltlcrossce.test b/src/tgbatest/ltlcrossce.test
new file mode 100755
index 0000000000000000000000000000000000000000..81f1aa1a73e635846d4e55de3eeb95c23f02e854
--- /dev/null
+++ b/src/tgbatest/ltlcrossce.test
@@ -0,0 +1,95 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013 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
+
+ltl2tgba=../../bin/ltl2tgba
+
+# The following "fake" script behaves as
+# version 1.5.9 of modella, when run as
+# 'modella -r12 -g -e %L %T' on
+# 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))'
+# or its negation. The translation is bogus
+# because the automata generated for this formula
+# and its negation both include the language of G(!p0).
+cat >fake <<\EOF
+#!/bin/sh
+case $1 in
+"| G & F p0 F G ! p1 & F G ! p0 G F p1")
+cat <<\END
+7 1 0 1 -1 1 t
+2 | & ! p0 ! p1 & ! p0 p1
+3 t
+4 | & ! p0 ! p1 & p0 ! p1
+-1 1 0 -1 1 t
+5 | & ! p0 ! p1 & ! p0 p1
+-1 2 0 -1 5 | & ! p0 ! p1 & ! p0 p1
+-1 3 0 1 -1 3 t
+-1 4 0 1 -1 4 | & ! p0 ! p1 & p0 ! p1
+-1 5 0 -1 5 & ! p0 ! p1
+6 & ! p0 p1
+-1 6 0 1 -1 2 | & ! p0 ! p1 & ! p0 p1
+-1
+END
+;;
+"! | G & F p0 F G ! p1 & F G ! p0 G F p1")
+cat <<\END
+12 1 0 1 -1 1 t
+2 | & ! p0 ! p1 & p0 ! p1
+3 t
+4 t
+5 | & ! p0 ! p1 & ! p0 p1
+6 & ! p0 ! p1
+-1 1 0 -1 1 t
+2 | & ! p0 ! p1 & p0 ! p1
+8 | & ! p0 ! p1 & ! p0 p1
+6 & ! p0 ! p1
+-1 2 0 -1 2 | & ! p0 ! p1 & p0 ! p1
+6 & ! p0 ! p1
+-1 3 0 -1 3 t
+7 t
+-1 4 0 -1 7 t
+-1 5 0 -1 8 | & ! p0 ! p1 & ! p0 p1
+6 & ! p0 ! p1
+-1 6 0 1 -1 6 & ! p0 ! p1
+-1 7 0 -1 7 | & ! p0 ! p1 & ! p0 p1
+9 | & p0 ! p1 & p0 p1
+-1 8 0 -1 10 | & ! p0 ! p1 & ! p0 p1
+6 & ! p0 ! p1
+-1 9 0 -1 11 t
+-1 10 0 -1 10 | & ! p0 ! p1 & ! p0 p1
+6 & ! p0 ! p1
+-1 11 0 1 -1 4 t
+-1
+END
+;;
+esac
+EOF
+chmod +x fake
+
+run 1 ../../bin/ltlcross -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \
+ "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
+cat errors
+grep 'error: P0\*N1 is nonempty' errors
+grep 'error: P1\*N0 is nonempty' errors
+grep 'error: P1\*N1 is nonempty' errors
+test `grep cycle errors | wc -l` = 3
+test `grep '^error:' errors | wc -l` = 4
+