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

stutterize: fix sl2() to keep the correct properties

Combined with 87c2b291, this fixes #7.

* src/tgbaalgos/stutterize.cc: Call keep_props().
* src/tgbaalgos/closure.cc: Just specify the encoding.
* src/bin/autfilt.cc: Add a --instut=2 option.
* src/tgbatest/stutter.test: More test.
parent 314993b2
......@@ -97,16 +97,17 @@ static const argp_option options[] =
{ "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
"randomize states and transitions (specify 's' or 't' to "
"randomize only states or transitions)", 0 },
{ "instut", OPT_INSTUT, 0, 0, "allow more stuttering", 0 },
{ "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
"allow more stuttering (two possible algorithms)", 0 },
{ "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Filters:", 6 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
"keep automata that are isomorphic to the automaton in FILENAME", 0 },
{ "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 },
{ "unique", 'u', 0, 0,
"do not output the same automaton twice (same in the sense that they "\
"are isomorphic)", 0 },
{ "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 },
{ "is-complete", OPT_IS_COMPLETE, 0, 0,
"the automaton is complete", 0 },
{ "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
......@@ -160,7 +161,7 @@ static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
static int opt_max_count = -1;
static bool opt_destut = false;
static bool opt_instut = false;
static char opt_instut = 0;
static bool opt_is_empty = false;
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
......@@ -235,7 +236,12 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case OPT_INSTUT:
opt_instut = true;
if (!arg || (arg[0] == '1' && arg[1] == 0))
opt_instut = 1;
else if (arg[0] == '2' && arg[1] == 0)
opt_instut = 2;
else
error(2, 0, "unknown argument for --instut: %s", arg);
break;
case OPT_DESTUT:
opt_destut = true;
......@@ -375,8 +381,10 @@ namespace
if (opt_destut)
aut = spot::closure(std::move(aut));
if (opt_instut)
if (opt_instut == 1)
aut = spot::sl(std::move(aut));
else if (opt_instut == 2)
aut = spot::sl2(std::move(aut));
if (opt_product)
aut = spot::product(std::move(aut), opt_product);
......
// Copyright (C) 2014 Laboratoire de Recherche et Développement
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche
// Copyright (C) 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -152,34 +149,37 @@ namespace spot
atomic_propositions = get_all_ap(a);
unsigned num_states = a->num_states();
unsigned num_transitions = a->num_transitions();
for (unsigned state = 0; state < num_states; ++state)
for (unsigned src = 0; src < num_states; ++src)
{
auto trans = a->out(state);
auto trans = a->out(src);
for (auto it = trans.begin(); it != trans.end()
&& it.trans() <= num_transitions; ++it)
{
if (it->dst != state)
{
bdd all = it->cond;
while (all != bddfalse)
{
unsigned dst = it->dst;
bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
unsigned tmp = a->new_state();
unsigned i = a->new_transition(state, tmp, one,
it->acc);
assert(i > num_transitions);
i = a->new_transition(tmp, tmp, one, 0U);
assert(i > num_transitions);
i = a->new_transition(tmp, dst, one,
it->acc);
assert(i > num_transitions);
all -= one;
}
}
}
if (it->dst != src)
{
bdd all = it->cond;
while (all != bddfalse)
{
unsigned dst = it->dst;
bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
unsigned tmp = a->new_state();
unsigned i = a->new_transition(src, tmp, one, it->acc);
assert(i > num_transitions);
i = a->new_transition(tmp, tmp, one, 0U);
assert(i > num_transitions);
// No acceptance here to preserve the state-based property.
i = a->new_transition(tmp, dst, one, 0U);
assert(i > num_transitions);
all -= one;
}
}
}
if (num_states != a->num_states())
a->prop_keep({true, // state_based
true, // single_acc
false, // inherently_weak
false, // deterministic
});
a->merge_transitions();
return a;
}
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014 Laboratoire de Recherche et Développement
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -36,3 +36,13 @@ $ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa
$autfilt pos.hoa --product neg.hoa -H > prod.hoa
$autfilt --is-empty prod.hoa -q && exit 1
$autfilt --states=12 prod.hoa -q
# Check for issue #7.
#
# We just run those without checking the output, it is enough to
# trigger assertions in the HOA output routines.
run 0 ../../bin/ltl2tgba -H 'X(a U b)' > det.hoa
run 0 ../../bin/autfilt --destut det.hoa -H
run 0 ../../bin/autfilt --instut=1 det.hoa -H
run 0 ../../bin/autfilt --instut=2 det.hoa -H
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