alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Pick the most readable format available for displaying formulas.

Browse source 
* src/bin/ltlcheck.cc (translator_runner::formula): New function.
(processor::process_formula): Use it.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-05 14:11:03 +02:00
parent 3f5e6102dc
commit e99fdfb650
1 changed files with 24 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/bin/ltlcheck.cc
View file

@ -270,6 +270,19 @@ namespace
toclean.push_back(tmpname); toclean.push_back(tmpname);
} }
const std::string& formula() const
{
// Pick the most readable format we have...
if (!string_ltl_spot.val().empty())
return string_ltl_spot;
if (!string_ltl_spin.val().empty())
return string_ltl_spin;
if (!string_ltl_lbt.val().empty())
return string_ltl_lbt;
error(2, 0, "None of the translators need the input formula?");
return string_ltl_spot;
}
void round_formula(const spot::ltl::formula* f, unsigned serial) void round_formula(const spot::ltl::formula* f, unsigned serial)
{ {
if (has('f') || has('F')) if (has('f') || has('F'))
@ -461,21 +474,23 @@ namespace
(void) linenum; (void) linenum;
static unsigned round = 0; static unsigned round = 0;
if (filename)
std::cerr << filename << ":";
if (linenum)
std::cerr << linenum << ":";
if (filename || linenum)
std::cerr << " ";
spot::ltl::to_string(f, std::cerr);
std::cerr << "\n";
size_t m = translators.size(); size_t m = translators.size();
std::vector<const spot::tgba*> pos(m); std::vector<const spot::tgba*> pos(m);
std::vector<const spot::tgba*> neg(m); std::vector<const spot::tgba*> neg(m);
runner.round_formula(f, round); runner.round_formula(f, round);
// Call formula() before printing anything else, in case it
// complains.
std::string fstr = runner.formula();
if (filename)
std::cerr << filename << ":";
if (linenum)
std::cerr << linenum << ":";
if (filename || linenum)
std::cerr << " ";
std::cerr << fstr << "\n";
for (size_t n = 0; n < m; ++n) for (size_t n = 0; n < m; ++n)
pos[n] = runner.translate(n, 'P'); pos[n] = runner.translate(n, 'P');