common_trans.hh 3.23 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
// -*- 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/>.

20
#pragma once
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
21 22 23 24 25

#include "common_sys.hh"
#include <vector>
#include <argp.h>

26 27 28
#include <spot/misc/formater.hh>
#include <spot/misc/tmpfile.hh>
#include <spot/twa/twagraph.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29 30 31 32 33 34 35 36 37 38 39 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 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96


extern const struct argp trans_argp;

struct translator_spec
{
  // The translator command, as specified on the command-line.
  // If this has the form of
  //    {name}cmd
  // then it is split in two components.
  // Otherwise, spec=cmd=name.
  const char* spec;
  // actual shell command (or spec)
  const char* cmd;
  // name of the translator (or spec)
  const char* name;

  translator_spec(const char* spec);
  translator_spec(const translator_spec& other);
  ~translator_spec();
};

extern std::vector<translator_spec> translators;

struct quoted_string final: public spot::printable_value<std::string>
{
  using spot::printable_value<std::string>::operator=;
  void print(std::ostream& os, const char* pos) const override;
};

struct printable_result_filename final:
  public spot::printable_value<spot::temporary_file*>
{
  unsigned translator_num;

  printable_result_filename();
  ~printable_result_filename();
  void reset(unsigned n);
  void cleanup();

  void print(std::ostream& os, const char* pos) const override;
};


class translator_runner: protected spot::formater
{
protected:
  spot::bdd_dict_ptr dict;
  // Round-specific variables
  quoted_string string_ltl_spot;
  quoted_string string_ltl_spin;
  quoted_string string_ltl_lbt;
  quoted_string string_ltl_wring;
  quoted_string filename_ltl_spot;
  quoted_string filename_ltl_spin;
  quoted_string filename_ltl_lbt;
  quoted_string filename_ltl_wring;
  // Run-specific variables
  printable_result_filename output;
public:
  using spot::formater::has;

  translator_runner(spot::bdd_dict_ptr dict,
		    // whether we accept the absence of output
		    // specifier
		    bool no_output_allowed = false);
  void string_to_tmp(std::string& str, unsigned n, std::string& tmpname);
  const std::string& formula() const;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
97
  void round_formula(spot::formula f, unsigned serial);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
};


// Disable handling of timeout on systems that miss kill() or alarm().
// For instance MinGW.
#if HAVE_KILL && HAVE_ALARM
# define ENABLE_TIMEOUT 1
#else
# define ENABLE_TIMEOUT 0
#endif

extern volatile bool timed_out;
extern unsigned timeout_count;
#if ENABLE_TIMEOUT
void setup_sig_handler();
int exec_with_timeout(const char* cmd);
#else // !ENABLE_TIMEOUT
#define exec_with_timeout(cmd) system(cmd)
#define setup_sig_handler() while (0);
#endif // !ENABLE_TIMEOUT