diff --git a/NEWS b/NEWS index b9ed0cac9..86554f017 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,16 @@ New in spot 1.99.3a (not yet released) exactly one acceptance sets. This is useful when targeting parity acceptance. + * autfilt has a new --product-or option. This builds a synchronized + product of two (completed of needed) automata in order to + recognize the *sum* of their languages. This works by just using + the disjunction of their acceptance conditions (with appropriate + renumbering of the acceptance sets). + + For consistency, the --product option (that builds a synchronized + product that recognizes the *intersection* of the languages) now + also has a --product-and alias. + * the parser for ltl2dstar's format has been merged with the parser for the other automata formats. This implies two things: - autfilt and dstar2tgba (despite its name) can now both read @@ -18,20 +28,18 @@ New in spot 1.99.3a (not yet released) * The class hierarchy for temporal formulas has been entirely rewritten. This change is actually quite massive (~13200 lines removed, ~8200 lines added), and brings some nice benefits: - - LTL/PSL formulas are now represented by lightweight - ltl::formula objects (instead of ltl::formula* pointers) - that perform reference counting automatically. - - There is no hierachy anymore: all operators are represented - by a single type of node in the syntax tree, and an - enumerator is used to distinguish between operators. - - Visitors have been replaced by member functions such - as map() or traverse(), that take a function (usually - written as a lambda function) and apply it to the - nodes of the tree. - - As a consequence, writing algorithms that manipulate - formula is more friendly, and several functions - algorithms that spanned a few pages have been - reduced to a few lines. + - LTL/PSL formulas are now represented by lightweight ltl::formula + objects (instead of ltl::formula* pointers) that perform + reference counting automatically. + - There is no hierachy anymore: all operators are represented by a + single type of node in the syntax tree, and an enumerator is + used to distinguish between operators. + - Visitors have been replaced by member functions such as map() or + traverse(), that take a function (usually written as a lambda + function) and apply it to the nodes of the tree. + - As a consequence, writing algorithms that manipulate formula is + more friendly, and several algorithms that spanned a few pages + have been reduced to a few lines. New in spot 1.99.3 (2015-08-26) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 040860f5e..aa538f6c2 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -85,7 +85,8 @@ enum { OPT_KEEP_STATES, OPT_MASK_ACC, OPT_MERGE, - OPT_PRODUCT, + OPT_PRODUCT_AND, + OPT_PRODUCT_OR, OPT_RANDOMIZE, OPT_REM_AP, OPT_REM_DEAD, @@ -122,8 +123,13 @@ static const argp_option options[] = { 0, 0, 0, 0, "Transformations:", 5 }, { "merge-transitions", OPT_MERGE, 0, 0, "merge transitions with same destination and acceptance", 0 }, - { "product", OPT_PRODUCT, "FILENAME", 0, - "build the product with the automaton in FILENAME", 0 }, + { "product", OPT_PRODUCT_AND, "FILENAME", 0, + "build the product with the automaton in FILENAME " + "to intersect languages", 0 }, + { "product-and", 0, 0, OPTION_ALIAS, 0, 0 }, + { "product-or", OPT_PRODUCT_OR, "FILENAME", 0, + "build the product with the automaton in FILENAME " + "to sum languages", 0 }, { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL, "randomize states and transitions (specify 's' or 't' to " "randomize only states or transitions)", 0 }, @@ -231,7 +237,8 @@ static int opt_seed = 0; static struct opt_t { spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::twa_graph_ptr product = nullptr; + spot::twa_graph_ptr product_and = nullptr; + spot::twa_graph_ptr product_or = nullptr; spot::twa_graph_ptr intersect = nullptr; spot::twa_graph_ptr are_isomorphic = nullptr; std::unique_ptr @@ -393,14 +400,24 @@ parse_opt(int key, char* arg, struct argp_state*) opt_rem_unreach = true; break; } - case OPT_PRODUCT: + case OPT_PRODUCT_AND: { auto a = read_automaton(arg, opt->dict); - if (!opt->product) - opt->product = std::move(a); + if (!opt->product_and) + opt->product_and = std::move(a); else - opt->product = spot::product(std::move(opt->product), - std::move(a)); + opt->product_and = spot::product(std::move(opt->product_and), + std::move(a)); + } + break; + case OPT_PRODUCT_OR: + { + auto a = read_automaton(arg, opt->dict); + if (!opt->product_or) + opt->product_or = std::move(a); + else + opt->product_or = spot::product_or(std::move(opt->product_or), + std::move(a)); } break; case OPT_RANDOMIZE: @@ -579,8 +596,10 @@ namespace else if (opt_rem_unreach) aut->purge_unreachable_states(); - if (opt->product) - aut = spot::product(std::move(aut), opt->product); + if (opt->product_and) + aut = spot::product(std::move(aut), opt->product_and); + if (opt->product_or) + aut = spot::product_or(std::move(aut), opt->product_or); if (opt_sat_minimize) { diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 47958b188..4ff21b10d 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -181,6 +181,7 @@ TESTS_twa = \ ltldo2.test \ maskacc.test \ maskkeep.test \ + prodor.test \ simdet.test \ sim2.test \ sim3.test \ diff --git a/src/tests/prodor.test b/src/tests/prodor.test new file mode 100755 index 000000000..d5528ccee --- /dev/null +++ b/src/tests/prodor.test @@ -0,0 +1,169 @@ +#!/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 +set -e + +ltl2tgba=../../bin/ltl2tgba +autfilt=../../bin/autfilt + +$ltl2tgba -DH 'GFa' > gfa.hoa +$ltl2tgba -DH 'FGb' > fgb.hoa +$autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa +cat por.hoa + +cat >exp < pand.hoa +cat pand.hoa + +cat >exp < gfa.hoa +$ltl2tgba -BDH 'Xb' > xb.hoa +$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa +cat por.hoa + +cat >exp < gfa.hoa +$ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa +$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa +cat por.hoa + +cat >exp < #include #include "misc/hash.hh" @@ -37,77 +38,115 @@ namespace spot return wang32_hash(s.first ^ wang32_hash(s.second)); } }; - } + static + twa_graph_ptr product_aux(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state, + bool and_acc) + { + std::unordered_map s2n; + std::deque> todo; - twa_graph_ptr product(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right, - unsigned left_state, - unsigned right_state) - { - std::unordered_map s2n; - std::deque> todo; + assert(left->get_dict() == right->get_dict()); + auto res = make_twa_graph(left->get_dict()); + res->copy_ap_of(left); + res->copy_ap_of(right); + auto left_num = left->num_sets(); + auto right_acc = right->get_acceptance(); + right_acc.shift_left(left_num); + if (and_acc) + right_acc.append_and(left->get_acceptance()); + else + right_acc.append_or(acc_cond::acc_code(left->get_acceptance())); + res->set_acceptance(left_num + right->num_sets(), right_acc); - assert(left->get_dict() == right->get_dict()); - auto res = make_twa_graph(left->get_dict()); - res->copy_ap_of(left); - res->copy_ap_of(right); - auto left_num = left->num_sets(); - auto right_acc = right->get_acceptance(); - right_acc.shift_left(left_num); - right_acc.append_and(left->get_acceptance()); - res->set_acceptance(left_num + right->num_sets(), right_acc); + auto v = new product_states; + res->set_named_prop("product-states", v); - auto v = new product_states; - res->set_named_prop("product-states", v); - - auto new_state = - [&](unsigned left_state, unsigned right_state) -> unsigned - { - product_state x(left_state, right_state); - auto p = s2n.emplace(x, 0); - if (p.second) // This is a new state - { - p.first->second = res->new_state(); - todo.emplace_back(x, p.first->second); - assert(p.first->second == v->size()); - v->push_back(x); - } - return p.first->second; - }; - - res->set_init_state(new_state(left_state, right_state)); - if (right_acc.is_false()) - // Do not bother doing any work if the resulting acceptance is - // false. - return res; - while (!todo.empty()) - { - auto top = todo.front(); - todo.pop_front(); - for (auto& l: left->out(top.first.first)) - for (auto& r: right->out(top.first.second)) + auto new_state = + [&](unsigned left_state, unsigned right_state) -> unsigned + { + product_state x(left_state, right_state); + auto p = s2n.emplace(x, 0); + if (p.second) // This is a new state { - auto cond = l.cond & r.cond; - if (cond == bddfalse) - continue; - auto dst = new_state(l.dst, r.dst); - res->new_edge(top.second, dst, cond, - res->acc().join(left->acc(), l.acc, - right->acc(), r.acc)); - // If right is deterministic, we can abort immediately! + p.first->second = res->new_state(); + todo.emplace_back(x, p.first->second); + assert(p.first->second == v->size()); + v->push_back(x); } - } + return p.first->second; + }; - return res; + res->set_init_state(new_state(left_state, right_state)); + if (right_acc.is_false()) + // Do not bother doing any work if the resulting acceptance is + // false. + return res; + while (!todo.empty()) + { + auto top = todo.front(); + todo.pop_front(); + for (auto& l: left->out(top.first.first)) + for (auto& r: right->out(top.first.second)) + { + auto cond = l.cond & r.cond; + if (cond == bddfalse) + continue; + auto dst = new_state(l.dst, r.dst); + res->new_edge(top.second, dst, cond, + res->acc().join(left->acc(), l.acc, + right->acc(), r.acc)); + // If right is deterministic, we can abort immediately! + } + } + + res->prop_deterministic(left->is_deterministic() + && right->is_deterministic()); + res->prop_stutter_invariant(left->is_stutter_invariant() + && right->is_stutter_invariant()); + res->prop_stutter_sensitive(left->is_stutter_sensitive() + && right->is_stutter_sensitive()); + res->prop_state_based_acc(left->has_state_based_acc() + && right->has_state_based_acc()); + return res; + } } twa_graph_ptr product(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right) + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state) + { + return product_aux(left, right, left_state, right_state, true); + } + + twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) { return product(left, right, left->get_init_state_number(), right->get_init_state_number()); } + twa_graph_ptr product_or(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state) + { + return product_aux(tgba_complete(left), + tgba_complete(right), + left_state, right_state, false); + } + + twa_graph_ptr product_or(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) + { + return product_or(left, right, + left->get_init_state_number(), + right->get_init_state_number()); + } + } diff --git a/src/twaalgos/product.hh b/src/twaalgos/product.hh index f7e98a4fa..1ef1e244b 100644 --- a/src/twaalgos/product.hh +++ b/src/twaalgos/product.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -32,11 +32,22 @@ namespace spot SPOT_API twa_graph_ptr product(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right); + const const_twa_graph_ptr& right); SPOT_API twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state); + + SPOT_API + twa_graph_ptr product_or(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right); + + SPOT_API + twa_graph_ptr product_or(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right, unsigned left_state, unsigned right_state); + }