introduce spot::split_edges()

Fixes #255.

* spot/twaalgos/split.cc, spot/twaalgos/split.hh,
tests/core/split.test: New files.
* spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
* bin/autfilt.cc (--split-edges): New option.
* python/spot/impl.i: Process split.hh.
* tests/python/alternating.py: Test split_edges() on
an alternating automaton.

NEWS

@@ -14,6 +14,10 @@ New in spot 2.3.3.dev (not yet released)
   - genaut is a binary to produce families of automata defined in the
     literature (in the same way as we have genltl for LTL formulas).
 
+  - autfilt learned --split-edges to convert labels that are Boolean
+    formulas into labels that are min-terms.  (See spot::split_edges()
+    below.)
+
   Library:
 
   - A new library, libspotgen, gathers all functions used to generate
@@ -62,6 +66,13 @@ New in spot 2.3.3.dev (not yet released)
     level.  A similar trick was already used in sbacc(), and saves a
     few states in some cases.
 
+  - There is a new spot::split_edges() function that transforms edges
+    (labeled by Boolean formulas over atomic propositions) into
+    transitions (labeled by conjunctions where each atomic proposition
+    appear either positive or negative).  This can be used to
+    preprocess automata before feeding them to algorithms or tools
+    that expect transitions labeled by letters.
+
   Python:
 
   - The 'spot.gen' package exports the functions from libspotgen.

bin/autfilt.cc

@@ -40,34 +40,35 @@
 #include "common_conv.hh"
 #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>
 #include <spot/misc/optionmap.hh>
-#include <spot/misc/timer.hh>
 #include <spot/misc/random.hh>
+#include <spot/misc/timer.hh>
 #include <spot/parseaut/public.hh>
 #include <spot/tl/exclusive.hh>
-#include <spot/twaalgos/remprop.hh>
-#include <spot/twaalgos/randomize.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
 #include <spot/twaalgos/canonicalize.hh>
-#include <spot/twaalgos/mask.hh>
-#include <spot/twaalgos/sepsets.hh>
-#include <spot/twaalgos/stripacc.hh>
-#include <spot/twaalgos/remfin.hh>
 #include <spot/twaalgos/cleanacc.hh>
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/dualize.hh>
-#include <spot/twaalgos/strength.hh>
-#include <spot/twaalgos/hoa.hh>
-#include <spot/twaalgos/sccinfo.hh>
-#include <spot/twaalgos/isweakscc.hh>
 #include <spot/twaalgos/gtec/gtec.hh>
-#include <spot/twaalgos/totgba.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/isdet.hh>
+#include <spot/twaalgos/isunamb.hh>
+#include <spot/twaalgos/isweakscc.hh>
 #include <spot/twaalgos/langmap.hh>
+#include <spot/twaalgos/mask.hh>
+#include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/randomize.hh>
+#include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/remprop.hh>
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/sepsets.hh>
+#include <spot/twaalgos/split.hh>
+#include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/stripacc.hh>
+#include <spot/twaalgos/stutter.hh>
+#include <spot/twaalgos/sum.hh>
+#include <spot/twaalgos/totgba.hh>
 
 static const char argp_program_doc[] ="\
 Convert, transform, and filter omega-automata.\v\
@@ -137,6 +138,7 @@ enum {
   OPT_SEED,
   OPT_SEP_SETS,
   OPT_SIMPLIFY_EXCLUSIVE_AP,
+  OPT_SPLIT_EDGES,
   OPT_STATES,
   OPT_STRIPACC,
   OPT_SUM_OR,
@@ -323,6 +325,9 @@ 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 },
+    { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
+      "split edges into transitions labeled by conjunctions of all atomic "
+      "propositions, so they can be read as letters", 0 },
     { "sum", OPT_SUM_OR, "FILENAME", 0,
       "build the sum with the automaton in FILENAME "
       "to sum languages", 0 },
@@ -497,6 +502,7 @@ static bool opt_rem_dead = false;
 static bool opt_rem_unreach = false;
 static bool opt_rem_unused_ap = false;
 static bool opt_sep_sets = false;
+static bool opt_split_edges = false;
 static const char* opt_sat_minimize = nullptr;
 static int opt_highlight_nondet_states = -1;
 static int opt_highlight_nondet_edges = -1;
@@ -865,6 +871,9 @@ parse_opt(int key, char* arg, struct argp_state*)
       opt_simplify_exclusive_ap = true;
       opt_merge = true;
       break;
+    case OPT_SPLIT_EDGES:
+      opt_split_edges = true;
+      break;
     case OPT_STATES:
       opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
@@ -1277,6 +1286,9 @@ namespace
       else if (opt_rem_unused_ap) // constrain(aut, true) already does that
         aut->remove_unused_ap();
 
+      if (opt_split_edges)
+        aut = spot::split_edges(aut);
+
       if (randomize_st || randomize_tr)
         spot::randomize(aut, randomize_st, randomize_tr);
 

python/spot/impl.i

@@ -145,6 +145,7 @@
 #include <spot/twaalgos/isunamb.hh>
 #include <spot/twaalgos/langmap.hh>
 #include <spot/twaalgos/simulation.hh>
+#include <spot/twaalgos/split.hh>
 #include <spot/twaalgos/sum.hh>
 #include <spot/twaalgos/postproc.hh>
 #include <spot/twaalgos/product.hh>
@@ -563,6 +564,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/split.hh>
 %include <spot/twaalgos/sum.hh>
 %include <spot/twaalgos/stutter.hh>
 %include <spot/twaalgos/translate.hh>

spot/twaalgos/Makefile.am

@@ -1,9 +1,9 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
+## Copyright (C) 2008-2017 Laboratoire de Recherche et Développement
-## de Recherche et Développement de l'Epita (LRDE).
+## de l'Epita (LRDE).
-## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
+## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
-## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
-## Université Pierre et Marie Curie.
+## Pierre et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -69,6 +69,7 @@ twaalgos_HEADERS = \
   relabel.hh \
   remfin.hh \
   remprop.hh \
+  split.hh \
   strength.hh \
   sbacc.hh \
   sccfilter.hh \
@@ -129,6 +130,7 @@ libtwaalgos_la_SOURCES = \
   remfin.cc \
   remprop.cc \
   relabel.cc \
+  split.cc \
   strength.cc \
   sbacc.cc \
   sccinfo.cc \

spot/twaalgos/split.cc

@@ -0,0 +1,56 @@
+// -*- 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/>.
+
+#include <spot/twaalgos/split.hh>
+
+namespace spot
+{
+  twa_graph_ptr split_edges(const const_twa_graph_ptr& aut)
+  {
+    twa_graph_ptr out = make_twa_graph(aut->get_dict());
+    out->copy_acceptance_of(aut);
+    out->copy_ap_of(aut);
+    out->prop_copy(aut, twa::prop_set::all());
+    out->new_states(aut->num_states());
+    out->set_init_state(aut->get_init_state_number());
+
+    internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph());
+
+    bdd all = aut->ap_vars();
+    for (auto& e: aut->edges())
+      {
+        bdd cond = e.cond;
+        if (cond == bddfalse)
+          continue;
+        unsigned dst = e.dst;
+        if (aut->is_univ_dest(dst))
+          {
+            auto d = aut->univ_dests(dst);
+            dst = uniq.new_univ_dests(d.begin(), d.end());
+          }
+        while (cond != bddfalse)
+          {
+            bdd cube = bdd_satoneset(cond, all, bddfalse);
+            cond -= cube;
+            out->new_edge(e.src, dst, cube, e.acc);
+          }
+      }
+    return out;
+  }
+}

spot/twaalgos/split.hh

@@ -0,0 +1,33 @@
+// -*- 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/>.
+
+#pragma once
+
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  /// \brief transform edges into transitions
+  ///
+  /// Create a new version of the automaton where all edges are split
+  /// so that they are all labeled by a conjunction of all atomic
+  /// propositions.  After this we can consider that each edge of the
+  /// automate is a transition labeled by one letter.
+  SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut);
+}

tests/Makefile.am

@@ -247,6 +247,7 @@ TESTS_twa = \
   core/sccdot.test \
   core/sccsimpl.test \
   core/sepsets.test \
+  core/split.test \
   core/dbacomp.test \
   core/obligation.test \
   core/wdba.test \

tests/core/split.test

@@ -0,0 +1,29 @@
+#!/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
+
+test 3,7 = `ltl2tgba 'a U b' --stats=%e,%t`
+test 7,7 = `ltl2tgba 'a U b' | autfilt --split --stats=%e,%t`
+test 12,12 = `ltl2tgba 'a U b' | autfilt -C --split --stats=%e,%t`
+test 0,0 = `ltl2tgba 0 | autfilt --split --stats=%e,%t`
+test 1,1 = `ltl2tgba 0 | autfilt -C --split --stats=%e,%t`

tests/python/alternating.py

@@ -137,3 +137,35 @@ State: 4
 State: 5
 [0&1] 0&1&2
 --END--"""
+
+h = spot.split_edges(aut).to_str('hoa')
+print(h)
+assert h == """HOA: v1
+States: 6
+Start: 0
+AP: 2 "p1" "p2"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: univ-branch trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0&!1] 1&2 {0}
+[0&1] 1&2 {0}
+[!0&1] 0&1
+[0&1] 0&1
+State: 1
+[0&1] 0&1&2
+State: 2
+[!0&1] 2
+[0&!1] 2
+[0&1] 2
+State: 3
+[0&!1] 1&2
+[0&1] 1&2
+[!0&1] 0&1&2
+[0&1] 0&1&2
+State: 4
+[0&1] 0&1&2
+State: 5
+[0&1] 0&1&2
+--END--"""