ltl2tgta.cc 6.47 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
19
20
21
22
23
24
25
26
27
28

#include "common_sys.hh"

#include <string>
#include <iostream>
#include <fstream>

#include <argp.h>
#include "error.h"

29
#include "common_setup.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
31
32
33
34
35
#include "common_r.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "common_post.hh"

#include "ltlparse/public.hh"
36
#include "ltlvisit/tostring.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
38
39
#include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
40
#include "tgbaalgos/translate.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
41
42
43
44
45
#include "tgba/bddprint.hh"

#include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh"
#include "taalgos/minimize.hh"
46
#include "misc/optionmap.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

const char argp_program_doc[] ="\
Translate linear-time formulas (LTL/PSL) into Testing Automata.\n\n\
By default it outputs a transition-based generalized Testing Automaton \
the smallest Transition-based Generalized Büchi Automata, \
in GraphViz's format.  The input formula is assumed to be \
stuttering-insensitive.";

#define OPT_TGTA 1
#define OPT_TA 2
#define OPT_GTA 3
#define OPT_SPLV 4
#define OPT_SPNO 5
#define OPT_INIT 6

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Automaton type:", 1 },
    { "tgta", OPT_TGTA, 0, 0,
      "Transition-based Generalized Testing Automaton (default)", 0 },
    { "ta", OPT_TA, 0, 0, "Testing Automaton", 0 },
    { "gta", OPT_GTA, 0, 0, "Generalized Testing Automaton", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Options for TA and GTA creation:", 3 },
    { "single-pass-lv", OPT_SPLV, 0, 0,
      "add an artificial livelock state to obtain a single-pass (G)TA", 0 },
    { "single-pass", OPT_SPNO, 0, 0,
      "create a single-pass (G)TA without artificial livelock state", 0 },
    { "multiple-init", OPT_INIT, 0, 0,
      "do not create the fake initial state", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Output options:", 4 },
    { "utf8", '8', 0, 0, "enable UTF-8 characters in output", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
83
84
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
85
86
87
88
89
90
91
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
    { &post_argp, 0, 0, 20 },
92
    { &misc_argp, 0, 0, -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
93
94
95
96
97
98
99
100
    { 0, 0, 0, 0 }
  };

enum ta_types { TGTA, GTA, TA };
ta_types ta_type = TGTA;

bool utf8 = false;
const char* stats = "";
101
spot::option_map extra_options;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
bool opt_with_artificial_initial_state = true;
bool opt_single_pass_emptiness_check = false;
bool opt_with_artificial_livelock = false;

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
    case 'B':
      type = spot::postprocessor::BA;
      break;
118
119
120
121
122
123
124
    case 'x':
      {
	const char* opt = extra_options.parse_options(arg);
	if (opt)
	  error(2, 0, "failed to parse --options near '%s'", opt);
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
    case OPT_TGTA:
      ta_type = TGTA;
      type = spot::postprocessor::TGBA;
      break;
    case OPT_GTA:
      ta_type = GTA;
      type = spot::postprocessor::TGBA;
      break;
    case OPT_TA:
      ta_type = TA;
      type = spot::postprocessor::BA;
      break;
    case OPT_INIT:
      opt_with_artificial_initial_state = false;
      break;
    case OPT_SPLV:
      opt_with_artificial_livelock = true;
      break;
    case OPT_SPNO:
      opt_single_pass_emptiness_check = true;
      break;
    case ARGP_KEY_ARG:
      // FIXME: use stat() to distinguish filename from string?
148
      jobs.emplace_back(arg, false);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
149
150
151
152
153
154
155
156
157
158
159
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
160
  class trans_processor: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
161
162
  {
  public:
163
    spot::translator& trans;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
164

165
166
    trans_processor(spot::translator& trans)
      : trans(trans)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
167
168
169
170
    {
    }

    int
171
    process_formula(const spot::ltl::formula* f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
172
173
		    const char* filename = 0, int linenum = 0)
    {
174
      auto aut = trans.run(&f);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
175

176
177
178
179
180
181
182
183
184
185
186
187
      // This should not happen, because the parser we use can only
      // read PSL/LTL formula, but since our ltl::formula* type can
      // represent more than PSL formula, let's make this
      // future-proof.
      if (!f->is_psl_formula())
	{
	  std::string s = spot::ltl::to_string(f);
	  error_at_line(2, 0, filename, linenum,
			"formula '%s' is not an LTL or PSL formula",
			s.c_str());
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
188
189
190
191
      bdd ap_set = atomic_prop_collect_as_bdd(f, aut);

      if (ta_type != TGTA)
	{
192
	  auto testing_automaton =
193
194
195
196
	    tgba_to_ta(aut, ap_set, type == spot::postprocessor::BA,
		       opt_with_artificial_initial_state,
		       opt_single_pass_emptiness_check,
		       opt_with_artificial_livelock);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
197
	  if (level != spot::postprocessor::Low)
198
	    testing_automaton = spot::minimize_ta(testing_automaton);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
199
200
201
202
	  spot::dotty_reachable(std::cout, testing_automaton);
	}
      else
	{
203
	  auto tgta = tgba_to_tgta(aut, ap_set);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
204
	  if (level != spot::postprocessor::Low)
205
206
	    tgta = spot::minimize_tgta(tgta);
	  spot::dotty_reachable(std::cout, tgta->get_ta());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
207
	}
208
      f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
209
210
211
212
213
214
215
216
217
      flush_cout();
      return 0;
    }
  };
}

int
main(int argc, char** argv)
{
218
  setup(argv);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
219
220
221
222

  const argp ap = { options, parse_opt, "[FORMULA...]",
		    argp_program_doc, children, 0, 0 };

223
224
  simplification_level = 3;

225
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
226
227
228
229
230
231
    exit(err);

  if (jobs.empty())
    error(2, 0, "No formula to translate?  Run '%s --help' for usage.",
	  program_name);

232
233
234
235
  spot::translator trans(&extra_options);
  trans.set_pref(pref | comp);
  trans.set_type(type);
  trans.set_level(level);
236

237
  trans_processor processor(trans);
238
239
240
  if (processor.run())
    return 2;
  return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
241
}