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

bin: introduce autcross

Browse source 
Fixes #252.

* NEWS: Mention it.
* bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
files.
* bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
doc/Makefile.am: Add them.
* bin/autfilt.cc: Use is_universal() instead of is_deterministic().
* bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
ltlcross, ltldo and autcross.
* tests/core/autcross.test, tests/core/autcross2.test: New files.
* tests/Makefile.am: Add them.
* tests/core/dra2dba.test, tests/core/sbacc.test,
tests/core/streett.test: Use autcross.
This commit is contained in:
Alexandre Duret-Lutz 2017-07-27 18:42:05 +02:00
parent b9fff6a4b1
commit 0cf250d839
21 changed files with 1726 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

11
NEWS
View file

@ -2,6 +2,14 @@ New in spot 2.3.5.dev (not yet released)
Tools:
- genaut is a new binary that produces families of automata defined
in the literature (in the same way as we have genltl for LTL
formulas).
- autcross is a new binary that compares the output of tools
transforming automata (in the same way as we have ltlcross for
LTL translators).
- autfilt learned to build the union (--sum) or the intersection
(--sum-and) of two language by putting two automata side-by-side
and fiddling with the initial states. This complement the already
@ -11,9 +19,6 @@ New in spot 2.3.5.dev (not yet released)
- autfilt learned to complement any alternating automaton with
option --dualize.
- genaut is a binary to produce families of automata defined in the
literature (in the same way as we have genltl for LTL formulas).
- autfilt learned --split-edges to convert labels that are Boolean
formulas into labels that are min-terms. (See spot::split_edges()
below.)

1
bin/.gitignore vendored
View file

@ -1,3 +1,4 @@
autcross
autfilt
dstar2tgba
genaut

2
bin/Makefile.am
View file

@ -59,6 +59,7 @@ libcommon_a_SOURCES = \
common_trans.hh
bin_PROGRAMS = \
autcross \
autfilt \
dstar2tgba \
genaut \
@ -77,6 +78,7 @@ bin_PROGRAMS = \
# version number that is automatically updated).
noinst_PROGRAMS = spot-x spot
autcross_SOURCES = autcross.cc
autfilt_SOURCES = autfilt.cc
ltlfilt_SOURCES = ltlfilt.cc
genaut_SOURCES = genaut.cc

898
bin/autcross.cc Normal file
View file

@ -0,0 +1,898 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "common_sys.hh"
#include <string>
#include <iostream>
#include <sstream>
#include <cstdlib>
#include <cstdio>
#include <argp.h>
#include <unistd.h>
#include <cmath>
#include <sys/wait.h>
#include <iomanip>
#include "error.h"
#include "argmatch.h"
#include "common_setup.hh"
#include "common_hoaread.hh"
#include "common_finput.hh"
#include "common_color.hh"
#include "common_trans.hh"
#include "common_cout.hh"
#include "common_aoutput.hh"
#include "common_post.hh"
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/product.hh>
#include <spot/misc/escape.hh>
const char argp_program_doc[] ="\
Call several tools that process automata and cross-compare their output \
to detect bugs, or to gather statistics. The list of automata to use \
should be supplied on standard input, or using the -f or -F options.\v\
Exit status:\n\
0 everything went fine (timeouts are OK too)\n\
1 some tools failed to output something we understand, or failed\n\
sanity checks (statistics were output nonetheless)\n\
2 autcross aborted on error\n\
";
enum {
OPT_BOGUS = 256,
OPT_CSV,
OPT_HIGH,
OPT_IGNORE_EXEC_FAIL,
OPT_LANG,
OPT_LOW,
OPT_MEDIUM,
OPT_NOCHECKS,
OPT_OMIT,
OPT_STOP_ERR,
OPT_VERBOSE,
};
static const argp_option options[] =
{
{ nullptr, 0, nullptr, 0, "Input:", 1 },
{ "file", 'F', "FILENAME", 0,
"process automata from FILENAME", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "autcross behavior:", 5 },
{ "stop-on-error", OPT_STOP_ERR, nullptr, 0,
"stop on first execution error or failure to pass"
" sanity checks (timeouts are OK)", 0 },
{ "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
"ignore automata from translators that return with a non-zero exit code,"
" but do not flag this as an error", 0 },
{ "language-preserved", OPT_LANG, nullptr, 0,
"expect that each tool preserves the input language", 0 },
{ "no-checks", OPT_NOCHECKS, nullptr, 0,
"do not perform any sanity checks", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Statistics output:", 7 },
{ "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
"output statistics as CSV in FILENAME or on standard output "
"(if '>>' is used to request append mode, the header line is "
"not output)", 0 },
{ "omit-missing", OPT_OMIT, nullptr, 0,
"do not output statistics for timeouts or failed translations", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification level (for complementation):",
21 },
{ "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 },
{ "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
{ "high", OPT_HIGH, nullptr, 0,
"all available optimizations (slow, default)", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -2 },
{ "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
"save formulas for which problems were detected in FILENAME", 0 },
{ "verbose", OPT_VERBOSE, nullptr, 0,
"print what is being done, for debugging", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
const struct argp_child children[] =
{
{ &autproc_argp, 0, nullptr, 0 },
{ &hoaread_argp, 0, "Parsing of automata:", 4 },
{ &misc_argp, 0, nullptr, -2 },
{ &color_argp, 0, nullptr, 0 },
{ nullptr, 0, nullptr, 0 }
};
static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;
static bool stop_on_error = false;
static bool no_checks = false;
static bool opt_language_preserved = false;
static bool opt_omit = false;
static const char* csv_output = nullptr;
static unsigned round_num = 0;
static const char* bogus_output_filename = nullptr;
static output_file* bogus_output = nullptr;
static int
parse_opt(int key, char* arg, struct argp_state*)
{
switch (key)
{
case 'F':
jobs.emplace_back(arg, true);
break;
case OPT_BOGUS:
{
bogus_output = new output_file(arg);
bogus_output_filename = arg;
break;
}
case OPT_CSV:
csv_output = arg ? arg : "-";
break;
case OPT_HIGH:
level = spot::postprocessor::High;
level_set = true;
break;
case OPT_IGNORE_EXEC_FAIL:
ignore_exec_fail = true;
break;
case OPT_LANG:
opt_language_preserved = true;
break;
case OPT_LOW:
level = spot::postprocessor::Low;
level_set = true;
break;
case OPT_MEDIUM:
level = spot::postprocessor::Medium;
level_set = true;
break;
case OPT_NOCHECKS:
no_checks = true;
break;
case OPT_OMIT:
opt_omit = true;
break;
case OPT_STOP_ERR:
stop_on_error = true;
break;
case OPT_VERBOSE:
verbose = true;
break;
case ARGP_KEY_ARG:
if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true);
else
tools_push_autproc(arg);
break;
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
static bool global_error_flag = false;
// static unsigned oom_count = 0U;
static std::ostream&
global_error()
{
global_error_flag = true;
std::cerr << bright_red;
return std::cerr;
}
static void
end_error()
{
std::cerr << reset_color;
}
static std::ostream&
example()
{
std::cerr << bold_std;
return std::cerr;
}
struct aut_statistics
{
unsigned ap;
unsigned states;
unsigned edges;
unsigned transitions;
unsigned acc_sets;
unsigned scc;
unsigned nondetstates;
bool nondeterministic;
bool alternating;
aut_statistics()
{
}
void set(const spot::const_twa_graph_ptr& aut)
{
if (!csv_output)
// Do not waste time.
return;
ap = aut->ap().size();
spot::twa_sub_statistics s = sub_stats_reachable(aut);
states = s.states;
edges = s.edges;
transitions = s.transitions;
spot::scc_info m(aut);
acc_sets = aut->num_sets();
unsigned c = m.scc_count();
scc = c;
nondetstates = spot::count_nondet_states(aut);
nondeterministic = nondetstates != 0;
alternating = !aut->is_existential();
}
void to_csv(std::ostream& os) const
{
os << ap << ','
<< states << ','
<< edges << ','
<< transitions << ','
<< acc_sets << ','
<< scc << ','
<< nondetstates << ','
<< nondeterministic << ','
<< alternating;
}
void empty(std::ostream& os) const
{
os << ",,,,,,,,";
}
static void fields(std::ostream& os, const char* prefix)
{
os << '"'
<< prefix << "ap\",\""
<< prefix << "states\",\""
<< prefix << "edges\",\""
<< prefix << "transitions\",\""
<< prefix << "acc_sets\",\""
<< prefix << "scc\",\""
<< prefix << "nondetstates\",\""
<< prefix << "nondeterministic\",\""
<< prefix << "alternating\"";
}
};
struct in_statistics
{
std::string input_source;
std::string input_name;
aut_statistics input;
static void fields(std::ostream& os)
{
os << "\"input.source\",\"input.name\",";
aut_statistics::fields(os, "input.");
}
void to_csv(std::ostream& os) const
{
spot::escape_rfc4180(os << '"', input_source) << "\",";
if (!input_name.empty())
spot::escape_rfc4180(os << '"', input_name) << "\",";
else
os << ',';
input.to_csv(os);
}
};
struct out_statistics
{
// If OK is false, output statistics are not available.
bool ok;
const char* status_str;
int status_code;
double time;
aut_statistics output;
out_statistics()
: ok(false),
status_str(nullptr),
status_code(0),
time(0)
{
}
static void fields(std::ostream& os)
{
os << "\"exit_status\",\"exit_code\",\"time\",";
aut_statistics::fields(os, "output.");
}
void to_csv(std::ostream& os) const
{
os << '"' << status_str << "\"," << status_code << ','
<< time << ',';
if (ok)
output.to_csv(os);
else
output.empty(os);
}
};
std::vector<in_statistics> input_statistics;
typedef std::vector<out_statistics> vector_tool_statistics;
std::vector<vector_tool_statistics> output_statistics;
namespace
{
class autcross_runner final: public autproc_runner
{
spot::bdd_dict_ptr dict;
public:
autcross_runner(spot::bdd_dict_ptr dict)
: dict(dict)
{
}
spot::twa_graph_ptr
run_tool(unsigned int tool_num, char l, bool& problem,
out_statistics& stats)
{
output.reset(tool_num);
std::ostringstream command;
format(command, tools[tool_num].cmd);
std::string cmd = command.str();
std::cerr << "Running [" << l << tool_num << "]: "
<< cmd << std::endl;
process_timer timer;
timer.start();
int es = exec_with_timeout(cmd.c_str());
timer.stop();
const char* status_str = nullptr;
spot::twa_graph_ptr res = nullptr;
if (timed_out)
{
// This is not considered to be a global error.
std::cerr << "warning: timeout during execution of command\n";
++timeout_count;
status_str = "timeout";
problem = false; // A timeout is not a sign of a bug
es = -1;
}
else if (WIFSIGNALED(es))
{
status_str = "signal";
problem = true;
es = WTERMSIG(es);
global_error() << "error: execution terminated by signal "
<< es << ".\n";
end_error();
}
else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
{
es = WEXITSTATUS(es);
status_str = "exit code";
if (!ignore_exec_fail)
{
problem = true;
global_error() << "error: execution returned exit code "
<< es << ".\n";
end_error();
}
else
{
problem = false;
std::cerr << "warning: execution returned exit code "
<< es << ".\n";
++ignored_exec_fail;
}
}
else
{
status_str = "ok";
problem = false;
es = 0;
auto aut = spot::parse_aut(output.val()->name(), dict,
spot::default_environment::instance(),
opt_parse);
if (!aut->errors.empty())
{
status_str = "parse error";
problem = true;
es = -1;
std::ostream& err = global_error();
err << "error: failed to parse the produced automaton.\n";
aut->format_errors(err);
end_error();
res = nullptr;
}
else if (aut->aborted)
{
status_str = "aborted";
problem = true;
es = -1;
global_error() << "error: aborted HOA file.\n";
end_error();
res = nullptr;
}
else
{
res = aut->aut;
}
}
output.cleanup();
stats.status_str = status_str;
stats.status_code = es;
stats.time = timer.get_lap_sw();
if (res)
{
stats.ok = true;
stats.output.set(res);
}
return res;
}
};
static std::string
autname(unsigned i, bool complemented = false)
{
std::ostringstream str;
if (complemented)
str << "Comp(";
if (i < tools.size())
str << 'A' << i;
else
str << "input";
if (complemented)
str << ')';
return str.str();
}
static bool
check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
const spot::const_twa_graph_ptr& aut_j,
size_t i, size_t j)
{
if (aut_i->num_sets() + aut_j->num_sets()
> 8 * sizeof(spot::acc_cond::mark_t::value_t))
{
std::cerr << "info: building " << autname(i)
<< '*' << autname(j, true)
<< " requires more acceptance sets than supported\n";
return false;
}
auto prod = spot::product(aut_i, aut_j);
if (verbose)
std::cerr << "info: check_empty "
<< autname(i) << '*' << autname(j, true) << '\n';
auto w = prod->accepting_word();
if (w)
{
std::ostream& err = global_error();
err << "error: " << autname(i) << '*' << autname(j, true)
<< (" is nonempty; both automata accept the infinite word:\n"
" ");
example() << *w << '\n';
end_error();
}
return !!w;
}
class autcross_processor final: public hoa_processor
{
autcross_runner runner;
public:
autcross_processor()
: hoa_processor(spot::make_bdd_dict()), runner(dict_)
{
}
int
process_automaton(const spot::const_parsed_aut_ptr& haut) override
{
auto printsize = [](const spot::const_twa_graph_ptr& aut,
bool props)
{
std::cerr << '(' << aut->num_states() << " st.,"
<< aut->num_edges() << " ed.,"
<< aut->num_sets() << " sets)";
if (props)
{
if (!aut->is_existential())
std::cerr << " univ-edges";
if (is_deterministic(aut))
std::cerr << " deterministic";
if (is_complete(aut))
std::cerr << " complete";
std::cerr << '\n';
}
};
spot::twa_graph_ptr input = haut->aut;
runner.round_automaton(input, round_num);
std::string source = [&]()
{
std::ostringstream src;
src << haut->filename << ':' << haut->loc;
return src.str();
}();
input_statistics.push_back(in_statistics());
std::cerr << bold << source << reset_color;
input_statistics[round_num].input_source = std::move(source);
if (auto name = input->get_named_prop<std::string>("automaton-name"))
{
std::cerr << '\t' << *name;
input_statistics[round_num].input_name = *name;
}
std::cerr << '\n';
input_statistics[round_num].input.set(input);
int problems = 0;
size_t m = tools.size();
size_t mi = m + opt_language_preserved;
std::vector<spot::twa_graph_ptr> pos(mi);
std::vector<spot::twa_graph_ptr> neg(mi);
vector_tool_statistics stats(m);
if (opt_language_preserved)
pos[mi - 1] = input;
if (verbose)
{
std::cerr << "info: input\t";
printsize(input, true);
}
for (size_t n = 0; n < m; ++n)
{
bool prob;
pos[n] = runner.run_tool(n, 'A', prob, stats[n]);
problems += prob;
}
spot::cleanup_tmpfiles();
++round_num;
output_statistics.push_back(std::move(stats));
if (verbose)
{
std::cerr << "info: collected automata:\n";
for (unsigned i = 0; i < m; ++i)
if (pos[i])
{
std::cerr << "info: A" << i << '\t';
printsize(pos[i], true);
}
}
if (!no_checks)
{
std::cerr << "Performing sanity checks and gathering statistics..."
<< std::endl;
{
bool print_first = true;
for (unsigned i = 0; i < mi; ++i)
{
if (!pos[i])
continue;
if (!pos[i]->is_existential())
{
if (verbose)
{
if (print_first)
{
std::cerr <<
"info: getting rid of universal edges...\n";
print_first = false;
}
std::cerr << "info: "
<< std::setw(8) << autname(i) << '\t';
printsize(pos[i], false);
std::cerr << " -> ";
}
pos[i] = remove_alternation(pos[i]);
if (verbose)
{
printsize(pos[i], false);
std::cerr << '\n';
}
}
if (is_universal(pos[i]))
neg[i] = dualize(pos[i]);
}
}
{
bool print_first = verbose;
for (unsigned i = 0; i < mi; ++i)
{
if (pos[i] && !neg[i])
{
if (print_first)
{
std::cerr << "info: complementing non-deterministic "
"automata via determinization...\n";
print_first = false;
}
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(level);
neg[i] = dualize(p.run(pos[i]));
if (verbose)
{
std::cerr << "info: "
<< std::setw(8) << autname(i) << '\t';
printsize(pos[i], false);
std::cerr << " -> ";
printsize(neg[i], false);
std::cerr << '\t' << autname(i, true) << '\n';
}
}
};
}
{
bool print_first = true;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
bool neg)
{
if (!x[i])
return;
if (x[i]->acc().uses_fin_acceptance())
{
if (verbose)
{
if (print_first)
{
std::cerr <<
"info: getting rid of any Fin acceptance...\n";
print_first = false;
}
std::cerr << "info: "
<< std::setw(8) << autname(i, neg) << '\t';
printsize(x[i], false);
std::cerr << " ->";
}
cleanup_acceptance_here(x[i]);
x[i] = remove_fin(x[i]);
if (verbose)
{
std::cerr << ' ';
printsize(x[i], false);
std::cerr << '\n';
}
}
else
{
// Remove useless sets nonetheless.
cleanup_acceptance_here(x[i]);
}
};
for (unsigned i = 0; i < mi; ++i)
{
tmp(pos, i, false);
tmp(neg, i, true);
}
}
// Just make a circular implication check
// A0 <= A1, A1 <= A2, ..., AN <= A0
unsigned ok = 0;
for (size_t i = 0; i < mi; ++i)
if (pos[i])
{
size_t j = ((i + 1) % mi);
if (i != j && neg[j])
{
int res = check_empty_prod(pos[i], neg[j], i, j);
problems += res;
ok += !res;
}
}
// If the circular check failed, do the rest of all
// mi(mi-1)/2 checks, as this will help diagnose the issue.
if (ok != mi)
for (size_t i = 0; i < mi; ++i)
if (pos[i])
{
size_t k = ((i + 1) % mi);
for (size_t j = 0; j < mi; ++j)
if (i != j && j != k && neg[j])
problems += check_empty_prod(pos[i], neg[j], i, j);
}
}
else
{
std::cerr << "Gathering statistics..." << std::endl;
}
if (problems && bogus_output)
print_hoa(bogus_output->ostream(), input) << std::endl;
std::cerr << std::endl;
// Shall we stop processing now?
abort_run = global_error_flag && stop_on_error;
return problems;
}
};
}
// Output an RFC4180-compatible CSV file.
static void
print_stats_csv(const char* filename)
{
if (verbose)
std::cerr << "info: writing CSV to " << filename << '\n';
output_file outf(filename);
std::ostream& out = outf.ostream();
unsigned ntools = tools.size();
assert(round_num == output_statistics.size());
assert(round_num == input_statistics.size());
if (!outf.append())
{
// Do not output the header line if we append to a file.
// (Even if that file was empty initially.)
in_statistics::fields(out);
out << ",\"tool\",";
out_statistics::fields(out);
out << '\n';
}
for (unsigned r = 0; r < round_num; ++r)
for (unsigned t = 0; t < ntools; ++t)
if (!opt_omit || output_statistics[r][t].ok)
{
input_statistics[r].to_csv(out);
out << ",\"";
spot::escape_rfc4180(out, tools[t].name);
out << "\",";
output_statistics[r][t].to_csv(out);
out << '\n';
}
outf.close(filename);
}
int
main(int argc, char** argv)
{
setup(argv);
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
exit(err);
check_no_automaton();
auto s = tools.size();
if (s == 0)
error(2, 0, "No tool to run? Run '%s --help' for usage.",
program_name);
if (s == 1 && !opt_language_preserved && !no_checks)
error(2, 0, "Since --language-preserved is not used, you need "
"at least two tools to compare.");
setup_color();
setup_sig_handler();
autcross_processor p;
if (p.run())
return 2;
if (round_num == 0)
{
error(2, 0, "no automaton to translate");
}
else
{
if (global_error_flag)
{
std::ostream& err = global_error();
if (bogus_output)
err << ("error: some error was detected during the above runs.\n"
" Check file ")
<< bogus_output_filename
<< " for problematic automata.";
else
err << ("error: some error was detected during the above runs,\n"
" please search for 'error:' messages in the above"
" trace.");
err << std::endl;
end_error();
}
else if (timeout_count == 0 && ignored_exec_fail == 0)
{
std::cerr << "No problem detected." << std::endl;
}
else
{
std::cerr << "No major problem detected." << std::endl;
}
unsigned additional_errors = 0U;
additional_errors += timeout_count > 0;
additional_errors += ignored_exec_fail > 0;
if (additional_errors)
{
std::cerr << (global_error_flag ? "Additionally, " : "However, ");
if (timeout_count)
{
if (additional_errors > 1)
std::cerr << "\n - ";
if (timeout_count == 1)
std::cerr << "1 timeout occurred";
else
std::cerr << timeout_count << " timeouts occurred";
}
if (ignored_exec_fail)
{
if (additional_errors > 1)
std::cerr << "\n - ";
if (ignored_exec_fail == 1)
std::cerr << "1 non-zero exit status was ignored";
else
std::cerr << ignored_exec_fail
<< " non-zero exit statuses were ignored";
}
if (additional_errors == 1)
std::cerr << '.';
std::cerr << std::endl;
}
}
if (csv_output)
print_stats_csv(csv_output);
return global_error_flag;
}

2
bin/autfilt.cc
View file

@ -515,7 +515,7 @@ static bool opt_highlight_languages = false;
static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
{
if ((!nonalt || aut->is_existential()) && spot::is_deterministic(aut))
if ((!nonalt || aut->is_existential()) && spot::is_universal(aut))
return aut;
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);

1
bin/common_hoaread.hh
View file

@ -43,6 +43,7 @@ read_automaton(const char* filename, spot::bdd_dict_ptr& dict);
class hoa_processor: public job_processor
{
protected:
spot::bdd_dict_ptr dict_;
public:

218
bin/common_trans.cc
View file

@ -33,14 +33,17 @@
#include <spot/tl/unabbrev.hh>
#include "common_conv.hh"
#include <spot/misc/escape.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/lbtt.hh>
#include <spot/twaalgos/neverclaim.hh>
// A set of tools for which we know the correct output
static struct shorthands_t
struct shorthands_t
{
const char* prefix;
const char* suffix;
}
shorthands[] = {
};
static shorthands_t shorthands_ltl[] = {
{ "lbt", " <%L>%O" },
{ "ltl2ba", " -f %s>%O" },
{ "ltl2da", " %f>%O" },
@ -55,25 +58,30 @@ static struct shorthands_t
{ "spin", " -f %s>%O" },
};
static void show_shorthands()
static shorthands_t shorthands_autproc[] = {
{ "autfilt", " %H>%O" },
{ "dstar2tgba", " %H>%O" },
{ "ltl2dstar", " -B %H %O" },
{ "nba2ldpa", " <%H>%O" },
{ "seminator", " %H>%O" },
};
static void show_shorthands(shorthands_t* begin, shorthands_t* end)
{
std::cout
<< ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n"
"the following words, then the string on the right is appended.\n\n");
for (auto& s: shorthands)
std::cout << " "
<< std::left << std::setw(12) << s.prefix
<< s.suffix << '\n';
std::cout
<< ("\nAny {name} and directory component is skipped for the purpose of\n"
"matching those prefixes. So for instance\n"
" '{DRA} ~/mytools/ltl2dstar-0.5.2'\n"
"will changed into\n"
" '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'\n");
while (begin != end)
{
std::cout << " "
<< std::left << std::setw(12) << begin->prefix
<< begin->suffix << '\n';
++begin;
}
}
tool_spec::tool_spec(const char* spec)
tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end)
: spec(spec), cmd(spec), name(spec)
{
if (*cmd == '{')
@ -114,8 +122,9 @@ tool_spec::tool_spec(const char* spec)
++pos;
}
// Match a shorthand.
for (auto& p: shorthands)
while (begin != end)
{
auto& p = *begin++;
int n = strlen(p.prefix);
if (strncmp(basename, p.prefix, n) == 0)
{
@ -165,6 +174,20 @@ tool_spec::~tool_spec()
std::vector<tool_spec> tools;
void tools_push_trans(const char* trans)
{
tools.emplace_back(trans,
std::begin(shorthands_ltl),
std::end(shorthands_ltl));
}
void tools_push_autproc(const char* proc)
{
tools.emplace_back(proc,
std::begin(shorthands_autproc),
std::end(shorthands_autproc));
}
void
quoted_string::print(std::ostream& os, const char*) const
{
@ -254,16 +277,8 @@ printable_result_filename::print(std::ostream& os, const char*) const
spot::quote_shell_string(os, val()->name());
}
void
filed_formula::print(std::ostream& os, const char* pos) const
{
std::ostringstream ss;
f_.print(ss, pos);
os << '\'' << string_to_tmp(ss.str(), serial_) << '\'';
}
std::string
filed_formula::string_to_tmp(const std::string str, unsigned n) const
static std::string
string_to_tmp(const std::string str, unsigned n)
{
char prefix[30];
snprintf(prefix, sizeof prefix, "lcr-i%u-", n);
@ -278,6 +293,43 @@ filed_formula::string_to_tmp(const std::string str, unsigned n) const
return tmpname;
}
void
filed_formula::print(std::ostream& os, const char* pos) const
{
std::ostringstream ss;
f_.print(ss, pos);
os << '\'' << string_to_tmp(ss.str(), serial_) << '\'';
}
void
filed_automaton::print(std::ostream& os, const char* pos) const
{
std::ostringstream ss;
char* opt = nullptr;
if (*pos == '[')
{
++pos;
auto end = strchr(pos, ']');
opt = strndup(pos, end - pos);
pos = end + 1;
}
switch (*pos)
{
case 'H':
spot::print_hoa(ss, aut_, opt);
break;
case 'S':
spot::print_never_claim(ss, aut_, opt);
break;
case 'L':
spot::print_lbtt(ss, aut_, opt);
break;
}
if (opt)
free(opt);
os << '\'' << string_to_tmp(ss.str(), serial_) << '\'';
}
translator_runner::translator_runner(spot::bdd_dict_ptr dict,
bool no_output_allowed)
: dict(dict)
@ -345,6 +397,42 @@ translator_runner::round_formula(spot::formula f, unsigned serial)
filename_formula.new_round(serial);
}
autproc_runner::autproc_runner(bool no_output_allowed)
{
declare('H', &filename_automaton);
declare('S', &filename_automaton);
declare('L', &filename_automaton);
declare('O', &output);
size_t s = tools.size();
assert(s);
for (size_t n = 0; n < s; ++n)
{
// Check that each translator uses at least one input and
// one output.
std::vector<bool> has(256);
const tool_spec& t = tools[n];
scan(t.cmd, has);
if (!(has['H'] || has['S'] || has['L']))
error(2, 0, "no input %%-sequence in '%s'.\n Use "
"one of %%H,%%S,%%L to indicate the input automaton filename.",
t.spec);
if (!no_output_allowed && !has['O'])
error(2, 0, "no output %%-sequence in '%s'.\n Use "
"%%O to indicate where the automaton is output.",
t.spec);
// Remember the %-sequences used by all tools.
prime(t.cmd);
}
}
void
autproc_runner::round_automaton(spot::const_twa_graph_ptr aut, unsigned serial)
{
filename_automaton.new_round(aut, serial);
}
volatile bool timed_out = false;
unsigned timeout_count = 0;
@ -553,7 +641,7 @@ exec_command(const char* cmd)
int fd0 = open(stdin, O_RDONLY, 0644);
if (fd0 < 0)
error(2, errno, "failed to open '%s'", stdin);
if (dup2(fd0, 0) < 0)
if (dup2(fd0, STDIN_FILENO) < 0)
error(2, errno, "dup2() failed");
if (close(fd0) < 0)
error(2, errno, "close() failed");
@ -563,7 +651,7 @@ exec_command(const char* cmd)
int fd1 = creat(stdout, 0644);
if (fd1 < 0)
error(2, errno, "failed to open '%s'", stdout);
if (dup2(fd1, 1) < 0)
if (dup2(fd1, STDOUT_FILENO) < 0)
error(2, errno, "dup2() failed");
if (close(fd1) < 0)
error(2, errno, "close() failed");
@ -602,6 +690,11 @@ exec_with_timeout(const char* cmd)
if (child_pid == 0)
{
setpgid(0, 0);
// Close stdin so that children may not read our input. We had
// this nice surprise with Seminator, who greedily consumes its
// stdin (which was also ours) even if it does not use it
// because it was given a file.
close(STDIN_FILENO);
exec_command(cmd);
// never reached
return -1;
@ -675,7 +768,7 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*)
switch (key)
{
case 't':
tools.push_back(arg);
tools_push_trans(arg);
break;
case 'T':
timeout = to_pos_int(arg);
@ -685,7 +778,14 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*)
#endif
break;
case OPT_LIST:
show_shorthands();
show_shorthands(std::begin(shorthands_ltl), std::end(shorthands_ltl));
std::cout
<< ("\nAny {name} and directory component is skipped for the purpose "
"of\nmatching those prefixes. So for instance\n "
"'{DRA} ~/mytools/ltl2dstar-0.5.2'\n"
"will be changed into\n "
"'{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MW]L %O'"
"\n");
exit(0);
case OPT_RELABEL:
opt_relabel = true;
@ -698,3 +798,61 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*)
const struct argp trans_argp = { options, parse_opt_trans, nullptr, nullptr,
nullptr, nullptr, nullptr };
static const argp_option options_aut[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Specifying tools to call:", 2 },
{ "tool", 't', "COMMANDFMT", 0,
"register one tool to call", 0 },
{ "timeout", 'T', "NUMBER", 0, "kill tools after NUMBER seconds", 0 },
{ "list-shorthands", OPT_LIST, nullptr, 0,
"list availabled shorthands to use in COMMANDFMT", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0,
"COMMANDFMT should specify input and output arguments using the "
"following character sequences:", 3 },
{ "%H,%S,%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"filename for the input automaton in (H) HOA, (S) Spin's neverclaim, "
"or (L) LBTT's format", 0 },
{ "%O", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"filename for the automaton output in HOA, never claim, LBTT, or "
"ltl2dstar's format", 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
static int parse_opt_autproc(int key, char* arg, struct argp_state*)
{
switch (key)
{
case 't':
tools_push_autproc(arg);
break;
case 'T':
timeout = to_pos_int(arg);
#if !ENABLE_TIMEOUT
std::cerr << "warning: setting a timeout is not supported "
<< "on your platform" << std::endl;
#endif
break;
case OPT_LIST:
show_shorthands(std::begin(shorthands_autproc),
std::end(shorthands_autproc));
std::cout
<< ("\nAny {name} and directory component is skipped for the purpose "
"of\nmatching those prefixes. So for instance\n "
"'{AF} ~/mytools/autfilt-2.4 --remove-fin'\n"
"will be changed into\n "
"'{AF} ~/mytools/autfilt-2.4 --remove-fin %H>%O'\n");
exit(0);
default:
return ARGP_ERR_UNKNOWN;
}
return 0;
}
const struct argp autproc_argp = { options_aut, parse_opt_autproc, nullptr,
nullptr, nullptr, nullptr, nullptr };

48
bin/common_trans.hh
View file

@ -28,9 +28,13 @@
#include <spot/twa/twagraph.hh>
extern const struct argp trans_argp;
extern const struct argp trans_argp; // ltlcross, ltldo
extern const struct argp autproc_argp; // autcross
extern bool opt_relabel;
struct shorthands_t;
struct tool_spec
{
// The translator command, as specified on the command-line.
@ -44,7 +48,7 @@ struct tool_spec
// name of the translator (or spec)
const char* name;
tool_spec(const char* spec);
tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end);
tool_spec(const tool_spec& other);
tool_spec& operator=(const tool_spec& other);
~tool_spec();
@ -52,6 +56,9 @@ struct tool_spec
extern std::vector<tool_spec> tools;
void tools_push_trans(const char* trans);
void tools_push_autproc(const char* proc);
struct quoted_string final: public spot::printable_value<std::string>
{
using spot::printable_value<std::string>::operator=;
@ -80,7 +87,25 @@ struct filed_formula final: public spot::printable
private:
const quoted_formula& f_;
unsigned serial_;
std::string string_to_tmp(const std::string str, unsigned n) const;
};
struct filed_automaton final: public spot::printable
{
filed_automaton()
{
}
void print(std::ostream& os, const char* pos) const override;
void new_round(spot::const_twa_graph_ptr aut, unsigned serial)
{
aut_ = aut;
serial_ = serial;
}
private:
spot::const_twa_graph_ptr aut_;
unsigned serial_;
};
struct printable_result_filename final:
@ -118,6 +143,23 @@ public:
};
class autproc_runner: protected spot::formater
{
protected:
// Round-specific variables
filed_automaton filename_automaton;
// Run-specific variables
printable_result_filename output;
public:
using spot::formater::has;
autproc_runner(// whether we accept the absence of output
// specifier
bool no_output_allowed = false);
void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial);
};
// Disable handling of timeout on systems that miss kill() or alarm().
// For instance MinGW.
#if HAVE_KILL && HAVE_ALARM

5
bin/ltlcross.cc
View file

@ -219,7 +219,6 @@ example()
return std::cerr;
}
static void
end_error()
{
@ -423,7 +422,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true);
else
tools.push_back(arg);
tools_push_trans(arg);
break;
case OPT_AUTOMATA:
opt_automata = true;
@ -1111,7 +1110,7 @@ namespace
std::vector<spot::twa_graph_ptr>& comp,
unsigned i)
{
if (!no_complement && x[i] && is_deterministic(x[i]))
if (!no_complement && x[i] && is_universal(x[i]))
comp[i] = dualize(x[i]);
};

2
bin/ltldo.cc
View file

@ -171,7 +171,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true);
else
tools.push_back(arg);
tools_push_trans(arg);
break;
default:
return ARGP_ERR_UNKNOWN;

4
bin/man/Makefile.am
View file

@ -25,6 +25,7 @@ convman7 = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
"$(PERL)" "$(top_srcdir)/tools/help2man -s7 -N"
dist_man1_MANS = \
autcross.1 \
autfilt.1 \
dstar2tgba.1 \
genaut.1 \
@ -44,6 +45,9 @@ dist_man7_MANS = \
MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS)
EXTRA_DIST = $(dist_man1_MANS:.1=.x) $(dist_man7_MANS:.7=.x)
autcross.1: $(common_dep) $(srcdir)/autcross.x $(srcdir)/../autcross.cc
$(convman) ../autcross$(EXEEXT) $(srcdir)/autcross.x $@
autfilt.1: $(common_dep) $(srcdir)/autfilt.x $(srcdir)/../autfilt.cc
$(convman) ../autfilt$(EXEEXT) $(srcdir)/autfilt.x $@

97
bin/man/autcross.x Normal file
View file

@ -0,0 +1,97 @@
.\" -*- coding: utf-8 -*-
[NAME]
autcross \- cross-compare tools that process automata
[ENVIRONMENT VARIABLES]
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
These variables control in which directory temporary files (e.g.,
those who contain the input and output when interfacing with
translators) are created. \fBTMPDIR\fR is only read if
\fBSPOT_TMPDIR\fR does not exist. If none of these environment
variables exist, or if their value is empty, files are created in the
current directory.
.TP
\fBSPOT_TMPKEEP\fR
When this variable is defined, temporary files are not removed.
This is mostly useful for debugging.
[OUTPUT DATA]
The following columns are output in the CSV files.
.TP
\fBinput.source\fR
Location of the input automaton fed to the tool.
.TP
\fBinput.name\fR
Name of the input automaton, if any. This is supported
by the HOA format.
.TP
\fBinput.ap\fR,\fBoutput.ap\fR,
Number of atomic proposition in the input and output automata.
.TP
\fBinput.states\fR,\fBoutput.states\fR
Number of states in the input and output automata.
.TP
\fBinput.edges\fR,\fBoutput.edges\fR
Number of edges in the input and output automata.
.TP
\fBinput.transitions\fR,\fBoutput.transitions\fR
Number of transitions in the input and output automata.
.TP
\fBinput.acc_sets\fR,\fBoutput.acc_sets\fR
Number of acceptance sets in the input and output automata.
.TP
\fBinput.scc\fR,\fBoutput.scc\fR
Number of strongly connected components in the input and output automata.
.TP
\fBinput.nondetstates\fR,\fBoutput.nondetstates\fR
Number of nondeterministic states in the input and output automata.
.TP
\fBinput.nondeterministic\fR,\fBoutput.nondetstates\fR
1 if the automaton is nondeterministic, 0 if it is deterministic.
.TP
\fBinput.alternating\fR,\fBoutput.alternating\fR
1 if the automaton has some universal branching, 0 otherwise.
\fBexit_status\fR, \fBexit_code\fR
Information about how the execution of the tool went.
\fBexit_status\fR is a string that can take the following
values:
.RS
.TP
\f(CW"ok"\fR
The tool ran succesfully (this does not imply that the produced
automaton is correct) and autcross could parse the resulting
automaton. In this case \fBexit_code\fR is always 0.
.TP
\f(CW"timeout"\fR
The tool ran for more than the number of seconds
specified with the \fB\-\-timeout\fR option. In this
case \fBexit_code\fR is always -1.
.TP
\f(CW"exit code"\fR
The tool terminated with a non-zero exit code.
\fBexit_code\fR contains that value.
.TP
\f(CW"signal"\fR
The tool terminated with a signal.
\fBexit_code\fR contains that signal's number.
.TP
\f(CW"parse error"\fR
The tool terminated normally, but autcross could not
parse its output. In this case \fBexit_code\fR is always -1.
.TP
\f(CW"no output"\fR
The tool terminated normally, but without creating the specified
output file. In this case \fBexit_code\fR is always -1.
.RE
.TP
\fBtime\fR
A floating point number giving the run time of the tool in seconds.
This is reported for all executions, even failling ones.
[SEE ALSO]
.BR randaut (1),
.BR genaut (1),
.BR autfilt (1),
.BR ltlcross (1)

1
doc/Makefile.am
View file

@ -78,6 +78,7 @@ ORG_FILES = \
org/spot.css \
org/arch.tex \
$(srcdir)/org/arch.png \
org/autcross.org \
org/autfilt.org \
org/csv.org \
org/citing.org \

388
doc/org/autcross.org Normal file
View file

@ -0,0 +1,388 @@
# -*- coding: utf-8 -*-
#+TITLE: =autcross=
#+DESCRIPTION: Spot command-line tool for cross-comparing the output of automaton processors.
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
=autcross= is a tool for cross-comparing the output of tools that
transform automata. It works similarly to [[file:ltlcross.org][=ltlcross=]] except that
inputs are automata.
The core of =autcross= is a loop that does the following steps:
- Input an automaton
- Process that input automaton with all the configured tools.
If there are 3 translators, the automata produced by those tools
will be named =A0=, =A1=, and =A2=.
- Ensure that all produced automata are equivalent.
Statistics about the results of each tools can optionally be saved in
a CSV file. And in case only those statistics matters, it is also
possible to disable the equivalence checks.
* Input automata
The input automata can be supplied either on standard input, or in
files specified with option =-F=.
If an input automaton is expressed in the HOA format and has a name,
that name will be displayed by =autcross= when processing the automaton,
and will appear in the CSV file if such a file is output.
* Specifying the tools to test
Each tool should be specified as a string that uses some of the
following character sequences:
#+BEGIN_SRC sh :results verbatim :exports results
autcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
: %% a single %
: %H,%S,%L filename for the input automaton in (H) HOA, (S)
: Spin's neverclaim, or (L) LBTT's format
: %O filename for the automaton output in HOA, never
: claim, LBTT, or ltl2dstar's format
For instance we can use =autfilt --complement %H >%O= to indicate that
=autfilt= reads one file (=%H=) in the HOA format, and to redirect the
output in file so that =autcross= can find it. The output format is
automatically detected, so a generic =%O= is used for the output file
regardless of its format.
Another tool that can complement automata is =ltl2dstar=, using
the syntax =ltl2dstar -B --complement-input=yes %H %O=. So to
compare the results of these two tools we could use:
#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b |
autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O'
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports output
randaut -B -n 3 a b |
autcross 'autfilt --complement %H >%O' 'ltl2dstar --complement-input=yes -B %H %O' 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
-:1.1-45.7
Running [A0]: autfilt --complement 'lcr-i0-Nr1xZO' >'lcr-o0-urHakt'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i0-mmkgH7' 'lcr-o1-ABdm4L'
Performing sanity checks and gathering statistics...
-:46.1-92.7
Running [A0]: autfilt --complement 'lcr-i1-5kMYrq' >'lcr-o0-9kvBP4'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i1-lVlGfJ' 'lcr-o1-BexLFn'
Performing sanity checks and gathering statistics...
-:93.1-137.7
Running [A0]: autfilt --complement 'lcr-i2-rjvy61' >'lcr-o0-rKKlxG'
Running [A1]: ltl2dstar -B --complement-input=yes 'lcr-i2-Musr0k' 'lcr-o1-LyAxtZ'
Performing sanity checks and gathering statistics...
No problem detected.
#+end_example
In this example, we generate 3 random Büchi automata (because
=ltl2dstar= expects Büchi automata as input) using [[file:randaut.org][=randaut=]], and pipe
them to =autcross=. For each of those automata, =autcross= display
the source location of that automaton (here =-= indicate that the
automaton is read from standard input, and this is followed by
=beginline.column-endline.colum= specifying the position of that
automaton in the input. If the automata had names, they would
be displayed as well.
Then, each tool is called using temporary files to exchange the
automata, and the resulting automata are then compared. The last line
specifies that no problem was detected.
To simplify the use of some known tools, a set of predefined
shorthands are available. Those can be listed with the
=--list-shorthands= option.
#+BEGIN_SRC sh :results verbatim :exports both
autcross --list-shorthands
#+END_SRC
#+RESULTS:
#+begin_example
If a COMMANDFMT does not use any %-sequence, and starts with one of
the following words, then the string on the right is appended.
autfilt %H>%O
seminator %H>%O
ltl2dstar -B %H %O
nba2ldpa <%H>%O
Any {name} and directory component is skipped for the purpose of
matching those prefixes. So for instance
'{AF} ~/mytools/autfilt-2.4 --remove-fin'
will be changed into
'{AF} ~/mytools/autfilt-2.4 --remove-fin %H>%O'
#+end_example
What this implies is our previous example could be shortened to:
#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes'
#+END_SRC
* Getting statistics
Detailed statistics about the result of each translation, and the
product of that resulting automaton with the random state-space, can
be obtained using the =--csv=FILE= option.
** CSV output
Let's take our example and modify it in two ways. First we pass a
=--name= option to =randaut= to give each automaton a name (in
=randaut=, =%L= denotes the serial number of the automaton); this is
mostly a cosmetic change, so that =autcross= will display names.
Second, we pass a =--csv= option to =autcross= to save statistics in a
file.
#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports results
randaut -B -n 3 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --csv=autcross.csv 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
-:1.1-46.7 automaton 0
Running [A0]: autfilt --complement 'lcr-i0-QHReWu'>'lcr-o0-0eTOmZ'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-jsoPPt' 'lcr-o1-66bQiY'
Performing sanity checks and gathering statistics...
-:47.1-94.7 automaton 1
Running [A0]: autfilt --complement 'lcr-i1-IubpMs'>'lcr-o0-dfmYfX'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i1-13NXLr' 'lcr-o1-zSwXhW'
Performing sanity checks and gathering statistics...
-:95.1-140.7 automaton 2
Running [A0]: autfilt --complement 'lcr-i2-g5bDOq'>'lcr-o0-X71ilV'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i2-og1mUp' 'lcr-o1-QVurtU'
Performing sanity checks and gathering statistics...
No problem detected.
#+end_example
After this execution, the file =autcross.csv= contains the following:
#+BEGIN_SRC sh :results verbatim :exports results
cat autcross.csv
#+END_SRC
#+RESULTS:
: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating"
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"autfilt --complement","ok",0,0.0129685,2,27,95,108,3,2,0,0,0
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00202496,2,34,121,136,6,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"autfilt --complement","ok",0,0.0128458,2,58,216,232,3,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"ltl2dstar --complement-input=yes","ok",0,0.0026184,2,74,268,296,6,2,0,8,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"autfilt --complement","ok",0,0.0127144,2,21,69,84,2,4,0,20,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"ltl2dstar --complement-input=yes","ok",0,0.00180888,2,24,74,96,2,4,0,35,0
This file can then be loaded in any spreadsheet or statistical application.
When computing such statistics, you should be aware that inputs for
which a tool failed to generate an automaton (e.g. it crashed, or it
was killed if you used =autcross='s =--timeout= option to limit run
time) will appear with empty columns at the end of the CSV line.
Those lines with missing data can be omitted with the =--omit-missing=
option.
However data for bogus automata are still included: as shown below
=autcross= will report inconsistencies between automata as errors, but
it does not try to guess who is incorrect.
The column names should be almost self-explanatory. See the [[./man/autcross.1.html][man page]]
for a description of the columns.
** Changing the name of the translators
By default, the names used in the CSV output to designate the
tools are the command specified on the command line. Like with
=ltlcross=, this can be adjusted by using a command specification of
the form ={short name}actual command=.
For instance
#+BEGIN_SRC sh :results verbatim :exports both
randaut -B -n 3 a b --name="automaton %L" |
autcross '{AF}autfilt --complement' '{L2D}ltl2dstar --complement-input=yes' --csv
#+END_SRC
#+RESULTS:
: "input.source","input.name","input.ap","input.states","input.edges","input.transitions","input.acc_sets","input.scc","input.nondetstates","input.nondeterministic","input.alternating","tool","exit_status","exit_code","time","output.ap","output.states","output.edges","output.transitions","output.acc_sets","output.scc","output.nondetstates","output.nondeterministic","output.alternating"
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"AF","ok",0,0.039722,2,27,95,108,3,2,0,0,0
: "-:1.1-46.7","automaton 0",2,10,26,26,1,1,6,0,0,"L2D","ok",0,0.00640371,2,34,121,136,6,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"AF","ok",0,0.0400776,2,58,216,232,3,2,0,9,0
: "-:47.1-94.7","automaton 1",2,10,28,28,1,1,4,0,0,"L2D","ok",0,0.00489558,2,74,268,296,6,2,0,20,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"AF","ok",0,0.0220585,2,21,69,84,2,4,0,7,0
: "-:95.1-140.7","automaton 2",2,10,26,26,1,2,6,0,0,"L2D","ok",0,0.00329786,2,24,74,96,2,4,0,23,0
* Language preserving transformation
By default =autcross= assumes that for a given input the automata
produced by all tools should be equivalent. However it does not
assume that those language should be equivalent to the input (it is
clearly not the case in our complementation test above).
If the transformation being tested does preserve the language of an
automaton, it is worth to pass the =--language-preserved= option to
=autfilt=. Doing so a bit like adding =cat %H>%O= as another tool: it
will also ensure that the output is equivalent to the input.
* Detecting problems
:PROPERTIES:
:CUSTOM_ID: checks
:END:
If a translator exits with a non-zero status code, or fails to output
an automaton =autcross= can read, and error will be displayed and the
result of the tool will be discarded.
Otherwise =autcross= performs equivalence checks between each pair of
automata. This is done in two steps. First, all produced automata
=A0=, =A1=, etc. are complemented: the complement automata are
named =Comp(A0)=, =Comp(A1)= etc. Second, =autcross= ensures
that =Ai*Comp(Aj)= is empty for all =i= and =j=.
If the =--language-preserved= option is passed, the =input= automaton
also participate to these equivalence checks.
To simulate a problem, let's compare pretend we want verify that
=autfilt --complement= preserves the input language (clearly it does
not, since it actually complement the language of the automaton).
#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 3 a b --name="automaton %L" |
autcross --language-preserved 'autfilt --complement'
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports output
randaut -B -n 3 a b --name="automaton %L" |
autcross --language-preserved 'autfilt --complement' 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
-:1.1-46.7 automaton 0
Running [A0]: autfilt --complement 'lcr-i0-3gRqrd'>'lcr-o0-ubUpHb'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
!a & !b; a & !b; cycle{!a & !b; a & !b; !a & b; !a & b; !a & !b; !a & b; !a & b; !a & !b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
!a & !b; !a & !b; cycle{!a & !b; !a & b; a & b}
-:47.1-94.7 automaton 1
Running [A0]: autfilt --complement 'lcr-i1-JxFi09'>'lcr-o0-oQGbj8'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
!a & b; cycle{a & !b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
!a & b; a & !b; cycle{!a & b; a & b}
-:95.1-140.7 automaton 2
Running [A0]: autfilt --complement 'lcr-i2-SQT7E6'>'lcr-o0-kWt404'
Performing sanity checks and gathering statistics...
error: A0*Comp(input) is nonempty; both automata accept the infinite word:
a & !b; !a & !b; cycle{a & !b; !a & b}
error: input*Comp(A0) is nonempty; both automata accept the infinite word:
cycle{!a & b; !a & b; !a & !b; a & !b; a & !b; !a & !b}
error: some error was detected during the above runs,
please search for 'error:' messages in the above trace.
#+end_example
Here, for each automaton, we get an example of word that is accepted
by the automaton and rejected by the input (i.e., accepted by
=Comp(input)=), as well as an example of word accepted by the input
but rejected by the automaton (i.e. accepted by =Comp(A0)=). Those
examples would not exit if the language was really preserved by the
tool.
Incoherence between the output of several tools (even with
=--language-preserved=) are reported in a similar way.
* Miscellaneous options
** =--stop-on-error=
The =--stop-on-error= option will cause =autcross= to abort on the
first detected error. This include failure to start some tool,
read its output, or failure to passe the sanity checks. Timeouts are
allowed.
One use for this option is when =autcross= is used in combination with
=randaut= to check tools on an infinite stream of formulas.
** =--save-bogus=FILENAME=
The =--save-bogus=FILENAME= will save any automaton for which an error
was detected (either some tool failed, or some problem was
detected using the resulting automata) in =FILENAME=. Again, timeouts
are not considered to be errors, and therefore not reported in this
file.
The main use for this feature is in conjunction with =randaut='s
generation of random formulas. For instance the following command
will run the translators on an infinite number of formulas, saving
any problematic formula in =bugs.ltl=.
** =--no-check=
The =--no-check= option disables all sanity checks. This
makes sense if you only care about the output of =--csv=.
** =--verbose=
The verbose option can be useful to troubleshoot problems or simply
follow the list of transformations and tests performed by =autcross=.
#+BEGIN_SRC sh :results verbatim :exports code
randaut -B -n 1 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports results
randaut -B -n 1 a b --name="automaton %L" |
autcross 'autfilt --complement' 'ltl2dstar --complement-input=yes' --verbose 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
-:1.1-46.7 automaton 0
info: input (10 st.,26 ed.,1 sets)
Running [A0]: autfilt --complement 'lcr-i0-oZm5P2'>'lcr-o0-O4P0IB'
Running [A1]: ltl2dstar --complement-input=yes -B 'lcr-i0-gEwlJa' 'lcr-o1-wSaHJJ'
info: collected automata:
info: A0 (27 st.,95 ed.,3 sets) deterministic complete
info: A1 (34 st.,121 ed.,6 sets) deterministic complete
Performing sanity checks and gathering statistics...
info: getting rid of any Fin acceptance...
info: A0 (27 st.,95 ed.,3 sets) -> (58 st.,203 ed.,2 sets)
info: Comp(A0) (27 st.,95 ed.,3 sets) -> (51 st.,188 ed.,1 sets)
info: A1 (34 st.,121 ed.,6 sets) -> (64 st.,228 ed.,3 sets)
info: Comp(A1) (34 st.,121 ed.,6 sets) -> (34 st.,121 ed.,1 sets)
info: check_empty A0*Comp(A1)
info: check_empty A1*Comp(A0)
No problem detected.
#+end_example
# LocalWords: utf autcross SETUPFILE html HOA neverclaim dstar's Nr
# LocalWords: autfilt dstar randaut lcr xZO urHakt mmkgH ABdm kMYrq
# LocalWords: kvBP lVlGfJ BexLFn rjvy rKKlxG Musr LyAxtZ shorthands
# LocalWords: COMMANDFMT seminator nba ldpa QHReWu eTOmZ jsoPPt ilV
# LocalWords: bQiY IubpMs dfmYfX NXLr zSwXhW bDOq og mUp QVurtU ap
# LocalWords: ok complementation Ai Aj gRqrd ubUpHb JxFi oQGbj SQT
# LocalWords: kWt Eo Xsc WXgCB vLwKMQ tI SXF qqlE KXplk ZFTCz PNY
# LocalWords: hUAK IjnFhD cWys ZqjdQh

6
doc/org/tools.org
View file

@ -47,13 +47,14 @@ corresponding commands are hidden.
- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-automata translators.
- [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL
formula.
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
and [[file:oaut.org][output]] interfaces.
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into
variants of Büchi automata.
- [[file:randaut.org][=randaut=]] Generate random \omega-automata.
- [[file:genaut.org][=genaut=]] Generate ω-automata from scalable patterns.
- [[file:autfilt.org][=autfilt=]] Filter, convert, and transform \omega-automata.
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
and [[file:oaut.org][output]] interfaces.
- [[file:autcross.org][=autcross=]] Cross-compare tools that process automata.
* Man pages
@ -63,6 +64,7 @@ automatically from the =--help= output of each tool, and often
completed with additional text (like examples or bibliography). For
convenience, you can browse their HTML versions:
[[./man/autcross.1.html][=autcross=]](1),
[[./man/autfilt.1.html][=autfilt=]](1),
[[./man/dstar2tgba.1.html][=dstar2tgba=]](1),
[[./man/genaut.1.html][=genaut=]](1),

2
tests/Makefile.am
View file

@ -293,6 +293,8 @@ TESTS_twa = \
core/ltlcross.test \
core/spotlbtt2.test \
core/ltlcross2.test \
core/autcross.test \
core/autcross2.test \
core/complementation.test \
core/randpsl.test \
core/cycles.test \

45
tests/core/autcross.test Executable file
View file

@ -0,0 +1,45 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
# Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77
randaut -n10 2 |
autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \
--csv=out.csv 2>stderr
# 5 lines per input automaton, and 1 "No problem detected" line.
test 51 = `wc -l < stderr`
grep -q 'sanity check' stderr
# --no-check still allows to build a CSV
randaut -n10 2 |
autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \
--csv=out2.csv --no-check 2>stderr
test 51 = `wc -l < stderr`
grep -q 'sanity check' stderr && exit 1
for f in out.csv out2.csv; do
sed 's/,[0-9]*\.[0-9]*,/,TIME,/' $f > _$f
done
diff _out.csv _out2.csv

30
tests/core/autcross2.test Executable file
View file

@ -0,0 +1,30 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
randaut -n10 2 | tee input |
autcross --language-preserve 'autfilt' 'autfilt --complement' \
--save-bogus=bogus.hoa 2>stderr && exit 1
cat stderr
# We should have 4 counterexample per input automaton
test 40 = `grep 'both automata accept the infinite word:' stderr | wc -l`
diff input bogus.hoa

8
tests/core/dra2dba.test
View file

@ -1,7 +1,7 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2014, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -329,5 +329,5 @@ Acc-Sig: +2
13
EOF
test `dstar2tgba -D in.dra --stats="%d:%s:%e"` = "1:23:143"
autcross 'dstar2tgba -D' --language-preserved -F in.dra --csv=out.csv
grep '3,23,143,184,1,2,0,0,0$' out.csv

4
tests/core/sbacc.test
View file

@ -163,7 +163,7 @@ test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`
# Test case from Thibaud Michaud. This used to fail, because sbacc()
# would remove acceptance marks from all rejecting SCCS...
cat >tm.hoa <<EOF
autcross 'autfilt --sbacc' --language-preserve <<EOF
HOA: v1
States: 5
Start: 1
@ -188,8 +188,6 @@ State: 4
[!2] 3 {1}
--END--
EOF
autfilt --sbacc tm.hoa > out.hoa
autfilt -q --equivalent-to out.hoa tm.hoa
# Tautological acceptances are converted to "t"
cat >taut.hoa <<EOF

6
tests/core/streett.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -110,6 +110,6 @@ State: 7 {0 2 4}
--END--
EOF
run 0 autfilt --tgba streett.hoa > out.hoa
autfilt -q --equivalent-to streett.hoa out.hoa
run 0 autcross --language-preserved \
'autfilt --tgba %H | tee out.hoa >%O' -F streett.hoa
grep 'generalized-Buchi 2' out.hoa