common_output.cc 8.13 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#include "common_sys.hh"
21
22
#include "common_output.hh"
#include <iostream>
23
#include <sstream>
24
#include "ltlvisit/print.hh"
25
#include "misc/formater.hh"
26
#include "misc/escape.hh"
27
#include "common_cout.hh"
28
#include "error.h"
29

30
31
32
33
34
35
36
enum {
  OPT_CSV = 1,
  OPT_FORMAT,
  OPT_LATEX,
  OPT_SPOT,
  OPT_WRING,
};
37
38
39

output_format_t output_format = spot_output;
bool full_parenth = false;
40
bool escape_csv = false;
41
char output_terminator = '\n';
42
43
44
45
46
47
48

static const argp_option options[] =
  {
    { "full-parentheses", 'p', 0, 0,
      "output fully-parenthesized formulas", -20 },
    { "spin", 's', 0, 0, "output in Spin's syntax", -20 },
    { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", -20 },
49
    { "lbt", 'l', 0, 0, "output in LBT's syntax", -20 },
50
    { "wring", OPT_WRING, 0, 0, "output in Wring's syntax", -20 },
51
    { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 },
52
    { "latex", OPT_LATEX, 0, 0, "output using LaTeX macros", -20 },
53
54
    { "csv-escape", OPT_CSV, 0, 0, "quote the formula for use in a CSV file",
      -20 },
55
56
    { "format", OPT_FORMAT, "FORMAT", 0,
      "specify how each line should be output (default: \"%f\")", -20 },
57
58
59
60
    { "output", 'o', "FORMAT", 0,
      "send output to a file named FORMAT instead of standard output.  The"
      " first formula sent to a file truncates it unless FORMAT starts"
      " with '>>'.", 0 },
61
62
63
    { "zero-terminated-output", '0', 0, 0,
      "separate output formulas with \\0 instead of \\n "
      "(for use with xargs -0)", 0 },
64
65
66
67
68
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp output_argp = { options, parse_opt_output, 0, 0, 0, 0, 0 };

69
static
70
void
71
report_not_ltl(spot::ltl::formula f,
72
73
	       const char* filename, int linenum, const char* syn)
{
74
  std::string s = spot::ltl::str_psl(f);
75
76
77
78
79
80
81
82
  static const char msg[] =
    "formula '%s' cannot be written %s's syntax because it is not LTL";
  if (filename)
    error_at_line(2, 0, filename, linenum, msg, s.c_str(), syn);
  else
    error(2, 0, msg, s.c_str(), syn);
}

83
std::ostream&
84
stream_formula(std::ostream& out,
85
	       spot::ltl::formula f, const char* filename, int linenum)
86
87
88
{
  switch (output_format)
    {
89
    case lbt_output:
90
      if (f.is_ltl_formula())
91
	spot::ltl::print_lbt_ltl(out, f);
92
93
94
      else
	report_not_ltl(f, filename, linenum, "LBT");
      break;
95
    case spot_output:
96
      spot::ltl::print_psl(out, f, full_parenth);
97
98
      break;
    case spin_output:
99
      if (f.is_ltl_formula())
100
	spot::ltl::print_spin_ltl(out, f, full_parenth);
101
102
      else
	report_not_ltl(f, filename, linenum, "Spin");
103
      break;
104
    case wring_output:
105
      if (f.is_ltl_formula())
106
	spot::ltl::print_wring_ltl(out, f);
107
108
109
      else
	report_not_ltl(f, filename, linenum, "Wring");
      break;
110
    case utf8_output:
111
      spot::ltl::print_utf8_psl(out, f, full_parenth);
112
      break;
113
    case latex_output:
114
      spot::ltl::print_latex_psl(out, f, full_parenth);
115
      break;
116
    case count_output:
117
118
    case quiet_output:
      break;
119
    }
120
  return out;
121
122
}

123
124
static void
stream_escapable_formula(std::ostream& os,
125
			 spot::ltl::formula f,
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
			 const char* filename, int linenum)
{
  if (escape_csv)
    {
      std::ostringstream out;
      stream_formula(out, f, filename, linenum);
      os << '"';
      spot::escape_rfc4180(os, out.str());
      os << '"';
    }
  else
    {
      stream_formula(os, f, filename, linenum);
    }
}


143
144
145
146
namespace
{
  struct formula_with_location
  {
147
    spot::ltl::formula f;
148
149
    const char* filename;
    int line;
150
151
    const char* prefix;
    const char* suffix;
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  };

  class printable_formula:
    public spot::printable_value<const formula_with_location*>
  {
  public:
    printable_formula&
    operator=(const formula_with_location* new_val)
    {
      val_ = new_val;
      return *this;
    }

    virtual void
    print(std::ostream& os, const char*) const
    {
168
      stream_escapable_formula(os, val_->f, val_->filename, val_->line);
169
170
171
172
173
174
175
176
177
178
179
180
    }
  };

  class formula_printer: protected spot::formater
  {
  public:
    formula_printer(std::ostream& os, const char* format)
      : format_(format)
    {
      declare('f', &fl_);
      declare('F', &filename_);
      declare('L', &line_);
181
182
      declare('<', &prefix_);
      declare('>', &suffix_);
183
184
185
186
187
188
189
190
191
      set_output(os);
    }

    std::ostream&
    print(const formula_with_location& fl)
    {
      fl_ = &fl;
      filename_ = fl.filename ? fl.filename : "";
      line_ = fl.line;
192
193
      prefix_ = fl.prefix ? fl.prefix : "";
      suffix_ = fl.suffix ? fl.suffix : "";
194
195
196
197
198
199
200
201
      return format(format_);
    }

  private:
    const char* format_;
    printable_formula fl_;
    spot::printable_value<const char*> filename_;
    spot::printable_value<int> line_;
202
203
    spot::printable_value<const char*> prefix_;
    spot::printable_value<const char*> suffix_;
204
205
206
207
  };
}

static formula_printer* format = 0;
208
209
210
static std::ostringstream outputname;
static formula_printer* outputnamer = 0;
static std::map<std::string, std::unique_ptr<output_file>> outputfiles;
211
212
213
214
215
216
217

int
parse_opt_output(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
218
219
220
    case '0':
      output_terminator = 0;
      break;
221
222
223
224
225
226
    case '8':
      output_format = utf8_output;
      break;
    case 'l':
      output_format = lbt_output;
      break;
227
228
229
    case 'o':
      outputnamer = new formula_printer(outputname, arg);
      break;
230
231
232
233
234
235
    case 'p':
      full_parenth = true;
      break;
    case 's':
      output_format = spin_output;
      break;
236
237
238
    case OPT_CSV:
      escape_csv = true;
      break;
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
    case OPT_LATEX:
      output_format = latex_output;
      break;
    case OPT_SPOT:
      output_format = spot_output;
      break;
    case OPT_WRING:
      output_format = wring_output;
      break;
    case OPT_FORMAT:
      delete format;
      format = new formula_printer(std::cout, arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


259
static void
260
output_formula(std::ostream& out,
261
	       spot::ltl::formula f,
262
263
	       const char* filename = nullptr, int linenum = 0,
	       const char* prefix = nullptr, const char* suffix = nullptr)
264
265
266
{
  if (!format)
    {
267
      if (prefix)
268
	out << prefix << ',';
269
      stream_escapable_formula(out, f, filename, linenum);
270
      if (suffix)
271
	out << ',' << suffix;
272
273
274
    }
  else
    {
275
      formula_with_location fl = { f, filename, linenum, prefix, suffix };
276
277
      format->print(fl);
    }
278
}
279

280
281
282
283
284
285
void
::printable_formula::print(std::ostream& os, const char*) const
{
  output_formula(os, val_);
}

286
void
287
output_formula_checked(spot::ltl::formula f,
288
289
290
		       const char* filename, int linenum,
		       const char* prefix, const char* suffix)
{
291
292
293
294
295
296
297
298
  if (output_format == count_output)
    {
      if (outputnamer)
	throw std::runtime_error
	  ("options --output and --count are incompatible");
      return;
    }
  if (output_format == quiet_output)
299
    return;
300
301
302
303
304
305
306
307
308
309
310
311
312
  std::ostream* out = &std::cout;
  if (outputnamer)
    {
      outputname.str("");
      formula_with_location fl = { f, filename, linenum, prefix, suffix };
      outputnamer->print(fl);
      std::string fname = outputname.str();
      auto p = outputfiles.emplace(fname, nullptr);
      if (p.second)
	p.first->second.reset(new output_file(fname.c_str()));
      out = &p.first->second->ostream();
    }
  output_formula(*out, f, filename, linenum, prefix, suffix);
313
  *out << output_terminator;
314
315
316
  // Make sure we abort if we can't write to std::cout anymore
  // (like disk full or broken pipe with SIGPIPE ignored).
  check_cout();
317
}