From a65b42a046a07db3c7d572806ec969842de7b57c Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Mon, 27 Apr 2020 14:17:06 +0200 Subject: [PATCH 1/9] add google benchmark framework --- .gitmodules | 3 +++ third_party/google/benchmark | 1 + 2 files changed, 4 insertions(+) create mode 160000 third_party/google/benchmark diff --git a/.gitmodules b/.gitmodules index 4605afa7..d6aabe1a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -13,3 +13,6 @@ [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 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 From 9f3ae4d21c68eb4c41091fc2f6135222433aa249 Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Mon, 27 Apr 2020 18:12:18 +0200 Subject: [PATCH 2/9] add benchmark in CI and build --- .github/workflows/build_cmake.yml | 3 +++ lib/CMakeLists.txt | 1 + lib/benchmark/CMakeLists.txt | 39 +++++++++++++++++++++++++++++++ lib/benchmark/src/main.cpp | 35 +++++++++++++++++++++++++++ scripts/_ci-bench.sh | 5 ++++ scripts/_ci-test.sh | 1 - scripts/build-dev.sh | 3 +++ third_party/CMakeLists.txt | 14 ++++++++++- 8 files changed, 99 insertions(+), 2 deletions(-) create mode 100644 lib/benchmark/CMakeLists.txt create mode 100644 lib/benchmark/src/main.cpp create mode 100755 scripts/_ci-bench.sh 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/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..aa309927 --- /dev/null +++ b/lib/benchmark/CMakeLists.txt @@ -0,0 +1,39 @@ +# +# 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}) diff --git a/lib/benchmark/src/main.cpp b/lib/benchmark/src/main.cpp new file mode 100644 index 00000000..336a0179 --- /dev/null +++ b/lib/benchmark/src/main.cpp @@ -0,0 +1,35 @@ +/* + * 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 + +static void BM_StringCreation(benchmark::State &state) { + for (auto _ : state) + std::string empty_string; +} +// Register the function as a benchmark +BENCHMARK(BM_StringCreation); + +// Define another benchmark +static void BM_StringCopy(benchmark::State &state) { + std::string x = "hello"; + for (auto _ : state) + std::string copy(x); +} +BENCHMARK(BM_StringCopy); + +BENCHMARK_MAIN(); \ No newline at end of file diff --git a/scripts/_ci-bench.sh b/scripts/_ci-bench.sh new file mode 100755 index 00000000..68a1b5c0 --- /dev/null +++ b/scripts/_ci-bench.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +cd build && ./bin/lydiaBench 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/build-dev.sh b/scripts/build-dev.sh index f29babf9..79617721 100755 --- a/scripts/build-dev.sh +++ b/scripts/build-dev.sh @@ -19,3 +19,6 @@ 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 + +echo "========== Benchmark ==========" +./build/bin/lydiaBench diff --git a/third_party/CMakeLists.txt b/third_party/CMakeLists.txt index 64e39f98..5fd3adc4 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 @@ -66,7 +78,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} ${CUDD_INCLUDE_PATH} ${GOOGLE_BENCHMARK_INCLUDE_PATH}) #set variables for tests set (TEST_THIRD_PARTY_INCLUDE_PATH ${CATCH_INCLUDE_PATH}) From 4f615d1e6eee34493230ae9fc24590e3f940aaeb Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Mon, 27 Apr 2020 20:03:27 +0200 Subject: [PATCH 3/9] add benchmark as cmake target --- CMakeLists.txt | 22 +++++++++++++--------- README.md | 6 +++++- lib/benchmark/CMakeLists.txt | 5 +++++ scripts/_ci-bench.sh | 2 +- scripts/benchmark.sh | 4 ++++ scripts/build-dev.sh | 5 +---- scripts/build.sh | 6 ++++-- 7 files changed, 33 insertions(+), 17 deletions(-) create mode 100755 scripts/benchmark.sh diff --git a/CMakeLists.txt b/CMakeLists.txt index 7901167c..307dd70d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -27,10 +27,23 @@ 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' at some point +set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic") + +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() + # TODO include this eventually #set(CMAKE_CXX_CLANG_TIDY # clang-tidy; @@ -48,15 +61,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/lib/benchmark/CMakeLists.txt b/lib/benchmark/CMakeLists.txt index aa309927..3109ca69 100644 --- a/lib/benchmark/CMakeLists.txt +++ b/lib/benchmark/CMakeLists.txt @@ -37,3 +37,8 @@ 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/scripts/_ci-bench.sh b/scripts/_ci-bench.sh index 68a1b5c0..e3acb64a 100755 --- a/scripts/_ci-bench.sh +++ b/scripts/_ci-bench.sh @@ -2,4 +2,4 @@ set -e -cd build && ./bin/lydiaBench +cd build && make lydia-benchmark 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 79617721..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 @@ -19,6 +19,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 - -echo "========== Benchmark ==========" -./build/bin/lydiaBench 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 From 1c6b940ff4eceb29fbb942a64e20866bf5ab0afa Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Tue, 28 Apr 2020 01:21:16 +0200 Subject: [PATCH 4/9] add first microbenchmarks --- CMakeLists.txt | 10 +++- lib/benchmark/src/dfa.cpp | 46 ++++++++++++++++ lib/benchmark/src/logic.cpp | 96 +++++++++++++++++++++++++++++++++ lib/benchmark/src/main.cpp | 17 +----- lib/benchmark/src/translate.cpp | 53 ++++++++++++++++++ lib/include/translate.hpp | 3 +- lib/include/utils/benchmark.hpp | 21 ++++++++ lib/src/translate.cpp | 8 ++- 8 files changed, 234 insertions(+), 20 deletions(-) create mode 100644 lib/benchmark/src/dfa.cpp create mode 100644 lib/benchmark/src/logic.cpp create mode 100644 lib/benchmark/src/translate.cpp create mode 100644 lib/include/utils/benchmark.hpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 307dd70d..0c8089ab 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -33,9 +33,13 @@ set (CMAKE_CXX_STANDARD 17) set (CMAKE_CXX_STANDARD_REQUIRED ON) set(CMAKE_EXPORT_COMPILE_COMMANDS ON) -# TODO introduce '-Werror' at some point +# 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") @@ -44,6 +48,10 @@ if (CMAKE_BUILD_TYPE EQUAL "Debug" AND ENABLE_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; diff --git a/lib/benchmark/src/dfa.cpp b/lib/benchmark/src/dfa.cpp new file mode 100644 index 00000000..29fdb4af --- /dev/null +++ b/lib/benchmark/src/dfa.cpp @@ -0,0 +1,46 @@ +/* + * 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 = new 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 + auto mgr = new CUDD::Cudd(); + for (auto _ : state) { + auto my_dfa = new 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 index 336a0179..8ea9ade9 100644 --- a/lib/benchmark/src/main.cpp +++ b/lib/benchmark/src/main.cpp @@ -17,19 +17,4 @@ #include -static void BM_StringCreation(benchmark::State &state) { - for (auto _ : state) - std::string empty_string; -} -// Register the function as a benchmark -BENCHMARK(BM_StringCreation); - -// Define another benchmark -static void BM_StringCopy(benchmark::State &state) { - std::string x = "hello"; - for (auto _ : state) - std::string copy(x); -} -BENCHMARK(BM_StringCopy); - -BENCHMARK_MAIN(); \ No newline at end of file +BENCHMARK_MAIN(); diff --git a/lib/benchmark/src/translate.cpp b/lib/benchmark/src/translate.cpp new file mode 100644 index 00000000..e41f7e49 --- /dev/null +++ b/lib/benchmark/src/translate.cpp @@ -0,0 +1,53 @@ +/* + * 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 = new CUDD::Cudd(); + 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 = new CUDD::Cudd(); + 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); + +} // namespace whitemech::lydia::Benchmark diff --git a/lib/include/translate.hpp b/lib/include/translate.hpp index e37b1e4b..4f2c5dba 100644 --- a/lib/include/translate.hpp +++ b/lib/include/translate.hpp @@ -35,7 +35,8 @@ namespace lydia { * @param formula the LDLf formula. * @return the equivalent DFA. */ -dfa *to_dfa(LDLfFormula &formula); +dfa *to_dfa(const LDLfFormula &formula, CUDD::Cudd *mgr); +dfa *to_dfa(const LDLfFormula &formula); /*! * 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..75f5f43b --- /dev/null +++ b/lib/include/utils/benchmark.hpp @@ -0,0 +1,21 @@ +#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 . + */ + +static void escape(void *p) { asm volatile("" : : "g"(p) : "memory"); } + +static void clobber() { asm volatile("" : : : "memory"); } diff --git a/lib/src/translate.cpp b/lib/src/translate.cpp index e433e2c9..ae1c4578 100644 --- a/lib/src/translate.cpp +++ b/lib/src/translate.cpp @@ -27,7 +27,11 @@ namespace whitemech { namespace lydia { -dfa *to_dfa(LDLfFormula &formula) { +dfa *to_dfa(const LDLfFormula &formula) { + return to_dfa(formula, new CUDD::Cudd()); +} + +dfa *to_dfa(const LDLfFormula &formula, CUDD::Cudd *mgr) { // build initial state of the DFA. auto formula_nnf = to_nnf(formula); set_formulas initial_state_formulas{formula_nnf}; @@ -43,7 +47,7 @@ dfa *to_dfa(LDLfFormula &formula) { auto all_interpretations = powerset(atoms); // TODO max number of bits - dfa *automaton = new dfa(10, atoms.size()); + dfa *automaton = new dfa(mgr, 10, atoms.size()); automaton->add_state(); automaton->set_initial_state(1); From 4863c5d2bf4aaac06185462a320e7c36869d8dac Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Tue, 28 Apr 2020 15:53:58 +0200 Subject: [PATCH 5/9] pass CUDD manager as reference for DFA construction. --- app/mona2sym/src/main.cpp | 15 +-- lib/benchmark/src/dfa.cpp | 7 +- lib/benchmark/src/translate.cpp | 14 +-- lib/include/dfa.hpp | 52 ++++----- lib/include/translate.hpp | 3 +- lib/include/utils/benchmark.hpp | 3 + lib/src/dfa.cpp | 50 +++++---- lib/src/translate.cpp | 8 +- lib/test/src/test_dfa.cpp | 186 ++++++++++++++++---------------- lib/test/src/test_misc.cpp | 14 +-- lib/test/src/test_translate.cpp | 54 ++++++---- 11 files changed, 206 insertions(+), 200 deletions(-) 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/benchmark/src/dfa.cpp b/lib/benchmark/src/dfa.cpp index 29fdb4af..84d42700 100644 --- a/lib/benchmark/src/dfa.cpp +++ b/lib/benchmark/src/dfa.cpp @@ -25,7 +25,7 @@ namespace whitemech::lydia::Benchmark { static void BM_cudd_manager_instantiation(benchmark::State &state) { for (auto _ : state) { - auto mgr = new CUDD::Cudd(); + auto mgr = CUDD::Cudd(); escape(&mgr); (void)mgr; } @@ -34,9 +34,10 @@ 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 - auto mgr = new CUDD::Cudd(); + // preallocate + auto mgr = CUDD::Cudd(); for (auto _ : state) { - auto my_dfa = new dfa(mgr, 1, 1); + auto my_dfa = dfa(mgr, 1, 1); escape(&my_dfa); (void)my_dfa; } diff --git a/lib/benchmark/src/translate.cpp b/lib/benchmark/src/translate.cpp index e41f7e49..0ca903ae 100644 --- a/lib/benchmark/src/translate.cpp +++ b/lib/benchmark/src/translate.cpp @@ -25,29 +25,31 @@ 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 = new CUDD::Cudd(); + 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); + escape(&my_dfa); (void)my_dfa; } } -// BENCHMARK(BM_translate_boolean); +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 = new CUDD::Cudd(); + 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); + escape(&my_dfa); (void)my_dfa; } } -// BENCHMARK(BM_translate_diamond); +BENCHMARK(BM_translate_diamond); } // namespace whitemech::lydia::Benchmark diff --git a/lib/include/dfa.hpp b/lib/include/dfa.hpp index 2b2251f2..c6d1c820 100644 --- a/lib/include/dfa.hpp +++ b/lib/include/dfa.hpp @@ -38,11 +38,28 @@ 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; dfa &operator=(dfa &&) = delete; + ~dfa(); + /*! * Initialize the DFA from scratch. * @@ -67,8 +84,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 +107,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 +134,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 +145,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 4f2c5dba..563f3c8b 100644 --- a/lib/include/translate.hpp +++ b/lib/include/translate.hpp @@ -35,8 +35,7 @@ namespace lydia { * @param formula the LDLf formula. * @return the equivalent DFA. */ -dfa *to_dfa(const LDLfFormula &formula, CUDD::Cudd *mgr); -dfa *to_dfa(const 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 index 75f5f43b..1b3a5ba0 100644 --- a/lib/include/utils/benchmark.hpp +++ b/lib/include/utils/benchmark.hpp @@ -19,3 +19,6 @@ 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; diff --git a/lib/src/dfa.cpp b/lib/src/dfa.cpp index c87a340a..0fe12889 100644 --- a/lib/src/dfa.cpp +++ b/lib/src/dfa.cpp @@ -26,28 +26,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 +64,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 +89,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 +113,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 +122,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 +146,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 +189,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 +282,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 +325,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; */ @@ -452,5 +444,11 @@ bool dfa::is_final(int state) const { return finalstatesBDD.Eval(state_as_binary_vect.data()).IsOne(); } +dfa::~dfa() { + for (const auto &var : bddvars) { + Cudd_Deref(var.getNode()); + } +} + } // namespace lydia } // namespace whitemech diff --git a/lib/src/translate.cpp b/lib/src/translate.cpp index ae1c4578..439a5ede 100644 --- a/lib/src/translate.cpp +++ b/lib/src/translate.cpp @@ -27,11 +27,7 @@ namespace whitemech { namespace lydia { -dfa *to_dfa(const LDLfFormula &formula) { - return to_dfa(formula, new CUDD::Cudd()); -} - -dfa *to_dfa(const LDLfFormula &formula, CUDD::Cudd *mgr) { +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}; @@ -47,7 +43,7 @@ dfa *to_dfa(const LDLfFormula &formula, CUDD::Cudd *mgr) { auto all_interpretations = powerset(atoms); // TODO max number of bits - dfa *automaton = new dfa(mgr, 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/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..913a6f25 100644 --- a/lib/test/src/test_misc.cpp +++ b/lib/test/src/test_misc.cpp @@ -60,15 +60,15 @@ 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"); } } // 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"); From 883fbc1852bc803d21d1de99d95780e4c17e7dd7 Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Tue, 28 Apr 2020 19:51:10 +0200 Subject: [PATCH 6/9] add scalability benchmark on number of propositions for seq and union regex. --- lib/benchmark/src/translate.cpp | 46 +++++++++++++++++++++++++++++++++ lib/include/dfa.hpp | 2 -- lib/include/utils/benchmark.hpp | 35 +++++++++++++++++++++++++ lib/src/dfa.cpp | 7 ----- lib/test/src/test_translate.cpp | 22 ++++++++++++++++ 5 files changed, 103 insertions(+), 9 deletions(-) diff --git a/lib/benchmark/src/translate.cpp b/lib/benchmark/src/translate.cpp index 0ca903ae..523cf0d6 100644 --- a/lib/benchmark/src/translate.cpp +++ b/lib/benchmark/src/translate.cpp @@ -52,4 +52,50 @@ static void BM_translate_diamond(benchmark::State &state) { } 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 c6d1c820..6822d0fb 100644 --- a/lib/include/dfa.hpp +++ b/lib/include/dfa.hpp @@ -58,8 +58,6 @@ class dfa { dfa(dfa &&) = delete; dfa &operator=(dfa &&) = delete; - ~dfa(); - /*! * Initialize the DFA from scratch. * diff --git a/lib/include/utils/benchmark.hpp b/lib/include/utils/benchmark.hpp index 1b3a5ba0..db8ee340 100644 --- a/lib/include/utils/benchmark.hpp +++ b/lib/include/utils/benchmark.hpp @@ -16,9 +16,44 @@ * 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/src/dfa.cpp b/lib/src/dfa.cpp index 0fe12889..f3240bf1 100644 --- a/lib/src/dfa.cpp +++ b/lib/src/dfa.cpp @@ -17,7 +17,6 @@ #include "dfa.hpp" #include -#include #include #include @@ -444,11 +443,5 @@ bool dfa::is_final(int state) const { return finalstatesBDD.Eval(state_as_binary_vect.data()).IsOne(); } -dfa::~dfa() { - for (const auto &var : bddvars) { - Cudd_Deref(var.getNode()); - } -} - } // namespace lydia } // namespace whitemech diff --git a/lib/test/src/test_translate.cpp b/lib/test/src/test_translate.cpp index 1beb0b0f..054fa30d 100644 --- a/lib/test/src/test_translate.cpp +++ b/lib/test/src/test_translate.cpp @@ -531,4 +531,26 @@ TEST_CASE("Translate tt", "[translate]") { REQUIRE(my_dfa->accepts(trace{a_, b_, e})); } +TEST_CASE("translate_sequence", "[translate]") { + auto mgr = CUDD::Cudd(); + std::string alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"; + auto tt = boolean(true); + auto true_ = std::make_shared(); + auto a = std::make_shared("a"); + auto regex_true = std::make_shared(true_); + auto regex_a = std::make_shared(a); + auto N = 2; + 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); + } + auto regex_seq = std::make_shared(vregex); + auto diamond_formula = std::make_shared(regex_seq, tt); + auto my_dfa = to_dfa(*diamond_formula, mgr); +} + } // namespace whitemech::lydia::Test \ No newline at end of file From 6d5943a962fbd46cc654d64c38314e120bbc372c Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Tue, 28 Apr 2020 22:30:50 +0200 Subject: [PATCH 7/9] remove temporary test. --- lib/test/src/test_translate.cpp | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/lib/test/src/test_translate.cpp b/lib/test/src/test_translate.cpp index 054fa30d..1beb0b0f 100644 --- a/lib/test/src/test_translate.cpp +++ b/lib/test/src/test_translate.cpp @@ -531,26 +531,4 @@ TEST_CASE("Translate tt", "[translate]") { REQUIRE(my_dfa->accepts(trace{a_, b_, e})); } -TEST_CASE("translate_sequence", "[translate]") { - auto mgr = CUDD::Cudd(); - std::string alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"; - auto tt = boolean(true); - auto true_ = std::make_shared(); - auto a = std::make_shared("a"); - auto regex_true = std::make_shared(true_); - auto regex_a = std::make_shared(a); - auto N = 2; - 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); - } - auto regex_seq = std::make_shared(vregex); - auto diamond_formula = std::make_shared(regex_seq, tt); - auto my_dfa = to_dfa(*diamond_formula, mgr); -} - } // namespace whitemech::lydia::Test \ No newline at end of file From 1c47568629ecf1f1e1f9984517298800b3a9b4de Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Tue, 28 Apr 2020 23:24:16 +0200 Subject: [PATCH 8/9] add cpphoafparser in third_party --- .gitmodules | 3 +++ third_party/cpphoafparser | 1 + 2 files changed, 4 insertions(+) create mode 160000 third_party/cpphoafparser diff --git a/.gitmodules b/.gitmodules index d6aabe1a..e7bdb7f7 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,3 +16,6 @@ [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/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 From b03bcb4133a12ba637b03a831e5b5d20a53decaf Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Wed, 29 Apr 2020 01:03:09 +0200 Subject: [PATCH 9/9] complete DFA to HOA, header --- lib/include/utils/dfa_transform.hpp | 4 +++- lib/src/utils/dfa_transform.cpp | 28 ++++++++++++++++++++++++++++ lib/test/src/test_misc.cpp | 18 ++++++++++++++++++ third_party/CMakeLists.txt | 11 ++++++++++- 4 files changed, 59 insertions(+), 2 deletions(-) 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/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_misc.cpp b/lib/test/src/test_misc.cpp index 913a6f25..0925bff1 100644 --- a/lib/test/src/test_misc.cpp +++ b/lib/test/src/test_misc.cpp @@ -71,4 +71,22 @@ TEST_CASE("DFA to Graphviz", "[dfa_transform]") { 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/third_party/CMakeLists.txt b/third_party/CMakeLists.txt index 5fd3adc4..d3aeacca 100644 --- a/third_party/CMakeLists.txt +++ b/third_party/CMakeLists.txt @@ -69,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 @@ -78,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} ${GOOGLE_BENCHMARK_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})