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.
This commit is contained in:
Alexandre Duret-Lutz
parent
4bafa4e1b0
commit
e7522056ca
8 changed files with 324 additions and 37 deletions
4
NEWS
4
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.
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
110
src/tgbaalgos/word.cc
Normal file
110
src/tgbaalgos/word.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
43
src/tgbaalgos/word.hh
Normal file
43
src/tgbaalgos/word.hh
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#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<bdd> seq_t;
|
||||
seq_t prefix;
|
||||
seq_t cycle;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBAALGOS_WORD_HH
|
||||
|
|
@ -108,6 +108,7 @@ TESTS = \
|
|||
emptchk.test \
|
||||
emptchke.test \
|
||||
dfs.test \
|
||||
ltlcrossce.test \
|
||||
emptchkr.test \
|
||||
ltlcounter.test \
|
||||
basimul.test \
|
||||
|
|
|
|||
95
src/tgbatest/ltlcrossce.test
Executable file
95
src/tgbatest/ltlcrossce.test
Executable file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue