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

maskacc: Add a tgba_digraph version

* src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh: New files.
* src/tgbaalgos/Makefile.am: Adjust.
* src/tgba/acc.hh (mark_t::set): New method.
* src/bin/autfilt.cc: Add option --mask-acc.
* src/tgbatest/maskacc.test: Rewrite.
* src/tgbatest/maskacc.cc: Delete.
* src/tgbatest/Makefile.am: Adjust.
parent a0a035e0
......@@ -46,6 +46,7 @@
#include "tgbaalgos/randomize.hh"
#include "tgbaalgos/are_isomorphic.hh"
#include "tgbaalgos/canonicalize.hh"
#include "tgbaalgos/mask.hh"
static const char argp_program_doc[] ="\
......@@ -72,6 +73,7 @@ Exit status:\n\
#define OPT_INSTUT 14
#define OPT_IS_EMPTY 15
#define OPT_INTERSECT 16
#define OPT_MASK_ACC 17
static const argp_option options[] =
{
......@@ -125,6 +127,8 @@ static const argp_option options[] =
"keep automata whose number of edges are in RANGE", 0 },
{ "acc-sets", OPT_ACC_SETS, "RANGE", 0,
"keep automata whose number of acceptance sets are in RANGE", 0 },
{ "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
"remove all transitions in specified acceptance sets", 0 },
RANGE_DOC_FULL,
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
......@@ -169,6 +173,7 @@ static bool opt_destut = false;
static char opt_instut = 0;
static bool opt_is_empty = false;
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
static spot::acc_cond::mark_t opt_mask_acc = 0U;
static int
parse_opt(int key, char* arg, struct argp_state*)
......@@ -240,6 +245,28 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_MERGE:
opt_merge = true;
break;
case OPT_MASK_ACC:
{
while (*arg)
{
char* endptr;
long res = strtol(arg, &endptr, 10);
if (res < 0)
error(2, 0, "acceptance sets should be non-negative:"
" --mask-acc=%ld", res);
if (static_cast<unsigned long>(res)
> sizeof(spot::acc_cond::mark_t::value_t))
error(2, 0, "this implementation does not support that much"
" acceptance sets: --mask-acc=%ld", res);
opt_mask_acc.set(res);
if (endptr == arg)
error(2, 0, "failed to parse '%s' as an integer.", arg);
while (*endptr == ' ' || *endptr == ',')
++endptr;
arg = endptr;
}
break;
}
case OPT_PRODUCT:
{
auto a = read_automaton(arg, dict);
......@@ -359,6 +386,9 @@ namespace
// Postprocessing.
if (opt_mask_acc)
aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
if (opt_destut)
aut = spot::closure(std::move(aut));
if (opt_instut == 1)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
// l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -96,6 +96,11 @@ namespace spot
return id & (1U << u);
}
void set(unsigned u)
{
id |= (1U << u);
}
mark_t& operator&=(mark_t r)
{
id &= r.id;
......
......@@ -50,6 +50,7 @@ tgbaalgos_HEADERS = \
ltl2taa.hh \
ltl2tgba_fm.hh \
magic.hh \
mask.hh \
minimize.hh \
neverclaim.hh \
postproc.hh \
......@@ -100,6 +101,7 @@ libtgbaalgos_la_SOURCES = \
ltl2taa.cc \
ltl2tgba_fm.cc \
magic.cc \
mask.cc \
minimize.cc \
ndfs_result.hxx \
neverclaim.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Développement
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -17,51 +17,31 @@
// 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 <iostream>
#include <cassert>
#include <cstdlib>
#include "tgbaparse/public.hh"
#include "tgbaalgos/save.hh"
#include "tgba/tgbamask.hh"
#include "ltlast/allnodes.hh"
#include "mask.hh"
void
syntax(char* prog)
namespace spot
{
std::cerr << prog << " file" << std::endl;
exit(2);
}
int
main(int argc, char** argv)
{
int exit_code = 0;
if (argc != 2)
syntax(argv[0]);
tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in,
acc_cond::mark_t to_remove)
{
auto dict = spot::make_bdd_dict();
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
auto aut = spot::tgba_parse(argv[1], pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel))
return 2;
unsigned nsets = aut->acc().num_sets();
for (unsigned n = 0; n < nsets; ++n)
{
auto masked = spot::build_tgba_mask_acc_ignore(aut, n);
spot::tgba_save_reachable(std::cout, masked);
}
auto& inacc = in->acc();
auto res = make_tgba_digraph(in->get_dict());
res->copy_ap_of(in);
res->prop_copy(in, { true, false, true, true });
unsigned na = inacc.num_sets();
unsigned tr = to_remove.count();
assert(tr <= na);
res->set_acceptance_conditions(na - tr);
transform_mask(in, res, [&](bdd& cond,
acc_cond::mark_t& acc,
unsigned)
{
if (acc & to_remove)
cond = bddfalse;
else
acc = inacc.strip(acc, to_remove);
});
return res;
}
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
assert(spot::ltl::bunop::instance_count() == 0);
assert(spot::ltl::atomic_prop::instance_count() == 0);
return exit_code;
}
// -*- 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/>.
#ifndef SPOT_TGBAALGOS_MASK_HH
# define SPOT_TGBAALGOS_MASK_HH
#include "tgba/tgbagraph.hh"
namespace spot
{
/// \brief Clone and mask an automaton.
///
/// Copy the transition of the automaton \a old, into the automaton
/// \a cpy, creating new states at the same time. The argument \a
/// trans should behave as a fonction with the following prototype:
/// <code>
/// void (*trans) (bdd& cond, acc_cond::mark_t& acc, unsigned dst)
/// </code>
/// It can modify either the condition or the acceptance sets of
/// the transitions. Set the condition to bddfalse to remove it
/// (this will also remove the destination state and its descendants
/// if they are not reachable by another transition).
template<typename Trans>
void transform_mask(const const_tgba_digraph_ptr& old,
tgba_digraph_ptr& cpy,
Trans trans)
{
std::vector<unsigned> todo;
std::vector<unsigned> seen(old->num_states(), -1U);
auto new_state =
[&](unsigned old_state) -> unsigned
{
unsigned tmp = seen[old_state];
if (tmp == -1U)
{
tmp = cpy->new_state();
seen[old_state] = tmp;
todo.push_back(old_state);
}
return tmp;
};
new_state(old->get_init_state_number());
while (!todo.empty())
{
unsigned old_src = todo.back();
todo.pop_back();
unsigned new_src = seen[old_src];
assert(new_src != -1U);
for (auto& t: old->out(old_src))
{
bdd cond = t.cond;
acc_cond::mark_t acc = t.acc;
trans(cond, acc, t.dst);
if (cond != bddfalse)
cpy->new_transition(new_src,
new_state(t.dst),
cond, acc);
}
}
}
/// \brief Remove all transitions that are in some given acceptance sets.
SPOT_API
tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in,
acc_cond::mark_t to_remove);
}
#endif // SPOT_TGBAALGOS_MASK_HH
......@@ -40,7 +40,6 @@ check_PROGRAMS = \
intvcomp \
intvcmp2 \
ltlprod \
maskacc \
readsat \
taatgba
......@@ -55,7 +54,6 @@ intvcomp_SOURCES = intvcomp.cc
intvcmp2_SOURCES = intvcmp2.cc
ltl2tgba_SOURCES = ltl2tgba.cc
ltlprod_SOURCES = ltlprod.cc
maskacc_SOURCES = maskacc.cc
randtgba_SOURCES = randtgba.cc
readsat_SOURCES = readsat.cc
taatgba_SOURCES = taatgba.cc
......
......@@ -24,28 +24,94 @@
set -e
cat >input1 <<EOF
acc = A B;
s1, s2, "a", A;
s1, s3, "b", B;
s2, s3, "a",;
s3, s2, "b",;
s2, s4, "a", B;
s3, s4, "b", A;
s4, s4, "a", A B;
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 trans-acc
--BODY--
State: 0
[0] 1 {0}
[1] 2 {1}
State: 1
[0] 2
[0] 3 {1}
State: 2
[1] 1
[1] 3 {0}
State: 3
[0] 3 {0 1}
--END--
EOF
cat >expect1 <<EOF
acc = "0" "1";
"0", "2", "b", "1";
"2", "1", "b",;
"1", "2", "a",;
"1", "3", "a", "1";
acc = "0" "1";
"0", "1", "a", "0";
"1", "2", "a",;
"2", "1", "b",;
"2", "3", "b", "0";
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[1] 1 {0}
State: 1
[1] 2
State: 2
[0] 1
[0] 3 {0}
State: 3
--END--
EOF
run 0 ../maskacc input1 | tee stdout
diff stdout expect1
run 0 ../../bin/autfilt --mask-acc=0 input1 -H >output
diff output expect1
cat >expect2 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1 {0}
State: 1
[0] 2
State: 2
[1] 1
[1] 3 {0}
State: 3
--END--
EOF
run 0 ../../bin/autfilt --mask-acc=1 input1 -H >output
diff output expect2
cat >expect3 <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
--END--
EOF
run 0 ../../bin/autfilt --mask-acc=0,1,2 input1 -H >output
diff output expect3
run 0 ../../bin/autfilt --mask-acc=0 --mask-acc=1 input1 -H >output
diff output expect3
# Errors
run 2 ../../bin/autfilt --mask-acc=a3 input1
run 2 ../../bin/autfilt --mask-acc=3-2 input1
run 2 ../../bin/autfilt --mask-acc=0,9999,1 input1
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