alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: add support for alternating automata

Browse source 
* bin/ltlcross.cc: Add an alternation-removal pass, and
adjust CSV output.
* doc/org/ltlcross.org: Update.
* tests/core/ltl3dra.test, tests/core/ltl3ba.test: Add more tests.
* tests/Makefile.am: Add tests/core/ltl3ba.test.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-23 15:27:39 +01:00
parent 543e0db9a0
commit 87c9d6f039
6 changed files with 205 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -1,5 +1,10 @@
New in spot 2.2.2.dev (Not yet released)
Tools:
* ltlcross supports translators that output weak alternating
automata in the HOA format (not necessarily *very* weak).
Library:
* A twa is required to have at least one state, the initial state.

86
bin/ltlcross.cc
View file

@ -56,6 +56,7 @@
#include <spot/twaalgos/word.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/misc/formater.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/isdet.hh>
@ -146,9 +147,10 @@ static const argp_option options[] =
"store automata (in the HOA format) into the CSV or JSON output", 0 },
{ "strength", OPT_STRENGTH, nullptr, 0,
"output statistics about SCC strengths (non-accepting, terminal, weak, "
"strong)", 0 },
"strong) [not supported for alternating automata]", 0 },
{ "ambiguous", OPT_AMBIGUOUS, nullptr, 0,
"output statistics about ambiguous automata", 0 },
"output statistics about ambiguous automata "
"[not supported for alternating automata]", 0 },
{ "unambiguous", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -2 },
@ -257,6 +259,7 @@ struct statistics
{
statistics()
: ok(false),
alternating(false),
status_str(nullptr),
status_code(0),
time(0),
@ -280,6 +283,7 @@ struct statistics
// If OK is false, only the status_str, status_code, and time fields
// should be valid.
bool ok;
bool alternating;
const char* status_str;
int status_code;
double time;
@ -351,18 +355,33 @@ struct statistics
<< acc << ','
<< scc << ',';
if (opt_strength)
{
if (alternating)
os << ",,,,";
else
os << nonacc_scc << ','
<< terminal_scc << ','
<< weak_scc << ','
<< strong_scc << ',';
}
os << nondetstates << ','
<< nondeterministic << ',';
if (opt_strength)
{
if (alternating)
os << ",,,";
else
os << terminal_aut << ','
<< weak_aut << ','
<< strong_aut << ',';
}
if (opt_ambiguous)
{
if (alternating)
os << ',';
else
os << ambiguous << ',';
}
os << complete;
if (!products_avg)
{
@ -627,6 +646,7 @@ namespace
if (verbose)
std::cerr << "info: getting statistics\n";
st->ok = true;
st->alternating = res->is_alternating();
spot::twa_sub_statistics s = sub_stats_reachable(res);
st->states = s.states;
st->edges = s.edges;
@ -637,7 +657,7 @@ namespace
st->scc = c;
st->nondetstates = spot::count_nondet_states(res);
st->nondeterministic = st->nondetstates != 0;
if (opt_strength)
if (opt_strength && !st->alternating)
{
m.determine_unknown_acceptance();
for (unsigned n = 0; n < c; ++n)
@ -658,7 +678,7 @@ namespace
else
st->terminal_aut = true;
}
if (opt_ambiguous)
if (opt_ambiguous && !st->alternating)
st->ambiguous = !spot::is_unambiguous(res);
st->complete = spot::is_complete(res);
@ -1037,11 +1057,6 @@ namespace
bool prob;
pos[n] = runner.translate(n, 'P', pstats, prob);
problems += prob;
// If the automaton is deterministic, compute its complement
// as well.
if (!no_complement && pos[n] && is_deterministic(pos[n]))
comp_pos[n] = dtwa_complement(pos[n]);
}
// ---------- Negative Formula ----------
@ -1073,11 +1088,6 @@ namespace
bool prob;
neg[n] = runner.translate(n, 'N', nstats, prob);
problems += prob;
// If the automaton is deterministic, compute its
// complement as well.
if (!no_complement && neg[n] && is_deterministic(neg[n]))
comp_neg[n] = dtwa_complement(neg[n]);
}
}
@ -1102,6 +1112,8 @@ namespace
std::cerr << "info: " << prefix << i << "\t(";
printsize(x[i]);
std::cerr << ')';
if (x[i]->is_alternating())
std::cerr << " univ-edges";
if (is_deterministic(x[i]))
std::cerr << " deterministic";
if (is_complete(x[i]))
@ -1120,9 +1132,51 @@ namespace
std::cerr << "Performing sanity checks and gathering statistics..."
<< std::endl;
bool print_first = verbose;
auto unalt = [&](std::vector<spot::twa_graph_ptr>& x,
unsigned i, char prefix)
{
if (!(x[i] && x[i]->is_alternating()))
return;
if (verbose)
{
if (print_first)
{
std::cerr <<
"info: getting rid of universal edges...\n";
print_first = false;
}
std::cerr << "info: " << prefix << i << "\t(";
printsize(x[i]);
std::cerr << ") ->";
}
x[i] = remove_alternation(x[i]);
if (verbose)
{
std::cerr << " (";
printsize(x[i]);
std::cerr << ")\n";
}
};
auto complement = [&](const std::vector<spot::twa_graph_ptr>& x,
std::vector<spot::twa_graph_ptr>& comp,
unsigned i)
{
if (!no_complement && x[i] && is_deterministic(x[i]))
comp[i] = dtwa_complement(x[i]);
};
for (unsigned i = 0; i < m; ++i)
{
unalt(pos, i, 'P');
complement(pos, comp_pos, i);
unalt(neg, i, 'N');
complement(neg, comp_neg, i);
}
if (determinize && !no_complement)
{
bool print_first = verbose;
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& from,
std::vector<spot::twa_graph_ptr>& to, unsigned i,
char prefix)
@ -1157,7 +1211,7 @@ namespace
}
}
bool print_first = verbose;
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char* prefix, const char* suffix)
{

86
doc/org/ltlcross.org
View file

@ -9,19 +9,22 @@ translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Softw
/LTL-to-Büchi Translator Testbench/, that essentially performs the
same sanity checks.
The main differences are:
- support for PSL formulas in addition to LTL
- more statistics, especially:
The main differences with LBTT are:
- *support for PSL formulas in addition to LTL*
- support for (non-alternating) automata with *any type of acceptance condition*,
- support for *weak alternating automata*,
- additional intersection *checks with the complement*, allowing
to check equivalence of automata more precisely,
- *more statistics*, especially:
- the number of logical transitions represented by each physical edge,
- the number of deterministic states and automata
- the number of SCCs with their various strengths (nonaccepting, terminal, weak, strong)
- the number of terminal, weak, and strong automata
- statistics output in a format that can be more easily be post-processed,
- more precise time measurement (LBTT was only precise to
1/100 of a second, reporting most times as "0.00s"),
- support for any type of acceptance condition,
- additional intersection checks with the complement, allowing
to check equivalence of automata more precisely.
- an option to *reduce counterexample* by attempting to mutate and
shorten troublesome formulas,
- statistics output in *CSV* for easier post-processing,
- *more precise time measurement* (LBTT was only precise to
1/100 of a second, reporting most times as "0.00s").
Although =ltlcross= performs the same sanity checks as LBTT, it does
not implement any of the interactive features of LBTT. In our almost
@ -120,6 +123,7 @@ be rewritten using the other supported operators.
--lbtt=.
- Non-alternating automata in [[file:http://adl.github.io/hoaf/][the HOA format]] with any acceptance
condition.
- [[file:concepts.org::#property-flags][Weak]] alternating automata in [[file:http://adl.github.io/hoaf/][the HOA format]].
- [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dstar='s format]], which supports deterministic Rabin or Streett
automata.
@ -496,7 +500,9 @@ This classification is used to fill the =terminal_aut=, =weak_aut=,
=--strength= is passed). Only one of these should contain =1=. We
usually prefer terminal automata over weak automata, and weak automata
over strong automata, because the emptiness check of terminal (and
weak) automata is easier.
weak) automata is easier. When working with alternating automata, all
those strength-related columns will be empty, because the routines
used to compute those statistic do not yet support universal edges.
=nondetstates= counts the number of non-deterministic states in the
automaton. =nondeterministic= is a Boolean value indicating if the
@ -509,7 +515,8 @@ assignment $ab$) and is therefore not deterministic.
If option =--aumbiguous= was passed to =ltlcross=, the column
=ambiguous_aut= holds a Boolean indicating whether the automaton is
ambiguous, i.e., if there exists a word that can be accepted by at
least two different runs.
least two different runs. (This information is not yet available for
alternating automata.)
=complete_aut= is a Boolean indicating whether the automaton is
complete.
@ -962,30 +969,40 @@ The verbose option can be useful to troubleshoot problems or simply
follow the list of transformations and tests performed by =ltlcross=.
For instance here is what happens if we try to cross check =ltl2tgba=
and =ltl3ba= on the formula =FGa=.
and =ltl3ba -H1= on the formula =FGa=. Note that =ltl2tgba= will
produce transition-based generalized Büchi automata, while =ltl3ba
-H1= produces co-Büchi alternating automata.
#+BEGIN_SRC sh :results verbatim :exports code
ltlcross -f 'FGa' ltl2tgba ltl3ba --determinize --verbose
ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --determinize --verbose
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports results
ltlcross -f 'FGa' ltl2tgba ltl3ba --determinize --verbose 2>&1
ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --determinize --verbose 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
F(G(a))
Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-vfVUzt'
Running [P1]: ltl3ba -f '<>([](a))'>'lcr-o1-IiXGfZ'
Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-T02eWu'
Running [N1]: ltl3ba -f '!(<>([](a)))'>'lcr-o1-0DpXF0'
Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-Ak0bYx'
Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-5U1MyT'
Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-sX2kaf'
Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-4siKPA'
info: collected automata:
info: P0 (2 st.,3 ed.,1 sets)
info: N0 (1 st.,2 ed.,1 sets) deterministic complete
info: P1 (2 st.,3 ed.,1 sets)
info: N1 (3 st.,5 ed.,1 sets) univ-edges deterministic complete
Performing sanity checks and gathering statistics...
info: getting rid of universal edges...
info: N1 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets)
info: complementing non-deterministic automata via determinization...
info: P0 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P0)
info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,4 ed.,2 sets) Comp(P1)
info: getting rid of any Fin acceptance...
info: Comp(P0) (2 st.,4 ed.,2 sets) -> (3 st.,7 ed.,2 sets)
info: Comp(N0) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: Comp(P1) (2 st.,4 ed.,2 sets) -> (4 st.,9 ed.,2 sets)
info: Comp(N1) (2 st.,4 ed.,1 sets) -> (3 st.,6 ed.,1 sets)
info: check_empty P0*N0
@ -999,10 +1016,19 @@ No problem detected.
#+end_example
First =FGa= and its negations =!FGa= are translated with the two
tools, resulting in four automata: to positive automata =P0= and =P1=
tools, resulting in four automata: two positive automata =P0= and =P1=
for =FGa=, and two negative automata =N0= and =N1=.
=ltlcross= then proceeds to compute the complement of these four
Some basic information about the collected automata are displayed.
For instance we can see that although =ltl3ba -H1= outputs co-Büchi
alternating automata, only automaton =N1= uses universal edges: the
automaton =P1= can be used like a non-alternating co-Büchi automaton.
=ltlcross= then proceeds to transform alternating automata (only weak
alternating automata are supported) into non-alternating automata.
Here only =N1= needs this transformation.
Then =ltlcross= computes the complement of these four
automata. Since =P0= and =P1= are nondeterministic and the
=--determinize= option was given, a first pass determinize and
complete these two automata, creating =Comp(P0)= and =Comp(P1)=.
@ -1030,23 +1056,31 @@ Note that if we had not used the =--determinize= option, the procedure
would look slightly more complex:
#+BEGIN_SRC sh :results verbatim :exports code
ltlcross -f 'FGa' ltl2tgba ltl3ba --verbose
ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --verbose
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports results
ltlcross -f 'FGa' ltl2tgba ltl3ba --verbose 2>&1
ltlcross -f 'FGa' ltl2tgba 'ltl3ba -H1' --verbose 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
F(G(a))
Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-YvMdzU'
Running [P1]: ltl3ba -f '<>([](a))'>'lcr-o1-Ixj7RI'
Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-uBbTbx'
Running [N1]: ltl3ba -f '!(<>([](a)))'>'lcr-o1-eo0fzl'
Running [P0]: ltl2tgba -H 'F(G(a))'>'lcr-o0-jD32mW'
Running [P1]: ltl3ba -H1 -f '<>([](a))'>'lcr-o1-w6IJYI'
Running [N0]: ltl2tgba -H '!(F(G(a)))'>'lcr-o0-dac1Av'
Running [N1]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o1-OZL7fi'
info: collected automata:
info: P0 (2 st.,3 ed.,1 sets)
info: N0 (1 st.,2 ed.,1 sets) deterministic complete
info: P1 (2 st.,3 ed.,1 sets)
info: N1 (3 st.,5 ed.,1 sets) univ-edges deterministic complete
Performing sanity checks and gathering statistics...
info: getting rid of universal edges...
info: N1 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets)
info: getting rid of any Fin acceptance...
info: Comp(N0) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: P1 (2 st.,3 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: Comp(N1) (2 st.,4 ed.,1 sets) -> (3 st.,6 ed.,1 sets)
info: check_empty P0*N0
info: check_empty P0*N1

1
tests/Makefile.am
View file

@ -256,6 +256,7 @@ TESTS_twa = \
core/dra2dba.test \
core/unambig.test \
core/ltlcross4.test \
core/ltl3ba.test \
core/streett.test \
core/ltl3dra.test \
core/ltl2dstar.test \

42
tests/core/ltl3ba.test Executable file
View file

@ -0,0 +1,42 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 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/>.
# Do some quick translations to make sure the neverclaims produced by
# spot actually look correct! We do that by parsing them via ltlcross.
# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed.
. ./defs
set -e
# Skip this test if ltl3dra is not installed.
(ltl3ba -v) || exit 77
# The -H1 option will output alternating automata, so this tests
# ltlcross's support in this area.
randltl -n 30 2 |
ltlcross 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' \
--ambiguous --strength --csv=output.csv
# Make sure all lines in output.csv have the same number of comas
sed 's/[^,]//g' <output.csv |
( read first
while read l; do
test "x$first" = "x$l" || exit 1
done)

20
tests/core/ltl3dra.test
View file

@ -29,7 +29,7 @@ set -e
(ltl3dra -v) || exit 77
# This used to crash ltlcross because the number of
# acceptance sets generated was to high.
# acceptance sets generated was too high.
ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) &&
(!(<>(p2)))) || ((!(p0)) && (<>(p2)))) U ((<>(((p0) && (!([](((!(p1))
&& ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1))
@ -41,3 +41,21 @@ ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) &&
# relabeled p0&p1, and then p0 was unregistered despite being one of
# the new variables.
ltldo ltl3dra -f '"a=0" & p0' | grep 'AP: 2.*p0'
# ltl3dra 0.2.2 has a bug were 'ltl3dra -H1 -f true' produce an
# empty automaton. ltl3dra 0.2.3 fixes that but introduces another
# bug where 'ltl3dra -f "!(a <-> Fb)" rejects cycle{!a & b}.
#
# # The -H1 option will output alternating automata, so this tests
# # ltlcross's support in this area.
# randltl -n 30 2 |
# ltlcross 'ltl3dra -H1' 'ltl3dra -H2' 'ltl3dra -H3' \
# --ignore-execution-failures --ambiguous \
# --strength --csv=output.csv
#
# # Make sure all lines in output.csv have the same number of comas
# sed 's/[^,]//g' <output.csv |
# ( read first
# while read l; do
# test "x$first" = "x$l" || exit 1
# done)