powerset.cc 3.23 KB
Newer Older
1
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Dveloppement
Guillaume Sadegh's avatar
Guillaume Sadegh committed
2
3
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
4
5
6
7
8
9
10
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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
11
// the Free Software Foundation; either version 3 of the License, or
12
13
14
15
16
17
18
19
// (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
20
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
21
22
23

#include <set>
#include <deque>
24
#include "powerset.hh"
25
26
27
28
29
30
#include "misc/hash.hh"
#include "tgbaalgos/powerset.hh"
#include "bdd.h"

namespace spot
{
31
32
  tgba_explicit_number*
  tgba_powerset(const tgba* aut, power_map& pm)
33
  {
34
35
36
    typedef power_map::power_state power_state;
    typedef std::map<power_map::power_state, int> power_set;
    typedef std::deque<power_map::power_state> todo_list;
37
38
39

    power_set seen;
    todo_list todo;
40
    tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict());
41
42
43
44

    {
      power_state ps;
      state* s = aut->get_init_state();
45
      pm.states.insert(s);
46
47
      ps.insert(s);
      todo.push_back(ps);
48
      seen[ps] = 1;
49
      pm.map_[1] = ps;
50
51
52
53
    }

    unsigned state_num = 1;

54
    while (!todo.empty())
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
      {
	power_state src = todo.front();
	todo.pop_front();
	// Compute all variables occurring on outgoing arcs.
	bdd all_vars = bddtrue;
	power_state::const_iterator i;

	for (i = src.begin(); i != src.end(); ++i)
	  all_vars &= aut->support_variables(*i);

	// Compute all possible combinations of these variables.
	bdd all_conds = bddtrue;
	while (all_conds != bddfalse)
	  {
	    bdd cond = bdd_satoneset(all_conds, all_vars, bddtrue);
	    all_conds -= cond;

	    // Construct the set of all states reachable via COND.
	    power_state dest;
	    for (i = src.begin(); i != src.end(); ++i)
	      {
		tgba_succ_iterator *si = aut->succ_iter(*i);
77
		for (si->first(); !si->done(); si->next())
78
79
		  if ((cond >> si->current_condition()) == bddtrue)
		    {
80
		      const state* s = pm.canonicalize(si->current_state());
81
82
83
84
85
86
87
88
		      dest.insert(s);
		    }
		delete si;
	      }
	    if (dest.empty())
	      continue;
	    // Add that transition.
	    power_set::const_iterator i = seen.find(dest);
89
	    int dest_num;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
90
	    state_explicit_number::transition* t;
91
92
	    if (i != seen.end())
	      {
93
94
		dest_num = i->second;
                t = res->create_transition(seen[src], dest_num);
95
96
97
	      }
	    else
	      {
98
99
		dest_num = ++state_num;
		seen[dest] = dest_num;
100
		pm.map_[dest_num] = dest;
101
		todo.push_back(dest);
102
                t = res->create_transition(seen[src], dest_num);
103
104
105
106
107
108
109
	      }
	    res->add_conditions(t, cond);
	  }
      }
    res->merge_transitions();
    return res;
  }
110
111
112
113
114
115
116

  tgba_explicit_number*
  tgba_powerset(const tgba* aut)
  {
    power_map pm;
    return tgba_powerset(aut, pm);
  }
117
}