ltl2tgta.cc 7.23 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
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
45
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
82
83
84
85
86
87
#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"

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 },
    { 0, 0, 0, 0, 0, 0 }
  };

const struct argp_child children[] =
  {
    { &finput_argp, 0, 0, 1 },
    { &post_argp, 0, 0, 20 },
88
    { &misc_argp, 0, 0, -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
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
141
142
143
144
145
146
147
    { 0, 0, 0, 0 }
  };

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

bool utf8 = false;
const char* stats = "";
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;
    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
{
148
  class trans_processor: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
149
150
151
152
153
154
155
156
157
158
159
160
  {
  public:
    spot::ltl::ltl_simplifier& simpl;
    spot::postprocessor& post;

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

    int
161
    process_formula(const spot::ltl::formula* f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
162
163
164
165
166
167
168
169
170
		    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();

171
172
173
174
175
176
177
178
179
180
181
182
      // 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
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
      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)
	{
202
203
204
205
206
	  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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
	  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;
232
      f->destroy();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
234
235
236
237
238
239
240
241
      flush_cout();
      return 0;
    }
  };
}

int
main(int argc, char** argv)
{
242
  setup(argv);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
243
244
245
246

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

247
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
248
249
250
251
252
253
    exit(err);

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

254
255
256
257
258
259
260
261
262
263
264
  spot::ltl::ltl_simplifier simpl(simplifier_options());

  spot::postprocessor postproc;
  postproc.set_pref(pref);
  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
265
}