Commit 6bc2fa24 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: add a stutter-sensitive property

* src/twa/twa.hh: Support this new property.
* src/twaalgos/stutter.cc: Set it if needed.
* src/twaalgos/hoa.cc: Output it.
* src/tests/stutter-tgba.test: More tests.
parent fe2fc88f
......@@ -70,6 +70,8 @@ State: 2
--END--
EOF
diff output expected
run 0 $ltl2tgba -H 'F(a & X(!a & b))' > input
grep stutter-invariant input && exit 1
run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
......@@ -77,4 +79,9 @@ grep stutter-invariant input.2
run 0 $autfilt --check=stutter input > input.2
grep stutter-invariant input.2
diff output expected
run 0 $ltl2tgba -H 'F(a & X(a & b))' > input
grep stutter-invariant input && exit 1
run 0 $ltl2tgba --check=stutter 'F(a & X(a & b))' > input.2
grep stutter-sensitive input.2
run 0 $autfilt --check=stutter input > input.2
grep stutter-sensitive input.2
......@@ -715,7 +715,8 @@ namespace spot
bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Weak automaton.
bool deterministic:1; // Deterministic automaton.
bool stutter_inv:1; // Stutter invariant
bool stutter_invariant:1; // Stutter invariant language.
bool stutter_sensitive:1; // Stutter sensitive language.
};
union
{
......@@ -798,12 +799,22 @@ namespace spot
bool is_stutter_invariant() const
{
return is.stutter_inv;
return is.stutter_invariant;
}
bool is_stutter_sensitive() const
{
return is.stutter_sensitive;
}
void prop_stutter_invariant(bool val = true)
{
is.stutter_inv = val;
is.stutter_invariant = val;
}
void prop_stutter_sensitive(bool val = true)
{
is.stutter_sensitive = val;
}
struct prop_set
......@@ -830,7 +841,10 @@ namespace spot
if (p.deterministic)
prop_deterministic(other->is_deterministic());
if (p.stutter_inv)
prop_stutter_invariant(other->is_stutter_invariant());
{
prop_stutter_invariant(other->is_stutter_invariant());
prop_stutter_sensitive(other->is_stutter_sensitive());
}
}
void prop_keep(prop_set p)
......@@ -841,6 +855,11 @@ namespace spot
prop_inherently_weak(false);
if (!p.deterministic)
prop_deterministic(false);
if (!p.stutter_inv)
{
prop_stutter_invariant(false);
prop_stutter_sensitive(false);
}
}
};
......
......@@ -327,8 +327,11 @@ namespace spot
prop(" complete");
if (md.is_deterministic)
prop(" deterministic");
assert(!(aut->is_stutter_invariant() && aut->is_stutter_sensitive()));
if (aut->is_stutter_invariant())
prop(" stutter-invariant");
if (aut->is_stutter_sensitive())
prop(" stutter-sensitive");
if (aut->is_inherently_weak())
prop(" inherently-weak");
os << nl;
......
......@@ -667,8 +667,8 @@ namespace spot
is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
std::move(neg), get_all_ap(aut));
if (is_stut)
aut->prop_stutter_invariant(is_stut);
aut->prop_stutter_invariant(is_stut);
aut->prop_stutter_sensitive(!is_stut);
return is_stut;
}
}
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