Commit 14bee1ae authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

implement conversion to GRA and GSA

Fixes #174.

* spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
(to_generalized_streett, to_generalized_rabin): New functions.
* spot/twa/acc.hh: Declare more methods as static.
* bin/autfilt.cc: Implement --generalized-rabin and
--generalized-streett options.
* NEWS: Mention these.
* tests/core/gragsa.test: New file.
* tests/Makefile.am: Add it.
parent 73600305
......@@ -82,6 +82,9 @@ New in spot 2.0.3a (not yet released)
--highlight-word=[NUM,]WORD option. However currently this only
work on automata with Fin-less acceptance.
* autfilt learned two options --generalized-rabin and
--generalized-streett to convert the acceptance conditions.
* genltl learned three new families: --dac-patterns=1..45,
--eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options
these do not output scalable patterns, but simply a list of formulas
......@@ -127,6 +130,10 @@ New in spot 2.0.3a (not yet released)
and pushing acceptance marks common to all incoming edges) to
reduce the number of additional states needed.
* to_generalized_rabin() and to_generalized_streett() are two new
functions that convert the acceptance condition as requested
without changing the transition structure.
* language_containment_checker now has default values for all
parameters of its constructor.
......
......@@ -27,6 +27,7 @@
#include <argp.h>
#include "error.h"
#include "argmatch.h"
#include "common_setup.hh"
#include "common_finput.hh"
......@@ -62,6 +63,7 @@
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/totgba.hh>
static const char argp_program_doc[] ="\
Convert, transform, and filter omega-automata.\v\
......@@ -88,7 +90,8 @@ enum {
OPT_EDGES,
OPT_EQUIVALENT_TO,
OPT_EXCLUSIVE_AP,
OPT_GENERIC,
OPT_GENERALIZED_RABIN,
OPT_GENERALIZED_STREETT,
OPT_HIGHLIGHT_NONDET,
OPT_HIGHLIGHT_NONDET_EDGES,
OPT_HIGHLIGHT_NONDET_STATES,
......@@ -252,6 +255,20 @@ static const argp_option options[] =
"put the acceptance condition in Conjunctive Normal Form", 0 },
{ "remove-fin", OPT_REM_FIN, nullptr, 0,
"rewrite the automaton without using Fin acceptance", 0 },
{ "generalized-rabin", OPT_GENERALIZED_RABIN,
"unique-inf|share-inf", OPTION_ARG_OPTIONAL,
"rewrite the acceptance condition as generalized Rabin; the default "
"\"unique-inf\" option uses the generalized Rabin definition from the "
"HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
"therefore reducing the number of sets", 0 },
{ "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "generalized-streett", OPT_GENERALIZED_STREETT,
"unique-fin|share-fin", OPTION_ARG_OPTIONAL,
"rewrite the acceptance condition as generalized Streett;"
" the \"share-fin\" option allows clauses to share Fin sets,"
" therefore reducing the number of sets; the default"
" \"unique-fin\" does not", 0 },
{ "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
"remove unused acceptance sets from the automaton", 0 },
{ "complement", OPT_COMPLEMENT, nullptr, 0,
......@@ -329,6 +346,7 @@ static const struct argp_child children[] =
{ nullptr, 0, nullptr, 0 }
};
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
typedef std::set<std::vector<tr_t>> unique_aut_t;
static long int match_count = 0;
......@@ -337,6 +355,30 @@ static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
static gra_type opt_gra = GRA_NO;
static char const *const gra_args[] =
{
"default", "share-inf", "hoa", "unique-inf", nullptr
};
static gra_type const gra_types[] =
{
GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
};
ARGMATCH_VERIFY(gra_args, gra_types);
enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 };
static gsa_type opt_gsa = GSA_NO;
static char const *const gsa_args[] =
{
"default", "share-fin", "unique-fin", nullptr
};
static gsa_type const gsa_types[] =
{
GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN
};
ARGMATCH_VERIFY(gsa_args, gsa_types);
// We want all these variables to be destroyed when we exit main, to
// make sure it happens before all other global variables (like the
// atomic propositions maps) are destroyed. Otherwise we risk
......@@ -517,6 +559,20 @@ parse_opt(int key, char* arg, struct argp_state*)
opt->equivalent_neg =
spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos));
break;
case OPT_GENERALIZED_RABIN:
if (arg)
opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
else
opt_gra = GRA_UNIQUE_INF;
opt_gsa = GSA_NO;
break;
case OPT_GENERALIZED_STREETT:
if (arg)
opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
else
opt_gsa = GSA_UNIQUE_FIN;
opt_gra = GRA_NO;
break;
case OPT_HIGHLIGHT_NONDET:
{
int v = arg ? to_pos_int(arg) : 1;
......@@ -1013,6 +1069,11 @@ namespace
aut = post.run(aut, nullptr);
if (opt_gra)
aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF);
if (opt_gsa)
aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN);
if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
aut = opt->excl_ap.constrain(aut, true);
else if (opt_rem_unused_ap) // constrain(aut, true) already does that
......
......@@ -1056,42 +1056,42 @@ namespace spot
bool check_fin_acceptance() const;
public:
acc_code inf(mark_t mark) const
static acc_code inf(mark_t mark)
{
return acc_code::inf(mark);
}
acc_code inf(std::initializer_list<unsigned> vals) const
static acc_code inf(std::initializer_list<unsigned> vals)
{
return inf(mark_t(vals.begin(), vals.end()));
}
acc_code inf_neg(mark_t mark) const
static acc_code inf_neg(mark_t mark)
{
return acc_code::inf_neg(mark);
}
acc_code inf_neg(std::initializer_list<unsigned> vals) const
static acc_code inf_neg(std::initializer_list<unsigned> vals)
{
return inf_neg(mark_t(vals.begin(), vals.end()));
}
acc_code fin(mark_t mark) const
static acc_code fin(mark_t mark)
{
return acc_code::fin(mark);
}
acc_code fin(std::initializer_list<unsigned> vals) const
static acc_code fin(std::initializer_list<unsigned> vals)
{
return fin(mark_t(vals.begin(), vals.end()));
}
acc_code fin_neg(mark_t mark) const
static acc_code fin_neg(mark_t mark)
{
return acc_code::fin_neg(mark);
}
acc_code fin_neg(std::initializer_list<unsigned> vals) const
static acc_code fin_neg(std::initializer_list<unsigned> vals)
{
return fin_neg(mark_t(vals.begin(), vals.end()));
}
......
......@@ -329,7 +329,7 @@ namespace spot
// Handle false specifically. We want the output
// an automaton with Acceptance: t, that has a single
// state without successor.
if (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin)
if (cnf.is_f())
{
assert(cnf.front().mark == 0U);
res = make_twa_graph(aut->get_dict());
......@@ -357,4 +357,203 @@ namespace spot
}
return res;
}
namespace
{
// If the DNF is
// Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) |
// Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4)
// this returns the following vector of pairs:
// [({1}, {2,4})
// ({2,3}, {1}),
// ({}, {1,3}),
// ({}, {2}),
// ({4}, t)]
static std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
split_dnf_acc(const acc_cond::acc_code& acc)
{
std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>> res;
if (acc.empty())
{
res.emplace_back(0U, 0U);
return res;
}
auto pos = &acc.back();
if (pos->op == acc_cond::acc_op::Or)
--pos;
auto start = &acc.front();
while (pos > start)
{
if (pos->op == acc_cond::acc_op::Fin)
{
// We have only a Fin term, without Inf. In this case
// only, the Fin() may encode a disjunction of sets.
for (auto s: pos[-1].mark.sets())
res.emplace_back(acc_cond::mark_t({s}), 0U);
pos -= pos->size + 1;
}
else
{
// We have a conjunction of Fin and Inf sets.
auto end = pos - pos->size - 1;
acc_cond::mark_t fin = 0U;
acc_cond::mark_t inf = 0U;
while (pos > end)
{
switch (pos->op)
{
case acc_cond::acc_op::And:
--pos;
break;
case acc_cond::acc_op::Fin:
fin |= pos[-1].mark;
assert(pos[-1].mark.count() == 1);
pos -= 2;
break;
case acc_cond::acc_op::Inf:
inf |= pos[-1].mark;
pos -= 2;
break;
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
case acc_cond::acc_op::Or:
SPOT_UNREACHABLE();
break;
}
}
assert(pos == end);
res.emplace_back(fin, inf);
}
}
return res;
}
static twa_graph_ptr
to_generalized_rabin_aux(const const_twa_graph_ptr& aut,
bool share_inf, bool complement)
{
auto res = cleanup_acceptance(aut);
auto oldacc = res->get_acceptance();
if (complement)
res->set_acceptance(res->acc().num_sets(), oldacc.complement());
{
std::vector<unsigned> pairs;
if (res->acc().is_generalized_rabin(pairs))
{
if (complement)
res->set_acceptance(res->acc().num_sets(), oldacc);
return res;
}
}
auto dnf = res->get_acceptance().to_dnf();
if (dnf.is_f())
{
if (complement)
res->set_acceptance(0, acc_cond::acc_code::t());
return res;
}
auto v = split_dnf_acc(dnf);
// Decide how we will rename each input set.
//
// inf_rename is only used if hoa_style=false, to
// reuse previously used Inf sets.
unsigned ns = res->num_sets();
std::vector<acc_cond::mark_t> rename(ns);
std::vector<unsigned> inf_rename(ns);
unsigned next_set = 0;
// The output acceptance conditions.
acc_cond::acc_code code =
complement ? acc_cond::acc_code::t() : acc_cond::acc_code::f();
for (auto& i: v)
{
unsigned fin_set = 0U;
if (!complement)
{
for (auto s: i.first.sets())
rename[s].set(next_set);
fin_set = next_set++;
}
acc_cond::mark_t infsets = 0U;
if (share_inf)
for (auto s: i.second.sets())
{
unsigned n = inf_rename[s];
if (n == 0)
n = inf_rename[s] = next_set++;
rename[s].set(n);
infsets.set(n);
}
else // HOA style
{
for (auto s: i.second.sets())
{
unsigned n = next_set++;
rename[s].set(n);
infsets.set(n);
}
}
// The definition of Streett wants the Fin first in clauses,
// so we do the same for generalized Streett since HOA does
// not specify anything. See
// https://github.com/adl/hoaf/issues/62
if (complement)
{
for (auto s: i.first.sets())
rename[s].set(next_set);
fin_set = next_set++;
auto pair = acc_cond::inf({fin_set});
pair |= acc_cond::acc_code::fin(infsets);
pair &= std::move(code);
code = std::move(pair);
}
else
{
auto pair = acc_cond::acc_code::inf(infsets);
pair &= acc_cond::fin({fin_set});
pair |= std::move(code);
code = std::move(pair);
}
}
// Fix the automaton
res->set_acceptance(next_set, code);
for (auto& e: res->edges())
{
acc_cond::mark_t m = 0U;
for (auto s: e.acc.sets())
m |= rename[s];
e.acc = m;
}
return res;
}
}
twa_graph_ptr
to_generalized_rabin(const const_twa_graph_ptr& aut,
bool share_inf)
{
return to_generalized_rabin_aux(aut, share_inf, false);
}
twa_graph_ptr
to_generalized_streett(const const_twa_graph_ptr& aut,
bool share_fin)
{
return to_generalized_rabin_aux(aut, share_fin, true);
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -38,4 +38,32 @@ namespace spot
/// less than the number of pairs used by IN.
SPOT_API twa_graph_ptr
streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in);
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Rabin automaton.
///
/// This works by putting the acceptance condition in disjunctive
/// normal form, and then merging all the
/// Fin(x1)&Fin(x2)&...&Fin(xn) that may occur in clauses into a
/// single Fin(X).
///
/// The acceptance-set numbers used by Inf may appear in
/// multiple clauses if \a share_inf is set.
SPOT_API twa_graph_ptr
to_generalized_rabin(const const_twa_graph_ptr& aut,
bool share_inf = false);
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Streett automaton.
///
/// This works by putting the acceptance condition in cunjunctive
/// normal form, and then merging all the
/// Inf(x1)|Inf(x2)|...|Inf(xn) that may occur in clauses into a
/// single Inf(X).
///
/// The acceptance-set numbers used by Fin may appear in
/// multiple clauses if \a share_fin is set.
SPOT_API twa_graph_ptr
to_generalized_streett(const const_twa_graph_ptr& aut,
bool share_fin = false);
}
......@@ -207,6 +207,7 @@ TESTS_twa = \
core/complete.test \
core/complement.test \
core/remfin.test \
core/gragsa.test \
core/dstar.test \
core/readsave.test \
core/ltldo.test \
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 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
set -e
randltl -n 100 p1 p2 p3 --tree-size 5..15 --seed=200 |
ltlcross --timeout=60 \
"ltl2tgba %f > %T" \
"ltl2tgba -G -D %f > %T" \
"ltl2tgba -G -D %f | autfilt --gsa=unique-fin > %T" \
"ltl2tgba -G -D %f | autfilt --gra=unique-inf > %T" \
"ltl2tgba -G -D %f | autfilt --gsa=share-fin > %T" \
"ltl2tgba -G -D %f | autfilt --gra=share-inf > %T"
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