common_output.cc 3.28 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
#include "common_sys.hh"
23
24
#include "common_output.hh"
#include <iostream>
25
#include "ltlvisit/tostring.hh"
26
#include "ltlvisit/lbt.hh"
27
#include "common_cout.hh"
28
#include "error.h"
29
30
31
32
33
34
35
36
37
38
39
40

#define OPT_SPOT 1

output_format_t output_format = spot_output;
bool full_parenth = false;

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 },
41
    { "lbt", 'l', 0, 0, "output in LBT's syntax", -20 },
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
    { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 },
    { 0, 0, 0, 0, 0, 0 }
  };

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

int
parse_opt_output(int key, char*, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      output_format = utf8_output;
      break;
57
58
59
    case 'l':
      output_format = lbt_output;
      break;
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
    case 'p':
      full_parenth = true;
      break;
    case 's':
      output_format = spin_output;
      break;
    case OPT_SPOT:
      output_format = spot_output;
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

75
static
76
void
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
report_not_ltl(const spot::ltl::formula* f,
	       const char* filename, int linenum, const char* syn)
{
  std::string s = spot::ltl::to_string(f);
  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);
}


void
output_formula(const spot::ltl::formula* f, const char* filename, int linenum)
92
93
94
{
  switch (output_format)
    {
95
96
97
98
99
100
    case lbt_output:
      if (f->is_ltl_formula())
	spot::ltl::to_lbt_string(f, std::cout);
      else
	report_not_ltl(f, filename, linenum, "LBT");
      break;
101
102
103
104
    case spot_output:
      spot::ltl::to_string(f, std::cout, full_parenth);
      break;
    case spin_output:
105
106
107
108
      if (f->is_ltl_formula())
	spot::ltl::to_spin_string(f, std::cout, full_parenth);
      else
	report_not_ltl(f, filename, linenum, "Spin");
109
110
111
112
113
      break;
    case utf8_output:
      spot::ltl::to_utf8_string(f, std::cout, full_parenth);
      break;
    }
114
115
116
117
  // Make sure we abort if we can't write to std::cout anymore
  // (like disk full or broken pipe with SIGPIPE ignored).
  std::cout << std::endl;
  check_cout();
118
}