Commit 6a547371 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: diagnose missing i/o specifications earlier.

* src/misc/formater.cc, src/misc/formater.hh (scan): New method.
(prime): Use it.
* src/bin/ltlcross.cc (translator_runner::translator_runner): Scan each
specification string, and report those missing an input or output
%-sequence.
* NEWS: Mention it.
parent edd687a3
......@@ -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
......
......@@ -494,10 +494,28 @@ namespace
declare('N', &output);
declare('T', &output);
std::vector<bool> 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 << "]: "
......
// -*- 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<bool>& 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)
{
......
// -*- 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<bool>& has) const;
void
scan(const std::string& fmt, std::vector<bool>& 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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment