alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twa: add support for very-weak property

Browse source 
* spot/twa/twa.hh: Implement the property.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input
and output for it.
* spot/twaalgos/strength.cc,
spot/twaalgos/strength.hh (is_very_weak_automaton): New function.
* tests/core/alternating.test: Add a test for --check=strength
on an alternating automaton.
* tests/core/strength.test, tests/core/parseaut.test: Adjust expected
output.
* NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-01 18:27:54 +01:00
parent a4ce999402
commit 582d455c23
11 changed files with 146 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -14,6 +14,10 @@ New in spot 2.2.2.dev (Not yet released)
* The new version of the Couvreur emptiness check is now the default
one, used by is_empty() and accepting_run().
* twa objects have a new property, very-weak, that can be set or
retrieved via twa::prop_very_weak(), and that can be tested by
is_very_weak_automaton().
Build:
* The configure script has a new option --enable-c++14, to compile in

1
doc/org/concepts.org
View file

@ -995,6 +995,7 @@ automaton, and that can be queried or set by algorithms:
| =state_acc= | automaton should be considered has having state-based acceptance |
| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC |
| =weak= | transitions of an SCC all belong to the same acceptance sets |
| =very-weak= | weak automaton where all SCCs have size 1 |
| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs |
| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it |
| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) |

45
doc/org/hoa.org
View file

@ -603,10 +603,10 @@ body of the file, and then return and error if what has been declared
does not correspond to the reality.
Some supported properties (like =weak=, =inherently-weak=,
=unambiguous=, or =stutter-invariant=) are not double-checked, because
that would require more operations. Command-line tools that
read HOA files all take a =--trust-hoa=no= option to ignore properties
that are not double-checked by the parser.
=very-weak=, =terminal=, =unambiguous=, or =stutter-invariant=) are
not double-checked, because that would require more operations.
Command-line tools that read HOA files all take a =--trust-hoa=no=
option to ignore properties that are not double-checked by the parser.
It should be noted that each property can take three values: true,
false, or maybe. So actually two bits are used per property. For
@ -652,24 +652,25 @@ particular:
to detect deterministic automata that have been output by algorithms
that do not try to output deterministic automata.
| property | parser | stored | printer | notes |
|---------------------+---------+--------+---------------------------------------------+------------------------------------------------------------------|
| =state-labels= | checked | no | checked if =-Hk= | state labels are converted to transition labels when reading TωA |
| =trans-labels= | checked | no | always, unless =-Hi= or =-Hk= | |
| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata |
| =explicit-labels= | checked | no | always, unless =-Hi= | |
| =state-acc= | checked | yes | checked, unless =-Ht= or =-Hm= | |
| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | |
| =no-univ-branch= | ignored | no | only if =-Hv= | |
| =deterministic= | checked | yes | checked | |
| =complete= | checked | no | checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored (opposite of =stutter-invariant=) | can be checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= |
| =colored= | ignored | no | checked | |
| property | parser | stored | printer | notes |
|---------------------+---------+--------+---------------------------------------------------------+------------------------------------------------------------------|
| =state-labels= | checked | no | checked if =-Hk= | state labels are converted to transition labels when reading TωA |
| =trans-labels= | checked | no | always, unless =-Hi= or =-Hk= | |
| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata |
| =explicit-labels= | checked | no | always, unless =-Hi= | |
| =state-acc= | checked | yes | checked, unless =-Ht= or =-Hm= | |
| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | |
| =no-univ-branch= | ignored | no | only if =-Hv= | |
| =deterministic= | checked | yes | checked | |
| =complete= | checked | no | checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored (opposite of =stutter-invariant=) | can be checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= |
| =very-weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not (=terminal= or =very-weak=)) | can be checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= |
| =colored= | ignored | no | checked | |
The above table is for version 1 of the format. When version 1.1 is
selected (using =-H1.1=), some negated properties may be output. In

19
spot/parseaut/parseaut.yy
View file

@ -526,8 +526,27 @@ header: format-version header-items
a->prop_stutter_invariant(!ss->second.val);
}
auto iw = p.find("inherently-weak");
auto vw = p.find("very-weak");
auto w = p.find("weak");
auto t = p.find("terminal");
if (vw != e)
{
a->prop_very_weak(vw->second.val);
if (w != e && !w->second.val && vw->second.val)
{
error(w->second.loc,
"'properties: !weak' contradicts...");
error(vw->second.loc,
"... 'properties: very-weak' given here");
}
if (iw != e && !iw->second.val && vw->second.val)
{
error(iw->second.loc,
"'properties: !inherently-weak' contradicts...");
error(vw->second.loc,
"... 'properties: very-weak' given here");
}
}
if (iw != e)
{
a->prop_inherently_weak(iw->second.val);

37
spot/twa/twa.hh
View file

@ -990,6 +990,7 @@ namespace spot
trival::repr_t deterministic:2; // Deterministic automaton.
trival::repr_t unambiguous:2; // Unambiguous automaton.
trival::repr_t stutter_invariant:2; // Stutter invariant language.
trival::repr_t very_weak:2; // very-weak, or 1-weak
};
union
{
@ -1167,7 +1168,7 @@ namespace spot
/// \brief Set the "inherently weak" proeprty.
///
/// Setting "inherently weak" to false automatically
/// disables "terminal" and "weak".
/// disables "terminal", "very weak", and "weak".
///
/// \see prop_weak()
/// \see prop_terminal()
@ -1175,7 +1176,7 @@ namespace spot
{
is.inherently_weak = val.val();
if (!val)
is.terminal = is.weak = val.val();
is.very_weak = is.terminal = is.weak = val.val();
}
/// \brief Whether the automaton is terminal.
@ -1234,9 +1235,38 @@ namespace spot
if (val)
is.inherently_weak = val.val();
if (!val)
is.terminal = val.val();
is.very_weak = is.terminal = val.val();
}
/// \brief Whether the automaton is very-weak.
///
/// An automaton is very-weak if it is weak (inside each strongly connected
/// component, all transitions belong to the same acceptance sets)
/// and each SCC contains only one state.
///
/// \see prop_terminal()
/// \see prop_weak()
trival prop_very_weak() const
{
return is.very_weak;
}
/// \brief Set the very-weak property.
///
/// Marking an automaton as "very-weak" automatically marks it as
/// "weak" and "inherently weak".
///
/// \see prop_terminal()
/// \see prop_weak()
void prop_very_weak(trival val)
{
is.very_weak = val.val();
if (val)
is.weak = is.inherently_weak = val.val();
}
/// \brief Whether the automaton is deterministic.
///
/// An automaton is deterministic if the conjunction between the
@ -1400,6 +1430,7 @@ namespace spot
{
prop_terminal(other->prop_terminal());
prop_weak(other->prop_weak());
prop_very_weak(other->prop_very_weak());
prop_inherently_weak(other->prop_inherently_weak());
}
if (p.deterministic)

8
spot/twaalgos/hoa.cc
View file

@ -500,12 +500,18 @@ namespace spot
}
if (aut->prop_terminal())
prop(" terminal");
if (aut->prop_weak() && (verbose || aut->prop_terminal() != true))
if (aut->prop_very_weak() && (verbose || aut->prop_terminal() != true))
prop(" very-weak");
if (aut->prop_weak() && (verbose || (aut->prop_terminal() != true &&
aut->prop_very_weak() != true)))
prop(" weak");
if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
prop(" inherently-weak");
if (v1_1 && !aut->prop_terminal() && (verbose || aut->prop_weak() != false))
prop(" !terminal");
if (v1_1 && !aut->prop_very_weak() && (verbose
|| aut->prop_weak() != false))
prop(" !very-weak");
if (v1_1 && !aut->prop_weak() && (verbose ||
aut->prop_inherently_weak() != false))
prop(" !weak");

28
spot/twaalgos/strength.cc
View file

@ -34,22 +34,29 @@ namespace spot
bool need_si = !si;
if (need_si)
si = new scc_info(aut);
si->determine_unknown_acceptance();
if (inweak)
si->determine_unknown_acceptance();
bool is_inweak = true;
bool is_weak = true;
bool is_single_state_scc = true;
bool is_term = true;
unsigned n = si->scc_count();
for (unsigned i = 0; i < n; ++i)
{
if (si->is_trivial(i))
continue;
if (si->states_of(i).size() > 1)
is_single_state_scc = false;
bool first = true;
acc_cond::mark_t m = 0U;
if (is_weak)
for (auto src: si->states_of(i))
for (auto& t: aut->out(src))
if (si->scc_of(t.dst) == i)
// In case of a universal edge we only need to check
// the first destination of an inside the SCC, because
// the other have the same t.acc.
if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i)
{
if (first)
{
@ -98,6 +105,7 @@ namespace spot
if (terminal)
aut->prop_terminal(is_term && is_weak);
aut->prop_weak(is_weak);
aut->prop_very_weak(is_single_state_scc && is_weak);
if (inweak)
aut->prop_inherently_weak(is_inweak);
}
@ -131,6 +139,17 @@ namespace spot
return res;
}
bool
is_very_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
trival v = aut->prop_very_weak();
if (v.is_known())
return v.is_true();
is_type_automaton<false, false, true>
(std::const_pointer_cast<twa_graph>(aut), si);
return aut->prop_very_weak().is_true();
}
bool
is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{
@ -145,7 +164,10 @@ namespace spot
void check_strength(const twa_graph_ptr& aut, scc_info* si)
{
is_type_automaton<true, true, true>(aut, si);
if (aut->is_alternating())
is_type_automaton<false, false, true>(aut, si);
else
is_type_automaton<true, true, true>(aut, si);
}
bool is_safety_mwdba(const const_twa_graph_ptr& aut)

21
spot/twaalgos/strength.hh
View file

@ -60,6 +60,24 @@ namespace spot
SPOT_API bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr);
/// \brief Check whether an automaton is very-weak.
///
/// An automaton is very-weak if in any given SCC, all transitions
/// belong to the same acceptance sets, and the SCC has only one
/// state.
///
/// \param aut the automaton to check
///
/// \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_very_weak() and prop_weak() properties of the automaton
/// as a side-effect, so further calls will return in constant-time.
SPOT_API bool
is_very_weak_automaton(const const_twa_graph_ptr& aut,
scc_info* sm = nullptr);
/// \brief Check whether an automaton is inherently weak.
///
/// An automaton is inherently weak if in any given SCC, there
@ -90,7 +108,8 @@ namespace spot
/// \brief Check whether an automaton is weak or terminal.
///
/// This sets the "weak" and "terminal" property as appropriate.
/// This sets the "inherently weak", "weak", "very-weak" and
/// "terminal" properties as appropriate.
///
/// \param aut the automaton to check
///

7
tests/core/alternating.test
View file

@ -126,3 +126,10 @@ digraph G {
EOF
diff expect.dot alt.dot
autfilt --trust=no --check=strength alt.hoa | grep properties: >output
cat >expected <<EOF
properties: univ-branch trans-labels explicit-labels state-acc
properties: very-weak
EOF
diff output expected

3
tests/core/parseaut.test
View file

@ -1928,6 +1928,7 @@ AP: 4 "p2" "c1" "p1" "c2"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels state-acc
properties: very-weak
--BODY--
State: 0 "X (G(c2))"
[t] 1
@ -2403,6 +2404,7 @@ AP: 2 "b" "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels state-acc
properties: very-weak
--BODY--
State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
[0] 3&1
@ -2608,6 +2610,7 @@ AP: 2 "b" "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: univ-branch trans-labels explicit-labels state-acc
properties: very-weak
--BODY--
State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
[0] 3&1

6
tests/core/strength.test
View file

@ -182,7 +182,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
properties: deterministic very-weak
--BODY--
State: 0 {0}
[t] 1
@ -644,7 +644,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic weak
properties: deterministic very-weak
--BODY--
State: 0
[t] 0
@ -659,7 +659,7 @@ AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic weak
properties: deterministic very-weak
--BODY--
State: 0
[t] 0