From 194c199232b9574cfd3a2c2d5e7fb731c7aaa336 Mon Sep 17 00:00:00 2001 From: Thomas Medioni Date: Mon, 6 Mar 2017 17:03:34 +0100 Subject: [PATCH] Implement sum(..) and sum_and(..). Fixes #231. * NEWS: Mention of implementation of sum, sum_and. * bin/autfilt.cc: Add --sum, --sum-or and --sum-and options. * python/spot/impl.i: Add bindings for sum, sum_and. * spot/twaalgos/Makefile.am: Add sum.cc, sum.hh. * spot/twaalgos/sum.cc: Implement sum, sum_and. * spot/twaalgos/sum.hh: Declaration of sum, sum_and. * tests/Makefile.am: Add sum tests. * tests/core/explsum.test: Test the sum of two automatons, false or false, unsatisfied mark propagation, handling of univ. transitions. * tests/python/sum.py: Check that two automatons that does not share their bdd dict are not accepted, then run tests over the sum of randomly generated LTL formulas. --- NEWS | 8 ++ bin/autfilt.cc | 37 +++++++ python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/sum.cc | 182 ++++++++++++++++++++++++++++++++ spot/twaalgos/sum.hh | 74 +++++++++++++ tests/Makefile.am | 2 + tests/core/explsum.test | 217 ++++++++++++++++++++++++++++++++++++++ tests/python/sum.py | 91 ++++++++++++++++ 9 files changed, 615 insertions(+) create mode 100644 spot/twaalgos/sum.cc create mode 100644 spot/twaalgos/sum.hh create mode 100755 tests/core/explsum.test create mode 100644 tests/python/sum.py diff --git a/NEWS b/NEWS index 68b5f8edc..a21ce9c34 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,14 @@ New in spot 2.3.1.dev (not yet released) atomic propositions instead of conting them. Tools that output formulas also support --format=%x for this purpose. + - In autfilt, the options --sum(--sum-or) and --sum-and are + implemented. + + Library: + + - spot::sum() and spot::sum_and() implements the union and the + intersection of two automatons, respectively. + Python: - The bdd_to_formula(), and to_generalized_buchi() functions can now diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 84998b4da..be2ef6537 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -41,6 +41,7 @@ #include "common_hoaread.hh" #include +#include #include #include #include @@ -137,6 +138,8 @@ enum { OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_STATES, OPT_STRIPACC, + OPT_SUM_OR, + OPT_SUM_AND, OPT_TERMINAL_SCCS, OPT_TRIV_SCCS, OPT_USED_AP_N, @@ -317,6 +320,13 @@ static const argp_option options[] = { "remove-dead-states", OPT_REM_DEAD, nullptr, 0, "remove states that are unreachable, or that cannot belong to an " "infinite path", 0 }, + { "sum", OPT_SUM_OR, "FILENAME", 0, + "build the sum with the automaton in FILENAME " + "to sum languages", 0 }, + { "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "sum-and", OPT_SUM_AND, "FILENAME", 0, + "build the sum with the automaton in FILENAME " + "to intersect languages", 0 }, { "separate-sets", OPT_SEP_SETS, nullptr, 0, "if both Inf(x) and Fin(x) appear in the acceptance condition, replace " "Fin(x) by a new Fin(y) and adjust the automaton", 0 }, @@ -412,6 +422,8 @@ static struct opt_t spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::twa_graph_ptr product_and = nullptr; spot::twa_graph_ptr product_or = nullptr; + spot::twa_graph_ptr sum_and = nullptr; + spot::twa_graph_ptr sum_or = nullptr; spot::twa_graph_ptr intersect = nullptr; spot::twa_graph_ptr included_in = nullptr; spot::twa_graph_ptr equivalent_pos = nullptr; @@ -846,6 +858,26 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STRIPACC: opt_stripacc = true; break; + case OPT_SUM_OR: + { + auto a = read_automaton(arg, opt->dict); + if (!opt->sum_or) + opt->sum_or = std::move(a); + else + opt->sum_or = spot::sum(std::move(opt->sum_or), + std::move(a)); + } + break; + case OPT_SUM_AND: + { + auto a = read_automaton(arg, opt->dict); + if (!opt->sum_and) + opt->sum_and = std::move(a); + else + opt->sum_and = spot::sum_and(std::move(opt->sum_and), + std::move(a)); + } + break; case OPT_TERMINAL_SCCS: opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits::max()); opt_terminal_sccs_set = true; @@ -1188,6 +1220,11 @@ namespace if (opt->product_or) aut = spot::product_or(std::move(aut), opt->product_or); + if (opt->sum_or) + aut = spot::sum(std::move(aut), opt->sum_or); + if (opt->sum_and) + aut = spot::sum_and(std::move(aut), opt->sum_and); + if (opt_decompose_strength) { aut = decompose_strength(aut, opt_decompose_strength); diff --git a/python/spot/impl.i b/python/spot/impl.i index fedae556e..2df9f8f53 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -143,6 +143,7 @@ #include #include #include +#include #include #include #include @@ -549,6 +550,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 352d88e76..8b8a89d6e 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -78,6 +78,7 @@ twaalgos_HEADERS = \ stats.hh \ stripacc.hh \ stutter.hh \ + sum.hh \ tau03.hh \ tau03opt.hh \ totgba.hh \ @@ -136,6 +137,7 @@ libtwaalgos_la_SOURCES = \ stats.cc \ stripacc.cc \ stutter.cc \ + sum.cc \ tau03.cc \ tau03opt.cc \ totgba.cc \ diff --git a/spot/twaalgos/sum.cc b/spot/twaalgos/sum.cc new file mode 100644 index 000000000..ba1b8a429 --- /dev/null +++ b/spot/twaalgos/sum.cc @@ -0,0 +1,182 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 +#include +#include +#include + +namespace spot +{ + namespace + { + // Helper function that connects a new initial state to the automaton, + // in replacement of graph_init + static + void connect_init_state(const twa_graph_ptr& res, + const const_twa_graph_ptr& graph, + unsigned init, + unsigned graph_init, + unsigned offset = 0U) + { + std::map edges; + std::vector dst; + for (auto& e : graph->out(graph_init)) + { + for (auto& d : graph->univ_dests(e)) + dst.push_back(d + offset); + if (dst.size() > 1) + res->new_univ_edge(init, dst.begin(), dst.end(), e.cond, 0U); + else + edges[dst[0]] |= e.cond; + dst.clear(); + } + for (auto& p : edges) + res->new_edge(init, p.first, p.second); + } + + // Helper function that copies the states of graph into res, adding + // offset to the state ID, mark to the current mark of the edges, + // and setting the number of states to num_sets + static + void copy_union(const twa_graph_ptr& res, + const const_twa_graph_ptr& graph, + acc_cond::mark_t mark = 0U, + unsigned offset = 0U) + { + auto state_offset = res->num_states(); + + res->new_states(graph->num_states()); + + std::vector dst; + for (auto& e : graph->edges()) + { + for (auto& d : graph->univ_dests(e)) + dst.push_back(d + state_offset); + + res->new_univ_edge(e.src + state_offset, + dst.begin(), dst.end(), + e.cond, + (e.acc << offset)| mark); + dst.clear(); + } + } + + // Helper function that perform the sum of the automaton in left and the + // automaton in right, using is_sum true for sum_or and is_sum false + // as sum_and + static + twa_graph_ptr sum_aux(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state, + bool is_sum) + { + if (left->get_dict() != right->get_dict()) + throw std::runtime_error("sum: left and right automata should " + "share their bdd_dict"); + auto res = make_twa_graph(left->get_dict()); + res->copy_ap_of(left); + res->copy_ap_of(right); + + auto unsatl = left->acc().unsat_mark(); + acc_cond::mark_t markl = 0U; + acc_cond::mark_t markr = 0U; + auto left_acc = left->get_acceptance(); + auto left_num_sets = left->num_sets(); + if (!unsatl.first) + { + markl.set(0); + left_num_sets = 1; + left_acc = acc_cond::acc_code::buchi(); + } + else + { + markr |= unsatl.second; + } + + auto unsatr = right->acc().unsat_mark(); + auto right_acc = right->get_acceptance(); + auto right_num_sets = right->num_sets(); + if (!unsatr.first) + { + markr.set(left_num_sets); + right_num_sets = 1; + right_acc = acc_cond::acc_code::buchi(); + } + else + { + markl |= (unsatr.second << left_num_sets); + } + res->set_acceptance(left_num_sets + right_num_sets, + (right_acc << left_num_sets) |= left_acc); + copy_union(res, left, markl); + copy_union(res, right, markr, left_num_sets); + + if (is_sum) + { + unsigned init = res->new_state(); + res->set_init_state(init); + + connect_init_state(res, left, init, left_state); + connect_init_state(res, right, init, right_state, left->num_states()); + } + else + { + res->set_univ_init_state({ left_state, + right_state + left->num_states() }); + } + return res; + } + + + } + twa_graph_ptr sum(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state) + { + return sum_aux(left, right, left_state, right_state, true); + } + + twa_graph_ptr sum(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) + { + return sum(left, right, + left->get_init_state_number(), + right->get_init_state_number()); + } + + twa_graph_ptr sum_and(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state) + { + return sum_aux(left, right, left_state, right_state, false); + } + twa_graph_ptr sum_and(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) + { + return sum_and(left, + right, + left->get_init_state_number(), + right->get_init_state_number()); + } + +} diff --git a/spot/twaalgos/sum.hh b/spot/twaalgos/sum.hh new file mode 100644 index 000000000..34df70f8c --- /dev/null +++ b/spot/twaalgos/sum.hh @@ -0,0 +1,74 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 + +namespace spot +{ + /// \brief Sum two twa into a new twa, performing the union of the two input + /// automatons. + /// + /// \param left Left term of the sum. + /// \param right Right term of the sum. + /// \return A spot::twa_graph containing the sum of \a left and \a right + SPOT_API + twa_graph_ptr sum(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right); + + /// \brief Sum two twa into a new twa, performing the union of the two input + /// automatons. + /// + /// \param left Left term of the sum. + /// \param right Right term of the sum. + /// \param left_state Initial state of the left term of the sum. + /// \param right_state Initial state of the right term of the sum. + /// \return A spot::twa_graph containing the sum of \a left and \a right + SPOT_API + twa_graph_ptr sum(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state); + + /// \brief Sum two twa into a new twa, using an universal initial transition, + /// performing the intersection of the two languages of the input automatons. + /// + /// \param left Left term of the sum. + /// \param right Right term of the sum. + /// \return A spot::twa_graph containing the sum of \a left and \a right + SPOT_API + twa_graph_ptr sum_and(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right); + + /// \brief Sum two twa into a new twa, using an universal initial transition, + /// performing the intersection of the two languages of the input automatons. + /// + /// \param left Left term of the sum. + /// \param right Right term of the sum. + /// \param left_state Initial state of the left term of the sum. + /// \param right_state Initial state of the right term of the sum. + /// \return A spot::twa_graph containing the sum of \a left and \a right + SPOT_API + twa_graph_ptr sum_and(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, + unsigned left_state, + unsigned right_state); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index ee24084c2..c1b37ddeb 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -231,6 +231,7 @@ TESTS_twa = \ core/explpro2.test \ core/explpro3.test \ core/explpro4.test \ + core/explsum.test \ core/tripprod.test \ core/dupexp.test \ core/exclusive-tgba.test \ @@ -349,6 +350,7 @@ TESTS_python = \ python/setacc.py \ python/sccfilter.py \ python/setxor.py \ + python/sum.py \ python/trival.py \ python/twagraph.py \ $(TESTS_ipython) diff --git a/tests/core/explsum.test b/tests/core/explsum.test new file mode 100755 index 000000000..b4883a18e --- /dev/null +++ b/tests/core/explsum.test @@ -0,0 +1,217 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 + +cat >input1 <input2 <input3 <input4 <false1 <false2 <expected <expected <. + +import spot +import sys +import itertools + +# make sure that we are not allowed to build the sum of two automata with +# different dictionaries. + +aut1 = spot.translate('Xa') +aut2 = spot.translate('Xb', dict=spot.make_bdd_dict()) + +try: + spot.sum(aut1, aut2) + exit(2) +except RuntimeError: + pass + + +opts = spot.option_map() +opts.set('output', spot.OUTPUTLTL) +opts.set('tree_size_min', 15) +opts.set('tree_size_max', 15) +opts.set('wf', False) +opts.set('seed', 0) +opts.set('simplification_level', 0) +spot.srand(0) +rg = spot.randltlgenerator(2, opts) + + +dict = spot.make_bdd_dict() + +def produce_phi(rg, n): + phi = [] + while len(phi) < n: + f = rg.next() + if f.is_syntactic_persistence(): + phi.append(f) + return phi + +def equivalent(a, phi): + negphi = spot.formula.Not(phi) + nega = spot.dtwa_complement(spot.tgba_determinize(a)) + a2 = spot.ltl_to_tgba_fm(phi, dict) + nega2 = spot.ltl_to_tgba_fm(negphi, dict) + return spot.product(a, nega2).is_empty()\ + and spot.product(nega, a2).is_empty() + +phi1 = produce_phi(rg, 1000) +phi2 = produce_phi(rg, 1000) +inputres = [] +aut = [] +for p in zip(phi1, phi2): + inputres.append(spot.formula.Or(p)) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) + aut.append(spot.to_generalized_buchi( \ + spot.remove_alternation(spot.sum(a1, a2), True))) + +for p in zip(aut, inputres): + assert equivalent(p[0], p[1]) + +aut = [] +inputres = [] + +for p in zip(phi1, phi2): + inputres.append(spot.formula.And(p)) + a1 = spot.ltl_to_tgba_fm(p[0], dict) + a2 = spot.ltl_to_tgba_fm(p[1], dict) + aut.append(spot.to_generalized_buchi( \ + spot.remove_alternation(spot.sum_and(a1, a2), True))) + +for p in zip(aut, inputres): + assert equivalent(p[0], p[1])