randomgraph.cc 6.67 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de
3
// Recherche et Développement de l'Epita (LRDE).
4
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22
23

#include "randomgraph.hh"
24
#include "twa/twagraph.hh"
25
#include "misc/random.hh"
26
#include "misc/bddlt.hh"
27
#include "ltlast/atomic_prop.hh"
28
29
30
#include <sstream>
#include <list>
#include <set>
31
#include <iterator>
32
#include <vector>
33
34
35
36
37
38

namespace spot
{

  namespace
  {
39
    static unsigned
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
    random_deterministic_labels_rec(std::vector<bdd>& labels, int *props,
				    int props_n, bdd current, unsigned n)
    {
      if (n >  1 && props_n >= 1)
        {
	  bdd ap = bdd_ithvar(*props);
          ++props;
	  --props_n;

	  // There are m labels generated from "current & ap"
	  // and n - m labels generated from "current & !ap"
          unsigned m = rrand(1, n - 1);
	  if (2 * m < n)
	    {
	      m = n - m;
	      ap = !ap;
	    }

	  unsigned res = random_deterministic_labels_rec(labels, props,
							 props_n,
							 current & ap, m);
	  res += random_deterministic_labels_rec(labels, props, props_n,
						 current & !ap, n - res);
          return res;
        }
      else
        {
	  labels.push_back(current);
          return 1;
        }
    }

72
    static std::vector<bdd>
73
74
75
76
77
78
79
    random_deterministic_labels(int *props, int props_n, unsigned n)
    {
      std::vector<bdd> bddvec;
      random_deterministic_labels_rec(bddvec, props, props_n, bddtrue, n);
      return bddvec;
    }

80
81
    static acc_cond::mark_t
    random_acc(unsigned n_accs, float a)
82
83
84
85
    {
      acc_cond::mark_t m = 0U;
      for (unsigned i = 0U; i < n_accs; ++i)
	if (drand() < a)
86
	  m.set(i);
87
88
89
      return m;
    }

90
91
92
93
94
95
96
    static acc_cond::mark_t
    random_acc1(unsigned n_accs)
    {
      auto u = static_cast<unsigned>(mrand(static_cast<int>(n_accs)));
      return acc_cond::mark_t({u});
    }

97
98
    bdd
    random_labels(int* props, int props_n, float t)
99
    {
100
101
      int val = 0;
      int size = 0;
102
      bdd p = bddtrue;
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
      while (props_n)
	{
	  if (size == 8 * sizeof(int))
	    {
	      p &= bdd_ibuildcube(val, size, props);
	      props += size;
	      val = 0;
	      size = 0;
	    }
	  val <<= 1;
	  val |= (drand() < t);
	  ++size;
	  --props_n;
	}
      if (size > 0)
	p &= bdd_ibuildcube(val, size, props);
119

120
      return p;
121
122
123
    }
  }

124
  twa_graph_ptr
125
  random_graph(int n, float d,
126
	       const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
127
	       unsigned n_accs, float a, float t,
128
	       bool deterministic, bool state_acc, bool colored)
129
  {
130
    assert(n > 0);
131
    auto res = make_twa_graph(dict);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132
133
134
135
    if (deterministic)
      res->prop_deterministic();
    if (state_acc)
      res->prop_state_based_acc();
136

137
138
139
140
    int props_n = ap->size();
    int* props = new int[props_n];

    int pi = 0;
141
142
    for (auto i: *ap)
      props[pi++] = dict->register_proposition(i, res);
143

144
    res->set_generalized_buchi(n_accs);
145

146
    // Using std::unordered_set instead of std::set for these sets is 3
147
    // times slower (tested on a 50000 nodes example).
148
    typedef std::set<int> node_set;
149
150
151
    node_set nodes_to_process;
    node_set unreachable_nodes;

152
    res->new_states(n);
153
154

    std::vector<unsigned> state_randomizer(n);
155
    state_randomizer[0] = 0;
156
    nodes_to_process.insert(0);
157
158

    for (int i = 1; i < n; ++i)
159
      {
160
	state_randomizer[i] = i;
161
	unreachable_nodes.insert(i);
162
      }
163
164

    // We want to connect each node to a number of successors between
165
166
    // 1 and n.  If the probability to connect to each successor is d,
    // the number of connected successors follows a binomial distribution.
167
    barand<nrand> bin(n - 1, d);
168
169
170

    while (!nodes_to_process.empty())
      {
171
	auto src = *nodes_to_process.begin();
172
173
	nodes_to_process.erase(nodes_to_process.begin());

174
175
	// Choose a random number of successors (at least one), using
	// a binomial distribution.
176
	unsigned nsucc = 1 + bin.rand();
177

178
	bool saw_unreachable = false;
179
180
181
182

	// Create NSUCC random labels.
	std::vector<bdd> labels;
	if (deterministic)
183
	  {
184
185
186
187
188
189
190
191
192
193
194
195
	    labels = random_deterministic_labels(props, props_n, nsucc);

	    // if nsucc > 2^props_n, we cannot produce nsucc deterministic
	    // transitions so we set it to labels.size()
	    nsucc = labels.size();
	  }
	else
	  for (unsigned i = 0; i < nsucc; ++i)
	    labels.push_back(random_labels(props, props_n, t));

        int possibilities = n;
	unsigned dst;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
196
197
	acc_cond::mark_t m = 0U;
	if (state_acc)
198
	  m = colored ? random_acc1(n_accs) : random_acc(n_accs, a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
199

200
201
	for (auto& l: labels)
	  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202
	    if (!state_acc)
203
	      m = colored ? random_acc1(n_accs) : random_acc(n_accs, a);
204

205
206
	    // No connection to unreachable successors so far.  This
	    // is our last chance, so force it now.
207
208
209
	    if (--nsucc == 0
		&& !unreachable_nodes.empty()
		&& !saw_unreachable)
210
211
212
213
214
	      {
		// Pick a random unreachable node.
		int index = mrand(unreachable_nodes.size());
		node_set::const_iterator i = unreachable_nodes.begin();
		std::advance(i, index);
215

216
		// Link it from src.
217
		res->new_transition(src, *i, l, m);
218
		nodes_to_process.insert(*i);
219
		unreachable_nodes.erase(*i);
220
221
		break;
	      }
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239

            // Pick the index of a random node.
            int index = mrand(possibilities--);

            // Permute it with state_randomizer[possibilities], so
            // we cannot pick it again.
            dst = state_randomizer[index];
            state_randomizer[index] = state_randomizer[possibilities];
            state_randomizer[possibilities] = dst;

            res->new_transition(src, dst, l, m);
            auto j = unreachable_nodes.find(dst);
            if (j != unreachable_nodes.end())
              {
                nodes_to_process.insert(dst);
                unreachable_nodes.erase(j);
                saw_unreachable = true;
              }
240
	  }
241

242
	// The node must have at least one successor.
243
	assert(res->get_graph().state_storage(src).succ);
244
      }
245
246
247
    // All nodes must be reachable.
    assert(unreachable_nodes.empty());
    delete[] props;
248
249
250
    return res;
  }
}