Commit 2b10745d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: support --products=+N

* src/bin/ltlcross.cc: Implement it.
* NEWS, doc/org/ltlcross.org: Document it.
* src/tgbatest/ltlcross3.test: Test it.
parent 9577e5d5
......@@ -14,6 +14,9 @@ New in spot 1.2a (not released)
area left empty (in CVS) or null (in JSON). A new option,
--omit-missing can be used to remove lines for failed
translations, and remove these two columns.
- if ltlcross is used with --products=+5 instead of --products=5
then the stastics for each of the five products will be output
separately instead of being averaged.
* Bug fixes:
- ltlcross' CSV output now stricly follows RFC 4180.
- ltlcross failed to report missing input or output escape sequences
......
......@@ -444,6 +444,14 @@ is used, =N= products are builds instead of one, and the fields
=product_states=, =product_transitions=, and =product_scc= contain
average values.
If the option =--products=+N= is used (with a =+= in front of the
number), then no average value is computed. Instead, three columns
=product_states=, =product_transitions=, and =product_scc= are output
for each individual product (i.e., $3\times N$ columns are output).
This might be useful if you want to compute different kind of
statistic (e.g., a median instead of a mean) or if you want to build
scatter plots of all these products.
** Changing the name of the translators
By default, the names used in the CSV and JSON output to designate the
......
......@@ -142,9 +142,9 @@ static const argp_option options[] =
"two states (0.1 by default)", 0 },
{ "seed", OPT_SEED, "INT", 0,
"seed for the random number generator (0 by default)", 0 },
{ "products", OPT_PRODUCTS, "INT", 0,
"number of product to perform (1 by default), statistics will be "
"averaged", 0 },
{ "products", OPT_PRODUCTS, "[+]INT", 0,
"number of products to perform (1 by default), statistics will be "
"averaged unless the number is prefixed with '+'", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Statistics output:", 6 },
{ "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL,
......@@ -203,6 +203,7 @@ bool no_complement = false;
bool stop_on_error = false;
int seed = 0;
unsigned products = 1;
bool products_avg = true;
bool opt_omit = false;
struct translator_spec
......@@ -306,10 +307,7 @@ struct statistics
nondeterministic(false),
terminal_aut(false),
weak_aut(false),
strong_aut(false),
product_states(0),
product_transitions(0),
product_scc(0)
strong_aut(false)
{
}
......@@ -333,9 +331,9 @@ struct statistics
bool terminal_aut;
bool weak_aut;
bool strong_aut;
double product_states;
double product_transitions;
double product_scc;
std::vector<double> product_states;
std::vector<double> product_transitions;
std::vector<double> product_scc;
static void
fields(std::ostream& os, bool all)
......@@ -356,10 +354,10 @@ struct statistics
"\"nondet_aut\","
"\"terminal_aut\","
"\"weak_aut\","
"\"strong_aut\","
"\"product_states\","
"\"product_transitions\","
"\"product_scc\"");
"\"strong_aut\"");
size_t m = products_avg ? 1U : products;
for (size_t i = 0; i < m; ++i)
os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
}
void
......@@ -369,41 +367,64 @@ struct statistics
os << '"' << status_str << "\"," << status_code << ',';
os << time << ',';
if (ok)
os << states << ','
<< edges << ','
<< transitions << ','
<< acc << ','
<< scc << ','
<< nonacc_scc << ','
<< terminal_scc << ','
<< weak_scc << ','
<< strong_scc << ','
<< nondetstates << ','
<< nondeterministic << ','
<< terminal_aut << ','
<< weak_aut << ','
<< strong_aut << ','
<< product_states << ','
<< product_transitions << ','
<< product_scc;
{
os << states << ','
<< edges << ','
<< transitions << ','
<< acc << ','
<< scc << ','
<< nonacc_scc << ','
<< terminal_scc << ','
<< weak_scc << ','
<< strong_scc << ','
<< nondetstates << ','
<< nondeterministic << ','
<< terminal_aut << ','
<< weak_aut << ','
<< strong_aut;
if (!products_avg)
{
for (size_t i = 0; i < products; ++i)
os << ',' << product_states[i]
<< ',' << product_transitions[i]
<< ',' << product_scc[i];
}
else
{
double st = 0.0;
double tr = 0.0;
double sc = 0.0;
for (size_t i = 0; i < products; ++i)
{
st += product_states[i];
tr += product_transitions[i];
sc += product_scc[i];
}
os << ',' << (st / products)
<< ',' << (tr / products)
<< ',' << (sc / products);
}
}
else
os << na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na;
{
os << na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na;
size_t m = products_avg ? 1U : products;
for (size_t i = 0; i < m; ++i)
os << ',' << na << ',' << na << ',' << na;
}
}
};
......@@ -492,6 +513,11 @@ parse_opt(int key, char* arg, struct argp_state*)
json_output = arg ? arg : "-";
break;
case OPT_PRODUCTS:
if (*arg == '+')
{
products_avg = false;
++arg;
}
products = to_pos_int(arg);
break;
case OPT_NOCHECKS:
......@@ -1313,6 +1339,19 @@ namespace
spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
f->destroy();
if (want_stats)
for (size_t i = 0; i < m; ++i)
{
(*pstats)[i].product_states.reserve(products);
(*pstats)[i].product_transitions.reserve(products);
(*pstats)[i].product_scc.reserve(products);
if (neg[i])
{
(*nstats)[i].product_states.reserve(products);
(*nstats)[i].product_transitions.reserve(products);
(*nstats)[i].product_scc.reserve(products);
}
}
for (unsigned p = 0; p < products; ++p)
{
// build a random state-space.
......@@ -1339,14 +1378,13 @@ namespace
// Statistics
if (want_stats)
{
(*pstats)[i].product_scc += sm->scc_count();
(*pstats)[i].product_scc.push_back(sm->scc_count());
spot::tgba_statistics s = spot::stats_reachable(p);
(*pstats)[i].product_states += s.states;
(*pstats)[i].product_transitions += s.transitions;
(*pstats)[i].product_states.push_back(s.states);
(*pstats)[i].product_transitions.push_back(s.transitions);
}
}
if (!no_checks)
for (size_t i = 0; i < m; ++i)
if (neg[i])
......@@ -1360,10 +1398,10 @@ namespace
// Statistics
if (want_stats)
{
(*nstats)[i].product_scc += sm->scc_count();
(*nstats)[i].product_scc.push_back(sm->scc_count());
spot::tgba_statistics s = spot::stats_reachable(p);
(*nstats)[i].product_states += s.states;
(*nstats)[i].product_transitions += s.transitions;
(*nstats)[i].product_states.push_back(s.states);
(*nstats)[i].product_transitions.push_back(s.transitions);
}
}
......@@ -1391,29 +1429,16 @@ namespace
}
// Cleanup.
if (!no_checks)
for (size_t i = 0; i < m; ++i)
{
delete neg_map[i];
delete neg_prod[i];
if (want_stats)
{
(*nstats)[i].product_scc /= products;
(*nstats)[i].product_states /= products;
(*nstats)[i].product_transitions /= products;
}
}
for (size_t i = 0; i < m; ++i)
{
delete pos_map[i];
delete pos_prod[i];
if (want_stats)
{
(*pstats)[i].product_scc /= products;
(*pstats)[i].product_states /= products;
(*pstats)[i].product_transitions /= products;
}
}
delete statespace;
++seed;
......
......@@ -70,3 +70,44 @@ grep '"exit_code"' out.csv && exit 1
test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
test `wc -l < out.csv` -eq 1
check_csv out.csv
# Check with --products=5
run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --products=5 2>stderr
p=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv
# ... unless --omit-missing is supplied.
run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --omit-missing --products=5 2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv
# Check with --products=+5
run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --products=+5 2>stderr
q=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv
# ... unless --omit-missing is supplied.
run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --omit-missing --products=+5 2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv
test $q -eq `expr $p + 12`
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