diff --git a/NEWS b/NEWS index d18039eb1..18caa0615 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index f93804c56..edca1167e 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -56,6 +56,7 @@ #include #include #include +#include #include #include #include @@ -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) - os << nonacc_scc << ',' - << terminal_scc << ',' - << weak_scc << ',' - << strong_scc << ','; + { + if (alternating) + os << ",,,,"; + else + os << nonacc_scc << ',' + << terminal_scc << ',' + << weak_scc << ',' + << strong_scc << ','; + } os << nondetstates << ',' << nondeterministic << ','; if (opt_strength) - os << terminal_aut << ',' - << weak_aut << ',' - << strong_aut << ','; + { + if (alternating) + os << ",,,"; + else + os << terminal_aut << ',' + << weak_aut << ',' + << strong_aut << ','; + } if (opt_ambiguous) - os << 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& 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& x, + std::vector& 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& from, std::vector& to, unsigned i, char prefix) @@ -1157,7 +1211,7 @@ namespace } } - bool print_first = verbose; + print_first = verbose; auto tmp = [&](std::vector& x, unsigned i, const char* prefix, const char* suffix) { diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 14bca24c8..fd282244c 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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 diff --git a/tests/Makefile.am b/tests/Makefile.am index 4248f5773..f94d44f74 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test new file mode 100755 index 000000000..348d67381 --- /dev/null +++ b/tests/core/ltl3ba.test @@ -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 . + +# 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' ((((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'