ltl2tgta.cc 7.6 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013 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
36
37
38
39
40
41
42
43
44
#include "common_r.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "common_post.hh"

#include "ltlparse/public.hh"
#include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/postproc.hh"
#include "tgba/bddprint.hh"

#include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh"
#include "taalgos/minimize.hh"
45
#include "misc/optionmap.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46
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

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 },
82
83
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84
85
86
87
88
89
90
    { 0, 0, 0, 0, 0, 0 }
  };

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

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

bool utf8 = false;
const char* stats = "";
100
spot::option_map extra_options;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
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;
117
118
119
120
121
122
123
    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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
    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?
      jobs.push_back(job(arg, false));
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
159
  class trans_processor: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
160
161
162
163
164
165
166
167
168
169
170
171
  {
  public:
    spot::ltl::ltl_simplifier& simpl;
    spot::postprocessor& post;

    trans_processor(spot::ltl::ltl_simplifier& simpl,
		    spot::postprocessor& post)
      : simpl(simpl), post(post)
    {
    }

    int
172
    process_formula(const spot::ltl::formula* f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
173
174
175
176
177
178
179
180
181
		    const char* filename = 0, int linenum = 0)
    {
      const spot::ltl::formula* res = simpl.simplify(f);
      f->destroy();
      f = res;
      // This helps ltl_to_tgba_fm() to order BDD variables in a more
      // natural way (improving the degeneralization).
      simpl.clear_as_bdd_cache();

182
183
184
185
186
187
188
189
190
191
192
193
      // 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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
      bool exprop = level == spot::postprocessor::High;
      const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
      aut = post.run(aut, f);

      if (utf8)
	{
	  spot::tgba* a = const_cast<spot::tgba*>(aut);
	  if (spot::tgba_explicit_formula* tef =
	      dynamic_cast<spot::tgba_explicit_formula*>(a))
	    tef->enable_utf8();
	  else if (spot::sba_explicit_formula* sef =
		   dynamic_cast<spot::sba_explicit_formula*>(a))
	    sef->enable_utf8();
	}

      bdd ap_set = atomic_prop_collect_as_bdd(f, aut);

      if (ta_type != TGTA)
	{
213
214
215
216
217
	  spot::ta* testing_automaton =
	    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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
	  if (level != spot::postprocessor::Low)
	    {
	      spot::ta* testing_automaton_nm = testing_automaton;
	      testing_automaton = spot::minimize_ta(testing_automaton);
	      delete testing_automaton_nm;
	    }
	  spot::dotty_reachable(std::cout, testing_automaton);
	  delete testing_automaton;
	}
      else
	{
	  spot::tgta_explicit* tgta = tgba_to_tgta(aut, ap_set);
	  if (level != spot::postprocessor::Low)
	    {
	      spot::tgta_explicit* a = spot::minimize_tgta(tgta);
	      delete tgta;
	      tgta = a;
	    }
	  spot::dotty_reachable(std::cout,
				dynamic_cast<spot::tgta_explicit*>(tgta)
				->get_ta());
	  delete tgta;
	}

      delete aut;
243
      f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
244
245
246
247
248
249
250
251
252
      flush_cout();
      return 0;
    }
  };
}

int
main(int argc, char** argv)
{
253
  setup(argv);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
254
255
256
257

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

258
259
  simplification_level = 3;

260
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
261
262
263
264
265
266
    exit(err);

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

267
268
  spot::ltl::ltl_simplifier simpl(simplifier_options());

269
  spot::postprocessor postproc(&extra_options);
270
  postproc.set_pref(pref | comp);
271
272
273
274
275
276
277
  postproc.set_type(type);
  postproc.set_level(level);

  trans_processor processor(simpl, postproc);
  if (processor.run())
    return 2;
  return 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
278
}