ltldo.cc 8.67 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
// -*- coding: utf-8 -*-
// Copyright (C) 2015 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 <sstream>
#include <fstream>
26
#include <sys/wait.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
27 28 29 30 31 32 33 34 35 36

#include "error.h"

#include "common_setup.hh"
#include "common_cout.hh"
#include "common_conv.hh"
#include "common_finput.hh"
#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_trans.hh"
37
#include "common_hoaread.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38

39
#include "tl/relabel.hh"
40
#include "misc/bareword.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
41
#include "misc/timer.hh"
42 43
#include "twaalgos/lbtt.hh"
#include "twaalgos/relabel.hh"
44
#include "twaalgos/totgba.hh"
45
#include "parseaut/public.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46 47 48 49 50 51 52

const char argp_program_doc[] ="\
Run LTL/PSL formulas through another program, performing conversion\n\
of input and output as required.";

static const argp_option options[] =
  {
53 54
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55 56 57 58 59
  };


static const argp_option more_o_format[] =
  {
60
    { "%R", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
61
      "serial number of the formula translated", 0 },
62
    { "%T", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
      "tool used for translation", 0 },
64
    { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
      "formula translated", 0 },
66
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
  };

// This is not very elegant, but we need to add the above %-escape
// sequences to those of aoutput_o_fromat_argp for the --help output.
// So far I've failed to instruct argp to merge those two lists into a
// single block.
static const struct argp*
build_percent_list()
{
  const argp_option* iter = aoutput_o_format_argp.options;
  unsigned count = 0;
  while (iter->name || iter->doc)
    {
      ++count;
      ++iter;
    }

  unsigned s = count * sizeof(argp_option);
  argp_option* d =
    static_cast<argp_option*>(malloc(sizeof(more_o_format) + s));
  memcpy(d, aoutput_o_format_argp.options, s);
  memcpy(d + count, more_o_format, sizeof(more_o_format));

  static const struct argp more_o_format_argp =
91
    { d, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
92 93 94 95 96
  return &more_o_format_argp;
}

const struct argp_child children[] =
  {
97
    { &hoaread_argp, 0, "Parsing of automata:", 3 },
98 99 100 101 102 103
    { &finput_argp, 0, nullptr, 1 },
    { &trans_argp, 0, nullptr, 3 },
    { &aoutput_argp, 0, nullptr, 4 },
    { build_percent_list(), 0, nullptr, 5 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
  };

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  switch (key)
    {
    case ARGP_KEY_ARG:
      translators.push_back(arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

namespace
{
  class xtranslator_runner: public translator_runner
  {
  public:
    xtranslator_runner(spot::bdd_dict_ptr dict)
      : translator_runner(dict, true)
    {
    }

130
    spot::twa_graph_ptr
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
    translate(unsigned int translator_num, bool& problem, double& duration)
    {
      output.reset(translator_num);

      std::ostringstream command;
      format(command, translators[translator_num].cmd);

      std::string cmd = command.str();
      //std::cerr << "Running [" << l << translator_num << "]: "
      // << cmd << std::endl;
      spot::stopwatch sw;
      sw.start();
      int es = exec_with_timeout(cmd.c_str());
      duration = sw.stop();

146
      spot::twa_graph_ptr res = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
      if (timed_out)
	{
	  problem = false;	// A timeout is considered benign
	  std::cerr << "warning: timeout during execution of command \""
		    << cmd << "\"\n";
	  ++timeout_count;
	}
      else if (WIFSIGNALED(es))
	{
	  problem = true;
	  es = WTERMSIG(es);
	  std::cerr << "error: execution of command \"" << cmd
		    << "\" terminated by signal " << es << ".\n";
	}
      else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
	{
	  problem = true;
	  es = WEXITSTATUS(es);
	  std::cerr << "error: execution of command \"" << cmd
		    << "\" returned exit code " << es << ".\n";
	}
168
      else if (output.val())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
169 170
	{
	  problem = false;
171 172 173

	  spot::parse_aut_error_list pel;
	  std::string filename = output.val()->name();
174 175 176
	  auto aut = spot::parse_aut(filename, pel, dict,
				     spot::default_environment::instance(),
				     opt_parse);
177
	  if (!pel.empty())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
178
	    {
179 180 181 182
	      problem = true;
	      std::cerr << "error: failed to parse the automaton "
		"produced by \"" << cmd << "\".\n";
	      spot::format_parse_aut_errors(std::cerr, filename, pel);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
183 184
	      res = nullptr;
	    }
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
	  else if (!aut)
	    {
	      problem = true;
	      std::cerr << "error: command \"" << cmd
			<< "\" produced an empty output.\n";
	      res = nullptr;
	    }
	  else if (aut->aborted)
	    {
	      problem = true;
	      std::cerr << "error: command \"" << cmd
			<< "\" aborted its output.\n";
	      res = nullptr;
	    }
	  else
	    {
	      res = aut->aut;
	    }
	}
      else			// No automaton output
	{
	  problem = false;
	  res = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
	}

      output.cleanup();
      return res;
    }
  };


  class processor: public job_processor
  {
    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
    xtranslator_runner runner;
    automaton_printer printer;
    spot::postprocessor& post;
    spot::printable_value<std::string> cmdname;
    spot::printable_value<unsigned> roundval;
    spot::printable_value<std::string> inputf;

  public:
    processor(spot::postprocessor& post)
      : runner(dict), post(post)
    {
      printer.add_stat('T', &cmdname);
      printer.add_stat('R', &roundval);
      printer.add_stat('f', &inputf);
    }

    ~processor()
    {
    }

    int
    process_string(const std::string& input,
		   const char* filename,
		   int linenum)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
244 245
      spot::parse_error_list pel;
      spot::formula f = parse_formula(input, pel);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
246 247 248 249 250

      if (!f || !pel.empty())
	{
	  if (filename)
	    error_at_line(0, 0, filename, linenum, "parse error:");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
251
	  spot::format_parse_errors(std::cerr, input, pel);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
252 253 254 255 256 257 258 259 260 261
	  return 1;
	}

      inputf = input;
      process_formula(f, filename, linenum);
      return 0;
    }


    int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
262
    process_formula(spot::formula f,
263
		    const char* filename = nullptr, int linenum = 0)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
264
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
265
      std::unique_ptr<spot::relabeling_map> relmap;
266 267 268

      // If atomic propositions are incompatible with one of the
      // output, relabel the formula.
269
      if ((!f.has_lbt_atomic_props() &&
270
	   (runner.has('l') || runner.has('L') || runner.has('T')))
271
	  || (!f.has_spin_atomic_props() &&
272 273
	      (runner.has('s') || runner.has('S'))))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
274 275
	  relmap.reset(new spot::relabeling_map);
	  f = spot::relabel(f, spot::Pnn, relmap.get());
276 277
	}

278
      static unsigned round = 1;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
279 280 281 282 283 284 285 286 287 288 289 290
      runner.round_formula(f, round);

      unsigned ts = translators.size();
      for (unsigned t = 0; t < ts; ++t)
	{
	  bool problem;
	  double translation_time;
	  auto aut = runner.translate(t, problem, translation_time);
	  if (problem)
	    error_at_line(2, 0, filename, linenum, "aborting here");
	  if (aut)
	    {
291 292
	      if (relmap)
		relabel_here(aut, relmap.get());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293 294 295 296 297 298 299
	      aut = post.run(aut, f);
	      cmdname = translators[t].name;
	      roundval = round;
	      printer.print(aut, f, filename, linenum, translation_time,
			    nullptr);
	    };
	}
300
      spot::cleanup_tmpfiles();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
301 302 303 304 305 306 307 308 309 310 311 312
      ++round;
      return 0;
    }
  };
}

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

  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
313
		    argp_program_doc, children, nullptr, nullptr };
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
314 315 316 317

  // Disable post-processing as much as possible by default.
  level = spot::postprocessor::Low;
  pref = spot::postprocessor::Any;
318
  type = spot::postprocessor::Generic;
319
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
320 321 322 323 324 325 326 327 328 329 330 331
    exit(err);

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

  if (translators.empty())
    error(2, 0, "No translator to run?  Run '%s --help' for usage.",
	  program_name);

  setup_sig_handler();

  spot::postprocessor post;
332
  post.set_pref(pref | comp | sbacc);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
333 334 335
  post.set_type(type);
  post.set_level(level);

336 337 338 339 340 341 342 343 344 345
  try
    {
      processor p(post);
      if (p.run())
	return 2;
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346 347
  return 0;
}