randaut.cc 12.2 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
// 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/>.

#include "common_sys.hh"

#include <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
#include <sstream>
#include <iterator>
#include "error.h"
29
#include "argmatch.h"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30 31 32 33

#include "common_setup.hh"
#include "common_range.hh"
#include "common_cout.hh"
34
#include "common_aoutput.hh"
35
#include "common_conv.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
36

37 38
#include <spot/misc/timer.hh>
#include <spot/misc/random.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39

40 41 42
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/randomgraph.hh>
#include <spot/twaalgos/canonicalize.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
43 44 45 46 47 48


const char argp_program_doc[] = "\
Generate random connected automata.\n\n\
The automata are built over the atomic propositions named by PROPS...\n\
or, if N is a nonnegative number, using N arbitrary names.\n\
49 50 51
If the density is set to D, and the number of states to Q, the degree\n\
of each state follows a normal distribution with mean 1+(Q-1)D and\n\
variance (Q-1)D(1-D).  In particular, for D=0 all states have a single\n\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
52 53 54 55 56
successor, while for D=1 all states are interconnected.\v\
Examples:\n\
\n\
This builds a random neverclaim with 4 states and labeled using the two\n\
atomic propositions \"a\" and \"b\":\n\
57
  % randaut --spin -Q4 a b\n\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58 59 60
\n\
This builds three random, complete, and deterministic TGBA with 5 to 10\n\
states, 1 to 3 acceptance sets, and three atomic propositions:\n\
61
  % randaut -n3 -D -H -Q5..10 -A1..3 3\n\
62 63 64
\n\
Build 3 random, complete, and deterministic Rabin automata\n\
with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\
65
a high density of edges, and 3 to 4 atomic propositions:\n\
66
  % randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
67 68
";

69 70
enum {
  OPT_SEED = 1,
71
  OPT_COLORED,
72
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
73 74 75 76

static const argp_option options[] =
  {
    /**************************************************/
77
    { nullptr, 0, nullptr, 0, "Generation:", 1 },
78 79
    { "acceptance", 'A', "ACCEPTANCE", 0,
      "specify the acceptance type of the automaton", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
80
    { "acc-probability", 'a', "FLOAT", 0,
81
      "probability that an edge belongs to one acceptance set (0.2)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
82 83
    { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\
      "use a negative value for unbounded generation", 0 },
84
    { "ba", 'B', nullptr, 0,
85
      "build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 },
86
    { "colored", OPT_COLORED, nullptr, 0,
87
      "build an automaton in which each edge (or state if combined with "
88
      "-S) belong to a single acceptance set", 0 },
89
    { "density", 'd', "FLOAT", 0, "density of the edges (0.2)", 0 },
90 91 92
    { "deterministic", 'D', nullptr, 0,
      "build a complete, deterministic automaton ", 0 },
    { "unique", 'u', nullptr, 0,
93 94
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
95 96
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
97
    { "states", 'Q', "RANGE", 0, "number of states to output (10)", 0 },
98 99 100
    { "state-based-acceptance", 'S', nullptr, 0,
      "used state-based acceptance", 0 },
    { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
    RANGE_DOC,
102
    { nullptr, 0, nullptr, 0, "ACCEPTANCE may be either a RANGE (in which case "
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
      "generalized Büchi is assumed), or an arbitrary acceptance formula "
      "such as 'Fin(0)|Inf(1)&Fin(2)' in the same syntax as in the HOA "
      "format, or one of the following patterns:\n"
      "  none\n"
      "  all\n"
      "  Buchi\n"
      "  co-Buchi\n"
      "  generalized-Buchi RANGE\n"
      "  generalized-co-Buchi RANGE\n"
      "  Rabin RANGE\n"
      "  Streett RANGE\n"
      "  generalized-Rabin INT RANGE RANGE ... RANGE\n"
      "  parity (min|max|rand) (odd|even|rand) RANGE\n"
      "  random RANGE\n"
      "  random RANGE PROBABILITY\n"
      "The random acceptance condition uses each set only once, "
      "unless a probability (to reuse the set again every time it is used) "
      "is given.", 2 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
121
    /**************************************************/
122 123
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124 125 126 127 128
  };


static const struct argp_child children[] =
  {
129 130 131 132
    { &aoutput_argp, 0, nullptr, 3 },
    { &aoutput_o_format_argp, 0, nullptr, 4 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
133 134
  };

135
static const char* opt_acceptance = nullptr;
136
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
137
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
138
static spot::atomic_prop_set aprops;
139
static range ap_count_given = {-1, -2}; // Must be two different negative val
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
140
static int opt_seed = 0;
141
static const char* opt_seed_str = "0";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142 143 144
static int opt_automata = 1;
static range opt_states = { 10, 10 };
static float opt_density = 0.2;
145
static range opt_acc_sets = { -1, 0 };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
146 147 148
static float opt_acc_prob = 0.2;
static bool opt_deterministic = false;
static bool opt_state_acc = false;
149
static bool opt_colored = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
150
static bool ba_wanted = false;
151 152
static bool generic_wanted = false;
static bool gba_wanted = false;
153
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154 155 156 157 158 159 160 161

static void
ba_options()
{
  opt_acc_sets = { 1, 1 };
  opt_state_acc = true;
}

162 163 164 165 166 167 168 169 170 171 172 173
// Range should have the form 12..34 or 12:34, maybe with spaces.  The
// characters between '.' and ':' include all digits plus '/', but the
// parser will later choke on '/' if it is used, so let's not worry
// here.
static bool
looks_like_a_range(const char* str)
{
  while (*str == ' ' || (*str >= '.' && *str <= ':'))
    ++str;
  return !*str;
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
static int
parse_opt(int key, char* arg, struct argp_state* as)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
    case 'a':
      opt_acc_prob = to_float(arg);
      if (opt_acc_prob < 0.0 || opt_acc_prob > 1.0)
	error(2, 0, "probability of acceptance set membership "
	      "should be between 0.0 and 1.0");
      break;
    case 'A':
190 191 192 193 194 195 196 197 198 199 200 201 202 203
      if (looks_like_a_range(arg))
	{
	  opt_acc_sets = parse_range(arg);
	  if (opt_acc_sets.min > opt_acc_sets.max)
	    std::swap(opt_acc_sets.min, opt_acc_sets.max);
	  if (opt_acc_sets.min < 0)
	    error(2, 0, "number of acceptance sets should be positive");
	  gba_wanted = true;
	}
      else
	{
	  opt_acceptance = arg;
	  generic_wanted = true;
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
      break;
    case 'B':
      ba_options();
      ba_wanted = true;
      break;
    case 'd':
      opt_density = to_float(arg);
      if (opt_density < 0.0 || opt_density > 1.0)
	error(2, 0, "density should be between 0.0 and 1.0");
      break;
    case 'D':
      opt_deterministic = true;
      break;
    case 'n':
      opt_automata = to_int(arg);
      break;
220
    case 'Q':
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
221 222 223
      opt_states = parse_range(arg);
      if (opt_states.min > opt_states.max)
	std::swap(opt_states.min, opt_states.max);
224 225
      if (opt_states.min == 0)
	error(1, 0, "cannot build an automaton with 0 states");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
226
      break;
227 228 229
    case 'S':
      opt_state_acc = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
230 231 232 233
    case 'u':
      opt_uniq =
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
234 235 236
    case OPT_COLORED:
      opt_colored = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
237 238
    case OPT_SEED:
      opt_seed = to_int(arg);
239
      opt_seed_str = arg;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240 241 242 243 244 245 246 247 248
      break;
    case ARGP_KEY_ARG:
      // If this is the unique non-option argument, it can
      // be a number of atomic propositions to build.
      //
      // argp reorganizes argv[] so that options always come before
      // non-options.  So if as->argc == as->next we know this is the
      // last non-option argument, and if aprops.empty() we know this
      // is the also the first one.
249
      if (aprops.empty() && as->argc == as->next && looks_like_a_range(arg))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
250
	{
251 252 253
	  ap_count_given = parse_range(arg);
	  // Create the set once if the count is fixed.
	  if (ap_count_given.min == ap_count_given.max)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
254
	    aprops = spot::create_atomic_prop_set(ap_count_given.min);
255
	  break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
256
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
257
      aprops.insert(spot::formula::ap(arg));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
258 259 260 261 262 263 264 265 266 267 268 269
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


int
main(int argc, char** argv)
{
270 271
  strcpy(F_doc, "seed number");
  strcpy(L_doc, "automaton number");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
272 273 274
  setup(argv);

  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
275
		    children, nullptr, nullptr };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
276

277
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
278 279 280 281
    exit(err);

  // running 'randaut 0' is one way to generate automata using no
  // atomic propositions so do not complain in that case.
282
  if (aprops.empty() && ap_count_given.max < 0)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
283 284 285
    error(2, 0, "No atomic proposition supplied?   Run '%s --help' for usage.",
	  program_name);

286 287 288 289 290
  if (generic_wanted && automaton_format == Spin)
    error(2, 0, "--spin implies --ba so should not be used with --acceptance");
  if (generic_wanted && ba_wanted)
    error(2, 0, "--acceptance and --ba may not be used together");

291
  if (automaton_format == Spin && opt_acc_sets.max > 1)
292
    error(2, 0, "--spin is incompatible with --acceptance=%d..%d",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293 294
	  opt_acc_sets.min, opt_acc_sets.max);
  if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1)
295
    error(2, 0, "--ba is incompatible with --acceptance=%d..%d",
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
296
	  opt_acc_sets.min, opt_acc_sets.max);
297 298 299 300 301
  if (ba_wanted && generic_wanted)
    error(2, 0, "--ba is incompatible with --acceptance=%s", opt_acceptance);

  if (automaton_format == Spin)
    ba_options();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
302

303 304 305 306 307 308 309 310 311 312
  if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted)
    error(2, 0, "--colored requires at least one acceptance set; "
	  "use --acceptance");
  if (opt_colored && opt_acc_sets.min == 0)
    error(2, 0, "--colored requires at least one acceptance set; "
	  "fix the range of --acceptance");

  if (opt_acc_sets.min == -1)
    opt_acc_sets.min = 0;

313 314


315 316 317 318
  try
    {
      spot::srand(opt_seed);
      auto d = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
319

320
      automaton_printer printer;
321

322 323
      constexpr unsigned max_trials = 10000;
      unsigned trials = max_trials;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
324

325
      int automaton_num = 0;
326

327 328 329 330 331
      for (;;)
	{
	  spot::stopwatch sw;
	  sw.start();

332 333 334 335
	  if (ap_count_given.max > 0
	      && ap_count_given.min != ap_count_given.max)
	    {
	      int c = spot::rrand(ap_count_given.min, ap_count_given.max);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
336
	      aprops = spot::create_atomic_prop_set(c);
337 338
	    }

339 340 341 342 343 344 345 346
	  int size = opt_states.min;
	  if (size != opt_states.max)
	    size = spot::rrand(size, opt_states.max);

	  int accs = opt_acc_sets.min;
	  if (accs != opt_acc_sets.max)
	    accs = spot::rrand(accs, opt_acc_sets.max);

347 348 349
	  spot::acc_cond::acc_code code;
	  if (opt_acceptance)
	    {
350
	      code = spot::acc_cond::acc_code(opt_acceptance);
351
	      accs = code.used_sets().max_set();
352 353 354
	      if (opt_colored && accs == 0)
		error(2, 0, "--colored requires at least one acceptance set; "
		      "fix the range of --acceptance");
355 356
	    }

357 358 359
	  auto aut =
	    spot::random_graph(size, opt_density, &aprops, d,
			       accs, opt_acc_prob, 0.5,
360 361
			       opt_deterministic, opt_state_acc,
			       opt_colored);
362

363 364
	  if (opt_acceptance)
	    aut->set_acceptance(accs, code);
365

366
	  if (opt_uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
367
	    {
368
	      auto tmp = spot::canonicalize
369
		(make_twa_graph(aut, spot::twa::prop_set::all()));
370 371
	      std::vector<tr_t> trans(tmp->edge_vector().begin() + 1,
				      tmp->edge_vector().end());
372 373 374 375 376 377 378 379 380
	      if (!opt_uniq->emplace(trans).second)
		{
		  --trials;
		  if (trials == 0)
		    error(2, 0, "failed to generate a new unique automaton"
			  " after %d trials", max_trials);
		  continue;
		}
	      trials = max_trials;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
	    }
382

383
	  auto runtime = sw.stop();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
384

385 386
	  printer.print(aut, nullptr,
			opt_seed_str, automaton_num, runtime, nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
387

388 389 390 391 392 393 394 395 396
	  ++automaton_num;
	  if (opt_automata > 0 && automaton_num >= opt_automata)
	    break;
	}
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
397
}