minimize.hh 6.68 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Laboratoire de Recherche et 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
#pragma once
21

22
23
#include <spot/twa/twagraph.hh>
#include <spot/tl/formula.hh>
24
25
26

namespace spot
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
27
  /// \addtogroup twa_reduction
28
29
30
  /// @{

  /// \brief Construct a minimal deterministic monitor.
31
  ///
32
33
34
35
  /// The automaton will be converted into minimal deterministic
  /// monitor.  All useless SCCs should have been previously removed
  /// (using scc_filter() for instance).  Then the automaton will be
  /// determinized and minimized using the standard DFA construction
36
  /// as if all states were accepting states.
37
  ///
38
  /// For more detail about monitors, see the following paper:
39
40
41
42
43
  /** \verbatim
      @InProceedings{	  tabakov.10.rv,
        author	  = {Deian Tabakov and Moshe Y. Vardi},
        title	  = {Optimized Temporal Monitors for SystemC{$^*$}},
        booktitle = {Proceedings of the 10th International Conferance
44
                     on Runtime Verification},
45
46
47
48
49
50
51
52
        pages	  = {436--451},
        year	  = 2010,
        volume	  = {6418},
        series	  = {Lecture Notes in Computer Science},
        month	  = nov,
        publisher = {Spring-Verlag}
      }
      \endverbatim */
53
54
  /// (Note: although the above paper uses Spot, this function did not
  /// exist in Spot at that time.)
55
  ///
56
57
58
  /// \param a the automaton to convert into a minimal deterministic monitor
  /// \pre Dead SCCs should have been removed from \a a before
  ///      calling this function.
59
  SPOT_API twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a);
60

61
  /// \brief Minimize a Büchi automaton in the WDBA class.
62
  ///
63
64
65
66
67
  /// This takes a TGBA whose language is representable by a Weak
  /// Deterministic Büchi Automaton, and construct a minimal WDBA for
  /// this language.  This essentially chains three algorithms:
  /// determinization, acceptance adjustment (Löding's coloring
  /// algorithm), and minimization (using a Moore-like approache).
68
  ///
69
70
71
72
73
74
75
76
  /// If the input automaton does not represent a WDBA language,
  /// the resulting automaton is still a WDBA, but it will not
  /// be equivalent to the original automaton.   Use the
  /// minimize_obligation() function if you are not sure whether
  /// it is safe to call this function.
  ///
  /// Please see the following paper for a discussion of this
  /// technique.
77
  ///
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
  /** \verbatim
      @InProceedings{	  dax.07.atva,
        author	  = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
        title     = {Mechanizing the Powerset Construction for Restricted
      		     Classes of {$\omega$}-Automata},
        year      = 2007,
        series	  = {Lecture Notes in Computer Science},
        publisher = {Springer-Verlag},
        volume	  = 4762,
        booktitle = {Proceedings of the 5th International Symposium on
      		     Automated Technology for Verification and Analysis
      		     (ATVA'07)},
        editor	  = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
      		     and Yoshio Okamura},
        month     = oct
      }
      \endverbatim */
95
  SPOT_API twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a);
96
97
98

  /// \brief Minimize an automaton if it represents an obligation property.
  ///
99
100
  /// This function attempts to minimize the automaton \a aut_f using the
  /// algorithm implemented in the minimize_wdba() function, and presented
101
102
  /// by the following paper:
  ///
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
  /** \verbatim
      @InProceedings{	  dax.07.atva,
        author	  = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
        title     = {Mechanizing the Powerset Construction for Restricted
      		     Classes of {$\omega$}-Automata},
        year      = 2007,
        series	  = {Lecture Notes in Computer Science},
        publisher = {Springer-Verlag},
        volume	  = 4762,
        booktitle = {Proceedings of the 5th International Symposium on
      		     Automated Technology for Verification and Analysis
      		     (ATVA'07)},
        editor	  = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
      		     and Yoshio Okamura},
        month     = oct
      }
      \endverbatim */
120
  ///
121
  /// Because it is hard to determine if an automaton corresponds
122
123
124
125
126
127
128
  /// to an obligation property, you should supply either the formula
  /// \a f expressed by the automaton \a aut_f, or \a aut_neg_f the negation
  /// of the automaton \a aut_neg_f.
  ///
  /// \param aut_f the automaton to minimize
  /// \param f the LTL formula represented by the automaton \a aut_f
  /// \param aut_neg_f an automaton representing the negation of \a aut_f
129
130
  /// \param reject_bigger Whether the minimal WDBA should be discarded if
  /// it has more states than the input.
131
132
  /// \return a new tgba if the automaton could be minimized, \a aut_f if
  /// the automaton cannot be minimized, 0 if we do not know if the
133
134
135
136
137
  /// minimization is correct because neither \a f nor \a aut_neg_f
  /// were supplied.
  ///
  /// The function proceeds as follows.  If the formula \a f or the
  /// automaton \a aut can easily be proved to represent an obligation
138
139
140
141
142
143
144
  /// formula, then the result of <code>minimize(aut)</code> is
  /// returned.  Otherwise, if \a aut_neg_f was not supplied but \a f
  /// was, \a aut_neg_f is built from the negation of \a f.  Then we
  /// check that <code>product(aut,!minimize(aut_f))</code> and <code>
  /// product(aut_neg_f,minize(aut))</code> are both empty.  If they
  /// are, the the minimization was sound.  (See the paper for full
  /// details.)
145
146
147
148
149
150
151
  ///
  /// If \a reject_bigger is set, this function will return the input
  /// automaton \a aut_f when the minimized WDBA has more states than
  /// the input automaton.  (More states are possible because of
  /// determinization step during minimize_wdba().)  Note that
  /// checking the size of the minimized WDBA occurs before ensuring
  /// that the minimized WDBA is correct.
152
153
  SPOT_API twa_graph_ptr
  minimize_obligation(const const_twa_graph_ptr& aut_f,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154
		      formula f = nullptr,
155
		      const_twa_graph_ptr aut_neg_f = nullptr,
156
		      bool reject_bigger = false);
157
  /// @}
158
}