spot  2.12.1
hoa.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 <iosfwd>
22 #include <spot/misc/common.hh>
23 #include <spot/twa/fwd.hh>
24 #include <vector>
25 #include <unordered_map>
26 #include <utility>
27 #include <functional>
28 #include <bddx.h>
29 
30 namespace spot
31 {
45  SPOT_API std::ostream&
46  print_hoa(std::ostream& os,
47  const const_twa_ptr& g,
48  const char* opt = nullptr);
49 
55  SPOT_API std::vector<std::pair<std::string, bdd>>*
56  get_aliases(const const_twa_ptr& g);
57 
65  SPOT_API void
66  set_aliases(twa_ptr g,
67  const std::vector<std::pair<std::string, bdd>>& aliases);
68 
71  class SPOT_API hoa_alias_formater final
72  {
73  public:
74  typedef std::vector<std::pair<std::string, bdd>> aliases_t;
75  private:
76  aliases_t* aliases_;
77  std::unordered_map<int, unsigned> aliases_map_;
78  std::vector<std::pair<bdd, unsigned>> alias_cubes_;
79  const char* false_str_;
80  const char* true_str_;
81  const char* or_str_;
82  const char* and_str_;
83  const char* not_str_;
84  const char* lpar_str_;
85  const char* rpar_str_;
86  std::function<std::string(int)> ap_printer_;
87  public:
103  hoa_alias_formater(const const_twa_graph_ptr& aut,
104  const char* false_str,
105  const char* true_str,
106  const char* or_str,
107  const char* and_str,
108  const char* not_str,
109  const char* lpar_str,
110  const char* rpar_str,
111  std::function<std::string(int)> ap_printer);
112 
151  std::string
152  encode_label(bdd label, unsigned aliases_start = 0);
153 
163  aliases_t* aliases()
164  {
165  return aliases_;
166  }
167  };
168 
180  SPOT_API void
181  create_alias_basis(const twa_graph_ptr& aut);
182 
183 }
Help printing BDDs as text, using aliases.
Definition: hoa.hh:72
std::string encode_label(bdd label, unsigned aliases_start=0)
Attempt to format a BDD label using aliases.
hoa_alias_formater(const const_twa_graph_ptr &aut, const char *false_str, const char *true_str, const char *or_str, const char *and_str, const char *not_str, const char *lpar_str, const char *rpar_str, std::function< std::string(int)> ap_printer)
Initialize this class from the aliases defined for an automaton.
aliases_t * aliases()
Retrieve the list of aliases.
Definition: hoa.hh:163
std::vector< std::pair< std::string, bdd > > * get_aliases(const const_twa_ptr &g)
Obtain aliases used in the HOA format.
void create_alias_basis(const twa_graph_ptr &aut)
Create an alias basis.
std::ostream & print_hoa(std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
Print reachable states in Hanoi Omega Automata format.
void set_aliases(twa_ptr g, const std::vector< std::pair< std::string, bdd >> &aliases)
Define all aliases used in the HOA format.
Definition: automata.hh:26

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