spot  2.12.2
powerset.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <set>
22 #include <vector>
23 #include <iosfwd>
24 #include <spot/twa/twagraph.hh>
25 
26 namespace spot
27 {
28 
29  struct SPOT_API power_map
30  {
31  typedef std::set<unsigned> power_state;
32  std::vector<power_state> map_;
33 
34  const power_state&
35  states_of(unsigned s) const
36  {
37  return map_.at(s);
38  }
39  };
40 
43  class SPOT_API output_aborter
44  {
45  unsigned max_states_;
46  unsigned max_edges_;
47  mutable bool reason_is_states_;
48  public:
49  output_aborter(unsigned max_states,
50  unsigned max_edges = ~0U)
51  : max_states_(max_states), max_edges_(max_edges)
52  {
53  }
54 
55  unsigned max_states() const
56  {
57  return max_states_;
58  }
59 
60  unsigned max_edges() const
61  {
62  return max_edges_;
63  }
64 
65  bool too_large(const const_twa_graph_ptr& aut) const
66  {
67  bool too_many_states = aut->num_states() > max_states_;
68  if (!too_many_states && (aut->num_edges() <= max_edges_))
69  return false;
70  // Only update the reason if we return true;
71  reason_is_states_ = too_many_states;
72  return true;
73  }
74 
75  std::ostream& print_reason(std::ostream&) const;
76  };
77 
78 
98 
99  SPOT_API twa_graph_ptr
100  tgba_powerset(const const_twa_graph_ptr& aut,
101  power_map& pm, bool merge = true,
102  const output_aborter* aborter = nullptr,
103  std::vector<unsigned>* accepting_sinks = nullptr);
104  SPOT_API twa_graph_ptr
105  tgba_powerset(const const_twa_graph_ptr& aut,
106  const output_aborter* aborter = nullptr,
107  std::vector<unsigned>* accepting_sinks = nullptr);
109 
110 
130  SPOT_API twa_graph_ptr
131  tba_determinize(const const_twa_graph_ptr& aut,
132  unsigned threshold_states = 0,
133  unsigned threshold_cycles = 0);
134 
162  SPOT_API twa_graph_ptr
163  tba_determinize_check(const twa_graph_ptr& aut,
164  unsigned threshold_states = 0,
165  unsigned threshold_cycles = 0,
166  formula f = nullptr,
167  const_twa_graph_ptr neg_aut = nullptr);
168 
169 }
Main class for temporal logic formula.
Definition: formula.hh:732
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:44
@ U
until
twa_graph_ptr tgba_powerset(const const_twa_graph_ptr &aut, power_map &pm, bool merge=true, const output_aborter *aborter=nullptr, std::vector< unsigned > *accepting_sinks=nullptr)
Build a deterministic automaton, ignoring acceptance conditions.
Definition: automata.hh:26
twa_graph_ptr tba_determinize(const const_twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0)
Determinize a TBA using the powerset construction.
twa_graph_ptr tba_determinize_check(const twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0, formula f=nullptr, const_twa_graph_ptr neg_aut=nullptr)
Determinize a TBA and make sure it is correct.
Definition: powerset.hh:30

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1