convert: twa to twacube translation

* spot/twacube/Makefile.am, spot/twacube/twacube.cc,
spot/twacube/twacube.hh, spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/twacube.cc,
tests/core/twacube.test: here.

spot/twacube/Makefile.am

@@ -25,8 +25,9 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 twacubedir = $(pkgincludedir)/twacube
 
-twacube_HEADERS =  cube.hh
+twacube_HEADERS =  cube.hh twacube.hh
 
 noinst_LTLIBRARIES = libtwacube.la
 libtwacube_la_SOURCES = \
-   cube.cc
+   cube.cc \
+   twacube.cc

spot/twacube/twacube.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Developpement 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 "twacube.hh"
+#include <iostream>
+
+namespace spot
+{
+  cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_))
+  {
+  }
+  cstate::cstate(unsigned int id): id_(id)
+  {
+  }
+
+  cstate::~cstate()
+  { }
+
+  unsigned int cstate::label()
+  {
+    return id_;
+  }
+
+  transition::transition(transition&& t) noexcept:
+  cube_(std::move(t.cube_)), acc_(std::move(t.acc_))
+  {  }
+
+  transition::transition(const cube& cube,
+			 acc_cond::mark_t acc):
+    cube_(cube),  acc_(acc)
+  { }
+
+  transition::~transition()
+  { }
+
+  transition::transition()
+  { }
+
+  twacube::twacube(const std::vector<std::string>& aps):
+    init_(0U), aps_(aps), cubeset_(aps.size())
+  {
+  }
+
+  twacube::~twacube()
+  {
+    spot::cubeset cs = get_cubeset();
+    for (unsigned int i = 1; i <= theg_.num_edges(); ++i)
+      cs.release(theg_.edge_data(i).cube_);
+  }
+
+  const acc_cond& twacube::acc() const
+  {
+    return acc_;
+  }
+
+  acc_cond& twacube::acc()
+  {
+    return acc_;
+  }
+
+  const std::vector<std::string>&  twacube::get_ap()
+  {
+    return aps_;
+  }
+
+  unsigned int twacube::new_state()
+  {
+    return theg_.new_state();
+  }
+
+  void twacube::set_initial(unsigned int init)
+  {
+    init_ = init;
+  }
+
+  unsigned int twacube::get_initial()
+  {
+    if (theg_.num_states() == 0)
+      new_state();
+
+    return init_;
+  }
+
+  cstate* twacube::state_from_int(unsigned int i)
+  {
+    return &theg_.state_data(i);
+  }
+
+  void
+  twacube::create_transition(unsigned int src, const cube& cube,
+			     const acc_cond::mark_t& mark, unsigned int dst)
+  {
+    theg_.new_edge(src, dst, cube, mark);
+  }
+
+  const cubeset&
+  twacube::get_cubeset()  const
+  {
+    return cubeset_;
+  }
+
+  bool
+  twacube::succ_contiguous() const
+  {
+    unsigned int i = 1;
+    while (i <= theg_.num_edges())
+      {
+	unsigned int j = i;
+
+	// Walk first bucket of successors
+	while (j <= theg_.num_edges() &&
+	       theg_.edge_storage(i).src == theg_.edge_storage(j).src)
+	  ++j;
+
+	// Remove the next bucket
+	unsigned int itmp = j;
+
+	// Look if there are some transitions missing in this bucket.
+	while (j <= theg_.num_edges())
+	  {
+	    if (theg_.edge_storage(i).src == theg_.edge_storage(j).src)
+	      return false;
+	    ++j;
+	  }
+	i = itmp;
+      }
+    return true;
+  }
+
+  std::ostream&
+  operator<<(std::ostream& os, const twacube& twa)
+  {
+    spot::cubeset cs = twa.get_cubeset();
+    os << "init : " << twa.init_ << '\n';
+     for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i)
+       os << twa.theg_.edge_storage(i).src << "->"
+	  << twa.theg_.edge_storage(i).dst <<  " : "
+	  << cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
+	  << ' ' << twa.theg_.edge_data(i).acc_
+	  << '\n';
+    return os;
+  }
+}

spot/twacube/twacube.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 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 <vector>
+#include <iosfwd>
+#include <spot/graph/graph.hh>
+#include <spot/twa/acc.hh>
+#include <spot/twacube/cube.hh>
+
+namespace spot
+{
+  class SPOT_API cstate
+  {
+  public:
+    cstate() {}
+    cstate(const cstate& s) = delete;
+    cstate(cstate&& s) noexcept;
+    cstate(unsigned int id);
+    virtual ~cstate();
+    unsigned int label();
+  private:
+    unsigned int id_;
+  };
+
+  class SPOT_API transition
+  {
+  public:
+    cube cube_;
+    acc_cond::mark_t acc_;
+    transition();
+    transition(const transition& t) = delete;
+    transition(transition&& t) noexcept;
+    transition(const cube& cube, acc_cond::mark_t acc);
+    virtual ~transition();
+  };
+
+  class SPOT_API trans_index final
+  {
+  public:
+    typedef digraph<cstate, transition> graph_t;
+    typedef graph_t::edge_storage_t edge_storage_t;
+
+    trans_index(trans_index& ci) = delete;
+    trans_index(unsigned int state, graph_t& g):
+      st_(g.state_storage(state))
+    {
+      reset();
+    }
+
+    trans_index(trans_index&& ci):
+      idx_(ci.idx_),
+      st_(ci.st_)
+    {
+    }
+
+    inline void reset()
+    {
+      idx_ = st_.succ;
+    }
+
+    inline void next()
+    {
+      ++idx_;
+    }
+
+    inline bool done() const
+    {
+      return !idx_ || idx_ > st_.succ_tail;
+    }
+
+    inline unsigned int current(unsigned int seed = 0) const
+    {
+      // no-swarming : since twacube are dedicated for parallelism, i.e.
+      // swarming, we expect swarming is activated.
+      if (SPOT_UNLIKELY(!seed))
+	return idx_;
+      // swarming.
+      return (((idx_-st_.succ+1)*seed) % (st_.succ_tail-st_.succ+1)) + st_.succ;
+    }
+
+  private:
+    unsigned int idx_;
+    const graph_t::state_storage_t& st_;
+  };
+
+  class SPOT_API twacube final
+  {
+  public:
+    twacube() = delete;
+    twacube(const std::vector<std::string>& aps);
+    virtual ~twacube();
+    const acc_cond& acc() const;
+    acc_cond& acc();
+    const std::vector<std::string>& get_ap();
+    unsigned int new_state();
+    void set_initial(unsigned int init);
+    unsigned int get_initial();
+    cstate* state_from_int(unsigned int i);
+    void create_transition(unsigned int src, const cube& cube,
+			   const acc_cond::mark_t& mark, unsigned int dst);
+    const cubeset& get_cubeset() const;
+    bool succ_contiguous() const;
+    typedef digraph<cstate, transition> graph_t;
+    const graph_t& get_graph()
+    {
+      return theg_;
+    }
+    typedef graph_t::edge_storage_t edge_storage_t;
+    const graph_t::edge_storage_t&
+      trans_storage(std::shared_ptr<trans_index> ci,
+		    unsigned int seed = 0) const
+    {
+      return theg_.edge_storage(ci->current(seed));
+    }
+    const transition& trans_data(std::shared_ptr<trans_index> ci,
+				 unsigned int seed = 0) const
+    {
+      return theg_.edge_data(ci->current(seed));
+    }
+
+    std::shared_ptr<trans_index> succ(unsigned int i)
+    {
+      return std::make_shared<trans_index>(i, theg_);
+    }
+
+    friend SPOT_API std::ostream& operator<<(std::ostream& os,
+    					     const twacube& twa);
+  private:
+    unsigned int init_;
+    acc_cond acc_;
+    const std::vector<std::string>& aps_;
+    graph_t theg_;
+    cubeset cubeset_;
+  };
+}

spot/twacube_algos/convert.cc

@@ -58,4 +58,76 @@ namespace spot
       }
     return result;
   }
+
+  spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut,
+				std::unordered_map<int, int>& ap_binder,
+				std::vector<std::string>& aps)
+  {
+    // Declare the twa cube
+    spot::twacube* tg = new spot::twacube(aps);
+
+    // Fix acceptance
+    tg->acc() = aut->acc();
+
+    // This binder maps twagraph indexes to twacube ones.
+    std::unordered_map<int, int> st_binder;
+
+    // Fill binder and create corresponding states into twacube
+    for (unsigned n = 0; n < aut->num_states(); ++n)
+      st_binder.insert({n, tg->new_state()});
+
+    // Fix the initial state
+    tg->set_initial(st_binder[aut->get_init_state_number()]);
+
+    // Get the cubeset
+    auto cs = tg->get_cubeset();
+
+    // Now just build all transitions of this automaton
+    // spot::cube cube(aps);
+    for (unsigned n = 0; n < aut->num_states(); ++n)
+      for (auto& t: aut->out(n))
+    	{
+    	  bdd cond = t.cond;
+
+    	  // Special case for bddfalse
+    	  if (cond == bddfalse)
+    	    {
+	      spot::cube cube = tg->get_cubeset().alloc();
+	      for (unsigned int i = 0; i < cs.size(); ++i)
+		cs.set_false_var(cube, i); // FIXME ! use fill!
+    	      tg->create_transition(st_binder[n], cube,
+    				    t.acc, st_binder[t.dst]);
+    	    }
+    	  else
+    	    // Split the bdd into multiple transitions
+    	    while (cond != bddfalse)
+    	      {
+    		bdd one = bdd_satone(cond);
+    		cond -= one;
+		spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
+    		tg->create_transition(st_binder[n], cube, t.acc,
+    				      st_binder[t.dst]);
+    	      }
+    	}
+    // Must be contiguous to support swarming.
+    assert(tg->succ_contiguous());
+    return tg;
+  }
+
+  std::vector<std::string>*
+  extract_aps(spot::twa_graph_ptr& aut,
+	      std::unordered_map<int, int>& ap_binder)
+  {
+    std::vector<std::string>* aps = new std::vector<std::string>();
+    for (auto f: aut->ap())
+      {
+	int size = aps->size();
+	if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end())
+	  {
+	    aps->push_back(f.ap_name());
+	    ap_binder.insert({aut->get_dict()->var_map[f], size});
+	  }
+      }
+    return aps;
+  }
 }

spot/twacube_algos/convert.hh

@@ -24,6 +24,8 @@
 #include <unordered_map>
 #include <spot/misc/common.hh>
 #include <spot/twacube/cube.hh>
+#include <spot/twacube/twacube.hh>
+#include <spot/twa/twagraph.hh>
 
 namespace spot
 {
@@ -37,4 +39,15 @@ namespace spot
   /// that bind cube indexes to bdd indexes.
   SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
   			   std::unordered_map<int, int>& reverse_binder);
+
+  /// \brief Extract the atomic propositions from the automaton
+  SPOT_API std::vector<std::string>*
+  extract_aps(spot::twa_graph_ptr& aut,
+	      std::unordered_map<int, int>& ap_binder);
+
+  /// \brief Convert a twa into a twacube
+  SPOT_API spot::twacube*
+  twa_to_twacube(spot::twa_graph_ptr& aut,
+		 std::unordered_map<int, int>& ap_binder,
+		 std::vector<std::string>& aps);
 }

tests/Makefile.am

@@ -98,7 +98,8 @@ check_PROGRAMS = \
   core/tgbagraph \
   core/tostring \
   core/tunabbrev \
-  core/tunenoform
+  core/tunenoform \
+  core/twacube
 
 # Keep this sorted alphabetically.
 core_acc_SOURCES = core/acc.cc
@@ -148,6 +149,7 @@ core_tunabbrev_SOURCES = core/equalsf.cc
 core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"'
 core_tunenoform_SOURCES = core/equalsf.cc
 core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"'
+core_twacube_SOURCES = core/twacube.cc
 
 
 TESTS_tl = \
@@ -318,7 +320,8 @@ TESTS_twa = \
   core/parity.test \
   core/parity2.test \
   core/ltlsynt.test \
-  core/rabin2parity.test
+  core/rabin2parity.test \
+  core/twacube.test
 
 ############################## PYTHON ##############################
 

tests/core/.gitignore

@@ -73,5 +73,6 @@ tripprod
 trival
 tunabbrev
 tunenoform
+twacube
 unabbrevwm
 safra

tests/core/twacube.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016 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 <bddx.h>
+
+#include <iostream>
+#include <spot/twacube/twacube.hh>
+#include <spot/twacube_algos/convert.hh>
+#include <iostream>
+#include <spot/twa/twagraph.hh>
+#include <spot/twaalgos/dot.hh>
+#include <spot/tl/defaultenv.hh>
+
+int main()
+{
+  // Build some TWA
+  auto d = spot::make_bdd_dict();
+  auto tg = make_twa_graph(d);
+  bdd p1 = bdd_ithvar(tg->register_ap("p1"));
+  bdd p2 = bdd_ithvar(tg->register_ap("p2"));
+  tg->acc().add_sets(2);
+  auto s1 = tg->new_state();
+  auto s2 = tg->new_state();
+  auto s3 = tg->new_state();
+  tg->new_edge(s1, s1, bddfalse, 0U);
+  tg->new_edge(s1, s2, p1, 0U);
+  tg->new_edge(s1, s3, p2, tg->acc().mark(1));
+  tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0));
+  tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1}));
+  tg->new_edge(s3, s2, p1 >> p2, 0U);
+  tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
+
+  // Map Bdd indexes to cube indexes
+  std::unordered_map<int, int> ap_binder;
+
+  // Get the set of propositions used by this automaton
+  std::vector<std::string>* aps = extract_aps(tg, ap_binder);
+
+  // Test translation
+  auto* aut = twa_to_twacube(tg, ap_binder, *aps);
+  spot::print_dot(std::cout, tg);
+  std::cout << "-----------\n" << *aut << "-----------\n";
+
+  unsigned int seed = 17;
+  for (auto it = aut->succ(2); !it->done(); it->next())
+    {
+      auto& t = aut->trans_storage(it, seed);
+      auto& d = aut->trans_data(it, seed);
+      std::cout << t.src << ' ' << t.dst << ' '
+		<< ' ' << aut->get_cubeset().dump(d.cube_, *aps)
+		<< ' ' << d.acc_
+		<< std::endl;
+    }
+
+  delete aps;
+  delete aut;
+}

tests/core/twacube.test

+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2014, 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 <http://www.gnu.org/licenses/>.
+
+# While running some benchmark, Tomáš Babiak found that Spot took too
+# much time (i.e. >1h) to translate those six formulae.  It turns out
+# that the WDBA minimization was performed after the degeneralization
+# algorithm, while this is not necessary (WDBA will produce a BA, so
+# we may as well skip degeneralization).  Translating these formulae
+# in the test-suite ensure that they don't take too much time (the
+# buildfarm will timeout if it does).
+
+. ./defs
+
+set -e
+
+run 0 ../twacube > stdout
+
+cat >expected <<EOF
+digraph G {
+  rankdir=LR
+  node [shape="circle"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="0"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="p1 | p2\n{0,1}"]
+  2 -> 1 [label="!p1 | p2"]
+  2 -> 2 [label="1\n{0,1}"]
+}
+-----------
+init : 0
+0->0 : !p1&!p2 {}
+0->1 : p1 {}
+0->2 : p2 {1}
+1->2 : p1&p2 {0}
+2->0 : !p1&p2 {0,1}
+2->0 : p1 {0,1}
+2->1 : !p1 {}
+2->1 : p1&p2 {}
+2->2 : 1 {0,1}
+-----------
+2 1  !p1 {}
+2 2  1 {0,1}
+2 0  p1 {0,1}
+2 1  p1&p2 {}
+2 0  !p1&p2 {0,1}
+EOF
+
+diff stdout expected