Commit 3428fb32 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Add support for --check=strength

* src/twaalgos/strength.cc, src/twaalgos/strength.hh (check_strength):
New function.
* src/bin/common_aoutput.cc: Add --check=strength.
* src/tests/strength.test: New file.
* src/tests/Makefile.am: Add it.
* doc/org/hoa.org, NEWS: Document it.
parent f4cf0f40
...@@ -4,6 +4,12 @@ New in spot 1.99.5a (not yet released) ...@@ -4,6 +4,12 @@ New in spot 1.99.5a (not yet released)
* autfilt has two now filters: --is-weak and --is-terminal. * autfilt has two now filters: --is-weak and --is-terminal.
* All tools that output HOA files accept a --check=strength option
to request automata to be marked as "weak" or "terminal" as
appropriate. Without this option, these properties may only be
set as a side-effect of running transformations that use this
information.
Library: Library:
* Properties of automata (like the "properties:" line of the HOA * Properties of automata (like the "properties:" line of the HOA
......
...@@ -591,8 +591,8 @@ particular: ...@@ -591,8 +591,8 @@ particular:
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= | | =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= |
| =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | | =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | | =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= |
| =terminal= | trusted | yes | as stored | | | =terminal= | trusted | yes | as stored | can be re-checked with =--check=strength= |
| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | | | =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be re-checked with =--check=strength= |
| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | | | =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =colored= | ignored | no | checked | | | =colored= | ignored | no | checked | |
...@@ -867,6 +867,6 @@ When an automaton is output in HOA format, the =property:= lines ...@@ -867,6 +867,6 @@ When an automaton is output in HOA format, the =property:= lines
includes property registered into the automaton (see the Property includes property registered into the automaton (see the Property
bits section above), and property that are trivial to compute. bits section above), and property that are trivial to compute.
Command-line with a HOA output all have a =--check= option that can be Command-line tools with a HOA output all have a =--check= option that
used to request additional checks such as testing whether the can be used to request additional checks such as testing whether the
automaton is stutter-invariant, or unambiguous. automaton is stutter-invariant, unambiguous, weak, and terminal.
...@@ -33,6 +33,7 @@ ...@@ -33,6 +33,7 @@
#include "twaalgos/neverclaim.hh" #include "twaalgos/neverclaim.hh"
#include "twaalgos/stutter.hh" #include "twaalgos/stutter.hh"
#include "twaalgos/isunamb.hh" #include "twaalgos/isunamb.hh"
#include "twaalgos/strength.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;
...@@ -46,6 +47,7 @@ enum check_type ...@@ -46,6 +47,7 @@ enum check_type
{ {
check_unambiguous = (1 << 0), check_unambiguous = (1 << 0),
check_stutter = (1 << 1), check_stutter = (1 << 1),
check_strength = (1 << 2),
check_all = -1U, check_all = -1U,
}; };
static char const *const check_args[] = static char const *const check_args[] =
...@@ -54,6 +56,7 @@ static char const *const check_args[] = ...@@ -54,6 +56,7 @@ static char const *const check_args[] =
"stutter-invariant", "stuttering-invariant", "stutter-invariant", "stuttering-invariant",
"stutter-insensitive", "stuttering-insensitive", "stutter-insensitive", "stuttering-insensitive",
"stutter-sensitive", "stuttering-sensitive", "stutter-sensitive", "stuttering-sensitive",
"strength", "weak", "terminal",
"all", "all",
nullptr nullptr
}; };
...@@ -63,6 +66,7 @@ static check_type const check_types[] = ...@@ -63,6 +66,7 @@ static check_type const check_types[] =
check_stutter, check_stutter, check_stutter, check_stutter,
check_stutter, check_stutter, check_stutter, check_stutter,
check_stutter, check_stutter, check_stutter, check_stutter,
check_strength, check_strength, check_strength,
check_all check_all
}; };
ARGMATCH_VERIFY(check_args, check_types); ARGMATCH_VERIFY(check_args, check_types);
...@@ -121,7 +125,8 @@ static const argp_option options[] = ...@@ -121,7 +125,8 @@ 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), 'unambiguous', or 'stutter-invariant'.", 0 }, "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 } { nullptr, 0, nullptr, 0, nullptr, 0 }
}; };
...@@ -299,9 +304,11 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, ...@@ -299,9 +304,11 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
if (opt_check) if (opt_check)
{ {
if (opt_check & check_stutter) if (opt_check & check_stutter)
check_stutter_invariance(aut, f); spot::check_stutter_invariance(aut, f);
if (opt_check & check_unambiguous) if (opt_check & check_unambiguous)
spot::check_unambiguous(aut); spot::check_unambiguous(aut);
if (opt_check & check_strength)
spot::check_strength(aut);
} }
// Name the output automaton. // Name the output automaton.
......
...@@ -229,6 +229,7 @@ TESTS_twa = \ ...@@ -229,6 +229,7 @@ TESTS_twa = \
uniq.test \ uniq.test \
sbacc.test \ sbacc.test \
stutter-tgba.test \ stutter-tgba.test \
strength.test \
emptchk.test \ emptchk.test \
emptchke.test \ emptchke.test \
dfs.test \ dfs.test \
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Developpement
# de l'Epita
#
# 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
autfilt=../../bin/autfilt
cat >in <<EOF
HOA: v1
name: "a U b"
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 1
State: 1
[0] 0 {0}
[!0] 1 {0}
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 2 Inf(0)|Inf(1)
--BODY--
State: 0 {0}
[t] 1
State: 1
[0] 0 {1}
[!0] 1 {0}
--END--
HOA: v1
States: 2
Start: 1
Acceptance: 0 t
--BODY--
State: 0
[t] 1
State: 1
[t] 0
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 1
State: 1
[!0] 1 {0}
--END--
EOF
run 0 $autfilt -H --check=strength in | tee out
cat >expected <<EOF
HOA: v1
name: "a U b"
States: 2
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[0] 0
[!0] 1
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
Acceptance: 2 Inf(0) | Inf(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[t] 1 {0}
State: 1
[0] 0 {1}
[!0] 1 {0}
--END--
HOA: v1
States: 2
Start: 1
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
--BODY--
State: 0
[t] 1
State: 1
[t] 0
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 1
State: 1 {0}
[!0] 1
--END--
EOF
diff out expected
...@@ -26,8 +26,8 @@ namespace spot ...@@ -26,8 +26,8 @@ namespace spot
{ {
namespace namespace
{ {
template <bool terminal> template <bool terminal, bool set = false>
bool is_type_automaton(const const_twa_graph_ptr& aut, scc_info* si) bool is_type_automaton(const twa_graph_ptr& aut, scc_info* si)
{ {
// Create an scc_info if the user did not give one to us. // Create an scc_info if the user did not give one to us.
bool need_si = !si; bool need_si = !si;
...@@ -35,7 +35,8 @@ namespace spot ...@@ -35,7 +35,8 @@ namespace spot
si = new scc_info(aut); si = new scc_info(aut);
si->determine_unknown_acceptance(); si->determine_unknown_acceptance();
bool result = true; bool is_weak = true;
bool is_term = true;
unsigned n = si->scc_count(); unsigned n = si->scc_count();
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
{ {
...@@ -54,33 +55,49 @@ namespace spot ...@@ -54,33 +55,49 @@ namespace spot
} }
else if (m != t.acc) else if (m != t.acc)
{ {
result = false; is_weak = false;
goto exit; goto exit;
} }
} }
if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i)) if (terminal && si->is_accepting_scc(i) && !is_complete_scc(*si, i))
{ {
result = false; is_term = false;
break; if (!set)
break;
} }
} }
exit: exit:
if (need_si) if (need_si)
delete si; delete si;
return result; if (set)
{
if (terminal)
aut->prop_terminal(is_term && is_weak);
aut->prop_weak(is_weak);
}
return is_weak && is_term;
} }
} }
bool bool
is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si) is_terminal_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{ {
return aut->prop_terminal() || is_type_automaton<true>(aut, si); return (aut->prop_terminal() ||
is_type_automaton<true>(std::const_pointer_cast<twa_graph>(aut),
si));
} }
bool bool
is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si)
{ {
return aut->prop_weak() || is_type_automaton<false>(aut, si); return (aut->prop_weak() ||
is_type_automaton<false>(std::const_pointer_cast<twa_graph>(aut),
si));
}
void check_strength(const twa_graph_ptr& aut, scc_info* si)
{
is_type_automaton<true, true>(aut, si);
} }
bool is_safety_mwdba(const const_twa_graph_ptr& aut) bool is_safety_mwdba(const const_twa_graph_ptr& aut)
......
...@@ -58,4 +58,14 @@ namespace spot ...@@ -58,4 +58,14 @@ namespace spot
SPOT_API bool SPOT_API bool
is_safety_mwdba(const const_twa_graph_ptr& aut); is_safety_mwdba(const const_twa_graph_ptr& aut);
/// \brief Whether an automaton is weak or terminal.
///
/// This sets the "weak" and "terminal" property as appropriate.
///
/// \param aut the automaton to check
///
/// \param sm an scc_info object for the automaton if available (it
/// will be built otherwise).
SPOT_API void
check_strength(const twa_graph_ptr& aut, scc_info* sm = nullptr);
} }
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