convert.hh 2.41 KB
 Etienne Renault committed May 18, 2020 1 ``````// -*- coding: utf-8 -*- `````` Etienne Renault committed May 18, 2020 2 ``````// Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Developpement de `````` Etienne Renault committed May 18, 2020 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 ``````// l'Epita (LRDE). // // 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 // the Free Software Foundation; either version 3 of the License, or // (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 // along with this program. If not, see . #pragma once #include #include #include #include `````` Etienne Renault committed May 18, 2020 27 28 ``````#include #include `````` Etienne Renault committed May 18, 2020 29 30 31 32 33 34 35 `````` namespace spot { /// \brief Transform one truth assignment represented as a BDD /// into a \a cube cube passed in parameter. The parameter /// \a binder map bdd indexes to cube indexes. SPOT_API spot::cube satone_to_cube(bdd one, cubeset& cubeset, `````` Etienne Renault committed May 18, 2020 36 `````` std::unordered_map& binder); `````` Etienne Renault committed May 18, 2020 37 38 39 40 `````` /// \brief Transform a \a cube cube into bdd using the map /// that bind cube indexes to bdd indexes. SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset, `````` Etienne Renault committed May 18, 2020 41 `````` std::unordered_map& reverse_binder); `````` Etienne Renault committed May 18, 2020 42 `````` `````` Etienne Renault committed May 18, 2020 43 44 `````` /// \brief Extract the atomic propositions from the automaton. This method /// also fill the binder, i.e. the mapping between BDD indexes to cube indexes `````` Etienne Renault committed May 18, 2020 45 `````` SPOT_API std::vector* `````` Etienne Renault committed May 18, 2020 46 `````` extract_aps(spot::const_twa_graph_ptr aut, `````` Etienne Renault committed May 18, 2020 47 `````` std::unordered_map& ap_binder); `````` Etienne Renault committed May 18, 2020 48 49 `````` /// \brief Convert a twa into a twacube `````` Etienne Renault committed May 18, 2020 50 `````` SPOT_API twacube_ptr `````` Etienne Renault committed May 18, 2020 51 `````` twa_to_twacube(spot::const_twa_graph_ptr aut); `````` Etienne Renault committed May 18, 2020 52 `````` `````` Etienne Renault committed May 22, 2020 53 54 55 `````` /// \brief Convert a twacube into a twa. /// When \d is specified, the BDD_dict in parameter is used rather than /// creating a new one. `````` Etienne Renault committed May 18, 2020 56 `````` SPOT_API spot::twa_graph_ptr `````` Etienne Renault committed May 22, 2020 57 58 `````` twacube_to_twa(spot::twacube_ptr twacube, spot::bdd_dict_ptr d = nullptr); `````` Etienne Renault committed May 18, 2020 59 60 61 62 `````` /// \brief Check wether a twacube and a twa are equivalent SPOT_API bool are_equivalent(const spot::twacube_ptr twacube, const spot::const_twa_graph_ptr twa); `````` Etienne Renault committed May 18, 2020 63 ``}``