spot/spot/twacube_algos/convert.cc

// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 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 <spot/twacube_algos/convert.hh>
#include <assert.h>

namespace spot
{
  spot::cube satone_to_cube(bdd one, cubeset& cubeset,
			    std::unordered_map<int, int>& binder)
  {
    auto cube = cubeset.alloc();
    while (one != bddtrue)
      {
	if (bdd_high(one) == bddfalse)
	  {
	    assert(binder.find(bdd_var(one)) != binder.end());
	    cubeset.set_false_var(cube, binder[bdd_var(one)]);
	    one = bdd_low(one);
	  }
	else
	  {
	    assert(binder.find(bdd_var(one)) != binder.end());
	    cubeset.set_true_var(cube, binder[bdd_var(one)]);
	    one = bdd_high(one);
	  }
      }
    return cube;
  }

  bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
		  std::unordered_map<int, int>& reverse_binder)
  {
    bdd result = bddtrue;
    for (unsigned int i = 0; i < cubeset.size(); ++i)
      {
    	assert(reverse_binder.find(i) != reverse_binder.end());
	if (cubeset.is_false_var(cube, i))
    	  result &= bdd_nithvar(reverse_binder[i]);
	if (cubeset.is_true_var(cube, i))
    	  result &= bdd_ithvar(reverse_binder[i]);
      }
    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::twa_graph_ptr
  twacube_to_twa(spot::twacube* twacube)
  {
    // Grab necessary variables
    auto& theg = twacube->get_graph();
    spot::cubeset cs = twacube->get_cubeset();

    // Build the resulting graph
    auto d = spot::make_bdd_dict();
    auto res = make_twa_graph(d);

    // Fix the acceptance of the resulting automaton
    res->acc() = twacube->acc();

    // Grep bdd id for each atomic propositions
    std::vector<int> bdds_ref;
    for (auto& ap : twacube->get_ap())
      bdds_ref.push_back(res->register_ap(ap));

    // Build all resulting states
    for (unsigned int i = 0; i < theg.num_states(); ++i)
      {
	unsigned st = res->new_state();
	(void) st;
	assert(st == i);
      }

    // Build all resulting conditions.
    for (unsigned int i = 1; i <= theg.num_edges(); ++i)
      {
	bdd cond = bddtrue;
	for (unsigned j = 0; j < cs.size(); ++j)
	  {
	    if (cs.is_true_var(theg.edge_data(i).cube_, j))
	      cond &= bdd_ithvar(bdds_ref[j]);
	    else if (cs.is_false_var(theg.edge_data(i).cube_, j))
	      cond &= bdd_nithvar(bdds_ref[j]);
	    // otherwise it 's a free variable do nothing
	  }

	res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
		      cond, theg.edge_data(i).acc_);
      }

    // Fix the initial state
    res->set_init_state(twacube->get_initial());

    return res;
  }
}