Line data Source code
1 : // Author(s): Maurice Laveaux 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : 10 : #ifndef MCRL2_SYMBOLIC_TEST_UTILITY_H 11 : #define MCRL2_SYMBOLIC_TEST_UTILITY_H 12 : 13 : #ifdef MCRL2_ENABLE_SYLVAN 14 : 15 : #include "mcrl2/utilities/logger.h" 16 : 17 : #include <sylvan_ldd.hpp> 18 : 19 : #include <random> 20 : #include <vector> 21 : 22 : namespace mcrl2::symbolic 23 : { 24 : 25 0 : std::mt19937& gen() 26 : { 27 0 : static thread_local std::random_device rd; 28 0 : static thread_local std::mt19937 gen(rd()); 29 0 : return gen; 30 : } 31 : 32 : /// \brief Generate a random (state) vector. 33 0 : std::vector<std::uint32_t> random_vector(std::size_t length, std::size_t max_value) 34 : { 35 0 : std::uniform_int_distribution<> dist(0, max_value); 36 : 37 0 : std::vector<std::uint32_t> result(length); 38 0 : for (std::size_t i = 0; i < length; ++i) 39 : { 40 0 : result[i] = dist(gen()); 41 : } 42 : 43 0 : return result; 44 0 : } 45 : 46 : /// \brief Generate a set of random (state) vectors. 47 0 : sylvan::ldds::ldd random_set(std::size_t amount, std::size_t length, std::size_t max_value) 48 : { 49 0 : sylvan::ldds::ldd result; 50 : 51 0 : for (std::size_t i = 0; i < amount; ++i) 52 : { 53 0 : std::vector<std::uint32_t> random = random_vector(length, max_value); 54 0 : result = union_cube(result, random); 55 0 : } 56 : 57 0 : return result; 58 0 : } 59 : 60 : /// \brief Returns a random subset of U. 61 0 : sylvan::ldds::ldd random_subset(const sylvan::ldds::ldd& U, std::size_t amount) 62 : { 63 0 : std::uniform_int_distribution<> dist(0, satcount(U)); 64 : 65 0 : std::vector<std::vector<std::uint32_t>> contained = ldd_solutions(U); 66 0 : std::vector<std::vector<std::uint32_t>> result_vector; 67 : 68 : // Choose amount vectors. 69 0 : std::size_t added = 0; 70 0 : for (const auto& vector : contained) 71 : { 72 0 : if (dist(gen()) <= amount) 73 : { 74 0 : result_vector.push_back(vector); 75 0 : ++added; 76 : } 77 : 78 0 : if (added == amount) 79 : { 80 0 : break; 81 : } 82 : } 83 : 84 : // Construct the ldd. 85 0 : sylvan::ldds::ldd result; 86 0 : for (const auto& vector : result_vector) 87 : { 88 0 : result = union_cube(result, vector); 89 : } 90 : 91 0 : return result; 92 0 : } 93 : 94 : /// \brief Initialise the Sylvan library. 95 1 : void initialise_sylvan() 96 : { 97 : //mcrl2::log::logger::set_reporting_level(mcrl2::log::debug); 98 1 : lace_init(1, 1024*1024*4); 99 1 : lace_startup(0, nullptr, nullptr); 100 1 : sylvan::sylvan_set_limits(1024 * 1024 * 1024, 6, 6); 101 1 : sylvan::sylvan_init_package(); 102 1 : sylvan::sylvan_init_ldd(); 103 1 : } 104 : 105 : /// \brief Destroy the Sylvan library. 106 1 : void quit_sylvan() 107 : { 108 1 : sylvan::sylvan_quit(); 109 1 : lace_exit(); 110 1 : } 111 : 112 : } // namespace mcrl2::symbolic 113 : 114 : #endif // MCRL2_ENABLE_SYLVAN 115 : 116 : #endif // MCRL2_SYMBOLIC_TEST_UTILITY_H