Commit 3d1ccdc4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: new --separate-sets option

* src/twaalgos/sepsets.cc, src/twaalgos/sepsets.hh: New files.
* src/twaalgos/Makefile.am: Add them.
* src/twa/acc.hh (get_acceptance): Add a non-const version.
* src/bin/autfilt.cc: Add the --separate-sets option.
* src/tests/sepsets.test: New file.
* src/tests/Makefile.am: Add it.
parent 5ed321fc
......@@ -51,6 +51,7 @@
#include "twaalgos/canonicalize.hh"
#include "twaalgos/mask.hh"
#include "twaalgos/sbacc.hh"
#include "twaalgos/sepsets.hh"
#include "twaalgos/stripacc.hh"
#include "twaalgos/remfin.hh"
#include "twaalgos/cleanacc.hh"
......@@ -93,6 +94,7 @@ enum {
OPT_REM_FIN,
OPT_SBACC,
OPT_SEED,
OPT_SEP_SETS,
OPT_SIMPLIFY_EXCLUSIVE_AP,
OPT_STATES,
OPT_STRIPACC,
......@@ -167,7 +169,9 @@ static const argp_option options[] =
{ "remove-dead-states", OPT_REM_DEAD, 0, 0,
"remove states that are unreachable, or that cannot belong to an "
"infinite path", 0 },
/**************************************************/
{ "separate-sets", OPT_SEP_SETS, 0, 0,
"if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
"Fin(x) by a new Fin(y) and adjust the automaton", 0 },
{ 0, 0, 0, 0, "Filtering options:", 6 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
"keep automata that are isomorphic to the automaton in FILENAME", 0 },
......@@ -262,6 +266,7 @@ static spot::remove_ap rem_ap;
static bool opt_simplify_exclusive_ap = false;
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
static bool opt_sep_sets = false;
static int
parse_opt(int key, char* arg, struct argp_state*)
......@@ -438,6 +443,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_SEED:
opt_seed = to_int(arg);
break;
case OPT_SEP_SETS:
opt_sep_sets = true;
break;
case OPT_SIMPLIFY_EXCLUSIVE_AP:
opt_simplify_exclusive_ap = true;
opt_merge = true;
......@@ -507,6 +515,8 @@ namespace
aut->merge_transitions();
if (opt_clean_acc || opt_rem_fin)
cleanup_acceptance_here(aut);
if (opt_sep_sets)
separate_sets_here(aut);
if (opt_complement_acc)
aut->set_acceptance(aut->acc().num_sets(),
aut->get_acceptance().complement());
......
......@@ -204,6 +204,7 @@ TESTS_twa = \
scc.test \
sccdot.test \
sccsimpl.test \
sepsets.test \
dbacomp.test \
obligation.test \
wdba.test \
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 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
cat >in <<EOF
HOA: v1
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 2 Fin(0)&Inf(1) | Fin(1)&Inf(0)
--BODY--
State: 0
[0] 0 {1}
[!0] 0 {0}
State: 1
[2] 0 {0}
[1&!2] 1 {1}
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2 {0 1}
--END--
EOF
cat >expected <<EOF
HOA: v1
States: 3
Start: 2
AP: 3 "a" "b" "c"
Acceptance: 4 (Fin(2) & Inf(1)) | (Fin(3) & Inf(0))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0] 0 {1 3}
[!0] 0 {0 2}
State: 1
[2] 0 {0 2}
[1&!2] 1 {1 3}
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2 {0 1 2 3}
--END--
EOF
run 0 ../../bin/autfilt --separate-sets in -H > out
diff out expected
......@@ -744,6 +744,11 @@ namespace spot
return code_;
}
acc_code& get_acceptance()
{
return code_;
}
bool uses_fin_acceptance() const
{
return uses_fin_acceptance_;
......
......@@ -73,6 +73,7 @@ twaalgos_HEADERS = \
scc.hh \
sccinfo.hh \
se05.hh \
sepsets.hh \
simulation.hh \
stats.hh \
stripacc.hh \
......@@ -130,6 +131,7 @@ libtwaalgos_la_SOURCES = \
sccinfo.cc \
sccfilter.cc \
se05.cc \
sepsets.cc \
simulation.cc \
stats.cc \
stripacc.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et
// Développement 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/>.
#include "sepsets.hh"
#include "sccinfo.hh"
namespace spot
{
namespace
{
static acc_cond::mark_t common_sets(const const_twa_graph_ptr& aut)
{
auto p = aut->get_acceptance().used_inf_fin_sets();
return p.first & p.second;
}
}
bool has_separate_sets(const const_twa_graph_ptr& aut)
{
return common_sets(aut) == 0U;
}
twa_graph_ptr
separate_sets_here(const twa_graph_ptr& aut)
{
auto common = common_sets(aut);
if (common == 0U)
return aut;
// Each Fin(first) should be replaced by Fin(second).
std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> map;
{
unsigned base = aut->acc().add_sets(common.count());
for (auto s: common.sets())
map.emplace_back(acc_cond::mark_t({s}),
acc_cond::mark_t({base++}));
}
// Fix the acceptance condition
auto& code = aut->acc().get_acceptance();
// If code were empty, then common would have been 0.
assert (!code.empty());
acc_cond::acc_word* pos = &code.back();
acc_cond::acc_word* start = &code.front();
while (pos > start)
{
switch (pos->op)
{
case acc_cond::acc_op::Or:
case acc_cond::acc_op::And:
--pos;
break;
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
if ((pos[-1].mark & common) == 0U)
break;
for (auto p: map)
if (pos[-1].mark & p.first)
{
pos[-1].mark -= p.first;
pos[-1].mark |= p.second;
}
/* fall through */
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
break;
}
}
// Fix the transitions
for (auto& t: aut->transitions())
{
if ((t.acc & common) == 0U)
continue;
for (auto p: map)
if (t.acc & p.first)
t.acc |= p.second;
}
return aut;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// 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/>.
#pragma once
#include "twa/twagraph.hh"
namespace spot
{
/// \brief Whether the Inf and Fin numbers are disjoints
SPOT_API bool
has_separate_sets(const const_twa_graph_ptr& aut);
/// \brief Separate the Fin and Inf sets used by an automaton
///
/// This makes sure that the numbers used a Fin and Inf are
/// disjoints.
SPOT_API twa_graph_ptr
separate_sets_here(const twa_graph_ptr& aut);
}
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