From 579ccf0a9ddce44ebd18841eb9e07f56a752593b Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 6 Jul 2026 17:42:32 +0200 Subject: [PATCH 1/2] added test case for rewrites of expressions to use leq instead of eq --- boost_tests/CMakeLists.txt | 3 ++ boost_tests/PushNegationTests.cpp | 58 +++++++++++++++++++++++++++++++ 2 files changed, 61 insertions(+) diff --git a/boost_tests/CMakeLists.txt b/boost_tests/CMakeLists.txt index 59ef49eeb..9417f99e7 100644 --- a/boost_tests/CMakeLists.txt +++ b/boost_tests/CMakeLists.txt @@ -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) @@ -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) @@ -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) diff --git a/boost_tests/PushNegationTests.cpp b/boost_tests/PushNegationTests.cpp index 0053ef708..489f61d49 100644 --- a/boost_tests/PushNegationTests.cpp +++ b/boost_tests/PushNegationTests.cpp @@ -30,6 +30,64 @@ BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) { "Less than operands should be swapped"); } +// 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(std::vector{ + std::make_shared(std::vector{ + std::make_shared("P0"), + std::make_shared("P1") + }), + std::make_shared("P2") + }); + auto condition = std::make_shared( + subtraction, + std::make_shared(0) + ); + auto stats = negstat_t(); + + auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false); + + BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast(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(std::vector{ + std::make_shared("P0"), + std::make_shared("P1") + }); + auto condition = std::make_shared( + std::make_shared( + subtraction, + std::make_shared(0) + ) + ); + auto stats = negstat_t(); + + auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false); + + BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast(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(std::vector{ + std::make_shared("P0"), + std::make_shared("P1") + }); + auto condition = std::make_shared( + sum, + std::make_shared(0) + ); + auto stats = negstat_t(); + + auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false); + + BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast(res) != nullptr, + "Equality with non-negative expression should be rewritten to LessThanOrEqual"); +} + //BOOST_AUTO_TEST_CASE(AirplaneLD_PT_0050_3) { // auto cond = std::make_shared(std::make_shared( // std::make_shared( From 6c3e918cc34196173f0602060582b0d02d1e62a0 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Tue, 14 Jul 2026 12:55:05 +0200 Subject: [PATCH 2/2] fix workflow error --- boost_tests/PushNegationTests.cpp | 52 +++++++------------------------ 1 file changed, 11 insertions(+), 41 deletions(-) diff --git a/boost_tests/PushNegationTests.cpp b/boost_tests/PushNegationTests.cpp index 489f61d49..e88d274b7 100644 --- a/boost_tests/PushNegationTests.cpp +++ b/boost_tests/PushNegationTests.cpp @@ -7,9 +7,12 @@ using namespace PetriEngine::PQL; +inline std::shared_ptr make_id(const std::string& name) { + return std::make_shared(std::make_shared(name)); +} BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) { - auto identifier = std::make_shared("a"); + auto identifier = make_id("a"); auto literal = std::make_shared(1); auto condition = std::make_shared( std::make_shared( @@ -34,10 +37,10 @@ BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) { BOOST_AUTO_TEST_CASE(equal_zero_with_subtraction_is_not_rewritten) { auto subtraction = std::make_shared(std::vector{ std::make_shared(std::vector{ - std::make_shared("P0"), - std::make_shared("P1") + make_id("P0"), + make_id("P1") }), - std::make_shared("P2") + make_id("P2") }); auto condition = std::make_shared( subtraction, @@ -53,8 +56,8 @@ BOOST_AUTO_TEST_CASE(equal_zero_with_subtraction_is_not_rewritten) { BOOST_AUTO_TEST_CASE(not_equal_zero_with_subtraction_is_not_rewritten) { auto subtraction = std::make_shared(std::vector{ - std::make_shared("P0"), - std::make_shared("P1") + make_id("P0"), + make_id("P1") }); auto condition = std::make_shared( std::make_shared( @@ -73,8 +76,8 @@ BOOST_AUTO_TEST_CASE(not_equal_zero_with_subtraction_is_not_rewritten) { // 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(std::vector{ - std::make_shared("P0"), - std::make_shared("P1") + make_id("P0"), + make_id("P1") }); auto condition = std::make_shared( sum, @@ -87,36 +90,3 @@ BOOST_AUTO_TEST_CASE(equal_zero_with_plus_is_rewritten_to_leq) { BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast(res) != nullptr, "Equality with non-negative expression should be rewritten to LessThanOrEqual"); } - -//BOOST_AUTO_TEST_CASE(AirplaneLD_PT_0050_3) { -// auto cond = std::make_shared(std::make_shared( -// std::make_shared( -// std::make_shared( -// std::make_shared( -// std::make_shared( -// std::make_shared( -// std::make_shared( -// std::make_shared(std::vector{ -// std::make_shared( -// "P3"), -// std::make_shared( -// "stp5") -// }), -// std::make_shared(12) -// ), -// std::make_shared( -// std::make_shared(std::vector{ -// std::make_shared( -// "SpeedPossibleVal_38"), -// std::make_shared( -// "SpeedPossibleVal_26") -// }), -// std::make_shared(35) -// ) -// ) -// ) -// ) -// ) -// ) -// )); -//}