diff --git a/NEWS b/NEWS index ead5684b7..f5af7bad2 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,8 @@ New in spot 1.0a (not released): transition counts, just as the ltlcross tool. - ltlcross will display the number of timeouts at the end of its execution. + - ltlcross will diagnose tools with missing input or + output %-sequence before attempting to run any of them. - The parser for LBT's prefix-style LTL formulas will now read atomic propositions that are not of the form p1, p2... This makes it possible to process formulas written in diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 58d5aba1d..c667729c4 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -494,10 +494,28 @@ namespace declare('N', &output); declare('T', &output); + std::vector has(256); size_t s = translators.size(); assert(s); for (size_t n = 0; n < s; ++n) - prime(translators[n]); + { + // Check that each translator uses at least one input and + // one output. + has.clear(); + scan(translators[n], has); + if (!(has['f'] || has['s'] || has['l'] || has['w'] + || has['F'] || has['S'] || has['L'] || has['W'])) + error(2, 0, "no input %%-sequence in '%s'.\n Use " + "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " + "to pass the formula.", translators[n]); + if (!(has['N'] || has['T'])) + error(2, 0, "no output %%-sequence in '%s'.\n Use " + "one of %%N,%%T to indicate where the automaton is saved.", + translators[n]); + + // Remember the %-sequences used by all translators. + prime(translators[n]); + } } @@ -526,7 +544,7 @@ namespace return string_ltl_wring; if (!string_ltl_lbt.val().empty()) return string_ltl_lbt; - error(2, 0, "None of the translators need the input formula?"); + assert(!"None of the translators need the input formula?"); return string_ltl_spot; } @@ -560,9 +578,7 @@ namespace format(command, translators[translator_num]); toclean.push_back(output.val()); - if (output.format == printable_result_filename::None) - error(2, 0, "no output sequence used in %s", - translators[translator_num]); + assert(output.format != printable_result_filename::None); std::string cmd = command.str(); std::cerr << "Running [" << l << translator_num << "]: " diff --git a/src/misc/formater.cc b/src/misc/formater.cc index 68acf2fb3..9851098c5 100644 --- a/src/misc/formater.cc +++ b/src/misc/formater.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,18 +23,24 @@ namespace spot { void - formater::prime(const char* fmt) + formater::scan(const char* fmt, std::vector& has) const { for (const char* pos = fmt; *pos; ++pos) if (*pos == '%') { char c = *++pos; - has_[c] = true; + has[c] = true; if (!c) break; } } + void + formater::prime(const char* fmt) + { + scan(fmt, has_); + } + std::ostream& formater::format(const char* fmt) { diff --git a/src/misc/formater.hh b/src/misc/formater.hh index 0f3d83fd7..ff56cb08f 100644 --- a/src/misc/formater.hh +++ b/src/misc/formater.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -117,16 +117,32 @@ namespace spot { } + /// \brief Scan the %-sequences occuring in \a fmt. + /// + /// Set has['c'] for each %c in \a fmt. \a has must + /// be 256 wide. + /// @{ + void + scan(const char* fmt, std::vector& has) const; + + void + scan(const std::string& fmt, std::vector& has) const + { + scan(fmt.c_str(), has); + } + /// @} + /// Collect the %-sequences occurring in \a fmt. + /// @{ void prime(const char* fmt); - /// Collect the %-sequences occurring in \a fmt. void prime(const std::string& fmt) { prime(fmt.c_str()); } + /// @} /// Whether %c occurred in the primed formats. bool