From a626a32dbcdfa9a553050500c18bb49be5272d47 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Dec 2014 09:35:52 +0100 Subject: [PATCH] autfilt: --instut, --destut, --is-empty * src/bin/autfilt.cc: Add these new options. * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Make it possible to call sl() and sl2() without passing the set of atomic propositions. * src/tgbatest/stutter.test: New file. * src/tgbatest/Makefile.am: Add it. --- src/bin/autfilt.cc | 28 +++++++++++++++++++++++++++ src/tgbaalgos/stutterize.cc | 19 +++++++++++++++++-- src/tgbaalgos/stutterize.hh | 6 +++--- src/tgbatest/Makefile.am | 1 + src/tgbatest/stutter.test | 38 +++++++++++++++++++++++++++++++++++++ 5 files changed, 87 insertions(+), 5 deletions(-) create mode 100755 src/tgbatest/stutter.test diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 4cc8aba3a..94d5f2091 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -40,6 +40,8 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/isdet.hh" +#include "tgbaalgos/stutterize.hh" +#include "tgbaalgos/closure.hh" #include "tgba/bddprint.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" @@ -75,6 +77,9 @@ Exit status:\n\ #define OPT_NAME 19 #define OPT_EDGES 20 #define OPT_ACC_SETS 21 +#define OPT_DESTUT 22 +#define OPT_INSTUT 23 +#define OPT_IS_EMPTY 24 static const argp_option options[] = { @@ -150,6 +155,8 @@ static const argp_option options[] = { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL, "randomize states and transitions (specify 's' or 't' to " "randomize only states or transitions)", 0 }, + { "instut", OPT_INSTUT, 0, 0, "allow more stuttering", 0 }, + { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filters:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -159,6 +166,8 @@ static const argp_option options[] = "the automaton is complete", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0, "the automaton is deterministic", 0 }, + { "is-empty", OPT_IS_EMPTY, 0, 0, + "keep automata with an empty language", 0 }, { "invert-match", 'v', 0, 0, "select non-matching automata", 0 }, { "states", OPT_STATES, "RANGE", 0, "keep automata whose number of states are in RANGE", 0 }, @@ -204,6 +213,9 @@ static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; static const char* opt_name = nullptr; static int opt_max_count = -1; +static bool opt_destut = false; +static bool opt_instut = false; +static bool opt_is_empty = false; static int to_int(const char* s) @@ -289,12 +301,21 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_INSTUT: + opt_instut = true; + break; + case OPT_DESTUT: + opt_destut = true; + break; case OPT_IS_COMPLETE: opt_is_complete = true; break; case OPT_IS_DETERMINISTIC: opt_is_deterministic = true; break; + case OPT_IS_EMPTY: + opt_is_empty = true; + break; case OPT_LBTT: if (arg) { @@ -526,6 +547,8 @@ namespace matched &= is_deterministic(aut); if (opt_are_isomorphic) matched &= !are_isomorphic(aut, opt_are_isomorphic).empty(); + if (opt_is_empty) + matched &= aut->is_empty(); // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) @@ -535,6 +558,11 @@ namespace // Postprocessing. + if (opt_destut) + aut = spot::closure(std::move(aut)); + if (opt_instut) + aut = spot::sl(aut); + if (opt_product) aut = spot::product(std::move(aut), opt_product); diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc index 99eec217e..f57d258e7 100644 --- a/src/tgbaalgos/stutterize.cc +++ b/src/tgbaalgos/stutterize.cc @@ -54,17 +54,30 @@ namespace spot typedef std::deque queue_t; } + static bdd + get_all_ap(const const_tgba_digraph_ptr& a) + { + bdd res = bddtrue; + for (auto& i: a->transitions()) + res &= bdd_support(i.cond); + return res; + } + tgba_digraph_ptr sl(const const_tgba_digraph_ptr& a, const ltl::formula* f) { - bdd aps = atomic_prop_collect_as_bdd(f, a); + bdd aps = f + ? atomic_prop_collect_as_bdd(f, a) + : get_all_ap(a); return sl(a, aps); } tgba_digraph_ptr sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f) { - bdd aps = atomic_prop_collect_as_bdd(f, a); + bdd aps = f + ? atomic_prop_collect_as_bdd(f, a) + : get_all_ap(a); return sl2(a, aps); } @@ -135,6 +148,8 @@ namespace spot tgba_digraph_ptr sl2(tgba_digraph_ptr&& a, bdd atomic_propositions) { + if (atomic_propositions == bddfalse) + atomic_propositions = get_all_ap(a); unsigned num_states = a->num_states(); unsigned num_transitions = a->num_transitions(); for (unsigned state = 0; state < num_states; ++state) diff --git a/src/tgbaalgos/stutterize.hh b/src/tgbaalgos/stutterize.hh index 47d94cf1e..f4bc6b86a 100644 --- a/src/tgbaalgos/stutterize.hh +++ b/src/tgbaalgos/stutterize.hh @@ -28,20 +28,20 @@ namespace spot { SPOT_API tgba_digraph_ptr - sl(const const_tgba_digraph_ptr&, const ltl::formula*); + sl(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr); SPOT_API tgba_digraph_ptr sl(const const_tgba_digraph_ptr&, bdd); SPOT_API tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr&, const ltl::formula*); + sl2(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr); SPOT_API tgba_digraph_ptr sl2(const const_tgba_digraph_ptr&, bdd); #ifndef SWIG SPOT_API tgba_digraph_ptr - sl2(tgba_digraph_ptr&&); + sl2(tgba_digraph_ptr&&, bdd = bddfalse); #endif } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 34d0598ed..06cfe7c4c 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -119,6 +119,7 @@ TESTS = \ randaut.test \ randtgba.test \ isomorph.test \ + stutter.test \ emptchk.test \ emptchke.test \ dfs.test \ diff --git a/src/tgbatest/stutter.test b/src/tgbatest/stutter.test new file mode 100755 index 000000000..7a32e69f6 --- /dev/null +++ b/src/tgbatest/stutter.test @@ -0,0 +1,38 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014 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 . + +. ./defs || exit 1 + +set -e + +ltl2tgba=../../bin/ltl2tgba +autfilt=../../bin/autfilt + +$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa +$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa +$autfilt pos.hoa --product neg.hoa -H > prod.hoa +$autfilt --is-empty prod.hoa -q && exit 1 +$autfilt --states=10 prod.hoa -q + +$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa +$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa +$autfilt pos.hoa --product neg.hoa -H > prod.hoa +$autfilt --is-empty prod.hoa -q && exit 1 +$autfilt --states=12 prod.hoa -q