spot 2.11.3.dev
alternation.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement
3// de l'Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// 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// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// 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#include <spot/twa/twagraph.hh>
23#include <spot/twaalgos/powerset.hh>
24#include <utility>
25
26namespace spot
27{
46 class SPOT_API outedge_combiner
47 {
48 private:
49 const twa_graph_ptr& aut_;
50 std::map<unsigned, int> state_to_var;
51 std::map<int, unsigned> var_to_state;
52 bdd vars_;
53 public:
54 outedge_combiner(const twa_graph_ptr& aut);
55 ~outedge_combiner();
56 bdd operator()(unsigned st);
57 void new_dests(unsigned st, bdd out) const;
58 };
59
70 template<class I>
71 SPOT_API
72 unsigned states_and(const twa_graph_ptr& aut, I begin, I end)
73 {
74 if (begin == end)
75 throw std::runtime_error
76 ("state_and() expects an non-empty list of states");
77 outedge_combiner combiner(aut);
78 bdd combination = bddtrue;
79 while (begin != end)
80 combination &= combiner(*begin++);
81 unsigned new_s = aut->new_state();
82 combiner.new_dests(new_s, combination);
83 return new_s;
84 }
85
86 template<class T>
87 SPOT_API
88 unsigned states_and(const twa_graph_ptr& aut,
89 const std::initializer_list<T>& il)
90 {
91 return states_and(aut, il.begin(), il.end());
92 }
94
106 SPOT_API
107 twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut,
108 bool named_states = false,
109 const output_aborter* aborter = nullptr);
110
111
112 // Remove universal edges on the fly.
113
114 class SPOT_API univ_remover_state: public state
115 {
116 protected:
117 std::set<unsigned> states_;
118 bool is_reset_;
119
120 public:
121 univ_remover_state(const std::set<unsigned>& states);
122 univ_remover_state(const univ_remover_state& other)
123 : states_(other.states_), is_reset_(other.is_reset_)
124 {
125 }
126 int compare(const state* other) const override;
127 size_t hash() const override;
128 state* clone() const override;
129 const std::set<unsigned>& states() const;
130 bool is_reset() const;
131 };
132
133 class SPOT_API twa_univ_remover: public twa
134 {
135
136 private:
137 const_twa_graph_ptr aut_;
138 std::vector<int> state_to_var_;
139 std::map<int, unsigned> var_to_state_;
140 bdd all_states_;
141
142 public:
143 twa_univ_remover(const const_twa_graph_ptr& aut);
144 void allocate_state_vars();
145 const state* get_init_state() const override;
146 twa_succ_iterator* succ_iter(const state* s) const override;
147 std::string format_state(const state* s) const override;
148 };
149
150 typedef std::shared_ptr<twa_univ_remover> twa_univ_remover_ptr;
151
168 SPOT_API
169 twa_univ_remover_ptr remove_univ_otf(const const_twa_graph_ptr& aut);
170}
Definition: automata.hh:27

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