common_output.hh 4.16 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
3
// et 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
#pragma once
21

22
#include "common_sys.hh"
23
24

#include <argp.h>
25
26
#include <map>
#include <memory>
27
28
#include <spot/tl/formula.hh>
#include <spot/twaalgos/stats.hh>
29
#include <spot/misc/timer.hh>
30
#include "common_output.hh"
31
#include "common_file.hh"
32

33
enum output_format_t { spot_output, spin_output, utf8_output,
34
                       lbt_output, wring_output, latex_output,
35
                       quiet_output, count_output };
36
37
extern output_format_t output_format;
extern bool full_parenth;
38
extern bool escape_csv;
39

40
41
42
43
44
45
46
47
48
49
50
#define COMMON_X_OUTPUT_SPECS(where)                                    \
      "number of atomic propositions " #where "; "      \
      " add LETTERS to list atomic propositions with "                  \
      "(n) no quoting, "                                                \
      "(s) occasional double-quotes with C-style escape, "              \
      "(d) double-quotes with C-style escape, "                         \
      "(c) double-quotes with CSV-style escape, "                       \
      "(p) between parentheses, "                                       \
      "any extra non-alphanumeric character will be used to "           \
      "separate propositions"

51
52
53
54
55
56
57
58
59
#define COMMON_LTL_OUTPUT_SPECS                                         \
    { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,                   \
        "the length (or size) of the formula", 0 },                     \
    { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,                   \
        "the Boolean-length of the formula (i.e., all Boolean "         \
        "subformulas count as 1)", 0 },                                 \
    { "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,           \
        "the class of the formula is the Manna-Pnueli hierarchy "       \
        "([v] replaces abbreviations by class names, [w] for all "      \
60
61
62
63
        "compatible classes)", 0 },                                     \
    { "%x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,                       \
        OPTION_DOC | OPTION_NO_USAGE,                                   \
        COMMON_X_OUTPUT_SPECS(used in the formula), 0 }
64

65
66
67
extern const struct argp output_argp;

int parse_opt_output(int key, char* arg, struct argp_state* state);
68

69
70
71
// Low-level output
std::ostream&
stream_formula(std::ostream& out,
72
               spot::formula f, const char* filename, int linenum);
73

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
void output_formula_checked(spot::formula f,
75
                            spot::process_timer* ptimer = nullptr,
76
77
78
                            const char* filename = nullptr, int linenum = 0,
                            const char* prefix = nullptr,
                            const char* suffix = nullptr);
79
80
81


class printable_formula:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
82
  public spot::printable_value<spot::formula>
83
84
85
{
public:
  printable_formula&
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
86
  operator=(spot::formula new_val)
87
88
89
90
91
92
  {
    val_ = new_val;
    return *this;
  }

  virtual void
93
  print(std::ostream& os, const char*) const override;
94
95
96
97
98
99
100
101
};

class aut_stat_printer: protected spot::stat_printer
{
public:
  aut_stat_printer(std::ostream& os, const char* format)
    : spot::stat_printer(os, format)
  {
102
    declare('f', &formula_);        // Override the formula printer.
103
104
  }

105
106
  using spot::formater::set_output;

107
  std::ostream&
108
  print(const spot::const_twa_graph_ptr& aut,
109
        spot::formula f = nullptr)
110
111
  {
    formula_ = f;
112
    return this->spot::stat_printer::print(aut, f);
113
114
115
116
  }

  printable_formula formula_;
};