diff --git a/.github/workflows/build_cmake.yml b/.github/workflows/build_cmake.yml index b7b05dd9..c2088af5 100644 --- a/.github/workflows/build_cmake.yml +++ b/.github/workflows/build_cmake.yml @@ -61,3 +61,6 @@ jobs: name: codecov-umbrella yml: ./codecov.yml fail_ci_if_error: true + - name: Benchmarks + run: | + ./scripts/_ci-bench.sh diff --git a/.gitmodules b/.gitmodules index 4605afa7..e7bdb7f7 100644 --- a/.gitmodules +++ b/.gitmodules @@ -13,3 +13,9 @@ [submodule "third_party/CLI11"] path = third_party/CLI11 url = https://github.com/CLIUtils/CLI11.git +[submodule "third_party/google/benchmark"] + path = third_party/google/benchmark + url = https://github.com/google/benchmark.git +[submodule "third_party/cpphoafparser"] + path = third_party/cpphoafparser + url = https://github.com/whitemech/cpphoafparser.git diff --git a/CMakeLists.txt b/CMakeLists.txt index 7901167c..0c8089ab 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -27,10 +27,31 @@ project (Lydia set_property (GLOBAL PROPERTY USE_FOLDERS ON) +message("Using build type ${CMAKE_BUILD_TYPE}") + set (CMAKE_CXX_STANDARD 17) set (CMAKE_CXX_STANDARD_REQUIRED ON) set(CMAKE_EXPORT_COMPILE_COMMANDS ON) +# TODO introduce '-Werror', eventually +set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic") + +# these cannot be added due to Flex/Bison +#set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS} -fno-exceptions") +#set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS} -fno-rtti") + +if (CMAKE_BUILD_TYPE EQUAL "Debug" AND ENABLE_COVERAGE) + message("-- Code coverage enabled") + set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -O0") + set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -fprofile-arcs") + set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS} -ftest-coverage") + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage") +endif() + +if (PROFILE) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-omit-frame-pointer") +endif() + # TODO include this eventually #set(CMAKE_CXX_CLANG_TIDY # clang-tidy; @@ -48,15 +69,6 @@ set(CMAKE_MODULE_PATH set( CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin ) set( CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib ) -if (ENABLE_COVERAGE) - message("-- Code coverage enabled") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g ") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -O0") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fprofile-arcs") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ftest-coverage") - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage") -endif() - set (THREADS_PREFER_PTHREAD_FLAG ON) find_package (Threads REQUIRED) find_package(cudd REQUIRED) diff --git a/README.md b/README.md index 57fc53a6..8d5fd607 100644 --- a/README.md +++ b/README.md @@ -88,7 +88,8 @@ Afterwards, to run the tests: make test ``` -To configure the build for development, use the flag `-DENABLE_COVERAGE=ON` +To configure the build for development, +use the flag `-DCMAKE_BUILD_TYPE=Debug` ## Scripts @@ -106,6 +107,9 @@ For building: - `build.sh`: for normal build - `build-dev.sh` for development build +For benchmarking, use `./scripts/benchmark.sh` +(after `./scripts/build.sh`). + ## Docker development image We provide a Docker image for development. diff --git a/app/mona2sym/src/main.cpp b/app/mona2sym/src/main.cpp index 363b6a9d..9be98a23 100644 --- a/app/mona2sym/src/main.cpp +++ b/app/mona2sym/src/main.cpp @@ -38,14 +38,15 @@ * @param filename the path to the MONA DFA file. * @return nothing. */ -void transform(const std::string &input, const std::string &output_dir) { - auto my_dfa = whitemech::lydia::dfa::read_from_file(input); - // TODO reintroduce and make it work on CI... +void transform(const std::string &input, const std::string &output_dir, + const CUDD::Cudd &mgr) { + auto my_dfa = whitemech::lydia::dfa::read_from_file(input, mgr); + // TODO try to use , check CI // std::filesystem::create_directory(output_dir); auto cmd = "mkdir " + output_dir; std::system(cmd.c_str()); - my_dfa->bdd2dot(output_dir); - dfa_to_graphviz(*my_dfa, "output", "svg"); + my_dfa.bdd2dot(output_dir); + dfa_to_graphviz(my_dfa, "output", "svg"); } int main(int argc, char **argv) { @@ -63,7 +64,7 @@ int main(int argc, char **argv) { CLI11_PARSE(app, argc, argv); - transform(input_file, output_directory); - + auto mgr = CUDD::Cudd(); + transform(input_file, output_directory, mgr); return 0; } \ No newline at end of file diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt index 155e8913..316026f8 100644 --- a/lib/CMakeLists.txt +++ b/lib/CMakeLists.txt @@ -57,3 +57,4 @@ set (LIB_NAME ${LIB_NAME} PARENT_SCOPE) #test enable_testing () add_subdirectory (test) +add_subdirectory (benchmark) diff --git a/lib/benchmark/CMakeLists.txt b/lib/benchmark/CMakeLists.txt new file mode 100644 index 00000000..3109ca69 --- /dev/null +++ b/lib/benchmark/CMakeLists.txt @@ -0,0 +1,44 @@ +# +# This file is part of Lydia. +# +# Lydia 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. +# +# Lydia 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 Lydia. If not, see . +# + +# CMake build : library tests + +#configure variables +set (BENCHMARK_APP_NAME "${LIB_NAME}Bench") + +#configure directories +set (BENCHMARK_MODULE_PATH "${LIBRARY_MODULE_PATH}/benchmark") + +#configure benchmark directories +set (BENCHMARK_SRC_PATH "${BENCHMARK_MODULE_PATH}/src" ) + +#set includes +include_directories (${LIBRARY_INCLUDE_PATH} ${TEST_THIRD_PARTY_INCLUDE_PATH}) + +#set test sources +file (GLOB BENCHMARK_SOURCE_FILES "${BENCHMARK_SRC_PATH}/*.cpp") + +#set target executable +add_executable (${BENCHMARK_APP_NAME} ${BENCHMARK_SOURCE_FILES}) + +#add the library +target_link_libraries (${BENCHMARK_APP_NAME} ${LIB_NAME} Threads::Threads benchmark::benchmark ${CUDD_LIBRARIES}) + +add_custom_target(lydia-benchmark + COMMAND ${CMAKE_BINARY_DIR}/bin/${BENCHMARK_APP_NAME} + DEPENDS lydia + COMMENT "Run benchmarks." VERBATIM) diff --git a/lib/benchmark/src/dfa.cpp b/lib/benchmark/src/dfa.cpp new file mode 100644 index 00000000..84d42700 --- /dev/null +++ b/lib/benchmark/src/dfa.cpp @@ -0,0 +1,47 @@ +/* + * This file is part of Lydia. + * + * Lydia 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. + * + * Lydia 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 Lydia. If not, see . + */ + +#include "logic.hpp" +#include "translate.hpp" +#include "utils/benchmark.hpp" +#include +#include + +namespace whitemech::lydia::Benchmark { + +static void BM_cudd_manager_instantiation(benchmark::State &state) { + for (auto _ : state) { + auto mgr = CUDD::Cudd(); + escape(&mgr); + (void)mgr; + } +} +BENCHMARK(BM_cudd_manager_instantiation); + +static void BM_dfa_instantiation(benchmark::State &state) { + // we keep this outside since it's the operation that takes more time + // preallocate + auto mgr = CUDD::Cudd(); + for (auto _ : state) { + auto my_dfa = dfa(mgr, 1, 1); + escape(&my_dfa); + (void)my_dfa; + } +} +BENCHMARK(BM_dfa_instantiation); + +} // namespace whitemech::lydia::Benchmark diff --git a/lib/benchmark/src/logic.cpp b/lib/benchmark/src/logic.cpp new file mode 100644 index 00000000..48a44072 --- /dev/null +++ b/lib/benchmark/src/logic.cpp @@ -0,0 +1,96 @@ +/* + * This file is part of Lydia. + * + * Lydia 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. + * + * Lydia 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 Lydia. If not, see . + */ + +#include "logic.hpp" +#include "utils/benchmark.hpp" +#include +#include + +namespace whitemech::lydia::Benchmark { + +static void BM_boolean_from_constructor(benchmark::State &state) { + for (auto _ : state) { + auto x = LDLfBooleanAtom(true); + escape(&x); + (void)x; + } +} +BENCHMARK(BM_boolean_from_constructor); + +static void BM_shared_boolean_from_constructor(benchmark::State &state) { + for (auto _ : state) { + auto x = std::make_shared(true); + escape(&x); + (void)x; + } +} +BENCHMARK(BM_shared_boolean_from_constructor); + +static void BM_boolean_from_static_pointer(benchmark::State &state) { + for (auto _ : state) { + std::shared_ptr x = boolean(true); + escape(&x); + (void)x; + } +} +BENCHMARK(BM_boolean_from_static_pointer); + +static void BM_set_of_booleans_from_pointers(benchmark::State &state) { + for (auto _ : state) { + auto true_ = boolean(true); + auto false_ = boolean(false); + auto s = set_formulas{true_, false_}; + escape(&s); + (void)s; + } +} +BENCHMARK(BM_set_of_booleans_from_pointers); + +static void BM_set_of_booleans_from_shared_pointers(benchmark::State &state) { + for (auto _ : state) { + auto true_ = std::make_shared(true); + auto false_ = std::make_shared(false); + auto s = set_formulas{true_, false_}; + escape(&s); + (void)s; + } +} +BENCHMARK(BM_set_of_booleans_from_shared_pointers); + +static void BM_and_true_false(benchmark::State &state) { + for (auto _ : state) { + std::shared_ptr true_ = boolean(true); + std::shared_ptr false_ = boolean(false); + auto and_ = LDLfAnd(set_formulas{true_, false_}); + escape(&and_); + (void)and_; + } +} +BENCHMARK(BM_and_true_false); + +static void BM_shared_and_true_false(benchmark::State &state) { + for (auto _ : state) { + std::shared_ptr true_ = boolean(true); + std::shared_ptr false_ = boolean(false); + auto and_ = std::make_shared(set_formulas{true_, false_}); + escape(&and_); + (void)and_; + } +} +BENCHMARK(BM_shared_and_true_false); + +} // namespace whitemech::lydia::Benchmark diff --git a/lib/benchmark/src/main.cpp b/lib/benchmark/src/main.cpp new file mode 100644 index 00000000..8ea9ade9 --- /dev/null +++ b/lib/benchmark/src/main.cpp @@ -0,0 +1,20 @@ +/* + * This file is part of Lydia. + * + * Lydia 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. + * + * Lydia 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 Lydia. If not, see . + */ + +#include + +BENCHMARK_MAIN(); diff --git a/lib/benchmark/src/translate.cpp b/lib/benchmark/src/translate.cpp new file mode 100644 index 00000000..523cf0d6 --- /dev/null +++ b/lib/benchmark/src/translate.cpp @@ -0,0 +1,101 @@ +/* + * This file is part of Lydia. + * + * Lydia 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. + * + * Lydia 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 Lydia. If not, see . + */ + +#include "translate.hpp" +#include "logic.hpp" +#include "utils/benchmark.hpp" +#include +#include + +namespace whitemech::lydia::Benchmark { + +static void BM_translate_boolean(benchmark::State &state) { + // we keep this outside since it's the operation that takes more time + auto mgr = + CUDD::Cudd(0, 0, BENCH_CUDD_UNIQUE_SLOTS, BENCH_CUDD_CACHE_SLOTS, 0); + auto x = LDLfBooleanAtom(true); + for (auto _ : state) { + auto my_dfa = to_dfa(x, mgr); + escape(&my_dfa); + (void)my_dfa; + } +} +BENCHMARK(BM_translate_boolean); + +static void BM_translate_diamond(benchmark::State &state) { + // we keep this outside since it's the operation that takes more time + auto mgr = + CUDD::Cudd(0, 0, BENCH_CUDD_UNIQUE_SLOTS, BENCH_CUDD_CACHE_SLOTS, 0); + auto tt = std::make_shared(true); + auto true_ = std::make_shared(); + auto regex_true_ = std::make_shared(true_); + auto diamond = LDLfDiamond(regex_true_, tt); + for (auto _ : state) { + auto my_dfa = to_dfa(diamond, mgr); + escape(&my_dfa); + (void)my_dfa; + } +} +BENCHMARK(BM_translate_diamond); + +static void BM_translate_sequence(benchmark::State &state) { + auto mgr = + CUDD::Cudd(0, 0, BENCH_CUDD_UNIQUE_SLOTS, BENCH_CUDD_CACHE_SLOTS, 0); + auto tt = boolean(true); + for (auto _ : state) { + auto N = state.range(0); + auto regex = intitialize_sequence_regex(N); + auto diamond_formula = std::make_shared(regex, tt); + auto my_dfa = to_dfa(*diamond_formula, mgr); + escape(&my_dfa); + (void)my_dfa; + } +} +// clang-format off +BENCHMARK(BM_translate_sequence)->Arg(2)->Arg(3)->Arg(4) + ->Arg(5)->Arg(6)->Arg(7) + ->Arg(8)->Arg(9)->Arg(10) + ->Arg(11)->Arg(12)->Arg(13) + ->Unit(benchmark::kMillisecond) + ->Repetitions(5) + ->DisplayAggregatesOnly(true); +// clang-format on + +static void BM_translate_union(benchmark::State &state) { + auto mgr = + CUDD::Cudd(0, 0, BENCH_CUDD_UNIQUE_SLOTS, BENCH_CUDD_CACHE_SLOTS, 0); + auto tt = boolean(true); + for (auto _ : state) { + auto N = state.range(0); + auto regex = intitialize_union_regex(N); + auto diamond_formula = std::make_shared(regex, tt); + auto my_dfa = to_dfa(*diamond_formula, mgr); + escape(&my_dfa); + (void)my_dfa; + } +} +// clang-format off +BENCHMARK(BM_translate_union)->Arg(2)->Arg(3)->Arg(4) + ->Arg(5)->Arg(6)->Arg(7) + ->Arg(8)->Arg(9)->Arg(10) + ->Arg(11)->Arg(12)->Arg(13) + ->Unit(benchmark::kMillisecond) + ->Repetitions(5) + ->DisplayAggregatesOnly(true); +// clang-format on + +} // namespace whitemech::lydia::Benchmark diff --git a/lib/include/dfa.hpp b/lib/include/dfa.hpp index 2b2251f2..6822d0fb 100644 --- a/lib/include/dfa.hpp +++ b/lib/include/dfa.hpp @@ -38,6 +38,21 @@ class dfa { int nb_states{}; int nb_variables{}; + CUDD::BDD finalstatesBDD; + /*! + * Store the BDD roots - LSB order, i.e.: + * b_{n-1}, ..., b_1, b_0 + */ + vec_bdd root_bdds; + + /*! + * Store the BDD variables - LSB order, i.e.: + * b_{n-1}, ..., b_1, b_0, var_0, var_1, ... var_{m-1} + */ + vec_bdd bddvars; + + const CUDD::Cudd &mgr; + dfa(const dfa &) = delete; dfa &operator=(const dfa &) = delete; dfa(dfa &&) = delete; @@ -67,8 +82,7 @@ class dfa { * @param nb_bits the maximum number of bits available. * @param nb_variables the number of variables to be used. */ - dfa(CUDD::Cudd *mgr, int nb_bits, int nb_variables); - dfa(int nb_bits, int nb_variables); + dfa(const CUDD::Cudd &mgr, int nb_bits, int nb_variables); /* * @@ -91,20 +105,10 @@ class dfa { * @param behaviour the MONA behaviours * @param mona_bdd_nodes the shared multi-terminal BDD nodes (MONA DFA) */ - dfa(CUDD::Cudd *mgr, const std::vector &variables, int nb_states, - int initial_state, const std::vector &final_states, + dfa(const CUDD::Cudd &mgr, const std::vector &variables, + int nb_states, int initial_state, const std::vector &final_states, const std::vector &behaviour, std::vector &mona_bdd_nodes); - /* - * The same constructor as above, but the manager - * will be instantiated in the constructor. - */ - dfa(const std::vector &variables, int nb_states, - int initial_state, const std::vector &final_states, - const std::vector &behaviour, std::vector &smtbdd) - : dfa(new CUDD::Cudd(), variables, nb_states, initial_state, final_states, - behaviour, smtbdd) {} - static Logger logger; // void initialize(string filename, string partfile, Cudd& manager); @@ -128,21 +132,6 @@ class dfa { void dumpdot(CUDD::BDD &b, const std::string &filename); CUDD::BDD state2bdd(int s); - CUDD::BDD finalstatesBDD; - /*! - * Store the BDD roots - LSB order, i.e.: - * b_{n-1}, ..., b_1, b_0 - */ - vec_bdd root_bdds; - - /*! - * Store the BDD variables - LSB order, i.e.: - * b_{n-1}, ..., b_1, b_0, var_0, var_1, ... var_{m-1} - */ - vec_bdd bddvars; - - const std::unique_ptr mgr; - /*! * * Parse a MONA DFA file. @@ -154,8 +143,7 @@ class dfa { * @param filename path to the MONA DFA file. * @return a raw pointer to a DFA. */ - static dfa *read_from_file(const std::string &filename, - CUDD::Cudd *mgr = nullptr); + static dfa read_from_file(const std::string &filename, const CUDD::Cudd &mgr); /*! * Check whether a word of propositional interpretations diff --git a/lib/include/translate.hpp b/lib/include/translate.hpp index e37b1e4b..563f3c8b 100644 --- a/lib/include/translate.hpp +++ b/lib/include/translate.hpp @@ -35,7 +35,7 @@ namespace lydia { * @param formula the LDLf formula. * @return the equivalent DFA. */ -dfa *to_dfa(LDLfFormula &formula); +std::shared_ptr to_dfa(const LDLfFormula &formula, const CUDD::Cudd &mgr); /*! * This class represents an NFA state in diff --git a/lib/include/utils/benchmark.hpp b/lib/include/utils/benchmark.hpp new file mode 100644 index 00000000..db8ee340 --- /dev/null +++ b/lib/include/utils/benchmark.hpp @@ -0,0 +1,59 @@ +#pragma once +/* + * This file is part of Lydia. + * + * Lydia 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. + * + * Lydia 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 Lydia. If not, see . + */ + +#include +#include +#include + +static void escape(void *p) { asm volatile("" : : "g"(p) : "memory"); } + +static void clobber() { asm volatile("" : : : "memory"); } + +static const int BENCH_CUDD_UNIQUE_SLOTS = CUDD_UNIQUE_SLOTS; +static const int BENCH_CUDD_CACHE_SLOTS = CUDD_CACHE_SLOTS; + +namespace whitemech::lydia { + +static std::shared_ptr intitialize_sequence_regex(const int N) { + const std::string alphabet = + "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"; + auto vregex = vec_regex(); + vregex.reserve(N); + for (int i = 0; i < N; i++) { + auto tmp_symbol = std::to_string(alphabet.at(i)); + auto tmp = std::make_shared(tmp_symbol); + auto tmp_ptr = std::make_shared(tmp); + vregex.push_back(tmp_ptr); + } + return std::make_shared(vregex); +} + +static std::shared_ptr intitialize_union_regex(const int N) { + const std::string alphabet = + "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"; + auto sregex = set_regex(); + for (int i = 0; i < N; i++) { + auto tmp_symbol = std::to_string(alphabet.at(i)); + auto tmp = std::make_shared(tmp_symbol); + auto tmp_ptr = std::make_shared(tmp); + sregex.insert(tmp_ptr); + } + return std::make_shared(sregex); +} + +} // namespace whitemech::lydia \ No newline at end of file diff --git a/lib/include/utils/dfa_transform.hpp b/lib/include/utils/dfa_transform.hpp index 7dc33a6a..f6aadb3d 100644 --- a/lib/include/utils/dfa_transform.hpp +++ b/lib/include/utils/dfa_transform.hpp @@ -24,5 +24,7 @@ namespace lydia { void dfa_to_graphviz(const dfa &automaton, const std::string &output_filename, const std::string &format = "svg"); -} +void dfa_to_hoa(const dfa &automaton, std::ostream &o); + +} // namespace lydia } // namespace whitemech \ No newline at end of file diff --git a/lib/src/dfa.cpp b/lib/src/dfa.cpp index c87a340a..f3240bf1 100644 --- a/lib/src/dfa.cpp +++ b/lib/src/dfa.cpp @@ -17,7 +17,6 @@ #include "dfa.hpp" #include -#include #include #include @@ -26,28 +25,25 @@ namespace lydia { Logger dfa::logger = Logger("dfa"); -dfa::dfa(CUDD::Cudd *mgr, int nb_bits, int nb_variables) +dfa::dfa(const CUDD::Cudd &mgr, int nb_bits, int nb_variables) : mgr{mgr}, nb_bits{nb_bits}, nb_variables{nb_variables}, nb_states{1}, initial_state{0} { // add BDD variables for all the bits and variables for (int i = 0; i < nb_bits + nb_variables; i++) { - CUDD::BDD b = this->mgr->bddVar(); + CUDD::BDD b = this->mgr.bddVar(); bddvars.push_back(b); } for (int i = 0; i < nb_bits; i++) { // state 0 is a sink state - put a self-loop at bit 0. - CUDD::BDD zero = this->mgr->bddZero(); + CUDD::BDD zero = this->mgr.bddZero(); root_bdds.push_back(zero); } // start with empty set of final states. - finalstatesBDD = this->mgr->bddZero(); + finalstatesBDD = this->mgr.bddZero(); } -dfa::dfa(int nb_bits, int nb_variables) - : dfa(new CUDD::Cudd, nb_bits, nb_variables) {} - void dfa::bdd2dot(const std::string &directory) { for (int i = 0; i < root_bdds.size(); i++) { std::string filename = directory + "/" + std::to_string(i); @@ -67,13 +63,13 @@ void dfa::construct_bdd_from_mona( // for the variables. auto tBDD = std::vector(mona_bdd_nodes.size()); for (int i = 0; i < nb_bits + nb_variables; i++) { - CUDD::BDD b = mgr->bddVar(); + CUDD::BDD b = mgr.bddVar(); bddvars.push_back(b); } // For each bit of the state, create a BDD zero constant // Each var will be updated later in 'OR' (that's why we put zero) for (int i = 0; i < nb_bits; i++) { - CUDD::BDD d = mgr->bddZero(); + CUDD::BDD d = mgr.bddZero(); root_bdds.push_back(d); } // populate the tBDD mapping. @@ -92,7 +88,7 @@ void dfa::construct_bdd_from_mona( // Build the BDD representation of a state. // we set the temporary variable to 1 because // we are going to put it in 'AND' later. - CUDD::BDD tmp = mgr->bddOne(); + CUDD::BDD tmp = mgr.bddOne(); // the first for-loop handles the most significant bits // that are not covered by the binary representation. // the second for-loop handles all the other bits. @@ -116,7 +112,7 @@ void dfa::construct_bdd_from_mona( } // Create the BDD for recognizing the accepting states. - finalstatesBDD = mgr->bddZero(); + finalstatesBDD = mgr.bddZero(); for (int finalstate : final_states) { CUDD::BDD ac = state2bdd(finalstate); finalstatesBDD += ac; @@ -125,7 +121,7 @@ void dfa::construct_bdd_from_mona( CUDD::BDD dfa::state2bdd(int s) { std::string bin = state2bin(s, nb_bits); - CUDD::BDD b = mgr->bddOne(); + CUDD::BDD b = mgr.bddOne(); for (int j = 0; j < nb_bits; j++) { bool bit = int(bin[j]) - '0'; b *= var2bddvar(j, bit); @@ -149,16 +145,16 @@ vec_bdd dfa::try_get(int index, // than all the bits pre-allocated. // Set to zero the bits in excess. for (int m = 0; m < nb_bits - bins.size(); m++) { - CUDD::BDD temp_bdd = mgr->bddZero(); + CUDD::BDD temp_bdd = mgr.bddZero(); b.push_back(temp_bdd); } // Populate the LSBs for (char bin : bins) { if (bin == '0') { - CUDD::BDD temp_bdd = mgr->bddZero(); + CUDD::BDD temp_bdd = mgr.bddZero(); b.push_back(temp_bdd); } else if (bin == '1') { - CUDD::BDD temp_bdd = mgr->bddOne(); + CUDD::BDD temp_bdd = mgr.bddOne(); b.push_back(temp_bdd); } else { logger.error("error binary state"); @@ -192,11 +188,11 @@ void dfa::dumpdot(CUDD::BDD &b, const std::string &filename) { FILE *fp = fopen(filename.c_str(), "w"); std::vector single(1); single[0] = b; - this->mgr->DumpDot(single, nullptr, nullptr, fp); + this->mgr.DumpDot(single, nullptr, nullptr, fp); fclose(fp); } -dfa *dfa::read_from_file(const std::string &filename, CUDD::Cudd *mgr) { +dfa dfa::read_from_file(const std::string &filename, const CUDD::Cudd &mgr) { int nb_variables = -1; std::vector variables; int nb_states = -1; @@ -285,16 +281,11 @@ dfa *dfa::read_from_file(const std::string &filename, CUDD::Cudd *mgr) { assert(final_state >= 0 && final_state < nb_states); assert(mona_bdd_nodes.size() == nb_nodes); - if (mgr == nullptr) { - return new dfa(variables, nb_states, initial_state, final_states, behaviour, - mona_bdd_nodes); - } else { - return new dfa(mgr, variables, nb_states, initial_state, final_states, - behaviour, mona_bdd_nodes); - } + return dfa(mgr, variables, nb_states, initial_state, final_states, behaviour, + mona_bdd_nodes); } -dfa::dfa(CUDD::Cudd *mgr, const std::vector &variables, +dfa::dfa(const CUDD::Cudd &mgr, const std::vector &variables, int nb_states, int initial_state, const std::vector &final_states, const std::vector &behaviour, std::vector &mona_bdd_nodes) : mgr{mgr} { @@ -333,7 +324,7 @@ int dfa::add_state() { * How to deal with final_states_BDD? * * // add new state variable - * CUDD::BDD b = mgr->bddVar(); + * CUDD::BDD b = mgr.bddVar(); * bddvars.insert(bddvars.begin() + nb_bits, b); * ++nb_bits; */ diff --git a/lib/src/translate.cpp b/lib/src/translate.cpp index e433e2c9..439a5ede 100644 --- a/lib/src/translate.cpp +++ b/lib/src/translate.cpp @@ -27,7 +27,7 @@ namespace whitemech { namespace lydia { -dfa *to_dfa(LDLfFormula &formula) { +std::shared_ptr to_dfa(const LDLfFormula &formula, const CUDD::Cudd &mgr) { // build initial state of the DFA. auto formula_nnf = to_nnf(formula); set_formulas initial_state_formulas{formula_nnf}; @@ -43,7 +43,7 @@ dfa *to_dfa(LDLfFormula &formula) { auto all_interpretations = powerset(atoms); // TODO max number of bits - dfa *automaton = new dfa(10, atoms.size()); + std::shared_ptr automaton = std::make_shared(mgr, 10, atoms.size()); automaton->add_state(); automaton->set_initial_state(1); diff --git a/lib/src/utils/dfa_transform.cpp b/lib/src/utils/dfa_transform.cpp index c58b4b33..3f690a08 100644 --- a/lib/src/utils/dfa_transform.cpp +++ b/lib/src/utils/dfa_transform.cpp @@ -16,8 +16,10 @@ */ #include "utils/dfa_transform.hpp" +#include "cpphoafparser/consumer/hoa_consumer_print.hh" #include #include +#include #include #include #include @@ -101,5 +103,31 @@ void dfa_to_graphviz(const dfa &automaton, const std::string &output_filename, agclose(g); gvFreeContext(gvc); } + +void dfa_to_hoa(const dfa &automaton, std::ostream &o) { + auto printer = cpphoafparser::HOAConsumerPrint(o); + printer.notifyHeaderStart("v1"); + printer.setNumberOfStates(automaton.nb_states); + printer.addStartStates({static_cast(automaton.initial_state)}); + printer.provideAcceptanceName("Rabin", {1}); + + auto fin0 = cpphoafparser::HOAConsumer::acceptance_expr::Atom( + cpphoafparser::AtomAcceptance::Fin(0)); + auto inf1 = cpphoafparser::HOAConsumer::acceptance_expr::Atom( + cpphoafparser::AtomAcceptance::Inf(1)); + printer.setAcceptanceCondition(2, fin0 & inf1); + + std::vector range(automaton.nb_variables); + std::vector ap_names; + ap_names.reserve(automaton.nb_variables); + std::iota(range.begin(), range.end(), 0); + std::transform(std::begin(range), std::end(range), + std::back_inserter(ap_names), + [](int i) { return std::to_string(i); }); + printer.setAPs(ap_names); + printer.notifyBodyStart(); + // TODO do body according to automaton +} + } // namespace lydia } // namespace whitemech diff --git a/lib/test/src/test_dfa.cpp b/lib/test/src/test_dfa.cpp index 76a9ec48..af8b0dd9 100644 --- a/lib/test/src/test_dfa.cpp +++ b/lib/test/src/test_dfa.cpp @@ -99,23 +99,19 @@ TEST_CASE("Test Cudd", "[cudd]") { TEST_CASE("Test DFA initialization", "[dfa]") { whitemech::lydia::Logger::level(LogLevel::debug); - SECTION("Initialize without Cudd manager.") { - auto my_dfa = // NOLINT - dfa::read_from_file("../../../lib/test/src/data/mona/eventually_a.dfa"); - } - SECTION("Initialize with Cudd manager.") { - auto mgr = new CUDD::Cudd(); + auto mgr = CUDD::Cudd(); auto my_dfa = dfa::read_from_file( // NOLINT - "../../../lib/test/src/data/mona/eventually_a.dfa", mgr = mgr); + "../../../lib/test/src/data/mona/eventually_a.dfa", mgr); } } TEST_CASE("Test bdd2dot", "[dfa]") { whitemech::lydia::Logger::level(LogLevel::debug); - auto my_dfa = - dfa::read_from_file("../../../lib/test/src/data/mona/mona_example.dfa"); - my_dfa->bdd2dot(); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa::read_from_file( + "../../../lib/test/src/data/mona/mona_example.dfa", mgr); + my_dfa.bdd2dot(); } TEST_CASE("Test accepts", "[dfa]") { @@ -137,29 +133,31 @@ TEST_CASE("Test accepts", "[dfa]") { auto t_a_a = trace{empty, a, a}; SECTION("Test F(a)") { - auto my_dfa = - dfa::read_from_file("../../../lib/test/src/data/mona/eventually_a.dfa"); - - REQUIRE(!my_dfa->accepts(t_)); - REQUIRE(!my_dfa->accepts(t_na)); - REQUIRE(my_dfa->accepts(t_a)); - REQUIRE(!my_dfa->accepts(t_na_na)); - REQUIRE(my_dfa->accepts(t_na_a)); - REQUIRE(my_dfa->accepts(t_a_na)); - REQUIRE(my_dfa->accepts(t_a_a)); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa::read_from_file( + "../../../lib/test/src/data/mona/eventually_a.dfa", mgr); + + REQUIRE(!my_dfa.accepts(t_)); + REQUIRE(!my_dfa.accepts(t_na)); + REQUIRE(my_dfa.accepts(t_a)); + REQUIRE(!my_dfa.accepts(t_na_na)); + REQUIRE(my_dfa.accepts(t_na_a)); + REQUIRE(my_dfa.accepts(t_a_na)); + REQUIRE(my_dfa.accepts(t_a_a)); } SECTION("Test G(a)") { - auto my_dfa = - dfa::read_from_file("../../../lib/test/src/data/mona/always_a.dfa"); - - REQUIRE(!my_dfa->accepts(t_)); - REQUIRE(!my_dfa->accepts(t_na)); - REQUIRE(my_dfa->accepts(t_a)); - REQUIRE(!my_dfa->accepts(t_na_na)); - REQUIRE(!my_dfa->accepts(t_na_a)); - REQUIRE(!my_dfa->accepts(t_a_na)); - REQUIRE(my_dfa->accepts(t_a_a)); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa::read_from_file( + "../../../lib/test/src/data/mona/always_a.dfa", mgr); + + REQUIRE(!my_dfa.accepts(t_)); + REQUIRE(!my_dfa.accepts(t_na)); + REQUIRE(my_dfa.accepts(t_a)); + REQUIRE(!my_dfa.accepts(t_na_na)); + REQUIRE(!my_dfa.accepts(t_na_a)); + REQUIRE(!my_dfa.accepts(t_a_na)); + REQUIRE(my_dfa.accepts(t_a_a)); } } @@ -175,50 +173,50 @@ TEST_CASE("Incremental construction", "[dfa]") { auto t_a_a = trace{a, a}; SECTION("The starting DFA does not accept anything") { - auto mgr = new CUDD::Cudd(); - auto my_dfa = new dfa(mgr, 10, 1); - - REQUIRE(my_dfa->get_successor(0, t_na[0]) == 0); - REQUIRE(my_dfa->get_successor(0, t_a[0]) == 0); - - REQUIRE(!my_dfa->accepts(t_)); - REQUIRE(!my_dfa->accepts(t_na)); - REQUIRE(!my_dfa->accepts(t_a)); - REQUIRE(!my_dfa->accepts(t_na_na)); - REQUIRE(!my_dfa->accepts(t_na_a)); - REQUIRE(!my_dfa->accepts(t_a_na)); - REQUIRE(!my_dfa->accepts(t_a_a)); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa(mgr, 10, 1); + + REQUIRE(my_dfa.get_successor(0, t_na[0]) == 0); + REQUIRE(my_dfa.get_successor(0, t_a[0]) == 0); + + REQUIRE(!my_dfa.accepts(t_)); + REQUIRE(!my_dfa.accepts(t_na)); + REQUIRE(!my_dfa.accepts(t_a)); + REQUIRE(!my_dfa.accepts(t_na_na)); + REQUIRE(!my_dfa.accepts(t_na_a)); + REQUIRE(!my_dfa.accepts(t_a_na)); + REQUIRE(!my_dfa.accepts(t_a_a)); } SECTION("With the state 0 as final will make the DFA accept everything.") { - auto mgr = new CUDD::Cudd(); - auto my_dfa = new dfa(mgr, 10, 1); - my_dfa->set_final_state(0, true); - REQUIRE(my_dfa->accepts(t_)); - REQUIRE(my_dfa->accepts(t_na)); - REQUIRE(my_dfa->accepts(t_a)); - REQUIRE(my_dfa->accepts(t_na_na)); - REQUIRE(my_dfa->accepts(t_na_a)); - REQUIRE(my_dfa->accepts(t_a_na)); - REQUIRE(my_dfa->accepts(t_a_a)); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa(mgr, 10, 1); + my_dfa.set_final_state(0, true); + REQUIRE(my_dfa.accepts(t_)); + REQUIRE(my_dfa.accepts(t_na)); + REQUIRE(my_dfa.accepts(t_a)); + REQUIRE(my_dfa.accepts(t_na_na)); + REQUIRE(my_dfa.accepts(t_na_a)); + REQUIRE(my_dfa.accepts(t_a_na)); + REQUIRE(my_dfa.accepts(t_a_a)); } SECTION("Create a simple DFA: add new state, make it final, and add a " "transition to it.") { - auto mgr = new CUDD::Cudd(); - auto my_dfa = new dfa(mgr, 10, 1); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa(mgr, 10, 1); - int new_state = my_dfa->add_state(); + int new_state = my_dfa.add_state(); REQUIRE(new_state == 1); - my_dfa->set_initial_state(new_state); + my_dfa.set_initial_state(new_state); - REQUIRE(!my_dfa->accepts(t_)); - REQUIRE(!my_dfa->accepts(t_na)); - REQUIRE(!my_dfa->accepts(t_a)); - REQUIRE(!my_dfa->accepts(t_na_na)); - REQUIRE(!my_dfa->accepts(t_na_a)); - REQUIRE(!my_dfa->accepts(t_a_na)); - REQUIRE(!my_dfa->accepts(t_a_a)); + REQUIRE(!my_dfa.accepts(t_)); + REQUIRE(!my_dfa.accepts(t_na)); + REQUIRE(!my_dfa.accepts(t_a)); + REQUIRE(!my_dfa.accepts(t_na_na)); + REQUIRE(!my_dfa.accepts(t_na_a)); + REQUIRE(!my_dfa.accepts(t_a_na)); + REQUIRE(!my_dfa.accepts(t_a_a)); SECTION("... and add a self-loop with dont_care=true") { /* @@ -226,21 +224,21 @@ TEST_CASE("Incremental construction", "[dfa]") { * That is, with dont_care=true and an empty * set of constraints. */ - my_dfa->set_final_state(1, true); - my_dfa->add_transition(1, interpretation_set{}, 1, true); - - REQUIRE(my_dfa->get_successor(0, t_na[0]) == 0); - REQUIRE(my_dfa->get_successor(0, t_a[0]) == 0); - REQUIRE(my_dfa->get_successor(1, t_na[0]) == 1); - REQUIRE(my_dfa->get_successor(1, t_a[0]) == 1); - - REQUIRE(my_dfa->accepts(t_)); - REQUIRE(my_dfa->accepts(t_na)); - REQUIRE(my_dfa->accepts(t_a)); - REQUIRE(my_dfa->accepts(t_na_na)); - REQUIRE(my_dfa->accepts(t_na_a)); - REQUIRE(my_dfa->accepts(t_a_na)); - REQUIRE(my_dfa->accepts(t_a_a)); + my_dfa.set_final_state(1, true); + my_dfa.add_transition(1, interpretation_set{}, 1, true); + + REQUIRE(my_dfa.get_successor(0, t_na[0]) == 0); + REQUIRE(my_dfa.get_successor(0, t_a[0]) == 0); + REQUIRE(my_dfa.get_successor(1, t_na[0]) == 1); + REQUIRE(my_dfa.get_successor(1, t_a[0]) == 1); + + REQUIRE(my_dfa.accepts(t_)); + REQUIRE(my_dfa.accepts(t_na)); + REQUIRE(my_dfa.accepts(t_a)); + REQUIRE(my_dfa.accepts(t_na_na)); + REQUIRE(my_dfa.accepts(t_na_a)); + REQUIRE(my_dfa.accepts(t_a_na)); + REQUIRE(my_dfa.accepts(t_a_a)); } SECTION("... and add a self-loop with dont_care=false") { @@ -250,21 +248,21 @@ TEST_CASE("Incremental construction", "[dfa]") { * That means all the propositions not present in the interpretation set * have to be necessarily false in order to satisfy the guard. */ - my_dfa->set_final_state(1, true); - my_dfa->add_transition(1, interpretation_set{}, 1, false); - - REQUIRE(my_dfa->get_successor(0, t_na[0]) == 0); - REQUIRE(my_dfa->get_successor(0, t_a[0]) == 0); - REQUIRE(my_dfa->get_successor(1, t_na[0]) == 1); - REQUIRE(my_dfa->get_successor(1, t_a[0]) == 0); - - REQUIRE(my_dfa->accepts(t_)); - REQUIRE(my_dfa->accepts(t_na)); - REQUIRE(!my_dfa->accepts(t_a)); - REQUIRE(my_dfa->accepts(t_na_na)); - REQUIRE(!my_dfa->accepts(t_na_a)); - REQUIRE(!my_dfa->accepts(t_a_na)); - REQUIRE(!my_dfa->accepts(t_a_a)); + my_dfa.set_final_state(1, true); + my_dfa.add_transition(1, interpretation_set{}, 1, false); + + REQUIRE(my_dfa.get_successor(0, t_na[0]) == 0); + REQUIRE(my_dfa.get_successor(0, t_a[0]) == 0); + REQUIRE(my_dfa.get_successor(1, t_na[0]) == 1); + REQUIRE(my_dfa.get_successor(1, t_a[0]) == 0); + + REQUIRE(my_dfa.accepts(t_)); + REQUIRE(my_dfa.accepts(t_na)); + REQUIRE(!my_dfa.accepts(t_a)); + REQUIRE(my_dfa.accepts(t_na_na)); + REQUIRE(!my_dfa.accepts(t_na_a)); + REQUIRE(!my_dfa.accepts(t_a_na)); + REQUIRE(!my_dfa.accepts(t_a_a)); } } diff --git a/lib/test/src/test_misc.cpp b/lib/test/src/test_misc.cpp index 8b7dbf17..0925bff1 100644 --- a/lib/test/src/test_misc.cpp +++ b/lib/test/src/test_misc.cpp @@ -60,15 +60,33 @@ TEST_CASE("binary vector/string to int", "[bin2state]") { } TEST_CASE("DFA to Graphviz", "[dfa_transform]") { - auto *mgr = new CUDD::Cudd(); - dfa *my_dfa = new dfa(mgr, 1, 1); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa(mgr, 1, 1); - my_dfa->add_state(); - my_dfa->add_transition(0, interpretation_set{}, 1); - my_dfa->add_transition(1, interpretation_set{}, 1); - my_dfa->set_final_state(1, true); + my_dfa.add_state(); + my_dfa.add_transition(0, interpretation_set{}, 1); + my_dfa.add_transition(1, interpretation_set{}, 1); + my_dfa.set_final_state(1, true); - dfa_to_graphviz(*my_dfa, "output.svg", "svg"); + dfa_to_graphviz(my_dfa, "output.svg", "svg"); +} + +TEST_CASE("DFA to HOA", "[dfa_transform]") { + Logger log("DFA to HOA"); + auto mgr = CUDD::Cudd(); + auto my_dfa = dfa(mgr, 1, 1); + + my_dfa.add_state(); + my_dfa.add_transition(0, interpretation_set{}, 1); + my_dfa.add_transition(1, interpretation_set{}, 1); + my_dfa.set_final_state(1, true); + + std::stringstream o; + dfa_to_hoa(my_dfa, o); + + auto output = o.str(); + REQUIRE(output.length() > 0); + log.debug(output); } } // namespace whitemech::lydia::Test \ No newline at end of file diff --git a/lib/test/src/test_translate.cpp b/lib/test/src/test_translate.cpp index 917a7ffc..1beb0b0f 100644 --- a/lib/test/src/test_translate.cpp +++ b/lib/test/src/test_translate.cpp @@ -40,7 +40,8 @@ TEST_CASE("Translate !(ff & tt)", "[translate]") { auto not_and = LDLfNot(ff_and_tt); auto formula_name = to_string(*ff_and_tt); // TODO complete. - auto *my_dfa = to_dfa(not_and); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(not_and, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -59,7 +60,8 @@ TEST_CASE("Translate (ff & tt)", "[translate]") { auto ff_and_tt = std::make_shared(args); auto formula_name = to_string(*ff_and_tt); - auto *my_dfa = to_dfa(*ff_and_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*ff_and_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -80,7 +82,8 @@ TEST_CASE("Translate tt", "[translate]") { auto tt = boolean(true); auto diamond_formula_true_tt = std::make_shared(regex_true, tt); - auto *my_dfa = to_dfa(*diamond_formula_true_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_true_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -99,7 +102,8 @@ TEST_CASE("Translate tt", "[translate]") { auto tt = boolean(true); auto diamond_formula_a_tt = std::make_shared(regex_a, tt); - auto *my_dfa = to_dfa(*diamond_formula_a_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_a_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -127,7 +131,8 @@ TEST_CASE("Translate tt", "[translate]") { auto diamond_formula_a_and_b_tt = std::make_shared(regex_a_and_b, tt); - auto *my_dfa = to_dfa(*diamond_formula_a_and_b_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_a_and_b_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -156,7 +161,8 @@ TEST_CASE("Translate {true}tt", "[translate]") { auto tt = boolean(true); auto box_formula_true_tt = std::make_shared(regex_true, tt); - auto *my_dfa = to_dfa(*box_formula_true_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_true_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -175,7 +181,8 @@ TEST_CASE("Translate {a}tt", "[translate]") { auto tt = boolean(true); auto box_formula_a_tt = std::make_shared(regex_a, tt); - auto *my_dfa = to_dfa(*box_formula_a_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -202,7 +209,8 @@ TEST_CASE("Translate {a & b}tt", "[translate]") { auto tt = boolean(true); auto box_formula_a_and_b_tt = std::make_shared(regex_a_and_b, tt); - auto *my_dfa = to_dfa(*box_formula_a_and_b_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_and_b_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -231,7 +239,8 @@ TEST_CASE("Translate {a}ff", "[translate]") { auto tt = boolean(false); auto box_formula_a_tt = std::make_shared(regex_a, tt); - auto *my_dfa = to_dfa(*box_formula_a_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -257,7 +266,8 @@ TEST_CASE("Translate <tt?>tt", "[translate]") { auto regex_test = std::make_shared(diamond_formula_true_tt); auto diamond_test = std::make_shared(regex_test, tt); - auto *my_dfa = to_dfa(*diamond_test); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_test, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -279,7 +289,8 @@ TEST_CASE("Translate <{true}ff?>tt", "[translate]") { auto regex_test = std::make_shared(box_formula_true_ff); auto diamond_test = std::make_shared(regex_test, tt); - auto *my_dfa = to_dfa(*diamond_test); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_test, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -303,7 +314,8 @@ TEST_CASE("Translate tt", "[translate]") { auto diamond_formula_a_plus_b_tt = std::make_shared(regex_a_union_b, tt); - auto *my_dfa = to_dfa(*diamond_formula_a_plus_b_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_a_plus_b_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -336,7 +348,8 @@ TEST_CASE("Translate {a plus b}ff", "[translate]") { auto ff = boolean(false); auto box_formula_a_plus_b_ff = std::make_shared(regex_a_union_b, ff); - auto *my_dfa = to_dfa(*box_formula_a_plus_b_ff); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_plus_b_ff, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -370,7 +383,8 @@ TEST_CASE("Translate tt", "[translate]") { auto diamond_formula_a_seq_b_tt = std::make_shared(regex_a_seq_b, tt); - auto *my_dfa = to_dfa(*diamond_formula_a_seq_b_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_a_seq_b_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -405,7 +419,8 @@ TEST_CASE("Translate {a , b}ff", "[translate]") { std::make_shared(vec_regex{regex_a, regex_b}); auto box_formula_a_seq_b_ff = std::make_shared(regex_a_seq_b, ff); - auto *my_dfa = to_dfa(*box_formula_a_seq_b_ff); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_seq_b_ff, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -437,7 +452,8 @@ TEST_CASE("Translate tt", "[translate]") { auto tt = boolean(true); auto diamond_formula_a_tt = std::make_shared(regex_star_a, tt); - auto *my_dfa = to_dfa(*diamond_formula_a_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula_a_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -462,7 +478,8 @@ TEST_CASE("Translate {a*}tt", "[translate]") { auto tt = boolean(true); auto box_formula_a_star_tt = std::make_shared(regex_star_a, tt); - auto *my_dfa = to_dfa(*box_formula_a_star_tt); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*box_formula_a_star_tt, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); @@ -491,7 +508,8 @@ TEST_CASE("Translate tt", "[translate]") { auto tt = boolean(true); auto diamond_formula = std::make_shared(regex_seq, tt); - auto *my_dfa = to_dfa(*diamond_formula); + auto mgr = CUDD::Cudd(); + auto my_dfa = to_dfa(*diamond_formula, mgr); // print the DFA dfa_to_graphviz(*my_dfa, "translate_output_" + formula_name + ".svg", "svg"); diff --git a/scripts/_ci-bench.sh b/scripts/_ci-bench.sh new file mode 100755 index 00000000..e3acb64a --- /dev/null +++ b/scripts/_ci-bench.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +cd build && make lydia-benchmark diff --git a/scripts/_ci-test.sh b/scripts/_ci-test.sh index 3aea8aea..8e29258b 100755 --- a/scripts/_ci-test.sh +++ b/scripts/_ci-test.sh @@ -8,4 +8,3 @@ cd .. echo "========== Code coverage ==========" gcovr -r . -e "third_party/*" --print-summary --html --html-details -o coverage.html gcovr -r . -e "third_party/*" --xml -o coverage.xml - diff --git a/scripts/benchmark.sh b/scripts/benchmark.sh new file mode 100755 index 00000000..6613bcf5 --- /dev/null +++ b/scripts/benchmark.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +# Call this after ./scripts/build.sh +cd build && make lydia-benchmark && cd .. diff --git a/scripts/build-dev.sh b/scripts/build-dev.sh index f29babf9..e20e6173 100755 --- a/scripts/build-dev.sh +++ b/scripts/build-dev.sh @@ -7,7 +7,7 @@ BUILD_DIR=build mkdir -p ${BUILD_DIR} && cd ${BUILD_DIR} && rm -rf ./* # Configure compiler build with coverage flas -cmake .. -DENABLE_COVERAGE=ON +cmake .. -DCMAKE_BUILD_TYPE=Debug # compiler will generate *.gcno files for each compiled object # running tests will generate *.gcda for each compiled object # excuted partially or entirely by tests diff --git a/scripts/build.sh b/scripts/build.sh index ec7bc09d..c6c93b91 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -3,5 +3,7 @@ set -e mkdir -p ./build && cd ./build && rm -rf ./* -cmake .. -make -j "$@" +cmake .. -DCMAKE_BUILD_TYPE=Release +cmake --build . --config Release -j "$@" + +cd .. \ No newline at end of file diff --git a/third_party/CMakeLists.txt b/third_party/CMakeLists.txt index 64e39f98..d3aeacca 100644 --- a/third_party/CMakeLists.txt +++ b/third_party/CMakeLists.txt @@ -30,6 +30,18 @@ set (CATCH_INCLUDE_PATH "${CATCH_MODULE_PATH}/single_include/catch2") #include custom cmake function include ( "${CATCH_MODULE_PATH}/contrib/ParseAndAddCatchTests.cmake") +# ------------------------------------------------------------------------- +# google/benchmark + +#configure directories +set (GOOGLE_BENCHMARK_MODULE_PATH "${THIRD_PARTY_MODULE_PATH}/google/benchmark") +set (GOOGLE_BENCHMARK_INCLUDE_PATH "${GOOGLE_BENCHMARK_MODULE_PATH}/include") +set(BENCHMARK_ENABLE_GTEST_TESTS OFF) +add_subdirectory(${GOOGLE_BENCHMARK_MODULE_PATH}) + +#include custom cmake function +include ( "${CATCH_MODULE_PATH}/contrib/ParseAndAddCatchTests.cmake") + # ------------------------------------------------------------------------- # spdlog @@ -57,6 +69,15 @@ set (CLI11_INCLUDE_PATH "${CLI11_MODULE_PATH}/include") # ------------------------------------------------------------------------- +# ------------------------------------------------------------------------- +# cpphoafparser + +#configure directories +set (CPPHOAFPARSER_MODULE_PATH "${THIRD_PARTY_MODULE_PATH}/cpphoafparser") +set (CPPHOAFPARSER_INCLUDE_PATH "${CPPHOAFPARSER_MODULE_PATH}/include") + +# ------------------------------------------------------------------------- + # ------------------------------------------------------------------------- # CUDD @@ -66,7 +87,7 @@ set (CUDD_INCLUDE_PATH ${CUDD_INCLUDE_DIRS}) # ------------------------------------------------------------------------- #set variables -set (THIRD_PARTY_INCLUDE_PATH ${FMT_INCLUDE_PATH} ${SPDLOG_INCLUDE_PATH} ${CLI11_INCLUDE_PATH} ${CUDD_INCLUDE_PATH}) +set (THIRD_PARTY_INCLUDE_PATH ${FMT_INCLUDE_PATH} ${SPDLOG_INCLUDE_PATH} ${CLI11_INCLUDE_PATH} ${CPPHOAFPARSER_INCLUDE_PATH} ${CUDD_INCLUDE_PATH} ${GOOGLE_BENCHMARK_INCLUDE_PATH}) #set variables for tests set (TEST_THIRD_PARTY_INCLUDE_PATH ${CATCH_INCLUDE_PATH}) diff --git a/third_party/cpphoafparser b/third_party/cpphoafparser new file mode 160000 index 00000000..66da04ba --- /dev/null +++ b/third_party/cpphoafparser @@ -0,0 +1 @@ +Subproject commit 66da04bafb62376f4474492863fbb67450769dc7 diff --git a/third_party/google/benchmark b/third_party/google/benchmark new file mode 160000 index 00000000..56898e9a --- /dev/null +++ b/third_party/google/benchmark @@ -0,0 +1 @@ +Subproject commit 56898e9a92fba537671d5462df9c5ef2ea6a823a