convert.cc 3.9 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
// -*- 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;
  }
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

  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;
  }
133
}