From 21b3ce50933c28ccf8db1368c10c8c0ea3ba31b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Thu, 11 Dec 2025 18:34:26 +0300 Subject: [PATCH 1/6] implemented discrete with double buffer interval set and wrote simple tests --- .gitignore | 3 + benchmarks/benchmark_engine.cpp | 226 +++++++++++----------- include/do-verify/MTLEngine.hpp | 91 ++++++++- include/do-verify/binary_row_reader.hpp | 2 +- include/do-verify/interval_set.hpp | 26 ++- include/do-verify/json_reader.hpp | 2 +- tests/CMakeLists.txt | 1 + tests/test_dense.cpp | 246 ++++++++++++------------ tests/test_discrete.cpp | 92 +++++++++ 9 files changed, 444 insertions(+), 245 deletions(-) create mode 100644 tests/test_discrete.cpp diff --git a/.gitignore b/.gitignore index 25cacf1..bca5fb4 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ data/* build/ .vscode/ +misc/ +debugger +debugger.cpp *Zone.Identifier diff --git a/benchmarks/benchmark_engine.cpp b/benchmarks/benchmark_engine.cpp index cc732c7..f98a9b2 100644 --- a/benchmarks/benchmark_engine.cpp +++ b/benchmarks/benchmark_engine.cpp @@ -33,7 +33,7 @@ class InputCache { TEST_CASE("Dense AbsentAQ", "[dense_benchmarks][AbsentAQ]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; // --- 1. SETUP PARAMS --- @@ -58,14 +58,14 @@ TEST_CASE("Dense AbsentAQ", "[dense_benchmarks][AbsentAQ]") { BENCHMARK_ADVANCED("AbsentAQ " + benchmarkName)(Catch::Benchmark::Chronometer meter) { IntervalSetHolder holder = newHolder(1000); - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY}; - Node implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; - std::vector nodes{q, p, once, notNode, since, implies, always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DenseNode implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; + DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; std::string file_name = "data/fullsuite/AbsentAQ/" + CONDENSATION + "/1M/AbsentAQ" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -89,7 +89,7 @@ TEST_CASE("Dense AbsentAQ", "[dense_benchmarks][AbsentAQ]") { TEST_CASE("Dense AbsentBQR", "[dense_benchmarks][AbsentBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; // --- 1. SETUP PARAMS --- auto params = GENERATE(table({ @@ -116,19 +116,19 @@ TEST_CASE("Dense AbsentBQR", "[dense_benchmarks][AbsentBQR]") { const int since_a = 3 * (TIMINGS / 10); const int since_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 7 - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, since_a, since_b}; // 8 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // 9 - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // 10 + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 7 + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, since_a, since_b}; // 8 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // 9 + DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // 10 - std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; std::string file_name = "data/fullsuite/AbsentBQR/" + CONDENSATION + "/1M/AbsentBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -151,7 +151,7 @@ TEST_CASE("Dense AbsentBQR", "[dense_benchmarks][AbsentBQR]") { TEST_CASE("Dense AbsentBR", "[dense_benchmarks][AbsentBR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -170,15 +170,15 @@ TEST_CASE("Dense AbsentBR", "[dense_benchmarks][AbsentBR]") { const int inner_always_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 3 - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; // 4 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; // 5 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // 6 + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 3 + DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; // 4 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; // 5 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // 6 - std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; std::string file_name = "data/fullsuite/AbsentBR/" + CONDENSATION + "/1M/AbsentBR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -201,7 +201,7 @@ TEST_CASE("Dense AbsentBR", "[dense_benchmarks][AbsentBR]") { TEST_CASE("Dense AlwaysAQ", "[dense_benchmarks][AlwaysAQ]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -220,15 +220,15 @@ TEST_CASE("Dense AlwaysAQ", "[dense_benchmarks][AlwaysAQ]") { const int once_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; // 3 - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; // 4 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; // 5 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // 6 + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; // 3 + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; // 4 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; // 5 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // 6 - std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; std::string file_name = "data/fullsuite/AlwaysAQ/" + CONDENSATION + "/1M/AlwaysAQ" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -251,7 +251,7 @@ TEST_CASE("Dense AlwaysAQ", "[dense_benchmarks][AlwaysAQ]") { TEST_CASE("Dense AlwaysBQR", "[dense_benchmarks][AlwaysBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -271,19 +271,19 @@ TEST_CASE("Dense AlwaysBQR", "[dense_benchmarks][AlwaysBQR]") { const int since_a = 3 * (TIMINGS / 10); const int since_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 7 - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, since_a, since_b}; // 8 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // 9 - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // 10 + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 7 + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, since_a, since_b}; // 8 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // 9 + DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // 10 - std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; std::string file_name = "data/fullsuite/AlwaysBQR/" + CONDENSATION + "/1M/AlwaysBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -306,7 +306,7 @@ TEST_CASE("Dense AlwaysBQR", "[dense_benchmarks][AlwaysBQR]") { TEST_CASE("Dense AlwaysBR", "[dense_benchmarks][AlwaysBR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -325,14 +325,14 @@ TEST_CASE("Dense AlwaysBR", "[dense_benchmarks][AlwaysBR]") { const int inner_always_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; // 3 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; // 4 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; // 5 + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; // 3 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; // 4 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; // 5 - std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; std::string file_name = "data/fullsuite/AlwaysBR/" + CONDENSATION + "/1M/AlwaysBR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -355,7 +355,7 @@ TEST_CASE("Dense AlwaysBR", "[dense_benchmarks][AlwaysBR]") { TEST_CASE("Dense RecurBQR", "[dense_benchmarks][RecurBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -374,20 +374,20 @@ TEST_CASE("Dense RecurBQR", "[dense_benchmarks][RecurBQR]") { const int inner_once_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 - Node p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0}; // 7 - Node once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; // 8 - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY}; // 9 - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0}; // 10 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; // 11 - - std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 3 + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 4 + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // 5 + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // 6 + DenseNode p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0}; // 7 + DenseNode once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; // 8 + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY}; // 9 + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0}; // 10 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; // 11 + + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; std::string file_name = "data/fullsuite/RecurBQR/" + CONDENSATION + "/1M/RecurBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -412,7 +412,7 @@ TEST_CASE("Dense RecurBQR", "[dense_benchmarks][RecurBQR]") { TEST_CASE("Dense RecurGLB", "[dense_benchmarks][RecurGLB]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -428,10 +428,10 @@ TEST_CASE("Dense RecurGLB", "[dense_benchmarks][RecurGLB]") { BENCHMARK_ADVANCED("RecurGLB " + benchmarkName)(Catch::Benchmark::Chronometer meter) { IntervalSetHolder holder = newHolder(1000); - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; - std::vector nodes{p, once, always}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; std::string file_name = "data/fullsuite/RecurGLB/" + CONDENSATION + "/1M/RecurGLB" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -456,7 +456,7 @@ TEST_CASE("Dense RecurGLB", "[dense_benchmarks][RecurGLB]") { TEST_CASE("Dense RespondBQR", "[dense_benchmarks][RespondBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -477,25 +477,25 @@ TEST_CASE("Dense RespondBQR", "[dense_benchmarks][RespondBQR]") { const int once_b = TIMINGS; const int since_a = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 3 - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 4 - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 5 - Node and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; // 6 - Node and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0}; // 7 - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, once_a, once_b}; // 8 - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0}; // 9 - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0}; // 10 - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, since_a, B_INFINITY}; // 11 - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0}; // 12 - Node and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0}; // 13 - Node since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY}; // 14 - Node implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0}; // 15 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; // 16 - - std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 2 + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 3 + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // 4 + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // 5 + DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; // 6 + DenseNode and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0}; // 7 + DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, once_a, once_b}; // 8 + DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0}; // 9 + DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0}; // 10 + DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, since_a, B_INFINITY}; // 11 + DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0}; // 12 + DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0}; // 13 + DenseNode since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY}; // 14 + DenseNode implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0}; // 15 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; // 16 + + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; std::string file_name = "data/fullsuite/RespondBQR/" + CONDENSATION + "/1M/RespondBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); @@ -519,7 +519,7 @@ TEST_CASE("Dense RespondBQR", "[dense_benchmarks][RespondBQR]") { TEST_CASE("Dense RespondGLB", "[dense_benchmarks][RespondGLB]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -540,17 +540,17 @@ TEST_CASE("Dense RespondGLB", "[dense_benchmarks][RespondGLB]") { const int once_b = TIMINGS; const int since_a = TIMINGS; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; // 2 - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; // 3 - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 4 - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, since_a, B_INFINITY}; // 5 - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0}; // 6 - Node and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0}; // 7 - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; // 8 - - std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 0 + DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // 1 + DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; // 2 + DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; // 3 + DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // 4 + DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, since_a, B_INFINITY}; // 5 + DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0}; // 6 + DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0}; // 7 + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; // 8 + + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; std::string file_name = "data/fullsuite/RespondGLB/" + CONDENSATION + "/1M/RespondGLB" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = InputCache::get(file_name); diff --git a/include/do-verify/MTLEngine.hpp b/include/do-verify/MTLEngine.hpp index 6bf0d0a..6bd4b89 100644 --- a/include/do-verify/MTLEngine.hpp +++ b/include/do-verify/MTLEngine.hpp @@ -7,7 +7,7 @@ #define B_INFINITY std::numeric_limits::max() -namespace dense_vector { +namespace do_verify { enum class NodeType { PROPOSITION, @@ -21,7 +21,7 @@ enum class NodeType { TEST, }; -struct Node { +struct DenseNode { db_interval_set::IntervalSet state; db_interval_set::IntervalSet output; NodeType type; @@ -40,9 +40,9 @@ inline int add_with_inf(int a, int b) { } }; -db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector &propositionInputs) { +inline db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector &propositionInputs) { for(int node_index = 0; node_index < nodes.size(); node_index++) { - Node &curNode = nodes[node_index]; + DenseNode &curNode = nodes[node_index]; switch (curNode.type) { // TODO hocaya sor: datada bir time ve true, false geldiği zaman o timeden önce mi öyle sonra mı? // timescales'de timeless'lar var nasıl implemente edicem @@ -165,4 +165,87 @@ db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interva } +struct DiscreteNode { + db_interval_set::IntervalSet state; + bool output; + NodeType type; + unsigned int leftOperandIndex; + unsigned int rightOperandIndex; + int a; + int b; +}; + + +inline bool run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector &propositionInputs) { + for (unsigned int node_index = 0; node_index < nodes.size(); node_index++) { + DiscreteNode &curNode = nodes[node_index]; + switch (curNode.type) + { + case NodeType::PROPOSITION: + curNode.output = propositionInputs[node_index]; + break; + case NodeType::AND: + curNode.output = nodes[curNode.leftOperandIndex].output && nodes[curNode.rightOperandIndex].output; + break; + case NodeType::OR: + curNode.output = nodes[curNode.leftOperandIndex].output || nodes[curNode.rightOperandIndex].output; + break; + case NodeType::NOT: + curNode.output = !nodes[curNode.rightOperandIndex].output; + break; + case NodeType::IMPLIES: + curNode.output = !(nodes[curNode.leftOperandIndex].output && !nodes[curNode.rightOperandIndex].output); + break; + case NodeType::EVENTUALLY: + { + if (nodes[curNode.rightOperandIndex].output) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + curNode.output = db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + + } + case NodeType::ALWAYS: + { + if (!nodes[curNode.rightOperandIndex].output) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + curNode.output = !db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + } + case NodeType::SINCE: + { + bool leftOutput = nodes[curNode.leftOperandIndex].output; + bool rightOutput = nodes[curNode.rightOperandIndex].output; + if (leftOutput && rightOutput) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + else if (!leftOutput && rightOutput) { + curNode.state = db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)}); + } + else if (leftOutput && !rightOutput) { + + } + else { + curNode.state = db_interval_set::empty(setHolder); + } + curNode.output = db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + } + } + } + return nodes[nodes.size() - 1].output; + +} + + } \ No newline at end of file diff --git a/include/do-verify/binary_row_reader.hpp b/include/do-verify/binary_row_reader.hpp index 63702bd..813d639 100644 --- a/include/do-verify/binary_row_reader.hpp +++ b/include/do-verify/binary_row_reader.hpp @@ -16,7 +16,7 @@ struct TimescalesInput { }; #pragma pack(pop) -std::vector readInputFile(std::string fileName) { +inline std::vector readInputFile(std::string fileName) { // 2. Open File // std::ios::ate is NOT used here because we need to read from the start diff --git a/include/do-verify/interval_set.hpp b/include/do-verify/interval_set.hpp index cb75ea9..9b0753a 100644 --- a/include/do-verify/interval_set.hpp +++ b/include/do-verify/interval_set.hpp @@ -21,9 +21,6 @@ struct Transition { bool isStart; // true = start of an interval, false = end of an interval }; -// timescalest dene -// dense implemente dene - struct IntervalSet { Transition *buffer; int startIndex; @@ -81,6 +78,29 @@ inline IntervalSet empty(IntervalSetHolder &holder) { return IntervalSet{holder.writeBuffer, 1, 0}; }; +/** + * @brief Checks if a single time point is contained within the interval set. + * Since intervals are [start, end), start is inclusive and end is exclusive. + * + * @param set The interval set to check. + * @param time The time point to query. + * @return true if the time point is in the set, false otherwise. + */ +inline bool includes(const IntervalSet& set, int time) { + bool state = false; + for (int i = set.startIndex; i <= set.endIndex; ++i) { + const Transition& t = set.buffer[i]; + if (t.time <= time) { + state = t.isStart; + } else { + break; // No need to check further transitions + } + } + return state; +} + + + /** * @brief Creates a new set from a single [start, end) interval. * This is the primary way to get data into the system. diff --git a/include/do-verify/json_reader.hpp b/include/do-verify/json_reader.hpp index d88c0c0..49ddae7 100644 --- a/include/do-verify/json_reader.hpp +++ b/include/do-verify/json_reader.hpp @@ -13,7 +13,7 @@ struct TimescalesInput { std::vector propositions; }; -TimescalesInput read_line(std::string &line) { +inline TimescalesInput read_line(std::string &line) { std::vector propositions; int time = 0; std::string segment; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 60ae7ab..748faea 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -65,6 +65,7 @@ endif() add_executable(unit_tests + test_discrete.cpp test_dense.cpp test_interval_set.cpp ) diff --git a/tests/test_dense.cpp b/tests/test_dense.cpp index d3de859..1f842c1 100644 --- a/tests/test_dense.cpp +++ b/tests/test_dense.cpp @@ -13,16 +13,16 @@ #include "do-verify/MTLEngine.hpp" TEST_CASE("Dense Implementation tests", "[dense]") { using namespace std; - using namespace dense_vector; + using namespace do_verify; using namespace db_interval_set; auto holder = newHolder(1000); - vector nodes; - auto p = Node{empty(holder), createSetFromIntervals(holder, {{7, 30}}), NodeType::TEST, 0, 0, 0, 0}; + vector nodes; + auto p = DenseNode{empty(holder), createSetFromIntervals(holder, {{7, 30}}), NodeType::TEST, 0, 0, 0, 0}; nodes.push_back(p); - auto q = Node{empty(holder), createSetFromIntervals(holder, {{3, 8}}), NodeType::TEST, 0, 0, 0, 0}; + auto q = DenseNode{empty(holder), createSetFromIntervals(holder, {{3, 8}}), NodeType::TEST, 0, 0, 0, 0}; nodes.push_back(q); - auto since = Node{empty(holder), empty(holder), NodeType::SINCE, 0, 1, 18, 24}; + auto since = DenseNode{empty(holder), empty(holder), NodeType::SINCE, 0, 1, 18, 24}; nodes.push_back(since); auto out = run_evaluation(nodes, holder, 0, 30, {true, true}); @@ -60,13 +60,13 @@ TEST_CASE("Dense Implementation tests", "[dense]") { TEST_CASE("Dense Timescales Tests", "[dense][old]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; IntervalSetHolder holder = newHolder(1000); - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; - std::vector nodes{p, once, always}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10}; + DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; std::ifstream input_file("data/fullsuite/RecurGLB/Dense10/1M/RecurGLB10.jsonl"); json_reader::TimescalesInput prevInput; @@ -100,7 +100,7 @@ TEST_CASE("Dense Timescales Tests", "[dense][old]") { TEST_CASE("Dense AbsentAQ", "[dense][AbsentAQ]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; // --- 1. SETUP PARAMS --- @@ -125,14 +125,14 @@ TEST_CASE("Dense AbsentAQ", "[dense][AbsentAQ]") { SECTION("AbsentAQ " + benchmarkName) { IntervalSetHolder holder = newHolder(1000); - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY}; - Node implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; - std::vector nodes{q, p, once, notNode, since, implies, always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DenseNode implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; + DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; std::string file_name = "data/fullsuite/AbsentAQ/" + CONDENSATION + "/1M/AbsentAQ" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -161,7 +161,7 @@ TEST_CASE("Dense AbsentAQ", "[dense][AbsentAQ]") { TEST_CASE("Dense AbsentBQR", "[dense][AbsentBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -181,19 +181,19 @@ TEST_CASE("Dense AbsentBQR", "[dense][AbsentBQR]") { const int since_a = 3 * (TIMINGS / 10); const int since_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, since_a, since_b}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, since_a, since_b}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; + DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; - std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; std::string file_name = "data/fullsuite/AbsentBQR/" + CONDENSATION + "/1M/AbsentBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -222,7 +222,7 @@ TEST_CASE("Dense AbsentBQR", "[dense][AbsentBQR]") { TEST_CASE("Dense AbsentBR", "[dense][AbsentBR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -241,15 +241,15 @@ TEST_CASE("Dense AbsentBR", "[dense][AbsentBR]") { const int inner_always_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; - std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; std::string file_name = "data/fullsuite/AbsentBR/" + CONDENSATION + "/1M/AbsentBR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -279,7 +279,7 @@ TEST_CASE("Dense AbsentBR", "[dense][AbsentBR]") { TEST_CASE("Dense AlwaysAQ", "[dense][AlwaysAQ]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -298,15 +298,15 @@ TEST_CASE("Dense AlwaysAQ", "[dense][AlwaysAQ]") { const int once_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; - std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; std::string file_name = "data/fullsuite/AlwaysAQ/" + CONDENSATION + "/1M/AlwaysAQ" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -335,7 +335,7 @@ TEST_CASE("Dense AlwaysAQ", "[dense][AlwaysAQ]") { TEST_CASE("Dense AlwaysBQR", "[dense][AlwaysBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -355,19 +355,19 @@ TEST_CASE("Dense AlwaysBQR", "[dense][AlwaysBQR]") { const int since_a = 3 * (TIMINGS / 10); const int since_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, since_a, since_b}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; + DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, since_a, since_b}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; + DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; - std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; std::string file_name = "data/fullsuite/AlwaysBQR/" + CONDENSATION + "/1M/AlwaysBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -396,7 +396,7 @@ TEST_CASE("Dense AlwaysBQR", "[dense][AlwaysBQR]") { TEST_CASE("Dense AlwaysBR", "[dense][AlwaysBR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -415,14 +415,14 @@ TEST_CASE("Dense AlwaysBR", "[dense][AlwaysBR]") { const int inner_always_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; - std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; std::string file_name = "data/fullsuite/AlwaysBR/" + CONDENSATION + "/1M/AlwaysBR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -451,7 +451,7 @@ TEST_CASE("Dense AlwaysBR", "[dense][AlwaysBR]") { TEST_CASE("Dense RecurBQR", "[dense][RecurBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -470,20 +470,20 @@ TEST_CASE("Dense RecurBQR", "[dense][RecurBQR]") { const int inner_once_b = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; - Node p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0}; - Node once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY}; - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; - - std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; + DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; + DenseNode p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0}; + DenseNode once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; + DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY}; + DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; + + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; std::string file_name = "data/fullsuite/RecurBQR/" + CONDENSATION + "/1M/RecurBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -510,7 +510,7 @@ TEST_CASE("Dense RecurBQR", "[dense][RecurBQR]") { TEST_CASE("Dense RecurGLB", "[dense][RecurGLB]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -526,10 +526,10 @@ TEST_CASE("Dense RecurGLB", "[dense][RecurGLB]") { SECTION("RecurGLB " + benchmarkName) { IntervalSetHolder holder = newHolder(1000); - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; - std::vector nodes{p, once, always}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; std::string file_name = "data/fullsuite/RecurGLB/" + CONDENSATION + "/1M/RecurGLB" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -557,7 +557,7 @@ TEST_CASE("Dense RecurGLB", "[dense][RecurGLB]") { TEST_CASE("Dense RespondBQR", "[dense][RespondBQR]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -579,25 +579,25 @@ TEST_CASE("Dense RespondBQR", "[dense][RespondBQR]") { const int once_b = TIMINGS; const int since_a = TIMINGS; - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; - Node and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; - Node and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0}; - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, once_a, once_b}; - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0}; - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0}; - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, since_a, B_INFINITY}; - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0}; - Node and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0}; - Node since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY}; - Node implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; - - std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; + DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; + DenseNode and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0}; + DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, once_a, once_b}; + DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0}; + DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0}; + DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, since_a, B_INFINITY}; + DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0}; + DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0}; + DenseNode since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY}; + DenseNode implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; + + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; std::string file_name = "data/fullsuite/RespondBQR/" + CONDENSATION + "/1M/RespondBQR" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); @@ -626,7 +626,7 @@ TEST_CASE("Dense RespondBQR", "[dense][RespondBQR]") { TEST_CASE("Dense RespondGLB", "[dense][RespondGLB]") { using namespace db_interval_set; - using namespace dense_vector; + using namespace do_verify; auto params = GENERATE(table({ {"Dense10", 10}, {"Dense100", 10}, {"Discrete", 10}, @@ -647,17 +647,17 @@ TEST_CASE("Dense RespondGLB", "[dense][RespondGLB]") { const int once_b = TIMINGS; const int since_a = TIMINGS; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, since_a, B_INFINITY}; - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0}; - Node and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0}; - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; - - std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; + DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; + DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; + DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; + DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, since_a, B_INFINITY}; + DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0}; + DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0}; + DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; + + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; std::string file_name = "data/fullsuite/RespondGLB/" + CONDENSATION + "/1M/RespondGLB" + std::to_string(TIMINGS) +".row.bin"; const auto& allInputs = binary_row_reader::readInputFile(file_name); diff --git a/tests/test_discrete.cpp b/tests/test_discrete.cpp new file mode 100644 index 0000000..ea79247 --- /dev/null +++ b/tests/test_discrete.cpp @@ -0,0 +1,92 @@ +#include +#include +#include + +#include +#include +#include +#include +#include "do-verify/json_reader.hpp" +#include "do-verify/binary_row_reader.hpp" + + +#include "do-verify/MTLEngine.hpp" + + +TEST_CASE("Discrete Implementation Tests", "[discrete]") { + + SECTION("2 Eventually") { + std::vector> propositionInputs = { + {true, false, false, false, false, false}, // p + {false, false, false, false, true, false} // q + }; + db_interval_set::IntervalSetHolder holder = db_interval_set::newHolder(1000); + std::vector expectedOutput = {false, false, true, true, true, false}; + std::vector nodes; + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::PROPOSITION, + 0, 0, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::PROPOSITION, + 0, 0, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::OR, + 0, 1, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::EVENTUALLY, + 0, 2, 1, 2}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::EVENTUALLY, + 0, 3, 1, 2}); + bool allCorrect = true; + for(int time = 0; time < propositionInputs[0].size(); time++) { + bool output = do_verify::run_evaluation(nodes, holder, time, {propositionInputs[0][time], propositionInputs[1][time]}); + allCorrect &= output == expectedOutput[time]; + db_interval_set::swapBuffers(holder); + } + db_interval_set::destroyHolder(holder); + REQUIRE(allCorrect == true); + + } + + + SECTION("Always") { + std::vector> propositionInputs = { + {false, false, true, true, true, false}, // p + }; + db_interval_set::IntervalSetHolder holder = db_interval_set::newHolder(1000); + std::vector expectedOutput = {true, false, false, false, true, true}; + std::vector nodes; + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::PROPOSITION, + 0, 0, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::ALWAYS, + 0, 0, 1, 2}); + bool allCorrect = true; + for(int time = 0; time < propositionInputs[0].size(); time++) { + bool output = do_verify::run_evaluation(nodes, holder, time, {propositionInputs[0][time]}); + allCorrect &= output == expectedOutput[time]; + db_interval_set::swapBuffers(holder); + } + db_interval_set::destroyHolder(holder); + REQUIRE(allCorrect == true); + } + + SECTION("Since") { + std::vector> propositionInputs = { + {false, false, true, true, true, false}, // p + {false, true, false, false, true, false}, // q + }; + db_interval_set::IntervalSetHolder holder = db_interval_set::newHolder(1000); + std::vector expectedOutput = {false, false, false, true, true, false}; + std::vector nodes; + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::PROPOSITION, + 0, 0, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::PROPOSITION, + 0, 0, 0, 0}); + nodes.push_back(do_verify::DiscreteNode{db_interval_set::empty(holder), false, do_verify::NodeType::SINCE, + 0, 1, 2, 3}); + bool allCorrect = true; + for(int time = 0; time < propositionInputs[0].size(); time++) { + bool output = do_verify::run_evaluation(nodes, holder, time, {propositionInputs[0][time], propositionInputs[1][time]}); + allCorrect &= output == expectedOutput[time]; + db_interval_set::swapBuffers(holder); + } + db_interval_set::destroyHolder(holder); + REQUIRE(allCorrect == true); + } +} From d0c2719790ade3bb8d86d44589b75776089c47f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Thu, 11 Dec 2025 20:49:03 +0300 Subject: [PATCH 2/6] also added timescales tests --- tests/test_discrete.cpp | 576 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 576 insertions(+) diff --git a/tests/test_discrete.cpp b/tests/test_discrete.cpp index ea79247..019080b 100644 --- a/tests/test_discrete.cpp +++ b/tests/test_discrete.cpp @@ -90,3 +90,579 @@ TEST_CASE("Discrete Implementation Tests", "[discrete]") { REQUIRE(allCorrect == true); } } + + + + +TEST_CASE("Discrete AbsentAQ", "[discrete][AbsentAQ]") { + + using namespace db_interval_set; + using namespace do_verify; + + + // --- 1. SETUP PARAMS --- + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + // Unpack parameters + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AbsentAQ " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; + + std::string file_name = "data/fullsuite/AbsentAQ/" + CONDENSATION + "/1M/AbsentAQ" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + + }; +} + + + +TEST_CASE("Discrete AbsentBQR", "[discrete][AbsentBQR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AbsentBQR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int since_a = 3 * (TIMINGS / 10); + const int since_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, since_a, since_b}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + std::string file_name = "data/fullsuite/AbsentBQR/" + CONDENSATION + "/1M/AbsentBQR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "AbsentBQR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete AbsentBR", "[discrete][AbsentBR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AbsentBR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int inner_always_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, inner_always_b}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + + std::string file_name = "data/fullsuite/AbsentBR/" + CONDENSATION + "/1M/AbsentBR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "AbsentBR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete AlwaysAQ", "[discrete][AlwaysAQ]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AlwaysAQ " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int once_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, once_b}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + + std::string file_name = "data/fullsuite/AlwaysAQ/" + CONDENSATION + "/1M/AlwaysAQ" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "AlwaysAQ Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete AlwaysBQR", "[discrete][AlwaysBQR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AlwaysBQR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int since_a = 3 * (TIMINGS / 10); + const int since_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, since_a, since_b}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + std::string file_name = "data/fullsuite/AlwaysBQR/" + CONDENSATION + "/1M/AlwaysBQR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "AlwaysBQR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete AlwaysBR", "[discrete][AlwaysBR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("AlwaysBR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int inner_always_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, inner_always_b}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; + + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + + std::string file_name = "data/fullsuite/AlwaysBR/" + CONDENSATION + "/1M/AlwaysBR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "AlwaysBR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete RecurBQR", "[discrete][RecurBQR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("RecurBQR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int inner_once_b = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0}; + DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; + + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + + std::string file_name = "data/fullsuite/RecurBQR/" + CONDENSATION + "/1M/RecurBQR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "RecurBQR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete RecurGLB", "[discrete][RecurGLB]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("RecurGLB " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; + + std::string file_name = "data/fullsuite/RecurGLB/" + CONDENSATION + "/1M/RecurGLB" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "RecurGLB Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete RespondBQR", "[discrete][RespondBQR]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("RespondBQR " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int once_a = 3 * (TIMINGS / 10); + const int once_b = TIMINGS; + const int since_a = TIMINGS; + + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0}; + DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, once_a, once_b}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, since_a, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0}; + DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY}; + DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; + + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + + std::string file_name = "data/fullsuite/RespondBQR/" + CONDENSATION + "/1M/RespondBQR" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].s, allInputs[i].r}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "RespondBQR Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} + +TEST_CASE("Discrete RespondGLB", "[discrete][RespondGLB]") { + using namespace db_interval_set; + using namespace do_verify; + + auto params = GENERATE(table({ + {"Discrete", 10}, + {"Discrete", 100}, + {"Discrete", 1000}, + })); + + std::string CONDENSATION; + int TIMINGS; + std::tie(CONDENSATION, TIMINGS) = params; + + std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); + + SECTION("RespondGLB " + benchmarkName) { + IntervalSetHolder holder = newHolder(1000); + + const int once_a = 3 * (TIMINGS / 10); + const int once_b = TIMINGS; + const int since_a = TIMINGS; + + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, once_a, once_b}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, since_a, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; + + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + + std::string file_name = "data/fullsuite/RespondGLB/" + CONDENSATION + "/1M/RespondGLB" + std::to_string(TIMINGS) +".row.bin"; + const auto& allInputs = binary_row_reader::readInputFile(file_name); + + bool finalOutput; + bool all_correct = true; + int maxHolderUsage = 0; + + for (int i = 0; i < allInputs.size(); i++){ + bool output = run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p, allInputs[i].s}); + if (!output) { + all_correct = false; + std::cout << benchmarkName << std::endl; + break; + } + maxHolderUsage = std::max(maxHolderUsage, holder.writeIndex); + finalOutput = output; + swapBuffers(holder); + } + std::cout << "RespondGLB Usage: " << maxHolderUsage << std::endl; + REQUIRE(all_correct == true); + destroyHolder(holder); + }; +} \ No newline at end of file From c7b1fb7cba745e5807dfcdec3fcb7d1f8eae7d9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Fri, 12 Dec 2025 17:17:35 +0300 Subject: [PATCH 3/6] added tests for whether the json and binary reader are reading the same thing --- tests/CMakeLists.txt | 1 + tests/test_readers.cpp | 27 +++++++++++++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 tests/test_readers.cpp diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 748faea..a531b3b 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -68,6 +68,7 @@ add_executable(unit_tests test_discrete.cpp test_dense.cpp test_interval_set.cpp + test_readers.cpp ) target_link_libraries(unit_tests PRIVATE do-verify Catch2::Catch2WithMain) diff --git a/tests/test_readers.cpp b/tests/test_readers.cpp new file mode 100644 index 0000000..3593a53 --- /dev/null +++ b/tests/test_readers.cpp @@ -0,0 +1,27 @@ +#include +#include +#include + +#include +#include +#include +#include +#include "do-verify/json_reader.hpp" +#include "do-verify/binary_row_reader.hpp" + + +TEST_CASE("Readers Implementation Tests", "[reader]") { + const auto &allInputs = binary_row_reader::readInputFile("data/fullsuite/AbsentAQ/Dense10/1M/AbsentAQ10.row.bin"); + + int i = 0; + std::ifstream input_file("data/fullsuite/AbsentAQ/Dense10/1M/AbsentAQ10.jsonl"); + for (std::string line; std::getline(input_file, line);){ + auto newInput = json_reader::read_line(line); + bool q = newInput.propositions[0]; + bool p = newInput.propositions[1]; + int time = newInput.time; + REQUIRE(((allInputs[i].q == q) && (allInputs[i].p == p) && (allInputs[i].time == time))); + i++; + } + +} \ No newline at end of file From 8b998c090fcec416b7c3353660838cd3a63e63fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Sat, 13 Dec 2025 14:34:47 +0300 Subject: [PATCH 4/6] created main file for comparing against reelay --- CMakeLists.txt | 7 + src/main.cpp | 763 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 770 insertions(+) create mode 100644 src/main.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 1e9276f..4de093a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -32,6 +32,13 @@ FetchContent_Declare( ) FetchContent_MakeAvailable(Catch2) + +add_executable(do-verify-bin + src/main.cpp +) + +target_link_libraries(do-verify-bin PRIVATE do-verify) + # Add Subdirectories enable_testing() add_subdirectory(tests) diff --git a/src/main.cpp b/src/main.cpp new file mode 100644 index 0000000..64de8e1 --- /dev/null +++ b/src/main.cpp @@ -0,0 +1,763 @@ +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +using namespace db_interval_set; +using namespace do_verify; + +// argp option keys +enum RYBINX_OPTS : uint8_t +{ + OPT_DENSE = 'v', + OPT_DISCRETE = 'x' +}; + +const char *argp_program_version = "do-verify-bin 0.1.0"; +const char *argp_program_bug_address = "Arinc Demir "; +static const char *doc = "Do-verify (Reelay) on Binary Row format"; +static const char *args_doc = "SPEC FILE"; + +struct arguments +{ + char *spec; + char *file; + bool dense = false; + bool discrete = false; +}; + +static std::array options = { + {{"dense", OPT_DENSE, nullptr, 0, "Use dense time model (default)", 0}, + {"discrete", OPT_DISCRETE, nullptr, 0, "Use discrete time model", 0}, + {nullptr}}}; + +static error_t parse_opt(int key, char *arg, struct argp_state *state) +{ + auto *arguments = (struct arguments *)state->input; + switch (key) + { + case OPT_DENSE: + arguments->dense = true; + break; + case OPT_DISCRETE: + arguments->discrete = true; + break; + case ARGP_KEY_ARG: + if (state->arg_num == 0) + { + arguments->spec = arg; + } + else + { + arguments->file = arg; + } + break; + case ARGP_KEY_END: + if (state->arg_num < 2) + { + argp_usage(state); + } + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} +static struct argp argp = {options.data(), parse_opt, args_doc, doc}; + +void discrete_case(arguments arguments, std::vector allInputs); +void dense_case(arguments arguments, std::vector allInputs); + +int main(int argc, char **argv) +{ + struct arguments arguments; + argp_parse(&argp, argc, argv, 0, nullptr, &arguments); + + // Choices + bool use_discrete = arguments.discrete; + bool use_dense = arguments.dense; + + // Apply defaults + if (!use_discrete && !use_dense) + { + use_discrete = true; + } + + std::ifstream input(arguments.file, std::ios::binary); + if (!input) + { + std::cerr << "Error opening file: " << arguments.file << std::endl; + return 1; + } + + const auto &allInputs = binary_row_reader::readInputFile(arguments.file); + + if (use_discrete) + { + discrete_case(arguments, allInputs); + } + else + { + dense_case(arguments, allInputs); + } + +} + +void discrete_case(arguments arguments, std::vector allInputs) +{ + // AbsentAQ: historically((once[:N]{q}) -> ((not{p}) since {q})) + if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ((not{p}) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10}; + DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ((not{p}) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100}; + DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ((not{p}) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000}; + DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY}; + DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, once, notNode, since, implies, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // AbsentBQR: historically({r} && !{q} && once{q}) -> ((not{p}) since[A:B] {q}) + else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[3:10] {q})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 3, 10}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[30:100] {q})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 30, 100}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[300:1000] {q})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 300, 1000}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // AbsentBR: historically({r} -> (historically[:N](not{p}))) + else if (strcmp(arguments.spec, "historically({r} -> (historically[:10](not{p})))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 10}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} -> (historically[:100](not{p})))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 100}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000](not{p})))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 1000}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_p, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // AlwaysAQ: historically((once[:N]{q}) -> ({p} since {q})) + else if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ({p} since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ({p} since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ({p} since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; + std::vector nodes{q, p, r, once_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // AlwaysBQR: historically(({r} && !{q} && once{q}) -> ({p} since[A:B] {q})) + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[3:10] {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 3, 10}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[30:100] {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 30, 100}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[300:1000] {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 300, 1000}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0}; + DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // AlwaysBR: historically({r} -> (historically[:N]{p})) + else if (strcmp(arguments.spec, "historically({r} -> (historically[:10]{p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 10}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} -> (historically[:100]{p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 100}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000]{p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 1000}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; + std::vector nodes{q, p, r, inner_always, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // RecurBQR: historically(({r} && !{q} && once{q}) -> ((once[:N]({p} or {q})) since {q})) + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:10]({p} or {q})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0}; + DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 10}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:100]({p} or {q})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0}; + DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 100}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:1000]({p} or {q})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0}; + DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0}; + DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0}; + DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 1000}; + DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY}; + DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; + std::vector nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // RecurGLB: historically(once[:N]{p}) + else if (strcmp(arguments.spec, "historically(once[:10]{p})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(once[:100]{p})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(once[:1000]{p})") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000}; + DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; + std::vector nodes{p, once, always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // RespondBQR: historically(({r} && !{q} && once{q}) -> ( (({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p})) since {q})) + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0}; + DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 3, 10}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 10, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0}; + DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY}; + DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].s, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0}; + DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 30, 100}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 100, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0}; + DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY}; + DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].s, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p})) since {q}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0}; + DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; + DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0}; + DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 300, 1000}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 1000, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0}; + DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY}; + DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; + std::vector nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].q, allInputs[i].p, allInputs[i].s, allInputs[i].r}); + swapBuffers(holder); + } + destroyHolder(holder); + } + // RespondGLB: historically(({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p})) + else if (strcmp(arguments.spec, "historically(({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 3, 10}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 10, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p, allInputs[i].s}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 30, 100}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 100, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p, allInputs[i].s}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else if (strcmp(arguments.spec, "historically(({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p}))") == 0) + { + IntervalSetHolder holder = newHolder(1000); + DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0}; + DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 300, 1000}; + DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0}; + DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0}; + DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 1000, B_INFINITY}; + DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0}; + DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0}; + DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; + std::vector nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always}; + + for (size_t i = 0; i < allInputs.size(); i++) + { + run_evaluation(nodes, holder, allInputs[i].time, {allInputs[i].p, allInputs[i].s}); + swapBuffers(holder); + } + destroyHolder(holder); + } + else + { + std::cout << "Error: Can't find code for spec: " << arguments.spec << std::endl; + } +} + +void dense_case(arguments arguments, std::vector allInputs) { + +} \ No newline at end of file From 6d5a4489ab251ab9c60c5cfdef62975ed6728f97 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Sat, 13 Dec 2025 14:57:09 +0300 Subject: [PATCH 5/6] changed the project structure to header-source from header-only --- CMakeLists.txt | 13 +- include/do-verify/MTLEngine.hpp | 207 +- include/do-verify/binary_row_reader.hpp | 32 +- include/do-verify/interval_set.hpp | 389 +--- include/do-verify/json_reader.hpp | 37 +- src/MTLEngine.cpp | 214 ++ src/binary_row_reader.cpp | 33 + src/interval_set.cpp | 460 +++++ src/json_reader.cpp | 38 + tests/CMakeLists.txt | 11 +- tests/old_tests.cpp | 2394 ----------------------- 11 files changed, 794 insertions(+), 3034 deletions(-) create mode 100644 src/MTLEngine.cpp create mode 100644 src/binary_row_reader.cpp create mode 100644 src/interval_set.cpp create mode 100644 src/json_reader.cpp delete mode 100644 tests/old_tests.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 4de093a..e6b5f71 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -13,12 +13,16 @@ endif() set(CMAKE_CXX_STANDARD 20) set(CMAKE_CXX_STANDARD_REQUIRED ON) -# Define the Header-Only Library -# "INTERFACE" means "I have no .cpp files to compile, just headers" -add_library(do-verify INTERFACE) +# Define the library with source files +add_library(do-verify STATIC + src/interval_set.cpp + src/MTLEngine.cpp + src/binary_row_reader.cpp + src/json_reader.cpp +) # Tell CMake where the headers are -target_include_directories(do-verify INTERFACE +target_include_directories(do-verify PUBLIC $ $ ) @@ -42,4 +46,3 @@ target_link_libraries(do-verify-bin PRIVATE do-verify) # Add Subdirectories enable_testing() add_subdirectory(tests) -add_subdirectory(benchmarks) \ No newline at end of file diff --git a/include/do-verify/MTLEngine.hpp b/include/do-verify/MTLEngine.hpp index 6bd4b89..631d9ca 100644 --- a/include/do-verify/MTLEngine.hpp +++ b/include/do-verify/MTLEngine.hpp @@ -31,138 +31,9 @@ struct DenseNode { int b; }; -inline int add_with_inf(int a, int b) { - if (a == B_INFINITY || b == B_INFINITY) { - return B_INFINITY; - } - else { - return a + b; - } -}; - -inline db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector &propositionInputs) { - for(int node_index = 0; node_index < nodes.size(); node_index++) { - DenseNode &curNode = nodes[node_index]; - switch (curNode.type) - { // TODO hocaya sor: datada bir time ve true, false geldiği zaman o timeden önce mi öyle sonra mı? - // timescales'de timeless'lar var nasıl implemente edicem - - // once -> eventually - // historically -> always - // -> -> implies - case NodeType::PROPOSITION: - if (propositionInputs[node_index]) curNode.output = db_interval_set::fromInterval(setHolder, {startTime, endTime}); - else curNode.output = db_interval_set::empty(setHolder); - break; - case NodeType::AND: - curNode.output = db_interval_set::intersectSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output); - break; - case NodeType::OR: - curNode.output = db_interval_set::unionSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output); - break; - case NodeType::NOT: - curNode.output = db_interval_set::negateSet(setHolder, nodes[curNode.rightOperandIndex].output, {startTime, endTime}); - break; - case NodeType::IMPLIES: - { - // A IMPLIES B is equivalent to (NOT A) OR B - auto notLeft = db_interval_set::negateSet(setHolder, nodes[curNode.leftOperandIndex].output, - {startTime, endTime}); - - auto right = nodes[curNode.rightOperandIndex].output; - curNode.output = db_interval_set::unionSets(setHolder, notLeft, right); - break; - } - - case NodeType::EVENTUALLY: - { - auto rightOutput = nodes[curNode.rightOperandIndex].output; - - curNode.output = db_interval_set::empty(setHolder); - - auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime}); - int i = 0; - while (db_interval_set::getNextSegment(iterator)) { - if (iterator.interval.end == iterator.interval.start) continue; - if (iterator.rightTruthy) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); - int a = 0; - } - i++; - - - auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end})); - curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); - - } - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); - break; - } - case NodeType::ALWAYS: - { - auto rightOutput = nodes[curNode.rightOperandIndex].output; - - curNode.output = db_interval_set::empty(setHolder); +int add_with_inf(int a, int b); - auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime}); - - while (db_interval_set::getNextSegment(iterator)) { - if (iterator.interval.end == iterator.interval.start) continue; - if (!iterator.rightTruthy) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); - } - - auto segmentOutput = db_interval_set::negateSet(setHolder, curNode.state, {iterator.interval.start, iterator.interval.end}); - curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); - - } - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); - break; - } - case NodeType::SINCE: - { - auto leftOutput = nodes[curNode.leftOperandIndex].output; - auto rightOutput = nodes[curNode.rightOperandIndex].output; - curNode.output = db_interval_set::empty(setHolder); - - auto iterator = db_interval_set::createSegmentIterator(leftOutput, rightOutput, {startTime, endTime}); - - while (db_interval_set::getNextSegment(iterator)) { - if (iterator.interval.end == iterator.interval.start) continue; - if (iterator.leftTruthy && iterator.rightTruthy) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); - } - else if (!iterator.leftTruthy && iterator.rightTruthy) { - curNode.state = db_interval_set::fromInterval(setHolder, {iterator.interval.end + curNode.a, add_with_inf(iterator.interval.end, curNode.b)}); - } - else if (iterator.leftTruthy && !iterator.rightTruthy) { - } - else { - curNode.state = db_interval_set::empty(setHolder); - } - - auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end})); - curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); - - } - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); - break; - } - case NodeType::TEST: - break; - } - - } - return nodes[nodes.size() - 1].output; -} +db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector &propositionInputs); struct DiscreteNode { @@ -176,76 +47,6 @@ struct DiscreteNode { }; -inline bool run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector &propositionInputs) { - for (unsigned int node_index = 0; node_index < nodes.size(); node_index++) { - DiscreteNode &curNode = nodes[node_index]; - switch (curNode.type) - { - case NodeType::PROPOSITION: - curNode.output = propositionInputs[node_index]; - break; - case NodeType::AND: - curNode.output = nodes[curNode.leftOperandIndex].output && nodes[curNode.rightOperandIndex].output; - break; - case NodeType::OR: - curNode.output = nodes[curNode.leftOperandIndex].output || nodes[curNode.rightOperandIndex].output; - break; - case NodeType::NOT: - curNode.output = !nodes[curNode.rightOperandIndex].output; - break; - case NodeType::IMPLIES: - curNode.output = !(nodes[curNode.leftOperandIndex].output && !nodes[curNode.rightOperandIndex].output); - break; - case NodeType::EVENTUALLY: - { - if (nodes[curNode.rightOperandIndex].output) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); - } - curNode.output = db_interval_set::includes(curNode.state, time); - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); - break; - - } - case NodeType::ALWAYS: - { - if (!nodes[curNode.rightOperandIndex].output) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); - } - curNode.output = !db_interval_set::includes(curNode.state, time); - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); - break; - } - case NodeType::SINCE: - { - bool leftOutput = nodes[curNode.leftOperandIndex].output; - bool rightOutput = nodes[curNode.rightOperandIndex].output; - if (leftOutput && rightOutput) { - curNode.state = db_interval_set::unionSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); - } - else if (!leftOutput && rightOutput) { - curNode.state = db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)}); - } - else if (leftOutput && !rightOutput) { - - } - else { - curNode.state = db_interval_set::empty(setHolder); - } - curNode.output = db_interval_set::includes(curNode.state, time); - curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, - db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); - break; - } - } - } - return nodes[nodes.size() - 1].output; - -} - +bool run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector &propositionInputs); -} \ No newline at end of file +} // namespace do_verify diff --git a/include/do-verify/binary_row_reader.hpp b/include/do-verify/binary_row_reader.hpp index 813d639..00976e5 100644 --- a/include/do-verify/binary_row_reader.hpp +++ b/include/do-verify/binary_row_reader.hpp @@ -1,3 +1,5 @@ +#pragma once + #include #include #include @@ -16,32 +18,6 @@ struct TimescalesInput { }; #pragma pack(pop) -inline std::vector readInputFile(std::string fileName) { - - // 2. Open File - // std::ios::ate is NOT used here because we need to read from the start - std::ifstream file(fileName, std::ios::binary); - - // 3. Read the Header (The Count) - uint32_t total_lines = 0; - file.read(reinterpret_cast(&total_lines), sizeof(total_lines)); - - // 4. Allocate Memory - // We resize the vector to hold exactly the number of records. - // This performs a single heap allocation. - std::vector data; - data.resize(total_lines); - - // 5. Bulk Read (The "Cast" into Memory) - // We calculate the total bytes needed: count * 8 bytes - // We read directly from disk into the vector's internal array. - long bytes_to_read = total_lines * sizeof(TimescalesInput); - file.read(reinterpret_cast(data.data()), bytes_to_read); - - file.close(); - - - return data; -} +std::vector readInputFile(std::string fileName); -} \ No newline at end of file +} // namespace binary_row_reader diff --git a/include/do-verify/interval_set.hpp b/include/do-verify/interval_set.hpp index 9b0753a..0b33c03 100644 --- a/include/do-verify/interval_set.hpp +++ b/include/do-verify/interval_set.hpp @@ -62,21 +62,11 @@ struct SegmentIterator { }; -inline IntervalSetHolder newHolder(int bufferSize) { - // Allocate Transition buffers - return IntervalSetHolder{new Transition[bufferSize], new Transition[bufferSize], 0, bufferSize}; -}; +IntervalSetHolder newHolder(int bufferSize); -inline void swapBuffers(IntervalSetHolder &holder) { - Transition *temp = holder.readBuffer; - holder.readBuffer = holder.writeBuffer; - holder.writeBuffer = temp; - holder.writeIndex = 0; -}; +void swapBuffers(IntervalSetHolder &holder); -inline IntervalSet empty(IntervalSetHolder &holder) { - return IntervalSet{holder.writeBuffer, 1, 0}; -}; +IntervalSet empty(IntervalSetHolder &holder); /** * @brief Checks if a single time point is contained within the interval set. @@ -86,190 +76,39 @@ inline IntervalSet empty(IntervalSetHolder &holder) { * @param time The time point to query. * @return true if the time point is in the set, false otherwise. */ -inline bool includes(const IntervalSet& set, int time) { - bool state = false; - for (int i = set.startIndex; i <= set.endIndex; ++i) { - const Transition& t = set.buffer[i]; - if (t.time <= time) { - state = t.isStart; - } else { - break; // No need to check further transitions - } - } - return state; -} - - +bool includes(const IntervalSet& set, int time); /** * @brief Creates a new set from a single [start, end) interval. * This is the primary way to get data into the system. */ -inline IntervalSet fromInterval(IntervalSetHolder &holder, Interval interval) { - int newStartIndex = holder.writeIndex; - - // Only add a non-empty interval - if (interval.start < interval.end) { - holder.writeBuffer[holder.writeIndex++] = Transition{interval.start, true}; - holder.writeBuffer[holder.writeIndex++] = Transition{interval.end, false}; - } - - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -}; +IntervalSet fromInterval(IntervalSetHolder &holder, Interval interval); /** * @brief (NEW) Copies a set from either buffer to the end of the write buffer. * This is crucial for carrying over unmodified sets * before calling swapBuffers(). */ -inline IntervalSet copySet(IntervalSetHolder& holder, IntervalSet set) { - int newStartIndex = holder.writeIndex; - - // Read from the set's *own* buffer (could be read or write) - for (int i = set.startIndex; i <= set.endIndex; ++i) { - // Write to the main writeBuffer - holder.writeBuffer[holder.writeIndex++] = set.buffer[i]; - } - - // Return a new set handle pointing to the new copy - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -} +IntervalSet copySet(IntervalSetHolder& holder, IntervalSet set); /** * @brief Computes the union (OR) of two sets using a plane-sweep algorithm. */ -inline IntervalSet unionSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB) { - int newStartIndex = holder.writeIndex; - int i = setA.startIndex; - int j = setB.startIndex; - - int overlap = 0; // "Winding number" or overlap count (can be 0, 1, or 2) - - while (i <= setA.endIndex || j <= setB.endIndex) { - // Determine the next time point to process - int t = std::numeric_limits::max(); - if (i <= setA.endIndex) t = std::min(t, setA.buffer[i].time); - if (j <= setB.endIndex) t = std::min(t, setB.buffer[j].time); - - bool wasInSet = (overlap > 0); - - if (i <= setA.endIndex && setA.buffer[i].time == t) { - overlap += (setA.buffer[i].isStart ? 1 : -1); - i++; - } - if (j <= setB.endIndex && setB.buffer[j].time == t) { - overlap += (setB.buffer[j].isStart ? 1 : -1); - j++; - } - - bool isInSet = (overlap > 0); - - // If the state changed (e.g., from 0 to 1, or 1 to 0), - // we write a new transition to the output. - if (wasInSet != isInSet) { - holder.writeBuffer[holder.writeIndex++] = Transition{t, isInSet}; - } - } - - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -}; +IntervalSet unionSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB); /** * @brief Computes the intersection (AND) of two sets. */ -inline IntervalSet intersectSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB) { - int newStartIndex = holder.writeIndex; - int i = setA.startIndex; - int j = setB.startIndex; - - // A normalized set's "overlap" is just 0 or 1 (i.e., true/false). - bool isInA = false; - bool isInB = false; - - while (i <= setA.endIndex || j <= setB.endIndex) { - int t = std::numeric_limits::max(); - if (i <= setA.endIndex) t = std::min(t, setA.buffer[i].time); - if (j <= setB.endIndex) t = std::min(t, setB.buffer[j].time); - - bool wasInSet = (isInA && isInB); - - if (i <= setA.endIndex && setA.buffer[i].time == t) { - isInA = setA.buffer[i].isStart; // Just update the flag - i++; - } - if (j <= setB.endIndex && setB.buffer[j].time == t) { - isInB = setB.buffer[j].isStart; - j++; - } - - bool isInSet = (isInA && isInB); - - // If the intersection state changed, write a transition - if (wasInSet != isInSet) { - holder.writeBuffer[holder.writeIndex++] = Transition{t, isInSet}; - } - } - - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -}; +IntervalSet intersectSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB); /** * @brief Computes the negation of a set within a given domain. * This is (domain AND (NOT setA)). */ -inline IntervalSet negateSet(IntervalSetHolder &holder, IntervalSet setA, Interval domain) { - int newStartIndex = holder.writeIndex; - int i = setA.startIndex; - - // We assume setA is "off" (-infinity) - bool isSetAOn = false; - - // First, process all transitions in setA *before* the domain starts - // to determine the state of setA right at domain.start - while (i <= setA.endIndex && setA.buffer[i].time < domain.start) { - isSetAOn = setA.buffer[i].isStart; - i++; - } - - // The negation is the opposite of setA's state - bool isNegationOn = !isSetAOn; - - // If the negation is "on" at the start of the domain, - // we must create a 'start' transition. - if (isNegationOn) { - holder.writeBuffer[holder.writeIndex++] = Transition{domain.start, true}; - } - - // Now, process all transitions *within* the domain - while (i <= setA.endIndex && setA.buffer[i].time < domain.end) { - Transition t = setA.buffer[i]; - - // The state of setA is changing... - isSetAOn = t.isStart; - - // ...which means the state of the negation is also changing. - isNegationOn = !isSetAOn; - - // Write the corresponding transition for the negated set. - holder.writeBuffer[holder.writeIndex++] = Transition{t.time, isNegationOn}; - - i++; - } - - // We have passed all transitions in setA *before* domain.end. - // If the negation is still "on", we must close it at domain.end. - if (isNegationOn) { - holder.writeBuffer[holder.writeIndex++] = Transition{domain.end, false}; - } - - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -}; +IntervalSet negateSet(IntervalSetHolder &holder, IntervalSet setA, Interval domain); -inline void destroyHolder(IntervalSetHolder &holder) { - delete[] holder.writeBuffer; - delete[] holder.readBuffer; -}; +void destroyHolder(IntervalSetHolder &holder); // --- NEW SEGMENT ITERATOR FUNCTIONS --- @@ -283,113 +122,14 @@ inline void destroyHolder(IntervalSetHolder &holder) { * @param domain The interval [start, end) to iterate over. * @return An initialized SegmentIterator. */ -inline SegmentIterator createSegmentIterator(IntervalSet setA, IntervalSet setB, Interval domain) { - SegmentIterator it; - it.leftIntervalSet = setA; - it.rightIntervalSet = setB; - it.domain = domain; - - int i = setA.startIndex; - int j = setB.startIndex; - - // 1. Find the state of A and B right *at* domain.start - // We do this by processing all transitions *before* domain.start - bool isInA = false; - while (i <= setA.endIndex && setA.buffer[i].time < domain.start) { - isInA = setA.buffer[i].isStart; - i++; - } - - bool isInB = false; - while (j <= setB.endIndex && setB.buffer[j].time < domain.start) { - isInB = setB.buffer[j].isStart; - j++; - } - - // 2. Set the *initial* internal state for the iterator - it.leftIndex = i; // The next index to read from setA - it.rightIndex = j; // The next index to read from setB - - // 3. (FIX) Set the *internal state* for the *first* segment - // These fields track the segment we are *about* to process. - it.currentSegmentStart = domain.start; - it.currentLeftTruthy = isInA; - it.currentRightTruthy = isInB; - - // The 'result' fields (it.interval, it.leftTruthy, it.rightTruthy) - // are not yet valid. They are set by the first call to getNextSegment. - it.interval = {0, 0}; - it.leftTruthy = false; - it.rightTruthy = false; - - return it; -} +SegmentIterator createSegmentIterator(IntervalSet setA, IntervalSet setB, Interval domain); /** * @brief Advances the iterator to the next segment. * @param it The iterator (passed by reference) to advance. * @return true if a valid segment was found, false if the iteration is finished. */ -inline bool getNextSegment(SegmentIterator& it) { - // Check if the *start* of the segment we are *about* to process - // is already at or past the domain end. - if (it.currentSegmentStart >= it.domain.end) { - return false; - } - - // 1. Find the time `t` of the *next* transition from either set - int t = it.domain.end; // Default to the end of the domain - - // Check for the next transition in setA - if (it.leftIndex <= it.leftIntervalSet.endIndex) { - int tA = it.leftIntervalSet.buffer[it.leftIndex].time; - // Only consider transitions *within* the domain - if (tA < it.domain.end) { - t = std::min(t, tA); - } - } - // Check for the next transition in setB - if (it.rightIndex <= it.rightIntervalSet.endIndex) { - int tB = it.rightIntervalSet.buffer[it.rightIndex].time; - // Only consider transitions *within* the domain - if (tB < it.domain.end) { - t = std::min(t, tB); - } - } - - // 2. We found the segment. - // Set the "result" fields to the segment we just *completed*. - // The state for this segment was stored in the 'current...' fields. - it.interval.start = it.currentSegmentStart; - it.interval.end = t; - it.leftTruthy = it.currentLeftTruthy; - it.rightTruthy = it.currentRightTruthy; - - // 3. Update the *internal state* for the *next* segment (which starts at time `t`) - bool nextA = it.currentLeftTruthy; - bool nextB = it.currentRightTruthy; - - // Process all transitions *at* exactly time `t` - while (it.leftIndex <= it.leftIntervalSet.endIndex && - it.leftIntervalSet.buffer[it.leftIndex].time == t) { - nextA = it.leftIntervalSet.buffer[it.leftIndex].isStart; - it.leftIndex++; - } - - while (it.rightIndex <= it.rightIntervalSet.endIndex && - it.rightIntervalSet.buffer[it.rightIndex].time == t) { - nextB = it.rightIntervalSet.buffer[it.rightIndex].isStart; - it.rightIndex++; - } - - // 4. Store the state for the *next* call - it.currentSegmentStart = t; // The *start* of the next segment - it.currentLeftTruthy = nextA; // The *state* during the next segment - it.currentRightTruthy = nextB; // The *state* during the next segment - - // We successfully produced a segment. - return true; -} +bool getNextSegment(SegmentIterator& it); // --- Helper Functions --- @@ -398,127 +138,44 @@ inline bool getNextSegment(SegmentIterator& it) { * @brief Converts an IntervalSet (of transitions) back to a * std::vector for inspection. */ -inline std::vector toVectorIntervals(const IntervalSet& set) { - std::vector result; - if (set.startIndex > set.endIndex) { - return result; // Empty set - } - - int intervalStart = 0; - // This assumes the set is normalized (no overlapping starts) - // which our union/intersect/negate functions guarantee. - - for (int i = set.startIndex; i <= set.endIndex; ++i) { - const Transition& t = set.buffer[i]; - if (t.isStart) { - intervalStart = t.time; - } else { - // Only add if it's a valid interval - if (t.time > intervalStart) { - result.push_back(Interval{intervalStart, t.time}); - } - } - } - return result; -} +std::vector toVectorIntervals(const IntervalSet& set); /** * @brief Converts an IntervalSet to a std::vector of its raw transitions. */ -inline std::vector toVectorTransitions(const IntervalSet& set) { - if (set.startIndex > set.endIndex) { - return {}; // Return an empty vector - } - return std::vector( - set.buffer + set.startIndex, - set.buffer + set.endIndex + 1 - ); -} +std::vector toVectorTransitions(const IntervalSet& set); // Helper for std::sort -inline bool compareTransitions(const Transition& a, const Transition& b) { - if (a.time != b.time) { - return a.time < b.time; - } - // Handle {10, false}, {10, true} case. - // 'start' (true) should come before 'end' (false). - return a.isStart > b.isStart; -} - -inline IntervalSet createSetFromIntervals( +bool compareTransitions(const Transition& a, const Transition& b); + +IntervalSet createSetFromIntervals( IntervalSetHolder& holder, - const std::vector& intervals) { - int newStartIndex = holder.writeIndex; - - // 1. Create all transitions in a temporary vector - std::vector transitions; - transitions.reserve(intervals.size() * 2); - for (const auto& iv : intervals) { - if (iv.start < iv.end) { - transitions.push_back({iv.start, true}); - transitions.push_back({iv.end, false}); - } - } - - // 2. Sort the transitions (O(N log N)) - std::sort(transitions.begin(), transitions.end(), compareTransitions); - - // 3. Perform the union/normalization sweep (O(N)) - int overlap = 0; - for (const auto& t : transitions) { - bool wasInSet = (overlap > 0); - overlap += (t.isStart ? 1 : -1); - bool isInSet = (overlap > 0); - - if (wasInSet != isInSet) { - // Check for buffer overflow - // (In a real benchmark, just make the buffer huge) - // if (holder.writeIndex >= MAX_BUFFER_SIZE) { ... } - holder.writeBuffer[holder.writeIndex++] = {t.time, isInSet}; - } - } - - return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; -} + const std::vector& intervals); /** * @brief Overload operator== for Interval so Catch2 can compare vectors of them. */ -inline bool operator==(const Interval& a, const Interval& b) { - return a.start == b.start && a.end == b.end; -} +bool operator==(const Interval& a, const Interval& b); /** * @brief Overload operator== for Transition for testing. */ -inline bool operator==(const Transition& a, const Transition& b) { - return a.time == b.time && a.isStart == b.isStart; -} +bool operator==(const Transition& a, const Transition& b); /** * @brief Overload operator<< for Interval for printing. */ -inline std::ostream& operator<<(std::ostream& os, const Interval& iv) { - os << "[" << iv.start << ", " << iv.end << ")"; - return os; -} +std::ostream& operator<<(std::ostream& os, const Interval& iv); /** * @brief Overload operator<< for Transition for printing. */ -inline std::ostream& operator<<(std::ostream& os, const Transition& t) { - os << "{" << t.time << ", " << (t.isStart ? "T" : "F") << "}"; - return os; -} +std::ostream& operator<<(std::ostream& os, const Transition& t); /** * @brief Overload operator<< for SegmentIterator for printing. */ -inline std::ostream& operator<<(std::ostream& os, const SegmentIterator& it) { - os << "Seg{ " << it.interval << ", A:" << (it.leftTruthy ? "T" : "F") - << ", B:" << (it.rightTruthy ? "T" : "F") << " }"; - return os; -} +std::ostream& operator<<(std::ostream& os, const SegmentIterator& it); } // namespace db_interval_set diff --git a/include/do-verify/json_reader.hpp b/include/do-verify/json_reader.hpp index 49ddae7..cad9b0f 100644 --- a/include/do-verify/json_reader.hpp +++ b/include/do-verify/json_reader.hpp @@ -5,6 +5,7 @@ #include #include #include +#include namespace json_reader { @@ -13,38 +14,6 @@ struct TimescalesInput { std::vector propositions; }; -inline TimescalesInput read_line(std::string &line) { - std::vector propositions; - int time = 0; - std::string segment; - int index = 0; - while (!isdigit(line.at(index))) { - index++; - } - int numStart = index - 1; - while (isdigit(line.at(index))) { - index++; - } - time = stoi(line.substr(numStart, index - numStart)); - - while (line.at(index) != '}') { - while (line.at(index) != ':') { - index++; - } - int truthStart = index + 2; - while (line.at(index) != ',' && line.at(index) != '}') { - index++; - } - if ("true" == line.substr(truthStart, index - truthStart)) { - propositions.push_back(true); - } - else { - propositions.push_back(false); - } - } - return TimescalesInput{time, propositions}; - -}; - +TimescalesInput read_line(std::string &line); -} \ No newline at end of file +} // namespace json_reader diff --git a/src/MTLEngine.cpp b/src/MTLEngine.cpp new file mode 100644 index 0000000..1364808 --- /dev/null +++ b/src/MTLEngine.cpp @@ -0,0 +1,214 @@ +#include "do-verify/MTLEngine.hpp" + +namespace do_verify { + +int add_with_inf(int a, int b) { + if (a == B_INFINITY || b == B_INFINITY) { + return B_INFINITY; + } + else { + return a + b; + } +} + +db_interval_set::IntervalSet run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int startTime, const int endTime, const std::vector &propositionInputs) { + for(size_t node_index = 0; node_index < nodes.size(); node_index++) { + DenseNode &curNode = nodes[node_index]; + switch (curNode.type) + { // TODO hocaya sor: datada bir time ve true, false geldiği zaman o timeden önce mi öyle sonra mı? + // timescales'de timeless'lar var nasıl implemente edicem + + // once -> eventually + // historically -> always + // -> -> implies + + case NodeType::PROPOSITION: + if (propositionInputs[node_index]) curNode.output = db_interval_set::fromInterval(setHolder, {startTime, endTime}); + else curNode.output = db_interval_set::empty(setHolder); + break; + case NodeType::AND: + curNode.output = db_interval_set::intersectSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output); + break; + case NodeType::OR: + curNode.output = db_interval_set::unionSets(setHolder, nodes[curNode.leftOperandIndex].output, nodes[curNode.rightOperandIndex].output); + break; + case NodeType::NOT: + curNode.output = db_interval_set::negateSet(setHolder, nodes[curNode.rightOperandIndex].output, {startTime, endTime}); + break; + case NodeType::IMPLIES: + { + // A IMPLIES B is equivalent to (NOT A) OR B + auto notLeft = db_interval_set::negateSet(setHolder, nodes[curNode.leftOperandIndex].output, + {startTime, endTime}); + + auto right = nodes[curNode.rightOperandIndex].output; + curNode.output = db_interval_set::unionSets(setHolder, notLeft, right); + break; + } + + case NodeType::EVENTUALLY: + { + auto rightOutput = nodes[curNode.rightOperandIndex].output; + + curNode.output = db_interval_set::empty(setHolder); + + auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime}); + int i = 0; + while (db_interval_set::getNextSegment(iterator)) { + if (iterator.interval.end == iterator.interval.start) continue; + if (iterator.rightTruthy) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); + int a = 0; + (void)a; // Suppress unused variable warning + } + i++; + + + auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end})); + curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); + + } + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); + break; + } + case NodeType::ALWAYS: + { + auto rightOutput = nodes[curNode.rightOperandIndex].output; + + curNode.output = db_interval_set::empty(setHolder); + + auto iterator = db_interval_set::createSegmentIterator(db_interval_set::empty(setHolder), rightOutput, {startTime, endTime}); + + while (db_interval_set::getNextSegment(iterator)) { + if (iterator.interval.end == iterator.interval.start) continue; + if (!iterator.rightTruthy) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); + } + + auto segmentOutput = db_interval_set::negateSet(setHolder, curNode.state, {iterator.interval.start, iterator.interval.end}); + curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); + + } + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); + break; + } + case NodeType::SINCE: + { + auto leftOutput = nodes[curNode.leftOperandIndex].output; + auto rightOutput = nodes[curNode.rightOperandIndex].output; + curNode.output = db_interval_set::empty(setHolder); + + auto iterator = db_interval_set::createSegmentIterator(leftOutput, rightOutput, {startTime, endTime}); + + while (db_interval_set::getNextSegment(iterator)) { + if (iterator.interval.end == iterator.interval.start) continue; + if (iterator.leftTruthy && iterator.rightTruthy) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {iterator.interval.start + curNode.a, add_with_inf(iterator.interval.end, curNode.b)})); + } + else if (!iterator.leftTruthy && iterator.rightTruthy) { + curNode.state = db_interval_set::fromInterval(setHolder, {iterator.interval.end + curNode.a, add_with_inf(iterator.interval.end, curNode.b)}); + } + else if (iterator.leftTruthy && !iterator.rightTruthy) { + } + else { + curNode.state = db_interval_set::empty(setHolder); + } + + auto segmentOutput = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {iterator.interval.start, iterator.interval.end})); + curNode.output = db_interval_set::unionSets(setHolder, curNode.output, segmentOutput); + + } + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {endTime, B_INFINITY})); + break; + } + case NodeType::TEST: + break; + } + + } + return nodes[nodes.size() - 1].output; +} + + +bool run_evaluation(std::vector &nodes, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector &propositionInputs) { + for (unsigned int node_index = 0; node_index < nodes.size(); node_index++) { + DiscreteNode &curNode = nodes[node_index]; + switch (curNode.type) + { + case NodeType::PROPOSITION: + curNode.output = propositionInputs[node_index]; + break; + case NodeType::AND: + curNode.output = nodes[curNode.leftOperandIndex].output && nodes[curNode.rightOperandIndex].output; + break; + case NodeType::OR: + curNode.output = nodes[curNode.leftOperandIndex].output || nodes[curNode.rightOperandIndex].output; + break; + case NodeType::NOT: + curNode.output = !nodes[curNode.rightOperandIndex].output; + break; + case NodeType::IMPLIES: + curNode.output = !(nodes[curNode.leftOperandIndex].output && !nodes[curNode.rightOperandIndex].output); + break; + case NodeType::EVENTUALLY: + { + if (nodes[curNode.rightOperandIndex].output) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + curNode.output = db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + + } + case NodeType::ALWAYS: + { + if (!nodes[curNode.rightOperandIndex].output) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + curNode.output = !db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + } + case NodeType::SINCE: + { + bool leftOutput = nodes[curNode.leftOperandIndex].output; + bool rightOutput = nodes[curNode.rightOperandIndex].output; + if (leftOutput && rightOutput) { + curNode.state = db_interval_set::unionSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)})); + } + else if (!leftOutput && rightOutput) { + curNode.state = db_interval_set::fromInterval(setHolder, {time + curNode.a, add_with_inf(time + 1, curNode.b)}); + } + else if (leftOutput && !rightOutput) { + + } + else { + curNode.state = db_interval_set::empty(setHolder); + } + curNode.output = db_interval_set::includes(curNode.state, time); + curNode.state = db_interval_set::intersectSets(setHolder, curNode.state, + db_interval_set::fromInterval(setHolder, {time + 1, B_INFINITY})); + break; + } + case NodeType::TEST: + break; + } + } + return nodes[nodes.size() - 1].output; + +} + +} // namespace do_verify diff --git a/src/binary_row_reader.cpp b/src/binary_row_reader.cpp new file mode 100644 index 0000000..f362a05 --- /dev/null +++ b/src/binary_row_reader.cpp @@ -0,0 +1,33 @@ +#include "do-verify/binary_row_reader.hpp" + +namespace binary_row_reader { + +std::vector readInputFile(std::string fileName) { + + // 2. Open File + // std::ios::ate is NOT used here because we need to read from the start + std::ifstream file(fileName, std::ios::binary); + + // 3. Read the Header (The Count) + uint32_t total_lines = 0; + file.read(reinterpret_cast(&total_lines), sizeof(total_lines)); + + // 4. Allocate Memory + // We resize the vector to hold exactly the number of records. + // This performs a single heap allocation. + std::vector data; + data.resize(total_lines); + + // 5. Bulk Read (The "Cast" into Memory) + // We calculate the total bytes needed: count * 8 bytes + // We read directly from disk into the vector's internal array. + long bytes_to_read = total_lines * sizeof(TimescalesInput); + file.read(reinterpret_cast(data.data()), bytes_to_read); + + file.close(); + + + return data; +} + +} // namespace binary_row_reader diff --git a/src/interval_set.cpp b/src/interval_set.cpp new file mode 100644 index 0000000..c1f4489 --- /dev/null +++ b/src/interval_set.cpp @@ -0,0 +1,460 @@ +#include "do-verify/interval_set.hpp" + +namespace db_interval_set { + +IntervalSetHolder newHolder(int bufferSize) { + // Allocate Transition buffers + return IntervalSetHolder{new Transition[bufferSize], new Transition[bufferSize], 0, bufferSize}; +} + +void swapBuffers(IntervalSetHolder &holder) { + Transition *temp = holder.readBuffer; + holder.readBuffer = holder.writeBuffer; + holder.writeBuffer = temp; + holder.writeIndex = 0; +} + +IntervalSet empty(IntervalSetHolder &holder) { + return IntervalSet{holder.writeBuffer, 1, 0}; +} + +/** + * @brief Checks if a single time point is contained within the interval set. + * Since intervals are [start, end), start is inclusive and end is exclusive. + * + * @param set The interval set to check. + * @param time The time point to query. + * @return true if the time point is in the set, false otherwise. + */ +bool includes(const IntervalSet& set, int time) { + bool state = false; + for (int i = set.startIndex; i <= set.endIndex; ++i) { + const Transition& t = set.buffer[i]; + if (t.time <= time) { + state = t.isStart; + } else { + break; // No need to check further transitions + } + } + return state; +} + +/** + * @brief Creates a new set from a single [start, end) interval. + * This is the primary way to get data into the system. + */ +IntervalSet fromInterval(IntervalSetHolder &holder, Interval interval) { + int newStartIndex = holder.writeIndex; + + // Only add a non-empty interval + if (interval.start < interval.end) { + holder.writeBuffer[holder.writeIndex++] = Transition{interval.start, true}; + holder.writeBuffer[holder.writeIndex++] = Transition{interval.end, false}; + } + + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +/** + * @brief (NEW) Copies a set from either buffer to the end of the write buffer. + * This is crucial for carrying over unmodified sets + * before calling swapBuffers(). + */ +IntervalSet copySet(IntervalSetHolder& holder, IntervalSet set) { + int newStartIndex = holder.writeIndex; + + // Read from the set's *own* buffer (could be read or write) + for (int i = set.startIndex; i <= set.endIndex; ++i) { + // Write to the main writeBuffer + holder.writeBuffer[holder.writeIndex++] = set.buffer[i]; + } + + // Return a new set handle pointing to the new copy + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +/** + * @brief Computes the union (OR) of two sets using a plane-sweep algorithm. + */ +IntervalSet unionSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB) { + int newStartIndex = holder.writeIndex; + int i = setA.startIndex; + int j = setB.startIndex; + + int overlap = 0; // "Winding number" or overlap count (can be 0, 1, or 2) + + while (i <= setA.endIndex || j <= setB.endIndex) { + // Determine the next time point to process + int t = std::numeric_limits::max(); + if (i <= setA.endIndex) t = std::min(t, setA.buffer[i].time); + if (j <= setB.endIndex) t = std::min(t, setB.buffer[j].time); + + bool wasInSet = (overlap > 0); + + if (i <= setA.endIndex && setA.buffer[i].time == t) { + overlap += (setA.buffer[i].isStart ? 1 : -1); + i++; + } + if (j <= setB.endIndex && setB.buffer[j].time == t) { + overlap += (setB.buffer[j].isStart ? 1 : -1); + j++; + } + + bool isInSet = (overlap > 0); + + // If the state changed (e.g., from 0 to 1, or 1 to 0), + // we write a new transition to the output. + if (wasInSet != isInSet) { + holder.writeBuffer[holder.writeIndex++] = Transition{t, isInSet}; + } + } + + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +/** + * @brief Computes the intersection (AND) of two sets. + */ +IntervalSet intersectSets(IntervalSetHolder &holder, IntervalSet setA, IntervalSet setB) { + int newStartIndex = holder.writeIndex; + int i = setA.startIndex; + int j = setB.startIndex; + + // A normalized set's "overlap" is just 0 or 1 (i.e., true/false). + bool isInA = false; + bool isInB = false; + + while (i <= setA.endIndex || j <= setB.endIndex) { + int t = std::numeric_limits::max(); + if (i <= setA.endIndex) t = std::min(t, setA.buffer[i].time); + if (j <= setB.endIndex) t = std::min(t, setB.buffer[j].time); + + bool wasInSet = (isInA && isInB); + + if (i <= setA.endIndex && setA.buffer[i].time == t) { + isInA = setA.buffer[i].isStart; // Just update the flag + i++; + } + if (j <= setB.endIndex && setB.buffer[j].time == t) { + isInB = setB.buffer[j].isStart; + j++; + } + + bool isInSet = (isInA && isInB); + + // If the intersection state changed, write a transition + if (wasInSet != isInSet) { + holder.writeBuffer[holder.writeIndex++] = Transition{t, isInSet}; + } + } + + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +/** + * @brief Computes the negation of a set within a given domain. + * This is (domain AND (NOT setA)). + */ +IntervalSet negateSet(IntervalSetHolder &holder, IntervalSet setA, Interval domain) { + int newStartIndex = holder.writeIndex; + int i = setA.startIndex; + + // We assume setA is "off" (-infinity) + bool isSetAOn = false; + + // First, process all transitions in setA *before* the domain starts + // to determine the state of setA right at domain.start + while (i <= setA.endIndex && setA.buffer[i].time < domain.start) { + isSetAOn = setA.buffer[i].isStart; + i++; + } + + // The negation is the opposite of setA's state + bool isNegationOn = !isSetAOn; + + // If the negation is "on" at the start of the domain, + // we must create a 'start' transition. + if (isNegationOn) { + holder.writeBuffer[holder.writeIndex++] = Transition{domain.start, true}; + } + + // Now, process all transitions *within* the domain + while (i <= setA.endIndex && setA.buffer[i].time < domain.end) { + Transition t = setA.buffer[i]; + + // The state of setA is changing... + isSetAOn = t.isStart; + + // ...which means the state of the negation is also changing. + isNegationOn = !isSetAOn; + + // Write the corresponding transition for the negated set. + holder.writeBuffer[holder.writeIndex++] = Transition{t.time, isNegationOn}; + + i++; + } + + // We have passed all transitions in setA *before* domain.end. + // If the negation is still "on", we must close it at domain.end. + if (isNegationOn) { + holder.writeBuffer[holder.writeIndex++] = Transition{domain.end, false}; + } + + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +void destroyHolder(IntervalSetHolder &holder) { + delete[] holder.writeBuffer; + delete[] holder.readBuffer; +} + +// --- NEW SEGMENT ITERATOR FUNCTIONS --- + +/** + * @brief Creates and initializes a SegmentIterator. + * This iterator walks through a 'domain' and reports the boolean state + * of setA and setB for each sub-segment. + * + * @param setA The "left" interval set. + * @param setB The "right" interval set. + * @param domain The interval [start, end) to iterate over. + * @return An initialized SegmentIterator. + */ +SegmentIterator createSegmentIterator(IntervalSet setA, IntervalSet setB, Interval domain) { + SegmentIterator it; + it.leftIntervalSet = setA; + it.rightIntervalSet = setB; + it.domain = domain; + + int i = setA.startIndex; + int j = setB.startIndex; + + // 1. Find the state of A and B right *at* domain.start + // We do this by processing all transitions *before* domain.start + bool isInA = false; + while (i <= setA.endIndex && setA.buffer[i].time < domain.start) { + isInA = setA.buffer[i].isStart; + i++; + } + + bool isInB = false; + while (j <= setB.endIndex && setB.buffer[j].time < domain.start) { + isInB = setB.buffer[j].isStart; + j++; + } + + // 2. Set the *initial* internal state for the iterator + it.leftIndex = i; // The next index to read from setA + it.rightIndex = j; // The next index to read from setB + + // 3. (FIX) Set the *internal state* for the *first* segment + // These fields track the segment we are *about* to process. + it.currentSegmentStart = domain.start; + it.currentLeftTruthy = isInA; + it.currentRightTruthy = isInB; + + // The 'result' fields (it.interval, it.leftTruthy, it.rightTruthy) + // are not yet valid. They are set by the first call to getNextSegment. + it.interval = {0, 0}; + it.leftTruthy = false; + it.rightTruthy = false; + + return it; +} + +/** + * @brief Advances the iterator to the next segment. + * @param it The iterator (passed by reference) to advance. + * @return true if a valid segment was found, false if the iteration is finished. + */ +bool getNextSegment(SegmentIterator& it) { + // Check if the *start* of the segment we are *about* to process + // is already at or past the domain end. + if (it.currentSegmentStart >= it.domain.end) { + return false; + } + + // 1. Find the time `t` of the *next* transition from either set + int t = it.domain.end; // Default to the end of the domain + + // Check for the next transition in setA + if (it.leftIndex <= it.leftIntervalSet.endIndex) { + int tA = it.leftIntervalSet.buffer[it.leftIndex].time; + // Only consider transitions *within* the domain + if (tA < it.domain.end) { + t = std::min(t, tA); + } + } + // Check for the next transition in setB + if (it.rightIndex <= it.rightIntervalSet.endIndex) { + int tB = it.rightIntervalSet.buffer[it.rightIndex].time; + // Only consider transitions *within* the domain + if (tB < it.domain.end) { + t = std::min(t, tB); + } + } + + // 2. We found the segment. + // Set the "result" fields to the segment we just *completed*. + // The state for this segment was stored in the 'current...' fields. + it.interval.start = it.currentSegmentStart; + it.interval.end = t; + it.leftTruthy = it.currentLeftTruthy; + it.rightTruthy = it.currentRightTruthy; + + // 3. Update the *internal state* for the *next* segment (which starts at time `t`) + bool nextA = it.currentLeftTruthy; + bool nextB = it.currentRightTruthy; + + // Process all transitions *at* exactly time `t` + while (it.leftIndex <= it.leftIntervalSet.endIndex && + it.leftIntervalSet.buffer[it.leftIndex].time == t) { + nextA = it.leftIntervalSet.buffer[it.leftIndex].isStart; + it.leftIndex++; + } + + while (it.rightIndex <= it.rightIntervalSet.endIndex && + it.rightIntervalSet.buffer[it.rightIndex].time == t) { + nextB = it.rightIntervalSet.buffer[it.rightIndex].isStart; + it.rightIndex++; + } + + // 4. Store the state for the *next* call + it.currentSegmentStart = t; // The *start* of the next segment + it.currentLeftTruthy = nextA; // The *state* during the next segment + it.currentRightTruthy = nextB; // The *state* during the next segment + + // We successfully produced a segment. + return true; +} + + +// --- Helper Functions --- + +/** + * @brief Converts an IntervalSet (of transitions) back to a + * std::vector for inspection. + */ +std::vector toVectorIntervals(const IntervalSet& set) { + std::vector result; + if (set.startIndex > set.endIndex) { + return result; // Empty set + } + + int intervalStart = 0; + // This assumes the set is normalized (no overlapping starts) + // which our union/intersect/negate functions guarantee. + + for (int i = set.startIndex; i <= set.endIndex; ++i) { + const Transition& t = set.buffer[i]; + if (t.isStart) { + intervalStart = t.time; + } else { + // Only add if it's a valid interval + if (t.time > intervalStart) { + result.push_back(Interval{intervalStart, t.time}); + } + } + } + return result; +} + +/** + * @brief Converts an IntervalSet to a std::vector of its raw transitions. + */ +std::vector toVectorTransitions(const IntervalSet& set) { + if (set.startIndex > set.endIndex) { + return {}; // Return an empty vector + } + return std::vector( + set.buffer + set.startIndex, + set.buffer + set.endIndex + 1 + ); +} + +// Helper for std::sort +bool compareTransitions(const Transition& a, const Transition& b) { + if (a.time != b.time) { + return a.time < b.time; + } + // Handle {10, false}, {10, true} case. + // 'start' (true) should come before 'end' (false). + return a.isStart > b.isStart; +} + +IntervalSet createSetFromIntervals( + IntervalSetHolder& holder, + const std::vector& intervals) { + int newStartIndex = holder.writeIndex; + + // 1. Create all transitions in a temporary vector + std::vector transitions; + transitions.reserve(intervals.size() * 2); + for (const auto& iv : intervals) { + if (iv.start < iv.end) { + transitions.push_back({iv.start, true}); + transitions.push_back({iv.end, false}); + } + } + + // 2. Sort the transitions (O(N log N)) + std::sort(transitions.begin(), transitions.end(), compareTransitions); + + // 3. Perform the union/normalization sweep (O(N)) + int overlap = 0; + for (const auto& t : transitions) { + bool wasInSet = (overlap > 0); + overlap += (t.isStart ? 1 : -1); + bool isInSet = (overlap > 0); + + if (wasInSet != isInSet) { + // Check for buffer overflow + // (In a real benchmark, just make the buffer huge) + // if (holder.writeIndex >= MAX_BUFFER_SIZE) { ... } + holder.writeBuffer[holder.writeIndex++] = {t.time, isInSet}; + } + } + + return IntervalSet{holder.writeBuffer, newStartIndex, holder.writeIndex - 1}; +} + +/** + * @brief Overload operator== for Interval so Catch2 can compare vectors of them. + */ +bool operator==(const Interval& a, const Interval& b) { + return a.start == b.start && a.end == b.end; +} + +/** + * @brief Overload operator== for Transition for testing. + */ +bool operator==(const Transition& a, const Transition& b) { + return a.time == b.time && a.isStart == b.isStart; +} + +/** + * @brief Overload operator<< for Interval for printing. + */ +std::ostream& operator<<(std::ostream& os, const Interval& iv) { + os << "[" << iv.start << ", " << iv.end << ")"; + return os; +} + +/** + * @brief Overload operator<< for Transition for printing. + */ +std::ostream& operator<<(std::ostream& os, const Transition& t) { + os << "{" << t.time << ", " << (t.isStart ? "T" : "F") << "}"; + return os; +} + +/** + * @brief Overload operator<< for SegmentIterator for printing. + */ +std::ostream& operator<<(std::ostream& os, const SegmentIterator& it) { + os << "Seg{ " << it.interval << ", A:" << (it.leftTruthy ? "T" : "F") + << ", B:" << (it.rightTruthy ? "T" : "F") << " }"; + return os; +} + +} // namespace db_interval_set diff --git a/src/json_reader.cpp b/src/json_reader.cpp new file mode 100644 index 0000000..0b0567e --- /dev/null +++ b/src/json_reader.cpp @@ -0,0 +1,38 @@ +#include "do-verify/json_reader.hpp" + +namespace json_reader { + +TimescalesInput read_line(std::string &line) { + std::vector propositions; + int time = 0; + std::string segment; + size_t index = 0; + while (!isdigit(line.at(index))) { + index++; + } + size_t numStart = index - 1; + while (isdigit(line.at(index))) { + index++; + } + time = stoi(line.substr(numStart, index - numStart)); + + while (line.at(index) != '}') { + while (line.at(index) != ':') { + index++; + } + size_t truthStart = index + 2; + while (line.at(index) != ',' && line.at(index) != '}') { + index++; + } + if ("true" == line.substr(truthStart, index - truthStart)) { + propositions.push_back(true); + } + else { + propositions.push_back(false); + } + } + return TimescalesInput{time, propositions}; + +} + +} // namespace json_reader diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index a531b3b..5e14c91 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -12,6 +12,7 @@ if(ENABLE_COVERAGE) # 3. Generate Report COMMAND ${GCOVR_PATH} -r ${CMAKE_SOURCE_DIR} + --filter "${CMAKE_SOURCE_DIR}/src/" --filter "${CMAKE_SOURCE_DIR}/include/" --exclude "${CMAKE_BINARY_DIR}" --exclude "${CMAKE_SOURCE_DIR}/tests/" @@ -25,6 +26,7 @@ if(ENABLE_COVERAGE) # 4. Generate XML Report (For Tools/Codecov) COMMAND ${GCOVR_PATH} -r ${CMAKE_SOURCE_DIR} + --filter "${CMAKE_SOURCE_DIR}/src/" --filter "${CMAKE_SOURCE_DIR}/include/" --exclude "${CMAKE_BINARY_DIR}" --exclude "${CMAKE_SOURCE_DIR}/tests/" @@ -38,6 +40,7 @@ if(ENABLE_COVERAGE) # 5. Print Summary to Console (Standard Output) COMMAND ${GCOVR_PATH} -r ${CMAKE_SOURCE_DIR} + --filter "${CMAKE_SOURCE_DIR}/src/" --filter "${CMAKE_SOURCE_DIR}/include/" --exclude "${CMAKE_BINARY_DIR}" --exclude "${CMAKE_SOURCE_DIR}/tests/" @@ -47,13 +50,13 @@ if(ENABLE_COVERAGE) --exclude-throw-branches --txt # explicitly sets text format - COMMAND ${CMAKE_COMMAND} -E echo "------------------------------------------------" - COMMAND ${CMAKE_COMMAND} -E echo "Coverage Filter: ${CMAKE_SOURCE_DIR}/include/" + COMMAND ${CMAKE_COMMAND} -E echo "--------------------------------------------------" + COMMAND ${CMAKE_COMMAND} -E echo "Coverage Filter: ${CMAKE_SOURCE_DIR}/src/" COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 1: ${CMAKE_BINARY_DIR}" COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 2: ${CMAKE_SOURCE_DIR}/tests/" COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 3: ${CMAKE_SOURCE_DIR}/benchmarks/" - COMMAND ${CMAKE_COMMAND} -E echo "------------------------------------------------" - + COMMAND ${CMAKE_COMMAND} -E echo "--------------------------------------------------" + WORKING_DIRECTORY ${CMAKE_SOURCE_DIR} diff --git a/tests/old_tests.cpp b/tests/old_tests.cpp deleted file mode 100644 index 3fe53d7..0000000 --- a/tests/old_tests.cpp +++ /dev/null @@ -1,2394 +0,0 @@ -#include -#include -#include - - -#include -#include -#include - -#include "branching/engineSetup.hpp" -#include "branching/temporalLogicEngine.hpp" - -#include "branching_pro_seperate/engineSetup.hpp" -#include "branching_pro_seperate/temporalLogicEngine.hpp" - -#include "function_pointers/engineSetup.hpp" -#include "function_pointers/temporalLogicEngine.hpp" - -#include "branching_up_out_seperate/engineSetup.hpp" -#include "branching_up_out_seperate/temporalLogicEngine.hpp" - -#include "memory_block/engineSetup.hpp" -#include "memory_block/temporalLogicEngine.hpp" - -#include "heap_vs_entt/entt_linkedlist.hpp" -#include "heap_vs_entt/heap_linkedlist.hpp" - - - -TEST_CASE("Benchmarks", "[benchmark_first]") { - - - BENCHMARK_ADVANCED("Branching_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching::setupSinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Branching_Pro_Seperate_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching_pro_seperate::setupSinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching_pro_seperate::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Func_Pointers_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_func_ptr::setupSinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_func_ptr::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Branching_Up_Out_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching_up_out_seperate::setupSinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching_up_out_seperate::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Memory_Block_SinceAnd")(Catch::Benchmark::Chronometer meter) { - std::vector nodes = memory_block::setupAlternatingSinceAndRegistry(2, 2); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs(4); - meter.measure([&] { return memory_block::run_temporal_evaluation(nodes, propositionInputs, outputs); }); - }; - - - BENCHMARK_ADVANCED("Branching_Chain_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching::setup1000SinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - - BENCHMARK_ADVANCED("Branching_Pro_Seperate_Chain_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching_pro_seperate::setup1000SinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching_pro_seperate::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Func_Pointers_Chain_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_func_ptr::setup1000SinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_func_ptr::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Branching_Up_Out_Chain_SinceAnd")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry = tle_branching_up_out_seperate::setup1000SinceAndRegistry(); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs; - meter.measure([&] { return tle_branching_up_out_seperate::run_temporal_evaluation(registry, propositionInputs, outputs); }); - }; - - BENCHMARK_ADVANCED("Memory_Block_Chain_SinceAnd")(Catch::Benchmark::Chronometer meter) { - std::vector nodes = memory_block::setupAlternatingSinceAndRegistry(2, 998); - int noTimeSteps = 1000; - std::vector> propositionInputs = {std::vector(noTimeSteps), {std::vector(noTimeSteps)}}; - for (int timeStep = 0; timeStep < noTimeSteps; timeStep++){ - propositionInputs[0][timeStep] = (rand() % 2 == 0); - propositionInputs[1][timeStep] = (rand() % 2 == 0); - } - std::vector> outputs(1000); - meter.measure([&] { return memory_block::run_temporal_evaluation(nodes, propositionInputs, outputs); }); - }; - -} - - -TEST_CASE("Correctness for (p1 S p2) AND p2", "[correctness][complex]") { - - // The specific input for this test case - std::vector> propositionInputs = { - {true, true, false, true, true, true}, // p1 - {false, true, true, false, true, false} // p2 - }; - - // The final expected output after all operations - std::vector expected_final_output = {false, true, true, false, true, false}; - - // Assuming your other setups produce the same logical graph, - // you can test them all here. - // If they are different, you'll need separate TEST_CASEs. - - SECTION("Function Pointers Implementation") { - entt::registry registry = tle_func_ptr::setupSinceAndRegistry(); - std::vector> outputs; - - tle_func_ptr::run_temporal_evaluation(registry, propositionInputs, outputs); - - // 3. Assert the output is correct - // Check that the engine produced a single final output stream - // Check that the output stream matches our manually calculated result - REQUIRE(outputs[3] == expected_final_output); - } - - - SECTION("Branching Implementation") { - entt::registry registry = tle_branching::setupSinceAndRegistry(); - std::vector> outputs; - - tle_branching::run_temporal_evaluation(registry, propositionInputs, outputs); - - // 3. Assert the output is correct - // Check that the engine produced a single final output stream - // Check that the output stream matches our manually calculated result - REQUIRE(outputs[3] == expected_final_output); - } - - SECTION("Branching_Pro_Seperate Implementation") { - entt::registry registry = tle_branching_pro_seperate::setupSinceAndRegistry(); - std::vector> outputs; - - tle_branching_pro_seperate::run_temporal_evaluation(registry, propositionInputs, outputs); - - // 3. Assert the output is correct - // Check that the engine produced a single final output stream - // Check that the output stream matches our manually calculated result - REQUIRE(outputs[3] == expected_final_output); - } - - SECTION("Memory Block Implementation") { - std::vector nodes = memory_block::setupAlternatingSinceAndRegistry(2, 2); - std::vector> outputs(4); - - memory_block::run_temporal_evaluation(nodes, propositionInputs, outputs); - - // 3. Assert the output is correct - // Check that the engine produced a single final output stream - // Check that the output stream matches our manually calculated result - REQUIRE(outputs[3] == expected_final_output); - } -} - - -TEST_CASE("LinkedListBenchmarks", "[linked]") { - - - BENCHMARK_ADVANCED("Entt_creation")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry; - int length = 10000; - meter.measure([&] { return entt_linkedlist::createLinkedList(registry, length);}); - }; - - BENCHMARK_ADVANCED("Heap_creation")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry; - int length = 10000; - meter.measure([&] { return heap_linkedlist::createLinkedList(length);}); - }; - - BENCHMARK_ADVANCED("Entt_iteration")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry; - int length = 10000; - entt::entity head = entt_linkedlist::createLinkedList(registry, length); - meter.measure([&] { return entt_linkedlist::loopOverLinkedList(registry, head);}); - }; - - BENCHMARK_ADVANCED("Heap_iteration")(Catch::Benchmark::Chronometer meter) { - - entt::registry registry; - int length = 10000; - heap_linkedlist::Interval *head = heap_linkedlist::createLinkedList(length); - meter.measure([&] { return heap_linkedlist::loopOverLinkedList(head);}); - }; -} - -#include -#include "boost_test/benchmark_functions.hpp" -#include "my_interval_set/interval_set.hpp" -#include "my_interval_set/benchmark_functions.hpp" - -TEST_CASE("Interval Set Benchmarks", "[benchmark][interval]") { - - - BENCHMARK_ADVANCED("Boost One Interval")(Catch::Benchmark::Chronometer meter) { - - auto nodes = boost_tests::create_nodes(100); - - meter.measure([&] { return boost_tests::process_nodes(10, 20, 10000, nodes, 1.0);}); - }; - - BENCHMARK_ADVANCED("My Implementation One Interval")(Catch::Benchmark::Chronometer meter) { - - auto nodes = interval_set::create_nodes(100); - - meter.measure([&] { return interval_set::process_nodes(10, 20, 10000, nodes, 1.0);}); - }; - - BENCHMARK_ADVANCED("Boost Many Intervals")(Catch::Benchmark::Chronometer meter) { - - auto nodes = boost_tests::create_nodes(100); - - meter.measure([&] { return boost_tests::process_nodes(1000, 1000, 10000, nodes, 0.5);}); - }; - - BENCHMARK_ADVANCED("My Implementation Many Intervals")(Catch::Benchmark::Chronometer meter) { - - auto nodes = interval_set::create_nodes(100); - - meter.measure([&] { return interval_set::process_nodes(1000, 1000, 10000, nodes, 0.5);}); - }; - -} - - -#include "my_interval_set/interval_set.hpp" // The class we are testing - -TEST_CASE("IntervalSet functionality", "[interval_set_implementation]") { - interval_set::IntervalSet set; - - SECTION("Initial state is empty") { - // A new set should not pop anything successfully. - REQUIRE(set.pop_cur_time_from_left(0) == false); - REQUIRE(set.pop_cur_time_from_left(100) == false); - } - - SECTION("Adding and popping a single interval") { - set.add_interval_from_right(5, 7); // Adds interval [5, 7] - - // Test the 'k' time constraint - REQUIRE(set.pop_cur_time_from_left(4) == false); // Too early to pop - - // Pop the elements - REQUIRE(set.pop_cur_time_from_left(5) == true); // Pops 5, interval becomes [6, 7] - REQUIRE(set.pop_cur_time_from_left(6) == true); // Pops 6, interval becomes [7, 7] - REQUIRE(set.pop_cur_time_from_left(7) == true); // Pops 7, interval becomes empty - - // The set should now be empty - REQUIRE(set.pop_cur_time_from_left(7) == false); - } - - SECTION("Adding a disjoint interval") { - set.add_interval_from_right(2, 3); - set.add_interval_from_right(5, 6); - - REQUIRE(set.pop_cur_time_from_left(2) == true); // pop 2 - REQUIRE(set.pop_cur_time_from_left(3) == true); // pop 3 - - // First interval is gone, should be a gap at 4 - REQUIRE(set.pop_cur_time_from_left(4) == false); - - // We should now be able to pop from the second interval - REQUIRE(set.pop_cur_time_from_left(5) == true); // pop 5 - REQUIRE(set.pop_cur_time_from_left(6) == true); // pop 6 - - // Set is now empty - REQUIRE(set.pop_cur_time_from_left(6) == false); - } - - SECTION("Adding overlapping intervals should merge") { - set.add_interval_from_right(10, 15); - set.add_interval_from_right(14, 18); // This should merge - - // Pop until 18 - for(int k=10; k <= 18; ++k) { - REQUIRE(set.pop_cur_time_from_left(k) == true); - } - - // Set should now be empty - REQUIRE(set.pop_cur_time_from_left(19) == false); - } - - SECTION("Adding adjacent intervals should merge") { - set.add_interval_from_right(10, 12); - set.add_interval_from_right(13, 15); // This should merge - - for(int k=10; k <= 15; ++k) { - REQUIRE(set.pop_cur_time_from_left(k) == true); - } - REQUIRE(set.pop_cur_time_from_left(16) == false); - } - - - SECTION("Popping fully exhausts the list") { - set.add_interval_from_right(1, 1); - set.add_interval_from_right(3, 3); - - REQUIRE(set.pop_cur_time_from_left(1) == true); // Pop 1, first interval removed - REQUIRE(set.pop_cur_time_from_left(2) == false); // Gap - REQUIRE(set.pop_cur_time_from_left(3) == true); // Pop 3, second interval removed - - // The object should be in a clean state and can be added to again - set.add_interval_from_right(5, 5); - REQUIRE(set.pop_cur_time_from_left(5) == true); // Pop 5 - REQUIRE(set.pop_cur_time_from_left(5) == false); // Should be empty again - } -} - -#include "mtl_vector/MTLEngine.hpp" - -//#include "mtl_entt/MTLEngine.hpp" - -TEST_CASE("MTL Implementation Functionality", "[mtl_implementation]") { - - - /* - SECTION("2 Eventually Entt") { - std::vector> propositionInputs = { - {true, false, false, false, false, false}, // p - {false, false, false, false, true, false} // q - }; - std::vector expectedOutput = {false, false, true, true, true, false}; - entt::registry registry; - entt::entity p = registry.create(); - registry.emplace(p); - registry.emplace(p); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::OR, - 0, 1, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::EVENTUALLY, - 0, 2, 1, 2}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::EVENTUALLY, - 0, 3, 1, 2}); - std::vector output; - mtl_vector::run_evaluation(nodes, propositionInputs, output); - // A new set should not pop anything successfully. - REQUIRE(output == expectedOutput); - } - */ - - - SECTION("2 Eventually") { - std::vector> propositionInputs = { - {true, false, false, false, false, false}, // p - {false, false, false, false, true, false} // q - }; - std::vector expectedOutput = {false, false, true, true, true, false}; - std::vector nodes; - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::OR, - 0, 1, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::EVENTUALLY, - 0, 2, 1, 2}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::EVENTUALLY, - 0, 3, 1, 2}); - std::vector output; - mtl_vector::run_evaluation(nodes, propositionInputs, output); - // A new set should not pop anything successfully. - REQUIRE(output == expectedOutput); - } - - - SECTION("Always") { - std::vector> propositionInputs = { - {false, false, true, true, true, false}, // p - }; - std::vector expectedOutput = {true, false, false, false, true, true}; - std::vector nodes; - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::ALWAYS, - 0, 0, 1, 2}); - std::vector output; - mtl_vector::run_evaluation(nodes, propositionInputs, output); - // A new set should not pop anything successfully. - REQUIRE(output == expectedOutput); - } - - SECTION("Since") { - std::vector> propositionInputs = { - {false, false, true, true, true, false}, // p - {false, true, false, false, true, false}, // q - }; - std::vector expectedOutput = {false, false, false, true, true, false}; - std::vector nodes; - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::SINCE, - 0, 1, 2, 3}); - std::vector output; - mtl_vector::run_evaluation(nodes, propositionInputs, output); - // A new set should not pop anything successfully. - REQUIRE(output == expectedOutput); - } -} - -#include "parse_test_cases.hpp" - -TEST_CASE("MTL Timescales", "[timescales]") { - - - - BENCHMARK_ADVANCED("RecurGLB10")(Catch::Benchmark::Chronometer meter) { - std::vector nodes; - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::PROPOSITION, - 0, 0, 0, 0}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::EVENTUALLY, - 0, 0, 0, 10}); - nodes.push_back(mtl_vector::Node{interval_set::IntervalSet(), false, mtl_vector::NodeType::ALWAYS, - 0, 1, 0, 1000000}); - - std::vector output; - meter.measure([&] { - std::vector> propositionInputs = parseFile("/home/arinc/workspace/data-oriented-runtime-verif/largesuite/RecurGLB/RecurGLB10.jsonl"); - return mtl_vector::run_evaluation(nodes, propositionInputs, output);}); - }; - - -} - - -#include "double_buffer_interval_sets/interval_set.hpp" -#include - -// Use the namespace for cleaner tests -using namespace db_interval_set; - - -TEST_CASE("Basic Set Creation and Lifecycle", "[interval_set_correctness][core]") { - - SECTION("newHolder and destroyHolder") { - // This test mainly checks that the code compiles and doesn't crash. - // True memory leak detection would require a tool like Valgrind. - IntervalSetHolder holder = newHolder(128); - REQUIRE(holder.writeIndex == 0); - REQUIRE(holder.readBuffer != nullptr); - REQUIRE(holder.writeBuffer != nullptr); - destroyHolder(holder); - } - - SECTION("swapBuffers") { - IntervalSetHolder holder = newHolder(128); - Transition* readPtr = holder.readBuffer; - Transition* writePtr = holder.writeBuffer; - holder.writeIndex = 5; // Set a dummy index - - swapBuffers(holder); - - // Pointers should be swapped - REQUIRE(holder.readBuffer == writePtr); - REQUIRE(holder.writeBuffer == readPtr); - - // Write index should be reset - REQUIRE(holder.writeIndex == 0); - - destroyHolder(holder); - } - - SECTION("empty set") { - IntervalSetHolder holder = newHolder(128); - IntervalSet s = empty(holder); - - // Use the helper to convert back to intervals - std::vector v = toVectorIntervals(s); - - REQUIRE(v.empty()); - destroyHolder(holder); - } - - SECTION("fromInterval") { - IntervalSetHolder holder = newHolder(128); - - // Test a valid interval - IntervalSet s1 = fromInterval(holder, {10, 20}); - std::vector v1 = toVectorIntervals(s1); - REQUIRE(v1 == std::vector{{10, 20}}); - - // Test an empty interval - IntervalSet s2 = fromInterval(holder, {30, 30}); - std::vector v2 = toVectorIntervals(s2); - REQUIRE(v2.empty()); - - // Test an invalid interval - IntervalSet s3 = fromInterval(holder, {40, 30}); - std::vector v3 = toVectorIntervals(s3); - REQUIRE(v3.empty()); - - destroyHolder(holder); - } -} - - -TEST_CASE("Union Operations (unionSets)", "[interval_set_correctness][union]") { - IntervalSetHolder holder = newHolder(1024); - - // This is the core "double buffer" pattern for testing operations: - // 1. Create all your *input* sets in the writeBuffer. - // 2. swapBuffers() to move them to readBuffer. - // 3. Define IntervalSet structs pointing to the correct slices in readBuffer. - // 4. Run the operation (e.g., unionSets), which writes to writeBuffer. - // 5. Convert the *result* (which is in writeBuffer) to a vector for checking. - - SECTION("Simple Overlap") { - // A = {10, 20}, B = {15, 25} -> Union = {10, 25} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {15, 25}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 25}}); - } - - SECTION("Adjacent") { - // A = {10, 20}, B = {20, 30} -> Union = {10, 30} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {20, 30}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 30}}); - } - - SECTION("Disjoint") { - // A = {10, 20}, B = {30, 40} -> Union = {10, 20}, {30, 40} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {30, 40}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 20}, {30, 40}}); - } - - SECTION("Contained") { - // A = {10, 40}, B = {20, 30} -> Union = {10, 40} - auto s1_t = fromInterval(holder, {10, 40}); - auto s2_t = fromInterval(holder, {20, 30}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 40}}); - } - - SECTION("With Empty Set") { - // A = {10, 20}, B = {} -> Union = {10, 20} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = empty(holder); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 20}}); - } - - SECTION("Complex Multi-Interval Union") { - // A = {10, 20} U {30, 40} - // B = {15, 35} - // Result = {10, 40} - - // 1. Create {10, 20} and {30, 40} - auto i1_t = fromInterval(holder, {10, 20}); - auto i2_t = fromInterval(holder, {30, 40}); - swapBuffers(holder); - - // 2. Union them to create Set A - IntervalSet i1 = {holder.readBuffer, i1_t.startIndex, i1_t.endIndex}; - IntervalSet i2 = {holder.readBuffer, i2_t.startIndex, i2_t.endIndex}; - auto setA_t = unionSets(holder, i1, i2); // setA_t is in writeBuffer - - // 3. Create Set B in writeBuffer - auto setB_t = fromInterval(holder, {15, 35}); - - // 4. Swap. Now setA and setB are both in readBuffer - swapBuffers(holder); - - // 5. Define the final input sets - IntervalSet setA = {holder.readBuffer, setA_t.startIndex, setA_t.endIndex}; - IntervalSet setB = {holder.readBuffer, setB_t.startIndex, setB_t.endIndex}; - - // 6. Run the final operation - IntervalSet result = unionSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 40}}); - } - - destroyHolder(holder); -} - -TEST_CASE("Intersection Operations (intersectSets)", "[interval_set_correctness][intersect]") { - IntervalSetHolder holder = newHolder(1024); - - SECTION("Simple Overlap") { - // A = {10, 20}, B = {15, 25} -> Intersect = {15, 20} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {15, 25}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = intersectSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{15, 20}}); - } - - SECTION("Adjacent") { - // A = {10, 20}, B = {20, 30} -> Intersect = {} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {20, 30}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = intersectSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v.empty()); - } - - SECTION("Disjoint") { - // A = {10, 20}, B = {30, 40} -> Intersect = {} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = fromInterval(holder, {30, 40}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = intersectSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v.empty()); - } - - SECTION("Contained") { - // A = {10, 40}, B = {20, 30} -> Intersect = {20, 30} - auto s1_t = fromInterval(holder, {10, 40}); - auto s2_t = fromInterval(holder, {20, 30}); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = intersectSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{20, 30}}); - } - - SECTION("With Empty Set") { - // A = {10, 20}, B = {} -> Intersect = {} - auto s1_t = fromInterval(holder, {10, 20}); - auto s2_t = empty(holder); - swapBuffers(holder); - - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - IntervalSet setB = {holder.readBuffer, s2_t.startIndex, s2_t.endIndex}; - - IntervalSet result = intersectSets(holder, setA, setB); - std::vector v = toVectorIntervals(result); - - REQUIRE(v.empty()); - } - - destroyHolder(holder); -} - - -TEST_CASE("Negation Operations (negateSet)", "[interval_set_correctness][negate]") { - IntervalSetHolder holder = newHolder(1024); - Interval domain = {0, 100}; - - SECTION("Simple Negation") { - // A = {10, 20}, Domain = {0, 100} -> Negate = {0, 10}, {20, 100} - auto s1_t = fromInterval(holder, {10, 20}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{0, 10}, {20, 100}}); - } - - SECTION("Set touches domain start") { - // A = {0, 10}, Domain = {0, 100} -> Negate = {10, 100} - auto s1_t = fromInterval(holder, {0, 10}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 100}}); - } - - SECTION("Set touches domain end") { - // A = {90, 100}, Domain = {0, 100} -> Negate = {0, 90} - auto s1_t = fromInterval(holder, {90, 100}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{0, 90}}); - } - - SECTION("Set covers domain") { - // A = {0, 100}, Domain = {0, 100} -> Negate = {} - auto s1_t = fromInterval(holder, {0, 100}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v.empty()); - } - - SECTION("Empty set") { - // A = {}, Domain = {0, 100} -> Negate = {0, 100} - auto s1_t = empty(holder); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{0, 100}}); - } - - SECTION("Set partially outside domain") { - // A = {-10, 10}, Domain = {0, 100} -> Negate = {10, 100} - auto s1_t = fromInterval(holder, {-10, 10}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{10, 100}}); - } - - SECTION("Set fully outside domain") { - // A = {-20, -10}, Domain = {0, 100} -> Negate = {0, 100} - auto s1_t = fromInterval(holder, {-20, -10}); - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, s1_t.startIndex, s1_t.endIndex}; - - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{0, 100}}); - } - - SECTION("Multi-interval set") { - // A = {10, 20} U {50, 60} - // Domain = {0, 100} - // Negate = {0, 10}, {20, 50}, {60, 100} - - // 1. Create set A = {10, 20} U {50, 60} - auto i1_t = fromInterval(holder, {10, 20}); - auto i2_t = fromInterval(holder, {50, 60}); - swapBuffers(holder); - IntervalSet i1 = {holder.readBuffer, i1_t.startIndex, i1_t.endIndex}; - IntervalSet i2 = {holder.readBuffer, i2_t.startIndex, i2_t.endIndex}; - auto setA_t = unionSets(holder, i1, i2); - - // 2. Swap so setA is in readBuffer - swapBuffers(holder); - IntervalSet setA = {holder.readBuffer, setA_t.startIndex, setA_t.endIndex}; - - // 3. Run negation - IntervalSet result = negateSet(holder, setA, domain); - std::vector v = toVectorIntervals(result); - - REQUIRE(v == std::vector{{0, 10}, {20, 50}, {60, 100}}); - } - - destroyHolder(holder); -} - - -#include -#include // For [start, end) - -// A type alias for the Boost interval type matching yours -using BoostInterval = boost::icl::right_open_interval; - -// A type alias for the set -// Note: This is a complex template. We'll typedef it for sanity. -using BoostSet = boost::icl::interval_set< - int, // Domain type - std::less, // Comparator - BoostInterval // The interval type ->; - - -// C++ Standard Library -#include -#include -#include - -// --- Our code to test --- -using namespace db_interval_set; - -// --- Boost ICL Setup --- -using BoostInterval = boost::icl::right_open_interval; -using BoostSet = boost::icl::interval_set; - - -/** - * @brief Generates a vector of random intervals. - */ -std::vector generateRandomIntervals(int count, int maxStart, int maxDuration) { - // Use a fixed seed for reproducible benchmarks - std::mt19937 gen(1337); - std::uniform_int_distribution<> startDist(0, maxStart); - std::uniform_int_distribution<> durationDist(1, maxDuration); - - std::vector intervals; - intervals.reserve(count); - for (int i = 0; i < count; ++i) { - int start = startDist(gen); - int end = start + durationDist(gen); - intervals.push_back({start, end}); - } - return intervals; -} - -BoostSet createBoostSetFromIntervals(const std::vector& intervals) { - BoostSet set; - for (const auto& iv : intervals) { - set.add(BoostInterval(iv.start, iv.end)); - } - return set; -} - - -TEST_CASE("Performance Benchmarks", "[is_benchmark]") { - // --- 1. SETUP --- - // Generate a large set of test data. - // This is run ONCE before all benchmark sections. - const int N_A = 10000; - const int N_B = 10000; - const int TOTAL_N = N_A + N_B; - - auto intervalsA = generateRandomIntervals(N_A, 50000, 100); - auto intervalsB = generateRandomIntervals(N_B, 50000, 100); - - // Create a very large holder for your library - // Buffer needs to hold 2*N transitions (start/end) per set - // plus room for intermediate results. 4 * TOTAL_N is safe. - auto holder = newHolder(TOTAL_N * 4); - - // --- 2. PRE-BUILD SETS for Union/Intersect Tests --- - // We do this *outside* the benchmark macros so we only - // time the operation itself, not the setup. - - // Build DBSet A and B - auto dbSetA_t = createSetFromIntervals(holder, intervalsA); - auto dbSetB_t = createSetFromIntervals(holder, intervalsB); - swapBuffers(holder); // Move both sets to readBuffer - - // Create read-only handles to them - IntervalSet dbSetA = {holder.readBuffer, dbSetA_t.startIndex, dbSetA_t.endIndex}; - IntervalSet dbSetB = {holder.readBuffer, dbSetB_t.startIndex, dbSetB_t.endIndex}; - - // Build BoostSet A and B - BoostSet boostSetA = createBoostSetFromIntervals(intervalsA); - BoostSet boostSetB = createBoostSetFromIntervals(intervalsB); - - - // --- 3. RUN BENCHMARKS --- - - SECTION("Build (Construction)") { - // This benchmarks O(N log N) build performance - - BENCHMARK("DBSet: Build Set from " + std::to_string(TOTAL_N) + " intervals") { - // We must reset the write index each time - holder.writeIndex = 0; - return createSetFromIntervals(holder, intervalsA); // Using intervalsA as stand-in - }; - - BENCHMARK("Boost: Build Set from " + std::to_string(TOTAL_N) + " intervals") { - return createBoostSetFromIntervals(intervalsA); - }; - } - - SECTION("Union") { - // This benchmarks O(N+M) merge performance - - BENCHMARK("DBSet: Union (N=" + std::to_string(N_A) + ", M=" + std::to_string(N_B) + ")") { - holder.writeIndex = 0; // Reset output buffer - return unionSets(holder, dbSetA, dbSetB); - }; - - BENCHMARK("Boost: Union (N=" + std::to_string(N_A) + ", M=" + std::to_string(N_B) + ")") { - return boostSetA | boostSetB; - }; - } - - SECTION("Intersection") { - // This benchmarks O(N+M) intersection performance - - BENCHMARK("DBSet: Intersect (N=" + std::to_string(N_A) + ", M=" + std::to_string(N_B) + ")") { - holder.writeIndex = 0; // Reset output buffer - return intersectSets(holder, dbSetA, dbSetB); - }; - - BENCHMARK("Boost: Intersect (N=" + std::to_string(N_A) + ", M=" + std::to_string(N_B) + ")") { - return boostSetA & boostSetB; - }; - } - - // --- 4. CLEANUP --- - destroyHolder(holder); -} - - -#include "interval_set_scenario.hpp" -#include // <-- Added for std::tie - -TEST_CASE("Serial Update Benchmark", "[is_serial_benchmark]") { - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - // Tiny workload (for validation) - {50, 5, 100, 10000, 50}, - // Small workload - {100, 10, 1000, 50000, 100}, - // Large workload (WARNING: NEEDS ~20GB RAM) - // {500, 10, 5000, 50000, 100}, - // More sets, fewer intervals (WARNING: NEEDS ~10GB RAM) - // {1000, 10, 500, 50000, 100} - })); - - // Unpack parameters - int NUM_SETS, STEPS, INTERVALS_PER_SET, MAX_START, MAX_DURATION; - std::tie(NUM_SETS, STEPS, INTERVALS_PER_SET, MAX_START, MAX_DURATION) = params; - - // --- 2. DYNAMIC NAME (FIX 1) --- - // This creates a descriptive name for the output - std::string benchmark_name = - " (" + std::to_string(NUM_SETS) + " sets, " + - std::to_string(INTERVALS_PER_SET) + " iv/set)"; - - - // --- 3. COMMON DATA GENERATION --- - // This is run once *per generated scenario* - - std::vector operations; - std::mt19937 opGen(42); - std::uniform_int_distribution<> opDist(0, 1); - for(int i = 0; i < NUM_SETS; ++i) { - operations.push_back(opDist(opGen) == 1); - } - - std::mt19937 dataGen(1337); - std::vector> allIntervals(NUM_SETS); - for (int i = 0; i < NUM_SETS; ++i) { - allIntervals[i] = interval_set_scenario::generateRandomIntervals(dataGen, INTERVALS_PER_SET, MAX_START, MAX_DURATION); - } - - // --- 4. CORRECT BUFFER SIZE CALCULATION --- - // This is a O(N^2 * M) worst-case memory requirement. - // Use long long to prevent overflow during calculation. - const long long M = INTERVALS_PER_SET; - const long long N = NUM_SETS; - - // Sum of arithmetic series: (N * (N+1) / 2) * M * 2 transitions - const long long WORST_CASE_TRANSITIONS = M * N * (N + 1); - - // Add a 2x safety factor and check for overflow - // This size can be *enormous* (e.g., 20-40GB+ for your large tests) - const long long BUFFER_SIZE_LL = WORST_CASE_TRANSITIONS * 2; - if (BUFFER_SIZE_LL > std::numeric_limits::max()) { - // This will still probably fail to allocate, but at least it's correct - // In a real app, you might check if size_t is > max_alloc. - } - const size_t BUFFER_SIZE = static_cast(BUFFER_SIZE_LL); - - // --- 5. RUN BENCHMARKS (FIX 2) --- - // We use BENCHMARK_ADVANCED to reset state for each sample. - - BENCHMARK_ADVANCED("DBSet: Serial Update" + benchmark_name) (Catch::Benchmark::Chronometer meter) { - // This setup code runs *per sample* but is *not timed*. - - // Allocation might fail here if BUFFER_SIZE is too large - IntervalSetHolder holder = newHolder(BUFFER_SIZE); - - std::vector dbSets(NUM_SETS); - for (int i = 0; i < NUM_SETS; ++i) { - dbSets[i] = createSetFromIntervals(holder, allIntervals[i]); - } - swapBuffers(holder); // Move initial data to readBuffer - - // This is the code that gets timed - meter.measure([&] { - interval_set_scenario::run_scenario_serial_update(dbSets, holder, STEPS, operations); - }); - - // Teardown (not timed) - destroyHolder(holder); - }; - - BENCHMARK_ADVANCED("Boost: Serial Update" + benchmark_name) (Catch::Benchmark::Chronometer meter) { - // This setup code runs *per sample* but is *not timed*. - std::vector boostSets(NUM_SETS); - for (int i = 0; i < NUM_SETS; ++i) { - boostSets[i] = interval_set_scenario::createBoostSetFromIntervals(allIntervals[i]); - } - - // This is the code that gets timed - meter.measure([&] { - interval_set_scenario::run_scenario_boost(boostSets, STEPS, operations); - }); - - // (No teardown needed for Boost, vectors clean up themselves) - }; -} - - - - - -// Helper struct for testing segments -struct ExpectedSegment { - db_interval_set::Interval interval; - bool a; - bool b; - - // Overload operator== for Catch2 vector comparison - bool operator==(const ExpectedSegment& other) const { - return interval == other.interval && a == other.a && b == other.b; - } - - // Friend function for printing - friend std::ostream& operator<<(std::ostream& os, const ExpectedSegment& seg) { - os << "Seg{ " << seg.interval << ", A:" << (seg.a ? "T" : "F") - << ", B:" << (seg.b ? "T" : "F") << " }"; - return os; - } -}; - -// Helper function to run the iteration and collect results -std::vector runIteration( - db_interval_set::IntervalSet setA, - db_interval_set::IntervalSet setB, - db_interval_set::Interval domain) -{ - std::vector results; - - db_interval_set::SegmentIterator it = - db_interval_set::createSegmentIterator(setA, setB, domain); - - int segStart = it.interval.start; - bool segA = it.leftTruthy; - bool segB = it.rightTruthy; - - while (db_interval_set::getNextSegment(it)) { - int segEnd = it.interval.end; - - // Only add non-empty segments - if (segStart < segEnd) { - results.push_back(ExpectedSegment{ {segStart, segEnd}, segA, segB }); - } - - // Update state for the next segment - segStart = it.interval.start; - segA = it.leftTruthy; - segB = it.rightTruthy; - } - - return results; -} - - -TEST_CASE("SegmentIterator tests", "[SegmentIterator]") { - using namespace db_interval_set; - - IntervalSetHolder holder = newHolder(1024); - - // setA = [10, 20) U [30, 40) - IntervalSet setA = createSetFromIntervals(holder, { - {10, 20}, {30, 40} - }); - - // setB = [15, 35) - IntervalSet setB = fromInterval(holder, {15, 35}); - - // An empty set for testing - IntervalSet setEmpty = empty(holder); - - SECTION("Full Domain Iteration [0, 50)") { - Interval domain = {0, 50}; - std::vector results = runIteration(setA, setB, domain); - - std::vector expected = { - { {0, 10}, false, false }, - { {10, 15}, true, false }, - { {15, 20}, true, true }, - { {20, 30}, false, true }, - { {30, 35}, true, true }, - { {35, 40}, true, false }, - { {40, 50}, false, false } - }; - - REQUIRE(results == expected); - } - - SECTION("Partial Domain [12, 32)") { - Interval domain = {12, 32}; - std::vector results = runIteration(setA, setB, domain); - - std::vector expected = { - { {12, 15}, true, false }, - { {15, 20}, true, true }, - { {20, 30}, false, true }, - { {30, 32}, true, true } - }; - - REQUIRE(results == expected); - } - - SECTION("Domain before all intervals [0, 5)") { - Interval domain = {0, 5}; - std::vector results = runIteration(setA, setB, domain); - - std::vector expected = { - { {0, 5}, false, false } - }; - - REQUIRE(results == expected); - } - - SECTION("Domain after all intervals [45, 55)") { - Interval domain = {45, 55}; - std::vector results = runIteration(setA, setB, domain); - - std::vector expected= { - { {45, 55}, false, false } - }; - - REQUIRE(results == expected); - } - - SECTION("Empty Domain [5, 5)") { - Interval domain = {5, 5}; - std::vector results = runIteration(setA, setB, domain); - std::vector expected = {}; // No non-empty segments - - REQUIRE(results == expected); - } - - SECTION("Iteration with an empty set") { - Interval domain = {0, 20}; - // setA = empty, setB = [15, 35) (but we only care up to 20) - std::vector results = runIteration(setEmpty, setB, domain); - - std::vector expected = { - { {0, 15}, false, false }, - { {15, 20}, false, true } - }; - - REQUIRE(results == expected); - } - - SECTION("Iteration with two empty sets") { - Interval domain = {0, 20}; - std::vector results = runIteration(setEmpty, setEmpty, domain); - - std::vector expected = { - { {0, 20}, false, false } - }; - - REQUIRE(results == expected); - } - - SECTION("Domain exactly matching a transition [10, 15)") { - Interval domain = {10, 15}; - std::vector results = runIteration(setA, setB, domain); - - std::vector expected = { - { {10, 15}, true, false } - }; - - REQUIRE(results == expected); - } - - destroyHolder(holder); -} - - - -#include "dense_mtl/MTLEngine.hpp" -TEST_CASE("Dense Implementation tests", "[dense_tests]") { - using namespace std; - using namespace dense_vector; - using namespace db_interval_set; - - auto holder = newHolder(10000); - vector nodes; - auto p = Node{empty(holder), createSetFromIntervals(holder, {{7, 30}}), NodeType::TEST, 0, 0, 0, 0}; - nodes.push_back(p); - auto q = Node{empty(holder), createSetFromIntervals(holder, {{3, 8}}), NodeType::TEST, 0, 0, 0, 0}; - nodes.push_back(q); - auto since = Node{empty(holder), empty(holder), NodeType::SINCE, 0, 1, 18, 24}; - nodes.push_back(since); - - auto out = run_evaluation(nodes, holder, 0, 30, {true, true}); - auto converted = toVectorIntervals(out); - REQUIRE(converted == std::vector{{25, 30}}); - swapBuffers(holder); - - nodes[0].output = createSetFromIntervals(holder, {{30,35},{39,47}}); - nodes[1].output = createSetFromIntervals(holder, {{38,39}}); - out = run_evaluation(nodes, holder, 30, 47, {true, true}); - converted = toVectorIntervals(out); - REQUIRE(converted == std::vector{{30, 32}}); - swapBuffers(holder); - - nodes[0].output = createSetFromIntervals(holder, {{47,49},{63,75}}); - nodes[1].output = createSetFromIntervals(holder, {{70,75}}); - out = run_evaluation(nodes, holder, 47, 75, {true, true}); - converted = toVectorIntervals(out); - REQUIRE(converted == std::vector{}); - - swapBuffers(holder); - - nodes[0].output = createSetFromIntervals(holder, {{75,99}}); - nodes[1].output = createSetFromIntervals(holder, {{75,89}}); - out = run_evaluation(nodes, holder, 75, 99, {true, true}); - converted = toVectorIntervals(out); - REQUIRE(converted == std::vector{{88, 99}}); - - swapBuffers(holder); - destroyHolder(holder); -} - - -#include -#include -#include -#include -#include "json_reader.hpp" -TEST_CASE("Dense Timescales Tests", "[dense_tests]") { - - using namespace db_interval_set; - using namespace dense_vector; - - IntervalSetHolder holder = newHolder(1000000); - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; - std::vector nodes{p, once, always}; - - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/RecurGLB/Dense10/1M/RecurGLB10.jsonl"); - json_reader::TimescalesInput prevInput; - int step = 0; - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - REQUIRE(toVectorIntervals(output) == std::vector{{prevInput.time, newInput.time}}); - prevInput = newInput; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - }; - -} - -#include - - - - -TEST_CASE("Dense AbsentAQ", "[dense_benchmarks][AbsentAQ]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AbsentAQ " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; - Node since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY}; - Node implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; - std::vector nodes{q, p, once, notNode, since, implies, always}; - - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AbsentAQ/" + CONDENSATION + "/1M/AbsentAQ" + std::to_string(TIMINGS) +".jsonl"); - meter.measure([&] { - // Add these two lines to rewind the file for every run - input_file.clear(); // Clear all error flags (like the eofbit) - input_file.seekg(0); // Seek back to the beginning of the file - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - //std::cout << toVectorIntervals(output)[0].start << std::endl; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - -TEST_CASE("Dense AbsentBQR", "[dense_benchmarks][AbsentBQR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AbsentBQR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically({r} && !{q} && once {q} ) -> ((not {p}) since[a:b] {q}) - // Where [a:b] scales with TIMINGS. - // a = 3 * (TIMINGS / 10) - // b = TIMINGS - - const int since_a = 3 * (TIMINGS / 10); - const int since_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - - // Left side of '->' - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // index 3: !{q} (op: 0) - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // index 4: once {q} (op: 0) - - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // index 5: {r} && !{q} (ops: 2, 3) - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // index 6: ({r} && !{q}) && (once {q}) (ops: 5, 4) - - // Right side of '->' - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // index 7: !{p} (op: 1) - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, since_a, since_b}; // index 8: (not {p}) since[a:b] {q} (ops: 7, 0) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // index 9: (left_side) -> (right_side) (ops: 6, 8) - - // Root node - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // index 10: historically(...) (op: 9) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - not_q, // 3 - once_q, // 4 - and1, // 5 - and2, // 6 - not_p, // 7 - since_node, // 8 - implies_node, // 9 - always_node // 10 - }; - - // --- 3. RUN EVALUATION --- - // This file path assumes the "RecurGLB" dataset, as in your previous example - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AbsentBQR/" + CONDENSATION + "/1M/AbsentBQR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - -TEST_CASE("Dense AbsentBR", "[dense_benchmarks][AbsentBR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AbsentBR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically({r} -> (historically[:TIMINGS](not {p}))) - // We use TIMINGS for the [0, b] interval. - - const int inner_always_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - - // Right side of '->' - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // index 3: !{p} (op: 1) - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, inner_always_b}; // index 4: historically[:b](not {p}) (op: 3) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0}; // index 5: {r} -> (right_side) (ops: 2, 4) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // index 6: historically(...) (op: 5) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - not_p, // 3 - inner_always, // 4 - implies_node, // 5 - root_always // 6 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for AbsentBR dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AbsentBR/" + CONDENSATION + "/1M/AbsentBR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - -TEST_CASE("Dense AlwaysAQ", "[dense_benchmarks][AlwaysAQ]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AlwaysAQ " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically((once[:TIMINGS]({q})) -> ({p} since {q})) - // We use TIMINGS for the [0, b] interval on 'once'. - - const int once_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 (unused) - - // Left side of '->' - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, once_b}; // index 3: once[:b]({q}) (op: 0) - - // Right side of '->' - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY}; // index 4: {p} since {q} (ops: 1, 0) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0}; // index 5: (left_side) -> (right_side) (ops: 3, 4) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY}; // index 6: historically(...) (op: 5) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - once_q, // 3 - since_node, // 4 - implies_node, // 5 - root_always // 6 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for AlwaysAQ dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AlwaysAQ/" + CONDENSATION + "/1M/AlwaysAQ" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - -TEST_CASE("Dense AlwaysBQR", "[dense_benchmarks][AlwaysBQR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AlwaysBQR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically(({r} && !{q} && once {q}) -> ({p} since[a:b] {q})) - // Where [a:b] scales with TIMINGS. - // a = 3 * (TIMINGS / 10) - // b = TIMINGS - - const int since_a = 3 * (TIMINGS / 10); - const int since_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - - // Left side of '->' - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // index 3: !{q} (op: 0) - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // index 4: once {q} (op: 0) - - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // index 5: {r} && !{q} (ops: 2, 3) - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // index 6: ({r} && !{q}) && (once {q}) (ops: 5, 4) - - // Right side of '->' - Node not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // index 7: !{p} (op: 1) - - // --- THIS IS THE ONLY DIFFERENCE from AbsentBQR --- - // AbsentBQR used (not {p}), this one uses {p} - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, since_a, since_b}; // index 8: ({p}) since[a:b] {q} (ops: 1, 0) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0}; // index 9: (left_side) -> (right_side) (ops: 6, 8) - - // Root node - Node always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY}; // index 10: historically(...) (op: 9) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - not_q, // 3 - once_q, // 4 - and1, // 5 - and2, // 6 - not_p, // 7 (This node is now unused, but leaving it is harmless and keeps indices consistent) - since_node, // 8 - implies_node, // 9 - always_node // 10 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for AlwaysBQR dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AlwaysBQR/" + CONDENSATION + "/1M/AlwaysBQR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - - - -TEST_CASE("Dense AlwaysBR", "[dense_benchmarks][AlwaysBR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("AlwaysBR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically({r} -> (historically[:TIMINGS]({p}))) - // We use TIMINGS for the [0, b] interval. - - const int inner_always_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 (unused) - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - - // Right side of '->' - Node inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, inner_always_b}; // index 3: historically[:b]({p}) (op: 1) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0}; // index 4: {r} -> (right_side) (ops: 2, 3) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY}; // index 5: historically(...) (op: 4) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - inner_always, // 3 - implies_node, // 4 - root_always // 5 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for AlwaysBR dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/AlwaysBR/" + CONDENSATION + "/1M/AlwaysBR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - - -TEST_CASE("Dense RecurBQR", "[dense_benchmarks][RecurBQR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("RecurBQR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically(({r} && !{q} && once {q}) -> ((once[:TIMINGS]({p} or {q})) since {q})) - // We use TIMINGS for the [0, b] interval on 'once'. - - const int inner_once_b = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - - // Left side of '->' - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // index 3: !{q} (op: 0) - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // index 4: once {q} (op: 0) - Node and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0}; // index 5: {r} && !{q} (ops: 2, 3) - Node and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0}; // index 6: ({r} && !{q}) && (once {q}) (ops: 5, 4) - - // Right side of '->' - Node p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0}; // index 7: {p} or {q} (ops: 1, 0) - Node once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, inner_once_b}; // index 8: once[:b]({p} or {q}) (op: 7) - Node since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY}; // index 9: (right_side_inner) since {q} (ops: 8, 0) - - // Main implication - Node implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0}; // index 10: (left_side) -> (right_side) (ops: 6, 9) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY}; // index 11: historically(...) (op: 10) - - - // The vector of all nodes - std::vector nodes{ - q, p, r, // 0, 1, 2 - not_q, // 3 - once_q, // 4 - and1, // 5 - and2, // 6 - p_or_q, // 7 - once_p_or_q, // 8 - since_node, // 9 - implies_node, // 10 - root_always // 11 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for RecurBQR dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/RecurBQR/" + CONDENSATION + "/1M/RecurBQR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - -TEST_CASE("Dense RecurGLB", "[dense_benchmarks][RecurGLB]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("RecurGLB " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; - Node once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, TIMINGS}; - Node always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY}; - std::vector nodes{p, once, always}; - - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/RecurGLB/" + CONDENSATION + "/1M/RecurGLB" + std::to_string(TIMINGS) +".jsonl"); - meter.measure([&] { - // Add these two lines to rewind the file for every run - input_file.clear(); // Clear all error flags (like the eofbit) - input_file.seekg(0); // Seek back to the beginning of the file - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - //std::cout << toVectorIntervals(output)[0].start << std::endl; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - - -TEST_CASE("Dense RespondBQR", "[dense_benchmarks][RespondBQR]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("RespondBQR " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(1000000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically(({r} && !{q} && once {q}) -> ( (({s} -> once[a1:b1] {p}) and not( not({s}) since[a2:] {p})) since {q})) - - // Scale intervals based on TIMINGS - const int once_a = 3 * (TIMINGS / 10); - const int once_b = TIMINGS; - const int since_a = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [q, p, s, r] - Node q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 2 - Node r{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 3 - - // Left side of '->': A = ({r} && !{q} && once {q}) - Node not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0}; // index 4: !{q} (op: 0) - Node once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY}; // index 5: once {q} (op: 0) - Node and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0}; // index 6: {r} && !{q} (ops: 3, 4) - Node and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0}; // index 7: ({r} && !{q}) && once {q} (ops: 6, 5) - - // Right side of '->': B = (C since {q}) - // C = (D and E) - // D = ({s} -> once[a:b] {p}) - // E = not(F) - // F = (not({s}) since[a:] {p}) - - // Sub-formula D - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, once_a, once_b}; // index 8: once[a:b] {p} (op: 1) - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0}; // index 9: {s} -> once_p (ops: 2, 8) - - // Sub-formula F - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0}; // index 10: not({s}) (op: 2) - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, since_a, B_INFINITY}; // index 11: not({s}) since[a:] {p} (ops: 10, 1) - - // Sub-formula E - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0}; // index 12: not(F) (op: 11) - - // Sub-formula C - Node and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0}; // index 13: (D and E) (ops: 9, 12) - - // Sub-formula B - Node since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY}; // index 14: (C since {q}) (ops: 13, 0) - - // Main implication: A -> B - Node implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0}; // index 15: (A -> B) (ops: 7, 14) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY}; // index 16: historically(...) (op: 15) - - - // The vector of all nodes - std::vector nodes{ - q, p, s, r, // 0, 1, 2, 3 - not_q, // 4 - once_q, // 5 - and_A1, // 6 - and_A2, // 7 - once_p, // 8 - implies_D, // 9 - not_s, // 10 - since_F, // 11 - not_F, // 12 - and_C, // 13 - since_B, // 14 - implies_main, // 15 - root_always // 16 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for RespondBQR dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/RespondBQR/" + CONDENSATION + "/1M/RespondBQR" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - int maxBufferIndex = 0; - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - - - - -TEST_CASE("Dense RespondGLB", "[dense_benchmarks][RespondGLB]") { - - using namespace db_interval_set; - using namespace dense_vector; - - - // --- 1. SETUP PARAMS --- - auto params = GENERATE(table({ - {"Dense10", 10}, - {"Dense100", 10}, - {"Discrete", 10}, - {"Dense10", 100}, - {"Dense100", 100}, - {"Discrete", 100}, - {"Dense10", 1000}, - {"Dense100", 1000}, - {"Discrete", 1000}, - })); - - // Unpack parameters - std::string CONDENSATION; - int TIMINGS; - std::tie(CONDENSATION, TIMINGS) = params; - - std::string benchmarkName = CONDENSATION + " " + std::to_string(TIMINGS); - - BENCHMARK_ADVANCED("RespondGLB " + benchmarkName)(Catch::Benchmark::Chronometer meter) { - IntervalSetHolder holder = newHolder(100000); - - // --- 2. DEFINE FORMULA NODES --- - // Formula: historically(C) - // C = (D and E) - // D = ({s} -> once[a:b] {p}) - // E = not(F) - // F = (not({s}) since[a:] {p}) - - // Scale intervals based on TIMINGS - const int once_a = 3 * (TIMINGS / 10); - const int once_b = TIMINGS; - const int since_a = TIMINGS; - - // --- NODES (in topological order) --- - // Propositions (must be first, matching JSON input order) - // We assume input is [p, s] - Node p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 0 - Node s{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0}; // index 1 - - // Sub-formula D - Node once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, once_a, once_b}; // index 2: once[a:b] {p} (op: 0) - Node implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0}; // index 3: {s} -> once_p (ops: 1, 2) - - // Sub-formula F - Node not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0}; // index 4: not({s}) (op: 1) - Node since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, since_a, B_INFINITY}; // index 5: not({s}) since[a:] {p} (ops: 4, 0) - - // Sub-formula E - Node not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0}; // index 6: not(F) (op: 5) - - // Sub-formula C - Node and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0}; // index 7: (D and E) (ops: 3, 6) - - // Root node - Node root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY}; // index 8: historically(C) (op: 7) - - - // The vector of all nodes - std::vector nodes{ - p, s, // 0, 1 - once_p, // 2 - implies_D, // 3 - not_s, // 4 - since_F, // 5 - not_F, // 6 - and_C, // 7 - root_always // 8 - }; - - // --- 3. RUN EVALUATION --- - // Updated file path for RespondGLB dataset - std::ifstream input_file("/home/arinc/workspace/data-oriented-runtime-verif/fullsuite/RespondGLB/" + CONDENSATION + "/1M/RespondGLB" + std::to_string(TIMINGS) +".jsonl"); - - meter.measure([&] { - // Rewind the file for every benchmark run - input_file.clear(); - input_file.seekg(0); - - json_reader::TimescalesInput prevInput; - int step = 0; - IntervalSet finalOutput; - - for (std::string line; std::getline(input_file, line);){ - if (step != 0) { - auto newInput = json_reader::read_line(line); - // Pass the proposition vector from the *previous* step - IntervalSet output = run_evaluation(nodes, holder, prevInput.time, newInput.time, prevInput.propositions); - prevInput = newInput; - finalOutput = output; - swapBuffers(holder); - } - else { - prevInput = json_reader::read_line(line); - } - step++; - } - return finalOutput; - }); - - }; -} - - From ec13cebe2b1464e4e3cda1ad2476f16912781ad0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ar=C4=B1n=C3=A7=20Demir?= Date: Sat, 13 Dec 2025 15:08:48 +0300 Subject: [PATCH 6/6] exclude main file from code coverage. --- tests/CMakeLists.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 5e14c91..1682f5f 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -45,6 +45,7 @@ if(ENABLE_COVERAGE) --exclude "${CMAKE_BINARY_DIR}" --exclude "${CMAKE_SOURCE_DIR}/tests/" --exclude "${CMAKE_SOURCE_DIR}/benchmarks/" + --exclude "${CMAKE_SOURCE_DIR}/src/main.cpp" --gcov-ignore-parse-errors --gcov-ignore-errors=all --exclude-throw-branches @@ -52,9 +53,12 @@ if(ENABLE_COVERAGE) COMMAND ${CMAKE_COMMAND} -E echo "--------------------------------------------------" COMMAND ${CMAKE_COMMAND} -E echo "Coverage Filter: ${CMAKE_SOURCE_DIR}/src/" + COMMAND ${CMAKE_COMMAND} -E echo "Coverage Filter: ${CMAKE_SOURCE_DIR}/src/" + COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 1: ${CMAKE_BINARY_DIR}" COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 2: ${CMAKE_SOURCE_DIR}/tests/" COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 3: ${CMAKE_SOURCE_DIR}/benchmarks/" + COMMAND ${CMAKE_COMMAND} -E echo "Exclude Path 3: ${CMAKE_SOURCE_DIR}/src/main.cpp" COMMAND ${CMAKE_COMMAND} -E echo "--------------------------------------------------"