ltlsynt.cc 14.4 KB
Newer Older
Thibaud Michaud's avatar
Thibaud Michaud committed
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
Thibaud Michaud's avatar
Thibaud Michaud committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

20
21
#include <config.h>

Thibaud Michaud's avatar
Thibaud Michaud committed
22
#include <memory>
23
24
25
#include <string>
#include <sstream>
#include <unordered_map>
Thibaud Michaud's avatar
Thibaud Michaud committed
26
27
#include <vector>

28
29
#include "argmatch.h"

Thibaud Michaud's avatar
Thibaud Michaud committed
30
31
32
33
34
#include "common_aoutput.hh"
#include "common_finput.hh"
#include "common_setup.hh"
#include "common_sys.hh"

35
#include <spot/misc/bddlt.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
36
37
38
#include <spot/misc/game.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
Maximilien Colange's avatar
Maximilien Colange committed
39
#include <spot/twaalgos/aiger.hh>
40
#include <spot/twaalgos/degen.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
41
42
43
44
45
46
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/parity.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twa/twagraph.hh>
47
48
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/split.hh>
49
#include <spot/twaalgos/toparity.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
50
51
52

enum
{
53
54
55
  OPT_ALGO = 256,
  OPT_INPUT,
  OPT_OUTPUT,
56
  OPT_PRINT,
Maximilien Colange's avatar
Maximilien Colange committed
57
  OPT_PRINT_AIGER,
58
59
  OPT_REAL,
  OPT_VERBOSE
Thibaud Michaud's avatar
Thibaud Michaud committed
60
61
62
63
};

static const argp_option options[] =
  {
64
65
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Input options:", 1 },
Maximilien Colange's avatar
Maximilien Colange committed
66
    { "ins", OPT_INPUT, "PROPS", 0,
67
68
      "comma-separated list of uncontrollable (a.k.a. input) atomic"
      " propositions", 0},
Maximilien Colange's avatar
Maximilien Colange committed
69
    { "outs", OPT_OUTPUT, "PROPS", 0,
70
71
      "comma-separated list of controllable (a.k.a. output) atomic"
      " propositions", 0},
72
73
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
    { "algo", OPT_ALGO, "ds|sd|large", 0,
75
      "choose the algorithm for synthesis:\n"
76
77
78
      " - sd:   split then determinize with Safra (default)\n"
      " - ds:   determinize (Safra) then split\n"
      " - lar:  translate to a deterministic automaton with arbitrary"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
79
80
      " acceptance condition, then use LAR to turn to parity,"
      " then split", 0 },
81
82
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Output options:", 20 },
Thibaud Michaud's avatar
Thibaud Michaud committed
83
84
    { "print-pg", OPT_PRINT, nullptr, 0,
      "print the parity game in the pgsolver format, do not solve it", 0},
85
    { "realizability", OPT_REAL, nullptr, 0,
Maximilien Colange's avatar
Maximilien Colange committed
86
87
88
      "realizability only, do not compute a winning strategy", 0},
    { "aiger", OPT_PRINT_AIGER, nullptr, 0,
      "prints the winning strategy as an AIGER circuit", 0},
89
90
    { "verbose", OPT_VERBOSE, nullptr, 0,
      "verbose mode", -1 },
91
92
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Thibaud Michaud's avatar
Thibaud Michaud committed
93
94
95
    { nullptr, 0, nullptr, 0, nullptr, 0 },
  };

Maximilien Colange's avatar
Maximilien Colange committed
96
static const struct argp_child children[] =
Thibaud Michaud's avatar
Thibaud Michaud committed
97
  {
98
    { &finput_argp_headless, 0, nullptr, 0 },
Maximilien Colange's avatar
Maximilien Colange committed
99
100
    { &aoutput_argp, 0, nullptr, 0 },
    //{ &aoutput_o_format_argp, 0, nullptr, 0 },
101
    { &misc_argp, 0, nullptr, 0 },
Thibaud Michaud's avatar
Thibaud Michaud committed
102
103
104
    { nullptr, 0, nullptr, 0 }
  };

Maximilien Colange's avatar
Maximilien Colange committed
105
106
107
108
109
110
const char argp_program_doc[] = "\
Synthesize a controller from its LTL specification.\v\
Exit status:\n\
  0   if the input problem is realizable\n\
  1   if the input problem is not realizable\n\
  2   if any error has been reported";
Thibaud Michaud's avatar
Thibaud Michaud committed
111

Maximilien Colange's avatar
Maximilien Colange committed
112
113
static std::vector<std::string> input_aps;
static std::vector<std::string> output_aps;
Thibaud Michaud's avatar
Thibaud Michaud committed
114

115
116
bool opt_print_pg(false);
bool opt_real(false);
Maximilien Colange's avatar
Maximilien Colange committed
117
bool opt_print_aiger(false);
118
119
120

enum solver
{
121
  DET_SPLIT,
122
123
  SPLIT_DET,
  LAR,
124
125
126
127
};

static char const *const solver_args[] =
{
128
129
  "detsplit", "ds",
  "splitdet", "sd",
130
  "lar",
131
132
133
134
  nullptr
};
static solver const solver_types[] =
{
135
  DET_SPLIT, DET_SPLIT,
136
137
  SPLIT_DET, SPLIT_DET,
  LAR,
138
139
140
};
ARGMATCH_VERIFY(solver_args, solver_types);

141
static solver opt_solver = SPLIT_DET;
142
static bool verbose = false;
Thibaud Michaud's avatar
Thibaud Michaud committed
143
144
145
146

namespace
{

147
148
149
  // Ensures that the game is complete for player 0.
  // Also computes the owner of each state (false for player 0, i.e. env).
  // Initial state belongs to Player 0 and the game is turn-based.
Maximilien Colange's avatar
Maximilien Colange committed
150
  static std::vector<bool>
151
  complete_env(spot::twa_graph_ptr& arena)
Thibaud Michaud's avatar
Thibaud Michaud committed
152
  {
153
154
155
156
157
158
159
160
161
162
163
164
165
166
    unsigned sink_env = arena->new_state();
    unsigned sink_con = arena->new_state();

    auto um = arena->acc().unsat_mark();
    if (!um.first)
      throw std::runtime_error("game winning condition is a tautology");
    arena->new_edge(sink_con, sink_env, bddtrue, um.second);
    arena->new_edge(sink_env, sink_con, bddtrue, um.second);

    std::vector<bool> seen(arena->num_states(), false);
    std::vector<unsigned> todo({arena->get_init_state_number()});
    std::vector<bool> owner(arena->num_states(), false);
    owner[arena->get_init_state_number()] = false;
    owner[sink_env] = true;
Thibaud Michaud's avatar
Thibaud Michaud committed
167
168
169
170
171
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        seen[src] = true;
172
173
        bdd missing = bddtrue;
        for (const auto& e: arena->out(src))
Thibaud Michaud's avatar
Thibaud Michaud committed
174
          {
175
176
177
            if (!owner[src])
              missing -= e.cond;

Thibaud Michaud's avatar
Thibaud Michaud committed
178
179
180
181
182
183
            if (!seen[e.dst])
              {
                owner[e.dst] = !owner[src];
                todo.push_back(e.dst);
              }
          }
184
185
        if (!owner[src] && missing != bddfalse)
          arena->new_edge(src, sink_con, missing, um.second);
Thibaud Michaud's avatar
Thibaud Michaud committed
186
      }
187

Thibaud Michaud's avatar
Thibaud Michaud committed
188
189
190
    return owner;
  }

Maximilien Colange's avatar
Maximilien Colange committed
191
192
  static spot::twa_graph_ptr
  to_dpa(const spot::twa_graph_ptr& split)
Thibaud Michaud's avatar
Thibaud Michaud committed
193
  {
194
195
    // if the input automaton is deterministic, degeneralize it to be sure to
    // end up with a parity automaton
196
197
    auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split),
                                      false, true, true, false);
Thibaud Michaud's avatar
Thibaud Michaud committed
198
    dpa->merge_edges();
199
200
    if (opt_print_pg)
      dpa = spot::sbacc(dpa);
Thibaud Michaud's avatar
Thibaud Michaud committed
201
202
203
    spot::colorize_parity_here(dpa, true);
    spot::change_parity_here(dpa, spot::parity_kind_max,
                             spot::parity_style_odd);
204
205
206
207
208
209
210
    assert((
      [&dpa]() -> bool
        {
          bool max, odd;
          dpa->acc().is_parity(max, odd);
          return max && odd;
        }()));
Thibaud Michaud's avatar
Thibaud Michaud committed
211
    assert(spot::is_deterministic(dpa));
212
213
214
215
216
217
    return dpa;
  }

  // Construct a smaller automaton, filtering out states that are not
  // accessible.  Also merge back pairs of p --(i)--> q --(o)--> r
  // transitions to p --(i&o)--> r.
Maximilien Colange's avatar
Maximilien Colange committed
218
  static spot::twa_graph_ptr
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
  strat_to_aut(const spot::parity_game& pg,
               const spot::parity_game::strategy_t& strat,
               const spot::twa_graph_ptr& dpa,
               bdd all_outputs)
  {
    auto aut = spot::make_twa_graph(dpa->get_dict());
    aut->copy_ap_of(dpa);
    std::vector<unsigned> todo{pg.get_init_state_number()};
    std::vector<int> pg2aut(pg.num_states(), -1);
    aut->set_init_state(aut->new_state());
    pg2aut[pg.get_init_state_number()] = aut->get_init_state_number();
    while (!todo.empty())
      {
        unsigned s = todo.back();
        todo.pop_back();
        for (auto& e1: dpa->out(s))
          {
            unsigned i = 0;
            for (auto& e2: dpa->out(e1.dst))
              {
                bool self_loop = false;
                if (e1.dst == s || e2.dst == e1.dst)
                  self_loop = true;
                if (self_loop || strat.at(e1.dst) == i)
                  {
                    bdd out = bdd_satoneset(e2.cond, all_outputs, bddfalse);
                    if (pg2aut[e2.dst] == -1)
                      {
                        pg2aut[e2.dst] = aut->new_state();
                        todo.push_back(e2.dst);
                      }
                    aut->new_edge(pg2aut[s], pg2aut[e2.dst],
251
                                  (e1.cond & out), {});
252
253
254
255
256
257
258
                    break;
                  }
                ++i;
              }
          }
      }
    aut->purge_dead_states();
Maximilien Colange's avatar
Maximilien Colange committed
259
    aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
260
261
262
    return aut;
  }

Thibaud Michaud's avatar
Thibaud Michaud committed
263
264
  class ltl_processor final : public job_processor
  {
265
266
267
268
269
  private:
    spot::translator& trans_;
    std::vector<std::string> input_aps_;
    std::vector<std::string> output_aps_;

Thibaud Michaud's avatar
Thibaud Michaud committed
270
271
  public:

272
273
274
275
    ltl_processor(spot::translator& trans,
                  std::vector<std::string> input_aps_,
                  std::vector<std::string> output_aps_)
      : trans_(trans), input_aps_(input_aps_), output_aps_(output_aps_)
Thibaud Michaud's avatar
Thibaud Michaud committed
276
277
278
279
280
281
    {
    }

    int process_formula(spot::formula f,
                        const char*, int) override
    {
Maximilien Colange's avatar
Maximilien Colange committed
282
283
284
      spot::process_timer timer;
      timer.start();

285
286
287
288
289
290
      if (opt_solver == LAR)
        {
          trans_.set_type(spot::postprocessor::Generic);
          trans_.set_pref(spot::postprocessor::Deterministic);
        }

291
      auto aut = trans_.run(&f);
292
293
      if (verbose)
        std::cerr << "translating formula done" << std::endl;
294
295
296
297
298
299
300
301
302
303
304
      bdd all_inputs = bddtrue;
      bdd all_outputs = bddtrue;
      for (unsigned i = 0; i < input_aps_.size(); ++i)
        {
          std::ostringstream lowercase;
          for (char c: input_aps_[i])
            lowercase << (char)std::tolower(c);
          unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
          all_inputs &= bdd_ithvar(v);
        }
      for (unsigned i = 0; i < output_aps_.size(); ++i)
Thibaud Michaud's avatar
Thibaud Michaud committed
305
306
        {
          std::ostringstream lowercase;
307
          for (char c: output_aps_[i])
Thibaud Michaud's avatar
Thibaud Michaud committed
308
            lowercase << (char)std::tolower(c);
309
310
          unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
          all_outputs &= bdd_ithvar(v);
Thibaud Michaud's avatar
Thibaud Michaud committed
311
        }
312

313
      spot::twa_graph_ptr dpa = nullptr;
314
      switch (opt_solver)
315
        {
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
          case DET_SPLIT:
            {
              auto tmp = to_dpa(aut);
              if (verbose)
                std::cerr << "determinization done\n"
                  << "dpa has " << tmp->num_states() << " states" << std::endl;
              tmp->merge_states();
              if (verbose)
                std::cerr << "simulation done\n"
                  << "dpa has " << tmp->num_states() << " states" << std::endl;
              dpa = split_2step(tmp, all_inputs);
              if (verbose)
                std::cerr << "split inputs and outputs done\n"
                  << "automaton has " << dpa->num_states() << " states"
                  << std::endl;
              spot::colorize_parity_here(dpa, true);
              break;
            }
          case SPLIT_DET:
            {
              auto split = split_2step(aut, all_inputs);
              if (verbose)
                std::cerr << "split inputs and outputs done\n"
                  << "automaton has " << split->num_states() << " states"
                  << std::endl;
              dpa = to_dpa(split);
              if (verbose)
                std::cerr << "determinization done\n"
                  << "dpa has " << dpa->num_states() << " states" << std::endl;
              dpa->merge_states();
              if (verbose)
                std::cerr << "simulation done\n"
                  << "dpa has " << dpa->num_states() << " states" << std::endl;
              break;
            }
          case LAR:
            {
              dpa = split_2step(aut, all_inputs);
              dpa->merge_states();
              if (verbose)
                std::cerr << "split inputs and outputs done\n"
                  << "automaton has " << dpa->num_states() << " states"
                  << std::endl;
              dpa = spot::to_parity(dpa);
              spot::cleanup_parity_here(dpa);
              spot::change_parity_here(dpa, spot::parity_kind_max,
                                       spot::parity_style_odd);
              if (verbose)
                std::cerr << "LAR construction done\n"
                  << "dpa has " << dpa->num_states() << " states" << std::endl;
              spot::colorize_parity_here(dpa, true);
              break;
            }
369
        }
370
      auto owner = complete_env(dpa);
371
      auto pg = spot::parity_game(dpa, owner);
372
373
      if (verbose)
        std::cerr << "parity game built" << std::endl;
Maximilien Colange's avatar
Maximilien Colange committed
374
375
      timer.stop();

Thibaud Michaud's avatar
Thibaud Michaud committed
376
377
378
379
380
      if (opt_print_pg)
        {
          pg.print(std::cout);
          return 0;
        }
381
382
383
384
385

      spot::parity_game::strategy_t strategy[2];
      spot::parity_game::region_t winning_region[2];
      pg.solve(winning_region, strategy);
      if (winning_region[1].count(pg.get_init_state_number()))
386
        {
387
388
          std::cout << "REALIZABLE\n";
          if (!opt_real)
389
            {
390
391
392
393
394
395
              auto strat_aut =
                strat_to_aut(pg, strategy[1], dpa, all_outputs);

              // output the winning strategy
              if (opt_print_aiger)
                spot::print_aiger(std::cout, strat_aut);
396
              else
Maximilien Colange's avatar
Maximilien Colange committed
397
                {
398
399
                  automaton_printer printer;
                  printer.print(strat_aut, timer);
Maximilien Colange's avatar
Maximilien Colange committed
400
                }
401
            }
402
403
404
405
406
407
          return 0;
        }
      else
        {
          std::cout << "UNREALIZABLE\n";
          return 1;
408
        }
Thibaud Michaud's avatar
Thibaud Michaud committed
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
    }
  };
}

static int
parse_opt(int key, char* arg, struct argp_state*)
{
  switch (key)
    {
    case OPT_INPUT:
      {
        std::istringstream aps(arg);
        std::string ap;
        while (std::getline(aps, ap, ','))
          {
            ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
            input_aps.push_back(ap);
          }
        break;
      }
429
430
431
432
433
434
435
436
437
438
439
    case OPT_OUTPUT:
      {
        std::istringstream aps(arg);
        std::string ap;
        while (std::getline(aps, ap, ','))
          {
            ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
            output_aps.push_back(ap);
          }
        break;
      }
Thibaud Michaud's avatar
Thibaud Michaud committed
440
441
442
    case OPT_PRINT:
      opt_print_pg = true;
      break;
443
    case OPT_ALGO:
444
      opt_solver = XARGMATCH("--algo", arg, solver_args, solver_types);
445
      break;
446
447
448
    case OPT_REAL:
      opt_real = true;
      break;
Maximilien Colange's avatar
Maximilien Colange committed
449
450
451
    case OPT_PRINT_AIGER:
      opt_print_aiger = true;
      break;
452
453
454
    case OPT_VERBOSE:
      verbose = true;
      break;
Thibaud Michaud's avatar
Thibaud Michaud committed
455
456
457
458
    }
  return 0;
}

Maximilien Colange's avatar
Maximilien Colange committed
459
460
int
main(int argc, char **argv)
Thibaud Michaud's avatar
Thibaud Michaud committed
461
{
462
463
464
465
466
467
468
469
470
471
472
  return protected_main(argv, [&] {
      const argp ap = { options, parse_opt, nullptr,
                        argp_program_doc, children, nullptr, nullptr };
      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
        exit(err);
      check_no_formula();

      spot::translator trans;
      ltl_processor processor(trans, input_aps, output_aps);
      return processor.run();
    });
Thibaud Michaud's avatar
Thibaud Michaud committed
473
}