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

ltlcross: add a complete column

Browse source 
* src/bin/ltlcross.cc: Add the column.
* NEWS: Update.
This commit is contained in:
Alexandre Duret-Lutz 2015-05-25 17:41:02 +02:00
parent ae0f0d5fc2
commit 7b6626d176
2 changed files with 20 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

22
NEWS
View file

@ -91,17 +91,21 @@ New in spot 1.99b (not yet released)
So it can effectively be used to validate tools producing Rabin So it can effectively be used to validate tools producing Rabin
or Streett automata. or Streett automata.
- ltlcross has a new option --grind, that attempts to reduce the - ltlcross has several new options:
size of any bogus formula it discovers, while still exhibiting
the bug.
- ltlcross has a new option --ignore-execution-failures that --grind attempts to reduce the size of any bogus formula it
ignore translator returning non-zero exist status instead of discovers, while still exhibiting the bug.
returning an error.
- ltlcross has a new option --automata to save the produced --ignore-execution-failures that ignores translators returning
automata into the CSV or JSON file. Those automata are saved non-zero exist status instead of returning an error.
into the HOA format.
--automata save the produced automata into the CSV or JSON
file. Those automata are saved into the HOA format.
ltlcross will also output two extra columns in its CSV/JSON
output: "ambiguous_aut" and "complete_aut" are Boolean
that respectively tells whether the automaton is
ambiguous and complete.
- "ltlfilt --stutter-invariant" will now work with PSL formulas. - "ltlfilt --stutter-invariant" will now work with PSL formulas.
The implementation is actually much more efficient The implementation is actually much more efficient

10
src/bin/ltlcross.cc
View file

@ -300,6 +300,7 @@ struct statistics
std::vector<double> product_transitions; std::vector<double> product_transitions;
std::vector<double> product_scc; std::vector<double> product_scc;
bool ambiguous; bool ambiguous;
bool complete;
std::string hoa_str; std::string hoa_str;
static void static void
@ -325,7 +326,8 @@ struct statistics
"\"terminal_aut\"," "\"terminal_aut\","
"\"weak_aut\"," "\"weak_aut\","
"\"strong_aut\"," "\"strong_aut\","
"\"ambiguous_aut\""); "\"ambiguous_aut\","
"\"complete_aut\"");
size_t m = products_avg ? 1U : products; size_t m = products_avg ? 1U : products;
for (size_t i = 0; i < m; ++i) for (size_t i = 0; i < m; ++i)
os << ",\"product_states\",\"product_transitions\",\"product_scc\""; os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
@ -366,7 +368,8 @@ struct statistics
<< terminal_aut << ',' << terminal_aut << ','
<< weak_aut << ',' << weak_aut << ','
<< strong_aut << ',' << strong_aut << ','
<< ambiguous; << ambiguous << ','
<< complete;
if (!products_avg) if (!products_avg)
{ {
for (size_t i = 0; i < products; ++i) for (size_t i = 0; i < products; ++i)
@ -394,7 +397,7 @@ struct statistics
{ {
size_t m = products_avg ? 1U : products; size_t m = products_avg ? 1U : products;
m *= 3; m *= 3;
m += 14 + show_sr * 6; m += 15 + show_sr * 6;
os << na; os << na;
for (size_t i = 0; i < m; ++i) for (size_t i = 0; i < m; ++i)
os << ',' << na; os << ',' << na;
@ -715,6 +718,7 @@ namespace
else else
st->terminal_aut = true; st->terminal_aut = true;
st->ambiguous = !spot::is_unambiguous(res); st->ambiguous = !spot::is_unambiguous(res);
st->complete = spot::is_complete(res);
if (opt_automata) if (opt_automata)
{ {