randaut.cc 9.75 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

#include "ltlenv/defaultenv.hh"
38
#include "misc/timer.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39 40 41 42
#include "misc/random.hh"

#include "tgba/bddprint.hh"
#include "tgbaalgos/randomgraph.hh"
43
#include "tgbaalgos/canonicalize.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64


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\
If the density is set to D, and the number of states to S, the degree\n\
of each state follows a normal distribution with mean 1+(S-1)D and\n\
variance (S-1)D(1-D).  In particular, for D=0 all states have a single\n\
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\
  % randaut --spin -S4 a b\n\
\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\
  % randaut -n 3 --hoa -S5..10 -A1..3 3\n\
";

65 66 67
enum {
  OPT_SEED = 1,
  OPT_STATE_ACC,
68
  OPT_ACC_TYPE,
69
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
70 71 72 73 74

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Generation:", 2 },
75 76 77
    { "acc-type", OPT_ACC_TYPE, "buchi|random", 0,
      "use a generalized buchi acceptance condition (default), or a "
      "random acceptance condition", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
78 79 80 81 82 83 84 85 86 87
    { "acc-sets", 'A', "RANGE", 0, "number of acceptance sets (0)", 0 },
    { "acc-probability", 'a', "FLOAT", 0,
      "probability that a transition belong to one acceptance set (0.2)", 0 },
    { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\
      "use a negative value for unbounded generation", 0 },
    { "ba", 'B', 0, 0,
      "build a Buchi automaton (implies --acc-sets=1 --state-acc)", 0 },
    { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 },
    { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ",
      0 },
88
    { "unique", 'u', 0, 0,
89 90
      "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
91 92 93 94 95 96
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
    { "states", 'S', "RANGE", 0, "number of states to output (10)", 0 },
    { "state-acc", OPT_STATE_ACC, 0, 0, "use state-based acceptance", 0 },
    RANGE_DOC,
    /**************************************************/
97
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98 99 100 101 102 103
    { 0, 0, 0, 0, 0, 0 }
  };


static const struct argp_child children[] =
  {
104 105
    { &aoutput_argp, 0, 0, 3 },
    { &aoutput_o_format_argp, 0, 0, 4 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
106 107 108 109
    { &misc_argp, 0, 0, -1 },
    { 0, 0, 0, 0 }
  };

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
enum acc_type { acc_buchi, acc_random };

static char const *const acc_args[] =
{
  "buchi", "ba", "gba",
  "random",
  0
};
static acc_type const acc_types[] =
{
  acc_buchi, acc_buchi, acc_buchi,
  acc_random,
};
ARGMATCH_VERIFY(acc_args, acc_types);


static acc_type opt_acc = acc_buchi;
127 128
typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t;
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
129 130 131
static spot::ltl::atomic_prop_set aprops;
static bool ap_count_given = false;
static int opt_seed = 0;
132
static const char* opt_seed_str = "0";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
133 134 135 136 137 138 139 140
static int opt_automata = 1;
static range opt_states = { 10, 10 };
static float opt_density = 0.2;
static range opt_acc_sets = { 0, 0 };
static float opt_acc_prob = 0.2;
static bool opt_deterministic = false;
static bool opt_state_acc = false;
static bool ba_wanted = false;
141
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191

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

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':
      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");
      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;
    case 'S':
      opt_states = parse_range(arg);
      if (opt_states.min > opt_states.max)
	std::swap(opt_states.min, opt_states.max);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
192 193 194 195
    case 'u':
      opt_uniq =
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
196 197 198
    case OPT_ACC_TYPE:
      opt_acc = XARGMATCH("--acc-type", arg, acc_args, acc_types);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
199 200
    case OPT_SEED:
      opt_seed = to_int(arg);
201
      opt_seed_str = arg;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
      break;
    case OPT_STATE_ACC:
      opt_state_acc = true;
      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.
      if (aprops.empty() && as->argc == as->next)
	{
	  char* endptr;
	  int res = strtol(arg, &endptr, 10);
	  if (!*endptr && res >= 0) // arg is a number
	    {
	      ap_count_given = true;
	      aprops = spot::ltl::create_atomic_prop_set(res);
	      break;
	    }
	}
225
      aprops.insert(spot::ltl::default_environment::instance().require(arg));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
226 227 228 229 230 231 232 233 234 235 236 237
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


int
main(int argc, char** argv)
{
238 239
  strcpy(F_doc, "seed number");
  strcpy(L_doc, "automaton number");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240 241 242 243 244 245 246 247 248 249 250 251 252 253
  setup(argv);

  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
		    children, 0, 0 };

  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
    exit(err);

  // running 'randaut 0' is one way to generate automata using no
  // atomic propositions so do not complain in that case.
  if (aprops.empty() && !ap_count_given)
    error(2, 0, "No atomic proposition supplied?   Run '%s --help' for usage.",
	  program_name);

254
  if (automaton_format == Spin && opt_acc_sets.max > 1)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
255 256
    error(2, 0, "--spin is incompatible with --acc-sets=%d..%d",
	  opt_acc_sets.min, opt_acc_sets.max);
257 258 259
  if (automaton_format == Spin && opt_acc != acc_buchi)
    error(2, 0,
	  "--spin implies --acc-type=buchi but a different --acc-type is used");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
260 261 262
  if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1)
    error(2, 0, "--ba is incompatible with --acc-sets=%d..%d",
	  opt_acc_sets.min, opt_acc_sets.max);
263 264 265
  if (ba_wanted && opt_acc != acc_buchi)
    error(2, 0,
	  "--ba implies --acc-type=buchi but a different --acc-type is used");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
266

267 268 269 270
  try
    {
      spot::srand(opt_seed);
      auto d = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
271

272
      automaton_printer printer;
273

274 275
      constexpr unsigned max_trials = 10000;
      unsigned trials = max_trials;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
276

277
      int automaton_num = 0;
278

279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
      for (;;)
	{
	  spot::stopwatch sw;
	  sw.start();

	  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);

	  auto aut =
	    spot::random_graph(size, opt_density, &aprops, d,
			       accs, opt_acc_prob, 0.5,
			       opt_deterministic, opt_state_acc);

297 298 299 300 301 302 303 304 305 306
	  switch (opt_acc)
	    {
	    case acc_buchi:
	      // Random_graph builds a GBA by default
	      break;
	    case acc_random:
	      aut->set_acceptance(accs, spot::random_acceptance(accs));
	      break;
	    }

307
	  if (opt_uniq)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
	    {
309
	      auto tmp = spot::canonicalize
310
		(make_tgba_digraph(aut, spot::twa::prop_set::all()));
311 312 313 314 315 316 317 318 319 320 321
	      std::vector<tr_t> trans(tmp->transition_vector().begin() + 1,
				      tmp->transition_vector().end());
	      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
322
	    }
323

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

326 327
	  printer.print(aut, nullptr,
			opt_seed_str, automaton_num, runtime, nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
328

329 330 331 332 333 334 335 336 337
	  ++automaton_num;
	  if (opt_automata > 0 && automaton_num >= opt_automata)
	    break;
	}
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
338
  spot::ltl::destroy_atomic_prop_set(aprops);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
339
}