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

support for semi-deterministic property

Browse source 
* spot/twa/twa.hh (prop_semi_deterministic): New methods.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
semi-deterministic property.
* doc/org/concepts.org, doc/org/hoa.org: Document it.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
* bin/autfilt.cc: Add --is-semi-deterministic.
* bin/common_aoutput.cc: Add --check=semi-deterministic.
* tests/core/semidet.test: New file.
* tests/Makefile.am: Add it.
* tests/core/parseaut.test, tests/core/readsave.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-29 16:37:43 +01:00
parent db5d9780f1
commit 4b01387817
14 changed files with 265 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

12
NEWS
View file

@ -11,7 +11,10 @@ New in spot 2.2.2.dev (Not yet released)
alternating automata, but in any case they should display a
diagnostic: if you see a crash, please report it.
* autfilt has two new filters: --is-very-weak and --is-alternating.
* autfilt has three new filters: --is-very-weak, --is-alternating,
and --is-semi-deterministic.
* the --check option can now take "semi-determinism" as argument.
Library:
@ -60,9 +63,10 @@ New in spot 2.2.2.dev (Not yet released)
https://www.lrde.epita.fr/tut24.html and
https://www.lrde.epita.fr/tut31.html for some code examples.
* 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().
* twa objects have two new properties, very-weak and
semi-deterministic, that can be set or retrieved via
twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can
be tested by is_very_weak_automaton()/is_semi_deterministic().
Build:

20
bin/autfilt.cc
View file

@ -107,6 +107,7 @@ enum {
OPT_IS_DETERMINISTIC,
OPT_IS_EMPTY,
OPT_IS_INHERENTLY_WEAK,
OPT_IS_SEMI_DETERMINISTIC,
OPT_IS_STUTTER_INVARIANT,
OPT_IS_TERMINAL,
OPT_IS_UNAMBIGUOUS,
@ -169,6 +170,8 @@ static const argp_option options[] =
"keep complete automata", 0 },
{ "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
"keep deterministic automata", 0 },
{ "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
"keep semi-deterministic automata", 0 },
{ "is-empty", OPT_IS_EMPTY, nullptr, 0,
"keep automata with an empty language", 0 },
{ "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
@ -415,6 +418,7 @@ static bool opt_merge = false;
static bool opt_is_alternating = false;
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
static bool opt_is_semi_deterministic = false;
static bool opt_is_unambiguous = false;
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
@ -672,6 +676,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_IS_VERY_WEAK:
opt_is_very_weak = true;
break;
case OPT_IS_SEMI_DETERMINISTIC:
opt_is_semi_deterministic = true;
break;
case OPT_IS_STUTTER_INVARIANT:
opt_is_stutter_invariant = true;
break;
@ -1072,9 +1079,16 @@ namespace
if (opt_nondet_states_set)
matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
if (opt_is_deterministic)
matched &= is_deterministic(aut);
else if (opt_is_unambiguous)
matched &= is_unambiguous(aut);
{
matched &= is_deterministic(aut);
}
else
{
if (opt_is_unambiguous)
matched &= is_unambiguous(aut);
if (opt_is_semi_deterministic)
matched &= is_semi_deterministic(aut);
}
if (opt_is_terminal)
matched &= is_terminal_automaton(aut);
else if (opt_is_very_weak)

6
bin/common_aoutput.cc
View file

@ -34,6 +34,7 @@
#include <spot/twaalgos/neverclaim.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/isdet.hh>
automaton_format_t automaton_format = Hoa;
static const char* automaton_format_opt = nullptr;
@ -45,6 +46,7 @@ enum check_type
check_unambiguous = (1 << 0),
check_stutter = (1 << 1),
check_strength = (1 << 2),
check_semi_determinism = (1 << 3),
check_all = -1U,
};
static char const *const check_args[] =
@ -54,6 +56,7 @@ static char const *const check_args[] =
"stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive",
"strength", "weak", "terminal",
"semi-determinism", "semi-deterministic",
"all",
nullptr
};
@ -64,6 +67,7 @@ static check_type const check_types[] =
check_stutter, check_stutter,
check_stutter, check_stutter,
check_strength, check_strength, check_strength,
check_semi_determinism, check_semi_determinism,
check_all
};
ARGMATCH_VERIFY(check_args, check_types);
@ -527,6 +531,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
spot::check_unambiguous(aut);
if (opt_check & check_strength)
spot::check_strength(aut);
if (opt_check & check_semi_determinism)
spot::is_semi_deterministic(aut); // sets the property as a side effect.
}
// Name the output automaton.

22
doc/org/concepts.org
View file

@ -554,7 +554,6 @@ $txt
#+RESULTS:
[[file:concept-twa1.png]]
* Alternating ω-automata
Alternating ω-automata are ω-automata in which the destination of an
@ -1055,16 +1054,17 @@ better choices.
There are actually several property flags that are stored into each
automaton, and that can be queried or set by algorithms:
| flag name | meaning when =true= |
|---------------------+----------------------------------------------------------------------------------------------|
| =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) |
| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] |
| flag name | meaning when =true= |
|----------------------+----------------------------------------------------------------------------------------------|
| =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 |
| =semi-deterministic= | any nondeterminism occurs before entering an accepting SCC |
| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) |
| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] |
For each flag =flagname=, the =twa= class has a method
=prop_flagname()= that returns the value of the flag as an instance of

50
doc/org/hoa.org
View file

@ -600,10 +600,11 @@ 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=,
=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.
=very-weak=, =terminal=, =unambiguous=, =semi-deterministic=, 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
@ -649,26 +650,27 @@ 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= | |
| =univ-branch= | checked | no | checked | |
| =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 | |
| 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= | |
| =univ-branch= | checked | no | checked | |
| =deterministic= | checked | yes | checked | |
| =complete= | checked | no | checked | |
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= |
| =semi-deterministic= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=semi-deterministic= |
| =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

13
spot/parseaut/parseaut.yy
View file

@ -590,6 +590,19 @@ header: format-version header-items
"... 'properties: !unambiguous' given here");
}
}
auto sd = p.find("semi-deterministic");
if (sd != e)
{
a->prop_semi_deterministic(sd->second.val);
auto d = p.find("deterministic");
if (d != e && !sd->second.val && d->second.val)
{
error(d->second.loc,
"'properties: deterministic' contradicts...");
error(sd->second.loc,
"... 'properties: !semi-deterministic' given here");
}
}
}
}

43
spot/twa/twa.hh
View file

@ -991,6 +991,7 @@ namespace spot
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
trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
};
union
{
@ -1285,16 +1286,17 @@ namespace spot
/// \brief Set the deterministic property.
///
/// Setting the "deterministic" property automatically
/// sets the "unambiguous" property.
/// Setting the "deterministic" property automatically sets the
/// "unambiguous" and "semi-deterministic" properties.
///
/// \see prop_unambiguous()
/// \see prop_semi_deterministic()
void prop_deterministic(trival val)
{
is.deterministic = val.val();
if (val)
// deterministic implies unambiguous
is.unambiguous = val.val();
// deterministic implies unambiguous and semi-deterministic
is.unambiguous = is.semi_deterministic = val.val();
}
/// \brief Whether the automaton is unambiguous
@ -1328,6 +1330,36 @@ namespace spot
is.deterministic = val.val();
}
/// \brief Whether the automaton is semi-deterministic
///
/// An automaton is semi-deterministic if the sub-automaton
/// reachable from any accepting SCC is deterministic.
///
/// Note that this method may return trival::maybe() when it is
/// unknown whether the automaton is semi-deterministic or not.
/// If you need a true/false answer, prefer the
/// is_semi_deterministic() function.
///
/// \see prop_deterministic()
/// \see is_semi_deterministic()
trival prop_semi_deterministic() const
{
return is.semi_deterministic;
}
/// \brief Sets the semi-deterministic property
///
/// Marking an automaton as "non semi-deterministic" automatically
/// marks it as "non deterministic".
///
/// \see prop_deterministic()
void prop_semi_deterministic(trival val)
{
is.semi_deterministic = val.val();
if (!val)
is.deterministic = val.val();
}
/// \brief Whether the automaton is stutter-invariant.
///
/// An automaton is stutter-invariant iff any accepted word
@ -1436,6 +1468,7 @@ namespace spot
if (p.deterministic)
{
prop_deterministic(other->prop_deterministic());
prop_semi_deterministic(other->prop_semi_deterministic());
prop_unambiguous(other->prop_unambiguous());
}
if (p.stutter_inv)
@ -1455,11 +1488,13 @@ namespace spot
{
prop_terminal(trival::maybe());
prop_weak(trival::maybe());
prop_very_weak(trival::maybe());
prop_inherently_weak(trival::maybe());
}
if (!p.deterministic)
{
prop_deterministic(trival::maybe());
prop_semi_deterministic(trival::maybe());
prop_unambiguous(trival::maybe());
}
if (!p.stutter_inv)

4
spot/twaalgos/hoa.cc
View file

@ -489,6 +489,10 @@ namespace spot
prop(" unambiguous");
else if (v1_1 && !aut->prop_unambiguous())
prop(" !unambiguous");
if (aut->prop_semi_deterministic() && (verbose || !md.is_deterministic))
prop(" semi-deterministic");
else if (v1_1 && !aut->prop_semi_deterministic())
prop(" !semi-deterministic");
if (aut->prop_stutter_invariant())
prop(" stutter-invariant");
if (!aut->prop_stutter_invariant())

47
spot/twaalgos/isdet.cc
View file

@ -18,8 +18,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <spot/twaalgos/isdet.hh>
#include <set>
#include <deque>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
{
@ -148,4 +147,48 @@ namespace spot
// initial state.
return ns > 0;
}
bool
is_semi_deterministic(const const_twa_graph_ptr& aut)
{
trival sd = aut->prop_semi_deterministic();
if (sd.is_known())
return sd.is_true();
scc_info si(aut);
si.determine_unknown_acceptance();
unsigned nscc = si.scc_count();
assert(nscc);
std::vector<bool> reachable_from_acc(nscc);
bool semi_det = true;
do // iterator of SCCs in reverse topological order
{
--nscc;
if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc])
{
for (unsigned succ: si.succ(nscc))
reachable_from_acc[succ] = true;
for (unsigned src: si.states_of(nscc))
{
bdd available = bddtrue;
for (auto& t: aut->out(src))
if (!bdd_implies(t.cond, available))
{
semi_det = false;
std::cerr << "Failed on state " << src << '\n';
goto done;
}
else
{
available -= t.cond;
}
}
}
}
while (nscc);
done:
std::const_pointer_cast<twa_graph>(aut)
->prop_semi_deterministic(semi_det);
return semi_det;
}
}

9
spot/twaalgos/isdet.hh
View file

@ -74,4 +74,13 @@ namespace spot
/// i.e., each state as a successor for any possible configuration.
SPOT_API bool
is_complete(const const_twa_graph_ptr& aut);
/// \brief Return true iff \a aut is semi-deterministic.
///
/// An automaton is semi-deterministic if the sub-automaton
/// reachable from any accepting SCC is deterministic.
SPOT_API bool
is_semi_deterministic(const const_twa_graph_ptr& aut);
}

1
tests/Makefile.am
View file

@ -208,6 +208,7 @@ TESTS_twa = \
core/renault.test \
core/nondet.test \
core/det.test \
core/semidet.test \
core/neverclaimread.test \
core/parseaut.test \
core/optba.test \

4
tests/core/parseaut.test
View file

@ -427,7 +427,7 @@ cat >input<<EOF
acc-name: generalized-Buchi 2
Acceptance: 2 (Inf(0) & Inf(1))
properties: implicit-labels trans-acc
properties: deterministic !unambiguous
properties: deterministic !unambiguous !semi-deterministic
AP: 2 "a" "b"
--BODY--
State: 0 "foo" { 0 }
@ -456,6 +456,8 @@ input:28.33-44: 'properties: state-labels' is incompatible with...
input:28.17-31: ... 'properties: implicit-labels'.
input:48.17-29: 'properties: deterministic' contradicts...
input:48.31-42: ... 'properties: !unambiguous' given here
input:48.17-29: 'properties: deterministic' contradicts...
input:48.44-62: ... 'properties: !semi-deterministic' given here
input:51.20-24: state-based acceptance used despite...
input:47.33-41: ... declaration of transition-based acceptance.
input:59.7-9: transition label used although the automaton was...

3
tests/core/readsave.test
View file

@ -811,7 +811,8 @@ AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: no-univ-branch trans-labels explicit-labels state-acc
properties: deterministic unambiguous weak inherently-weak
properties: deterministic unambiguous semi-deterministic weak
properties: inherently-weak
--BODY--
State: 0
[1] 2

81
tests/core/semidet.test Executable file
View file

@ -0,0 +1,81 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
cat >formulas <<EOF
0
!(F!p1 M 1)
(Gp0 | Fp1) M 1
F!(!p1 <-> FGp1)
Gp1 U (p1 U GFp1)
(!p1 U p1) U X(!p0 -> Fp1)
(p1 | (Fp0 R (p1 W p0))) M 1
!G(F(p1 & Fp0) W p1)
X(!p0 W Xp1)
1 U (p0 xor p1)
GF(p0)
FG(p0)
EOF
ltl2tgba -F formulas --check=semi-det -Hl |
sed 's/deterministic.*/deterministic/g;s/.* //g' >out
cat out
cat >expected <<EOF
deterministic
deterministic
semi-deterministic
deterministic
deterministic
semi-deterministic
deterministic
semi-deterministic
--END--
deterministic
deterministic
semi-deterministic
EOF
diff out expected
ltl2tgba -F formulas | autfilt --is-semi-det --stats=%M >out
cat out
cat >expected <<EOF
0
Gp1
F(p1 | Gp0)
F((!p1 & GF!p1) | (p1 & FGp1))
GFp1
Fp1 U X(p0 | Fp1)
F(p1 | (Fp0 R (p1 W p0)))
F(!p1 & G(!p1 | G!p0))
F((p0 & !p1) | (!p0 & p1))
GFp0
FGp0
EOF
diff out expected
ltl2tgba -F formulas | autfilt -v --is-semi-det --stats=%M >out
cat out
cat >expected <<EOF
X(!p0 W Xp1)
EOF
diff out expected