Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/IDNI/tau-lang
Browse files Browse the repository at this point in the history
  • Loading branch information
@castrod
castrod committed Jan 21, 2025
2 parents 624b33e + 2101998 commit 3373867
Show file tree
Hide file tree
Showing 5 changed files with 54 additions and 71 deletions.
2 changes: 1 addition & 1 deletion src/normal_forms.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2462,7 +2462,7 @@ tau<BAs...> shift_io_vars_in_fm (const tau<BAs...>& 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
Expand Down
8 changes: 6 additions & 2 deletions src/normalizer.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,12 +282,15 @@ bool are_nso_equivalent(tau<BAs...> n1, tau<BAs...> n2) {
BOOST_LOG_TRIVIAL(debug) << "(I) -- wff: " << build_wff_and(imp1, imp2);

auto dir1 = normalizer_step<BAs...>(imp1);
assert((dir1 == _T<BAs...> || dir1 == _F<BAs...>));
assert((dir1 == _T<BAs...> || dir1 == _F<BAs...> || find_top(dir1,
is_non_terminal<tau_parser::constraint, BAs...>)));
if (dir1 == _F<BAs...>) {
BOOST_LOG_TRIVIAL(debug) << "(I) -- End are_nso_equivalent: " << dir1;
return false;
}
auto dir2 = normalizer_step<BAs...>(imp2);
assert((dir2 == _T<BAs...> || dir2 == _F<BAs...> || find_top(dir2,
is_non_terminal<tau_parser::constraint, BAs...>)));
bool res = (dir1 == _T<BAs...> && dir2 == _T<BAs...>);

BOOST_LOG_TRIVIAL(debug) << "(I) -- End are_nso_equivalent: " << res;
Expand Down Expand Up @@ -330,7 +333,8 @@ bool is_nso_impl (tau<BAs...> n1, tau<BAs...> n2) {
BOOST_LOG_TRIVIAL(debug) << "(I) -- wff: " << imp;

auto res = normalizer_step<BAs...>(imp);
assert((res == _T<BAs...> || res == _F<BAs...>));
assert((res == _T<BAs...> || res == _F<BAs...> || find_top(res,
is_non_terminal<tau_parser::constraint, BAs...>)));
BOOST_LOG_TRIVIAL(debug) << "(I) -- End is_nso_impl: " << res;
return res == _T<BAs...>;
}
Expand Down
48 changes: 21 additions & 27 deletions src/satisfiability.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -688,7 +688,7 @@ tau<BAs...> create_guard(const auto& io_vars, const int_t number) {

// Assumes single normalized Tau DNF clause
template<typename... BAs>
tau<BAs...> transform_to_eventual_variables(const tau<BAs...>& fm) {
tau<BAs...> transform_to_eventual_variables(const tau<BAs...>& fm, bool reset_ctn_stream) {
using p = tau_parser;
auto smt_fms = select_top(fm, is_child_non_terminal<p::wff_sometimes, BAs...>);
if (smt_fms.empty()) return fm;
Expand All @@ -713,6 +713,11 @@ tau<BAs...> transform_to_eventual_variables(const tau<BAs...>& fm) {
auto st_io_vars = select_top(smt_fms[n], is_child_non_terminal<p::io_var, BAs...>);
int_t st_lookback = get_max_shift(st_io_vars);

// Transform constant time constraints to io var in sometimes statement
tau<BAs...> ctn_initials = _T<BAs...>, ctn_assm = _T<BAs...>;
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<p::io_var, BAs...>);

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<BAs...>(ss.str(), "t"));
Expand Down Expand Up @@ -751,6 +756,9 @@ tau<BAs...> transform_to_eventual_variables(const tau<BAs...>& 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<BAs...>;
Expand Down Expand Up @@ -813,7 +821,6 @@ template<typename... BAs>
tau<BAs...> to_unbounded_continuation(const tau<BAs...>& ubd_aw_continuation,
const tau<BAs...>& 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";

Expand All @@ -838,21 +845,9 @@ tau<BAs...> to_unbounded_continuation(const tau<BAs...>& ubd_aw_continuation,
is_child_non_terminal<p::io_var, BAs...>);

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<p::constraint, BAs...>)) {
// Transform constraint to stream
tau<BAs...> ctn_initials = _T<BAs...>, ctn_rules = _T<BAs...>;
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<p::io_var, BAs...>);
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<p::constraint, BAs...>));

int_t point_after_inits = get_max_initial<BAs...>(io_vars) + 1;
// Shift flags in order to match lookback of always part
Expand Down Expand Up @@ -976,15 +971,14 @@ tau<BAs...> transform_to_execution(const tau<BAs...>& fm, const bool output = fa
auto aw_fm = find_top(fm, is_child_non_terminal<p::wff_always, BAs...>);
tau<BAs...> ev_t;
tau<BAs...> 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);
std::map<tau<BAs...>, tau<BAs...> > changes = {
{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
Expand All @@ -994,8 +988,7 @@ tau<BAs...> transform_to_execution(const tau<BAs...>& 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
Expand All @@ -1017,8 +1010,7 @@ tau<BAs...> transform_to_execution(const tau<BAs...>& fm, const bool output = fa
tau<BAs...> res;
if (aw_after_ev.value() != _F<BAs...> && !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);
Expand Down Expand Up @@ -1051,8 +1043,9 @@ bool is_tau_formula_sat (const tau<BAs...>& normalized_fm, const bool output = f
// Check for temporal formulas if f1 implies f2
template<typename... BAs>
bool is_tau_impl (const tau<BAs...>& f1, const tau<BAs...>& 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) {
Expand All @@ -1067,8 +1060,9 @@ bool is_tau_impl (const tau<BAs...>& f1, const tau<BAs...>& f2) {
template<typename... BAs>
bool are_tau_equivalent (const tau<BAs...>& f1, const tau<BAs...>& 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) {
Expand Down
10 changes: 7 additions & 3 deletions src/splitter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,19 +83,23 @@ tau<BAs...> split(const tau<BAs...>& 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<typename... BAs>
bool is_splitter(const tau<BAs...>& fm, const tau<BAs...>& splitter, const tau<BAs...>& spec) {
bool is_splitter(const tau<BAs...>& fm, const tau<BAs...>& splitter, const tau<BAs...>& 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<BAs...>, tau<BAs...>> 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<BAs...>) return true;
!= _F<BAs...>) {
assert(is_nso_impl(splitter, fm));
return true;
}
}
return false;
}
Expand Down
57 changes: 19 additions & 38 deletions tests/integration/test_integration-splitter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,35 +32,31 @@ TEST_SUITE("Tau_splitter_upper_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_2") {
const char *sample = "xyz != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_3") {
const char *sample = "x = 0 && w != 0 || yz = 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_4") {
const char *sample = "x = 0 && w != 0 || y|z != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_5") {
Expand All @@ -85,25 +81,22 @@ TEST_SUITE("Tau_splitter_upper_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, 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<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s, fm));
}

TEST_CASE("Tau_splitter_9") {
const char *sample = "(always o1[t] = i1[t]).";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::upper);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s, fm));
}
}

Expand All @@ -113,35 +106,31 @@ TEST_SUITE("Tau_splitter_middle_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_2") {
const char *sample = "xyz != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_3") {
const char *sample = "x = 0 && w != 0 || yz = 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_4") {
const char *sample = "x = 0 && w != 0 || y|z != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, 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).";
Expand All @@ -165,16 +154,14 @@ TEST_SUITE("Tau_splitter_middle_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, 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<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::middle);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s, fm));
}
}

Expand All @@ -184,35 +171,31 @@ TEST_SUITE("Tau_splitter_lower_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_2") {
const char *sample = "xyz != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_3") {
const char *sample = "x = 0 && w != 0 || yz = 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(!check_uniter_const.has_value());
CHECK(is_splitter(fm, s));
}

TEST_CASE("Tau_splitter_4") {
const char *sample = "x = 0 && w != 0 || y|z != 0.";
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, 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).";
Expand All @@ -236,16 +219,14 @@ TEST_SUITE("Tau_splitter_lower_tests") {
auto src = make_tau_source(sample);
auto fm = make_nso_rr_using_factory<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, 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<tau_ba<sbf_ba>, sbf_ba>(src).value().main;
auto s = tau_splitter(fm, splitter_type::lower);
auto check_uniter_const = find_top(s, is_non_terminal<tau_parser::uninterpreted_constant, tau_ba<sbf_ba>, sbf_ba>);
CHECK(check_uniter_const.has_value());
CHECK(is_splitter(fm, s, fm));
}
}

Expand Down

0 comments on commit 3373867

Please sign in to comment.