Commit 73621e8f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

record properties as side-effect of is_deterministic() / is_weak() / ...

Fixes #165.

* spot/twaalgos/isdet.cc, spot/twaalgos/strength.cc: Here.
* spot/twaalgos/isdet.hh, spot/twaalgos/strength.hh, NEWS: Document it.
* spot/twaalgos/hoa.cc: Fix output of negated properties.
* tests/core/readsave.test: New test case.
parent b708ab77
...@@ -49,6 +49,10 @@ New in spot 2.0a (not yet released) ...@@ -49,6 +49,10 @@ New in spot 2.0a (not yet released)
is still the default, but we plan to default to version 1.1 in the is still the default, but we plan to default to version 1.1 in the
future. future.
* is_deterministic(), is_terminal(), is_weak(), and
is_inherently_weak() will update the corresponding properties of
the automaton as a side-effect of their check.
* twa::unregister_ap() and twa_graph::remove_unused_ap() are new * twa::unregister_ap() and twa_graph::remove_unused_ap() are new
methods introduced to fix some of the bugs below. methods introduced to fix some of the bugs below.
......
...@@ -484,9 +484,10 @@ namespace spot ...@@ -484,9 +484,10 @@ namespace spot
prop(" weak"); prop(" weak");
if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true)) if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
prop(" inherently-weak"); prop(" inherently-weak");
if (v1_1 && !aut->prop_terminal() && (aut->prop_weak() || verbose)) if (v1_1 && !aut->prop_terminal() && (verbose || aut->prop_weak() != false))
prop(" !terminal"); prop(" !terminal");
if (v1_1 && !aut->prop_weak() && (aut->prop_inherently_weak() || verbose)) if (v1_1 && !aut->prop_weak() && (verbose ||
aut->prop_inherently_weak() != false))
prop(" !weak"); prop(" !weak");
if (v1_1 && !aut->prop_inherently_weak()) if (v1_1 && !aut->prop_inherently_weak())
prop(" !inherently-weak"); prop(" !inherently-weak");
......
...@@ -66,7 +66,9 @@ namespace spot ...@@ -66,7 +66,9 @@ namespace spot
trival d = aut->prop_deterministic(); trival d = aut->prop_deterministic();
if (d.is_known()) if (d.is_known())
return d.is_true(); return d.is_true();
return !count_nondet_states_aux<false>(aut); bool res = !count_nondet_states_aux<false>(aut);
std::const_pointer_cast<twa_graph>(aut)->prop_deterministic(res);
return res;
} }
bool bool
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -39,6 +39,10 @@ namespace spot ...@@ -39,6 +39,10 @@ namespace spot
/// This function is more efficient than count_nondet_states() when /// This function is more efficient than count_nondet_states() when
/// the automaton is nondeterministic, because it can return before /// the automaton is nondeterministic, because it can return before
/// the entire automaton has been explored. /// the entire automaton has been explored.
///
/// In addition to returning the result as a Boolean, this will set
/// the prop_deterministic() property of the automaton as a
/// side-effect, so further calls will return in constant-time.
SPOT_API bool SPOT_API bool
is_deterministic(const const_twa_graph_ptr& aut); is_deterministic(const const_twa_graph_ptr& aut);
......
...@@ -102,7 +102,10 @@ namespace spot ...@@ -102,7 +102,10 @@ namespace spot
trival v = aut->prop_terminal(); trival v = aut->prop_terminal();
if (v.is_known()) if (v.is_known())
return v.is_true(); return v.is_true();
return is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si); bool res =
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut), si);
std::const_pointer_cast<twa_graph>(aut)->prop_terminal(res);
return res;
} }
bool bool
...@@ -111,8 +114,10 @@ namespace spot ...@@ -111,8 +114,10 @@ namespace spot
trival v = aut->prop_weak(); trival v = aut->prop_weak();
if (v.is_known()) if (v.is_known())
return v.is_true(); return v.is_true();
return is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut), bool res =
si); is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut), si);
std::const_pointer_cast<twa_graph>(aut)->prop_weak(res);
return res;
} }
bool bool
...@@ -121,8 +126,10 @@ namespace spot ...@@ -121,8 +126,10 @@ namespace spot
trival v = aut->prop_inherently_weak(); trival v = aut->prop_inherently_weak();
if (v.is_known()) if (v.is_known())
return v.is_true(); return v.is_true();
return is_type_automaton<false, true> bool res = is_type_automaton<false, true>
(std::const_pointer_cast<twa_graph>(aut), si); (std::const_pointer_cast<twa_graph>(aut), si);
std::const_pointer_cast<twa_graph>(aut)->prop_inherently_weak(res);
return res;
} }
void check_strength(const twa_graph_ptr& aut, scc_info* si) void check_strength(const twa_graph_ptr& aut, scc_info* si)
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche // Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
// et Développement de l'Epita (LRDE) // Recherche et Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -32,6 +32,10 @@ namespace spot ...@@ -32,6 +32,10 @@ namespace spot
/// ///
/// \param sm an scc_info object for the automaton if available (it /// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise). /// will be built otherwise).
///
/// In addition to returning the result as a Boolean, this will set
/// the prop_terminal() property of the automaton as a side-effect,
/// so further calls will return in constant-time.
SPOT_API bool SPOT_API bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
...@@ -45,6 +49,10 @@ namespace spot ...@@ -45,6 +49,10 @@ namespace spot
/// ///
/// \param sm an scc_info object for the automaton if available (it /// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise). /// will be built otherwise).
///
/// In addition to returning the result as a Boolean, this will set
/// the prop_weak() property of the automaton as a side-effect,
/// so further calls will return in constant-time.
SPOT_API bool SPOT_API bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
...@@ -57,6 +65,10 @@ namespace spot ...@@ -57,6 +65,10 @@ namespace spot
/// ///
/// \param sm an scc_info object for the automaton if available (it /// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise). /// will be built otherwise).
///
/// In addition to returning the result as a Boolean, this will set
/// the prop_inherently_weak() property of the automaton as a
/// side-effect, so further calls will return in constant-time.
SPOT_API bool SPOT_API bool
is_inherently_weak_automaton(const const_twa_graph_ptr& aut, is_inherently_weak_automaton(const const_twa_graph_ptr& aut,
scc_info* sm = nullptr); scc_info* sm = nullptr);
......
...@@ -49,6 +49,14 @@ diff stdout input ...@@ -49,6 +49,14 @@ diff stdout input
test `autfilt -c --is-weak input` = 0 test `autfilt -c --is-weak input` = 0
autfilt -H1.1 -v --is-weak input | grep properties: | tee props
cat >expected.props <<EOF
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic !weak
EOF
diff expected.props props
# Transition merging # Transition merging
cat >input <<\EOF cat >input <<\EOF
HOA: v1 HOA: v1
......
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