Commit acb67c1b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: add a --sbacc option

... to force automata into state-based acceptance.

* src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh,
src/tgbatest/sbacc.test: New files.
* src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am: Add
them.
* src/tgba/tgbagraph.hh (copy_acceptance_conditions_of):
Call set_acceptance_conditions().
* src/bin/autfilt.cc: Add option --sbacc.
parent cbee5c1a
......@@ -47,6 +47,7 @@
#include "tgbaalgos/are_isomorphic.hh"
#include "tgbaalgos/canonicalize.hh"
#include "tgbaalgos/mask.hh"
#include "tgbaalgos/sbacc.hh"
static const char argp_program_doc[] ="\
......@@ -74,6 +75,7 @@ Exit status:\n\
#define OPT_IS_EMPTY 15
#define OPT_INTERSECT 16
#define OPT_MASK_ACC 17
#define OPT_SBACC 18
static const argp_option options[] =
{
......@@ -105,6 +107,9 @@ static const argp_option options[] =
{ "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 },
{ "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
"remove all transitions in specified acceptance sets", 0 },
{ "state-based-acceptance", OPT_SBACC, 0, 0,
"define the acceptance using states", 0 },
{ "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
/**************************************************/
{ 0, 0, 0, 0, "Filtering options:", 6 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
......@@ -172,6 +177,7 @@ static int opt_max_count = -1;
static bool opt_destut = false;
static char opt_instut = 0;
static bool opt_is_empty = false;
static bool opt_sbacc = false;
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
static spot::acc_cond::mark_t opt_mask_acc = 0U;
......@@ -299,6 +305,9 @@ parse_opt(int key, char* arg, struct argp_state*)
randomize_st = true;
}
break;
case OPT_SBACC:
opt_sbacc = true;
break;
case OPT_SEED:
opt_seed = to_int(arg);
break;
......@@ -399,6 +408,9 @@ namespace
if (opt_product)
aut = spot::product(std::move(aut), opt_product);
if (opt_sbacc)
aut = spot::sbacc(aut);
aut = post.run(aut, nullptr);
if (randomize_st || randomize_tr)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
// l'Epita.
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
......@@ -429,8 +429,7 @@ namespace spot
/// \brief Copy the acceptance conditions of another tgba.
void copy_acceptance_conditions_of(const const_tgba_ptr& a)
{
assert(acc_.num_sets() == 0);
acc_.add_sets(a->acc().num_sets());
set_acceptance_conditions(a->acc().num_sets());
}
void copy_ap_of(const const_tgba_ptr& a)
......
......@@ -64,6 +64,7 @@ tgbaalgos_HEADERS = \
relabel.hh \
replayrun.hh \
safety.hh \
sbacc.hh \
sccfilter.hh \
scc.hh \
sccinfo.hh \
......@@ -115,6 +116,7 @@ libtgbaalgos_la_SOURCES = \
replayrun.cc \
relabel.cc \
safety.cc \
sbacc.cc \
scc.cc \
sccinfo.cc \
sccfilter.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 <vector>
#include <map>
#include <utility>
#include "sbacc.hh"
namespace spot
{
tgba_digraph_ptr sbacc(tgba_digraph_ptr& old)
{
if (old->has_state_based_acc())
return old;
auto res = make_tgba_digraph(old->get_dict());
res->copy_ap_of(old);
res->copy_acceptance_conditions_of(old);
typedef std::pair<unsigned, acc_cond::mark_t> pair_t;
std::map<pair_t, unsigned> s2n;
std::vector<std::pair<pair_t, unsigned>> todo;
auto new_state =
[&](unsigned state, acc_cond::mark_t m) -> unsigned
{
pair_t x(state, m);
auto p = s2n.emplace(x, 0);
if (p.second) // This is a new state
{
unsigned s = res->new_state();
p.first->second = s;
todo.emplace_back(x, s);
}
return p.first->second;
};
// Find any transition going into the initial state, and use its
// acceptance as mark.
acc_cond::mark_t init_acc = 0U;
unsigned old_init = old->get_init_state_number();
for (auto& t: old->transitions())
if (t.dst == old_init)
{
init_acc = t.acc;
break;
}
res->set_init_state(new_state(old_init, init_acc));
while (!todo.empty())
{
auto one = todo.back();
todo.pop_back();
for (auto& t: old->out(one.first.first))
res->new_transition(one.second,
new_state(t.dst, t.acc),
t.cond,
one.first.second);
}
return res;
}
}
// -*- 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/>.
#ifndef SPOT_TGBAALGOS_SBACC_HH
# define SPOT_TGBAALGOS_SBACC_HH
#include "tgba/tgbagraph.hh"
namespace spot
{
/// \brief Transform an automaton to use state-based acceptance
///
/// This is independent on the acceptance condition used.
SPOT_API tgba_digraph_ptr sbacc(tgba_digraph_ptr& aut);
}
#endif // SPOT_TGBAALGOS_COMPLETE_HH
......@@ -112,6 +112,7 @@ TESTS = \
randtgba.test \
isomorph.test \
uniq.test \
sbacc.test \
stutter.test \
emptchk.test \
emptchke.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 || exit 1
set -e
ltl2tgba=../../bin/ltl2tgba
autfilt=../../bin/autfilt
$ltl2tgba 'GFa & GFb' -H | run 0 $autfilt --sbacc -H > out.hoa
cat >expected<<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc complete deterministic
--BODY--
State: 0 {0 1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 1
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 2 {1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 3 {0}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
--END--
EOF
diff out.hoa expected
cat >in.hoa<<EOF
HOA: v1
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0
[0] 1
State: 1 {0}
[0] 2
State: 2
[0] 0 {1}
--END--
EOF
run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa
cat >expected <<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {1}
[0] 1
State: 1
[0] 2
State: 2 {0}
[0] 0
--END--
EOF
diff out.hoa expected
$autfilt --sba -H expected > out.hoa
diff out.hoa expected
../../bin/randltl --weak-fairness -n 20 2 |
../../bin/ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O"
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