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

introduce is_inherently_weak_automaton()

* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh
(is_inherently_weak_automaton): New function.
(is_type_automaton): Adjust to implement the above and
set prop_inherently_weak().
* spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh:
Rewrite is_inherently_weak_scc() to not enumerate cycles.
* spot/bin/autfilt.cc: Add a --is-inherently-weak option.
* spot/tests/readsave.test: More tests.
* spot/tests/strength.test: Adjust expected output.
* doc/org/hoa.org: Adjust documentation of --check.
* NEWS: Mention those changes.
parent 0edb2ad0
......@@ -2,6 +2,8 @@ New in spot 1.99.6a (not yet released)
Command-line tools:
* autfilt has a new option: --is-inherently-weak.
Library:
* Installed headers now assume that they will be included as
......@@ -23,6 +25,10 @@ New in spot 1.99.6a (not yet released)
of $includedir/spot/iface/, so that installed and non-installed
directories can be used similarly.
* is_inherently_weak_automaton() is a new function, and
check_strength() has been modified to also check inherently weak
automata.
Python:
Documentation:
......
......@@ -666,7 +666,7 @@ particular:
| =stutter-sensitive= | trusted | yes | as stored | can be checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= |
| =colored= | ignored | no | checked | |
** Named properties
......@@ -942,4 +942,5 @@ bits section above), and property that are trivial to compute.
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.
automaton is stutter-invariant, unambiguous, (inherently) weak, and
terminal.
......@@ -89,6 +89,7 @@ enum {
OPT_IS_UNAMBIGUOUS,
OPT_IS_TERMINAL,
OPT_IS_WEAK,
OPT_IS_INHERENTLY_WEAK,
OPT_KEEP_STATES,
OPT_MASK_ACC,
OPT_MERGE,
......@@ -200,6 +201,8 @@ static const argp_option options[] =
"keep only terminal automata", 0 },
{ "is-weak", OPT_IS_WEAK, nullptr, 0,
"keep only weak automata", 0 },
{ "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
"keep only inherently weak automata", 0 },
{ "intersect", OPT_INTERSECT, "FILENAME", 0,
"keep automata whose languages have an non-empty intersection with"
" the automaton from FILENAME", 0 },
......@@ -268,6 +271,7 @@ 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_is_inherently_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() };
......@@ -379,6 +383,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_IS_EMPTY:
opt_is_empty = true;
break;
case OPT_IS_INHERENTLY_WEAK:
opt_is_inherently_weak = true;
break;
case OPT_IS_UNAMBIGUOUS:
opt_is_unambiguous = true;
break;
......@@ -594,6 +601,8 @@ namespace
matched &= is_terminal_automaton(aut);
else if (opt_is_weak)
matched &= is_weak_automaton(aut);
else if (opt_is_inherently_weak)
matched &= is_inherently_weak_automaton(aut);
if (opt->are_isomorphic)
matched &= opt->isomorphism_checker->is_isomorphic(aut);
if (opt_is_empty)
......
......@@ -737,6 +737,7 @@ State: 2 {0 1} [0] 2
EOF
test `$autfilt --is-weak -c input4` = 1
test `$autfilt --is-inherently-weak -c input4` = 1
test `$autfilt --is-terminal -c input4` = 0
$autfilt -H --small --high input4 >output4
......@@ -837,3 +838,62 @@ State: [0] 2 {0}
EOF
diff output6 expect6
cat >input7 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: Buchi
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0 1}
--END--
EOF
test `$autfilt -c --is-inherently-weak input7` = 1
test `$autfilt -c --is-weak input7` = 0
$autfilt --check input7 -H >output7
cat >expected7 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc inherently-weak
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0 1}
State: 2
--END--
EOF
diff output7 expected7
cat >input8 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: Buchi
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0}
--END--
EOF
test `$autfilt -c --is-inherently-weak input8` = 0
test `$autfilt -c --is-weak input8` = 0
......@@ -153,7 +153,7 @@ Start: 1
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
properties: deterministic inherently-weak
--BODY--
State: 0
[t] 1 {0}
......
......@@ -17,51 +17,26 @@
// 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 <spot/twaalgos/cycles.hh>
#include <spot/tl/formula.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/mask.hh>
namespace spot
{
namespace
bool
scc_has_rejecting_cycle(scc_info& map, unsigned scc)
{
// Look for a non-accepting cycle.
class weak_checker final : public enumerate_cycles
{
public:
bool result;
weak_checker(const scc_info& map)
: enumerate_cycles(map), result(true)
{
}
virtual bool
cycle_found(unsigned start) override
{
dfs_stack::const_reverse_iterator i = dfs_.rbegin();
acc_cond::mark_t acc = 0U;
for (;;)
{
acc |= aut_->edge_storage(i->succ).acc;
if (i->s == start)
break;
++i;
// The const cast is here to please old g++ versions.
// At least version 4.0 needs it.
assert(i != const_cast<const dfs_stack&>(dfs_).rend());
}
if (!aut_->acc().accepting(acc))
{
// We have found an non-accepting cycle, so the SCC is not
// weak.
result = false;
return false;
}
return true;
}
};
// We check that by cloning the SCC and complementing its
// acceptance condition.
auto aut = map.get_aut();
std::vector<bool> keep(aut->num_states(), false);
auto& states = map.states_of(scc);
for (auto s: states)
keep[s] = true;
auto sccaut = mask_keep_states(aut, keep, states.front());
sccaut->set_acceptance(sccaut->acc().num_sets(),
sccaut->get_acceptance().complement());
return !sccaut->is_empty();
}
bool
......@@ -70,11 +45,10 @@ namespace spot
// Weak SCCs are inherently weak.
if (is_weak_scc(map, scc))
return true;
// If the SCC is accepting, but one cycle is not, the SCC is not
// weak.
weak_checker w(map);
w.run(scc);
return w.result;
// If we reach this place, we now the SCC has an accepting cycle.
// The question is now to find whether is also contains a
// rejecting cycle.
return !scc_has_rejecting_cycle(map, scc);
}
bool
......
......@@ -26,6 +26,11 @@ namespace spot
/// \addtogroup twa_misc
/// @{
/// \brief Whether the SCC number \a scc in \a map has a rejecting
/// cycle.
SPOT_API bool
scc_has_rejecting_cycle(scc_info& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is inherently
/// weak.
///
......@@ -34,13 +39,6 @@ namespace spot
///
/// Note the terminal SCCs are also inherently weak with that
/// definition.
///
/// The absence of accepting cycle is easy to check (the scc_info
/// object can tell whether the SCC is non-accepting already).
/// Similarly, an SCC in which all transitions belong to all
/// acceptance sets is necessarily weak. For other accepting SCCs,
/// this function enumerates all cycles in the given SCC (it stops
/// if it find a non-accepting cycle).
SPOT_API bool
is_inherently_weak_scc(scc_info& map, unsigned scc);
......
......@@ -27,7 +27,7 @@ namespace spot
{
namespace
{
template <bool terminal, bool set = false>
template <bool terminal, bool inweak = false, bool set = false>
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.
......@@ -36,6 +36,7 @@ namespace spot
si = new scc_info(aut);
si->determine_unknown_acceptance();
bool is_inweak = true;
bool is_weak = true;
bool is_term = true;
unsigned n = si->scc_count();
......@@ -45,21 +46,32 @@ namespace spot
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 (is_weak)
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)
{
is_weak = false;
if (!inweak)
goto exit;
}
}
if (!is_weak && si->is_accepting_scc(i))
{
assert(inweak);
if (scc_has_rejecting_cycle(*si, i))
{
if (first)
{
first = false;
m = t.acc;
}
else if (m != t.acc)
{
is_weak = false;
goto exit;
}
is_inweak = false;
break;
}
}
if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i))
{
is_term = false;
......@@ -75,7 +87,10 @@ namespace spot
if (terminal)
aut->prop_terminal(is_term && is_weak);
aut->prop_weak(is_weak);
aut->prop_inherently_weak(is_inweak);
}
if (inweak)
return is_inweak;
return is_weak && is_term;
}
}
......@@ -96,9 +111,17 @@ namespace spot
si));
}
bool
is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
return (aut->prop_inherently_weak() ||
is_type_automaton<false, true>
(std::const_pointer_cast<twa_graph>(aut), si));
}
void check_strength(const twa_graph_ptr& aut, scc_info* si)
{
is_type_automaton<true, true>(aut, si);
is_type_automaton<true, true, true>(aut, si);
}
bool is_safety_mwdba(const const_twa_graph_ptr& aut)
......
......@@ -38,7 +38,7 @@ namespace spot
/// \brief Whether an automaton is weak.
///
/// An automaton is weak if if any given SCC, all transitions belong
/// An automaton is weak if in any given SCC, all transitions belong
/// to the same acceptance sets.
///
/// \param aut the automaton to check
......@@ -48,6 +48,19 @@ namespace spot
SPOT_API bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
/// \brief Whether an automaton is inherently weak.
///
/// An automaton is inherently weak if in any given SCC, there
/// are only accepting cycles, or only rejecting cycles.
///
/// \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_inherently_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