Skip to content

Added test case for rewrites of expressions to use leq instead of eq #220

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
srba merged 2 commits into from
Jul 17, 2026
Merged

Added test case for rewrites of expressions to use leq instead of eq #220

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
579ccf0
added test case for rewrites of expressions to use leq instead of eq
mtygesen Jul 6, 2026
6c3e918
fix workflow error
mtygesen Jul 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions boost_tests/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ add_executable (BinaryPrinterTests BinaryPrinterTests.cpp)
add_executable (XMLPrinterTests XMLPrinterTests.cpp)
add_executable (PQLParserTests PQLParserTests.cpp)
add_executable (PredicateCheckerTests PredicateCheckerTests.cpp)
add_executable (PushNegationTests PushNegationTests.cpp)
add_executable (reachability reachability_test.cpp)
add_executable (ltl ltl_test.cpp)
add_executable (hyper_ltl hyper_ltl_test.cpp)
Expand All @@ -23,6 +24,7 @@ target_link_libraries(BinaryPrinterTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic
target_link_libraries(XMLPrinterTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(PQLParserTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(PredicateCheckerTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(PushNegationTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(reachability PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(ltl PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
target_link_libraries(hyper_ltl PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
Expand All @@ -35,6 +37,7 @@ add_test(NAME BinaryPrinterTests COMMAND BinaryPrinterTests)
add_test(NAME XMLPrinterTests COMMAND XMLPrinterTests)
add_test(NAME PQLParserTests COMMAND PQLParserTests)
add_test(NAME PredicateCheckerTests COMMAND PredicateCheckerTests)
add_test(NAME PushNegationTests COMMAND PushNegationTests)
add_test(NAME reachability COMMAND reachability)
add_test(NAME ltl COMMAND ltl)
add_test(NAME hyper_ltl COMMAND hyper_ltl)
Expand Down
94 changes: 61 additions & 33 deletions boost_tests/PushNegationTests.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,12 @@

using namespace PetriEngine::PQL;

inline std::shared_ptr<IdentifierExpr> make_id(const std::string& name) {
return std::make_shared<IdentifierExpr>(std::make_shared<const std::string>(name));
}

BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) {
auto identifier = std::make_shared<IdentifierExpr>("a");
auto identifier = make_id("a");
auto literal = std::make_shared<LiteralExpr>(1);
auto condition = std::make_shared<NotCondition>(
std::make_shared<LessThanCondition>(
Expand All @@ -30,35 +33,60 @@ BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) {
"Less than operands should be swapped");
}

//BOOST_AUTO_TEST_CASE(AirplaneLD_PT_0050_3) {
// auto cond = std::make_shared<NotCondition>(std::make_shared<NotCondition>(
// std::make_shared<EGCondition>(
// std::make_shared<AFCondition>(
// std::make_shared<NotCondition>(
// std::make_shared<ECondition>(
// std::make_shared<UntilCondition>(
// std::make_shared<LessThanOrEqualCondition>(
// std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
// std::make_shared<IdentifierExpr>(
// "P3"),
// std::make_shared<IdentifierExpr>(
// "stp5")
// }),
// std::make_shared<LiteralExpr>(12)
// ),
// std::make_shared<LessThanOrEqualCondition>(
// std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
// std::make_shared<IdentifierExpr>(
// "SpeedPossibleVal_38"),
// std::make_shared<IdentifierExpr>(
// "SpeedPossibleVal_26")
// }),
// std::make_shared<LiteralExpr>(35)
// )
// )
// )
// )
// )
// )
// ));
//}
// Regression test for wrong answer in bug #2156598: (P0 - P1) - P2 == 0 must not be rewritten to (P0 - P1) - P2 <= 0, since the subtraction can be negative.
BOOST_AUTO_TEST_CASE(equal_zero_with_subtraction_is_not_rewritten) {
auto subtraction = std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
make_id("P0"),
make_id("P1")
}),
make_id("P2")
});
auto condition = std::make_shared<EqualCondition>(
subtraction,
std::make_shared<LiteralExpr>(0)
);
auto stats = negstat_t();

auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);

BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<EqualCondition>(res) != nullptr,
"Equality with possibly negative expression should stay an EqualCondition");
}

BOOST_AUTO_TEST_CASE(not_equal_zero_with_subtraction_is_not_rewritten) {
auto subtraction = std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
make_id("P0"),
make_id("P1")
});
auto condition = std::make_shared<NotCondition>(
std::make_shared<EqualCondition>(
subtraction,
std::make_shared<LiteralExpr>(0)
)
);
auto stats = negstat_t();

auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);

BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<NotEqualCondition>(res) != nullptr,
"Negated equality with possibly negative expression should become NotEqualCondition");
}

// Keep rewrite for non-negative expressions: P0 + P1 == 0 -> P0 + P1 <= 0
BOOST_AUTO_TEST_CASE(equal_zero_with_plus_is_rewritten_to_leq) {
auto sum = std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
make_id("P0"),
make_id("P1")
});
auto condition = std::make_shared<EqualCondition>(
sum,
std::make_shared<LiteralExpr>(0)
);
auto stats = negstat_t();

auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);

BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<LessThanOrEqualCondition>(res) != nullptr,
"Equality with non-negative expression should be rewritten to LessThanOrEqual");
}
Loading