common_output.cc 10.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 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
#include "common_output.hh"
22
#include "common_aoutput.hh"
23
#include <iostream>
24
#include <sstream>
25
#include <spot/tl/print.hh>
26
27
#include <spot/tl/length.hh>
#include <spot/tl/apcollect.hh>
28
#include <spot/tl/hierarchy.hh>
29
30
#include <spot/misc/formater.hh>
#include <spot/misc/escape.hh>
31
#include "common_cout.hh"
32
#include "error.h"
33

34
35
36
37
38
39
40
enum {
  OPT_CSV = 1,
  OPT_FORMAT,
  OPT_LATEX,
  OPT_SPOT,
  OPT_WRING,
};
41
42
43

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

static const argp_option options[] =
  {
49
    { "full-parentheses", 'p', nullptr, 0,
50
      "output fully-parenthesized formulas", -20 },
51
52
53
54
55
56
    { "spin", 's', nullptr, 0, "output in Spin's syntax", -20 },
    { "spot", OPT_SPOT, nullptr, 0, "output in Spot's syntax (default)", -20 },
    { "lbt", 'l', nullptr, 0, "output in LBT's syntax", -20 },
    { "wring", OPT_WRING, nullptr, 0, "output in Wring's syntax", -20 },
    { "utf8", '8', nullptr, 0, "output using UTF-8 characters", -20 },
    { "latex", OPT_LATEX, nullptr, 0, "output using LaTeX macros", -20 },
57
58
59
    // --csv-escape was deprecated in Spot 2.1, we can remove it at
    // some point
    { "csv-escape", OPT_CSV, nullptr, OPTION_HIDDEN,
60
      "quote the formula for use in a CSV file", -20 },
61
62
    { "format", OPT_FORMAT, "FORMAT", 0,
      "specify how each line should be output (default: \"%f\")", -20 },
63
64
65
66
    { "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 },
67
    { "zero-terminated-output", '0', nullptr, 0,
68
69
      "separate output formulas with \\0 instead of \\n "
      "(for use with xargs -0)", 0 },
70
    { nullptr, 0, nullptr, 0, nullptr, 0 }
71
72
  };

73
const struct argp output_argp = { options, parse_opt_output,
74
75
                                  nullptr, nullptr, nullptr,
                                  nullptr, nullptr };
76

77
static
78
void
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
79
report_not_ltl(spot::formula f,
80
               const char* filename, int linenum, const char* syn)
81
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
82
  std::string s = spot::str_psl(f);
83
84
85
86
87
88
89
90
  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);
}

91
std::ostream&
92
stream_formula(std::ostream& out,
93
               spot::formula f, const char* filename, int linenum)
94
95
96
{
  switch (output_format)
    {
97
    case lbt_output:
98
      if (f.is_ltl_formula())
99
        spot::print_lbt_ltl(out, f);
100
      else
101
        report_not_ltl(f, filename, linenum, "LBT");
102
      break;
103
    case spot_output:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
104
      spot::print_psl(out, f, full_parenth);
105
106
      break;
    case spin_output:
107
      if (f.is_ltl_formula())
108
        spot::print_spin_ltl(out, f, full_parenth);
109
      else
110
        report_not_ltl(f, filename, linenum, "Spin");
111
      break;
112
    case wring_output:
113
      if (f.is_ltl_formula())
114
        spot::print_wring_ltl(out, f);
115
      else
116
        report_not_ltl(f, filename, linenum, "Wring");
117
      break;
118
    case utf8_output:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
      spot::print_utf8_psl(out, f, full_parenth);
120
      break;
121
    case latex_output:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
122
      spot::print_latex_psl(out, f, full_parenth);
123
      break;
124
    case count_output:
125
126
    case quiet_output:
      break;
127
    }
128
  return out;
129
130
}

131
132
static void
stream_escapable_formula(std::ostream& os,
133
134
                         spot::formula f,
                         const char* filename, int linenum)
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
{
  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);
    }
}


151
152
153
154
namespace
{
  struct formula_with_location
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
155
    spot::formula f;
156
157
    const char* filename;
    int line;
158
159
    const char* prefix;
    const char* suffix;
160
161
  };

162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
  class printable_formula_class final:
    public spot::printable_value<char>
  {
  public:
    printable_formula_class&
    operator=(char new_val)
    {
      val_ = new_val;
      return *this;
    }

    virtual void
    print(std::ostream& os, const char* opt) const override
    {
      if (*opt == '[')
177
178
179
        os << spot::mp_class(val_, opt + 1);
      else
        os << val_;
180
181
182
    }
  };

183
  class printable_formula final:
184
185
186
187
188
189
190
191
192
193
194
    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
195
    print(std::ostream& os, const char*) const override
196
    {
197
      stream_escapable_formula(os, val_->f, val_->filename, val_->line);
198
199
200
    }
  };

201
  class formula_printer final: protected spot::formater
202
203
204
205
206
  {
  public:
    formula_printer(std::ostream& os, const char* format)
      : format_(format)
    {
207
      declare('a', &ap_);       // deprecated in 2.3.2
208
      declare('b', &bool_size_);
209
210
211
      declare('f', &fl_);
      declare('F', &filename_);
      declare('L', &line_);
212
      declare('s', &size_);
213
      declare('h', &class_);
214
      declare('x', &ap_);
215
216
      declare('<', &prefix_);
      declare('>', &suffix_);
217
      set_output(os);
218
      prime(format);
219
220
221
222
223
224
225
226
    }

    std::ostream&
    print(const formula_with_location& fl)
    {
      fl_ = &fl;
      filename_ = fl.filename ? fl.filename : "";
      line_ = fl.line;
227
228
      prefix_ = fl.prefix ? fl.prefix : "";
      suffix_ = fl.suffix ? fl.suffix : "";
229
      auto f = fl_.val()->f;
230
      if (has('a') || has('x'))
231
232
        {
          auto s = spot::atomic_prop_collect(f);
233
          ap_.set(s->begin(), s->end());
234
235
236
237
238
239
          delete s;
        }
      if (has('b'))
        bool_size_ = spot::length_boolone(f);
      if (has('s'))
        size_ = spot::length(f);
240
241
      if (has('h'))
        class_ = spot::mp_class(f);
242
243
244
245
246
247
248
      auto& res = format(format_);
      // Make sure we do not store the formula until the next one is
      // printed, as the order in which APs are registered may
      // influence the automata output.
      fl_ = nullptr;
      ap_.clear();
      return res;
249
250
251
252
253
254
255
    }

  private:
    const char* format_;
    printable_formula fl_;
    spot::printable_value<const char*> filename_;
    spot::printable_value<int> line_;
256
257
    spot::printable_value<const char*> prefix_;
    spot::printable_value<const char*> suffix_;
258
    spot::printable_value<int> size_;
259
    printable_formula_class class_;
260
    spot::printable_value<int> bool_size_;
261
    printable_varset ap_;
262
263
264
  };
}

265
static formula_printer* format = nullptr;
266
static std::ostringstream outputname;
267
static formula_printer* outputnamer = nullptr;
268
static std::map<std::string, std::unique_ptr<output_file>> outputfiles;
269
270
271
272
273
274
275

int
parse_opt_output(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
276
277
278
    case '0':
      output_terminator = 0;
      break;
279
280
281
282
283
284
    case '8':
      output_format = utf8_output;
      break;
    case 'l':
      output_format = lbt_output;
      break;
285
286
287
    case 'o':
      outputnamer = new formula_printer(outputname, arg);
      break;
288
289
290
291
292
293
    case 'p':
      full_parenth = true;
      break;
    case 's':
      output_format = spin_output;
      break;
294
295
296
    case OPT_CSV:
      escape_csv = true;
      break;
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
    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;
}


317
static void
318
output_formula(std::ostream& out,
319
320
321
               spot::formula f,
               const char* filename = nullptr, int linenum = 0,
               const char* prefix = nullptr, const char* suffix = nullptr)
322
323
324
{
  if (!format)
    {
325
      if (prefix)
326
        out << prefix << ',';
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
      // For backward compatibility, we still run
      // stream_escapable_formula when --csv-escape has been given.
      // But eventually --csv-escape should be removed, and the
      // formula printed raw.
      if ((prefix || suffix) && !escape_csv)
        {
          std::ostringstream tmp;
          stream_formula(tmp, f, filename, linenum);
          std::string tmpstr = tmp.str();
          if (tmpstr.find_first_of("\",") != std::string::npos)
            {
              out << '"';
              spot::escape_rfc4180(out, tmpstr);
              out << '"';
            }
          else
            {
              out << tmpstr;
            }
        }
      else
        {
          stream_escapable_formula(out, f, filename, linenum);
        }
351
      if (suffix)
352
        out << ',' << suffix;
353
354
355
    }
  else
    {
356
      formula_with_location fl = { f, filename, linenum, prefix, suffix };
357
358
      format->print(fl);
    }
359
}
360

361
362
363
364
365
366
void
::printable_formula::print(std::ostream& os, const char*) const
{
  output_formula(os, val_);
}

367
void
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
output_formula_checked(spot::formula f,
369
370
                       const char* filename, int linenum,
                       const char* prefix, const char* suffix)
371
{
372
373
374
  if (output_format == count_output)
    {
      if (outputnamer)
375
376
        throw std::runtime_error
          ("options --output and --count are incompatible");
377
378
379
      return;
    }
  if (output_format == quiet_output)
380
    return;
381
382
383
384
385
386
387
388
389
  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)
390
        p.first->second.reset(new output_file(fname.c_str()));
391
392
393
      out = &p.first->second->ostream();
    }
  output_formula(*out, f, filename, linenum, prefix, suffix);
394
  *out << output_terminator;
395
396
397
  // Make sure we abort if we can't write to std::cout anymore
  // (like disk full or broken pipe with SIGPIPE ignored).
  check_cout();
398
}