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,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

bin/autfilt.cc

@@ -41,6 +41,7 @@
 #include "common_hoaread.hh"
 
 #include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/sum.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/stutter.hh>
 #include <spot/twaalgos/isunamb.hh>
@@ -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<int>::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);

python/spot/impl.i

@@ -143,6 +143,7 @@
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/langmap.hh>
 #include <spot/twaalgos/simulation.hh>
+#include <spot/twaalgos/sum.hh>
 #include <spot/twaalgos/postproc.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/stutter.hh>
@@ -549,6 +550,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/simulation.hh>
 %include <spot/twaalgos/postproc.hh>
 %include <spot/twaalgos/product.hh>
+%include <spot/twaalgos/sum.hh>
 %include <spot/twaalgos/stutter.hh>
 %include <spot/twaalgos/translate.hh>
 %include <spot/twaalgos/hoa.hh>

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 \

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 <http://www.gnu.org/licenses/>.
+
+#include <spot/twaalgos/sum.hh>
+#include <spot/twa/twagraph.hh>
+#include <vector>
+#include <map>
+
+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<unsigned, bdd> edges;
+      std::vector<unsigned> 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<unsigned> 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());
+  }
+
+}

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 <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/misc/common.hh>
+#include <spot/twa/fwd.hh>
+
+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);
+}

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)

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 <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+
+set -e
+
+cat >input1 <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[0] 1
+[1] 2
+State: 1
+State: 2 {0}
+[!0] 0
+[2] 1
+--END--
+EOF
+
+cat >input2 <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0}
+[0] 1
+State: 1 {1}
+[1] 0
+--END--
+EOF
+
+cat >input3 <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 1
+State: 1
+[1] 1
+--END--
+EOF
+
+cat >input4 <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc univ-branch
+--BODY--
+State: 0
+[0] 1&0
+State: 1
+[1] 0 {0}
+--END--
+EOF
+
+cat >false1 <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[t] 0 {0}
+--END--
+EOF
+
+cat >false2 <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[t] 0
+--END--
+EOF
+
+cat >expected <<EOF
+HOA: v1
+States: 6
+Start: 5
+AP: 3 "a" "b" "c"
+Acceptance: 3 (Inf(0)&Inf(1)) | Inf(2)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[1] 1 {0}
+State: 1
+[0] 0 {1}
+State: 2
+[0] 3 {2}
+[1] 4 {2}
+State: 3
+State: 4
+[!0] 2 {2}
+[2] 3 {2}
+State: 5
+[1] 1
+[0] 3
+[1] 4
+--END--
+HOA: v1
+States: 6
+Start: 5
+AP: 3 "a" "b" "c"
+acc-name: Streett 1
+Acceptance: 2 Fin(0) | Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 1
+State: 1
+[1] 1
+State: 2
+[0] 3 {0 1}
+[1] 4 {0 1}
+State: 3
+State: 4
+[!0] 2 {0 1}
+[2] 3 {0 1}
+State: 5
+[0] 0
+[1] 1
+[0] 3
+[1] 4
+--END--
+HOA: v1
+States: 6
+Start: 5
+AP: 3 "a" "b" "c"
+Acceptance: 2 Inf(0) | Inf(1)
+properties: univ-branch trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0&1
+State: 1
+[1] 0 {0}
+State: 2
+[0] 3 {1}
+[1] 4 {1}
+State: 3
+State: 4
+[!0] 2 {1}
+[2] 3 {1}
+State: 5
+[0] 0&1
+[0] 3
+[1] 4
+--END--
+EOF
+
+run 0 autfilt input2 --sum input1 input3 input4 --hoaf=t | tee stdout
+diff stdout expected
+
+cat >expected <<EOF
+HOA: v1
+States: 3
+Start: 2
+AP: 1 "a"
+acc-name: Streett 1
+Acceptance: 2 Fin(0) | Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 0 {0}
+State: 1
+[t] 1 {0}
+State: 2
+[t] 0
+[t] 1
+--END--
+EOF
+
+run 0 autfilt false1 --sum false2 --hoaf=t | tee stdout
+diff stdout expected
+rm false1 false2 input1 input2 input3 input4 expected stdout

tests/python/sum.py

@@ -0,0 +1,91 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2017  Laboratoire de Recherche et Développement
+# de l'Epita
+#
+# 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/>.
+
+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])