autfilt.cc 12.1 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et 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 <string>
#include <iostream>

#include <argp.h>
#include "error.h"

#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
#include "common_post.hh"

#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
35
#include "tgbaalgos/hoa.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
36 37 38 39 40 41
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh"
#include "tgba/bddprint.hh"
#include "misc/optionmap.hh"
#include "misc/timer.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
43 44
#include "hoaparse/public.hh"
#include "tgbaalgos/sccinfo.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
#include "tgbaalgos/randomize.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46 47


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
static const char argp_program_doc[] ="\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49 50 51 52 53 54 55 56 57
Convert, transform, and filter Büchi automata.\n\
";


#define OPT_TGBA 1
#define OPT_DOT 2
#define OPT_LBTT 3
#define OPT_SPOT 4
#define OPT_STATS 5
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58 59
#define OPT_RANDOMIZE 6
#define OPT_SEED 7
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
60 61 62 63 64 65 66 67 68 69 70 71 72

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Input:", 1 },
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Output automaton type:", 2 },
    { "tgba", OPT_TGBA, 0, 0,
      "Transition-based Generalized Büchi Automaton (default)", 0 },
    { "ba", 'B', 0, 0, "Büchi Automaton", 0 },
    { "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
73
      "of the given property)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
    /**************************************************/
    { 0, 0, 0, 0, "Output format:", 3 },
    { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
    { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
      "Output the automaton in HOA format.  Add letters to select "
      "(s) state-based acceptance, (t) transition-based acceptance, "
      "(m) mixed acceptance, (l) single-line output", 0 },
    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
      "LBTT's format (add =t to force transition-based acceptance even"
      " on Büchi automata)", 0 },
    { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
    { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
    { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
      "(ignored with --lbtt or --spin)", 0 },
    { "stats", OPT_STATS, "FORMAT", 0,
      "output statistics about the automaton", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
      "the following interpreted sequences (capitals for input,"
      " minuscules for output):", 4 },
    { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "name of the input file", 0 },
    { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of states", 0 },
    { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of edges", 0 },
    { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of transitions", 0 },
    { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of acceptance pairs or sets", 0 },
    { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs", 0 },
    { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of nondeterministic states in output", 0 },
    { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is deterministic, 0 otherwise", 0 },
    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is complete, 0 otherwise", 0 },
    { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "conversion time (including post-processings, but not parsing)"
      " in seconds", 0 },
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
118 119 120 121 122
    { 0, 0, 0, 0, "Transformation:", -1 },
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
      "randomize states and transitions (specify 's' or 't' to"
      "randomize only states or transitions)", 0 },
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
123 124 125
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126 127
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128 129 130
    { 0, 0, 0, 0, 0, 0 }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
131
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132 133 134 135 136 137
  {
    { &post_argp_disabled, 0, 0, 20 },
    { &misc_argp, 0, 0, -1 },
    { 0, 0, 0, 0 }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa }
  format = Dot;
static const char* stats = "";
static const char* hoa_opt = 0;
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;

static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as an integer.", s);
  return res;
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
    case 'B':
      type = spot::postprocessor::BA;
      break;
    case 'F':
      jobs.emplace_back(arg, true);
      break;
    case 'H':
      format = Hoa;
174
      hoa_opt = arg;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
      break;
    case 'M':
      type = spot::postprocessor::Monitor;
      break;
    case 's':
      format = Spin;
      if (type != spot::postprocessor::Monitor)
	type = spot::postprocessor::BA;
      break;
    case 'x':
      {
	const char* opt = extra_options.parse_options(arg);
	if (opt)
	  error(2, 0, "failed to parse --options near '%s'", opt);
      }
      break;
    case OPT_DOT:
      format = Dot;
      break;
    case OPT_LBTT:
      if (arg)
	{
	  if (arg[0] == 't' && arg[1] == 0)
	    format = Lbtt_t;
	  else
	    error(2, 0, "unknown argument for --lbtt: '%s'", arg);
	}
      else
	{
	  format = Lbtt;
	}
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
    case OPT_RANDOMIZE:
      if (arg)
	{
	  for (auto p = arg; *p; ++p)
	    switch (*p)
	      {
	      case 's':
		randomize_st = true;
		break;
	      case 't':
		randomize_tr = true;
		break;
	      default:
		error(2, 0, "unknown argument for --randomize: '%c'", *p);
	      }
	}
      else
	{
	  randomize_tr = true;
	  randomize_st = true;
	}
      break;
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
    case OPT_SPOT:
      format = Spot;
      break;
    case OPT_STATS:
      if (!*arg)
	error(2, 0, "empty format string for --stats");
      stats = arg;
      format = Stats;
      break;
    case OPT_TGBA:
      if (format == Spin)
	error(2, 0, "--spin and --tgba are incompatible");
      type = spot::postprocessor::TGBA;
      break;
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
  /// \brief prints various statistics about a TGBA
  ///
  /// This object can be configured to display various statistics
  /// about a TGBA.  Some %-sequence of characters are interpreted in
  /// the format string, and replaced by the corresponding statistics.
  class hoa_stat_printer: protected spot::stat_printer
  {
  public:
    hoa_stat_printer(std::ostream& os, const char* format)
      : spot::stat_printer(os, format)
    {
      declare('A', &haut_acc_);
      declare('C', &haut_scc_);
      declare('E', &haut_edges_);
      declare('F', &filename_);
      declare('f', &filename_);	// Override the formula printer.
      declare('S', &haut_states_);
      declare('T', &haut_trans_);
    }

    /// \brief print the configured statistics.
    ///
    /// The \a f argument is not needed if the Formula does not need
    /// to be output.
    std::ostream&
    print(const spot::const_hoa_aut_ptr& haut,
	  const spot::const_tgba_digraph_ptr& aut,
	  const char* filename, double run_time)
    {
      filename_ = filename;

      if (has('T'))
	{
	  spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
	  haut_states_ = s.states;
	  haut_edges_ = s.transitions;
	  haut_trans_ = s.sub_transitions;
	}
      else if (has('E'))
	{
	  spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
	  haut_states_ = s.states;
	  haut_edges_ = s.transitions;
	}
      else if (has('S'))
	{
	  haut_states_ = haut->aut->num_states();
	}

      if (has('A'))
	haut_acc_ = haut->aut->acc().num_sets();

      if (has('C'))
	haut_scc_ = spot::scc_info(haut->aut).scc_count();

      return this->spot::stat_printer::print(aut, 0, run_time);
    }

  private:
    spot::printable_value<const char*> filename_;
    spot::printable_value<unsigned> haut_states_;
    spot::printable_value<unsigned> haut_edges_;
    spot::printable_value<unsigned> haut_trans_;
    spot::printable_value<unsigned> haut_acc_;
    spot::printable_value<unsigned> haut_scc_;
  };


  class hoa_processor: public job_processor
  {
  public:
    spot::postprocessor& post;
    hoa_stat_printer statistics;

    hoa_processor(spot::postprocessor& post)
      : post(post), statistics(std::cout, stats)
    {
    }

    int
    process_formula(const spot::ltl::formula*, const char*, int)
    {
      SPOT_UNREACHABLE();
    }

    int
345 346
    process_automaton(const spot::const_hoa_aut_ptr& haut,
		      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
347 348 349 350 351 352
    {
      spot::stopwatch sw;
      sw.start();
      auto aut = post.run(haut->aut, nullptr);
      const double conversion_time = sw.stop();

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
353 354 355
      if (randomize_st || randomize_tr)
	spot::randomize(aut, randomize_st, randomize_tr);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
356 357 358 359 360 361 362 363 364 365 366 367 368 369
      switch (format)
	{
	case Dot:
	  spot::dotty_reachable(std::cout, aut,
				(type == spot::postprocessor::BA)
				|| (type == spot::postprocessor::Monitor));
	  break;
	case Lbtt:
	  spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
	  break;
	case Lbtt_t:
	  spot::lbtt_reachable(std::cout, aut, false);
	  break;
	case Hoa:
370
	  spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371 372 373 374 375 376 377 378 379 380 381 382 383 384
	  break;
	case Spot:
	  spot::tgba_save_reachable(std::cout, aut);
	  break;
	case Spin:
	  spot::never_claim_reachable(std::cout, aut);
	  break;
	case Stats:
	  statistics.print(haut, aut, filename, conversion_time) << '\n';
	  break;
	}
      flush_cout();
      return 0;
    }
385

386 387 388 389 390 391
    int
    aborted(const spot::const_hoa_aut_ptr& h, const char* filename)
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
392 393 394 395 396 397 398 399 400 401 402 403

    int
    process_file(const char* filename)
    {
      spot::hoa_parse_error_list pel;
      auto b = spot::make_bdd_dict();
      auto hp = spot::hoa_stream_parser(filename);

      int err = 0;

      for (;;)
	{
404
	  pel.clear();
405 406 407 408 409 410
	  auto haut = hp.parse(pel, b);
	  if (!haut && pel.empty())
	    break;
	  if (spot::format_hoa_parse_errors(std::cerr, filename, pel))
	    err = 2;
	  if (!haut)
411
	    error(2, 0, "failed to read automaton from %s", filename);
412 413
	  else if (haut->aborted)
	    err = std::max(err, aborted(haut, filename));
414 415 416 417 418 419
	  else
	    process_automaton(haut, filename);
	}

      return err;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
  };
}

int
main(int argc, char** argv)
{
  setup(argv);

  const argp ap = { options, parse_opt, "[FILENAMES...]",
		    argp_program_doc, children, 0, 0 };

  // Disable post-processing as much as possible by default.
  level = spot::postprocessor::Low;
  pref = spot::postprocessor::Any;
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
    exit(err);

  if (jobs.empty())
    jobs.emplace_back("-", true);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
440 441
  spot::srand(opt_seed);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
442 443 444 445 446 447
  spot::postprocessor post(&extra_options);
  post.set_pref(pref | comp);
  post.set_type(type);
  post.set_level(level);

  hoa_processor processor(post);
448 449 450 451 452 453 454 455 456
  try
    {
      if (processor.run())
	return 2;
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
457 458
  return 0;
}