From 4d82ca70559ac0adab07e2652bf31f034cae6f7f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Aug 2014 17:37:58 +0200 Subject: [PATCH 1/6] * src/tgbaalgos/hoaf.hh: Typos in comments. --- src/tgbaalgos/hoaf.hh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tgbaalgos/hoaf.hh b/src/tgbaalgos/hoaf.hh index 4fe83cbc2..84da433bc 100644 --- a/src/tgbaalgos/hoaf.hh +++ b/src/tgbaalgos/hoaf.hh @@ -44,10 +44,10 @@ namespace spot /// \param g The automaton to output. /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. - /// \parama acceptance Force the type of acceptance mode used + /// \param a acceptance Force the type of acceptance mode used /// in output. /// \param alias Whether aliases should be used in output. - /// \param newslines Whether to use newlines in output. + /// \param newlines Whether to use newlines in output. SPOT_API std::ostream& hoaf_reachable(std::ostream& os, const tgba* g, From 261b073ae7dd531b6f9672749c6415ebf24925dd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 31 Aug 2014 17:01:49 +0200 Subject: [PATCH 2/6] * doc/org/ltlcross.org: Typos. --- doc/org/ltlcross.org | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) From 49a0997866eb77f77ca02f3b5f5da038e77fef40 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 31 Aug 2014 17:50:46 +0200 Subject: [PATCH 3/6] ltlcross: add --verbose option * src/bin/ltlcross.cc: Implement it. * NEWS: Mention it. --- NEWS | 4 +- src/bin/ltlcross.cc | 104 ++++++++++++++++++++++++++++++++++---------- 2 files changed, 84 insertions(+), 24 deletions(-) diff --git a/NEWS b/NEWS index 993c118e1..398ab6366 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 1.2.5a (not yet released) - Nothing yet. + * New features: + + - ltlcross --verbose is a new option to see what is being done New in spot 1.2.5 (2014-08-21) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index be5f577fc..a79f276dd 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -95,6 +95,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[] = { @@ -162,6 +163,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 } }; @@ -211,6 +214,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 { @@ -571,6 +575,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; } @@ -985,22 +992,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; @@ -1013,6 +1022,8 @@ namespace st->in_scc = m.scc_count(); } // convert it into TGBA for further processing + if (verbose) + std::cerr << "info: converting " << type << " to TGBA\n"; res = dstar_to_tgba(aut); delete aut; } @@ -1034,6 +1045,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; @@ -1078,6 +1091,20 @@ namespace spot::emptiness_check* ec = spot::couvreur99(prod); spot::emptiness_check_result* res = ec->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(); @@ -1120,6 +1147,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; @@ -1468,6 +1509,10 @@ namespace { // build a random state-space. spot::srand(seed); + if (verbose) + std::cerr << "info: building state-space #" << p << '/' << products + << " with seed " << seed << '\n'; + spot::tgba* statespace = spot::random_graph(states, density, ap, &dict); @@ -1525,20 +1570,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(); + } } } @@ -1581,6 +1633,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)) @@ -1619,6 +1674,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)) From 9a8becb8d89014718fb94afaf1c1f8df3b55c7c4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 31 Aug 2014 18:12:28 +0200 Subject: [PATCH 4/6] ltlcross: fix missing check for complement of negative automata * src/bin/ltlcross.cc: Fix it. * src/tgbatest/ltl2dstar.test: Test it. * NEWS: Mention it. --- NEWS | 9 +++++++++ src/bin/ltlcross.cc | 2 +- src/tgbatest/ltl2dstar.test | 16 +++++++++++++++- 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 398ab6366..12456d143 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,15 @@ New in spot 1.2.5a (not yet released) - 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. + New in spot 1.2.5 (2014-08-21) * New features: diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index a79f276dd..8fb70d3e5 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1473,7 +1473,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); 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 From d401fadc65163f6cbb40908d790d72c695b35ab4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 31 Aug 2014 19:07:53 +0200 Subject: [PATCH 5/6] neverparse: diagnose redefinition of state labels Reported by Joachim Klein. * src/neverparse/neverclaimparse.yy: Store labels and the location of their first definition in a global map to catch redefinitions. * src/tgbatest/neverclaimread.test: Test it. * NEWS: Mention it. --- NEWS | 2 + src/neverparse/neverclaimparse.yy | 19 +++++-- src/tgbatest/neverclaimread.test | 83 ++++++++++++++++++++++++++++++- 3 files changed, 99 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 12456d143..d824666c4 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,8 @@ New in spot 1.2.5a (not yet released) 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. New in spot 1.2.5 (2014-08-21) diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 6e915b600..db601a853 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -59,6 +59,7 @@ using namespace spot::ltl; static bool accept_all_needed = false; static bool accept_all_seen = false; +static std::map labels; } %token NEVER "never" @@ -77,7 +78,7 @@ static bool accept_all_seen = false; %type formula opt_dest %type

transition src_dest %type transitions transition_block -%type ident_list +%type one_ident ident_list %destructor { delete $$; } @@ -108,12 +109,21 @@ states: | states ';' state | states ';' -ident_list: - IDENT ':' +one_ident: IDENT ':' { + 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 { result->add_state_alias(*$2, *$1); // Keep any identifier that starts with accept. @@ -294,6 +304,7 @@ namespace spot } accept_all_needed = false; accept_all_seen = false; + labels.clear(); return result; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 06d0b3c7c..ab8db0332 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< Date: Sat, 6 Sep 2014 11:15:45 +0200 Subject: [PATCH 6/6] hoaf: rename I(i) as Inf(i). We just changed the format specification today. * src/tgbaalgos/hoaf.cc: Here. * NEWS: mention it. --- NEWS | 2 ++ src/tgbaalgos/hoaf.cc | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index d824666c4..453650ec5 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,8 @@ New in spot 1.2.5a (not yet released) 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) diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc index 80eb8f3fe..152d5e506 100644 --- a/src/tgbaalgos/hoaf.cc +++ b/src/tgbaalgos/hoaf.cc @@ -278,9 +278,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