safra.cc 18.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et
// Développement de l'Epita.
//
// 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
#include <algorithm>
21
#include <deque>
22
#include <stack>
23 24
#include <utility>
#include <unordered_map>
25 26

#include "safra.hh"
27 28 29 30
#include "spot/twaalgos/degen.hh"
#include "spot/twaalgos/sccfilter.hh"
#include "spot/twaalgos/simulation.hh"
#include "spot/twaalgos/complete.hh"
31 32 33

namespace spot
{
34 35
  namespace
  {
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
    using power_set = std::map<safra_state, int>;
    const char* const sub[10] =
    {
      "\u2080",
      "\u2081",
      "\u2082",
      "\u2083",
      "\u2084",
      "\u2085",
      "\u2086",
      "\u2087",
      "\u2088",
      "\u2089",
    };

    std::string subscript(unsigned start)
    {
      std::string res;
      do
        {
          res = sub[start % 10] + res;
          start /= 10;
        }
      while (start);
      return res;
    }

63 64 65 66 67 68 69 70 71
    // Returns true if lhs has a smaller nesting pattern than rhs
    // If lhs and rhs are the same, return false.
    bool nesting_cmp(const std::vector<node_helper::brace_t>& lhs,
                     const std::vector<node_helper::brace_t>& rhs)
    {
      size_t m = std::min(lhs.size(), rhs.size());
      size_t i = 0;
      for (; i < m; ++i)
        {
72 73
          if (lhs[i] != rhs[i])
            return lhs[i] < rhs[i];
74 75 76 77
        }
      return lhs.size() > rhs.size();
    }

78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
  // Used to remove all acceptance whos value is above and equal max_acc
  void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
  {
    assert(max_acc < 32);
    unsigned mask = (1 << max_acc) - 1;
    for (auto& t: aut->edges())
      {
        t.acc &= mask;
      }
  }

  struct compare
  {
    bool
    operator() (const safra_state::safra_node_t& lhs,
                const safra_state::safra_node_t& rhs)
94
    {
95
      return lhs.second < rhs.second;
96
    }
97
  };
98

99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
  // Return the sorteds nodes in ascending order
  std::vector<safra_state::safra_node_t>
  sorted_nodes(const safra_state::nodes_t& nodes)
  {
    std::vector<safra_state::safra_node_t> res;
    for (auto& n: nodes)
      res.emplace_back(n.first, n.second);
    std::sort(res.begin(), res.end(), compare());
    return res;
  }

  std::string
  nodes_to_string(const safra_state::nodes_t& states)
  {
    auto copy = sorted_nodes(states);
    std::ostringstream os;
    std::stack<unsigned> s;
    bool first = true;
    for (auto& n: copy)
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 148 149 150
        auto it = n.second.begin();
        // Find brace on top of stack in vector
        // If brace is not present, then we close it as no other ones of that
        // type will be found since we ordered our vector
        while (!s.empty())
          {
            it = std::lower_bound(n.second.begin(), n.second.end(),
                                       s.top());
            if (it == n.second.end() || *it != s.top())
              {
                os << subscript(s.top()) << '}';
                s.pop();
              }
            else
              {
                if (*it == s.top())
                  ++it;
                break;
              }
          }
        // Add new braces
        while (it != n.second.end())
          {
            os << '{' << subscript(*it);
            s.push(*it);
            ++it;
            first = true;
          }
        if (!first)
          os << ' ';
        os << n.first;
        first = false;
151
      }
152 153 154 155 156 157 158 159
    // Finish unwinding stack to print last braces
    while (!s.empty())
      {
        os << subscript(s.top()) << '}';
        s.pop();
      }
    return os.str();
  }
160

161 162 163 164 165 166 167 168 169 170 171
  std::vector<std::string>*
  print_debug(std::map<safra_state, int>& states)
  {
    auto res = new std::vector<std::string>(states.size());
    for (auto& p: states)
      (*res)[p.second] = nodes_to_string(p.first.nodes_);
    return res;
  }

}

172 173
std::vector<bool> find_scc_paths(const scc_info& scc);

174 175 176 177
unsigned
safra_state::find_scc_brace_id(unsigned scc_id, const scc_info& scc)
{
  for (auto& n: nodes_)
178
    {
179 180
      if (scc_id == scc.scc_of(n.first))
        return n.second.front();
181
    }
182 183
  return -1U;
}
184

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 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 232 233
safra_state
safra_state::compute_succ(const const_twa_graph_ptr& aut,
                          const bdd& ap,
                          const scc_info& scc,
                          const std::map<int, bdd>& implications,
                          const std::vector<bool>& is_connected,
                          bool scc_opt,
                          bool use_bisimulation) const
{
  safra_state ss = safra_state(nb_braces_.size());
  for (auto& node: nodes_)
    {
      for (auto& t: aut->out(node.first))
        {
          if (!bdd_implies(ap, t.cond))
            continue;
          // Check if we are leaving the SCC, if so we delete all the
          // braces as no cycles can be found with that node
          if (scc_opt && scc.scc_of(node.first) != scc.scc_of(t.dst))
            if (scc.is_accepting_scc(scc.scc_of(t.dst)))
              {
                // Find scc_id in the safra state currently being
                // constructed
                unsigned scc_id = ss.find_scc_brace_id(scc.scc_of(t.dst),
                                                       scc);
                // If SCC is present in node use the same id
                if (scc_id != -1U)
                  ss.update_succ({ scc_id }, t.dst,
                                 { /* empty */ });
                // Create a new SCC
                else
                  ss.update_succ({ /* no braces */ }, t.dst,
                                 { 0 });
              }
            else
              // When entering non accepting SCC don't create any braces
              ss.update_succ({ /* no braces */ }, t.dst, { /* empty */ });
          else
            ss.update_succ(node.second, t.dst, t.acc);
          assert(ss.nb_braces_.size() == ss.is_green_.size());
        }
    }
  if (use_bisimulation)
    ss.merge_redundant_states(implications, scc, is_connected);
  ss.ungreenify_last_brace();
  ss.color_ = ss.finalize_construction();
  return ss;
}

234 235
void
safra_state::compute_succs(const const_twa_graph_ptr& aut,
236 237 238 239 240 241 242 243
                           succs_t& res,
                           const scc_info& scc,
                           const std::map<int, bdd>& implications,
                           const std::vector<bool>& is_connected,
                           std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num,
                           std::vector<bdd>& all_bdds,
                           bool scc_opt,
                           bool use_bisimulation) const
244
{
245
  for (auto& ap: all_bdds)
246
    {
247 248
      safra_state ss = compute_succ(aut, ap, scc, implications, is_connected,
                                    scc_opt, use_bisimulation);
249
      unsigned bdd_idx = bdd2num[ap];
250 251
      res.emplace_back(ss, bdd_idx);

252 253
    }
}
254

255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
  void
  safra_state::merge_redundant_states(const std::map<int, bdd>& implications,
                                      const scc_info& scc,
                                      const std::vector<bool>& is_connected)
  {
    std::vector<int> to_remove;
    for (auto& n1: nodes_)
      {
        for (auto& n2: nodes_)
          {
            if (n1 == n2)
              continue;
            // index to see if there is a path from scc2 -> scc1
            unsigned idx = scc.scc_count() * scc.scc_of(n2.first) +
                           scc.scc_of(n1.first);
            if (bdd_implies(implications.at(n1.first),
                            implications.at(n2.first)) && !is_connected[idx])
            {
              to_remove.push_back(n1.first);
            }
          }
      }
    for (auto& n: to_remove)
      {
        for (auto& brace: nodes_[n])
          {
            --nb_braces_[brace];
          }
        nodes_.erase(n);
      }
  }

287 288 289 290 291
  void safra_state::ungreenify_last_brace()
  {
    // Step A4: For a brace to emit green it must surround other braces.
    // Hence, the last brace cannot emit green as it is the most inside brace.
    for (auto& n: nodes_)
292 293 294 295
      {
        if (!n.second.empty())
          is_green_[n.second.back()] = false;
      }
296 297
  }

298
  safra_state::color_t safra_state::finalize_construction()
299
  {
300 301
    unsigned red = -1U;
    unsigned green = -1U;
302 303 304
    std::vector<unsigned> rem_succ_of;
    assert(is_green_.size() == nb_braces_.size());
    for (unsigned i = 0; i < is_green_.size(); ++i)
305 306 307
      {
        if (nb_braces_[i] == 0)
          {
308
            // Step A3: Brackets that do not contain any nodes emit red
309
            is_green_[i] = false;
310 311 312 313

            // First brace can now be zero with new optim making it possible to
            // emit red 0
            red = std::min(red, 2 * i);
314
          }
315 316
        else if (is_green_[i])
          {
317
            green = std::min(green, 2 * i + 1);
318 319 320
            // Step A4 Emit green
            rem_succ_of.emplace_back(i);
          }
321 322 323
      }
    for (auto& n: nodes_)
      {
324
        // Step A4 Remove all brackets inside each green pair
325
        node_helper::truncate_braces(n.second, rem_succ_of, nb_braces_);
326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
      }

    // Step A5 define the rem variable
    std::vector<unsigned> decr_by(nb_braces_.size());
    unsigned decr = 0;
    for (unsigned i = 0; i < nb_braces_.size(); ++i)
      {
        // Step A5 renumber braces
        nb_braces_[i - decr] = nb_braces_[i];
        if (nb_braces_[i] == 0)
          {
            ++decr;
          }
        // Step A5, renumber braces
        decr_by[i] = decr;
      }
    nb_braces_.resize(nb_braces_.size() - decr);
    for (auto& n: nodes_)
      {
345
        node_helper::renumber(n.second, decr_by);
346
      }
347
    return std::min(red, green);
348 349
  }

350 351
  void node_helper::renumber(std::vector<brace_t>& braces,
                             const std::vector<unsigned>& decr_by)
352
  {
353
    for (unsigned idx = 0; idx < braces.size(); ++idx)
354
      {
355
        braces[idx] -= decr_by[braces[idx]];
356 357 358 359
      }
  }

  void
360 361 362
  node_helper::truncate_braces(std::vector<brace_t>& braces,
                                const std::vector<unsigned>& rem_succ_of,
                                std::vector<size_t>& nb_braces)
363
  {
364
    for (unsigned idx = 0; idx < braces.size(); ++idx)
365 366 367 368 369
      {
        bool found = false;
        // find first brace that matches rem_succ_of
        for (auto s: rem_succ_of)
          {
370
            found |= braces[idx] == s;
371 372 373
          }
        if (found)
          {
374
            assert(idx < braces.size() - 1);
375 376
            // For each deleted brace, decrement elements of nb_braces
            // This corresponds to A4 step
377
            for (unsigned i = idx + 1; i < braces.size(); ++i)
378
              {
379
                --nb_braces[braces[i]];
380
              }
381
            braces.resize(idx + 1);
382 383 384 385 386
            break;
          }
      }
  }

387
  void safra_state::update_succ(const std::vector<node_helper::brace_t>& braces,
388
                                state_t dst, const acc_cond::mark_t acc)
389
  {
390 391 392
    std::vector<node_helper::brace_t> copy = braces;
    if (acc.count())
      {
393
        assert(acc.has(0) && acc.count() == 1 && "Only TBA are accepted");
394
        // Accepting edge generate new braces: step A1
395 396 397 398 399 400 401 402 403
        copy.emplace_back(nb_braces_.size());
        // nb_braces_ gets updated later so put 0 for now
        nb_braces_.emplace_back(0);
        // Newly created braces cannot emit green as they won't have
        // any braces inside them (by construction)
        is_green_.push_back(false);
      }
    auto i = nodes_.emplace(dst, copy);
    if (!i.second)
404
      {
405 406 407
        // Step A2: Only keep the smallest nesting pattern (i-e  braces_) for
        // identical nodes.  Nesting_cmp returnes true if copy is smaller
        if (nesting_cmp(copy, i.first->second))
408
          {
409 410 411 412
            // Remove brace count of replaced node
            for (auto b: i.first->second)
              --nb_braces_[b];
            i.first->second = std::move(copy);
413 414
          }
        else
415
          // Node already exists and has bigger nesting pattern value
416 417
          return;
      }
418 419 420
    // After inserting new node, update the brace count per node
    for (auto b: i.first->second)
      ++nb_braces_[b];
421 422 423
  }

  // Called only to initialize first state
424
  safra_state::safra_state(state_t val, bool init_state, bool accepting_scc)
425 426 427 428
  {
    if (init_state)
      {
        unsigned state_num = val;
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
        if (!accepting_scc)
          {
            std::vector<node_helper::brace_t> braces = { /* no braces */ };
            nodes_.emplace(state_num, std::move(braces));
          }
        else
          {
            std::vector<node_helper::brace_t> braces = { 0 };
            nodes_.emplace(state_num, std::move(braces));
            // First brace has init_state hence one state inside the first
            // braces.
            nb_braces_.push_back(1);
            // One brace set
            is_green_.push_back(true);
          }
444 445 446 447 448
      }
    else
      {
        unsigned nb_braces = val;
        // One brace set
449
        is_green_.assign(nb_braces, true);
450
        // Newly created states are the empty mocrstate
451 452 453 454 455
        nb_braces_.assign(nb_braces, 0);
      }
  }

  bool
456
  safra_state::operator<(const safra_state& other) const
457
  {
458
    return nodes_ < other.nodes_;
459 460
  }

461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
  std::vector<bool>
  find_scc_paths(const scc_info& scc)
  {
    unsigned scccount = scc.scc_count();
    std::vector<bool> res(scccount * scccount, 0);
    for (unsigned i = 0; i < scccount; ++i)
      res[i + scccount * i] = 1;
    for (unsigned i = 0; i < scccount; ++i)
      {
        std::stack<unsigned> s;
        s.push(i);
        while (!s.empty())
          {
            unsigned src = s.top();
            s.pop();
            for (auto& d: scc.succ(src))
              {
                s.push(d);
                unsigned idx = scccount * i + d;
                res[idx] = 1;
              }
          }
      }
    return res;
  }

487
  twa_graph_ptr
488
  tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
489 490
                       bool pretty_print, bool scc_opt, bool use_bisimulation,
                       bool complete)
491
  {
492
    // Degeneralize
493
    twa_graph_ptr aut = spot::degeneralize_tba(a);
494
    std::map<int, bdd> implications;
495 496 497 498 499
    if (use_bisimulation)
      {
        aut = spot::scc_filter(aut);
        aut = simulation(aut, &implications);
      }
500
    scc_info scc = scc_info(aut);
501
    std::vector<bool> is_connected = find_scc_paths(scc);
502 503 504 505 506 507

    bdd allap = bddtrue;
    {
      typedef std::set<bdd, bdd_less_than> sup_map;
      sup_map sup;
      // Record occurrences of all guards
508
      for (auto& t: aut->edges())
509 510 511 512 513 514 515 516 517 518 519 520
        sup.emplace(t.cond);
      for (auto& i: sup)
        allap &= bdd_support(i);
    }

    // Preprocessing
    // Used to convert atomic bdd to id
    std::unordered_map<bdd, unsigned, bdd_hash> bdd2num;
    std::vector<bdd> num2bdd;
    // Nedded for compute succs
    // Used to convert large bdd to indexes
    std::unordered_map<bdd, std::pair<unsigned, unsigned>, bdd_hash> deltas;
521
    std::vector<safra_state::bdd_id_t> bddnums;
522
    for (auto& t: aut->edges())
523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541
      {
        auto it = deltas.find(t.cond);
        if (it == deltas.end())
          {
            bdd all = t.cond;
            unsigned prev = bddnums.size();
            while (all != bddfalse)
              {
                bdd one = bdd_satoneset(all, allap, bddfalse);
                all -= one;
                auto p = bdd2num.emplace(one, num2bdd.size());
                if (p.second)
                  num2bdd.push_back(one);
                bddnums.emplace_back(p.first->second);
              }
            deltas[t.cond] = std::make_pair(prev, bddnums.size());
          }
      }

542 543 544
    auto res = make_twa_graph(aut->get_dict());
    res->copy_ap_of(aut);
    res->prop_copy(aut,
545
                   { false, // state based
546
                   false, // inherently_weak
547 548
                   false, // deterministic
                   true // stutter inv
549 550 551
                   });

    // Given a safra_state get its associated state in output automata.
552
    // Required to create new edges from 2 safra-state
553
    power_set seen;
554 555
    auto init_state = aut->get_init_state_number();
    bool start_accepting = scc.is_accepting_scc(scc.scc_of(init_state)) ||
556
                           !scc_opt;
557
    safra_state init(init_state, true, start_accepting);
558 559 560 561 562
    unsigned num = res->new_state();
    res->set_init_state(num);
    seen.insert(std::make_pair(init, num));
    std::deque<safra_state> todo;
    todo.push_back(init);
563
    unsigned sets = 0;
564 565
    using succs_t = safra_state::succs_t;
    succs_t succs;
566 567 568 569 570
    while (!todo.empty())
      {
        safra_state curr = todo.front();
        unsigned src_num = seen.find(curr)->second;
        todo.pop_front();
571 572
        curr.compute_succs(aut, succs, scc, implications, is_connected,
                           bdd2num, num2bdd, scc_opt, use_bisimulation);
573 574
        for (auto s: succs)
          {
575 576 577
            // Don't construct sink state as complete does a better job at this
            if (s.first.nodes_.size() == 0)
              continue;
578 579 580 581 582 583 584 585 586 587 588 589
            auto i = seen.find(s.first);
	    unsigned dst_num;
	    if (i != seen.end())
	      {
		dst_num = i->second;
	      }
	    else
	      {
                dst_num = res->new_state();
                todo.push_back(s.first);
                seen.insert(std::make_pair(s.first, dst_num));
              }
590
            if (s.first.color_ != -1U)
591
              {
592
                res->new_edge(src_num, dst_num, num2bdd[s.second],
593
                                    {s.first.color_});
594 595
                // We only care about green acc which are odd
                if (s.first.color_ % 2 == 1)
596 597
                  sets = std::max(s.first.color_ + 1, sets);
              }
598
            else
599
              res->new_edge(src_num, dst_num, num2bdd[s.second]);
600
          }
601
        succs.clear();
602
      }
603
    remove_dead_acc(res, sets);
604 605
    // Acceptance is now min(odd) since we con emit Red on paths 0 with new opti
    res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
606
    res->prop_deterministic(true);
607
    res->prop_state_acc(false);
608

609 610
    if (bisimulation)
      res = simulation(res);
611 612
    if (pretty_print)
      res->set_named_prop("state-names", print_debug(seen));
613 614
    if (complete)
      spot::complete_here(res);
615 616 617
    return res;
  }
}