common_aoutput.cc 8.55 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// 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
21
#include "common_sys.hh"
#include "error.h"
22
23
24
25
26

#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_cout.hh"

27
28
#include "tgba/bddprint.hh"

29
30
31
32
33
34
35
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/hoa.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh"

automaton_format_t automaton_format = Dot;
36
37
static const char* opt_dot = nullptr;
static const char* hoa_opt = nullptr;
38
const char* opt_name = nullptr;
39
40
41
42
43
44
45
46
47
48
49
50
static const char* stats = "";

#define OPT_DOT 1
#define OPT_LBTT 2
#define OPT_SPOT 3
#define OPT_STATS 4
#define OPT_NAME 5

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Output format:", 3 },
51
    { "dot", OPT_DOT, "c|h|n|N|s|t|v", OPTION_ARG_OPTIONAL,
52
53
      "GraphViz's format (default).  Add letters to chose (c) circular nodes, "
      "(h) horizontal layout, (v) vertical layout, (n) with name, "
54
55
      "(N) without name, (s) with SCCs, "
      "(t) always transition-based acceptance.", 0 },
56
57
58
59
60
61
62
    { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
      "Output the automaton in HOA format.  Add letters to select "
      "(s) state-based acceptance, (t) transition-based acceptance, "
      "(m) mixed acceptance, (l) single-line output", 0 },
    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
      "LBTT's format (add =t to force transition-based acceptance even"
      " on Büchi automata)", 0 },
63
64
    { "name", OPT_NAME, "FORMAT", 0,
      "set the name of the output automaton", 0 },
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
    { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
    { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
    { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
    { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
      "(ignored with --lbtt or --spin)", 0 },
    { "stats", OPT_STATS, "FORMAT", 0,
      "output statistics about the automaton", 0 },
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp aoutput_argp = { options, parse_opt_aoutput, 0, 0, 0, 0, 0 };

// Those can be overridden by individual tools. E.g. randaut has no
// notion of input file, so %F and %L represent something else.
char F_doc[32] = "name of the input file";
char L_doc[32] = "location in the input file";

static const argp_option io_options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
      "the following interpreted sequences (capitals for input,"
      " minuscules for output):", 4 },
    { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
    { "%M, %m", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
91
92
93
      "name of the automaton", 0 },
    { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of states", 0 },
    { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of edges", 0 },
94
95
96
    { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of transitions", 0 },
    { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
97
98
      "number of acceptance sets", 0 },
    { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 },
99
100
101
102
103
104
105
    { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of nondeterministic states in output", 0 },
    { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is deterministic, 0 otherwise", 0 },
    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is complete, 0 otherwise", 0 },
    { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
106
      "processing time (excluding parsing) in seconds", 0 },
107
108
    { "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the output automaton", 0 },
109
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp aoutput_io_format_argp = { io_options, 0, 0, 0, 0, 0, 0 };

static const argp_option o_options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
      "the following interpreted sequences:", 4 },
    { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
    { "%m", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "name of the automaton", 0 },
    { "%s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of states", 0 },
    { "%e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of edges", 0 },
    { "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 },
    { "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
127
128
      "number of acceptance sets", 0 },
    { "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 },
129
130
131
132
133
134
135
    { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of nondeterministic states in output", 0 },
    { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is deterministic, 0 otherwise", 0 },
    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is complete, 0 otherwise", 0 },
    { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
136
      "processing time (excluding parsing) in seconds", 0 },
137
138
    { "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the output automaton", 0 },
139
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 },
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp aoutput_o_format_argp = { o_options, 0, 0, 0, 0, 0, 0 };

int parse_opt_aoutput(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
    case 'H':
      automaton_format = Hoa;
      hoa_opt = arg;
      break;
    case 'q':
      automaton_format = Quiet;
      break;
    case 's':
      automaton_format = Spin;
      if (type != spot::postprocessor::Monitor)
	type = spot::postprocessor::BA;
      break;
    case OPT_DOT:
      automaton_format = Dot;
      opt_dot = arg;
      break;
    case OPT_LBTT:
      if (arg)
	{
	  if (arg[0] == 't' && arg[1] == 0)
	    automaton_format = Lbtt_t;
	  else
	    error(2, 0, "unknown argument for --lbtt: '%s'", arg);
	}
      else
	{
	  automaton_format = Lbtt;
	}
      break;
    case OPT_NAME:
183
      opt_name = arg;
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
      break;
    case OPT_SPOT:
      automaton_format = Spot;
      break;
    case OPT_STATS:
      if (!*arg)
	error(2, 0, "empty format string for --stats");
      stats = arg;
      automaton_format = Stats;
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}



202
203
204
automaton_printer::automaton_printer(stat_style input)
  : statistics(std::cout, stats, input),
    namer(name, opt_name, input)
205
206
{
}
207
208
209

void
automaton_printer::print(const spot::tgba_digraph_ptr& aut,
210
			 const spot::ltl::formula* f,
211
212
			 // Input location for errors and statistics.
			 const char* filename,
213
			 int loc,
214
215
216
217
218
219
220
221
			 // Time and input automaton for statistics
			 double time,
			 const spot::const_hoa_aut_ptr& haut)
{
  // Name the output automaton.
  if (opt_name)
    {
      name.str("");
222
      namer.print(haut, aut, f, filename, loc, time);
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
      aut->set_named_prop("automaton-name", new std::string(name.str()));
    }

  // Output it.
  switch (automaton_format)
    {
    case Count:
    case Quiet:
      // Do not output anything.
      break;
    case Dot:
      spot::dotty_reachable(std::cout, aut,
			    (type == spot::postprocessor::BA)
			    || (type == spot::postprocessor::Monitor),
			    opt_dot);
      break;
    case Lbtt:
      spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
      break;
    case Lbtt_t:
      spot::lbtt_reachable(std::cout, aut, false);
      break;
    case Hoa:
      spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
      break;
    case Spot:
      spot::tgba_save_reachable(std::cout, aut);
      break;
    case Spin:
      spot::never_claim_reachable(std::cout, aut);
      break;
    case Stats:
255
      statistics.print(haut, aut, f, filename, loc, time) << '\n';
256
257
258
259
      break;
    }
  flush_cout();
}