From e7522056caff8de677497f9f5d0f2d7870568d94 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Jul 2013 18:55:45 +0200 Subject: [PATCH] ltlcross: give an example of accepted word for nonempty cross-products * src/tgbaalgos/word.cc, src/tgbaalgos/word.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltlcrossce.test: New file. * src/tgbatest/Makefile.am: Add it. * src/bin/ltlcross.cc: Compute and display an accepted word for nonempty cross-products. * NEWS, doc/org/ltlcross.org: Document it. --- NEWS | 4 ++ doc/org/ltlcross.org | 44 +++++++------- src/bin/ltlcross.cc | 58 +++++++++++++----- src/tgbaalgos/Makefile.am | 6 +- src/tgbaalgos/word.cc | 110 +++++++++++++++++++++++++++++++++++ src/tgbaalgos/word.hh | 43 ++++++++++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/ltlcrossce.test | 95 ++++++++++++++++++++++++++++++ 8 files changed, 324 insertions(+), 37 deletions(-) create mode 100644 src/tgbaalgos/word.cc create mode 100644 src/tgbaalgos/word.hh create mode 100755 src/tgbatest/ltlcrossce.test diff --git a/NEWS b/NEWS index fa154b72c..17619300b 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 05ba2e0ea..af2ef4aa2 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 7c349a658..827f81d87 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 dcbc871c7..e24f4dfb6 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 000000000..1b8d9e3b4 --- /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 000000000..af3f5f51e --- /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 00cc920a3..073467851 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 000000000..81f1aa1a7 --- /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 + -- GitLab