new transformation from Fin-less to TGBA
Fixes #72. * src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Generic output type, and call to_generalized_buchi() if this type is not selected. * src/tgbatest/remfin.test: Add some tests. * src/bin/autfilt.cc: Add a --generic option, and set it by default.
This commit is contained in:
Alexandre Duret-Lutz
parent
16204e8e61
commit
e589e208bd
7 changed files with 296 additions and 3 deletions
|
|
@ -74,6 +74,7 @@ enum {
|
|||
OPT_DNF_ACC,
|
||||
OPT_EDGES,
|
||||
OPT_EXCLUSIVE_AP,
|
||||
OPT_GENERIC,
|
||||
OPT_INSTUT,
|
||||
OPT_INTERSECT,
|
||||
OPT_IS_COMPLETE,
|
||||
|
|
@ -102,8 +103,10 @@ static const argp_option options[] =
|
|||
"process the automaton in FILENAME", 0 },
|
||||
/**************************************************/
|
||||
{ 0, 0, 0, 0, "Output automaton type:", 2 },
|
||||
{ "generic", OPT_GENERIC, 0, 0,
|
||||
"Any acceptance is allowed (default)", 0 },
|
||||
{ "tgba", OPT_TGBA, 0, 0,
|
||||
"Transition-based Generalized Büchi Automaton (default)", 0 },
|
||||
"Transition-based Generalized Büchi Automaton", 0 },
|
||||
{ "ba", 'B', 0, 0, "Büchi Automaton", 0 },
|
||||
{ "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
|
||||
"of the given property)", 0 },
|
||||
|
|
@ -310,6 +313,8 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
case OPT_EXCLUSIVE_AP:
|
||||
excl_ap.add_group(arg);
|
||||
break;
|
||||
case OPT_GENERIC:
|
||||
type = spot::postprocessor::Generic;
|
||||
case OPT_INSTUT:
|
||||
if (!arg || (arg[0] == '1' && arg[1] == 0))
|
||||
opt_instut = 1;
|
||||
|
|
@ -423,6 +428,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
if (automaton_format == Spin)
|
||||
error(2, 0, "--spin and --tgba are incompatible");
|
||||
type = spot::postprocessor::TGBA;
|
||||
opt_rem_fin = true;
|
||||
break;
|
||||
case ARGP_KEY_ARG:
|
||||
jobs.emplace_back(arg, true);
|
||||
|
|
@ -621,6 +627,7 @@ main(int argc, char** argv)
|
|||
// Disable post-processing as much as possible by default.
|
||||
level = spot::postprocessor::Low;
|
||||
pref = spot::postprocessor::Any;
|
||||
type = spot::postprocessor::Generic;
|
||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
|
||||
exit(err);
|
||||
|
||||
|
|
|
|||
|
|
@ -78,6 +78,7 @@ tgbaalgos_HEADERS = \
|
|||
stutter.hh \
|
||||
tau03.hh \
|
||||
tau03opt.hh \
|
||||
totgba.hh \
|
||||
translate.hh \
|
||||
word.hh
|
||||
|
||||
|
|
@ -133,6 +134,7 @@ libtgbaalgos_la_SOURCES = \
|
|||
stutter.cc \
|
||||
tau03.cc \
|
||||
tau03opt.cc \
|
||||
totgba.cc \
|
||||
translate.cc \
|
||||
weight.cc \
|
||||
weight.hh \
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@
|
|||
#include "dtbasat.hh"
|
||||
#include "dtgbasat.hh"
|
||||
#include "complete.hh"
|
||||
#include "totgba.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -140,8 +141,12 @@ namespace spot
|
|||
tgba_digraph_ptr
|
||||
postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f)
|
||||
{
|
||||
if (type_ != Generic && !a->acc().is_generalized_buchi())
|
||||
a = to_generalized_buchi(a);
|
||||
|
||||
if (PREF_ == Any && level_ == Low)
|
||||
if (type_ == TGBA
|
||||
if (type_ == Generic
|
||||
|| type_ == TGBA
|
||||
|| (type_ == BA && a->is_sba())
|
||||
|| (type_ == Monitor && a->acc().num_sets() == 0))
|
||||
{
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ namespace spot
|
|||
/// options used for debugging or benchmarking.
|
||||
postprocessor(const option_map* opt = 0);
|
||||
|
||||
enum output_type { TGBA, BA, Monitor };
|
||||
enum output_type { TGBA, BA, Monitor, Generic };
|
||||
void
|
||||
set_type(output_type type)
|
||||
{
|
||||
|
|
|
|||
94
src/tgbaalgos/totgba.cc
Normal file
94
src/tgbaalgos/totgba.cc
Normal file
|
|
@ -0,0 +1,94 @@
|
|||
// -*- 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 "totgba.hh"
|
||||
#include "remfin.hh"
|
||||
#include "cleanacc.hh"
|
||||
#include "tgba/tgbagraph.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
typedef std::vector<acc_cond::mark_t> terms_t;
|
||||
|
||||
terms_t cnf_terms(const acc_cond::acc_code& code)
|
||||
{
|
||||
assert(!code.empty());
|
||||
terms_t res;
|
||||
auto pos = &code.back();
|
||||
auto end = &code.front();
|
||||
if (pos->op == acc_cond::acc_op::And)
|
||||
--pos;
|
||||
while (pos >= end)
|
||||
{
|
||||
auto term_end = pos - 1 - pos->size;
|
||||
if (pos->op == acc_cond::acc_op::Or)
|
||||
--pos;
|
||||
acc_cond::mark_t m = 0U;
|
||||
while (pos > term_end)
|
||||
{
|
||||
assert(pos->op == acc_cond::acc_op::Inf);
|
||||
m |= pos[-1].mark;
|
||||
pos -= 2;
|
||||
}
|
||||
res.push_back(m);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
/// \brief Take an automaton with any acceptance condition and return
|
||||
/// an equivalent Generalized Büchi automaton.
|
||||
tgba_digraph_ptr
|
||||
to_generalized_buchi(const const_tgba_digraph_ptr& aut)
|
||||
{
|
||||
auto res = remove_fin(cleanup_acceptance(aut));
|
||||
if (res->acc().is_generalized_buchi())
|
||||
return res;
|
||||
|
||||
auto cnf = res->get_acceptance().to_cnf();
|
||||
// If we are very lucky, building a CNF actually gave us a GBA...
|
||||
if (cnf.empty() ||
|
||||
(cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin))
|
||||
{
|
||||
res->set_acceptance(res->acc().num_sets(), cnf);
|
||||
cleanup_acceptance_here(res);
|
||||
return res;
|
||||
}
|
||||
|
||||
auto terms = cnf_terms(cnf);
|
||||
unsigned nterms = terms.size();
|
||||
assert(nterms > 0);
|
||||
res->set_generalized_buchi(nterms);
|
||||
|
||||
for (auto& t: res->transitions())
|
||||
{
|
||||
acc_cond::mark_t cur_m = t.acc;
|
||||
acc_cond::mark_t new_m = 0U;
|
||||
for (unsigned n = 0; n < nterms; ++n)
|
||||
if (cur_m & terms[n])
|
||||
new_m.set(n);
|
||||
t.acc = new_m;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
}
|
||||
30
src/tgbaalgos/totgba.hh
Normal file
30
src/tgbaalgos/totgba.hh
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
// -*- 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 "tgba/tgbagraph.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Take an automaton with any acceptance condition and return
|
||||
/// an equivalent Generalized Büchi automaton.
|
||||
SPOT_API tgba_digraph_ptr
|
||||
to_generalized_buchi(const const_tgba_digraph_ptr& aut);
|
||||
}
|
||||
|
|
@ -308,6 +308,161 @@ State: 9 {1}
|
|||
--END--
|
||||
EOF
|
||||
|
||||
cat >expected-tgba <<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[0&1] 0
|
||||
[!0&!1] 0
|
||||
[!0&1] 0
|
||||
[0&!1] 0
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
State: 1 {0}
|
||||
[!0&!1] 1
|
||||
[!0&1] 1
|
||||
State: 2 {0}
|
||||
[!0&!1] 2
|
||||
[0&!1] 2
|
||||
--END--
|
||||
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
|
||||
[t] 0 {0 1}
|
||||
[0] 1 {0 1}
|
||||
[!0] 2 {0 1}
|
||||
State: 1
|
||||
[1] 0 {1}
|
||||
[0&1] 1 {1}
|
||||
[!0&1] 2 {0 1}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[0&!1] 1
|
||||
[!0&!1] 2
|
||||
[!0&!1] 3
|
||||
State: 3
|
||||
[!0&!1] 3 {0 1}
|
||||
--END--
|
||||
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
|
||||
[t] 0 {1}
|
||||
[0] 1 {1}
|
||||
[!0] 2 {0 1}
|
||||
State: 1
|
||||
[1] 0 {1}
|
||||
[0&1] 1 {0 1}
|
||||
[!0&1] 2 {0 1}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[0&!1] 1 {0 1}
|
||||
[!0&!1] 2 {0 1}
|
||||
[!0&!1] 3 {0 1}
|
||||
State: 3
|
||||
[!0&!1] 3 {0 1}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 0
|
||||
Acceptance: 0 f
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[t] 0
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "p0"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 0
|
||||
[0] 1
|
||||
State: 1 {0}
|
||||
[!0] 1
|
||||
[0] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 10
|
||||
Start: 2
|
||||
AP: 1 "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 6
|
||||
[0] 0
|
||||
[0] 8
|
||||
[0] 9
|
||||
State: 1 {0}
|
||||
[!0] 3
|
||||
[0] 3
|
||||
State: 2 {0}
|
||||
[!0] 5
|
||||
[0] 1
|
||||
State: 3 {0}
|
||||
[!0] 6
|
||||
[0] 0
|
||||
State: 4 {0}
|
||||
[!0] 6
|
||||
[0] 4
|
||||
State: 5 {0}
|
||||
[!0] 7
|
||||
[0] 3
|
||||
State: 6
|
||||
[!0] 6
|
||||
[0] 0
|
||||
State: 7 {0}
|
||||
[!0] 6
|
||||
[0] 4
|
||||
State: 8
|
||||
[0] 8
|
||||
State: 9 {0}
|
||||
[0] 9
|
||||
--END--
|
||||
EOF
|
||||
|
||||
run 0 $autfilt -H --remove-fin test1 > output
|
||||
cat output
|
||||
diff -u output expected
|
||||
|
||||
run 0 $autfilt -H --tgba test1 > output
|
||||
cat output
|
||||
diff -u output expected-tgba
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue