From a025d346f3e92fdcc63ac6bcd5e1854b11338b4d Mon Sep 17 00:00:00 2001 From: Lucca Tiemens Date: Fri, 17 Jan 2025 18:05:35 +0100 Subject: [PATCH 1/2] Fix for conversion of constant time constraint to flag in sometimes statement. --- src/normal_forms.h | 2 +- src/satisfiability.h | 38 +++++++++++++++----------------------- 2 files changed, 16 insertions(+), 24 deletions(-) diff --git a/src/normal_forms.h b/src/normal_forms.h index 32c8d79..e92b24a 100644 --- a/src/normal_forms.h +++ b/src/normal_forms.h @@ -2462,7 +2462,7 @@ tau shift_io_vars_in_fm (const tau& fm, const auto& io_vars, con get_io_name(io_var), var_shift + shift)); } } - return replace(fm, changes); + return replace(fm, changes); } // Assumes a single DNF clause and normalizes the "always" parts into one diff --git a/src/satisfiability.h b/src/satisfiability.h index 5615c06..082dd56 100644 --- a/src/satisfiability.h +++ b/src/satisfiability.h @@ -688,7 +688,7 @@ tau create_guard(const auto& io_vars, const int_t number) { // Assumes single normalized Tau DNF clause template -tau transform_to_eventual_variables(const tau& fm) { +tau transform_to_eventual_variables(const tau& fm, bool reset_ctn_stream) { using p = tau_parser; auto smt_fms = select_top(fm, is_child_non_terminal); if (smt_fms.empty()) return fm; @@ -713,6 +713,11 @@ tau transform_to_eventual_variables(const tau& fm) { auto st_io_vars = select_top(smt_fms[n], is_child_non_terminal); int_t st_lookback = get_max_shift(st_io_vars); + // Transform constant time constraints to io var in sometimes statement + tau ctn_initials = _T, ctn_assm = _T; + smt_fms[n] = transform_ctn_to_streams(smt_fms[n], ctn_initials, ctn_assm, st_lookback); + st_io_vars = select_top(smt_fms[n], is_child_non_terminal); + std::stringstream ss; ss << "_e" << n; // Build the eventual var flags based on the maximal lookback auto eNt_without_lookback = wrap(p::bf, build_io_out(ss.str(), "t")); @@ -751,6 +756,9 @@ tau transform_to_eventual_variables(const tau& fm) { build_wff_and(eN0_is_not_zero, build_wff_imply(eNt_prev_is_zero, eNt_is_zero))); + // Add flag assumptions from constant time constraints + ev_assm = build_wff_and(ev_assm, build_wff_and(ctn_initials, ctn_assm)); + ev_collection = build_bf_or(ev_collection, eNt_without_lookback); } auto res = _T; @@ -813,7 +821,6 @@ template tau to_unbounded_continuation(const tau& ubd_aw_continuation, const tau& ev_var_flags, const auto& original_aw, - const bool reset_ctn_streams, const bool output = false) { BOOST_LOG_TRIVIAL(debug) << "(I) -- Begin to_unbounded_continuation"; @@ -838,21 +845,9 @@ tau to_unbounded_continuation(const tau& ubd_aw_continuation, is_child_non_terminal); int_t time_point = get_max_shift(io_vars); - // Check if a constant time constraint is still present - // Can happen due to constraints in sometimes clause - if (find_top(aw, is_non_terminal)) { - // Transform constraint to stream - tau ctn_initials = _T, ctn_rules = _T; - aw = transform_ctn_to_streams(aw, ctn_initials, ctn_rules, time_point, reset_ctn_streams); - aw = build_wff_and(ctn_rules, aw); - aw = build_wff_and(ctn_initials, aw); - // The lookback cannot be 0 due to presents of eventual variables - // Therefore, no adjustment of aw is needed - - // Search again for io_vars after transformation - io_vars = select_top(aw, is_child_non_terminal); - time_point = get_max_shift(io_vars); - } + + // There must not be a constant time constraint at this point + assert(!find_top(aw, is_non_terminal)); int_t point_after_inits = get_max_initial(io_vars) + 1; // Shift flags in order to match lookback of always part @@ -976,7 +971,6 @@ tau transform_to_execution(const tau& fm, const bool output = fa auto aw_fm = find_top(fm, is_child_non_terminal); tau ev_t; tau ubd_aw_fm; - bool reset_ctn_stream = false; if (aw_fm.has_value()) { // If there is an always part, replace it with its unbound continuation ubd_aw_fm = always_to_unbounded_continuation(aw_fm.value(), output); @@ -984,7 +978,7 @@ tau transform_to_execution(const tau& fm, const bool output = fa {aw_fm.value(), build_wff_always(ubd_aw_fm)} }; auto ubd_fm = replace(fm, changes); - ev_t = transform_to_eventual_variables(ubd_fm); + ev_t = transform_to_eventual_variables(ubd_fm, false); // Check if there is a sometimes present if (ev_t == ubd_fm) { #ifdef TAU_CACHE @@ -994,8 +988,7 @@ tau transform_to_execution(const tau& fm, const bool output = fa return elim_aw(ubd_fm); } } else { - reset_ctn_stream = true; - ev_t = transform_to_eventual_variables(fm); + ev_t = transform_to_eventual_variables(fm, true); // Check if there is a sometimes present if (ev_t == fm) { #ifdef TAU_CACHE @@ -1017,8 +1010,7 @@ tau transform_to_execution(const tau& fm, const bool output = fa tau res; if (aw_after_ev.value() != _F && !st.empty()) res = normalize_non_temp(to_unbounded_continuation( - aw_after_ev.value(), st[0], ubd_aw_fm, reset_ctn_stream, - output)); + aw_after_ev.value(), st[0], ubd_aw_fm, output)); else res = aw_after_ev.value(); BOOST_LOG_TRIVIAL(debug) << "(I) End transform_to_execution"; res = elim_aw(res); From 210199832c42ae195f77d074129b896130879727 Mon Sep 17 00:00:00 2001 From: Lucca Tiemens Date: Mon, 20 Jan 2025 16:21:39 +0100 Subject: [PATCH 2/2] Improvements in splitter tests. --- src/normalizer.h | 8 ++- src/satisfiability.h | 10 ++-- src/splitter.h | 10 +++- .../integration/test_integration-splitter.cpp | 57 +++++++------------ 4 files changed, 38 insertions(+), 47 deletions(-) diff --git a/src/normalizer.h b/src/normalizer.h index b392ed6..94cf4bf 100644 --- a/src/normalizer.h +++ b/src/normalizer.h @@ -282,12 +282,15 @@ bool are_nso_equivalent(tau n1, tau n2) { BOOST_LOG_TRIVIAL(debug) << "(I) -- wff: " << build_wff_and(imp1, imp2); auto dir1 = normalizer_step(imp1); - assert((dir1 == _T || dir1 == _F)); + assert((dir1 == _T || dir1 == _F || find_top(dir1, + is_non_terminal))); if (dir1 == _F) { BOOST_LOG_TRIVIAL(debug) << "(I) -- End are_nso_equivalent: " << dir1; return false; } auto dir2 = normalizer_step(imp2); + assert((dir2 == _T || dir2 == _F || find_top(dir2, + is_non_terminal))); bool res = (dir1 == _T && dir2 == _T); BOOST_LOG_TRIVIAL(debug) << "(I) -- End are_nso_equivalent: " << res; @@ -330,7 +333,8 @@ bool is_nso_impl (tau n1, tau n2) { BOOST_LOG_TRIVIAL(debug) << "(I) -- wff: " << imp; auto res = normalizer_step(imp); - assert((res == _T || res == _F)); + assert((res == _T || res == _F || find_top(res, + is_non_terminal))); BOOST_LOG_TRIVIAL(debug) << "(I) -- End is_nso_impl: " << res; return res == _T; } diff --git a/src/satisfiability.h b/src/satisfiability.h index 082dd56..73e537d 100644 --- a/src/satisfiability.h +++ b/src/satisfiability.h @@ -1043,8 +1043,9 @@ bool is_tau_formula_sat (const tau& normalized_fm, const bool output = f // Check for temporal formulas if f1 implies f2 template bool is_tau_impl (const tau& f1, const tau& f2) { - auto imp_check = normalizer_step(build_wff_imply(f1,f2)); - imp_check = to_dnf2(build_wff_neg(imp_check)); + auto f1_norm = normalizer_step(f1); + auto f2_norm = normalizer_step(f2); + auto imp_check = normalize_with_temp_simp((build_wff_neg(build_wff_imply(f1_norm,f2_norm)))); auto clauses = get_dnf_wff_clauses(imp_check); // Now check that each disjunct is not satisfiable for (const auto& c : clauses) { @@ -1059,8 +1060,9 @@ bool is_tau_impl (const tau& f1, const tau& f2) { template bool are_tau_equivalent (const tau& f1, const tau& f2) { // Negate equivalence for unsat check - auto equiv_check = normalizer_step(build_wff_equiv(f1, f2)); - equiv_check = to_dnf2(build_wff_neg(equiv_check)); + auto f1_norm = normalizer_step(f1); + auto f2_norm = normalizer_step(f2); + auto equiv_check = normalize_with_temp_simp(build_wff_neg(build_wff_equiv(f1_norm, f2_norm))); auto clauses = get_dnf_wff_clauses(equiv_check); // Now check that each disjunct is not satisfiable for (const auto& c : clauses) { diff --git a/src/splitter.h b/src/splitter.h index bbfe3c5..4e4f789 100644 --- a/src/splitter.h +++ b/src/splitter.h @@ -83,19 +83,23 @@ tau split(const tau& fm, const size_t fm_type, bool is_cnf, // If we check a non-temporal Tau formula, it suffices to place it in "fm" and // the proposed splitter in "splitter". template -bool is_splitter(const tau& fm, const tau& splitter, const tau& spec) { +bool is_splitter(const tau& fm, const tau& splitter, const tau& spec = nullptr) { if (spec) { // We are dealing with a temporal formula if (!are_tau_equivalent(splitter, fm)) { + assert(is_tau_impl(splitter, fm)); std::map, tau> c = {{fm, splitter}}; - auto new_spec = normalizer_step(replace(spec, c)); + auto new_spec = normalize_with_temp_simp(replace(spec, c)); if (is_tau_formula_sat(new_spec)) return true; } } else { // We are dealing with a non-temporal formula if (!are_nso_equivalent(splitter, fm) && normalizer_step(splitter) - != _F) return true; + != _F) { + assert(is_nso_impl(splitter, fm)); + return true; + } } return false; } diff --git a/tests/integration/test_integration-splitter.cpp b/tests/integration/test_integration-splitter.cpp index ee650b5..353e6f6 100644 --- a/tests/integration/test_integration-splitter.cpp +++ b/tests/integration/test_integration-splitter.cpp @@ -32,8 +32,7 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_2") { @@ -41,8 +40,7 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_3") { @@ -50,8 +48,7 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_4") { @@ -59,8 +56,7 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_5") { @@ -85,16 +81,14 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } TEST_CASE("Tau_splitter_8") { const char *sample = "(always o1[t] = 1)."; auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } TEST_CASE("Tau_splitter_9") { @@ -102,8 +96,7 @@ TEST_SUITE("Tau_splitter_upper_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::upper); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } } @@ -113,8 +106,7 @@ TEST_SUITE("Tau_splitter_middle_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_2") { @@ -122,8 +114,7 @@ TEST_SUITE("Tau_splitter_middle_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_3") { @@ -131,8 +122,7 @@ TEST_SUITE("Tau_splitter_middle_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_4") { @@ -140,8 +130,7 @@ TEST_SUITE("Tau_splitter_middle_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_5") { const char *sample = "(always ([t>0] -> (o1[t] = 0 || o1[t] = 1))) && (sometimes o1[t] != 0 && o1[t] != 1) && (sometimes o1[t] = 0)."; @@ -165,16 +154,14 @@ TEST_SUITE("Tau_splitter_middle_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } TEST_CASE("Tau_splitter_8") { const char *sample = "(always o1[t] = 1)."; auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::middle); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } } @@ -184,8 +171,7 @@ TEST_SUITE("Tau_splitter_lower_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_2") { @@ -193,8 +179,7 @@ TEST_SUITE("Tau_splitter_lower_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_3") { @@ -202,8 +187,7 @@ TEST_SUITE("Tau_splitter_lower_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_4") { @@ -211,8 +195,7 @@ TEST_SUITE("Tau_splitter_lower_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(!check_uniter_const.has_value()); + CHECK(is_splitter(fm, s)); } TEST_CASE("Tau_splitter_5") { const char *sample = "(always ([t>0] -> (o1[t] = 0 || o1[t] = 1))) && (sometimes o1[t] != 0 && o1[t] != 1) && (sometimes o1[t] = 0)."; @@ -236,16 +219,14 @@ TEST_SUITE("Tau_splitter_lower_tests") { auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } TEST_CASE("Tau_splitter_8") { const char *sample = "(always o1[t] = 1)."; auto src = make_tau_source(sample); auto fm = make_nso_rr_using_factory, sbf_ba>(src).value().main; auto s = tau_splitter(fm, splitter_type::lower); - auto check_uniter_const = find_top(s, is_non_terminal, sbf_ba>); - CHECK(check_uniter_const.has_value()); + CHECK(is_splitter(fm, s, fm)); } }