diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 90ddb9817..d8556b013 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -260,8 +260,11 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' --product=FILENAME build the product with the automaton in FILENAME --randomize[=s|t] randomize states and transitions (specify 's' or 't' to randomize only states or transitions) - --remove-fin rewrite the automaton without using Fin acceptance - + --remove-ap=AP[=0|=1][,AP...] + remove atomic propositions either by existential + quantification, or by assigning them 0 or 1 + --remove-fin rewrite the automaton without using Fin + acceptance --state-based-acceptance, --sbacc define the acceptance using states --strip-acceptance remove the acceptance condition and all acceptance @@ -531,3 +534,117 @@ $txt #+RESULTS: [[file:autfilt-ex5.png]] + + +Atomic propositions can be removed from an automaton in three ways: +- use ~--remove-ap=a~ to remove =a= by existential quantification, i.e., both =a= and its negation will be replaced by true. + This does not remove any transition. +- use ~--remove-ap=a=0~ to keep only transitions compatible with =!a= (i.e, transitions requiring =a= will be removed). +- use ~--remove-ap=a=1~ to keep only transitions compatible with =a= (i.e, transitions requiring =!a= will be removed). + +Here are the results of these three options on our example: + +#+NAME: autfilt-ex6a +#+BEGIN_SRC sh :results verbatim :export code +autfilt --remove-ap=a aut-ex1.hoa --dot=.a +#+END_SRC + +#+RESULTS: autfilt-ex6a +#+begin_example +digraph G { + rankdir=LR + label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=<1
❸>] + 0 -> 1 [label=<1
❶❸>] + 0 -> 2 [label=<1
⓿❸>] + 1 [label="1"] + 1 -> 0 [label=❸>] + 1 -> 1 [label=⓿❸>] + 1 -> 2 [label=❷❸>] + 2 [label="2"] + 2 -> 0 [label=] + 2 -> 1 [label=⓿>] + 2 -> 2 [label=⓿>] +} +#+end_example + +#+BEGIN_SRC dot :file autfilt-ex6a.png :cmdline -Tpng :var txt=autfilt-ex6a :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:autfilt-ex6a.png]] + +#+NAME: autfilt-ex6b +#+BEGIN_SRC sh :results verbatim :export code +autfilt --remove-ap=a=0 aut-ex1.hoa --dot=.a +#+END_SRC + +#+RESULTS: autfilt-ex6b +#+begin_example +digraph G { + rankdir=LR + label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=<1
❸>] + 0 -> 1 [label=<1
⓿❸>] + 1 [label="1"] + 1 -> 0 [label=] + 1 -> 1 [label=⓿>] +} +#+end_example + +#+BEGIN_SRC dot :file autfilt-ex6b.png :cmdline -Tpng :var txt=autfilt-ex6b :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:autfilt-ex6b.png]] + +#+NAME: autfilt-ex6c +#+BEGIN_SRC sh :results verbatim :export code +autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a +#+END_SRC + +#+RESULTS: autfilt-ex6c +#+begin_example +digraph G { + rankdir=LR + label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 0 [label=<1
❸>] + 0 -> 1 [label=<1
❶❸>] + 1 [label="1"] + 1 -> 0 [label=❸>] + 1 -> 1 [label=⓿❸>] +} +#+end_example + +#+BEGIN_SRC dot :file autfilt-ex6c.png :cmdline -Tpng :var txt=autfilt-ex6c :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:autfilt-ex6c.png]] diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 3807244c4..d17fa3aa8 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -44,6 +44,7 @@ #include "misc/random.hh" #include "hoaparse/public.hh" #include "ltlvisit/exclusive.hh" +#include "tgbaalgos/remprop.hh" #include "tgbaalgos/randomize.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" @@ -83,6 +84,7 @@ enum { OPT_MERGE, OPT_PRODUCT, OPT_RANDOMIZE, + OPT_REM_AP, OPT_REM_FIN, OPT_SBACC, OPT_SEED, @@ -145,6 +147,9 @@ static const argp_option options[] = "ensure two of them may not be true at the same time. Use this option " "multiple times to declare independent groups of exclusive " "propositions.", 0 }, + { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0, + "remove atomic propositions either by existential quantification, or " + "by assigning them 0 or 1", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -233,6 +238,7 @@ static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; static spot::exclusive_ap excl_ap; +static spot::remove_ap rem_ap; static int parse_opt(int key, char* arg, struct argp_state*) @@ -385,6 +391,9 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_REM_AP: + rem_ap.add_ap(arg); + break; case OPT_REM_FIN: opt_rem_fin = true; break; @@ -504,6 +513,9 @@ namespace if (!excl_ap.empty()) aut = excl_ap.constrain(aut); + if (!rem_ap.empty()) + aut = rem_ap.strip(aut); + if (opt_destut) aut = spot::closure(std::move(aut)); if (opt_instut == 1) @@ -586,38 +598,38 @@ main(int argc, char** argv) const argp ap = { options, parse_opt, "[FILENAMES...]", argp_program_doc, children, 0, 0 }; - // This will ensure that all objects stored in this struct are - // destroyed before global variables. - opt_t o; - opt = &o; - - // Disable post-processing as much as possible by default. - level = spot::postprocessor::Low; - pref = spot::postprocessor::Any; - if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) - exit(err); - - if (jobs.empty()) - jobs.emplace_back("-", true); - - if (opt->are_isomorphic) - { - if (opt_merge) - opt->are_isomorphic->merge_transitions(); - opt->isomorphism_checker = std::unique_ptr - (new spot::isomorphism_checker(opt->are_isomorphic)); - } - - - spot::srand(opt_seed); - - spot::postprocessor post(&extra_options); - post.set_pref(pref | comp); - post.set_type(type); - post.set_level(level); - try { + // This will ensure that all objects stored in this struct are + // destroyed before global variables. + opt_t o; + opt = &o; + + // Disable post-processing as much as possible by default. + level = spot::postprocessor::Low; + pref = spot::postprocessor::Any; + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) + exit(err); + + if (jobs.empty()) + jobs.emplace_back("-", true); + + if (opt->are_isomorphic) + { + if (opt_merge) + opt->are_isomorphic->merge_transitions(); + opt->isomorphism_checker = std::unique_ptr + (new spot::isomorphism_checker(opt->are_isomorphic)); + } + + + spot::srand(opt_seed); + + spot::postprocessor post(&extra_options); + post.set_pref(pref | comp); + post.set_type(type); + post.set_level(level); + hoa_processor processor(post); if (processor.run()) return 2; @@ -626,6 +638,10 @@ main(int argc, char** argv) { error(2, 0, "%s", e.what()); } + catch (const std::invalid_argument& e) + { + error(2, 0, "%s", e.what()); + } if (automaton_format == Count) std::cout << match_count << std::endl; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 43234d711..56ca96595 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -64,6 +64,7 @@ tgbaalgos_HEADERS = \ reducerun.hh \ relabel.hh \ remfin.hh \ + remprop.hh \ replayrun.hh \ safety.hh \ sbacc.hh \ @@ -117,6 +118,7 @@ libtgbaalgos_la_SOURCES = \ reachiter.cc \ reducerun.cc \ remfin.cc \ + remprop.cc \ replayrun.cc \ relabel.cc \ safety.cc \ diff --git a/src/tgbaalgos/remprop.cc b/src/tgbaalgos/remprop.cc new file mode 100644 index 000000000..9be2b3c95 --- /dev/null +++ b/src/tgbaalgos/remprop.cc @@ -0,0 +1,188 @@ +// -*- 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 . + +#include "remprop.hh" +#include "ltlenv/defaultenv.hh" +#include "tgbaalgos/mask.hh" +#include "misc/casts.hh" +#include "ltlvisit/tostring.hh" +#include +#include + +namespace spot +{ + remove_ap::~remove_ap() + { + for (auto& ap: props_exist) + ap->destroy(); + for (auto& ap: props_pos) + ap->destroy(); + for (auto& ap: props_neg) + ap->destroy(); + } + + namespace + { + static + void unexpected_char(const char* arg, const char* pos) + { + std::ostringstream out; + out << "unexpected "; + if (isprint(*pos)) + out << '\'' << *pos << '\''; + else + out << "character"; + out << " at position " << pos - arg << " in '"; + out << arg << '\''; + throw std::invalid_argument(out.str()); + } + } + + + void remove_ap::add_ap(const char* arg) + { + auto& env = spot::ltl::default_environment::instance(); + std::vector group; + auto start = arg; + while (*start) + { + while (*start == ' ' || *start == '\t') + ++start; + if (!*start) + break; + if (*start == ',' || *start == '=') + unexpected_char(arg, start); + const spot::ltl::atomic_prop* the_ap = nullptr; + + if (*start == '"') + { + auto end = ++start; + while (*end && *end != '"') + { + if (*end == '\\') + ++end; + ++end; + } + if (!*end) + { + std::string s = "missing closing '\"' in "; + s += arg; + throw std::invalid_argument(s); + } + std::string ap(start, end - start); + auto* t = env.require(ap); + the_ap = down_cast(t); + do + ++end; + while (*end == ' ' || *end == '\t'); + start = end; + } + else + { + auto end = start; + while (*end && *end != ',' && *end != '=') + ++end; + auto rend = end; + while (rend > start && (rend[-1] == ' ' || rend[-1] == '\t')) + --rend; + std::string ap(start, rend - start); + auto* t = env.require(ap); + the_ap = down_cast(t); + start = end; + } + if (*start) + { + if (!(*start == ',' || *start == '=')) + unexpected_char(arg, start); + if (*start == '=') + { + do + ++start; + while (*start == ' ' || *start == '\t'); + if (*start == '0') + props_neg.insert(the_ap); + else if (*start == '1') + props_pos.insert(the_ap); + else + unexpected_char(arg, start); + the_ap = nullptr; + do + ++start; + while (*start == ' ' || *start == '\t'); + } + if (*start) + { + if (*start != ',') + unexpected_char(arg, start); + ++start; + } + } + if (the_ap) + props_exist.insert(the_ap); + } + } + + tgba_digraph_ptr remove_ap::strip(const_tgba_digraph_ptr aut) const + { + bdd restrict = bddtrue; + bdd exist = bddtrue; + auto d = aut->get_dict(); + + tgba_digraph_ptr res = make_tgba_digraph(d); + res->copy_ap_of(aut); + res->prop_copy(aut, { true, true, false, false }); + res->copy_acceptance_of(aut); + + for (auto ap: props_exist) + { + int v = d->has_registered_proposition(ap, aut); + if (v >= 0) + { + exist &= bdd_ithvar(v); + d->unregister_variable(v, res); + } + } + for (auto ap: props_pos) + { + int v = d->has_registered_proposition(ap, aut); + if (v >= 0) + { + restrict &= bdd_ithvar(v); + d->unregister_variable(v, res); + } + } + for (auto ap: props_neg) + { + int v = d->has_registered_proposition(ap, aut); + if (v >= 0) + { + restrict &= bdd_nithvar(v); + d->unregister_variable(v, res); + } + } + + transform_accessible(aut, res, [&](unsigned, bdd& cond, + acc_cond::mark_t&, unsigned) + { + cond = bdd_restrict(bdd_exist(cond, exist), + restrict); + }); + return res; + } +} diff --git a/src/tgbaalgos/remprop.hh b/src/tgbaalgos/remprop.hh new file mode 100644 index 000000000..dbd72bed8 --- /dev/null +++ b/src/tgbaalgos/remprop.hh @@ -0,0 +1,44 @@ +// -*- 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 . + +#pragma once + +#include +#include "ltlast/atomic_prop.hh" +#include "tgba/tgbagraph.hh" + +namespace spot +{ + class SPOT_API remove_ap + { + std::set props_exist; + std::set props_pos; + std::set props_neg; + public: + ~remove_ap(); + void add_ap(const char* ap_csv); + + bool empty() const + { + return props_exist.empty() && props_pos.empty() && props_neg.empty(); + } + + tgba_digraph_ptr strip(const_tgba_digraph_ptr aut) const; + }; +} diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 41b734ad6..07968d46c 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -92,6 +92,7 @@ TESTS = \ tripprod.test \ dupexp.test \ exclusive.test \ + remprop.test \ degendet.test \ degenid.test \ degenlskip.test \ diff --git a/src/tgbatest/remprop.test b/src/tgbatest/remprop.test new file mode 100755 index 000000000..bf07fe053 --- /dev/null +++ b/src/tgbatest/remprop.test @@ -0,0 +1,97 @@ +#! /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 . + + +. ./defs || exit 1 + +set -e + +cat >automaton <expected <out +cat out +diff out expected + +cat >expected <out +cat out +diff out expected + +../../bin/autfilt -H --remove-ap=a==1 automaton 2>stderr && exit 1 +grep "autfilt: unexpected '=' at position 2 in 'a==1'" stderr