Skip to content

K-bound ignored in explicit engine - fix #2163245 #224

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 3 commits into from
Aug 14, 2026
+127 −73
Merged

K-bound ignored in explicit engine - fix #2163245 #224

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9308060
fixed k bound ignored
mtygesen Aug 12, 2026
432a6a5
Merge branch 'main' into explicit-engine-ignoring-k-bound
mtygesen Aug 13, 2026
e0d73f7
Merge branch 'TAPAAL:main' into explicit-engine-ignoring-k-bound
mtygesen Aug 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
19 changes: 15 additions & 4 deletions boost_tests/explicit_engine_test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,18 +16,23 @@ BOOST_AUTO_TEST_CASE(DirectoryTest) {
BOOST_REQUIRE(getenv("TEST_FILES"));
}

void test_explicit_engine(const char* fn, ExplicitColoredModelChecker::Result expected, size_t quid = 0) {
void test_explicit_engine(const char* fn, ExplicitColoredModelChecker::Result expected, size_t quid = 0,
uint32_t kbound = 4, const char* expectedOutput = nullptr) {
std::string model = std::string("/models/explicit-engine/") + fn + ".pnml";
std::string query = std::string("/models/explicit-engine/") + fn + ".xml";
std::set<size_t> qnums{quid};
auto [queries, querynames, sset, options] = load_explicit(model, query, qnums);
options.kbound = 4;
options.kbound = kbound;

ExplicitColoredModelChecker checker(sset, std::cout);

auto result = checker.checkQuery(queries[0], options);
std::ostringstream output;
ColoredResultPrinter printer(quid, output, querynames[0], options.seed(), output);
auto result = checker.checkQuery(queries[0], options, expectedOutput ? &printer : nullptr);

BOOST_REQUIRE_EQUAL(expected, result);
if (expectedOutput) {
BOOST_REQUIRE(output.str().find(expectedOutput) != std::string::npos);
}
}

BOOST_AUTO_TEST_CASE(SubtractionWithVars, * utf::timeout(5)) {
Expand All @@ -37,3 +42,9 @@ BOOST_AUTO_TEST_CASE(SubtractionWithVars, * utf::timeout(5)) {
BOOST_AUTO_TEST_CASE(ReferendumColoredSubtraction, * utf::timeout(5)) {
test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::SATISFIED);
}

BOOST_AUTO_TEST_CASE(KBound, * utf::timeout(5)) {
test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::UNSATISFIED, 1, 9,
"FORMULA Ten voting tokens are reachable FALSE");
test_explicit_engine("referendum_colored_subtraction", ExplicitColoredModelChecker::Result::SATISFIED, 1, 10);
}
17 changes: 17 additions & 0 deletions boost_tests/models/explicit-engine/referendum_colored_subtraction.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,4 +22,21 @@
</exists-path>
</formula>
</property>

<property>
<id>Ten voting tokens are reachable</id>
<description>Ten voting tokens are reachable</description>
<formula>
<exists-path>
<finally>
<integer-eq>
<tokens-count>
<place>Referendum_colored_voting</place>
</tokens-count>
<integer-constant>10</integer-constant>
</integer-eq>
</finally>
</exists-path>
</formula>
</property>
</property-set>
21 changes: 12 additions & 9 deletions include/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,11 @@ namespace PetriEngine::ExplicitColored {
const std::unordered_map<std::string, uint32_t>& placeNameIndices,
const std::unordered_map<std::string, Transition_t>& transitionNameIndices,
size_t seed,
bool createTrace
bool createTrace,
uint32_t kbound
);

bool check(Strategy searchStrategy, ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption);
Reachability::AbstractHandler::Result check(Strategy searchStrategy, ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption);
[[nodiscard]] const SearchStatistics& GetSearchStatistics() const;
std::optional<uint64_t> getCounterExampleId() const;
std::optional<std::vector<InternalTraceStep>> getTraceTo(uint64_t counterExampleId) const;
Expand All @@ -50,26 +51,28 @@ namespace PetriEngine::ExplicitColored {
const ColoredPetriNet& _net;
const ColoredSuccessorGenerator _successorGenerator;
const size_t _seed;
uint32_t _kbound;
bool _fullStatespace = true;
bool _createTrace;
StateMap _stateMap;
SearchStatistics _searchStatistics;
template <typename SuccessorGeneratorState>
[[nodiscard]] bool _search(Strategy searchStrategy);
[[nodiscard]] Reachability::AbstractHandler::Result _search(Strategy searchStrategy);
[[nodiscard]] bool _check(const ColoredPetriNetMarking& state, size_t id) const;
[[nodiscard]] uint64_t _tokenCount(const ColoredPetriNetMarking& marking) const;

template <typename T>
[[nodiscard]] bool _dfs();
[[nodiscard]] Reachability::AbstractHandler::Result _dfs();
template <typename T>
[[nodiscard]] bool _bfs();
[[nodiscard]] Reachability::AbstractHandler::Result _bfs();
template <typename T>
[[nodiscard]] bool _rdfs();
[[nodiscard]] Reachability::AbstractHandler::Result _rdfs();
template <typename T>
[[nodiscard]] bool _bestfs();
[[nodiscard]] Reachability::AbstractHandler::Result _bestfs();

template <template <typename> typename WaitingList, typename T>
[[nodiscard]] bool _genericSearch(WaitingList<T> waiting);
[[nodiscard]] bool _getResult(bool found, bool fullStatespace) const;
[[nodiscard]] Reachability::AbstractHandler::Result _genericSearch(WaitingList<T> waiting);
[[nodiscard]] Reachability::AbstractHandler::Result _getResult(bool found, bool fullStatespace) const;
};
}

Expand Down
3 changes: 2 additions & 1 deletion include/PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@ namespace PetriEngine::ExplicitColored {
uint32_t endWaitingStates = 0;
uint32_t peakWaitingStates = 0;
uint32_t discoveredStates = 0;
uint64_t maxTokens = 0;
size_t biggestEncoding = 0;
};
}

#endif
#endif
63 changes: 40 additions & 23 deletions src/PetriEngine/ExplicitColored/Algorithms/ExplicitWorklist.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,12 @@ namespace PetriEngine::ExplicitColored {
const std::unordered_map<std::string, uint32_t>& placeNameIndices,
const std::unordered_map<std::string, Transition_t>& transitionNameIndices,
const size_t seed,
bool createTrace
bool createTrace,
const uint32_t kbound
) : _net(std::move(net)),
_successorGenerator(ColoredSuccessorGenerator{_net}),
_seed(seed),
_kbound(kbound),
_createTrace(createTrace)
{
const ExplicitQueryPropositionCompiler queryCompiler(placeNameIndices, transitionNameIndices, _successorGenerator);
Expand All @@ -36,7 +38,7 @@ namespace PetriEngine::ExplicitColored {
}
}

bool ExplicitWorklist::check(const Strategy searchStrategy, const ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption) {
Reachability::AbstractHandler::Result ExplicitWorklist::check(const Strategy searchStrategy, const ColoredSuccessorGeneratorOption coloredSuccessorGeneratorOption) {
if (coloredSuccessorGeneratorOption == ColoredSuccessorGeneratorOption::FIXED) {
return _search<ColoredPetriNetStateFixed>(searchStrategy);
}
Expand Down Expand Up @@ -75,13 +77,28 @@ namespace PetriEngine::ExplicitColored {
return _gammaQuery->eval(_successorGenerator, state, id);
}

uint64_t ExplicitWorklist::_tokenCount(const ColoredPetriNetMarking& marking) const {
uint64_t totalTokens = 0;
for (const auto& placeMarking : marking.markings) {
totalTokens += placeMarking.totalCount();
}
return totalTokens;
}

template <template <typename> typename WaitingList, typename T>
bool ExplicitWorklist::_genericSearch(WaitingList<T> waiting) {
Reachability::AbstractHandler::Result ExplicitWorklist::_genericSearch(WaitingList<T> waiting) {
ptrie::set<uint8_t> passed;
ColoredEncoder encoder = ColoredEncoder{_net.getPlaces()};
const auto& initialState = _net.initial();
const auto earlyTerminationCondition = _quantifier == Quantifier::EF;

_searchStatistics.exploredStates = 1;
_searchStatistics.discoveredStates = 1;
_searchStatistics.maxTokens = _tokenCount(initialState);
if (_kbound != 0 && _searchStatistics.maxTokens > _kbound) {
return _getResult(false, encoder.isFullStatespace());
}

auto size = encoder.encode(initialState);
passed.insert(encoder.data(), size);
if constexpr (std::is_same_v<T, ColoredPetriNetStateEven>) {
Expand All @@ -94,9 +111,6 @@ namespace PetriEngine::ExplicitColored {
waiting.add(std::move(initial));
}

_searchStatistics.exploredStates = 1;
_searchStatistics.discoveredStates = 1;

if (_check(initialState, 0) == earlyTerminationCondition) {
_counterExampleId = 0;
return _getResult(true, encoder.isFullStatespace());
Expand Down Expand Up @@ -124,8 +138,14 @@ namespace PetriEngine::ExplicitColored {

successor.shrink();
const auto& marking = successor.marking;
size = encoder.encode(marking);
_searchStatistics.discoveredStates++;
const auto tokens = _tokenCount(marking);
_searchStatistics.maxTokens = std::max(tokens, _searchStatistics.maxTokens);
if (_kbound != 0 && tokens > _kbound) {
continue;
}

size = encoder.encode(marking);
if (!passed.exists(encoder.data(), size).first) {
if (_createTrace) {
_stateMap.transitions.emplace(successor.id, traceStep);
Expand All @@ -149,7 +169,7 @@ namespace PetriEngine::ExplicitColored {
}

template<typename SuccessorGeneratorState>
bool ExplicitWorklist::_search(const Strategy searchStrategy) {
Reachability::AbstractHandler::Result ExplicitWorklist::_search(const Strategy searchStrategy) {
switch (searchStrategy) {
case Strategy::DEFAULT:
case Strategy::DFS:
Expand All @@ -166,22 +186,22 @@ namespace PetriEngine::ExplicitColored {
}

template <typename T>
bool ExplicitWorklist::_dfs() {
Reachability::AbstractHandler::Result ExplicitWorklist::_dfs() {
return _genericSearch<DFSStructure>(DFSStructure<T> {});
}

template <typename T>
bool ExplicitWorklist::_bfs() {
Reachability::AbstractHandler::Result ExplicitWorklist::_bfs() {
return _genericSearch<BFSStructure>(BFSStructure<T> {});
}

template <typename T>
bool ExplicitWorklist::_rdfs() {
Reachability::AbstractHandler::Result ExplicitWorklist::_rdfs() {
return _genericSearch<RDFSStructure>(RDFSStructure<T>(_seed));
}

template <typename T>
bool ExplicitWorklist::_bestfs() {
Reachability::AbstractHandler::Result ExplicitWorklist::_bestfs() {
return _genericSearch<BestFSStructure>(
BestFSStructure<T>(
_seed,
Expand All @@ -191,19 +211,16 @@ namespace PetriEngine::ExplicitColored {
);
}

bool ExplicitWorklist::_getResult(const bool found, const bool fullStatespace) const {
Reachability::ResultPrinter::Result res;
Reachability::AbstractHandler::Result ExplicitWorklist::_getResult(const bool found, const bool fullStatespace) const {
if (!found && !fullStatespace) {
res = Reachability::ResultPrinter::Result::Unknown;
}else {
res = (
(!found && _quantifier == Quantifier::AG) ||
(found && _quantifier == Quantifier::EF))
? Reachability::ResultPrinter::Result::Satisfied
: Reachability::ResultPrinter::Result::NotSatisfied;
return Reachability::AbstractHandler::Unknown;
}
return res == Reachability::ResultPrinter::Result::Satisfied;

return ((!found && _quantifier == Quantifier::AG) ||
(found && _quantifier == Quantifier::EF))
? Reachability::AbstractHandler::Satisfied
: Reachability::AbstractHandler::NotSatisfied;
}
}

#endif //NAIVEWORKLIST_CPP
#endif //NAIVEWORKLIST_CPP
66 changes: 33 additions & 33 deletions src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,13 @@ namespace PetriEngine::ExplicitColored {
const ExplicitColoredTraceContext* trace
) const {
_printCommon(result, {});
_stream << "STATS:" << std::endl
<< " discovered states: " << searchStatistics.discoveredStates << std::endl
<< " explored states: " << searchStatistics.exploredStates << std::endl
<< " peak waiting states: " << searchStatistics.peakWaitingStates << std::endl
<< " end waiting states: " << searchStatistics.endWaitingStates << std::endl
<< " biggest encoded state: " << searchStatistics.biggestEncoding << " bytes" << std::endl;
_stream << "STATS:\n"
<< " discovered states: " << searchStatistics.discoveredStates << '\n'
<< " explored states: " << searchStatistics.exploredStates << '\n'
<< " peak waiting states: " << searchStatistics.peakWaitingStates << '\n'
<< " end waiting states: " << searchStatistics.endWaitingStates << '\n'
<< " max tokens: " << searchStatistics.maxTokens << '\n'
<< " biggest encoded state: " << searchStatistics.biggestEncoding << " bytes\n";
if (trace != nullptr) {
_printTrace(*trace);
}
Expand All @@ -30,56 +31,56 @@ namespace PetriEngine::ExplicitColored {
if (result == Reachability::AbstractHandler::Unknown) {
return;
}
std::cout << "FORMULA " << _queryName << " ";
_stream << "FORMULA " << _queryName << " ";
if (result == Reachability::AbstractHandler::Satisfied) {
std::cout << "TRUE ";
_stream << "TRUE ";
} else if (result == Reachability::AbstractHandler::NotSatisfied) {
std::cout << "FALSE ";
_stream << "FALSE ";
}

std::cout << "TECHNIQUES ";
_stream << "TECHNIQUES ";
for (const auto& techniqueFlag : _techniqueFlags) {
std::cout << techniqueFlag << " ";
_stream << techniqueFlag << " ";
}

for (const auto& techniqueFlag : extraTechniques) {
std::cout << techniqueFlag << " ";
_stream << techniqueFlag << " ";
}

std::cout << std::endl;
_stream << '\n';
if (result == Reachability::AbstractHandler::Satisfied || result == Reachability::AbstractHandler::NotSatisfied) {
std::cout << "Query index " << _queryOffset << " was solved" << std::endl;
_stream << "Query index " << _queryOffset << " was solved\n";
}
std::cout << std::endl;
_stream << '\n';

std::cout << "Query is ";
_stream << "Query is ";
if (result == Reachability::AbstractHandler::NotSatisfied) {
std::cout << "NOT ";
_stream << "NOT ";
}

std::cout << "satisfied" << std::endl;
_stream << "satisfied.\n";
}

void ColoredResultPrinter::_printTrace(const ExplicitColoredTraceContext& trace) const {
_traceStream << "Trace: " << std::endl;
_traceStream << "<trace>" << std::endl;
_traceStream << "Trace:\n";
_traceStream << "<trace>\n";
for (const auto& step : trace.traceSteps) {
if (!step.isInitial) {
_traceStream << "\t<transition id=" << std::quoted(step.transitionId) << ">" << std::endl;
_traceStream << "\t\t<bindings>" << std::endl;
_traceStream << "\t<transition id=" << std::quoted(step.transitionId) << ">\n";
_traceStream << "\t\t<bindings>" << '\n';
for (const auto& [variableId, value] : step.binding) {
_traceStream << "\t\t\t<variable id=" << std::quoted(variableId) << ">" << std::endl;
_traceStream << "\t\t\t\t<color>" << value << "</color>" << std::endl;
_traceStream << "\t\t\t</variable>" << std::endl;
_traceStream << "\t\t\t<variable id=" << std::quoted(variableId) << ">\n";
_traceStream << "\t\t\t\t<color>" << value << "</color>\n";
_traceStream << "\t\t\t</variable>\n";
}
_traceStream << "\t\t</bindings>" << std::endl;
_traceStream << "\t</transition>" << std::endl;
_traceStream << "\t\t</bindings>\n";
_traceStream << "\t</transition>\n";
}
_traceStream << "\t<marking>" << std::endl;
_traceStream << "\t<marking>\n";
_printMarkings(trace.cpnBuilder, step);
_traceStream << "\t</marking>" << std::endl;
_traceStream << "\t</marking>\n";
}
_traceStream << "</trace>" << std::endl;
_traceStream << "</trace>\n";
}

void ColoredResultPrinter::_printMarkings(
Expand Down Expand Up @@ -135,11 +136,10 @@ namespace PetriEngine::ExplicitColored {
{
if (!traceTokens.empty())
{
_traceStream << "\t\t<place id=" << std::quoted(place_id) << ">" << std::endl;
_traceStream << "\t\t<place id=" << std::quoted(place_id) << ">\n";
writer.writeInitialTokens(place_id);
_traceStream << "\t\t</place>" << std::endl;
_traceStream << "\t\t</place>\n";
}
}
}
}

Loading
Loading