diff --git a/NEWS b/NEWS
index 6ce684802..391522b0c 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,12 @@ New in spot 1.99.5a (not yet released)
* autfilt has two now filters: --is-weak and --is-terminal.
+ * All tools that output HOA files accept a --check=strength option
+ to request automata to be marked as "weak" or "terminal" as
+ appropriate. Without this option, these properties may only be
+ set as a side-effect of running transformations that use this
+ information.
+
Library:
* Properties of automata (like the "properties:" line of the HOA
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index 92e3891b8..b3184986d 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -591,8 +591,8 @@ particular:
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
-| =terminal= | trusted | yes | as stored | |
-| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | |
+| =terminal= | trusted | yes | as stored | can be re-checked with =--check=strength= |
+| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be re-checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =colored= | ignored | no | checked | |
@@ -867,6 +867,6 @@ When an automaton is output in HOA format, the =property:= lines
includes property registered into the automaton (see the Property
bits section above), and property that are trivial to compute.
-Command-line with a HOA output all have a =--check= option that can be
-used to request additional checks such as testing whether the
-automaton is stutter-invariant, or unambiguous.
+Command-line tools with a HOA output all have a =--check= option that
+can be used to request additional checks such as testing whether the
+automaton is stutter-invariant, unambiguous, weak, and terminal.
diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc
index 65b063039..ac6ee52f1 100644
--- a/src/bin/common_aoutput.cc
+++ b/src/bin/common_aoutput.cc
@@ -33,6 +33,7 @@
#include "twaalgos/neverclaim.hh"
#include "twaalgos/stutter.hh"
#include "twaalgos/isunamb.hh"
+#include "twaalgos/strength.hh"
automaton_format_t automaton_format = Dot;
static const char* opt_dot = nullptr;
@@ -46,6 +47,7 @@ enum check_type
{
check_unambiguous = (1 << 0),
check_stutter = (1 << 1),
+ check_strength = (1 << 2),
check_all = -1U,
};
static char const *const check_args[] =
@@ -54,6 +56,7 @@ static char const *const check_args[] =
"stutter-invariant", "stuttering-invariant",
"stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive",
+ "strength", "weak", "terminal",
"all",
nullptr
};
@@ -63,6 +66,7 @@ static check_type const check_types[] =
check_stutter, check_stutter,
check_stutter, check_stutter,
check_stutter, check_stutter,
+ check_strength, check_strength, check_strength,
check_all
};
ARGMATCH_VERIFY(check_args, check_types);
@@ -121,7 +125,8 @@ static const argp_option options[] =
{ "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), 'unambiguous', or 'stutter-invariant'.", 0 },
+ "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
+ 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
};
@@ -299,9 +304,11 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
if (opt_check)
{
if (opt_check & check_stutter)
- check_stutter_invariance(aut, f);
+ spot::check_stutter_invariance(aut, f);
if (opt_check & check_unambiguous)
spot::check_unambiguous(aut);
+ if (opt_check & check_strength)
+ spot::check_strength(aut);
}
// Name the output automaton.
diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am
index 05ab8a19b..51b9a0840 100644
--- a/src/tests/Makefile.am
+++ b/src/tests/Makefile.am
@@ -229,6 +229,7 @@ TESTS_twa = \
uniq.test \
sbacc.test \
stutter-tgba.test \
+ strength.test \
emptchk.test \
emptchke.test \
dfs.test \
diff --git a/src/tests/strength.test b/src/tests/strength.test
new file mode 100755
index 000000000..4d422a417
--- /dev/null
+++ b/src/tests/strength.test
@@ -0,0 +1,166 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015 Laboratoire de Recherche et Developpement
+# de l'Epita
+#
+# 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 .
+
+. ./defs
+
+set -e
+
+autfilt=../../bin/autfilt
+
+cat >in <expected <
- bool is_type_automaton(const const_twa_graph_ptr& aut, scc_info* si)
+ template
+ bool is_type_automaton(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;
@@ -35,7 +35,8 @@ namespace spot
si = new scc_info(aut);
si->determine_unknown_acceptance();
- bool result = true;
+ bool is_weak = true;
+ bool is_term = true;
unsigned n = si->scc_count();
for (unsigned i = 0; i < n; ++i)
{
@@ -54,33 +55,49 @@ namespace spot
}
else if (m != t.acc)
{
- result = false;
+ is_weak = false;
goto exit;
}
}
if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i))
{
- result = false;
- break;
+ is_term = false;
+ if (!set)
+ break;
}
}
exit:
if (need_si)
delete si;
- return result;
+ if (set)
+ {
+ if (terminal)
+ aut->prop_terminal(is_term && is_weak);
+ aut->prop_weak(is_weak);
+ }
+ return is_weak && is_term;
}
}
bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
- return aut->prop_terminal() || is_type_automaton(aut, si);
+ return (aut->prop_terminal() ||
+ is_type_automaton(std::const_pointer_cast(aut),
+ si));
}
bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
- return aut->prop_weak() || is_type_automaton(aut, si);
+ return (aut->prop_weak() ||
+ is_type_automaton(std::const_pointer_cast(aut),
+ si));
+ }
+
+ void check_strength(const twa_graph_ptr& aut, scc_info* si)
+ {
+ is_type_automaton(aut, si);
}
bool is_safety_mwdba(const const_twa_graph_ptr& aut)
diff --git a/src/twaalgos/strength.hh b/src/twaalgos/strength.hh
index 6bc197cb1..137129f1a 100644
--- a/src/twaalgos/strength.hh
+++ b/src/twaalgos/strength.hh
@@ -58,4 +58,14 @@ namespace spot
SPOT_API bool
is_safety_mwdba(const const_twa_graph_ptr& aut);
+ /// \brief Whether an automaton is weak or terminal.
+ ///
+ /// This sets the "weak" and "terminal" property as appropriate.
+ ///
+ /// \param aut the automaton to check
+ ///
+ /// \param sm an scc_info object for the automaton if available (it
+ /// will be built otherwise).
+ SPOT_API void
+ check_strength(const twa_graph_ptr& aut, scc_info* sm = nullptr);
}