diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 2312c1f52..8cabe4510 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -32,6 +32,7 @@ #include "twaalgos/hoa.hh" #include "twaalgos/neverclaim.hh" #include "twaalgos/stutter.hh" +#include "twaalgos/isunamb.hh" automaton_format_t automaton_format = Dot; static const char* opt_dot = nullptr; @@ -42,11 +43,13 @@ static const char* opt_output = nullptr; static const char* stats = ""; enum check_type { - check_stutter = (1 << 0), + check_unambiguous = (1 << 0), + check_stutter = (1 << 1), check_all = -1U, }; static char const *const check_args[] = { + "unambiguous", "stutter-invariant", "stuttering-invariant", "stutter-insensitive", "stuttering-insensitive", "stutter-sensitive", "stuttering-sensitive", @@ -55,6 +58,7 @@ static char const *const check_args[] = }; static check_type const check_types[] = { + check_unambiguous, check_stutter, check_stutter, check_stutter, check_stutter, check_stutter, check_stutter, @@ -115,7 +119,7 @@ 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), or 'stutter-invariant'.", 0 }, + "'all' (default), 'unambiguous', or 'stutter-invariant'.", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -283,6 +287,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, { if (opt_check & check_stutter) check_stutter_invariance(aut, f); + if (opt_check & check_unambiguous) + spot::check_unambiguous(aut); } // Name the output automaton. diff --git a/src/tests/unambig.test b/src/tests/unambig.test index 0ca222fe2..4832519d3 100755 --- a/src/tests/unambig.test +++ b/src/tests/unambig.test @@ -35,6 +35,8 @@ for f in 'Ga' \ do $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous + $ltl2tgba -UH "$f" | $autfilt --check | grep unambiguous + $ltl2tgba -UH "!($f)" | $autfilt --check | grep unambiguous done for f in FGa @@ -82,3 +84,5 @@ State: 1 EOF run 1 $autfilt -q --is-unambiguous input +run 0 $autfilt --check input > output +test `grep -c unambiguous output` = 0 diff --git a/src/twa/twa.hh b/src/twa/twa.hh index bb50212ec..4efee483f 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -715,6 +715,7 @@ namespace spot bool state_based_acc:1; // State-based acceptance. bool inherently_weak:1; // Weak automaton. bool deterministic:1; // Deterministic automaton. + bool unambiguous:1; // Unambiguous automaton. bool stutter_invariant:1; // Stutter invariant language. bool stutter_sensitive:1; // Stutter sensitive language. }; @@ -797,6 +798,16 @@ namespace spot is.deterministic = val; } + bool is_unambiguous() const + { + return is.unambiguous; + } + + void prop_unambiguous(bool val = true) + { + is.unambiguous = val; + } + bool is_stutter_invariant() const { return is.stutter_invariant; @@ -839,7 +850,10 @@ namespace spot if (p.inherently_weak) prop_inherently_weak(other->is_inherently_weak()); if (p.deterministic) - prop_deterministic(other->is_deterministic()); + { + prop_deterministic(other->is_deterministic()); + prop_unambiguous(other->is_unambiguous()); + } if (p.stutter_inv) { prop_stutter_invariant(other->is_stutter_invariant()); @@ -854,7 +868,10 @@ namespace spot if (!p.inherently_weak) prop_inherently_weak(false); if (!p.deterministic) - prop_deterministic(false); + { + prop_deterministic(false); + prop_unambiguous(false); + } if (!p.stutter_inv) { prop_stutter_invariant(false); diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 7068d0804..8e8922932 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -296,7 +296,6 @@ namespace spot os << aut->acc().get_acceptance(); os << nl; os << "properties:"; - // Make sure the property line is not too large, // otherwise our test cases do not fit in 80 columns... unsigned prop_len = 60; @@ -327,6 +326,8 @@ namespace spot prop(" complete"); if (md.is_deterministic) prop(" deterministic"); + if (aut->is_unambiguous()) + prop(" unambiguous"); assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive())); if (aut->is_stutter_invariant()) prop(" stutter-invariant"); diff --git a/src/twaalgos/isunamb.cc b/src/twaalgos/isunamb.cc index 7584a23eb..3a22c1687 100644 --- a/src/twaalgos/isunamb.cc +++ b/src/twaalgos/isunamb.cc @@ -28,7 +28,7 @@ namespace spot { bool is_unambiguous(const const_twa_graph_ptr& aut) { - if (aut->is_deterministic()) + if (aut->is_deterministic() || aut->is_unambiguous()) return true; auto clean_a = scc_filter_states(aut); auto prod = product(clean_a, clean_a); @@ -37,4 +37,10 @@ namespace spot tgba_statistics sp = stats_reachable(clean_p); return sa.states == sp.states && sa.transitions == sp.transitions; } + + bool check_unambiguous(const twa_graph_ptr& aut) + { + aut->prop_unambiguous(is_unambiguous(aut)); + return aut->is_unambiguous(); + } } diff --git a/src/twaalgos/isunamb.hh b/src/twaalgos/isunamb.hh index 57f7c2a3f..1fca6fb8f 100644 --- a/src/twaalgos/isunamb.hh +++ b/src/twaalgos/isunamb.hh @@ -25,7 +25,7 @@ namespace spot { class tgba; - /// \addtogroup tgba_misc + /// \addtogroup twa_misc /// @{ /// \brief Whether the automaton \a aut is unambiguous. @@ -40,5 +40,8 @@ namespace spot SPOT_API bool is_unambiguous(const const_twa_graph_ptr& aut); + /// Like is_unambiguous(), but also sets the property in the twa. + SPOT_API bool + check_unambiguous(const twa_graph_ptr& aut); /// @} } diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index 74bce3595..add30de53 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -2555,6 +2555,9 @@ namespace spot a->prop_inherently_weak(f->is_syntactic_persistence()); a->prop_stutter_invariant(f->is_syntactic_stutter_invariant()); + // Currently the unambiguous option work only with LTL. + a->prop_unambiguous(f->is_ltl_formula() && unambiguous); + if (!simplifier) // This should not be deleted before we have registered all propositions. delete s;