autfilt: add --aliases=drop|keep option
* bin/autfilt.cc: Here. * spot/twaalgos/hoa.cc, spot/twaalgos/hoa.hh: Fix the prototype of set_aliases so that it is usable. * tests/core/dualize.test: Add a simple test case. * NEWS: Mention the new option.
This commit is contained in:
parent
95b2e7366f
commit
f759697e1c
5 changed files with 85 additions and 5 deletions
6
NEWS
6
NEWS
|
|
@ -1,5 +1,11 @@
|
||||||
New in spot 2.10.4.dev (net yet released)
|
New in spot 2.10.4.dev (net yet released)
|
||||||
|
|
||||||
|
Command-line tools:
|
||||||
|
|
||||||
|
- autfilt has a new options --aliases=drop|keep to specify
|
||||||
|
if the output code should attempt to preserve aliases
|
||||||
|
present in the HOA input. This defaults to "keep".
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
- "original-classes" is a new named property similar to
|
- "original-classes" is a new named property similar to
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
|
// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -88,6 +88,7 @@ enum {
|
||||||
OPT_ACC_SETS,
|
OPT_ACC_SETS,
|
||||||
OPT_ACCEPT_WORD,
|
OPT_ACCEPT_WORD,
|
||||||
OPT_ACCEPTANCE_IS,
|
OPT_ACCEPTANCE_IS,
|
||||||
|
OPT_ALIASES,
|
||||||
OPT_AP_N,
|
OPT_AP_N,
|
||||||
OPT_ARE_ISOMORPHIC,
|
OPT_ARE_ISOMORPHIC,
|
||||||
OPT_CLEAN_ACC,
|
OPT_CLEAN_ACC,
|
||||||
|
|
@ -175,6 +176,10 @@ static const argp_option options[] =
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
{ "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
|
{ "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
|
||||||
{ "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
|
{ "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
|
||||||
|
{ "aliases", OPT_ALIASES, "drop|keep", 0,
|
||||||
|
"If the input automaton uses HOA aliases, this decides whether their "
|
||||||
|
"preservation should be attempted in the output. The default is "
|
||||||
|
"\"keep\".", 3 },
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
{ nullptr, 0, nullptr, 0, "Filtering options:", 5 },
|
{ nullptr, 0, nullptr, 0, "Filtering options:", 5 },
|
||||||
{ "ap", OPT_AP_N, "RANGE", 0,
|
{ "ap", OPT_AP_N, "RANGE", 0,
|
||||||
|
|
@ -474,6 +479,20 @@ static gra_type const gra_types[] =
|
||||||
};
|
};
|
||||||
ARGMATCH_VERIFY(gra_args, gra_types);
|
ARGMATCH_VERIFY(gra_args, gra_types);
|
||||||
|
|
||||||
|
static bool opt_aliases = true;
|
||||||
|
static char const* const aliases_args[] =
|
||||||
|
{
|
||||||
|
"drop", "no", "false", "0",
|
||||||
|
"keep", "yes", "true", "1",
|
||||||
|
nullptr,
|
||||||
|
};
|
||||||
|
static bool const aliases_types[] =
|
||||||
|
{
|
||||||
|
false, false, false, false,
|
||||||
|
true, true, true, true,
|
||||||
|
};
|
||||||
|
ARGMATCH_VERIFY(aliases_args, aliases_types);
|
||||||
|
|
||||||
enum acc_type {
|
enum acc_type {
|
||||||
ACC_Any = 0,
|
ACC_Any = 0,
|
||||||
ACC_Given,
|
ACC_Given,
|
||||||
|
|
@ -757,6 +776,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
error(2, 0, "failed to parse --options near '%s'", opt);
|
error(2, 0, "failed to parse --options near '%s'", opt);
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
|
case OPT_ALIASES:
|
||||||
|
opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types);
|
||||||
|
break;
|
||||||
case OPT_AP_N:
|
case OPT_AP_N:
|
||||||
opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
|
opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
break;
|
break;
|
||||||
|
|
@ -1363,6 +1385,8 @@ namespace
|
||||||
spot::process_timer timer;
|
spot::process_timer timer;
|
||||||
timer.start();
|
timer.start();
|
||||||
|
|
||||||
|
auto aliases = get_aliases(haut->aut);
|
||||||
|
|
||||||
// If --stats or --name is used, duplicate the automaton so we
|
// If --stats or --name is used, duplicate the automaton so we
|
||||||
// never modify the original automaton (e.g. with
|
// never modify the original automaton (e.g. with
|
||||||
// merge_edges()) and the statistics about it make sense.
|
// merge_edges()) and the statistics about it make sense.
|
||||||
|
|
@ -1660,6 +1684,13 @@ namespace
|
||||||
|
|
||||||
++match_count;
|
++match_count;
|
||||||
|
|
||||||
|
if (aliases)
|
||||||
|
{
|
||||||
|
if (opt_aliases)
|
||||||
|
set_aliases(aut, *aliases);
|
||||||
|
else
|
||||||
|
set_aliases(aut, {});
|
||||||
|
}
|
||||||
printer.print(aut, timer, nullptr, haut->filename.c_str(), -1,
|
printer.print(aut, timer, nullptr, haut->filename.c_str(), -1,
|
||||||
haut, prefix, suffix);
|
haut, prefix, suffix);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -970,7 +970,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
set_aliases(twa_ptr& g, std::vector<std::pair<std::string, bdd>> aliases)
|
set_aliases(twa_ptr g, std::vector<std::pair<std::string, bdd>> aliases)
|
||||||
{
|
{
|
||||||
if (aliases.empty())
|
if (aliases.empty())
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -61,5 +61,5 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// Pass an empty vector to remove existing aliases.
|
/// Pass an empty vector to remove existing aliases.
|
||||||
SPOT_API void
|
SPOT_API void
|
||||||
set_aliases(twa_ptr& g, std::vector<std::pair<std::string, bdd>> aliases);
|
set_aliases(twa_ptr g, std::vector<std::pair<std::string, bdd>> aliases);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2017, 2019, 2021 Laboratoire de Recherche et
|
# Copyright (C) 2017, 2019, 2021, 2022 Laboratoire de Recherche et
|
||||||
# Développement de l'Epita (LRDE).
|
# Développement de l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -72,6 +72,10 @@ HOA: v1
|
||||||
States: 10
|
States: 10
|
||||||
Start: 0&4
|
Start: 0&4
|
||||||
AP: 2 "p0" "p1"
|
AP: 2 "p0" "p1"
|
||||||
|
Alias: @a 0&!1
|
||||||
|
Alias: @b !0&!1
|
||||||
|
Alias: @c 0&1
|
||||||
|
Alias: @d !0&1
|
||||||
Acceptance: 2 Inf(0) | Inf(1)
|
Acceptance: 2 Inf(0) | Inf(1)
|
||||||
properties: trans-labels explicit-labels trans-acc univ-branch
|
properties: trans-labels explicit-labels trans-acc univ-branch
|
||||||
--BODY--
|
--BODY--
|
||||||
|
|
@ -104,7 +108,8 @@ State: 9
|
||||||
[!0] 9
|
[!0] 9
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
autfilt --dualize <input2 >output2
|
autfilt --dualize --aliases=drop <input2 >output2
|
||||||
|
autfilt --dualize <input2 >>output2
|
||||||
cat >expected2<<EOF
|
cat >expected2<<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 9
|
States: 9
|
||||||
|
|
@ -140,5 +145,43 @@ State: 8
|
||||||
[!1] 0&6&7
|
[!1] 0&6&7
|
||||||
[!0&!1] 0&7
|
[!0&!1] 0&7
|
||||||
--END--
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 9
|
||||||
|
Start: 8
|
||||||
|
AP: 2 "p0" "p1"
|
||||||
|
acc-name: co-Buchi
|
||||||
|
Acceptance: 1 Fin(0)
|
||||||
|
properties: trans-labels explicit-labels state-acc univ-branch
|
||||||
|
Alias: @a 0&!1
|
||||||
|
Alias: @b !0&!1
|
||||||
|
Alias: @c 0&1
|
||||||
|
Alias: @d !@c&!@b&!@a
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[@a] 0&6&7
|
||||||
|
[@b] 0&7
|
||||||
|
State: 1
|
||||||
|
[@c | @a] 1&2&3
|
||||||
|
[@d | @b] 1&3
|
||||||
|
State: 2
|
||||||
|
[@c | @a] 4
|
||||||
|
State: 3
|
||||||
|
[@c | @a] 4
|
||||||
|
[@d | @b] 5
|
||||||
|
State: 4
|
||||||
|
[t] 4
|
||||||
|
State: 5
|
||||||
|
[@d | @b] 5
|
||||||
|
State: 6 {0}
|
||||||
|
[@d | @b] 4
|
||||||
|
[@c | @a] 6
|
||||||
|
State: 7
|
||||||
|
[@b | @a] 7
|
||||||
|
State: 8
|
||||||
|
[t] 1&2&3
|
||||||
|
[@d | @b] 1&3
|
||||||
|
[@b | @a] 0&6&7
|
||||||
|
[@b] 0&7
|
||||||
|
--END--
|
||||||
EOF
|
EOF
|
||||||
diff output2 expected2
|
diff output2 expected2
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue