common_finput.cc 3.63 KB
Newer Older
1
2
3
4
5
6
7
8
// -*- 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
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
21

#include "common_finput.hh"
#include "error.h"
22
23
24
#include "ltlparse/public.hh"

#include <fstream>
25
26

#define OPT_LBT 1
27
#define OPT_LENIENT 2
28
29
30

jobs_t jobs;
bool lbt_input = false;
31
static bool lenient = false;
32
33
34
35
36
37
38
39
40

static const argp_option options[] =
  {
    { 0, 0, 0, 0, "Input options:", 1 },
    { "formula", 'f', "STRING", 0, "process the formula STRING", 0 },
    { "file", 'F', "FILENAME", 0,
      "process each line of FILENAME as a formula", 0 },
    { "lbt-input", OPT_LBT, 0, 0,
      "read all formulas using LBT's prefix syntax", 0 },
41
42
43
    { "lenient", OPT_LENIENT, 0, 0,
      "parenthesized blocks that cannot be parsed as subformulas "
      "are considered as atomic properties", 0 },
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp finput_argp = { options, parse_opt_finput, 0, 0, 0, 0, 0 };

int
parse_opt_finput(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case 'f':
      jobs.push_back(job(arg, false));
      break;
    case 'F':
      jobs.push_back(job(arg, true));
      break;
    case OPT_LBT:
      lbt_input = true;
      break;
64
65
66
    case OPT_LENIENT:
      lenient = true;
      break;
67
68
69
70
71
72
73
74
75
76
77
78
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

const spot::ltl::formula*
parse_formula(const std::string& s, spot::ltl::parse_error_list& pel)
{
  if (lbt_input)
    return spot::ltl::parse_lbt(s, pel);
  else
79
80
81
    return spot::ltl::parse(s, pel,
			    spot::ltl::default_environment::instance(),
			    false, lenient);
82
}
83

84
85
86
87
job_processor::job_processor()
  : abort_run(false)
{
}
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

int
job_processor::process_string(const std::string& input,
			      const char* filename,
			      int linenum)
{
  spot::ltl::parse_error_list pel;
  const spot::ltl::formula* f = parse_formula(input, pel);

  if (!f || pel.size() > 0)
    {
      if (filename)
	error_at_line(0, 0, filename, linenum, "parse error:");
      spot::ltl::format_parse_errors(std::cerr, input, pel);
      if (f)
	f->destroy();
      return 1;
    }
  return process_formula(f, filename, linenum);
}

int
job_processor::process_stream(std::istream& is,
			      const char* filename)
{
  int error = 0;
  int linenum = 0;
  std::string line;
116
  while (!abort_run && std::getline(is, line))
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
    error |= process_string(line, filename, ++linenum);
  return error;
}

int
job_processor::process_file(const char* filename)
{
  // Special case for stdin.
  if (filename[0] == '-' && filename[1] == 0)
    return process_stream(std::cin, filename);

  errno = 0;
  std::ifstream input(filename);
  if (!input)
    error(2, errno, "cannot open '%s'", filename);
  return process_stream(input, filename);
}

int
job_processor::run()
{
  int error = 0;
  jobs_t::const_iterator i;
140
  for (i = jobs.begin(); i != jobs.end() && !abort_run; ++i)
141
142
143
144
145
146
147
148
    {
      if (!i->file_p)
	error |= process_string(i->str);
      else
	error |= process_file(i->str);
    }
  return error;
}