Commit f4cf0f40 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: Add --is-terminal and --is-weak.

Fixes #47.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(is_weak_automaton): New function.
(is_terminal_automaton): Generalize slightly.
* src/bin/autfilt.cc: Add options --is-terminal and --is-weak.
* src/tests/readsave.test: Add a test.
* NEWS: Update.
parent 81cfa05a
New in spot 1.99.5a (not yet released)
Command-line tools:
* autfilt has two now filters: --is-weak and --is-terminal.
Library:
* Properties of automata (like the "properties:" line of the HOA
......
......@@ -57,6 +57,7 @@
#include "twaalgos/cleanacc.hh"
#include "twaalgos/dtgbasat.hh"
#include "twaalgos/complement.hh"
#include "twaalgos/strength.hh"
static const char argp_program_doc[] ="\
Convert, transform, and filter omega-automata.\v\
......@@ -85,6 +86,8 @@ enum {
OPT_IS_DETERMINISTIC,
OPT_IS_EMPTY,
OPT_IS_UNAMBIGUOUS,
OPT_IS_TERMINAL,
OPT_IS_WEAK,
OPT_KEEP_STATES,
OPT_MASK_ACC,
OPT_MERGE,
......@@ -189,6 +192,10 @@ static const argp_option options[] =
"keep automata with an empty language", 0 },
{ "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
"keep only unambiguous automata", 0 },
{ "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
"keep only terminal automata", 0 },
{ "is-weak", OPT_IS_WEAK, nullptr, 0,
"keep only weak automata", 0 },
{ "intersect", OPT_INTERSECT, "FILENAME", 0,
"keep automata whose languages have an non-empty intersection with"
" the automaton from FILENAME", 0 },
......@@ -255,6 +262,8 @@ static bool opt_merge = false;
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
static bool opt_is_unambiguous = false;
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
static bool opt_invert = false;
static range opt_states = { 0, std::numeric_limits<int>::max() };
static range opt_edges = { 0, std::numeric_limits<int>::max() };
......@@ -365,6 +374,12 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_IS_UNAMBIGUOUS:
opt_is_unambiguous = true;
break;
case OPT_IS_TERMINAL:
opt_is_terminal = true;
break;
case OPT_IS_WEAK:
opt_is_weak = true;
break;
case OPT_MERGE:
opt_merge = true;
break;
......@@ -567,6 +582,10 @@ namespace
matched &= is_deterministic(aut);
else if (opt_is_unambiguous)
matched &= is_unambiguous(aut);
if (opt_is_terminal)
matched &= is_terminal_automaton(aut);
else if (opt_is_weak)
matched &= is_weak_automaton(aut);
if (opt->are_isomorphic)
matched &= opt->isomorphism_checker->is_isomorphic(aut);
if (opt_is_empty)
......
......@@ -51,6 +51,8 @@ EOF
run 0 $autfilt --hoa input > stdout
diff stdout input
test `$autfilt -c --is-weak input` = 0
# Transition merging
cat >input <<\EOF
HOA: v1
......@@ -714,6 +716,9 @@ State: 2 {0 1} [0] 2
--END--
EOF
test `$autfilt --is-weak -c input4` = 1
test `$autfilt --is-terminal -c input4` = 0
$autfilt -H --small --high input4 >output4
$autfilt -H --small input4 >output4b
$autfilt -H --high input4 >output4c
......@@ -742,6 +747,12 @@ diff output4b expect4
diff output4c expect4
$autfilt -Hv --small input4 >output5
test `$autfilt --is-weak -c output4` = 1
test `$autfilt --is-terminal -c output4` = 0
sed 's/\[0\]/[t]/g' expect4 > output4d
test `$autfilt --is-terminal -c output4d` = 1
cat >expect5<<EOF
HOA: v1
......
......@@ -19,49 +19,68 @@
#include "strength.hh"
#include "misc/hash.hh"
#include "isweakscc.hh"
#include <deque>
namespace spot
{
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
namespace
{
if (aut->prop_terminal())
return true;
// Create an scc_info if the user did not give one to us.
bool need_si = !si;
if (need_si)
si = new scc_info(aut);
si->determine_unknown_acceptance();
template <bool terminal>
bool is_type_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
// Create an scc_info if the user did not give one to us.
bool need_si = !si;
if (need_si)
si = new scc_info(aut);
si->determine_unknown_acceptance();
bool result = true;
bool result = true;
unsigned n = si->scc_count();
for (unsigned i = 0; i < n; ++i)
{
if (si->is_trivial(i))
continue;
bool first = true;
acc_cond::mark_t m = 0U;
for (auto src: si->states_of(i))
for (auto& t: aut->out(src))
if (si->scc_of(t.dst) == i)
{
if (first)
{
first = false;
m = t.acc;
}
else if (m != t.acc)
{
result = false;
goto exit;
}
}
if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i))
{
result = false;
break;
}
}
exit:
if (need_si)
delete si;
return result;
}
}
for (auto& scc: *si)
{
if (scc.is_rejecting())
continue;
// Accepting SCCs should have only one state.
auto& st = scc.states();
if (st.size() != 1)
{
result = false;
break;
}
// The state should have only one edge that is a
// self-loop labelled by true.
auto src = st.front();
auto out = aut->out(src);
auto it = out.begin();
assert(it != out.end());
result =
(it->cond == bddtrue) && (it->dst == src) && (++it == out.end());
if (!result)
break;
}
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return aut->prop_terminal() || is_type_automaton<true>(aut, si);
}
if (need_si)
delete si;
return result;
bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return aut->prop_weak() || is_type_automaton<false>(aut, si);
}
bool is_safety_mwdba(const const_twa_graph_ptr& aut)
......
......@@ -25,9 +25,8 @@ namespace spot
{
/// \brief Whether an automaton is terminal.
///
/// An automaton is terminal if any accepting path ends on an
/// accepting state with only one transition that is a self-loop
/// labelled by true.
/// An automaton is terminal if it is weak, and all accepting SCCs
/// are complete.
///
/// \param aut the automaton to check
///
......@@ -36,6 +35,19 @@ namespace spot
SPOT_API bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
/// \brief Whether an automaton is weak.
///
/// An automaton is weak if if any given SCC, all transitions belong
/// to the same acceptance sets.
///
/// \param aut the automaton to check
///
/// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise).
SPOT_API bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
/// \brief Whether a minimized WDBA represents a safety property.
///
/// A minimized WDBA (as returned by a successful run of
......
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