ltlsynt.cc 13.2 KB
Newer Older
Thibaud Michaud's avatar
Thibaud Michaud committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
// -*- coding: utf-8 -*-
// Copyright (C) 2017 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
// 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 39
#include <spot/misc/game.hh>
#include <spot/misc/minato.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
Maximilien Colange's avatar
Maximilien Colange committed
40
#include <spot/twaalgos/aiger.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
41 42 43 44 45 46 47 48 49 50
#include <spot/twaalgos/complete.hh>
#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>

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

static const argp_option options[] =
  {
61 62
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Input options:", 1 },
Maximilien Colange's avatar
Maximilien Colange committed
63
    { "ins", OPT_INPUT, "PROPS", 0,
64 65
      "comma-separated list of uncontrollable (a.k.a. input) atomic"
      " propositions", 0},
Maximilien Colange's avatar
Maximilien Colange committed
66
    { "outs", OPT_OUTPUT, "PROPS", 0,
67 68
      "comma-separated list of controllable (a.k.a. output) atomic"
      " propositions", 0},
69 70
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
71
    { "algo", OPT_ALGO, "qp|rec", 0,
72 73 74 75 76
      "choose the parity game algorithm, valid ones are rec (Zielonka's"
      " recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
      " time algorithm)", 0 },
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Output options:", 20 },
Thibaud Michaud's avatar
Thibaud Michaud committed
77 78
    { "print-pg", OPT_PRINT, nullptr, 0,
      "print the parity game in the pgsolver format, do not solve it", 0},
79
    { "realizability", OPT_REAL, nullptr, 0,
Maximilien Colange's avatar
Maximilien Colange committed
80 81 82
      "realizability only, do not compute a winning strategy", 0},
    { "aiger", OPT_PRINT_AIGER, nullptr, 0,
      "prints the winning strategy as an AIGER circuit", 0},
83 84
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Thibaud Michaud's avatar
Thibaud Michaud committed
85 86 87
    { nullptr, 0, nullptr, 0, nullptr, 0 },
  };

Maximilien Colange's avatar
Maximilien Colange committed
88
static const struct argp_child children[] =
Thibaud Michaud's avatar
Thibaud Michaud committed
89
  {
90
    { &finput_argp_headless, 0, nullptr, 0 },
Maximilien Colange's avatar
Maximilien Colange committed
91 92
    { &aoutput_argp, 0, nullptr, 0 },
    //{ &aoutput_o_format_argp, 0, nullptr, 0 },
93
    { &misc_argp, 0, nullptr, 0 },
Thibaud Michaud's avatar
Thibaud Michaud committed
94 95 96
    { nullptr, 0, nullptr, 0 }
  };

Maximilien Colange's avatar
Maximilien Colange committed
97 98 99 100 101 102
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
103

Maximilien Colange's avatar
Maximilien Colange committed
104 105
static std::vector<std::string> input_aps;
static std::vector<std::string> output_aps;
Thibaud Michaud's avatar
Thibaud Michaud committed
106

107 108
bool opt_print_pg(false);
bool opt_real(false);
Maximilien Colange's avatar
Maximilien Colange committed
109
bool opt_print_aiger(false);
110

Maximilien Colange's avatar
Maximilien Colange committed
111
// FIXME rename options to choose the algorithm
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
enum solver
{
  QP,
  REC
};

static char const *const solver_args[] =
{
  "qp", "quasi-polynomial",
  "recursive",
  nullptr
};
static solver const solver_types[] =
{
  QP, QP,
  REC,
};
ARGMATCH_VERIFY(solver_args, solver_types);

Maximilien Colange's avatar
Maximilien Colange committed
131
static solver opt_solver = REC;
Thibaud Michaud's avatar
Thibaud Michaud committed
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151

namespace
{
  // Take an automaton and a set of atomic propositions I, and split each
  // transition
  //
  //     p -- cond --> q                cond in 2^2^AP
  //
  // into a set of transitions of the form
  //
  //     p -- i1 --> r1 -- o1 --> q     i1 in 2^I
  //                                    o1 in 2^O
  //
  //     p -- i2 --> r2 -- o2 --> q     i2 in 2^I
  //                                    o2 in 2^O
  //     ...
  //
  // where O = AP\I, and such that cond = (i1 & o1) | (i2 & o2) | ...
  //
  // When determinized, this encodes a game automaton that has a winning
152
  // strategy iff aut has an accepting run for any valuation of atomic
Thibaud Michaud's avatar
Thibaud Michaud committed
153 154
  // propositions in I.

Maximilien Colange's avatar
Maximilien Colange committed
155
  static spot::twa_graph_ptr
Thibaud Michaud's avatar
Thibaud Michaud committed
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187
  split_automaton(const spot::twa_graph_ptr& aut,
                  bdd input_bdd)
  {
    auto tgba = spot::to_generalized_buchi(aut);
    auto split = spot::make_twa_graph(tgba->get_dict());
    split->copy_ap_of(tgba);
    split->copy_acceptance_of(tgba);
    split->new_states(tgba->num_states());
    split->set_init_state(tgba->get_init_state_number());

    for (unsigned src = 0; src < tgba->num_states(); ++src)
      for (const auto& e: tgba->out(src))
        {
          spot::minato_isop isop(e.cond);
          bdd cube;
          while ((cube = isop.next()) != bddfalse)
            {
              unsigned q = split->new_state();
              bdd in = bdd_existcomp(cube, input_bdd);
              bdd out = bdd_exist(cube, input_bdd);
              split->new_edge(src, q, in, 0);
              split->new_edge(q, e.dst, out, e.acc);
            }
        }
    split->prop_universal(spot::trival::maybe());
    return split;
  }

  // Generates a vector indicating the owner of each state, with the
  // convention that false is player 0 (the environment) and true is player 1
  // (the controller).  Starting with player 0 on the initial state, the owner
  // is switched after each transition.
Maximilien Colange's avatar
Maximilien Colange committed
188 189 190
  static std::vector<bool>
  make_alternating_owner(const spot::twa_graph_ptr& dpa,
                         bool init_owner = false)
Thibaud Michaud's avatar
Thibaud Michaud committed
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
  {
    std::vector<bool> seen(dpa->num_states(), false);
    std::vector<unsigned> todo({dpa->get_init_state_number()});
    std::vector<bool> owner(dpa->num_states());
    owner[dpa->get_init_state_number()] = init_owner;
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        seen[src] = true;
        for (auto& e: dpa->out(src))
          {
            if (!seen[e.dst])
              {
                owner[e.dst] = !owner[src];
                todo.push_back(e.dst);
              }
          }
      }
    return owner;
  }

Maximilien Colange's avatar
Maximilien Colange committed
213 214
  static spot::twa_graph_ptr
  to_dpa(const spot::twa_graph_ptr& split)
Thibaud Michaud's avatar
Thibaud Michaud committed
215 216 217 218 219 220 221 222 223 224 225 226 227
  {
    auto dpa = spot::tgba_determinize(split);
    dpa->merge_edges();
    spot::complete_here(dpa);
    spot::colorize_parity_here(dpa, true);
    spot::change_parity_here(dpa, spot::parity_kind_max,
                             spot::parity_style_odd);
    if (opt_print_pg)
      dpa = spot::sbacc(dpa);
    bool max, odd;
    dpa->acc().is_parity(max, odd);
    assert(max && odd);
    assert(spot::is_deterministic(dpa));
228 229 230 231 232 233
    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
234
  static spot::twa_graph_ptr
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
  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],
                                  (e1.cond & out), 0);
                    break;
                  }
                ++i;
              }
          }
      }
    aut->purge_dead_states();
Maximilien Colange's avatar
Maximilien Colange committed
275
    aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
276 277 278
    return aut;
  }

Thibaud Michaud's avatar
Thibaud Michaud committed
279 280 281

  class ltl_processor final : public job_processor
  {
282 283 284 285 286
  private:
    spot::translator& trans_;
    std::vector<std::string> input_aps_;
    std::vector<std::string> output_aps_;

Thibaud Michaud's avatar
Thibaud Michaud committed
287 288
  public:

289 290 291 292
    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
293 294 295 296 297 298
    {
    }

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

302 303 304 305 306 307 308 309 310 311 312 313
      auto aut = trans_.run(&f);
      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
314 315
        {
          std::ostringstream lowercase;
316
          for (char c: output_aps_[i])
Thibaud Michaud's avatar
Thibaud Michaud committed
317
            lowercase << (char)std::tolower(c);
318 319
          unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
          all_outputs &= bdd_ithvar(v);
Thibaud Michaud's avatar
Thibaud Michaud committed
320
        }
321 322 323 324
      auto split = split_automaton(aut, all_inputs);
      auto dpa = to_dpa(split);
      auto owner = make_alternating_owner(dpa);
      auto pg = spot::parity_game(dpa, owner);
Maximilien Colange's avatar
Maximilien Colange committed
325 326
      timer.stop();

Thibaud Michaud's avatar
Thibaud Michaud committed
327 328 329 330 331
      if (opt_print_pg)
        {
          pg.print(std::cout);
          return 0;
        }
332 333 334 335
      switch (opt_solver)
        {
          case REC:
            {
336 337 338 339 340 341 342 343
              spot::parity_game::strategy_t strategy;
              spot::parity_game::region_t winning_region;
              std::tie(winning_region, strategy) = pg.solve();
              if (winning_region.count(pg.get_init_state_number()))
                {
                  std::cout << "REALIZABLE\n";
                  if (!opt_real)
                    {
344 345
                      auto strat_aut =
                        strat_to_aut(pg, strategy, dpa, all_outputs);
Maximilien Colange's avatar
Maximilien Colange committed
346 347 348 349 350 351 352 353 354

                      // output the winning strategy
                      if (opt_print_aiger)
                        spot::print_aiger(std::cout, strat_aut);
                      else
                        {
                          automaton_printer printer;
                          printer.print(strat_aut, timer);
                        }
355
                    }
Maximilien Colange's avatar
Maximilien Colange committed
356
                  return 0;
357
                }
358
              else
Maximilien Colange's avatar
Maximilien Colange committed
359 360 361 362
                {
                  std::cout << "UNREALIZABLE\n";
                  return 1;
                }
363 364
            }
          case QP:
365 366 367 368
            if (!opt_real)
              {
                std::cout << "The quasi-polynomial time algorithm does not"
                  " implement synthesis yet, use --realizability\n";
Maximilien Colange's avatar
Maximilien Colange committed
369
                return 2;
370 371
              }
            else if (pg.solve_qp())
Maximilien Colange's avatar
Maximilien Colange committed
372 373 374 375
              {
                std::cout << "REALIZABLE\n";
                return 0;
              }
376
            else
Maximilien Colange's avatar
Maximilien Colange committed
377 378 379 380
              {
                std::cout << "UNREALIZABLE\n";
                return 1;
              }
381 382
          default:
            SPOT_UNREACHABLE();
Maximilien Colange's avatar
Maximilien Colange committed
383
            return 2;
384
        }
Thibaud Michaud's avatar
Thibaud Michaud committed
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
    }
  };
}

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;
      }
405 406 407 408 409 410 411 412 413 414 415
    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
416 417 418
    case OPT_PRINT:
      opt_print_pg = true;
      break;
419
    case OPT_ALGO:
420
      opt_solver = XARGMATCH("--algo", arg, solver_args, solver_types);
421
      break;
422 423 424
    case OPT_REAL:
      opt_real = true;
      break;
Maximilien Colange's avatar
Maximilien Colange committed
425 426 427
    case OPT_PRINT_AIGER:
      opt_print_aiger = true;
      break;
Thibaud Michaud's avatar
Thibaud Michaud committed
428 429 430 431
    }
  return 0;
}

Maximilien Colange's avatar
Maximilien Colange committed
432 433
int
main(int argc, char **argv)
Thibaud Michaud's avatar
Thibaud Michaud committed
434 435 436 437 438 439
{
  setup(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);
440 441
  check_no_formula();

Thibaud Michaud's avatar
Thibaud Michaud committed
442
  spot::translator trans;
443
  ltl_processor processor(trans, input_aps, output_aps);
Maximilien Colange's avatar
Maximilien Colange committed
444
  return processor.run();
Thibaud Michaud's avatar
Thibaud Michaud committed
445
}