common_aoutput.cc 8.63 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
51
52
53
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 },
    { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL,
      "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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
    { "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,
      "name of the automaton (as specified in the HOA format)", 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 },
    { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of transitions", 0 },
    { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of acceptance pairs or sets", 0 },
    { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs", 0 },
    { "%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,
109
      "processing time (excluding parsing) in seconds", 0 },
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
    { "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the output automaton", 0 },
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    { 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,
      "number of acceptance pairs or sets", 0 },
    { "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs", 0 },
    { "%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,
141
      "processing time (excluding parsing) in seconds", 0 },
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
183
184
185
186
187
188
    { "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the output automaton", 0 },
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    { 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:
189
      opt_name = arg;
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
      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;
}



208
209
210
automaton_printer::automaton_printer(stat_style input)
  : statistics(std::cout, stats, input),
    namer(name, opt_name, input)
211
212
{
}
213
214
215

void
automaton_printer::print(const spot::tgba_digraph_ptr& aut,
216
			 const spot::ltl::formula* f,
217
218
			 // Input location for errors and statistics.
			 const char* filename,
219
			 int loc,
220
221
222
223
224
225
226
227
			 // Time and input automaton for statistics
			 double time,
			 const spot::const_hoa_aut_ptr& haut)
{
  // Name the output automaton.
  if (opt_name)
    {
      name.str("");
228
      namer.print(haut, aut, f, filename, loc, time);
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
255
256
257
258
259
260
      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:
261
      statistics.print(haut, aut, f, filename, loc, time) << '\n';
262
263
264
265
      break;
    }
  flush_cout();
}