ltlcross: follow RFC 4180 for CSV output.
* src/misc/escape.cc, src/misc/escape.hh (escape_rfc4180): New function. * src/bin/ltlcross.cc: Do not output space after ',', use "\r\n" for end of line, and use escape_rfc4180(). * NEWS: Mention it.
This commit is contained in:
parent
925a807f4f
commit
1c5536ea9c
4 changed files with 81 additions and 53 deletions
3
NEWS
3
NEWS
|
|
@ -1,6 +1,7 @@
|
||||||
New in spot 1.2a (not released)
|
New in spot 1.2a (not released)
|
||||||
|
|
||||||
Nothing yet.
|
* Bug fixes:
|
||||||
|
- ltlcross' CSV output now stricly follows RFC 4180.
|
||||||
|
|
||||||
New in spot 1.2 (2013-10-01)
|
New in spot 1.2 (2013-10-01)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -298,23 +298,23 @@ struct statistics
|
||||||
void
|
void
|
||||||
to_csv(std::ostream& os)
|
to_csv(std::ostream& os)
|
||||||
{
|
{
|
||||||
os << states << ", "
|
os << states << ','
|
||||||
<< edges << ", "
|
<< edges << ','
|
||||||
<< transitions << ", "
|
<< transitions << ','
|
||||||
<< acc << ", "
|
<< acc << ','
|
||||||
<< scc << ", "
|
<< scc << ','
|
||||||
<< nonacc_scc << ", "
|
<< nonacc_scc << ','
|
||||||
<< terminal_scc << ", "
|
<< terminal_scc << ','
|
||||||
<< weak_scc << ", "
|
<< weak_scc << ','
|
||||||
<< strong_scc << ", "
|
<< strong_scc << ','
|
||||||
<< nondetstates << ", "
|
<< nondetstates << ','
|
||||||
<< nondeterministic << ", "
|
<< nondeterministic << ','
|
||||||
<< terminal_aut << ", "
|
<< terminal_aut << ','
|
||||||
<< weak_aut << ", "
|
<< weak_aut << ','
|
||||||
<< strong_aut << ", "
|
<< strong_aut << ','
|
||||||
<< time << ", "
|
<< time << ','
|
||||||
<< product_states << ", "
|
<< product_states << ','
|
||||||
<< product_transitions << ", "
|
<< product_transitions << ','
|
||||||
<< product_scc;
|
<< product_scc;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
@ -935,7 +935,7 @@ namespace
|
||||||
if (first)
|
if (first)
|
||||||
first = false;
|
first = false;
|
||||||
else
|
else
|
||||||
err << ",";
|
err << ',';
|
||||||
err << l << i;
|
err << l << i;
|
||||||
}
|
}
|
||||||
err << "} disagree with {";
|
err << "} disagree with {";
|
||||||
|
|
@ -946,7 +946,7 @@ namespace
|
||||||
if (first)
|
if (first)
|
||||||
first = false;
|
first = false;
|
||||||
else
|
else
|
||||||
err << ",";
|
err << ',';
|
||||||
err << l << i;
|
err << l << i;
|
||||||
}
|
}
|
||||||
err << "} when evaluating ";
|
err << "} when evaluating ";
|
||||||
|
|
@ -1322,6 +1322,7 @@ namespace
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Output an RFC4180-compatible CSV file.
|
||||||
static void
|
static void
|
||||||
print_stats_csv(const char* filename)
|
print_stats_csv(const char* filename)
|
||||||
{
|
{
|
||||||
|
|
@ -1344,18 +1345,18 @@ print_stats_csv(const char* filename)
|
||||||
|
|
||||||
*out << "\"formula\",\"tool\",";
|
*out << "\"formula\",\"tool\",";
|
||||||
statistics::fields(*out);
|
statistics::fields(*out);
|
||||||
*out << "\n";
|
*out << "\r\n";
|
||||||
for (unsigned r = 0; r < rounds; ++r)
|
for (unsigned r = 0; r < rounds; ++r)
|
||||||
for (unsigned t = 0; t < ntrans; ++t)
|
for (unsigned t = 0; t < ntrans; ++t)
|
||||||
if (vstats[r][t].ok)
|
if (vstats[r][t].ok)
|
||||||
{
|
{
|
||||||
*out << "\"";
|
*out << "\"";
|
||||||
spot::escape_str(*out, formulas[r]);
|
spot::escape_rfc4180(*out, formulas[r]);
|
||||||
*out << "\",\"";
|
*out << "\",\"";
|
||||||
spot::escape_str(*out, translators[t]);
|
spot::escape_rfc4180(*out, translators[t]);
|
||||||
*out << "\",";
|
*out << "\",";
|
||||||
vstats[r][t].to_csv(*out);
|
vstats[r][t].to_csv(*out);
|
||||||
*out << "\n";
|
*out << "\r\n";
|
||||||
}
|
}
|
||||||
delete outfile;
|
delete outfile;
|
||||||
}
|
}
|
||||||
|
|
@ -1404,9 +1405,9 @@ print_stats_json(const char* filename)
|
||||||
if (vstats[r][t].ok)
|
if (vstats[r][t].ok)
|
||||||
{
|
{
|
||||||
if (notfirst)
|
if (notfirst)
|
||||||
*out << ",";
|
*out << ',';
|
||||||
notfirst = true;
|
notfirst = true;
|
||||||
*out << "\n [ " << r << ", " << t << ", ";
|
*out << "\n [ " << r << ',' << t << ',';
|
||||||
vstats[r][t].to_csv(*out);
|
vstats[r][t].to_csv(*out);
|
||||||
*out << " ]";
|
*out << " ]";
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,22 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
std::ostream&
|
||||||
|
escape_rfc4180(std::ostream& os, const std::string& str)
|
||||||
|
{
|
||||||
|
for (std::string::const_iterator i = str.begin(); i != str.end(); ++i)
|
||||||
|
switch (*i)
|
||||||
|
{
|
||||||
|
case '"':
|
||||||
|
os << "\"\"";
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
os << *i;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
return os;
|
||||||
|
}
|
||||||
|
|
||||||
std::ostream&
|
std::ostream&
|
||||||
escape_str(std::ostream& os, const std::string& str)
|
escape_str(std::ostream& os, const std::string& str)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -32,16 +32,26 @@ namespace spot
|
||||||
/// \addtogroup misc_tools
|
/// \addtogroup misc_tools
|
||||||
/// @{
|
/// @{
|
||||||
|
|
||||||
/// \brief Escape characters <code>"</code>, <code>\\</code>, and
|
/// \brief Double characters <code>"</code> in strings.
|
||||||
/// <code>\\n</code> in \a str.
|
///
|
||||||
SPOT_API std::ostream& escape_str(std::ostream& os, const std::string& str);
|
/// In CSV files, as defined by RFC4180, double-quoted string that
|
||||||
|
/// contain double-quotes should simply duplicate those quotes.
|
||||||
|
SPOT_API std::ostream&
|
||||||
|
escape_rfc4180(std::ostream& os, const std::string& str);
|
||||||
|
|
||||||
/// \brief Escape characters <code>"</code>, <code>\\</code>, and
|
/// \brief Escape characters <code>"</code>, <code>\\</code>, and
|
||||||
/// <code>\\n</code> in \a str.
|
/// <code>\\n</code> in \a str.
|
||||||
SPOT_API std::string escape_str(const std::string& str);
|
SPOT_API std::ostream&
|
||||||
|
escape_str(std::ostream& os, const std::string& str);
|
||||||
|
|
||||||
|
/// \brief Escape characters <code>"</code>, <code>\\</code>, and
|
||||||
|
/// <code>\\n</code> in \a str.
|
||||||
|
SPOT_API std::string
|
||||||
|
escape_str(const std::string& str);
|
||||||
|
|
||||||
/// \brief Remove spaces at the front and back of \a str.
|
/// \brief Remove spaces at the front and back of \a str.
|
||||||
SPOT_API void trim(std::string& str);
|
SPOT_API void
|
||||||
|
trim(std::string& str);
|
||||||
/// @}
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue