isweakscc.cc 3.33 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
3
// de l'Epita (LRDE).
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
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/>.
19

20
#include "config.h"
21 22
#include <spot/tl/formula.hh>
#include <spot/twaalgos/isweakscc.hh>
23
#include <spot/twaalgos/genem.hh>
24 25 26

namespace spot
{
27 28 29 30 31 32 33 34 35
  namespace
  {
    [[noreturn]] static void
    invalid_scc_number(const char* fn)
    {
      throw std::invalid_argument(std::string(fn) + "(): invalid SCC number");
    }
  }

36 37
  bool
  scc_has_rejecting_cycle(scc_info& map, unsigned scc)
38
  {
39 40
    if (SPOT_UNLIKELY(scc >= map.scc_count()))
      invalid_scc_number("scc_has_rejecting_cycle");
41 42
    acc_cond neg_acc = map.get_aut()->get_acceptance().complement();
    return !generic_emptiness_check_for_scc(map, scc, neg_acc);
43 44 45
  }

  bool
46
  is_inherently_weak_scc(scc_info& map, unsigned scc)
47
  {
48 49
    if (SPOT_UNLIKELY(scc >= map.scc_count()))
      invalid_scc_number("is_inherently_weak_scc");
50 51
     // Weak SCCs are inherently weak.
    if (is_weak_scc(map, scc))
52
      return true;
53 54 55 56
    // If we reach this place, we now the SCC has an accepting cycle.
    // The question is now to find whether is also contains a
    // rejecting cycle.
    return !scc_has_rejecting_cycle(map, scc);
57 58
  }

Etienne Renault's avatar
Etienne Renault committed
59
  bool
60
  is_weak_scc(scc_info& map, unsigned scc)
61
  {
62 63
    if (SPOT_UNLIKELY(scc >= map.scc_count()))
      invalid_scc_number("is_weak_scc");
64 65
    // Rejecting SCCs are weak.
    if (map.is_rejecting_scc(scc))
66
      return true;
67
    // If all transitions use the same acceptance set, the SCC is weak.
68
    return map.marks_of(scc).size() == 1;
Etienne Renault's avatar
Etienne Renault committed
69 70 71
  }

  bool
72
  is_complete_scc(scc_info& map, unsigned scc)
Etienne Renault's avatar
Etienne Renault committed
73
  {
74 75
    if (SPOT_UNLIKELY(scc >= map.scc_count()))
      invalid_scc_number("is_complete_scc");
76
    auto a = map.get_aut();
77
    for (auto s: map.states_of(scc))
Etienne Renault's avatar
Etienne Renault committed
78
      {
79 80 81 82 83
        bool has_succ = false;
        bdd sumall = bddfalse;
        for (auto& t: a->out(s))
          {
            has_succ = true;
84 85 86 87 88 89 90 91 92 93
            bool in = true;
            for (auto d: a->univ_dests(t.dst))
              if (map.scc_of(d) != scc)
                {
                  in = false;
                  break;
                }
            if (!in)
              continue;
            sumall |= t.cond;
94 95 96 97 98
            if (sumall == bddtrue)
              break;
          }
        if (!has_succ || sumall != bddtrue)
          return false;
Etienne Renault's avatar
Etienne Renault committed
99 100 101 102 103
      }
    return true;
  }

  bool
104
  is_terminal_scc(scc_info& map, unsigned scc)
Etienne Renault's avatar
Etienne Renault committed
105
  {
106 107
    if (SPOT_UNLIKELY(scc >= map.scc_count()))
      invalid_scc_number("is_terminal_scc");
108

Etienne Renault's avatar
Etienne Renault committed
109
    // If all transitions use all acceptance conditions, the SCC is weak.
110
    return (map.is_accepting_scc(scc)
111
            && map.marks_of(scc).size() == 1
112
            && is_complete_scc(map, scc));
Etienne Renault's avatar
Etienne Renault committed
113
  }
114
}