Commit 487a86d0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bin: add --check=unambiguous

* src/bin/common_aoutput.cc: Add --check=unambiguous.
* src/twa/twa.hh: New unambiguous property.
* src/twaalgos/hoa.cc: Print it.
* src/twaalgos/ltl2tgba_fm.cc: Set it.
* src/twaalgos/isunamb.cc, src/twaalgos/isunamb.hh
(check_unambiguous): New function.
* src/tests/unambig.test: More tests.
parent 98de84f3
...@@ -32,6 +32,7 @@ ...@@ -32,6 +32,7 @@
#include "twaalgos/hoa.hh" #include "twaalgos/hoa.hh"
#include "twaalgos/neverclaim.hh" #include "twaalgos/neverclaim.hh"
#include "twaalgos/stutter.hh" #include "twaalgos/stutter.hh"
#include "twaalgos/isunamb.hh"
automaton_format_t automaton_format = Dot; automaton_format_t automaton_format = Dot;
static const char* opt_dot = nullptr; static const char* opt_dot = nullptr;
...@@ -42,11 +43,13 @@ static const char* opt_output = nullptr; ...@@ -42,11 +43,13 @@ static const char* opt_output = nullptr;
static const char* stats = ""; static const char* stats = "";
enum check_type enum check_type
{ {
check_stutter = (1 << 0), check_unambiguous = (1 << 0),
check_stutter = (1 << 1),
check_all = -1U, check_all = -1U,
}; };
static char const *const check_args[] = static char const *const check_args[] =
{ {
"unambiguous",
"stutter-invariant", "stuttering-invariant", "stutter-invariant", "stuttering-invariant",
"stutter-insensitive", "stuttering-insensitive", "stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive", "stutter-sensitive", "stuttering-sensitive",
...@@ -55,6 +58,7 @@ static char const *const check_args[] = ...@@ -55,6 +58,7 @@ static char const *const check_args[] =
}; };
static check_type const check_types[] = static check_type const check_types[] =
{ {
check_unambiguous,
check_stutter, check_stutter, check_stutter, check_stutter,
check_stutter, check_stutter, check_stutter, check_stutter,
check_stutter, check_stutter, check_stutter, check_stutter,
...@@ -115,7 +119,7 @@ static const argp_option options[] = ...@@ -115,7 +119,7 @@ static const argp_option options[] =
{ "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL, { "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL,
"test for the additional property PROP and output the result " "test for the additional property PROP and output the result "
"in the HOA format (implies -H). PROP may be any prefix of " "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 } { 0, 0, 0, 0, 0, 0 }
}; };
...@@ -283,6 +287,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, ...@@ -283,6 +287,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
{ {
if (opt_check & check_stutter) if (opt_check & check_stutter)
check_stutter_invariance(aut, f); check_stutter_invariance(aut, f);
if (opt_check & check_unambiguous)
spot::check_unambiguous(aut);
} }
// Name the output automaton. // Name the output automaton.
......
...@@ -35,6 +35,8 @@ for f in 'Ga' \ ...@@ -35,6 +35,8 @@ for f in 'Ga' \
do do
$ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
$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 done
for f in FGa for f in FGa
...@@ -82,3 +84,5 @@ State: 1 ...@@ -82,3 +84,5 @@ State: 1
EOF EOF
run 1 $autfilt -q --is-unambiguous input run 1 $autfilt -q --is-unambiguous input
run 0 $autfilt --check input > output
test `grep -c unambiguous output` = 0
...@@ -715,6 +715,7 @@ namespace spot ...@@ -715,6 +715,7 @@ namespace spot
bool state_based_acc:1; // State-based acceptance. bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Weak automaton. bool inherently_weak:1; // Weak automaton.
bool deterministic:1; // Deterministic automaton. bool deterministic:1; // Deterministic automaton.
bool unambiguous:1; // Unambiguous automaton.
bool stutter_invariant:1; // Stutter invariant language. bool stutter_invariant:1; // Stutter invariant language.
bool stutter_sensitive:1; // Stutter sensitive language. bool stutter_sensitive:1; // Stutter sensitive language.
}; };
...@@ -797,6 +798,16 @@ namespace spot ...@@ -797,6 +798,16 @@ namespace spot
is.deterministic = val; is.deterministic = val;
} }
bool is_unambiguous() const
{
return is.unambiguous;
}
void prop_unambiguous(bool val = true)
{
is.unambiguous = val;
}
bool is_stutter_invariant() const bool is_stutter_invariant() const
{ {
return is.stutter_invariant; return is.stutter_invariant;
...@@ -839,7 +850,10 @@ namespace spot ...@@ -839,7 +850,10 @@ namespace spot
if (p.inherently_weak) if (p.inherently_weak)
prop_inherently_weak(other->is_inherently_weak()); prop_inherently_weak(other->is_inherently_weak());
if (p.deterministic) if (p.deterministic)
prop_deterministic(other->is_deterministic()); {
prop_deterministic(other->is_deterministic());
prop_unambiguous(other->is_unambiguous());
}
if (p.stutter_inv) if (p.stutter_inv)
{ {
prop_stutter_invariant(other->is_stutter_invariant()); prop_stutter_invariant(other->is_stutter_invariant());
...@@ -854,7 +868,10 @@ namespace spot ...@@ -854,7 +868,10 @@ namespace spot
if (!p.inherently_weak) if (!p.inherently_weak)
prop_inherently_weak(false); prop_inherently_weak(false);
if (!p.deterministic) if (!p.deterministic)
prop_deterministic(false); {
prop_deterministic(false);
prop_unambiguous(false);
}
if (!p.stutter_inv) if (!p.stutter_inv)
{ {
prop_stutter_invariant(false); prop_stutter_invariant(false);
......
...@@ -296,7 +296,6 @@ namespace spot ...@@ -296,7 +296,6 @@ namespace spot
os << aut->acc().get_acceptance(); os << aut->acc().get_acceptance();
os << nl; os << nl;
os << "properties:"; os << "properties:";
// Make sure the property line is not too large, // Make sure the property line is not too large,
// otherwise our test cases do not fit in 80 columns... // otherwise our test cases do not fit in 80 columns...
unsigned prop_len = 60; unsigned prop_len = 60;
...@@ -327,6 +326,8 @@ namespace spot ...@@ -327,6 +326,8 @@ namespace spot
prop(" complete"); prop(" complete");
if (md.is_deterministic) if (md.is_deterministic)
prop(" deterministic"); prop(" deterministic");
if (aut->is_unambiguous())
prop(" unambiguous");
assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive())); assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive()));
if (aut->is_stutter_invariant()) if (aut->is_stutter_invariant())
prop(" stutter-invariant"); prop(" stutter-invariant");
......
...@@ -28,7 +28,7 @@ namespace spot ...@@ -28,7 +28,7 @@ namespace spot
{ {
bool is_unambiguous(const const_twa_graph_ptr& aut) bool is_unambiguous(const const_twa_graph_ptr& aut)
{ {
if (aut->is_deterministic()) if (aut->is_deterministic() || aut->is_unambiguous())
return true; return true;
auto clean_a = scc_filter_states(aut); auto clean_a = scc_filter_states(aut);
auto prod = product(clean_a, clean_a); auto prod = product(clean_a, clean_a);
...@@ -37,4 +37,10 @@ namespace spot ...@@ -37,4 +37,10 @@ namespace spot
tgba_statistics sp = stats_reachable(clean_p); tgba_statistics sp = stats_reachable(clean_p);
return sa.states == sp.states && sa.transitions == sp.transitions; 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();
}
} }
...@@ -25,7 +25,7 @@ namespace spot ...@@ -25,7 +25,7 @@ namespace spot
{ {
class tgba; class tgba;
/// \addtogroup tgba_misc /// \addtogroup twa_misc
/// @{ /// @{
/// \brief Whether the automaton \a aut is unambiguous. /// \brief Whether the automaton \a aut is unambiguous.
...@@ -40,5 +40,8 @@ namespace spot ...@@ -40,5 +40,8 @@ namespace spot
SPOT_API bool SPOT_API bool
is_unambiguous(const const_twa_graph_ptr& aut); 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);
/// @} /// @}
} }
...@@ -2555,6 +2555,9 @@ namespace spot ...@@ -2555,6 +2555,9 @@ namespace spot
a->prop_inherently_weak(f->is_syntactic_persistence()); a->prop_inherently_weak(f->is_syntactic_persistence());
a->prop_stutter_invariant(f->is_syntactic_stutter_invariant()); 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) if (!simplifier)
// This should not be deleted before we have registered all propositions. // This should not be deleted before we have registered all propositions.
delete s; delete s;
......
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