diff --git a/NEWS b/NEWS index 6c2724751..d55e19aa3 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 1.2.5a (not yet released) +New in spot 1.99a (not yet released) * Major changes (including backward incompatible changes): @@ -87,6 +87,25 @@ New in spot 1.2.5a (not yet released) automata (when viewed explictely), using the above and non longuer supported tgba_bdd_concrete class. +New in spot 1.2.5a (not yet released) + + * New features: + + - ltlcross --verbose is a new option to see what is being done + + * Bug fixes: + + - When the automaton resulting from the translation of a positive + formula is deterministic, ltlcross will compute its complement + to perform additional checks against other translations of the + positive formula. The same procedure should be performed with + automata obtained from negated formulas, but because of a typo + this was not the case. + - the neverclaim parser will now diagnose redefinitions of + state labels. + - the acceptance specification in the HOA format output have been + adjusted to match recent changes in the format specifications. + New in spot 1.2.5 (2014-08-21) * New features: diff --git a/configure.ac b/configure.ac index 66ae8a1e2..725428436 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [1.2.5a], [spot@lrde.epita.fr]) +AC_INIT([spot], [1.99a], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index aff718f97..8c626e2e1 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -136,11 +136,11 @@ tools: - '=ltl2tgba --lbtt %s >%T=' (smaller output, TGBA) - '=ltl2tgba --lbtt -D %s >%T=' (more deterministic output, TGBA) - '=lbt <%L >%T=' - - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L %D=' + - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D=' (deterministic Rabin output) - - '=ltl2dstar --automata=streett --ltl2nba=spin:path/tp/ltl2tgba@-sD + - '=ltl2dstar --automata=streett --ltl2nba=spin:path/to/ltl2tgba@-sD %L %D=' (deterministic Streett output) - - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L - | dstar2tgba + - '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba -s >%N=' (external conversion from Rabin to Büchi done by =dstar2tgba= for more reduction of the Büchi automaton than what =ltlcross= would provide) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 695a0e094..873a78c4b 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -96,6 +96,7 @@ Exit status:\n\ #define OPT_NOCOMP 11 #define OPT_OMIT 12 #define OPT_BOGUS 13 +#define OPT_VERBOSE 14 static const argp_option options[] = { @@ -163,6 +164,8 @@ static const argp_option options[] = "'auto' (the default if --color is not used)", 0 }, { "save-bogus", OPT_BOGUS, "FILENAME", 0, "save formulas for which problems were detected in FILENAME", 0 }, + { "verbose", OPT_VERBOSE, 0, 0, + "print what is being done, for debugging", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -212,6 +215,7 @@ bool opt_omit = false; bool has_sr = false; // Has Streett or Rabin automata to process. const char* bogus_output_filename = 0; std::ofstream* bogus_output = 0; +bool verbose = false; struct translator_spec { @@ -572,6 +576,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STOP_ERR: stop_on_error = true; break; + case OPT_VERBOSE: + verbose = true; + break; default: return ARGP_ERR_UNKNOWN; } @@ -983,22 +990,24 @@ namespace } else { + const char* type = 0; + switch (aut->type) + { + case spot::Rabin: + type = "DRA"; + break; + case spot::Streett: + type = "DSA"; + break; + } + assert(type); + // Gather statistics about the input automaton if (want_stats) { statistics* st = &(*fstats)[translator_num]; st->has_in = true; - - switch (aut->type) - { - case spot::Rabin: - st->in_type = "DRA"; - break; - case spot::Streett: - st->in_type = "DSA"; - break; - } - + st->in_type = type; spot::tgba_sub_statistics s = sub_stats_reachable(aut->aut); st->in_states= s.states; @@ -1009,6 +1018,8 @@ namespace st->in_scc = spot::scc_info(aut->aut).scc_count(); } // convert it into TGBA for further processing + if (verbose) + std::cerr << "info: converting " << type << " to TGBA\n"; res = dstar_to_tgba(aut); } break; @@ -1029,6 +1040,8 @@ namespace // Compute statistics. if (res) { + if (verbose) + std::cerr << "info: getting statistics\n"; st->ok = true; spot::tgba_sub_statistics s = sub_stats_reachable(res); st->states = s.states; @@ -1072,6 +1085,21 @@ namespace { auto prod = spot::product(aut_i, aut_j); auto res = spot::couvreur99(prod)->check(); + + if (verbose) + { + std::cerr << "info: check_empty "; + if (icomp) + std::cerr << "Comp(N" << i << ')'; + else + std::cerr << 'P' << i; + if (jcomp) + std::cerr << "*Comp(P" << j << ')'; + else + std::cerr << "*N" << j; + std::cerr << '\n'; + } + if (res) { std::ostream& err = global_error(); @@ -1109,6 +1137,20 @@ namespace cross_check(const std::vector& maps, char l, unsigned p) { size_t m = maps.size(); + if (verbose) + { + std::cerr << "info: cross_check {"; + bool first = true; + for (size_t i = 0; i < m; ++i) + { + if (first) + first = false; + else + std::cerr << ','; + std::cerr << l << i; + } + std::cerr << "}, state-space #" << p << '/' << products << '\n'; + } std::vector res(m); unsigned verified = 0; @@ -1418,7 +1460,7 @@ namespace problems += check_empty_prod(pos[i], comp_pos[j], i, j, false, true); - if (i != j && comp_neg[i] && !comp_neg[i]) + if (i != j && comp_neg[i] && !comp_pos[i]) problems += check_empty_prod(comp_neg[i], neg[j], i, j, true, false); @@ -1454,6 +1496,11 @@ namespace { // build a random state-space. spot::srand(seed); + + if (verbose) + std::cerr << "info: building state-space #" << p << '/' << products + << " with seed " << seed << '\n'; + auto statespace = spot::random_graph(states, density, ap, dict); // Products of the state space with the positive automata. @@ -1510,20 +1557,27 @@ namespace // consistency check for (size_t i = 0; i < m; ++i) - if (pos_map[i] && neg_map[i] && - !(consistency_check(pos_map[i], neg_map[i], statespace))) + if (pos_map[i] && neg_map[i]) { - ++problems; + if (verbose) + std::cerr << "info: consistency_check (P" << i + << ",N" << i << "), state-space #" + << p << '/' << products << '\n'; + if (!(consistency_check(pos_map[i], neg_map[i], + statespace))) + { + ++problems; - std::ostream& err = global_error(); - err << "error: inconsistency between P" << i - << " and N" << i; - if (products > 1) - err << " for state-space #" << p - << '/' << products << '\n'; - else - err << '\n'; - end_error(); + std::ostream& err = global_error(); + err << "error: inconsistency between P" << i + << " and N" << i; + if (products > 1) + err << " for state-space #" << p + << '/' << products << '\n'; + else + err << '\n'; + end_error(); + } } } @@ -1549,6 +1603,9 @@ namespace static void print_stats_csv(const char* filename) { + if (verbose) + std::cerr << "info: writing CSV to " << filename << '\n'; + std::ofstream* outfile = 0; std::ostream* out; if (!strncmp(filename, "-", 2)) @@ -1587,6 +1644,9 @@ print_stats_csv(const char* filename) static void print_stats_json(const char* filename) { + if (verbose) + std::cerr << "info: writing JSON to " << filename << '\n'; + std::ofstream* outfile = 0; std::ostream* out; if (!strncmp(filename, "-", 2)) diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 2cffa71b5..3e777a91f 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -69,6 +69,7 @@ using namespace spot::ltl; static bool accept_all_needed = false; static bool accept_all_seen = false; +static std::map labels; } %token NEVER "never" @@ -88,7 +89,7 @@ static bool accept_all_seen = false; %type opt_dest formula_or_ident %type

transition src_dest %type transitions transition_block -%type ident_list +%type one_ident ident_list %destructor { delete $$; } @@ -118,13 +119,22 @@ states: | states ';' state | states ';' -ident_list: - IDENT ':' +one_ident: IDENT ':' { namer->new_state(*$1); + std::pair::const_iterator, bool> + res = labels.insert(std::make_pair(*$1, @1)); + if (!res.second) + { + error(@1, std::string("redefinition of ") + *$1 + "..."); + error(res.first->second, std::string("... ") + *$1 + " previously defined here"); + } $$ = $1; } - | ident_list IDENT ':' + + +ident_list: one_ident + | ident_list one_ident { namer->alias_state(namer->get_state(*$1), *$2); // Keep any identifier that starts with accept. @@ -319,6 +329,7 @@ namespace spot } accept_all_needed = false; accept_all_seen = false; + labels.clear(); delete namer; return result; diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc index 9417bbc83..0139cea29 100644 --- a/src/tgbaalgos/hoaf.cc +++ b/src/tgbaalgos/hoaf.cc @@ -276,9 +276,9 @@ namespace spot os << "Acceptance: " << num_acc; if (num_acc > 0) { - os << " I(0"; + os << " Inf(0"; for (unsigned i = 1; i < num_acc; ++i) - os << ")&I(" << i; + os << ")&Inf(" << i; os << ')'; } else diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test index 190bc149b..640c3fd23 100755 --- a/src/tgbatest/ltl2dstar.test +++ b/src/tgbatest/ltl2dstar.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013 Laboratoire de Recherche et +# Copyright (C) 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -61,3 +61,17 @@ grep '"in_type"' out.csv grep '"DSA"' out.csv grep '"DRA"' out.csv grep ',,,,' out.csv + + +# A bug in ltlcross <=1.2.5 caused it to not use the complement of the +# negative automaton. So running ltlcross with GFa would check one +# complement (the positive one), but running with FGa would ignore +# the negative complement. +$ltlcross -f 'GFa' --verbose \ +"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ +"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err +test `grep -c 'info: check_empty.*Comp' err` = 1 +$ltlcross -f 'FGa' --verbose \ +"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ +"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err +test `grep -c 'info: check_empty.*Comp' err` = 1 diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 22e8565b4..de5810c2d 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -169,7 +169,7 @@ run 2 ../ltl2tgba -XN input > stdout 2>stderr cat >expected <<\EOF input:9.16: syntax error, unexpected $undefined, expecting fi or ':' EOF -grep input: stderr >> stderrfilt +grep input: stderr > stderrfilt diff stderrfilt expected @@ -206,6 +206,87 @@ run 0 ../ltl2tgba -ks -XN input > output diff output expected +# Test duplicated labels. The following neverclaim was produced by +# ltl2ba 1.1 for '[](<>[]p1 U X[]<>Xp0)', but is rejected by Spin +# because of a duplicate label (accept_S10). We should +# complain as well. This was reported by Joachim Klein. + +cat >input <<\EOF +never { /* [](<>[]p1 U X[]<>Xp0) */ +T0_init: + if + :: (1) -> goto accept_S2 + :: (1) -> goto T1_S3 + :: (p1) -> goto T2_S4 + fi; +accept_S2: + if + :: (1) -> goto accept_S39 + :: (1) -> goto T1_S24 + :: (p1) -> goto accept_S10 + fi; +accept_S39: + if + :: (p0) -> goto accept_S39 + :: (1) -> goto T0_S39 + :: (1) -> goto T0_S24 + :: (p1) -> goto T0_S10 + fi; +T0_S39: + if + :: (p0) -> goto accept_S39 + :: (1) -> goto T0_S39 + :: (1) -> goto T0_S24 + :: (p1) -> goto T0_S10 + fi; +T0_S24: + if + :: (1) -> goto T0_S24 + :: (p1) -> goto T0_S10 + fi; +T0_S10: + if + :: (p0 && p1) -> goto accept_S10 + :: (p1) -> goto T0_S10 + fi; +accept_S10: + if + :: (p0 && p1) -> goto accept_S10 + :: (p1) -> goto T0_S10 + fi; +T1_S24: + if + :: (1) -> goto T1_S24 + :: (p1) -> goto accept_S10 + fi; +accept_S10: + if + :: (p1) -> goto accept_S10 + fi; +T1_S3: + if + :: (1) -> goto T1_S3 + :: (1) -> goto T1_S24 + :: (p1) -> goto T2_S4 + :: (p1) -> goto accept_S10 + fi; +T2_S4: + if + :: (p1) -> goto T2_S4 + :: (p1) -> goto accept_S10 + fi; +} +EOF + +run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr +cat stderr +cat >expected-err <<\EOF +input:48.1-10: redefinition of accept_S10... +input:38.1-10: ... accept_S10 previously defined here +EOF +grep input: stderr > stderrfilt +diff stderrfilt expected-err + cat >formulae<