isweakscc.cc 3.18 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Developpement 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 "cycles.hh"
Etienne Renault's avatar
Etienne Renault committed
21
#include "ltlast/formula.hh"
22
#include "isweakscc.hh"
23
24
25
26
27

namespace spot
{
  namespace
  {
28
    // Look for a non-accepting cycle.
29
    class weak_checker final : public enumerate_cycles
30
31
32
33
    {
    public:
      bool result;

34
      weak_checker(const scc_info& map)
35
	: enumerate_cycles(map), result(true)
36
37
38
39
      {
      }

      virtual bool
40
      cycle_found(unsigned start) override
41
      {
42
	dfs_stack::const_reverse_iterator i = dfs_.rbegin();
43
	acc_cond::mark_t acc = 0U;
44
	for (;;)
45
	  {
46
47
	    acc |= aut_->trans_storage(i->succ).acc;
	    if (i->s == start)
48
	      break;
49
	    ++i;
50
51
52
	    // The const cast is here to please old g++ versions.
	    // At least version 4.0 needs it.
	    assert(i != const_cast<const dfs_stack&>(dfs_).rend());
53
	  }
54
	if (!aut_->acc().accepting(acc))
55
56
57
58
59
60
61
62
63
64
65
66
67
	  {
	    // We have found an non-accepting cycle, so the SCC is not
	    // weak.
	    result = false;
	    return false;
	  }
	return true;
      }

    };
  }

  bool
68
  is_inherently_weak_scc(scc_info& map, unsigned scc)
69
  {
70
71
72
73
    if (!map.get_aut()->acc().uses_fin_acceptance())
      throw std::runtime_error
	("is_inherently_weak_scc() cannot work with Fin acceptance");

74
    // If no cycle is accepting, the SCC is weak.
75
    if (!map.is_accepting_scc(scc))
76
77
78
      return true;
    // If the SCC is accepting, but one cycle is not, the SCC is not
    // weak.
79
    weak_checker w(map);
80
81
82
83
    w.run(scc);
    return w.result;
  }

Etienne Renault's avatar
Etienne Renault committed
84
  bool
85
  is_weak_scc(scc_info& map, unsigned scc)
86
87
  {
    // If no cycle is accepting, the SCC is weak.
88
89
    if (!map.is_accepting_scc(scc)
	&& !map.get_aut()->acc().uses_fin_acceptance())
90
      return true;
91
    // If all transitions use the same acceptance set, the SCC is weak.
92
    return map.used_acc_of(scc).size() == 1;
Etienne Renault's avatar
Etienne Renault committed
93
94
95
  }

  bool
96
  is_complete_scc(scc_info& map, unsigned scc)
Etienne Renault's avatar
Etienne Renault committed
97
  {
98
    auto a = map.get_aut();
99
    for (auto s: map.states_of(scc))
Etienne Renault's avatar
Etienne Renault committed
100
      {
101
	bool has_succ = false;
Etienne Renault's avatar
Etienne Renault committed
102
	bdd sumall = bddfalse;
103
	for (auto& t: a->out(s))
Etienne Renault's avatar
Etienne Renault committed
104
	  {
105
106
107
	    has_succ = true;
	    if (map.scc_of(t.dst) == scc)
	      sumall |= t.cond;
108
109
	    if (sumall == bddtrue)
	      break;
Etienne Renault's avatar
Etienne Renault committed
110
	  }
111
	if (!has_succ || sumall != bddtrue)
112
	  return false;
Etienne Renault's avatar
Etienne Renault committed
113
114
115
116
117
      }
    return true;
  }

  bool
118
  is_terminal_scc(scc_info& map, unsigned scc)
Etienne Renault's avatar
Etienne Renault committed
119
120
  {
    // If all transitions use all acceptance conditions, the SCC is weak.
121
122
    return (map.is_accepting_scc(scc)
	    && map.used_acc_of(scc).size() == 1
123
	    && is_complete_scc(map, scc));
Etienne Renault's avatar
Etienne Renault committed
124
  }
125
}