dtgbacomp.cc 5.45 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita.
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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 "dtgbacomp.hh"
21
#include "sccinfo.hh"
22
23
#include "complete.hh"
#include "cleanacc.hh"
24
25
26

namespace spot
{
27
  twa_graph_ptr dtgba_complement_nonweak(const const_twa_graph_ptr& aut)
28
  {
29
    // Clone the original automaton.
30
    auto res = make_twa_graph(aut,
31
32
33
				 { false, // state based
				   false, // inherently_weak
				   false, // deterministic
34
				   true,  // stutter inv.
35
				  });
36
37
    // Copy the old acceptance condition before we replace it.
    acc_cond oldacc = aut->acc(); // Copy it!
38

39
40
    // We will modify res in place, and the resulting
    // automaton will only have one acceptance set.
41
    // This changes aut->acc();
42
    res->set_buchi();
43
44
45
    // The resulting automaton is weak.
    res->prop_inherently_weak();
    res->prop_state_based_acc();
46

47
    unsigned num_sets = oldacc.num_sets();
48
49
50
    unsigned n = res->num_states();
    // We will duplicate the automaton as many times as we have
    // acceptance sets, and we need one extra sink state.
51
    res->new_states(num_sets * n + 1);
52
53
    unsigned sink = res->num_states() - 1;
    // The sink state has an accepting self-loop.
54
    res->new_acc_transition(sink, sink, bddtrue);
55

56
    for (unsigned src = 0; src < n; ++src)
57
      {
58
59
60
61
	// Keep track of all conditions on transition leaving state
	// SRC, so we can complete it.
	bdd missingcond = bddtrue;
	for (auto& t: res->out(src))
62
	  {
63
	    if (t.dst >= n)	// Ignore transitions we added.
64
65
	      break;
	    missingcond -= t.cond;
66
	    acc_cond::mark_t curacc = t.acc;
67
	    // The original transition must not accept anymore.
68
69
	    t.acc = 0U;

70
	    // Transition that were fully accepting are never cloned.
71
	    if (oldacc.accepting(curacc))
72
73
74
75
76
	      continue;
	    // Save t.cond and t.dst as the reference to t
	    // is invalided by calls to new_transition().
	    unsigned dst = t.dst;
	    bdd cond = t.cond;
77

78
	    // Iterate over all the acceptance conditions in 'curacc',
79
	    // an duplicate it for each clone for which it does not
80
81
	    // belong to the acceptance set.
	    unsigned add = 0;
82
	    for (unsigned set = 0; set < num_sets; ++set)
83
	      {
84
		add += n;
85
		if (!oldacc.has(curacc, set))
86
		  {
87
		    // Clone the transition
88
		    res->new_acc_transition(src + add, dst + add, cond);
89
90
91
92
		    assert(dst + add < sink);
		    // Using `t' is disallowed from now on as it is a
		    // reference to a transition that may have been
		    // reallocated.
93

94
95
96
97
98
99
100
101
		    // At least one transition per cycle should have a
		    // nondeterministic copy from the original clone.
		    // We use state numbers to select it, as any cycle
		    // is guaranteed to have at least one transition
		    // with dst <= src.  FIXME: Computing a feedback
		    // arc set would be better.
		    if (dst <= src)
		      res->new_transition(src, dst + add, cond);
102
103
		  }
	      }
104
	    assert(add == num_sets * n);
105
	  }
106
107
108
	// Complete the original automaton.
	if (missingcond != bddfalse)
	  res->new_transition(src, sink, missingcond);
109
      }
110
    res->merge_transitions();
111
    res->purge_dead_states();
112
    return res;
113
  }
114

115
  twa_graph_ptr dtgba_complement_weak(const const_twa_graph_ptr& aut)
116
117
  {
    // Clone the original automaton.
118
    auto res = make_twa_graph(aut,
119
120
121
				 { true, // state based
				   true, // inherently weak
				   true, // determinisitic
122
				   true,  // stutter inv.
123
				 });
124
125
126
127
    scc_info si(res);

    // We will modify res in place, and the resulting
    // automaton will only have one acceptance set.
128
    acc_cond::mark_t all_acc = res->set_buchi();
129
130
131
132
133
134
    res->prop_state_based_acc();

    unsigned sink = res->num_states();

    for (unsigned src = 0; src < sink; ++src)
      {
135
	acc_cond::mark_t acc = 0U;
136
	unsigned scc = si.scc_of(src);
137
	if (si.is_rejecting_scc(scc) && !si.is_trivial(scc))
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
	  acc = all_acc;

	// Keep track of all conditions on transition leaving state
	// SRC, so we can complete it.
	bdd missingcond = bddtrue;
	for (auto& t: res->out(src))
	  {
	    missingcond -= t.cond;
	    t.acc = acc;
	  }
	// Complete the original automaton.
	if (missingcond != bddfalse)
	  {
	    if (res->num_states() == sink)
	      {
		res->new_state();
		res->new_acc_transition(sink, sink, bddtrue);
	      }
	    res->new_transition(src, sink, missingcond);
	  }
      }
    //res->merge_transitions();
    return res;
  }

163
  twa_graph_ptr dtgba_complement(const const_twa_graph_ptr& aut)
164
  {
165
166
167
168
169
170
171
    if (aut->acc().is_generalized_buchi())
      {
	if (aut->is_inherently_weak())
	  return dtgba_complement_weak(aut);
	else
	  return dtgba_complement_nonweak(aut);
      }
172
    else
173
174
175
      {
	// Simply complete the automaton, and complement its
	// acceptance.
176
	auto res = cleanup_acceptance_here(tgba_complete(aut));
177
178
179
180
	res->set_acceptance(res->acc().num_sets(),
			    res->get_acceptance().complement());
	return res;
      }
181
  }
182
}