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

bin: add a --check option for automata outputs

This currently only allows extra check for stutter invariance.

* src/bin/common_aoutput.cc: Add check option,
and test stutter invariance.
* src/twaalgos/stutter.cc, src/twaalgos/stutter.hh
(check_stutter_invariance): New function.
* src/tests/stutter-tgba.test: Test it.
parent fa37bc5f
......@@ -19,6 +19,7 @@
#include "common_sys.hh"
#include "error.h"
#include "argmatch.h"
#include "common_aoutput.hh"
#include "common_post.hh"
......@@ -31,6 +32,7 @@
#include "twaalgos/lbtt.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/neverclaim.hh"
#include "twaalgos/stutter.hh"
automaton_format_t automaton_format = Dot;
static const char* opt_dot = nullptr;
......@@ -39,12 +41,35 @@ static const char* hoa_opt = nullptr;
const char* opt_name = nullptr;
static const char* opt_output = nullptr;
static const char* stats = "";
enum check_type
{
check_stutter = (1 << 0),
check_all = -1U,
};
static char const *const check_args[] =
{
"stutter-invariant", "stuttering-invariant",
"stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive",
"all",
0
};
static check_type const check_types[] =
{
check_stutter, check_stutter,
check_stutter, check_stutter,
check_stutter, check_stutter,
check_all
};
ARGMATCH_VERIFY(check_args, check_types);
unsigned opt_check = 0U;
enum {
OPT_DOT = 1,
OPT_LBTT,
OPT_NAME,
OPT_STATS,
OPT_CHECK,
};
static const argp_option options[] =
......@@ -88,6 +113,10 @@ static const argp_option options[] =
"(ignored with --lbtt or --spin)", 0 },
{ "stats", OPT_STATS, "FORMAT", 0,
"output statistics about the automaton", 0 },
{ "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL,
"test for the additional property PROP and output the result "
"in the HOA format (implies -H). PROP may be any prefix of "
"'all' (default), or 'stutter-invariant'.", 0 },
{ 0, 0, 0, 0, 0, 0 }
};
......@@ -190,6 +219,13 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
case 'o':
opt_output = arg;
break;
case OPT_CHECK:
automaton_format = Hoa;
if (arg)
opt_check |= XARGMATCH("--check", arg, check_args, check_types);
else
opt_check |= check_all;
break;
case OPT_DOT:
automaton_format = Dot;
opt_dot = arg;
......@@ -244,6 +280,12 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
double time,
const spot::const_hoa_aut_ptr& haut)
{
if (opt_check)
{
if (opt_check & check_stutter)
check_stutter_invariance(aut, f);
}
// Name the output automaton.
if (opt_name)
{
......
......@@ -70,4 +70,11 @@ State: 2
--END--
EOF
run 0 $ltl2tgba -H 'F(a & X(!a & b))' > input
grep stutter-invariant input && exit 1
run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
grep stutter-invariant input.2
run 0 $autfilt --check=stutter input > input.2
grep stutter-invariant input.2
diff output expected
......@@ -29,6 +29,8 @@
#include "ltlvisit/remove_x.hh"
#include "twaalgos/product.hh"
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/isdet.hh"
#include "twaalgos/dtgbacomp.hh"
#include "twa/twaproduct.hh"
#include "twa/bddprint.hh"
#include <deque>
......@@ -637,4 +639,36 @@ namespace spot
SPOT_UNREACHABLE();
}
}
bool
check_stutter_invariance(const twa_graph_ptr& aut, const ltl::formula* f)
{
bool is_stut = aut->is_stutter_invariant();
if (is_stut)
return is_stut;
twa_graph_ptr neg = nullptr;
if (f)
{
auto* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
neg = translator(aut->get_dict()).run(nf);
nf->destroy();
}
else
{
// If the automaton is deterministic, we
// know how to complement it.
aut->prop_deterministic(is_deterministic(aut));
if (!aut->is_deterministic())
return false;
neg = dtgba_complement(aut);
}
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
std::move(neg), get_all_ap(aut));
if (is_stut)
aut->prop_stutter_invariant(is_stut);
return is_stut;
}
}
......@@ -57,4 +57,13 @@ namespace spot
is_stutter_invariant(twa_graph_ptr&& aut_f,
twa_graph_ptr&& aut_nf, bdd aps,
int algo = 0);
/// \brief Check whether \a aut is stutter-invariant
///
/// This procedure only works if \a aut is deterministic, or if the
/// equivalent formula \a f is given. The stutter-invariant property
/// of the automaton is updated and also returned.
SPOT_API bool
check_stutter_invariance(const twa_graph_ptr& aut,
const ltl::formula* f = nullptr);
}
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