safety.cc 2.62 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
3
// Développement 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 "safety.hh"
21
22
#include "misc/hash.hh"
#include <deque>
23
24
25
26

namespace spot
{
  bool
27
  is_guarantee_automaton(const const_tgba_ptr& aut, const scc_map* sm)
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
  {
    // Create an scc_map of the user did not give one to us.
    bool need_sm = !sm;
    if (need_sm)
      {
	scc_map* x = new scc_map(aut);
	x->build_map();
	sm = x;
      }

    bool result = true;

    unsigned scc_count = sm->scc_count();
    for (unsigned scc = 0; (scc < scc_count) && result; ++scc)
      {
	if (!sm->accepting(scc))
	  continue;
	// Accepting SCCs should have only one state.
	const std::list<const state*>& st = sm->states_of(scc);
	if (st.size() != 1)
	  {
	    result = false;
	    break;
	  }
	// The state should have only one transition that is a
	// self-loop labelled by true.
	const state* s = *st.begin();
	tgba_succ_iterator* it = aut->succ_iter(s);
	it->first();
	assert(!it->done());
	state* dest = it->current_state();
	bdd cond = it->current_condition();
60
	result = (!it->next()) && (cond == bddtrue) && (!dest->compare(s));
61
	dest->destroy();
62
	aut->release_iter(it);
63
64
65
66
67
68
69
70
71
      }

    // Free the scc_map if we created it.
    if (need_sm)
      delete sm;

    return result;
  }

72
  bool is_safety_mwdba(const const_tgba_ptr& aut)
73
  {
74
    state_unicity_table seen;	   // States already seen.
75
76
    std::deque<const state*> todo; // A queue of states yet to explore.

77
    todo.push_back(seen(aut->get_init_state()));
78
79
80
81
82
83
84

    bool all_accepting = true;
    while (all_accepting && !todo.empty())
      {
	const state* s = todo.front();
	todo.pop_front();

85
	for (auto it: aut->succ(s))
86
	  {
87
88
	    auto acc = it->current_acceptance_conditions();
	    if (!aut->acc().accepting(acc))
89
90
91
92
	      {
		all_accepting = false;
		break;
	      }
93
94
	    if (const state* d = seen.is_new(it->current_state()))
	      todo.push_back(d);
95
96
97
98
	  }
      }
    return all_accepting;
  }
99
100
101
102



}