spot 2.10.6.dev
powerset.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2011, 2013-2015, 2019 Laboratoire de Recherche et
3// Développement de l'Epita.
4// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6// et Marie Curie.
7//
8// This file is part of Spot, a model checking library.
9//
10// Spot is free software; you can redistribute it and/or modify it
11// under the terms of the GNU General Public License as published by
12// the Free Software Foundation; either version 3 of the License, or
13// (at your option) any later version.
14//
15// Spot is distributed in the hope that it will be useful, but WITHOUT
16// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18// License for more details.
19//
20// You should have received a copy of the GNU General Public License
21// along with this program. If not, see <http://www.gnu.org/licenses/>.
22
23#pragma once
24
25#include <set>
26#include <vector>
27#include <iosfwd>
28#include <spot/twa/twagraph.hh>
29
30namespace spot
31{
32
33 struct SPOT_API power_map
34 {
35 typedef std::set<unsigned> power_state;
36 std::vector<power_state> map_;
37
38 const power_state&
39 states_of(unsigned s) const
40 {
41 return map_.at(s);
42 }
43 };
44
47 class SPOT_API output_aborter
48 {
49 unsigned max_states_;
50 unsigned max_edges_;
51 mutable bool reason_is_states_;
52 public:
53 output_aborter(unsigned max_states,
54 unsigned max_edges = ~0U)
55 : max_states_(max_states), max_edges_(max_edges)
56 {
57 }
58
59 unsigned max_states() const
60 {
61 return max_states_;
62 }
63
64 unsigned max_edges() const
65 {
66 return max_edges_;
67 }
68
69 bool too_large(const const_twa_graph_ptr& aut) const
70 {
71 bool too_many_states = aut->num_states() > max_states_;
72 if (!too_many_states && (aut->num_edges() <= max_edges_))
73 return false;
74 // Only update the reason if we return true;
75 reason_is_states_ = too_many_states;
76 return true;
77 }
78
79 std::ostream& print_reason(std::ostream&) const;
80 };
81
82
102
103 SPOT_API twa_graph_ptr
104 tgba_powerset(const const_twa_graph_ptr& aut,
105 power_map& pm, bool merge = true,
106 const output_aborter* aborter = nullptr,
107 std::vector<unsigned>* accepting_sinks = nullptr);
108 SPOT_API twa_graph_ptr
109 tgba_powerset(const const_twa_graph_ptr& aut,
110 const output_aborter* aborter = nullptr,
111 std::vector<unsigned>* accepting_sinks = nullptr);
113
114
134 SPOT_API twa_graph_ptr
135 tba_determinize(const const_twa_graph_ptr& aut,
136 unsigned threshold_states = 0,
137 unsigned threshold_cycles = 0);
138
166 SPOT_API twa_graph_ptr
167 tba_determinize_check(const twa_graph_ptr& aut,
168 unsigned threshold_states = 0,
169 unsigned threshold_cycles = 0,
170 formula f = nullptr,
171 const_twa_graph_ptr neg_aut = nullptr);
172
173}
Main class for temporal logic formula.
Definition: formula.hh:715
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:48
@ 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:27
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:34

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.4