From 73621e8f175a72da4c2553970f66512e6dd34f78 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 May 2016 15:31:15 +0200 Subject: [PATCH] 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. --- NEWS | 4 ++++ spot/twaalgos/hoa.cc | 5 +++-- spot/twaalgos/isdet.cc | 4 +++- spot/twaalgos/isdet.hh | 8 ++++++-- spot/twaalgos/strength.cc | 15 +++++++++++---- spot/twaalgos/strength.hh | 16 ++++++++++++++-- tests/core/readsave.test | 8 ++++++++ 7 files changed, 49 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 6db3b49f0..ab031dddb 100644 --- a/NEWS +++ b/NEWS @@ -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 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 methods introduced to fix some of the bugs below. diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 5926df698..590b2bfc0 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -484,9 +484,10 @@ namespace spot prop(" weak"); if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true)) 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"); - 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"); if (v1_1 && !aut->prop_inherently_weak()) prop(" !inherently-weak"); diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 632f20a1c..afae5348b 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -66,7 +66,9 @@ namespace spot trival d = aut->prop_deterministic(); if (d.is_known()) return d.is_true(); - return !count_nondet_states_aux(aut); + bool res = !count_nondet_states_aux(aut); + std::const_pointer_cast(aut)->prop_deterministic(res); + return res; } bool diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index 4ddda5efc..a15792ccd 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -39,6 +39,10 @@ namespace spot /// This function is more efficient than count_nondet_states() when /// the automaton is nondeterministic, because it can return before /// 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 is_deterministic(const const_twa_graph_ptr& aut); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 09c29b115..1c4fb6524 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -102,7 +102,10 @@ namespace spot trival v = aut->prop_terminal(); if (v.is_known()) return v.is_true(); - return is_type_automaton(std::const_pointer_cast(aut), si); + bool res = + is_type_automaton(std::const_pointer_cast(aut), si); + std::const_pointer_cast(aut)->prop_terminal(res); + return res; } bool @@ -111,8 +114,10 @@ namespace spot trival v = aut->prop_weak(); if (v.is_known()) return v.is_true(); - return is_type_automaton(std::const_pointer_cast(aut), - si); + bool res = + is_type_automaton(std::const_pointer_cast(aut), si); + std::const_pointer_cast(aut)->prop_weak(res); + return res; } bool @@ -121,8 +126,10 @@ namespace spot trival v = aut->prop_inherently_weak(); if (v.is_known()) return v.is_true(); - return is_type_automaton + bool res = is_type_automaton (std::const_pointer_cast(aut), si); + std::const_pointer_cast(aut)->prop_inherently_weak(res); + return res; } void check_strength(const twa_graph_ptr& aut, scc_info* si) diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index e114faf16..dd0a426dc 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche -// et Développement de l'Epita (LRDE) +// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de +// Recherche et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -32,6 +32,10 @@ namespace spot /// /// \param sm an scc_info object for the automaton if available (it /// 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 is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); @@ -45,6 +49,10 @@ namespace spot /// /// \param sm an scc_info object for the automaton if available (it /// 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 is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); @@ -57,6 +65,10 @@ namespace spot /// /// \param sm an scc_info object for the automaton if available (it /// 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 is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 83617a021..facfe80db 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -49,6 +49,14 @@ diff stdout input test `autfilt -c --is-weak input` = 0 +autfilt -H1.1 -v --is-weak input | grep properties: | tee props +cat >expected.props <input <<\EOF HOA: v1 -- GitLab