From 533cb83ec1eb9354865b040f2e63cb0b05f9cfdd Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Mon, 22 Sep 2025 18:47:00 +0200 Subject: [PATCH 01/14] P >= 0 Constraints for LP and some linux include problems fixed --- include/PetriEngine/Simplification/Member.h | 1 + include/utils/structures/shared_string.h | 1 + src/PetriEngine/PQL/Contexts.cpp | 20 +++++++++++++++++++ .../Simplification/LinearProgram.cpp | 2 +- 4 files changed, 23 insertions(+), 1 deletion(-) diff --git a/include/PetriEngine/Simplification/Member.h b/include/PetriEngine/Simplification/Member.h index c30801b5b..a672d39b5 100644 --- a/include/PetriEngine/Simplification/Member.h +++ b/include/PetriEngine/Simplification/Member.h @@ -4,6 +4,7 @@ #include #include #include +#include //#include "../PQL/PQL.h" namespace PetriEngine { diff --git a/include/utils/structures/shared_string.h b/include/utils/structures/shared_string.h index 3cc41398c..f2de0f2da 100644 --- a/include/utils/structures/shared_string.h +++ b/include/utils/structures/shared_string.h @@ -14,6 +14,7 @@ #include #include #include +#include typedef const std::string const_string; typedef std::shared_ptr shared_const_string; diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index f0fb0b404..288346a84 100644 --- a/src/PetriEngine/PQL/Contexts.cpp +++ b/src/PetriEngine/PQL/Contexts.cpp @@ -153,6 +153,26 @@ namespace PetriEngine { return nullptr; } } + + glp_add_rows(lp, _net->numberOfPlaces()); + for (size_t p = 0; p < _net->numberOfPlaces(); p++) { + std::vector row(nCol, 0); + std::vector indices; + row.shrink_to_fit(); + + for (size_t t = 0; t < _net->numberOfTransitions(); t++) { + if(_net->outArc(t, p) - _net->inArc(p, t) != 0){ + row[t] = _net->outArc(t, p); + row[t] -= _net->inArc(p, t); + indices.push_back(t); + } + } + + glp_set_mat_row(lp, rowno, indices.size() - 1, indices.data(), row.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + ++rowno; + } + return lp; } } diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 5733e549d..3ae8c025b 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -76,7 +76,7 @@ namespace PetriEngine { if (lp == nullptr) return false; - int rowno = 1 + net->numberOfPlaces(); + int rowno = 1 + 2 * net->numberOfPlaces(); glp_add_rows(lp, _equations.size()); for (const auto& eq : _equations) { auto l = eq.row->write_indir(row, indir); From c01c8aa05b292b09da03763f5647b812bf211fdb Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Mon, 29 Sep 2025 13:12:40 +0200 Subject: [PATCH 02/14] fixed p>= constraints --- src/PetriEngine/PQL/Contexts.cpp | 12 ++++++------ src/PetriEngine/Simplification/LinearProgram.cpp | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index 288346a84..f39834163 100644 --- a/src/PetriEngine/PQL/Contexts.cpp +++ b/src/PetriEngine/PQL/Contexts.cpp @@ -156,20 +156,20 @@ namespace PetriEngine { glp_add_rows(lp, _net->numberOfPlaces()); for (size_t p = 0; p < _net->numberOfPlaces(); p++) { - std::vector row(nCol, 0); - std::vector indices; + std::vector row(nCol+1, 0); + std::vector indices(1, 0); row.shrink_to_fit(); for (size_t t = 0; t < _net->numberOfTransitions(); t++) { if(_net->outArc(t, p) - _net->inArc(p, t) != 0){ - row[t] = _net->outArc(t, p); - row[t] -= _net->inArc(p, t); - indices.push_back(t); + row[t+1] = _net->outArc(t, p); + row[t+1] -= _net->inArc(p, t); + indices.push_back(t+1); } } glp_set_mat_row(lp, rowno, indices.size() - 1, indices.data(), row.data()); - glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + glp_set_row_bnds(lp, rowno, GLP_LO, -1.0 * marking()[p], infty); ++rowno; } diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 3ae8c025b..5ee009152 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -65,7 +65,7 @@ namespace PetriEngine { } const uint32_t nCol = net->numberOfTransitions(); - const uint32_t nRow = net->numberOfPlaces() + _equations.size(); + const uint32_t nRow = 2 * net->numberOfPlaces() + _equations.size(); std::vector row = std::vector(nCol + 1); std::vector indir(std::max(nCol, nRow) + 1); From bafd669e1d2dd5eefb71d6744108080018395c07 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Fri, 17 Oct 2025 11:30:24 +0200 Subject: [PATCH 03/14] added lp and solution printing to potentially debug some cases --- include/PetriEngine/PQL/Contexts.h | 8 +- include/PetriEngine/options.h | 1 + src/PetriEngine/PQL/Contexts.cpp | 4 +- .../Simplification/LinearProgram.cpp | 94 ++++++++++++++++++- src/PetriEngine/options.cpp | 7 ++ src/VerifyPN.cpp | 4 +- 6 files changed, 112 insertions(+), 6 deletions(-) diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index f9f56535e..81445d454 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -180,7 +180,7 @@ namespace PetriEngine { SimplificationContext(const MarkVal* marking, const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, - Simplification::LPCache* cache, uint32_t potencyTimeout = 0) + Simplification::LPCache* cache, uint32_t potencyTimeout = 0, uint32_t printLevel = 0) : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), _potencyTimeout(potencyTimeout) { _negated = false; @@ -190,6 +190,7 @@ namespace PetriEngine { _start = std::chrono::high_resolution_clock::now(); _cache = cache; _markingOutOfBounds = false; + _printLevel = printLevel; for(size_t i = 0; i < net->numberOfPlaces(); ++i) { if (marking[i] > std::numeric_limits::max()) { //too many tokens exceeding int32_t limits, LP solver will give wrong results _markingOutOfBounds = true; @@ -230,6 +231,10 @@ namespace PetriEngine { double getReductionTime(); + uint32_t getPrintLevel() const{ + return _printLevel; + } + bool timeout() const { auto end = std::chrono::high_resolution_clock::now(); auto diff = std::chrono::duration_cast(end - _start); @@ -258,6 +263,7 @@ namespace PetriEngine { bool _markingOutOfBounds; const PetriNet* _net; uint32_t _queryTimeout, _lpTimeout, _potencyTimeout; + uint32_t _printLevel; mutable glp_prob* _base_lp = nullptr; std::chrono::high_resolution_clock::time_point _start; Simplification::LPCache* _cache; diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h index 49f29a216..157f9f500 100644 --- a/include/PetriEngine/options.h +++ b/include/PetriEngine/options.h @@ -63,6 +63,7 @@ struct options_t { std::set querynumbers; Strategy strategy = Strategy::DEFAULT; int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, initPotencyTimeout = 10; + int lpPrintLevel = 0; TraceLevel trace = TraceLevel::None; bool use_query_reductions = true; uint32_t siphontrapTimeout = 0; diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index f39834163..a1f486878 100644 --- a/src/PetriEngine/PQL/Contexts.cpp +++ b/src/PetriEngine/PQL/Contexts.cpp @@ -154,7 +154,7 @@ namespace PetriEngine { } } - glp_add_rows(lp, _net->numberOfPlaces()); + /*glp_add_rows(lp, _net->numberOfPlaces()); for (size_t p = 0; p < _net->numberOfPlaces(); p++) { std::vector row(nCol+1, 0); std::vector indices(1, 0); @@ -171,7 +171,7 @@ namespace PetriEngine { glp_set_mat_row(lp, rowno, indices.size() - 1, indices.data(), row.data()); glp_set_row_bnds(lp, rowno, GLP_LO, -1.0 * marking()[p], infty); ++rowno; - } + }*/ return lp; } diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 5ee009152..c8a8ff53d 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -46,10 +46,99 @@ namespace PetriEngine { constexpr auto infty = std::numeric_limits::infinity(); + std::string bound_or_inf(double bound){ + const std::string inf = "inf"; + const std::string ninf = "ninf"; + return (std::fabs(bound) != infty)? std::to_string(bound) : ((bound > 0)? inf : ninf); + } + + void printConstraints(const PQL::SimplificationContext& context, glp_prob* lp){ + int nCols = glp_get_num_cols(lp); + int nRows = glp_get_num_rows(lp); + + std::vector indices(nCols + 1); + std::vector coef(nCols + 1); + int l; + + for(int i = 1; i <= nRows; i++){ + std::cout << "Row " << i << ": "; + + l = glp_get_mat_row(lp, i, indices.data(), coef.data()); + + bool first_print = true; + for(int j = 1; j <= l; j++){ + if(!first_print) std::cout << " + "; + std::cout << coef[j] << "*" << *context.net()->transitionNames()[indices[j] - 1]; + first_print = false; + } + + if(first_print){ + std::cout << ""; + } + + + double up = glp_get_row_ub(lp, i); + double lb = glp_get_row_lb(lp, i); + switch(glp_get_row_type(lp, i)){ + case GLP_FR: + std::cout << " is unconstraint"; + break; + case GLP_LO: + std::cout << " >= " << bound_or_inf(lb); + break; + case GLP_UP: + std::cout << " <= " << bound_or_inf(up); + break; + case GLP_DB: + std::cout << " in [" << bound_or_inf(lb) << ", " << bound_or_inf(up) << "]"; + break; + case GLP_FX: + std::cout << " = " << bound_or_inf(lb); + break; + } + std::cout << "\n"; + } + + } + + + void printSolution(const PQL::SimplificationContext& context, glp_prob* lp, bool is_mip){ + if(context.getPrintLevel() == 0) + return; + + if(context.getPrintLevel() > 1){ + printConstraints(context, lp); + } + + int nCols = glp_get_num_cols(lp); + bool first_print = true; + if(is_mip){ + std::cout << "MIP Solution: "; + }else{ + std::cout << "LP Solution: "; + } + for(int i = 1; i <= nCols;i++){ + double coef = (is_mip)? glp_mip_col_val(lp, i) : glp_get_col_prim(lp, i); + if(coef != 0){ + if(!first_print) + std::cout << " + "; + first_print = false; + std::cout << coef << "*" << *context.net()->transitionNames()[i - 1]; + } + } + + if(first_print) + std::cout << "\n"; + else{ + std::cout << "\n"; + } + } + bool LinearProgram::isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime) { bool use_ilp = true; auto net = context.net(); + if (_result != result_t::UKNOWN) { if (_result == result_t::IMPOSSIBLE) @@ -76,7 +165,7 @@ namespace PetriEngine { if (lp == nullptr) return false; - int rowno = 1 + 2 * net->numberOfPlaces(); + int rowno = 1 + net->numberOfPlaces(); glp_add_rows(lp, _equations.size()); for (const auto& eq : _equations) { auto l = eq.row->write_indir(row, indir); @@ -146,6 +235,7 @@ namespace PetriEngine { auto ires = glp_intopt(lp, &iset); if (ires == GLP_ETMLIM) { + printSolution(context, lp, false); _result = result_t::UKNOWN; // std::cerr << "glpk mip: timeout" << std::endl; } @@ -153,6 +243,7 @@ namespace PetriEngine { { auto ist = glp_mip_status(lp); if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { + printSolution(context, lp, true); _result = result_t::POSSIBLE; } else @@ -163,6 +254,7 @@ namespace PetriEngine { } else if (status == GLP_FEAS || status == GLP_UNBND) { + printSolution(context, lp, false); _result = result_t::POSSIBLE; } else diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp index f5379408d..7bc04f96e 100644 --- a/src/PetriEngine/options.cpp +++ b/src/PetriEngine/options.cpp @@ -346,6 +346,13 @@ bool options_t::parse(int argc, const char** argv) { if (sscanf(argv[++i], "%d", &queryReductionTimeout) != 1 || queryReductionTimeout < 0) { throw base_error("Argument Error: Invalid query reduction timeout argument ", std::quoted(argv[i])); } + }else if (std::strcmp(argv[i], "-lpp") == 0 || std::strcmp(argv[i], "--lp-print") == 0) { + if (i == argc - 1) { + throw base_error("Missing number after ", std::quoted(argv[i])); + } + if (sscanf(argv[++i], "%d", &lpPrintLevel) != 1 || lpPrintLevel < 0) { + throw base_error("Argument Error: Invalid lp print level argument ", std::quoted(argv[i])); + } } else if (std::strcmp(argv[i], "--init-potency-timeout") == 0) { if (i == argc - 1) { throw base_error("Missing number after ", std::quoted(argv[i])); diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp index c669c2990..3b576edd0 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -578,7 +578,7 @@ void simplify_queries(const MarkVal* marking, if (options.logic == TemporalLogic::LTL) { if (options.queryReductionTimeout == 0 || qt == 0) continue; SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache); + options.lpsolveTimeout, &cache, 0, options.lpPrintLevel); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction for LTL is skipped.\n"; break; @@ -609,7 +609,7 @@ void simplify_queries(const MarkVal* marking, if (options.queryReductionTimeout > 0 && qt > 0) { SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache); + options.lpsolveTimeout, &cache, 0, options.lpPrintLevel); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction is skipped.\n"; break; From 623533687ddc4394ededa82d79dec12986e70cbe Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Fri, 21 Nov 2025 14:52:42 +0100 Subject: [PATCH 04/14] lp loop constraints --- .../Simplification/LinearProgram.cpp | 122 +++++++++++++++++- 1 file changed, 116 insertions(+), 6 deletions(-) diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index c8a8ff53d..251a3b2b8 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -47,8 +47,8 @@ namespace PetriEngine { constexpr auto infty = std::numeric_limits::infinity(); std::string bound_or_inf(double bound){ - const std::string inf = "inf"; - const std::string ninf = "ninf"; + std::string inf = "inf"; + std::string ninf = "ninf"; return (std::fabs(bound) != infty)? std::to_string(bound) : ((bound > 0)? inf : ninf); } @@ -61,14 +61,19 @@ namespace PetriEngine { int l; for(int i = 1; i <= nRows; i++){ - std::cout << "Row " << i << ": "; - l = glp_get_mat_row(lp, i, indices.data(), coef.data()); + std::cout << "Row " << i << "[len: " << l << "]: "; + + bool first_print = true; for(int j = 1; j <= l; j++){ if(!first_print) std::cout << " + "; - std::cout << coef[j] << "*" << *context.net()->transitionNames()[indices[j] - 1]; + if((indices[j] - 1) < context.net()->numberOfTransitions()){ + std::cout << coef[j] << "*" << *context.net()->transitionNames()[indices[j] - 1]; + }else{ + std::cout << coef[j] << "*" << glp_get_col_name(lp, indices[j]); + } first_print = false; } @@ -123,7 +128,11 @@ namespace PetriEngine { if(!first_print) std::cout << " + "; first_print = false; - std::cout << coef << "*" << *context.net()->transitionNames()[i - 1]; + if( i - 1 < context.net()->numberOfTransitions()){ + std::cout << coef << "*" << *context.net()->transitionNames()[i - 1]; + }else{ + std::cout << coef << "*" << glp_get_col_name(lp, i); + } } } @@ -207,6 +216,106 @@ namespace PetriEngine { glp_set_col_bnds(lp, i, GLP_LO, 0, infty); } + for (size_t p = 0; p < net->numberOfPlaces(); p++) { + auto numColsLP = glp_get_num_cols(lp); + std::vector inRow(1, 0); + std::vector inIndices(1, 0); + + std::vector outRow(1, 0); + std::vector outIndices(1, 0); + + + bool has_loop = false; + bool has_in = false; + //bool requires_tokens = false; + + //std::map> loops_by_weight; + //int min_pos_loop = 0; + uint32_t minimum_weight = UINT32_MAX; + + for (size_t t = 0; t < net->numberOfTransitions(); t++) { + if(net->outArc(t, p) != 0 && net->inArc(p, t) != 0){ + has_loop = true; + /*if(net->inArc(p, t) > context.marking()[p]) + requires_tokens = true; + + if(net->outArc(t, p) > net->inArc(p, t) && net->inArc(p, t) < min_pos_loop) + min_pos_loop = net->inArc(p, t);*/ + + minimum_weight = std::min(minimum_weight, net->inArc(p, t)); + + outRow.push_back(1.0); + outIndices.push_back(t+1); + } + else{ + if(net->inArc(p,t) != 0){ + outRow.push_back(1.0); + outIndices.push_back(t+1); + } + if(net->outArc(t,p) != 0){ + has_in = true; + + inRow.push_back(net->outArc(t, p)); + inIndices.push_back(t+1); + } + } + } + + if(!has_loop || !has_in || context.marking()[p] >= minimum_weight){ + //std::cout << "no loop applicable\n"; + continue; + } + else{ + //std::cout << "adding loop constraint for " << *net->placeNames()[p] <<"\n"; + } + + int idx = numColsLP + 1; + glp_add_cols(lp, 2); + + for(int i = glp_get_num_cols(lp) - 1; i <= glp_get_num_cols(lp); i++){ + glp_set_obj_coef(lp, i, 1); + glp_set_col_kind(lp, i, GLP_BV); + //glp_set_col_bnds(lp, i, GLP_DB, 0.0, 1.0); + } + + const int OR_P = glp_get_num_cols(lp) ; + std::string or_p_name = "NO_IMPLY_" + *net->placeNames()[p]; + glp_set_col_name(lp, OR_P, or_p_name.c_str()); + const int OR_Q = glp_get_num_cols(lp) - 1; + std::string or_q_name = "YES_IMPLY_" + *net->placeNames()[p]; + glp_set_col_name(lp, OR_Q, or_q_name.c_str()); + + const double needed_weight = (double) (minimum_weight - context.marking()[p]); + inRow.push_back(needed_weight); + inIndices.push_back(OR_P); + + outRow.push_back(-1000000.0); + outIndices.push_back(OR_Q); + + glp_add_rows(lp, 3); + + glp_set_mat_row(lp, rowno, inIndices.size() - 1, inIndices.data(), inRow.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, needed_weight, infty); + ++rowno; + + glp_set_mat_row(lp, rowno, outIndices.size() - 1, outIndices.data(), outRow.data()); + glp_set_row_bnds(lp, rowno, GLP_UP, 0.0, 0.0); + ++rowno; + + double orRow[3]; + int orIndices[3]; + + + orRow[1] = 1.0; + orRow[2] = 1.0; + orIndices[1] = OR_P; + orIndices[2] = OR_Q; + + glp_set_mat_row(lp, rowno, 2, orIndices, orRow); + glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); + ++rowno; + } + // Minimize the objective glp_set_obj_dir(lp, GLP_MIN); auto stime = glp_time(); @@ -230,6 +339,7 @@ namespace PetriEngine { glp_iocp iset; glp_init_iocp(&iset); iset.msg_lev = 0; + iset.tol_int = 1e-10; iset.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); iset.presolve = GLP_OFF; auto ires = glp_intopt(lp, &iset); From 17d4552379ba21e4d514c614f8796a6b28550df2 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Thu, 4 Dec 2025 18:18:30 +0100 Subject: [PATCH 05/14] changed tolerances and bound --- src/PetriEngine/Simplification/LinearProgram.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 251a3b2b8..5d964ee02 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -244,12 +244,12 @@ namespace PetriEngine { minimum_weight = std::min(minimum_weight, net->inArc(p, t)); - outRow.push_back(1.0); + outRow.push_back(1/1000.0); outIndices.push_back(t+1); } else{ if(net->inArc(p,t) != 0){ - outRow.push_back(1.0); + outRow.push_back(1/1000.0); outIndices.push_back(t+1); } if(net->outArc(t,p) != 0){ @@ -289,7 +289,7 @@ namespace PetriEngine { inRow.push_back(needed_weight); inIndices.push_back(OR_P); - outRow.push_back(-1000000.0); + outRow.push_back(-10000.0); outIndices.push_back(OR_Q); glp_add_rows(lp, 3); From a8befabcecc6781045661251a926aa64ddb1c49c Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Thu, 18 Dec 2025 13:25:15 +0100 Subject: [PATCH 06/14] lower constant --- include/PetriEngine/PQL/Contexts.h | 8 +- include/PetriEngine/options.h | 1 + .../Simplification/LinearProgram.cpp | 245 +++++++++++------- src/VerifyPN.cpp | 5 +- 4 files changed, 167 insertions(+), 92 deletions(-) diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index 81445d454..c4d7e2e91 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -180,10 +180,11 @@ namespace PetriEngine { SimplificationContext(const MarkVal* marking, const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, - Simplification::LPCache* cache, uint32_t potencyTimeout = 0, uint32_t printLevel = 0) + Simplification::LPCache* cache, uint32_t potencyTimeout = 0, uint32_t printLevel = 0, bool useBigM = true) : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), _potencyTimeout(potencyTimeout) { _negated = false; + _useBigM = useBigM; _marking = marking; _net = net; _base_lp = buildBase(); @@ -235,6 +236,10 @@ namespace PetriEngine { return _printLevel; } + bool useBigM() const { + return _useBigM; + } + bool timeout() const { auto end = std::chrono::high_resolution_clock::now(); auto diff = std::chrono::duration_cast(end - _start); @@ -259,6 +264,7 @@ namespace PetriEngine { private: bool _negated; + bool _useBigM; const MarkVal* _marking; bool _markingOutOfBounds; const PetriNet* _net; diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h index 157f9f500..66a8c29c5 100644 --- a/include/PetriEngine/options.h +++ b/include/PetriEngine/options.h @@ -63,6 +63,7 @@ struct options_t { std::set querynumbers; Strategy strategy = Strategy::DEFAULT; int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, initPotencyTimeout = 10; + bool lpUseBigM = true; int lpPrintLevel = 0; TraceLevel trace = TraceLevel::None; bool use_query_reductions = true; diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 5d964ee02..cd6330995 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -6,6 +6,7 @@ #include "PetriEngine/Simplification/LinearProgram.h" #include "PetriEngine/Simplification/LPCache.h" #include "PetriEngine/PQL/Contexts.h" +#include "VerifyPN.h" namespace PetriEngine { namespace Simplification { @@ -143,11 +144,44 @@ namespace PetriEngine { } } + std::vector bigMQuery(const PQL::SimplificationContext& context){ + + std::vector res; + + for(int p = 0; p < context.net()->numberOfPlaces(); p++){ + auto rhs = std::make_shared(context.net()->placeNames()[p]); + auto lhs = std::make_shared(10000); + auto lt = std::make_shared(lhs, rhs); + res.push_back(lt); + } + + auto orQuery = std::make_shared(res); + auto FQuery = std::make_shared(orQuery); + auto EFQuery = std::make_shared(FQuery); + std::vector queries; + queries.push_back(EFQuery); + return queries; + } + + + bool checkBigMConstraint(const PQL::SimplificationContext& context){ + return true; + auto queries = bigMQuery(context); + options_t options; + options.lpUseBigM = false; + simplify_queries(context.marking(), context.net(), queries, options, std::cout); + std::cout << "done big M\n"; + if(queries[0]->isTriviallyFalse()){ + return true; + }else{ + return false; + } + } + bool LinearProgram::isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime) { bool use_ilp = true; auto net = context.net(); - if (_result != result_t::UKNOWN) { if (_result == result_t::IMPOSSIBLE) @@ -216,104 +250,106 @@ namespace PetriEngine { glp_set_col_bnds(lp, i, GLP_LO, 0, infty); } - for (size_t p = 0; p < net->numberOfPlaces(); p++) { - auto numColsLP = glp_get_num_cols(lp); - std::vector inRow(1, 0); - std::vector inIndices(1, 0); + if(context.useBigM()){ + for (size_t p = 0; p < net->numberOfPlaces(); p++) { + auto numColsLP = glp_get_num_cols(lp); + std::vector inRow(1, 0); + std::vector inIndices(1, 0); + + std::vector outRow(1, 0); + std::vector outIndices(1, 0); - std::vector outRow(1, 0); - std::vector outIndices(1, 0); - - - bool has_loop = false; - bool has_in = false; - //bool requires_tokens = false; - - //std::map> loops_by_weight; - //int min_pos_loop = 0; - uint32_t minimum_weight = UINT32_MAX; - - for (size_t t = 0; t < net->numberOfTransitions(); t++) { - if(net->outArc(t, p) != 0 && net->inArc(p, t) != 0){ - has_loop = true; - /*if(net->inArc(p, t) > context.marking()[p]) - requires_tokens = true; - - if(net->outArc(t, p) > net->inArc(p, t) && net->inArc(p, t) < min_pos_loop) - min_pos_loop = net->inArc(p, t);*/ - - minimum_weight = std::min(minimum_weight, net->inArc(p, t)); - - outRow.push_back(1/1000.0); - outIndices.push_back(t+1); - } - else{ - if(net->inArc(p,t) != 0){ - outRow.push_back(1/1000.0); + + bool has_loop = false; + bool has_in = false; + //bool requires_tokens = false; + + //std::map> loops_by_weight; + //int min_pos_loop = 0; + uint32_t minimum_weight = UINT32_MAX; + + for (size_t t = 0; t < net->numberOfTransitions(); t++) { + if(net->outArc(t, p) != 0 && net->inArc(p, t) != 0){ + has_loop = true; + /*if(net->inArc(p, t) > context.marking()[p]) + requires_tokens = true; + + if(net->outArc(t, p) > net->inArc(p, t) && net->inArc(p, t) < min_pos_loop) + min_pos_loop = net->inArc(p, t);*/ + + minimum_weight = std::min(minimum_weight, net->inArc(p, t)); + + outRow.push_back(1); outIndices.push_back(t+1); } - if(net->outArc(t,p) != 0){ - has_in = true; - - inRow.push_back(net->outArc(t, p)); - inIndices.push_back(t+1); + else{ + if(net->inArc(p,t) != 0){ + outRow.push_back(1); + outIndices.push_back(t+1); + } + if(net->outArc(t,p) != 0){ + has_in = true; + + inRow.push_back(net->outArc(t, p)); + inIndices.push_back(t+1); + } } } - } - if(!has_loop || !has_in || context.marking()[p] >= minimum_weight){ - //std::cout << "no loop applicable\n"; - continue; - } - else{ - //std::cout << "adding loop constraint for " << *net->placeNames()[p] <<"\n"; - } + if(!has_loop || !has_in || context.marking()[p] >= minimum_weight){ + //std::cout << "no loop applicable\n"; + continue; + } + else{ + //std::cout << "adding loop constraint for " << *net->placeNames()[p] <<"\n"; + } - int idx = numColsLP + 1; - glp_add_cols(lp, 2); + int idx = numColsLP + 1; + glp_add_cols(lp, 2); - for(int i = glp_get_num_cols(lp) - 1; i <= glp_get_num_cols(lp); i++){ - glp_set_obj_coef(lp, i, 1); - glp_set_col_kind(lp, i, GLP_BV); - //glp_set_col_bnds(lp, i, GLP_DB, 0.0, 1.0); - } + for(int i = glp_get_num_cols(lp) - 1; i <= glp_get_num_cols(lp); i++){ + glp_set_obj_coef(lp, i, 1); + glp_set_col_kind(lp, i, GLP_BV); + //glp_set_col_bnds(lp, i, GLP_DB, 0.0, 1.0); + } - const int OR_P = glp_get_num_cols(lp) ; - std::string or_p_name = "NO_IMPLY_" + *net->placeNames()[p]; - glp_set_col_name(lp, OR_P, or_p_name.c_str()); - const int OR_Q = glp_get_num_cols(lp) - 1; - std::string or_q_name = "YES_IMPLY_" + *net->placeNames()[p]; - glp_set_col_name(lp, OR_Q, or_q_name.c_str()); - - const double needed_weight = (double) (minimum_weight - context.marking()[p]); - inRow.push_back(needed_weight); - inIndices.push_back(OR_P); - - outRow.push_back(-10000.0); - outIndices.push_back(OR_Q); - - glp_add_rows(lp, 3); + const int OR_P = glp_get_num_cols(lp) ; + std::string or_p_name = "NO_IMPLY_" + *net->placeNames()[p]; + glp_set_col_name(lp, OR_P, or_p_name.c_str()); + const int OR_Q = glp_get_num_cols(lp) - 1; + std::string or_q_name = "YES_IMPLY_" + *net->placeNames()[p]; + glp_set_col_name(lp, OR_Q, or_q_name.c_str()); + + const double needed_weight = (double) (minimum_weight - context.marking()[p]); + inRow.push_back(needed_weight); + inIndices.push_back(OR_P); + + outRow.push_back(-1.0 * 10000); + outIndices.push_back(OR_Q); + + glp_add_rows(lp, 3); - glp_set_mat_row(lp, rowno, inIndices.size() - 1, inIndices.data(), inRow.data()); - glp_set_row_bnds(lp, rowno, GLP_LO, needed_weight, infty); - ++rowno; + glp_set_mat_row(lp, rowno, inIndices.size() - 1, inIndices.data(), inRow.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, needed_weight, infty); + ++rowno; - glp_set_mat_row(lp, rowno, outIndices.size() - 1, outIndices.data(), outRow.data()); - glp_set_row_bnds(lp, rowno, GLP_UP, 0.0, 0.0); - ++rowno; + glp_set_mat_row(lp, rowno, outIndices.size() - 1, outIndices.data(), outRow.data()); + glp_set_row_bnds(lp, rowno, GLP_UP, 0.0, 0.0); + ++rowno; - double orRow[3]; - int orIndices[3]; - + double orRow[3]; + int orIndices[3]; + - orRow[1] = 1.0; - orRow[2] = 1.0; - orIndices[1] = OR_P; - orIndices[2] = OR_Q; + orRow[1] = 1.0; + orRow[2] = 1.0; + orIndices[1] = OR_P; + orIndices[2] = OR_Q; - glp_set_mat_row(lp, rowno, 2, orIndices, orRow); - glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); - ++rowno; + glp_set_mat_row(lp, rowno, 2, orIndices, orRow); + glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); + ++rowno; + } } // Minimize the objective @@ -336,6 +372,8 @@ namespace PetriEngine { auto status = glp_get_status(lp); if (status == GLP_OPT) { + + #if 1 glp_iocp iset; glp_init_iocp(&iset); iset.msg_lev = 0; @@ -343,6 +381,13 @@ namespace PetriEngine { iset.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); iset.presolve = GLP_OFF; auto ires = glp_intopt(lp, &iset); + #else + glp_smcp settings_exact; + settings_exact.msg_lev = 0; + settings_exact.it_lim = INT_MAX; + settings_exact.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); + auto ires = glp_exact(lp, &settings_exact); + #endif if (ires == GLP_ETMLIM) { printSolution(context, lp, false); @@ -350,15 +395,28 @@ namespace PetriEngine { // std::cerr << "glpk mip: timeout" << std::endl; } else if (ires == 0) - { + { + #if 1 auto ist = glp_mip_status(lp); + #else + auto ist = glp_get_status(lp); + #endif if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { printSolution(context, lp, true); _result = result_t::POSSIBLE; } else { - _result = result_t::IMPOSSIBLE; + if(context.useBigM()){ + if(checkBigMConstraint(context)){ + _result = result_t::IMPOSSIBLE; + }else{ + _result = result_t::POSSIBLE; + } + } + else{ + _result = result_t::IMPOSSIBLE; + } } } } @@ -369,7 +427,16 @@ namespace PetriEngine { } else { - _result = result_t::IMPOSSIBLE; + if(context.useBigM()){ + if(checkBigMConstraint(context)){ + _result = result_t::IMPOSSIBLE; + }else{ + _result = result_t::POSSIBLE; + } + } + else{ + _result = result_t::IMPOSSIBLE; + } } } else if (result == GLP_ENOPFS || result == GLP_ENODFS || result == GLP_ENOFEAS) @@ -565,7 +632,7 @@ namespace PetriEngine { for (size_t i = 1; i <= nCol; i++) { glp_set_obj_coef(tmp_lp, i, row[i]); glp_set_col_kind(tmp_lp, i, GLP_IV); - glp_set_col_bnds(tmp_lp, i, GLP_LO, 0, infty); + glp_set_col_bnds(tmp_lp, i, GLP_DB, 0, (double) INT32_MAX); } auto rs = glp_simplex(tmp_lp, &settings); diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp index 3b576edd0..3e7c0513e 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -388,6 +388,7 @@ std::vector getLTLQueries(const std::vector& ctlSt return ltlQueries; } + #ifdef VERIFYPN_MC_Simplification std::mutex spot_mutex; #endif @@ -578,7 +579,7 @@ void simplify_queries(const MarkVal* marking, if (options.logic == TemporalLogic::LTL) { if (options.queryReductionTimeout == 0 || qt == 0) continue; SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache, 0, options.lpPrintLevel); + options.lpsolveTimeout, &cache, 0, options.lpPrintLevel, options.lpUseBigM); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction for LTL is skipped.\n"; break; @@ -609,7 +610,7 @@ void simplify_queries(const MarkVal* marking, if (options.queryReductionTimeout > 0 && qt > 0) { SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache, 0, options.lpPrintLevel); + options.lpsolveTimeout, &cache, 0, options.lpPrintLevel, options.lpUseBigM); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction is skipped.\n"; break; From 7cfb5d47ea18e197ae163d8ee44d62ee4b2b9597 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Sat, 28 Feb 2026 13:12:58 +0100 Subject: [PATCH 07/14] lp changes mostly working? --- include/PetriEngine/AbstractPetriNetBuilder.h | 5 + .../Colored/ColoredPetriNetBuilder.h | 8 + include/PetriEngine/Colored/PnmlWriter.h | 19 +- .../ExplicitColored/ColoredResultPrinter.h | 18 +- .../ExplicitColoredInteractiveMode.h | 6 +- .../ExplicitColoredModelChecker.h | 3 +- .../ExplicitColoredPetriNetBuilder.h | 7 + include/PetriEngine/PQL/Contexts.h | 21 +- include/PetriEngine/PQL/Simplifier.h | 9 + .../Simplification/LinearPrograms.h | 2 + include/PetriEngine/options.h | 4 +- include/PetriParse/PNMLParser.h | 4 + .../Colored/ColoredPetriNetBuilder.cpp | 9 +- src/PetriEngine/Colored/PnmlWriter.cpp | 34 ++- .../ExplicitColored/ColoredResultPrinter.cpp | 83 +++++-- .../ExplicitColoredInteractiveMode.cpp | 145 ++++------- .../ExplicitColoredModelChecker.cpp | 8 +- .../ExplicitColoredPetriNetBuilder.cpp | 38 +++ src/PetriEngine/PQL/Contexts.cpp | 25 +- src/PetriEngine/PQL/Simplifier.cpp | 160 ++++++++++-- .../Simplification/LinearProgram.cpp | 231 ++---------------- .../Simplification/LinearPrograms.cpp | 18 +- src/PetriEngine/options.cpp | 29 ++- src/PetriParse/PNMLParser.cpp | 38 +++ src/VerifyPN.cpp | 7 +- 25 files changed, 501 insertions(+), 430 deletions(-) diff --git a/include/PetriEngine/AbstractPetriNetBuilder.h b/include/PetriEngine/AbstractPetriNetBuilder.h index 966a00a27..de275e60a 100644 --- a/include/PetriEngine/AbstractPetriNetBuilder.h +++ b/include/PetriEngine/AbstractPetriNetBuilder.h @@ -105,6 +105,11 @@ namespace PetriEngine { throw base_error("Product colors are not supported in standard P/T nets"); } + virtual void addTokens(std::string&& place, Colored::Multiset&& tokens) + { + throw base_error("Parsing marking is not supported"); + } + virtual void enableColors() { _isColored = true; } diff --git a/include/PetriEngine/Colored/ColoredPetriNetBuilder.h b/include/PetriEngine/Colored/ColoredPetriNetBuilder.h index 4a70e5c65..906130a21 100644 --- a/include/PetriEngine/Colored/ColoredPetriNetBuilder.h +++ b/include/PetriEngine/Colored/ColoredPetriNetBuilder.h @@ -152,6 +152,13 @@ namespace PetriEngine { return _string_set; } + // Since ColoredPetriNetBuilder takes ownership of any colors given to it, we need to be able to tell it to + // forget about those colors and "leak" the memory + void leak_colors() + { + _ownsColors = false; + } + private: shared_name_index_map _placenames; shared_name_index_map _transitionnames; @@ -164,6 +171,7 @@ namespace PetriEngine { Colored::ColorTypeMap _colors; PetriNetBuilder _ptBuilder; shared_string_set& _string_set; + bool _ownsColors = true; void addArc(const std::string& place, const std::string& transition, diff --git a/include/PetriEngine/Colored/PnmlWriter.h b/include/PetriEngine/Colored/PnmlWriter.h index 426caed5a..3a756e519 100644 --- a/include/PetriEngine/Colored/PnmlWriter.h +++ b/include/PetriEngine/Colored/PnmlWriter.h @@ -11,10 +11,23 @@ namespace PetriEngine::Colored { class PnmlWriter { public: - PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0) {} + PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0) + { + for (auto &namedSort: _builder._colors) + { + std::vector types; + ColorType *colortype = const_cast(namedSort.second); + colortype->getColortypes(types); + if (is_number(types[0]->operator[](size_t{0}).getColorName())) { + _namedSortTypes.emplace(colortype->getName(), "finite range"); + } else { + _namedSortTypes.emplace(colortype->getName(), "cyclic enumeration"); + } + } + } void toColPNML(); - + void writeInitialTokens(const std::string& placeId); private: PetriEngine::ColoredPetriNetBuilder &_builder; std::ostream &_out; @@ -77,6 +90,8 @@ namespace PetriEngine::Colored { void handlehlinitialMarking(Multiset marking); + void handleTokenExpression(const Multiset& tokens); + void handleType(const Place &place); void add_arcs_from_transition(Transition &transition); diff --git a/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h b/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h index 79ab674c9..bffe1a1c8 100644 --- a/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h +++ b/include/PetriEngine/ExplicitColored/ColoredResultPrinter.h @@ -2,6 +2,7 @@ #define COLORED_RESULT_PRINTER_H #include "AtomicTypes.h" +#include "ExplicitColoredPetriNetBuilder.h" #include "PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h" #include "PetriEngine/Reachability/ReachabilityResult.h" @@ -28,12 +29,22 @@ namespace PetriEngine::ExplicitColored { bool isInitial; }; + struct ExplicitColoredTraceContext + { + ExplicitColoredTraceContext(std::vector traceSteps, ExplicitColoredPetriNetBuilder cpnBuilder) + : traceSteps(std::move(traceSteps)), cpnBuilder(std::move(cpnBuilder)) {} + ExplicitColoredTraceContext(ExplicitColoredTraceContext&&) = default; + ExplicitColoredTraceContext& operator=(ExplicitColoredTraceContext&&) = default; + std::vector traceSteps; + ExplicitColoredPetriNetBuilder cpnBuilder; + }; + class IColoredResultPrinter { public: virtual void printResult( const SearchStatistics& searchStatistics, Reachability::AbstractHandler::Result result, - const std::vector* trace + const ExplicitColoredTraceContext* trace ) const = 0; virtual void printNonExplicitResult( std::vector techniques, @@ -58,7 +69,7 @@ namespace PetriEngine::ExplicitColored { void printResult( const SearchStatistics& searchStatistics, Reachability::AbstractHandler::Result result, - const std::vector* trace + const ExplicitColoredTraceContext* trace ) const override; void printNonExplicitResult( @@ -67,7 +78,8 @@ namespace PetriEngine::ExplicitColored { ) const override; private: void _printCommon(Reachability::AbstractHandler::Result result, const std::vector& extraTechniques) const; - void _printTrace(const std::vector& trace) const; + void _printTrace(const ExplicitColoredTraceContext& trace) const; + void _printMarkings(const ExplicitColoredPetriNetBuilder& explicitCpnBuilder, const TraceStep& traceStep) const; uint32_t _queryOffset; std::ostream& _stream; std::string _queryName; diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h b/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h index 18ced1178..de9439cfc 100644 --- a/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h +++ b/include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h @@ -12,17 +12,17 @@ namespace PetriEngine::ExplicitColored { public: static int run(const std::string& model_path); private: - ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, const ExplicitColoredPetriNetBuilder& builder); + ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, ExplicitColoredPetriNetBuilder& builder); int _run_internal(); static std::string _readUntilDoubleNewline(std::istream& in); - std::optional _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut) const; + std::optional _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut); std::optional> _parseTransition(const rapidxml::xml_document<>& transitionXml, std::ostream& errorOut) const; void _printCurrentMarking(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const; void _printValidBindings(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const; std::optional _findColorIndex(const Colored::ColorType* colorType, const char* colorName) const; const ColoredSuccessorGenerator& _successorGenerator; const ColoredPetriNet& _cpn; - const ExplicitColoredPetriNetBuilder& _builder; + ExplicitColoredPetriNetBuilder& _builder; }; } #endif //COLOREDINTERACTIVEMODE_H diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h b/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h index 8b3564e4e..1a8d226d1 100644 --- a/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h +++ b/include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h @@ -7,6 +7,7 @@ #include "Visitors/ConditionCopyVisitor.h" #include "ColoredResultPrinter.h" +#include "ExplicitColoredPetriNetBuilder.h" #include "Algorithms/ExplicitWorklist.h" namespace PetriEngine::ExplicitColored { @@ -34,7 +35,7 @@ namespace PetriEngine::ExplicitColored { options_t& options ) const; - std::pair>> explicitColorCheck( + std::pair> explicitColorCheck( const std::string& pnmlModel, const PQL::Condition_ptr& query, options_t& options, diff --git a/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h b/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h index e9d0c28ab..c8caba042 100644 --- a/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h +++ b/include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h @@ -1,5 +1,7 @@ #ifndef EXPLICIT_COLORED_PETRI_NET_BUILDER_H #define EXPLICIT_COLORED_PETRI_NET_BUILDER_H +#include + #include "PetriEngine/AbstractPetriNetBuilder.h" #include "ColoredPetriNet.h" @@ -27,6 +29,7 @@ namespace PetriEngine::ExplicitColored { void addColorType(const std::string& id, const Colored::ColorType* type) override; void addVariable(const Colored::Variable* variable) override; void addToColorType(Colored::ProductType* colorType, const Colored::ColorType* newConstituent) override; + void addTokens(std::string&& place, Colored::Multiset&& tokens) override; void sort() override; const std::unordered_map& getPlaceIndices() const; @@ -45,6 +48,8 @@ namespace PetriEngine::ExplicitColored { ColoredPetriNetBuilderStatus build(); ColoredPetriNet takeNet(); + + ColoredPetriNetMarking parseMarking(const rapidxml::xml_document<>& markingXml); private: std::unordered_map _underlyingColorType; std::unordered_map _placeIndices; @@ -66,6 +71,8 @@ namespace PetriEngine::ExplicitColored { std::unordered_map _transitionToId; std::unordered_map _variableToId; + bool _parsingStandAloneMarking = false; + ColoredPetriNetMarking _standAloneMarking; void _createArcsAndTransitions(); ColoredPetriNetBuilderStatus _calculateTransitionVariables(); void _calculatePrePlaceConstraints(); diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index c4d7e2e91..929557f94 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -179,19 +179,17 @@ namespace PetriEngine { public: SimplificationContext(const MarkVal* marking, - const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, - Simplification::LPCache* cache, uint32_t potencyTimeout = 0, uint32_t printLevel = 0, bool useBigM = true) - : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), + const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, uint32_t lpPrintLevel, + Simplification::LPCache* cache, uint32_t potencyTimeout = 0) + : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), _lpPrintLevel(lpPrintLevel), _potencyTimeout(potencyTimeout) { _negated = false; - _useBigM = useBigM; _marking = marking; _net = net; _base_lp = buildBase(); _start = std::chrono::high_resolution_clock::now(); _cache = cache; _markingOutOfBounds = false; - _printLevel = printLevel; for(size_t i = 0; i < net->numberOfPlaces(); ++i) { if (marking[i] > std::numeric_limits::max()) { //too many tokens exceeding int32_t limits, LP solver will give wrong results _markingOutOfBounds = true; @@ -232,14 +230,6 @@ namespace PetriEngine { double getReductionTime(); - uint32_t getPrintLevel() const{ - return _printLevel; - } - - bool useBigM() const { - return _useBigM; - } - bool timeout() const { auto end = std::chrono::high_resolution_clock::now(); auto diff = std::chrono::duration_cast(end - _start); @@ -254,6 +244,7 @@ namespace PetriEngine { uint32_t getLpTimeout() const; uint32_t getPotencyTimeout() const; + uint32_t getPrintLevel() const; Simplification::LPCache* cache() const { @@ -264,12 +255,10 @@ namespace PetriEngine { private: bool _negated; - bool _useBigM; const MarkVal* _marking; bool _markingOutOfBounds; const PetriNet* _net; - uint32_t _queryTimeout, _lpTimeout, _potencyTimeout; - uint32_t _printLevel; + uint32_t _queryTimeout, _lpTimeout, _lpPrintLevel, _potencyTimeout; mutable glp_prob* _base_lp = nullptr; std::chrono::high_resolution_clock::time_point _start; Simplification::LPCache* _cache; diff --git a/include/PetriEngine/PQL/Simplifier.h b/include/PetriEngine/PQL/Simplifier.h index d96e8e3ff..d04a4bb52 100644 --- a/include/PetriEngine/PQL/Simplifier.h +++ b/include/PetriEngine/PQL/Simplifier.h @@ -39,6 +39,13 @@ namespace PetriEngine { namespace PQL { SimplificationContext& _context; Retval _return_value; + enum LPQUANT {NONE, GLOBAL, FINAL, NONGLOBAL}; + LPQUANT quantifier_found = LPQUANT::NONE; + bool found_global_condition = false; + bool in_global_cond = false; + bool in_and_subexpr = false; + bool in_or_subexpr = false; + Retval simplify_or(const LogicalCondition* element); Retval simplify_and(const LogicalCondition *element); @@ -50,6 +57,8 @@ namespace PetriEngine { namespace PQL { Retval simplify_EF(Retval &r); Retval simplify_EX(Retval &r); + Retval simplify_global_quantifier(Retval &r); + template Retval simplify_simple_quantifier(Retval &r); diff --git a/include/PetriEngine/Simplification/LinearPrograms.h b/include/PetriEngine/Simplification/LinearPrograms.h index 0b222ebf6..c96ce1c78 100644 --- a/include/PetriEngine/Simplification/LinearPrograms.h +++ b/include/PetriEngine/Simplification/LinearPrograms.h @@ -31,9 +31,11 @@ namespace PetriEngine { virtual void clear() = 0; virtual void reset() = 0; + //virtual AbstractProgramCollection clone() = 0; virtual size_t size() const = 0; virtual bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) = 0; + virtual uint32_t explorePotency(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved = std::numeric_limits::max()); diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h index 66a8c29c5..3df53c6f2 100644 --- a/include/PetriEngine/options.h +++ b/include/PetriEngine/options.h @@ -62,9 +62,7 @@ struct options_t { StatisticsLevel printstatistics = StatisticsLevel::Full; std::set querynumbers; Strategy strategy = Strategy::DEFAULT; - int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, initPotencyTimeout = 10; - bool lpUseBigM = true; - int lpPrintLevel = 0; + int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, lpPrintLevel = 0, initPotencyTimeout = 10; TraceLevel trace = TraceLevel::None; bool use_query_reductions = true; uint32_t siphontrapTimeout = 0; diff --git a/include/PetriParse/PNMLParser.h b/include/PetriParse/PNMLParser.h index 061377ca1..3b841c892 100644 --- a/include/PetriParse/PNMLParser.h +++ b/include/PetriParse/PNMLParser.h @@ -79,6 +79,10 @@ class PNMLParser { return queries; } + void parseMarking( + const rapidxml::xml_document<>& doc, + PetriEngine::AbstractPetriNetBuilder* builder, + ColorTypeMap* colorTypes); private: void parseElement(rapidxml::xml_node<>* element); void parsePlace(rapidxml::xml_node<>* element); diff --git a/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp b/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp index 0e00c2bea..594d6fee6 100644 --- a/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp +++ b/src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp @@ -35,9 +35,12 @@ namespace PetriEngine { ColoredPetriNetBuilder::~ColoredPetriNetBuilder() { // cleaning up colors - for(auto& e : _colors) - if(e.second != Colored::ColorType::dotInstance()) - delete e.second; + if (_ownsColors) + { + for(auto& e : _colors) + if(e.second != Colored::ColorType::dotInstance()) + delete e.second; + } for(auto& v : _variables) delete v; _colors.clear(); diff --git a/src/PetriEngine/Colored/PnmlWriter.cpp b/src/PetriEngine/Colored/PnmlWriter.cpp index c481179fd..d14fb9b09 100644 --- a/src/PetriEngine/Colored/PnmlWriter.cpp +++ b/src/PetriEngine/Colored/PnmlWriter.cpp @@ -16,6 +16,21 @@ namespace PetriEngine { metaInfoClose(); } + void PnmlWriter::writeInitialTokens(const std::string& placeId) + { + const auto it = std::find_if( + _builder._placenames.begin(), + _builder._placenames.end(), + [&](const auto& kv) {return placeId == *kv.first;}); + + if (it == _builder._placenames.end()) + { + throw base_error("Could not write initial tokens, since the place '", placeId, "' does not exist"); + } + + handleTokenExpression(_builder.places()[it->second].marking); + } + void PnmlWriter::metaInfo() { _out << getTabs() << "\n" << getTabs() << "\n" @@ -60,10 +75,8 @@ namespace PetriEngine { //this is a hack, better way to find if a color is a finite int range? if (is_number(types[0]->operator[](size_t{0}).getColorName())) { - _namedSortTypes.emplace(colortype->getName(), "finite range"); handleFiniteRange(types); } else { - _namedSortTypes.emplace(colortype->getName(), "cyclic enumeration"); if (types[0]->getName() == "dot") { _out << increaseTabs() << "\n"; } else { @@ -216,11 +229,19 @@ namespace PetriEngine { _out << increaseTabs() << "" << marking.toString() << "\n"; _out << getTabs() << "\n"; - if (marking.size() > 1) { + handleTokenExpression(marking); + + _out << decreaseTabs() << "\n"; + _out << decreaseTabs() << "\n"; + } + + void PnmlWriter::handleTokenExpression(const Multiset& tokens) + { + if (tokens.size() > 1) { bool first = true; _out << increaseTabs() << "\n"; - for (const auto &p: marking) { + for (const auto &p: tokens) { if (p.second == 0) { continue; } @@ -235,16 +256,13 @@ namespace PetriEngine { } _out << decreaseTabs() << "\n"; } else { - for (const auto &p: marking) { + for (const auto &p: tokens) { if (p.second == 0) { continue; } handleNumberOf(p); } } - - _out << decreaseTabs() << "\n"; - _out << decreaseTabs() << "\n"; } void PnmlWriter::handleNumberOf(std::pair numberOff) { diff --git a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp index c35ec229d..72746a037 100644 --- a/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp +++ b/src/PetriEngine/ExplicitColored/ColoredResultPrinter.cpp @@ -1,12 +1,13 @@ #include "PetriEngine/ExplicitColored/ColoredResultPrinter.h" - #include +#include "PetriEngine/Colored/PnmlWriter.h" + namespace PetriEngine::ExplicitColored { void ColoredResultPrinter::printResult( const SearchStatistics& searchStatistics, const Reachability::AbstractHandler::Result result, - const std::vector* trace + const ExplicitColoredTraceContext* trace ) const { _printCommon(result, {}); _stream << "STATS:" << std::endl @@ -59,10 +60,10 @@ namespace PetriEngine::ExplicitColored { std::cout << "satisfied" << std::endl; } - void ColoredResultPrinter::_printTrace(const std::vector& trace) const { + void ColoredResultPrinter::_printTrace(const ExplicitColoredTraceContext& trace) const { _traceStream << "Trace: " << std::endl; _traceStream << "" << std::endl; - for (const auto& step : trace) { + for (const auto& step : trace.traceSteps) { if (!step.isInitial) { _traceStream << "\t" << std::endl; _traceStream << "\t\t" << std::endl; @@ -75,24 +76,70 @@ namespace PetriEngine::ExplicitColored { _traceStream << "\t" << std::endl; } _traceStream << "\t" << std::endl; - for (const auto& [placeId, marking] : step.marking) { - if (!marking.empty()) { - _traceStream << "\t\t" << std::endl; - for (const auto& [productColor, count] : marking) { - if (count > 0) { - _traceStream << "\t\t\t" << std::endl; - for (const auto& color : productColor) { - _traceStream << "\t\t\t\t" << color << "" << std::endl; - } - _traceStream << "\t\t\t" << std::endl; - } + _printMarkings(trace.cpnBuilder, step); + _traceStream << "\t" << std::endl; + } + _traceStream << "" << std::endl; + } + + void ColoredResultPrinter::_printMarkings( + const ExplicitColoredPetriNetBuilder& explicitCpnBuilder, const TraceStep& traceStep) const + { + shared_string_set sharedStringSet {}; + ColoredPetriNetBuilder builder(sharedStringSet); + for (const auto colorType : explicitCpnBuilder.getUnderlyingVariableColorTypes()) + { + builder.addColorType(colorType->getName(), colorType); + } + + for (const auto& [place_id, traceTokens] : traceStep.marking) { + const auto place = explicitCpnBuilder.getPlaceIndices().find(place_id)->second; + + Colored::Multiset tokens; + const auto& colorType = *explicitCpnBuilder.getPlaceUnderlyingColorType(place); + for (const auto& [color, count] : traceTokens) + { + if (color.size() > 1) + { + const auto productColorType = dynamic_cast(&colorType); + if (productColorType == nullptr) { + throw std::runtime_error("Trace color is inconsistent with underlying color type"); } - _traceStream << "\t\t" << std::endl; + + std::vector colorIndices; + for (size_t colorTypeIndex = 0; colorTypeIndex < color.size(); colorTypeIndex++) { + colorIndices.push_back( + (*productColorType->getNestedColorType(colorTypeIndex))[color[colorTypeIndex]]->getId()); + } + + tokens[productColorType->getColor(colorIndices)] = count; + } + else + { + tokens[colorType[color[0]]] = count; } } - _traceStream << "\t" << std::endl; + + builder.addPlace( + explicitCpnBuilder.getPlaceName(place), + explicitCpnBuilder.getPlaceUnderlyingColorType(place), + std::move(tokens), + 0, + 0); + } + + Colored::PnmlWriter writer(builder, _traceStream); + builder.leak_colors(); + + for (const auto& [place_id, traceTokens] : traceStep.marking) + { + if (!traceTokens.empty()) + { + _traceStream << "\t\t" << std::endl; + writer.writeInitialTokens(place_id); + _traceStream << "\t\t" << std::endl; + } } - _traceStream << "" << std::endl; } } diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp index 075035a1d..f5e11b1dc 100644 --- a/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp +++ b/src/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.cpp @@ -8,6 +8,10 @@ #include #include #include +#include +#include + +#include "PetriParse/PNMLParser.h" namespace PetriEngine::ExplicitColored { int ExplicitColoredInteractiveMode::run(const std::string &model_path) { @@ -33,7 +37,7 @@ namespace PetriEngine::ExplicitColored { ExplicitColoredInteractiveMode::ExplicitColoredInteractiveMode( const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, - const ExplicitColoredPetriNetBuilder& builder + ExplicitColoredPetriNetBuilder& builder ) : _successorGenerator(successorGenerator), _cpn(cpn), _builder(builder) { } @@ -115,6 +119,9 @@ namespace PetriEngine::ExplicitColored { } void ExplicitColoredInteractiveMode::_printValidBindings(std::ostream &out, const ColoredPetriNetMarking ¤tMarking) const { + // We always use the same state id in interactive mode, therefore we need to shrink state everytime + // to clear the generated color constraint data + _successorGenerator.shrinkState(0); out << "" << std::endl; for (Transition_t transition = 0; transition < _cpn.getTransitionCount(); transition++) { Binding_t currentBinding = 0; @@ -163,92 +170,8 @@ namespace PetriEngine::ExplicitColored { std::optional ExplicitColoredInteractiveMode::_parseMarking( const rapidxml::xml_document<>& markingXml, std::ostream& errorOut - ) const { - const auto root = markingXml.first_node(); - - ColoredPetriNetMarking generatedMarking; - generatedMarking.markings.resize(_builder.getPlaceCount()); - - auto placeNode = root->first_node(); - if (root->name() != std::string("marking")) { - errorOut << "Unexpected tag " << std::quoted(root->name()) << std::endl; - return std::nullopt; - } - - if (placeNode == nullptr) { - return generatedMarking; // Empty marking - } - - do { - if (placeNode->name() != std::string("place")) { - errorOut << "Unexpected tag " << std::quoted(placeNode->name()) << std::endl; - return std::nullopt; - } - - if (placeNode->first_attribute("id") == nullptr) { - errorOut << "Place tag is missing id attribute" << std::endl; - return std::nullopt; - } - - auto markingPlaceIndexIt = _builder.getPlaceIndices().find(placeNode->first_attribute("id")->value()); - if (markingPlaceIndexIt == _builder.getPlaceIndices().end()) { - errorOut << "Unknown place id " << std::quoted(placeNode->first_attribute("id")->value()) << std::endl; - return std::nullopt; - } - auto tokenNode = placeNode->first_node(); - auto placeColorType = _builder.getPlaceUnderlyingColorType(markingPlaceIndexIt->second); - do { - if (tokenNode->name() != std::string("token")) { - errorOut << "Unexpected tag " << std::quoted(tokenNode->name()) << std::endl; - return std::nullopt; - } - if (tokenNode->first_attribute("count") == nullptr) { - errorOut << "Token tag is missing count attribute" << std::endl; - return std::nullopt; - } - auto count = 0; - try { - count = std::stoi(tokenNode->first_attribute("count")->value()); - } catch (const std::out_of_range&) { - errorOut << "Token count " << tokenNode->first_attribute("count")->value() << " is too big or too small" << std::endl; - return std::nullopt; - } catch (const std::invalid_argument&) { - errorOut << "Token count " << tokenNode->first_attribute("count")->value() << " could not be parsed" << std::endl; - return std::nullopt; - } - auto colorComponentNode = tokenNode->first_node(); - uint64_t encodedColor = 0; - const auto& colorCodec = _cpn.getPlaces()[markingPlaceIndexIt->second].colorType->colorCodec; - auto componentIndex = 0; - do { - if (colorComponentNode->name() != std::string("color")) { - errorOut << "Unexpected tag " << colorComponentNode->name() << std::endl; - return std::nullopt; - } - if (colorComponentNode->type() != rapidxml::node_element) { - errorOut << "Expected color tag to only contain color id" << std::endl; - return std::nullopt; - } - const auto colorName = colorComponentNode->value(); - auto currentColorType = placeColorType; - if (auto productColor = dynamic_cast(placeColorType)) { - currentColorType = productColor->getNestedColorType(componentIndex); - } - - auto colorIndex = _findColorIndex(currentColorType, colorName); - if (colorIndex == std::nullopt) { - errorOut << "Unknown color id " << std::quoted(colorName) << std::endl; - return std::nullopt; - } - encodedColor = colorCodec.addToValue(encodedColor, componentIndex, *colorIndex); - - componentIndex++; - } while ((colorComponentNode = colorComponentNode->next_sibling()) != nullptr); - generatedMarking.markings[markingPlaceIndexIt->second].addCount(encodedColor, count); - } while ((tokenNode = tokenNode->next_sibling()) != nullptr); - } while ((placeNode = placeNode->next_sibling()) != nullptr); - - return generatedMarking; + ) { + return _builder.parseMarking(markingXml); } std::optional> ExplicitColoredInteractiveMode::_parseTransition( @@ -333,37 +256,55 @@ namespace PetriEngine::ExplicitColored { std::ostream &out, const ColoredPetriNetMarking ¤tMarking ) const { - out << "" << std::endl; - for (Place_t place = 0; place < currentMarking.markings.size(); place++) { - out << "\t" << std::endl; + shared_string_set sharedStringSet {}; + ColoredPetriNetBuilder builder(sharedStringSet); + builder.leak_colors(); + for (Place_t place = 0; place < currentMarking.markings.size(); place++) + { + builder.addColorType(_builder.getPlaceName(place), _builder.getPlaceUnderlyingColorType(place)); + + Colored::Multiset tokens; const auto& colorCodec = _cpn.getPlaces()[place].colorType->colorCodec; const auto& colorType = *_builder.getPlaceUnderlyingColorType(place); for (const auto& [encodedColor, count] : currentMarking.markings[place].counts()) { if (count > 0) { - out << "\t\t" << std::endl; if (colorCodec.getColorCount() > 1) { const auto productColorType = dynamic_cast(&colorType); if (productColorType == nullptr) { throw std::runtime_error("Color codec is inconsistent with underlying color type"); } + std::vector colorIndices; for (size_t colorIndex = 0; colorIndex < colorCodec.getColorCount(); colorIndex++) { - const Color_t color = colorCodec.decode(encodedColor, colorIndex); - out << "\t\t\t" - << (*(productColorType->getNestedColorType(colorIndex)))[color].getColorName() - << "" - << std::endl; + colorIndices.push_back(colorCodec.decode(encodedColor, colorIndex)); } + + tokens[productColorType->getColor(colorIndices)] += count; } else { - out << "\t\t\t" - << colorType[encodedColor].getColorName() - << "" - << std::endl; + tokens[&colorType[encodedColor]] += count; } - out << "\t\t" << std::endl; } } - out << "\t" << std::endl; + + builder.addPlace( + _builder.getPlaceName(place), + _builder.getPlaceUnderlyingColorType(place), + std::move(tokens), + 0, + 0); + } + + + Colored::PnmlWriter pnmlWriter(builder, out); + out << "" << std::endl; + for (Place_t place = 0; place < currentMarking.markings.size(); place++) { + if (currentMarking.markings[place].totalCount() > 0) + { + out << "\t" << std::endl; + pnmlWriter.writeInitialTokens(_builder.getPlaceName(place)); + out << "\t" << std::endl; + } } out << "" << std::endl; + } } diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp index 2f5882ab7..3cc4d9b96 100644 --- a/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp +++ b/src/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.cpp @@ -238,7 +238,7 @@ namespace PetriEngine::ExplicitColored { return Result::UNKNOWN; } - std::pair>> ExplicitColoredModelChecker::explicitColorCheck( + std::pair> ExplicitColoredModelChecker::explicitColorCheck( const std::string& pnmlModel, const Condition_ptr& query, options_t& options, @@ -268,18 +268,18 @@ namespace PetriEngine::ExplicitColored { *searchStatistics = worklist.GetSearchStatistics(); } - std::optional> trace = std::nullopt; + std::optional traceContext = std::nullopt; if (options.trace != TraceLevel::None) { auto counterExample = worklist.getCounterExampleId(); if (counterExample.has_value()) { auto internalTrace = worklist.getTraceTo(counterExample.value()); if (internalTrace.has_value()) { - trace = _translateTraceStep(internalTrace.value(), cpnBuilder, net); + traceContext.emplace(_translateTraceStep(internalTrace.value(), cpnBuilder, net), std::move(cpnBuilder)); } } } - return std::make_pair(result ? Result::SATISFIED : Result::UNSATISFIED, trace); + return std::make_pair(result ? Result::SATISFIED : Result::UNSATISFIED, std::move(traceContext)); } void ExplicitColoredModelChecker::_reduce( diff --git a/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp b/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp index 6defb57cb..09ed11eba 100644 --- a/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp +++ b/src/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.cpp @@ -2,6 +2,7 @@ #include "PetriEngine/ExplicitColored/ExpressionCompilers/ArcCompiler.h" #include "PetriEngine/ExplicitColored/ExpressionCompilers/GuardCompiler.h" #include +#include "PetriParse/PNMLParser.h" namespace PetriEngine::ExplicitColored { ExplicitColoredPetriNetBuilder::ExplicitColoredPetriNetBuilder() { @@ -156,6 +157,34 @@ namespace PetriEngine::ExplicitColored { colorType->addType(newConstituent); } + void ExplicitColoredPetriNetBuilder::addTokens(std::string&& place, Colored::Multiset&& tokens) + { + const auto placeId = _placeIndices.find(place); + if (placeId == _placeIndices.end()) + { + throw base_error("Unknown place name ", place); + } + + const auto underlyingColorType = getPlaceUnderlyingColorType(placeId->second); + + CPNMultiSet multiSet; + const auto& colorType = _colorTypeMap.find(underlyingColorType->getName())->second; + for (const auto& [tokenColor, count] : tokens) { + std::vector colorSequence; + if (tokenColor->isTuple()) { + for (const auto& color : tokenColor->getTupleColors()) { + colorSequence.push_back(color->getId()); + } + } else { + colorSequence.push_back(tokenColor->getId()); + } + multiSet.setCount(ColorSequence{colorSequence, *colorType}, count); + } + + + _standAloneMarking.markings[placeId->second] = multiSet; + } + void ExplicitColoredPetriNetBuilder::addVariable(const Colored::Variable* variable) { (*_variableMap)[variable->name] = _variableMap->size(); const auto colorType = _colorTypeMap.find(variable->colorType->getName())->second; @@ -203,6 +232,15 @@ namespace PetriEngine::ExplicitColored { return std::move(_currentNet); } + ColoredPetriNetMarking ExplicitColoredPetriNetBuilder::parseMarking(const rapidxml::xml_document<>& doc) + { + _standAloneMarking = ColoredPetriNetMarking(); + _standAloneMarking.markings.resize(getPlaceCount()); + PNMLParser parser; + parser.parseMarking(doc, this, _colors.get()); + return _standAloneMarking; + } + void ExplicitColoredPetriNetBuilder::_createArcsAndTransitions() { const auto transitions = _currentNet._transitions.size(); auto transIndices = std::vector>(transitions + 1); diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index a1f486878..6090c8047 100644 --- a/src/PetriEngine/PQL/Contexts.cpp +++ b/src/PetriEngine/PQL/Contexts.cpp @@ -68,6 +68,11 @@ namespace PetriEngine { return _potencyTimeout; } + uint32_t SimplificationContext::getPrintLevel() const + { + return _lpPrintLevel; + } + double SimplificationContext::getReductionTime() { // duration in seconds @@ -153,26 +158,6 @@ namespace PetriEngine { return nullptr; } } - - /*glp_add_rows(lp, _net->numberOfPlaces()); - for (size_t p = 0; p < _net->numberOfPlaces(); p++) { - std::vector row(nCol+1, 0); - std::vector indices(1, 0); - row.shrink_to_fit(); - - for (size_t t = 0; t < _net->numberOfTransitions(); t++) { - if(_net->outArc(t, p) - _net->inArc(p, t) != 0){ - row[t+1] = _net->outArc(t, p); - row[t+1] -= _net->inArc(p, t); - indices.push_back(t+1); - } - } - - glp_set_mat_row(lp, rowno, indices.size() - 1, indices.data(), row.data()); - glp_set_row_bnds(lp, rowno, GLP_LO, -1.0 * marking()[p], infty); - ++rowno; - }*/ - return lp; } } diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 85499d9b6..d0337c5e2 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -30,6 +30,7 @@ namespace PetriEngine { namespace PQL { } AbstractProgramCollection_ptr mergeLps(std::vector &&lps) { + std::cout << "merging Lps with " << lps.size() << " Elements\n"; if (lps.size() == 0) return nullptr; int j = 0; int i = lps.size() - 1; @@ -44,12 +45,43 @@ namespace PetriEngine { namespace PQL { return lps[0]; } - Retval Simplifier::simplify_or(const LogicalCondition *element) { + AbstractProgramCollection_ptr createGlobalUnion(AbstractProgramCollection_ptr &global_lp, std::vector &&nonglobal_lps) { + std::cout << "creating unioncollection of global and nonglobal conditions\n"; + + if(global_lp == nullptr) + return std::make_shared(std::move(nonglobal_lps)); + + if(nonglobal_lps.size() == 0) + return global_lp; + + + std::vector merges; + + for(int i = 0; i < nonglobal_lps.size(); i++){ + merges.emplace_back(std::make_shared(global_lp, nonglobal_lps[i])); + } + + return std::make_shared(std::move(merges)); + } + + Retval Simplifier::simplify_or(const LogicalCondition *element) { + std::cout << "simplifying or\n"; std::vector conditions; - std::vector lps, neglpsv; + std::vector lps; + std::vector global_neglpsv; + std::vector nonglobal_neglpsv; + //std::vector neggconds; + + bool was_and_subexpr = in_and_subexpr; + + for (const auto &c: element->getOperands()) { + found_global_condition = false; + in_and_subexpr = false; + quantifier_found = LPQUANT::NONE; Visitor::visit(this, c); + auto r = std::move(_return_value); assert(r.neglps); assert(r.lps); @@ -61,10 +93,22 @@ namespace PetriEngine { namespace PQL { } conditions.push_back(r.formula); lps.push_back(r.lps); - neglpsv.emplace_back(r.neglps); + + if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::FINAL){ + global_neglpsv.emplace_back(r.neglps); + }else{ + nonglobal_neglpsv.emplace_back(r.neglps); + } + + //neggconds.emplace_back(!found_global_condition); + + found_global_condition = false; + + in_and_subexpr = was_and_subexpr; } - AbstractProgramCollection_ptr neglps = mergeLps(std::move(neglpsv)); + AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv)); + neglps = createGlobalUnion(neglps, std::move(nonglobal_neglpsv)); if (conditions.size() == 0) { return Retval(BooleanCondition::FALSE_CONSTANT); @@ -83,7 +127,7 @@ namespace PetriEngine { namespace PQL { // Lets try to see if the r1 AND r2 can ever be false at the same time // If not, then we know that r1 || r2 must be true. // we check this by checking if !r1 && !r2 is unsat - + std::cout << "leaving or\n"; return Retval( makeOr(conditions), std::make_shared(std::move(lps)), @@ -91,12 +135,25 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_and(const LogicalCondition *element) { - + std::cout << "simplifying and\n"; std::vector conditions; - std::vector lpsv; + std::vector global_lpsv; + std::vector nonglobal_lpsv; + //std::vector lpsv; std::vector neglps; + + + + bool was_and_subexpr = in_and_subexpr; + int global_count = 0; + for (auto &c: element->getOperands()) { + in_and_subexpr = true; + found_global_condition = false; + quantifier_found = LPQUANT::NONE; Visitor::visit(this, c); + global_count += (found_global_condition );//&& in_and_subexpr); + auto r = std::move(_return_value); if (r.formula->isTriviallyFalse()) { return Retval(BooleanCondition::FALSE_CONSTANT); @@ -105,15 +162,30 @@ namespace PetriEngine { namespace PQL { } conditions.push_back(r.formula); - lpsv.emplace_back(r.lps); + + if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::GLOBAL){ + global_lpsv.emplace_back(r.lps); + }else{ + nonglobal_lpsv.emplace_back(r.lps); + } + //if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::FINAL) neglps.emplace_back(r.neglps); + //gconds.emplace_back(found_global_condition); + + found_global_condition = false; + + in_and_subexpr = was_and_subexpr; } + //std::cout << "and had [" << global_count << "] global conditions\n"; + if (conditions.size() == 0) { return Retval(BooleanCondition::TRUE_CONSTANT); } - auto lps = mergeLps(std::move(lpsv)); + auto lps = mergeLps(std::move(global_lpsv)); + lps = createGlobalUnion(lps, std::move(nonglobal_lpsv)); + try { if (!_context.timeout() && !lps->satisfiable(_context)) { @@ -125,10 +197,12 @@ namespace PetriEngine { namespace PQL { std::cout << "Query reduction: memory exceeded during LPS merge." << std::endl; } + // Lets try to see if the r1 AND r2 can ever be false at the same time // If not, then we know that r1 || r2 must be true. // we check this by checking if !r1 && !r2 is unsat + return Retval( makeAnd(conditions), std::move(lps), @@ -198,15 +272,56 @@ namespace PetriEngine { namespace PQL { } } + /*Retval Simplifier::simplify_global_quantifier(Retval &r) { + //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n"; + //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n"; + quantifier_found = LPQUANT::GLOBAL; + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } else { + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + } + }*/ + template Retval Simplifier::simplify_simple_quantifier(Retval &r) { + std::cout << "other quantifier\n"; static_assert(std::is_base_of_v); + quantifier_found = LPQUANT::NONGLOBAL; + //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n"; + //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n"; + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } else { + return Retval(std::make_shared(r.formula));//, r.lps, r.neglps); + } + } + + template<> + Retval Simplifier::simplify_simple_quantifier(Retval &r){ + quantifier_found = LPQUANT::GLOBAL; if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { return Retval(BooleanCondition::TRUE_CONSTANT); } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { - return Retval(std::make_shared(r.formula)); + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + } + } + + template<> + Retval Simplifier::simplify_simple_quantifier(Retval &r){ + quantifier_found = LPQUANT::FINAL; + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } else { + return Retval(std::make_shared(r.formula), r.lps, r.neglps); } } @@ -300,6 +415,7 @@ namespace PetriEngine { namespace PQL { /******* Simplifier accepts ********/ void Simplifier::_accept(const NotCondition *element) { + std::cout << "negating\n"; _context.negate(); Visitor::visit(this, element->getCond()); _context.negate(); @@ -896,14 +1012,30 @@ namespace PetriEngine { namespace PQL { void Simplifier::_accept(const FCondition *condition) { Visitor::visit(this, condition->getCond()); - RETURN(_context.negated() ? simplify_simple_quantifier(_return_value) - : simplify_simple_quantifier(_return_value)) + if(_context.negated()){ + std::cout << "negated GCondition\n"; + //SET_GLOBAL(true); + auto r = simplify_simple_quantifier(_return_value); + found_global_condition = true; + //RESTORE_GLOBAL; + RETURN(std::move(r)); + }else{ + std::cout << "FCondition\n"; + RETURN(simplify_simple_quantifier(_return_value)); + } } void Simplifier::_accept(const GCondition *condition) { Visitor::visit(this, condition->getCond()); - RETURN(_context.negated() ? simplify_simple_quantifier(_return_value) - : simplify_simple_quantifier(_return_value)) + if(_context.negated()){ + std::cout << "negated FCondition\n"; + RETURN(simplify_simple_quantifier(_return_value)); + }else{ + std::cout << "GCondition\n"; + auto r = simplify_simple_quantifier(_return_value); + found_global_condition = true; + RETURN(std::move(r)) + } } void Simplifier::_accept(const XCondition *condition) { diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index cd6330995..9f822df6f 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -6,7 +6,6 @@ #include "PetriEngine/Simplification/LinearProgram.h" #include "PetriEngine/Simplification/LPCache.h" #include "PetriEngine/PQL/Contexts.h" -#include "VerifyPN.h" namespace PetriEngine { namespace Simplification { @@ -54,6 +53,10 @@ namespace PetriEngine { } void printConstraints(const PQL::SimplificationContext& context, glp_prob* lp){ + + if(context.getPrintLevel() < 1) + return; + int nCols = glp_get_num_cols(lp); int nRows = glp_get_num_rows(lp); @@ -61,17 +64,17 @@ namespace PetriEngine { std::vector coef(nCols + 1); int l; + auto nt = context.net()->numberOfTransitions(); + for(int i = 1; i <= nRows; i++){ l = glp_get_mat_row(lp, i, indices.data(), coef.data()); std::cout << "Row " << i << "[len: " << l << "]: "; - - bool first_print = true; for(int j = 1; j <= l; j++){ if(!first_print) std::cout << " + "; - if((indices[j] - 1) < context.net()->numberOfTransitions()){ - std::cout << coef[j] << "*" << *context.net()->transitionNames()[indices[j] - 1]; + if((indices[j] - 1) < nt){ + std::cout << coef[j] << "*t" << (indices[j] - 1) / nt << "." << *context.net()->transitionNames()[(indices[j] - 1) % nt]; }else{ std::cout << coef[j] << "*" << glp_get_col_name(lp, indices[j]); } @@ -106,77 +109,6 @@ namespace PetriEngine { } } - - - void printSolution(const PQL::SimplificationContext& context, glp_prob* lp, bool is_mip){ - if(context.getPrintLevel() == 0) - return; - - if(context.getPrintLevel() > 1){ - printConstraints(context, lp); - } - - int nCols = glp_get_num_cols(lp); - bool first_print = true; - if(is_mip){ - std::cout << "MIP Solution: "; - }else{ - std::cout << "LP Solution: "; - } - for(int i = 1; i <= nCols;i++){ - double coef = (is_mip)? glp_mip_col_val(lp, i) : glp_get_col_prim(lp, i); - if(coef != 0){ - if(!first_print) - std::cout << " + "; - first_print = false; - if( i - 1 < context.net()->numberOfTransitions()){ - std::cout << coef << "*" << *context.net()->transitionNames()[i - 1]; - }else{ - std::cout << coef << "*" << glp_get_col_name(lp, i); - } - } - } - - if(first_print) - std::cout << "\n"; - else{ - std::cout << "\n"; - } - } - - std::vector bigMQuery(const PQL::SimplificationContext& context){ - - std::vector res; - - for(int p = 0; p < context.net()->numberOfPlaces(); p++){ - auto rhs = std::make_shared(context.net()->placeNames()[p]); - auto lhs = std::make_shared(10000); - auto lt = std::make_shared(lhs, rhs); - res.push_back(lt); - } - - auto orQuery = std::make_shared(res); - auto FQuery = std::make_shared(orQuery); - auto EFQuery = std::make_shared(FQuery); - std::vector queries; - queries.push_back(EFQuery); - return queries; - } - - - bool checkBigMConstraint(const PQL::SimplificationContext& context){ - return true; - auto queries = bigMQuery(context); - options_t options; - options.lpUseBigM = false; - simplify_queries(context.marking(), context.net(), queries, options, std::cout); - std::cout << "done big M\n"; - if(queries[0]->isTriviallyFalse()){ - return true; - }else{ - return false; - } - } bool LinearProgram::isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime) { bool use_ilp = true; @@ -197,7 +129,7 @@ namespace PetriEngine { } const uint32_t nCol = net->numberOfTransitions(); - const uint32_t nRow = 2 * net->numberOfPlaces() + _equations.size(); + const uint32_t nRow = net->numberOfPlaces() + _equations.size(); std::vector row = std::vector(nCol + 1); std::vector indir(std::max(nCol, nRow) + 1); @@ -250,108 +182,8 @@ namespace PetriEngine { glp_set_col_bnds(lp, i, GLP_LO, 0, infty); } - if(context.useBigM()){ - for (size_t p = 0; p < net->numberOfPlaces(); p++) { - auto numColsLP = glp_get_num_cols(lp); - std::vector inRow(1, 0); - std::vector inIndices(1, 0); - - std::vector outRow(1, 0); - std::vector outIndices(1, 0); - - - bool has_loop = false; - bool has_in = false; - //bool requires_tokens = false; - - //std::map> loops_by_weight; - //int min_pos_loop = 0; - uint32_t minimum_weight = UINT32_MAX; - - for (size_t t = 0; t < net->numberOfTransitions(); t++) { - if(net->outArc(t, p) != 0 && net->inArc(p, t) != 0){ - has_loop = true; - /*if(net->inArc(p, t) > context.marking()[p]) - requires_tokens = true; - - if(net->outArc(t, p) > net->inArc(p, t) && net->inArc(p, t) < min_pos_loop) - min_pos_loop = net->inArc(p, t);*/ - - minimum_weight = std::min(minimum_weight, net->inArc(p, t)); - - outRow.push_back(1); - outIndices.push_back(t+1); - } - else{ - if(net->inArc(p,t) != 0){ - outRow.push_back(1); - outIndices.push_back(t+1); - } - if(net->outArc(t,p) != 0){ - has_in = true; - - inRow.push_back(net->outArc(t, p)); - inIndices.push_back(t+1); - } - } - } - - if(!has_loop || !has_in || context.marking()[p] >= minimum_weight){ - //std::cout << "no loop applicable\n"; - continue; - } - else{ - //std::cout << "adding loop constraint for " << *net->placeNames()[p] <<"\n"; - } - - int idx = numColsLP + 1; - glp_add_cols(lp, 2); + printConstraints(context, lp); - for(int i = glp_get_num_cols(lp) - 1; i <= glp_get_num_cols(lp); i++){ - glp_set_obj_coef(lp, i, 1); - glp_set_col_kind(lp, i, GLP_BV); - //glp_set_col_bnds(lp, i, GLP_DB, 0.0, 1.0); - } - - const int OR_P = glp_get_num_cols(lp) ; - std::string or_p_name = "NO_IMPLY_" + *net->placeNames()[p]; - glp_set_col_name(lp, OR_P, or_p_name.c_str()); - const int OR_Q = glp_get_num_cols(lp) - 1; - std::string or_q_name = "YES_IMPLY_" + *net->placeNames()[p]; - glp_set_col_name(lp, OR_Q, or_q_name.c_str()); - - const double needed_weight = (double) (minimum_weight - context.marking()[p]); - inRow.push_back(needed_weight); - inIndices.push_back(OR_P); - - outRow.push_back(-1.0 * 10000); - outIndices.push_back(OR_Q); - - glp_add_rows(lp, 3); - - glp_set_mat_row(lp, rowno, inIndices.size() - 1, inIndices.data(), inRow.data()); - glp_set_row_bnds(lp, rowno, GLP_LO, needed_weight, infty); - ++rowno; - - glp_set_mat_row(lp, rowno, outIndices.size() - 1, outIndices.data(), outRow.data()); - glp_set_row_bnds(lp, rowno, GLP_UP, 0.0, 0.0); - ++rowno; - - double orRow[3]; - int orIndices[3]; - - - orRow[1] = 1.0; - orRow[2] = 1.0; - orIndices[1] = OR_P; - orIndices[2] = OR_Q; - - glp_set_mat_row(lp, rowno, 2, orIndices, orRow); - glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); - ++rowno; - } - } - // Minimize the objective glp_set_obj_dir(lp, GLP_MIN); auto stime = glp_time(); @@ -372,71 +204,36 @@ namespace PetriEngine { auto status = glp_get_status(lp); if (status == GLP_OPT) { - - #if 1 glp_iocp iset; glp_init_iocp(&iset); iset.msg_lev = 0; - iset.tol_int = 1e-10; iset.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); iset.presolve = GLP_OFF; auto ires = glp_intopt(lp, &iset); - #else - glp_smcp settings_exact; - settings_exact.msg_lev = 0; - settings_exact.it_lim = INT_MAX; - settings_exact.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); - auto ires = glp_exact(lp, &settings_exact); - #endif if (ires == GLP_ETMLIM) { - printSolution(context, lp, false); _result = result_t::UKNOWN; // std::cerr << "glpk mip: timeout" << std::endl; } else if (ires == 0) - { - #if 1 + { auto ist = glp_mip_status(lp); - #else - auto ist = glp_get_status(lp); - #endif if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { - printSolution(context, lp, true); _result = result_t::POSSIBLE; } else { - if(context.useBigM()){ - if(checkBigMConstraint(context)){ - _result = result_t::IMPOSSIBLE; - }else{ - _result = result_t::POSSIBLE; - } - } - else{ - _result = result_t::IMPOSSIBLE; - } + _result = result_t::IMPOSSIBLE; } } } else if (status == GLP_FEAS || status == GLP_UNBND) { - printSolution(context, lp, false); _result = result_t::POSSIBLE; } else { - if(context.useBigM()){ - if(checkBigMConstraint(context)){ - _result = result_t::IMPOSSIBLE; - }else{ - _result = result_t::POSSIBLE; - } - } - else{ - _result = result_t::IMPOSSIBLE; - } + _result = result_t::IMPOSSIBLE; } } else if (result == GLP_ENOPFS || result == GLP_ENODFS || result == GLP_ENOFEAS) @@ -632,7 +429,7 @@ namespace PetriEngine { for (size_t i = 1; i <= nCol; i++) { glp_set_obj_coef(tmp_lp, i, row[i]); glp_set_col_kind(tmp_lp, i, GLP_IV); - glp_set_col_bnds(tmp_lp, i, GLP_DB, 0, (double) INT32_MAX); + glp_set_col_bnds(tmp_lp, i, GLP_LO, 0, infty); } auto rs = glp_simplex(tmp_lp, &settings); diff --git a/src/PetriEngine/Simplification/LinearPrograms.cpp b/src/PetriEngine/Simplification/LinearPrograms.cpp index a8c311a37..104052e71 100644 --- a/src/PetriEngine/Simplification/LinearPrograms.cpp +++ b/src/PetriEngine/Simplification/LinearPrograms.cpp @@ -12,7 +12,10 @@ namespace PetriEngine { bool AbstractProgramCollection::satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime) { reset(); - if (context.timeout() || has_empty || solvetime == 0) return true; + if (context.timeout() || has_empty || solvetime == 0){ + std::cout << "returning from timeout/empty\n"; + return true; + } if (_result != UNKNOWN) { if (_result == IMPOSSIBLE) @@ -154,8 +157,9 @@ namespace PetriEngine { bool MergeCollection::merge(bool& has_empty, LinearProgram& program, bool dry_run) { - if (program.knownImpossible()) + if (program.knownImpossible()) { return false; + } bool lempty = false; bool more_left; @@ -172,17 +176,21 @@ namespace PetriEngine { left->reset(); merge_right = false; } + ++curr; assert(curr <= _size); + more_left = left->merge(lempty, prog/*, dry_run || curr < nsat*/); if (!more_left) merge_right = true; - if (curr >= nsat || !(more_left || more_right)) + if (curr > nsat || !(more_left || more_right)) { - if ((!dry_run && prog.knownImpossible()) && (more_left || more_right)) + if ((!dry_run && prog.knownImpossible()) && (more_left || more_right)) { continue; + } - if (!dry_run) + if (!dry_run) { program.swap(prog); + } break; } diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp index 7bc04f96e..d9d8e9fa7 100644 --- a/src/PetriEngine/options.cpp +++ b/src/PetriEngine/options.cpp @@ -110,6 +110,17 @@ void options_t::print(std::ostream& optionsOut) { optionsOut << ",LPSolve_Timeout=" << lpsolveTimeout; + switch(lpPrintLevel){ + case 0: + optionsOut << ",LP_Print=DISABLED"; + break; + case 1: + optionsOut << ",LP_Print=Constraints"; + break; + default: + optionsOut << ",LP_Print=Full"; + } + if (usedctl) { if (ctlalgorithm == CTL::CZero) { @@ -185,6 +196,10 @@ void printHelp() { " write --interval-timeout 0 to disable interval limits\n" " --partition-timeout Timeout for color partitioning in seconds (default 5)\n" " -l, --lpsolve-timeout LPSolve timeout in seconds, default 10\n" + " -lpp, --lp-print LP diagnostic print level\n" + " - 0 disabled (default)\n" + " - 1 constraints only\n" + " - 2 constraints and solutions}\n" " -p, --disable-partial-order Disable partial order reduction (stubborn sets)\n" " --ltl-por Select partial order method to use with LTL engine (default automaton).\n" " - automaton apply Büchi-guided stubborn set method (Jensen et al., 2021).\n" @@ -346,13 +361,6 @@ bool options_t::parse(int argc, const char** argv) { if (sscanf(argv[++i], "%d", &queryReductionTimeout) != 1 || queryReductionTimeout < 0) { throw base_error("Argument Error: Invalid query reduction timeout argument ", std::quoted(argv[i])); } - }else if (std::strcmp(argv[i], "-lpp") == 0 || std::strcmp(argv[i], "--lp-print") == 0) { - if (i == argc - 1) { - throw base_error("Missing number after ", std::quoted(argv[i])); - } - if (sscanf(argv[++i], "%d", &lpPrintLevel) != 1 || lpPrintLevel < 0) { - throw base_error("Argument Error: Invalid lp print level argument ", std::quoted(argv[i])); - } } else if (std::strcmp(argv[i], "--init-potency-timeout") == 0) { if (i == argc - 1) { throw base_error("Missing number after ", std::quoted(argv[i])); @@ -381,6 +389,13 @@ bool options_t::parse(int argc, const char** argv) { if (sscanf(argv[++i], "%d", &lpsolveTimeout) != 1 || lpsolveTimeout < 0) { throw base_error("Argument Error: Invalid LPSolve timeout argument ", std::quoted(argv[i])); } + } else if (std::strcmp(argv[i], "-lpp") == 0 || std::strcmp(argv[i], "--lp-print") == 0){ + if (i == argc - 1) { + throw base_error("Missing number after ", std::quoted(argv[i])); + } + if (sscanf(argv[++i], "%d", &lpPrintLevel) != 1 || lpPrintLevel < 0) { + throw base_error("Argument Error: Invalid lpPrintLevel argument ", std::quoted(argv[i])); + } } else if (std::strcmp(argv[i], "-e") == 0 || std::strcmp(argv[i], "--state-space-exploration") == 0) { statespaceexploration = true; computePartition = false; diff --git a/src/PetriParse/PNMLParser.cpp b/src/PetriParse/PNMLParser.cpp index 819246f9f..bc00dd66e 100644 --- a/src/PetriParse/PNMLParser.cpp +++ b/src/PetriParse/PNMLParser.cpp @@ -592,6 +592,44 @@ ArcExpression_ptr PNMLParser::parseNumberOfExpression(rapidxml::xml_node<>* elem return std::make_shared(std::move(result)); } +void PNMLParser::parseMarking(const rapidxml::xml_document<>& doc, PetriEngine::AbstractPetriNetBuilder* builder, + ColorTypeMap* colorTypes) +{ + this->colorTypes = *colorTypes; + this->builder = builder; + + rapidxml::xml_node<>* root = doc.first_node(); + if(strcmp(root->name(), "marking") != 0) + { + throw base_error("expected marking tag, got ", root->name()); + } + + for (auto child = root->first_node(); child != nullptr; child = child->next_sibling()) + { + if (strcmp(child->name(), "place") != 0) + { + throw base_error("expected only place tags in marking, got ", child->name()); + } + + const auto idAttribute = child->first_attribute("id"); + + if (idAttribute == nullptr) + { + throw base_error("expected place to have id attribute"); + } + + std::string id = idAttribute->value(); + + std::unordered_map binding; + EquivalenceVec placePartition; + ExpressionContext context {binding, *colorTypes, placePartition}; + auto ae = parseArcExpression(child->first_node()); + auto initialMarking = EvaluationVisitor::evaluate(*ae, context); + + builder->addTokens(std::move(id), std::move(initialMarking)); + } +} + void PNMLParser::parseElement(rapidxml::xml_node<>* element) { for (auto it = element->first_node(); it; it = it->next_sibling()) { diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp index 3e7c0513e..a58f0640b 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -388,7 +388,6 @@ std::vector getLTLQueries(const std::vector& ctlSt return ltlQueries; } - #ifdef VERIFYPN_MC_Simplification std::mutex spot_mutex; #endif @@ -579,7 +578,7 @@ void simplify_queries(const MarkVal* marking, if (options.logic == TemporalLogic::LTL) { if (options.queryReductionTimeout == 0 || qt == 0) continue; SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache, 0, options.lpPrintLevel, options.lpUseBigM); + options.lpsolveTimeout, options.lpPrintLevel, &cache); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction for LTL is skipped.\n"; break; @@ -610,7 +609,7 @@ void simplify_queries(const MarkVal* marking, if (options.queryReductionTimeout > 0 && qt > 0) { SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache, 0, options.lpPrintLevel, options.lpUseBigM); + options.lpsolveTimeout, options.lpPrintLevel, &cache); if (simplificationContext.markingOutOfBounds()) { std::cout << "WARNING: Initial marking contains a place or places with too many tokens. Query simplifaction is skipped.\n"; break; @@ -734,7 +733,7 @@ void initialize_potency(const MarkVal* marking, if (options.initPotencyTimeout > 0 && pt > 0) { SimplificationContext potencyInitializationContext(marking, net, pt, - options.lpsolveTimeout, + options.lpsolveTimeout, options.lpPrintLevel, &cache, options.initPotencyTimeout); try { uint32_t maxConfigurationsSolved = 10; From 5ed6931f8b8e153f076c192a093d200df31bd8dc Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Thu, 5 Mar 2026 13:55:08 +0100 Subject: [PATCH 08/14] fix nested operators creating incorrect lps --- include/PetriEngine/PQL/Simplifier.h | 6 +- src/PetriEngine/PQL/Simplifier.cpp | 113 +++++++++++++++------------ src/VerifyPN.cpp | 4 + 3 files changed, 71 insertions(+), 52 deletions(-) diff --git a/include/PetriEngine/PQL/Simplifier.h b/include/PetriEngine/PQL/Simplifier.h index d04a4bb52..ba62b9c08 100644 --- a/include/PetriEngine/PQL/Simplifier.h +++ b/include/PetriEngine/PQL/Simplifier.h @@ -41,10 +41,8 @@ namespace PetriEngine { namespace PQL { enum LPQUANT {NONE, GLOBAL, FINAL, NONGLOBAL}; LPQUANT quantifier_found = LPQUANT::NONE; - bool found_global_condition = false; - bool in_global_cond = false; - bool in_and_subexpr = false; - bool in_or_subexpr = false; + int32_t quantifiers = 0; + Retval simplify_or(const LogicalCondition* element); Retval simplify_and(const LogicalCondition *element); diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index d0337c5e2..00a7e8c8a 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -30,7 +30,7 @@ namespace PetriEngine { namespace PQL { } AbstractProgramCollection_ptr mergeLps(std::vector &&lps) { - std::cout << "merging Lps with " << lps.size() << " Elements\n"; + //std::cout << "merging Lps with " << lps.size() << " Elements\n"; if (lps.size() == 0) return nullptr; int j = 0; int i = lps.size() - 1; @@ -47,13 +47,22 @@ namespace PetriEngine { namespace PQL { AbstractProgramCollection_ptr createGlobalUnion(AbstractProgramCollection_ptr &global_lp, std::vector &&nonglobal_lps) { - std::cout << "creating unioncollection of global and nonglobal conditions\n"; + //std::cout << "creating unioncollection of global and nonglobal conditions\n"; - if(global_lp == nullptr) - return std::make_shared(std::move(nonglobal_lps)); + if(global_lp == nullptr){ + //std::cout << "global_lp is NULL\n"; + if(nonglobal_lps.size() == 0){ + //std::cout << "returning null from createGlobalUnion\n"; + return nullptr; + }else{ + return std::make_shared(std::move(nonglobal_lps)); + } + } - if(nonglobal_lps.size() == 0) + if(nonglobal_lps.size() == 0){ + //std::cout << "nonglobal_lps is empty\n"; return global_lp; + } std::vector merges; @@ -66,21 +75,18 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_or(const LogicalCondition *element) { - std::cout << "simplifying or\n"; + //std::cout << "simplifying or\n"; std::vector conditions; std::vector lps; std::vector global_neglpsv; std::vector nonglobal_neglpsv; - //std::vector neggconds; - - bool was_and_subexpr = in_and_subexpr; - - + for (const auto &c: element->getOperands()) { - found_global_condition = false; - in_and_subexpr = false; quantifier_found = LPQUANT::NONE; + int32_t pre_quantifiers = quantifiers; Visitor::visit(this, c); + + //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n"; auto r = std::move(_return_value); assert(r.neglps); @@ -91,29 +97,40 @@ namespace PetriEngine { namespace PQL { } else if (r.formula->isTriviallyFalse()) { continue; } + conditions.push_back(r.formula); - lps.push_back(r.lps); + + if( ( quantifiers - pre_quantifiers ) > 1){ + //std::cout << "exceeded depth\n"; + continue; + } + + lps.emplace_back(r.lps); if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::FINAL){ global_neglpsv.emplace_back(r.neglps); }else{ nonglobal_neglpsv.emplace_back(r.neglps); } + } - //neggconds.emplace_back(!found_global_condition); - - found_global_condition = false; + //std::cout << "sizes or: " << lps.size() << ", " << global_neglpsv.size() << ", " << nonglobal_neglpsv.size() << "\n"; - in_and_subexpr = was_and_subexpr; + if (conditions.size() == 0) { + return Retval(BooleanCondition::FALSE_CONSTANT); } AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv)); neglps = createGlobalUnion(neglps, std::move(nonglobal_neglpsv)); - if (conditions.size() == 0) { - return Retval(BooleanCondition::FALSE_CONSTANT); + if(neglps == nullptr){ + neglps = std::make_shared(); } + if(lps.size() == 0){ + lps.emplace_back(std::make_shared()); + } + try { if (!_context.timeout() && !neglps->satisfiable(_context)) { return Retval(BooleanCondition::TRUE_CONSTANT); @@ -127,7 +144,7 @@ namespace PetriEngine { namespace PQL { // Lets try to see if the r1 AND r2 can ever be false at the same time // If not, then we know that r1 || r2 must be true. // we check this by checking if !r1 && !r2 is unsat - std::cout << "leaving or\n"; + //std::cout << "leaving or\n"; return Retval( makeOr(conditions), std::make_shared(std::move(lps)), @@ -135,24 +152,18 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_and(const LogicalCondition *element) { - std::cout << "simplifying and\n"; + //std::cout << "simplifying and\n"; std::vector conditions; std::vector global_lpsv; std::vector nonglobal_lpsv; - //std::vector lpsv; std::vector neglps; - - - bool was_and_subexpr = in_and_subexpr; - int global_count = 0; - for (auto &c: element->getOperands()) { - in_and_subexpr = true; - found_global_condition = false; quantifier_found = LPQUANT::NONE; + int32_t pre_quantifiers = quantifiers; Visitor::visit(this, c); - global_count += (found_global_condition );//&& in_and_subexpr); + + //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n"; auto r = std::move(_return_value); if (r.formula->isTriviallyFalse()) { @@ -163,22 +174,20 @@ namespace PetriEngine { namespace PQL { conditions.push_back(r.formula); + if( ( quantifiers - pre_quantifiers ) > 1) + continue; + if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::GLOBAL){ global_lpsv.emplace_back(r.lps); }else{ nonglobal_lpsv.emplace_back(r.lps); } - //if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::FINAL) neglps.emplace_back(r.neglps); - //gconds.emplace_back(found_global_condition); - - found_global_condition = false; - - in_and_subexpr = was_and_subexpr; } - //std::cout << "and had [" << global_count << "] global conditions\n"; + //std::cout << "sizes and: " << neglps.size() << ", " << global_lpsv.size() << ", " << nonglobal_lpsv.size() << "\n"; + if (conditions.size() == 0) { return Retval(BooleanCondition::TRUE_CONSTANT); } @@ -186,6 +195,13 @@ namespace PetriEngine { namespace PQL { auto lps = mergeLps(std::move(global_lpsv)); lps = createGlobalUnion(lps, std::move(nonglobal_lpsv)); + if(lps == nullptr){ + lps = std::make_shared(); + } + + if(neglps.size() == 0){ + neglps.emplace_back(std::make_shared()); + } try { if (!_context.timeout() && !lps->satisfiable(_context)) { @@ -287,7 +303,7 @@ namespace PetriEngine { namespace PQL { template Retval Simplifier::simplify_simple_quantifier(Retval &r) { - std::cout << "other quantifier\n"; + //std::cout << "other quantifier\n"; static_assert(std::is_base_of_v); quantifier_found = LPQUANT::NONGLOBAL; //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n"; @@ -415,7 +431,7 @@ namespace PetriEngine { namespace PQL { /******* Simplifier accepts ********/ void Simplifier::_accept(const NotCondition *element) { - std::cout << "negating\n"; + //std::cout << "negating\n"; _context.negate(); Visitor::visit(this, element->getCond()); _context.negate(); @@ -947,6 +963,7 @@ namespace PetriEngine { namespace PQL { void Simplifier::_accept(const UntilCondition *condition) { bool neg = _context.negated(); _context.setNegate(false); + quantifiers++; Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(_return_value); @@ -1011,34 +1028,34 @@ namespace PetriEngine { namespace PQL { } void Simplifier::_accept(const FCondition *condition) { + quantifiers++; Visitor::visit(this, condition->getCond()); if(_context.negated()){ - std::cout << "negated GCondition\n"; - //SET_GLOBAL(true); + //std::cout << "negated GCondition\n"; auto r = simplify_simple_quantifier(_return_value); - found_global_condition = true; - //RESTORE_GLOBAL; RETURN(std::move(r)); }else{ - std::cout << "FCondition\n"; + //std::cout << "FCondition\n"; RETURN(simplify_simple_quantifier(_return_value)); } } void Simplifier::_accept(const GCondition *condition) { + quantifiers++; Visitor::visit(this, condition->getCond()); + if(_context.negated()){ - std::cout << "negated FCondition\n"; + //std::cout << "negated FCondition\n"; RETURN(simplify_simple_quantifier(_return_value)); }else{ - std::cout << "GCondition\n"; + //std::cout << "GCondition\n"; auto r = simplify_simple_quantifier(_return_value); - found_global_condition = true; RETURN(std::move(r)) } } void Simplifier::_accept(const XCondition *condition) { + quantifiers++; Visitor::visit(this, condition->getCond()); RETURN(simplify_simple_quantifier(_return_value)) } diff --git a/src/VerifyPN.cpp b/src/VerifyPN.cpp index a58f0640b..5b9d46727 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -443,6 +443,10 @@ Condition_ptr simplify_ltl_query(Condition_ptr query, out << std::endl; } + std::cout << "PushNegated: "; + cond->toString(std::cout); + std::cout << "\n"; + try { auto simp_cond = PetriEngine::PQL::simplify(cond, simplificationContext); cond = pushNegation(simp_cond.formula, stats, evalContext, names.size() > 1, false, true); From 07ab9f036d4c86c98f9e14dd1c09177e07d39089 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Sun, 8 Mar 2026 16:14:21 +0100 Subject: [PATCH 09/14] fix unqunatified conditions --- src/PetriEngine/PQL/Simplifier.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 00a7e8c8a..92fc9779b 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -107,7 +107,7 @@ namespace PetriEngine { namespace PQL { lps.emplace_back(r.lps); - if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::FINAL){ + if(/*quantifier_found == LPQUANT::NONE ||*/ quantifier_found == LPQUANT::FINAL){ global_neglpsv.emplace_back(r.neglps); }else{ nonglobal_neglpsv.emplace_back(r.neglps); @@ -177,7 +177,7 @@ namespace PetriEngine { namespace PQL { if( ( quantifiers - pre_quantifiers ) > 1) continue; - if(quantifier_found == LPQUANT::NONE || quantifier_found == LPQUANT::GLOBAL){ + if(/*quantifier_found == LPQUANT::NONE ||*/ quantifier_found == LPQUANT::GLOBAL){ global_lpsv.emplace_back(r.lps); }else{ nonglobal_lpsv.emplace_back(r.lps); From 99308c0ed7fdfba15bdf60abd1b72154691a8dd8 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Sun, 8 Mar 2026 22:40:21 +0100 Subject: [PATCH 10/14] improve unquantified condition handling --- src/PetriEngine/PQL/Simplifier.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 92fc9779b..67c83a71a 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -78,6 +78,7 @@ namespace PetriEngine { namespace PQL { //std::cout << "simplifying or\n"; std::vector conditions; std::vector lps; + std::vector unquantified_neglpsv; std::vector global_neglpsv; std::vector nonglobal_neglpsv; @@ -107,7 +108,9 @@ namespace PetriEngine { namespace PQL { lps.emplace_back(r.lps); - if(/*quantifier_found == LPQUANT::NONE ||*/ quantifier_found == LPQUANT::FINAL){ + if(quantifier_found == LPQUANT::NONE){ + unquantified_neglpsv.emplace_back(r.neglps); + }else if(quantifier_found == LPQUANT::FINAL){ global_neglpsv.emplace_back(r.neglps); }else{ nonglobal_neglpsv.emplace_back(r.neglps); @@ -120,6 +123,11 @@ namespace PetriEngine { namespace PQL { return Retval(BooleanCondition::FALSE_CONSTANT); } + if(unquantified_neglpsv.size() > 0){ + auto uq_neglps = mergeLps(std::move(unquantified_neglpsv)); + nonglobal_neglpsv.emplace_back(uq_neglps); + } + AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv)); neglps = createGlobalUnion(neglps, std::move(nonglobal_neglpsv)); @@ -155,6 +163,7 @@ namespace PetriEngine { namespace PQL { //std::cout << "simplifying and\n"; std::vector conditions; std::vector global_lpsv; + std::vector unquantified_lpsv; std::vector nonglobal_lpsv; std::vector neglps; @@ -177,7 +186,9 @@ namespace PetriEngine { namespace PQL { if( ( quantifiers - pre_quantifiers ) > 1) continue; - if(/*quantifier_found == LPQUANT::NONE ||*/ quantifier_found == LPQUANT::GLOBAL){ + if(quantifier_found == LPQUANT::NONE){ + unquantified_lpsv.emplace_back(r.lps); + }else if (quantifier_found == LPQUANT::GLOBAL){ global_lpsv.emplace_back(r.lps); }else{ nonglobal_lpsv.emplace_back(r.lps); @@ -192,6 +203,11 @@ namespace PetriEngine { namespace PQL { return Retval(BooleanCondition::TRUE_CONSTANT); } + if(unquantified_lpsv.size() > 0){ + auto uq_lps = mergeLps(std::move(unquantified_lpsv)); + nonglobal_lpsv.emplace_back(uq_lps); + } + auto lps = mergeLps(std::move(global_lpsv)); lps = createGlobalUnion(lps, std::move(nonglobal_lpsv)); From c7102bd301ddafcbdd228c88f4e61ca609a84425 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Mon, 16 Mar 2026 16:45:09 +0100 Subject: [PATCH 11/14] less conservative operator handling --- include/PetriEngine/PQL/Simplifier.h | 4 +- src/PetriEngine/PQL/Simplifier.cpp | 65 +++++++++++++++++++++------- 2 files changed, 53 insertions(+), 16 deletions(-) diff --git a/include/PetriEngine/PQL/Simplifier.h b/include/PetriEngine/PQL/Simplifier.h index ba62b9c08..9ca81c469 100644 --- a/include/PetriEngine/PQL/Simplifier.h +++ b/include/PetriEngine/PQL/Simplifier.h @@ -39,8 +39,10 @@ namespace PetriEngine { namespace PQL { SimplificationContext& _context; Retval _return_value; - enum LPQUANT {NONE, GLOBAL, FINAL, NONGLOBAL}; + enum LPQUANT {NONE, GLOBAL, FINAL, OTHER, UNTIL}; LPQUANT quantifier_found = LPQUANT::NONE; + LPQUANT quantifier_parent = LPQUANT::NONE; + bool qparent_neg_context = false; int32_t quantifiers = 0; diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 67c83a71a..8286bb43b 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -81,7 +81,11 @@ namespace PetriEngine { namespace PQL { std::vector unquantified_neglpsv; std::vector global_neglpsv; std::vector nonglobal_neglpsv; - + + const bool same_context = qparent_neg_context == _context.negated(); + const bool parent_final = quantifier_parent == LPQUANT::FINAL; + const bool parent_global = quantifier_parent == LPQUANT::GLOBAL; + const bool neg_is_invariant = (same_context && parent_final) || (!same_context && parent_global); for (const auto &c: element->getOperands()) { quantifier_found = LPQUANT::NONE; int32_t pre_quantifiers = quantifiers; @@ -101,15 +105,17 @@ namespace PetriEngine { namespace PQL { conditions.push_back(r.formula); - if( ( quantifiers - pre_quantifiers ) > 1){ - //std::cout << "exceeded depth\n"; - continue; - } lps.emplace_back(r.lps); - if(quantifier_found == LPQUANT::NONE){ - unquantified_neglpsv.emplace_back(r.neglps); + if( ( quantifiers - pre_quantifiers ) > 1){ + nonglobal_neglpsv.emplace_back(r.neglps); + }else if(quantifier_found == LPQUANT::NONE){ + if(neg_is_invariant){ + global_neglpsv.emplace_back(r.neglps); + }else{ + unquantified_neglpsv.emplace_back(r.neglps); + } }else if(quantifier_found == LPQUANT::FINAL){ global_neglpsv.emplace_back(r.neglps); }else{ @@ -128,6 +134,10 @@ namespace PetriEngine { namespace PQL { nonglobal_neglpsv.emplace_back(uq_neglps); } + if(global_neglpsv.size() > 0 && nonglobal_neglpsv.size() > 0){ + std::cout << "# MERGE RULE APPLIED\n"; + } + AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv)); neglps = createGlobalUnion(neglps, std::move(nonglobal_neglpsv)); @@ -166,7 +176,11 @@ namespace PetriEngine { namespace PQL { std::vector unquantified_lpsv; std::vector nonglobal_lpsv; std::vector neglps; - + + const bool same_context = qparent_neg_context == _context.negated(); + const bool parent_final = quantifier_parent == LPQUANT::FINAL; + const bool parent_global = quantifier_parent == LPQUANT::GLOBAL; + const bool is_invariant = (same_context && parent_global) || (!same_context && parent_final); for (auto &c: element->getOperands()) { quantifier_found = LPQUANT::NONE; int32_t pre_quantifiers = quantifiers; @@ -183,11 +197,14 @@ namespace PetriEngine { namespace PQL { conditions.push_back(r.formula); - if( ( quantifiers - pre_quantifiers ) > 1) - continue; - - if(quantifier_found == LPQUANT::NONE){ - unquantified_lpsv.emplace_back(r.lps); + if( ( quantifiers - pre_quantifiers ) > 1){ + nonglobal_lpsv.emplace_back(r.lps); + }else if(quantifier_found == LPQUANT::NONE){ + if(is_invariant){ + global_lpsv.emplace_back(r.lps); + }else{ + unquantified_lpsv.emplace_back(r.lps); + } }else if (quantifier_found == LPQUANT::GLOBAL){ global_lpsv.emplace_back(r.lps); }else{ @@ -208,6 +225,9 @@ namespace PetriEngine { namespace PQL { nonglobal_lpsv.emplace_back(uq_lps); } + if(global_lpsv.size() > 0 && nonglobal_lpsv.size() > 0){ + std::cout << "# MERGE RULE APPLIED\n"; + } auto lps = mergeLps(std::move(global_lpsv)); lps = createGlobalUnion(lps, std::move(nonglobal_lpsv)); @@ -321,7 +341,7 @@ namespace PetriEngine { namespace PQL { Retval Simplifier::simplify_simple_quantifier(Retval &r) { //std::cout << "other quantifier\n"; static_assert(std::is_base_of_v); - quantifier_found = LPQUANT::NONGLOBAL; + quantifier_found = LPQUANT::OTHER; //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n"; //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n"; if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { @@ -329,7 +349,7 @@ namespace PetriEngine { namespace PQL { } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { - return Retval(std::make_shared(r.formula));//, r.lps, r.neglps); + return Retval(std::make_shared(r.formula), r.lps, r.neglps); } } @@ -980,6 +1000,7 @@ namespace PetriEngine { namespace PQL { bool neg = _context.negated(); _context.setNegate(false); quantifiers++; + quantifier_parent = LPQUANT::OTHER; Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(_return_value); @@ -994,6 +1015,7 @@ namespace PetriEngine { namespace PQL { Retval(BooleanCondition::TRUE_CONSTANT) : Retval(BooleanCondition::FALSE_CONSTANT)) } + quantifier_parent = LPQUANT::OTHER; Visitor::visit(this, condition->getCond1()); Retval r1 = std::move(_return_value); @@ -1045,6 +1067,12 @@ namespace PetriEngine { namespace PQL { void Simplifier::_accept(const FCondition *condition) { quantifiers++; + if(_context.negated()){ + quantifier_parent = LPQUANT::GLOBAL; + }else{ + quantifier_parent = LPQUANT::FINAL; + } + qparent_neg_context = _context.negated(); Visitor::visit(this, condition->getCond()); if(_context.negated()){ //std::cout << "negated GCondition\n"; @@ -1058,6 +1086,12 @@ namespace PetriEngine { namespace PQL { void Simplifier::_accept(const GCondition *condition) { quantifiers++; + if(_context.negated()){ + quantifier_parent = LPQUANT::FINAL; + }else{ + quantifier_parent = LPQUANT::GLOBAL; + } + qparent_neg_context = _context.negated(); Visitor::visit(this, condition->getCond()); if(_context.negated()){ @@ -1072,6 +1106,7 @@ namespace PetriEngine { namespace PQL { void Simplifier::_accept(const XCondition *condition) { quantifiers++; + quantifier_parent = LPQUANT::OTHER; Visitor::visit(this, condition->getCond()); RETURN(simplify_simple_quantifier(_return_value)) } From 72974d9b5d04ea6aafa01325c310753a5b65e9ad Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Thu, 19 Mar 2026 16:44:09 +0100 Subject: [PATCH 12/14] small changes --- src/PetriEngine/PQL/Simplifier.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 8286bb43b..a2cf03113 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -86,10 +86,16 @@ namespace PetriEngine { namespace PQL { const bool parent_final = quantifier_parent == LPQUANT::FINAL; const bool parent_global = quantifier_parent == LPQUANT::GLOBAL; const bool neg_is_invariant = (same_context && parent_final) || (!same_context && parent_global); + + const auto local_parent = quantifier_parent; + for (const auto &c: element->getOperands()) { quantifier_found = LPQUANT::NONE; int32_t pre_quantifiers = quantifiers; + if(!neg_is_invariant) + quantifier_parent = LPQUANT::OTHER; Visitor::visit(this, c); + quantifier_parent = local_parent; //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n"; @@ -135,6 +141,7 @@ namespace PetriEngine { namespace PQL { } if(global_neglpsv.size() > 0 && nonglobal_neglpsv.size() > 0){ + std::cout << "# OR\n"; std::cout << "# MERGE RULE APPLIED\n"; } @@ -181,10 +188,16 @@ namespace PetriEngine { namespace PQL { const bool parent_final = quantifier_parent == LPQUANT::FINAL; const bool parent_global = quantifier_parent == LPQUANT::GLOBAL; const bool is_invariant = (same_context && parent_global) || (!same_context && parent_final); + + const auto local_parent = quantifier_parent; + for (auto &c: element->getOperands()) { quantifier_found = LPQUANT::NONE; int32_t pre_quantifiers = quantifiers; + if(!is_invariant) + quantifier_parent = LPQUANT::OTHER; Visitor::visit(this, c); + quantifier_parent = local_parent; //std::cout << "sub expression quant depth: " << quantifiers - pre_quantifiers << "\n"; From 9da2d6f5c43e22497bb9614eceb8964771074fb0 Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Thu, 19 Mar 2026 18:33:49 +0100 Subject: [PATCH 13/14] timestamp added --- include/PetriEngine/PQL/Contexts.h | 6 ++++++ src/PetriEngine/PQL/Simplifier.cpp | 7 ++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index 929557f94..fa29e27fe 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -36,6 +36,8 @@ #include #include +#include + namespace PetriEngine { namespace PQL { @@ -195,8 +197,12 @@ namespace PetriEngine { _markingOutOfBounds = true; } } + + _id = std::chrono::system_clock::now(); } + std::chrono::time_point _id; + virtual ~SimplificationContext() { if(_base_lp != nullptr) glp_delete_prob(_base_lp); diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index a2cf03113..218161f9d 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -141,8 +141,8 @@ namespace PetriEngine { namespace PQL { } if(global_neglpsv.size() > 0 && nonglobal_neglpsv.size() > 0){ - std::cout << "# OR\n"; - std::cout << "# MERGE RULE APPLIED\n"; + auto id = std::chrono::duration_cast(_context._id.time_since_epoch()).count(); + std::cout << "# MERGE RULE APPLIED " << id << "\n"; } AbstractProgramCollection_ptr neglps = mergeLps(std::move(global_neglpsv)); @@ -239,7 +239,8 @@ namespace PetriEngine { namespace PQL { } if(global_lpsv.size() > 0 && nonglobal_lpsv.size() > 0){ - std::cout << "# MERGE RULE APPLIED\n"; + auto id = std::chrono::duration_cast(_context._id.time_since_epoch()).count(); + std::cout << "# MERGE RULE APPLIED " << id << "\n"; } auto lps = mergeLps(std::move(global_lpsv)); lps = createGlobalUnion(lps, std::move(nonglobal_lpsv)); From 880c09daba47ca6d9a7084b12895bffe32706b2d Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Sun, 17 May 2026 12:52:19 +0200 Subject: [PATCH 14/14] basic lp construction changes --- include/PetriEngine/PQL/Contexts.h | 2 + include/PetriEngine/PQL/Simplifier.h | 1 + .../Simplification/LinearProgram.h | 4 + .../Simplification/LinearPrograms.h | 12 + src/PetriEngine/PQL/Contexts.cpp | 121 +++++++- src/PetriEngine/PQL/Simplifier.cpp | 126 ++++++-- .../Simplification/LinearProgram.cpp | 287 +++++++++++++++++- .../Simplification/LinearPrograms.cpp | 113 +++++++ 8 files changed, 641 insertions(+), 25 deletions(-) diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index fa29e27fe..b2a612e74 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -259,6 +259,8 @@ namespace PetriEngine { glp_prob* makeBaseLP() const; + glp_prob* buildBaseFromMarking(std::vector, double>>& setMarking) const; + private: bool _negated; const MarkVal* _marking; diff --git a/include/PetriEngine/PQL/Simplifier.h b/include/PetriEngine/PQL/Simplifier.h index 9ca81c469..3825e5afb 100644 --- a/include/PetriEngine/PQL/Simplifier.h +++ b/include/PetriEngine/PQL/Simplifier.h @@ -45,6 +45,7 @@ namespace PetriEngine { namespace PQL { bool qparent_neg_context = false; int32_t quantifiers = 0; + bool solveFinalCond(std::vector& final_lps); Retval simplify_or(const LogicalCondition* element); Retval simplify_and(const LogicalCondition *element); diff --git a/include/PetriEngine/Simplification/LinearProgram.h b/include/PetriEngine/Simplification/LinearProgram.h index 310465c6d..da56ddab2 100644 --- a/include/PetriEngine/Simplification/LinearProgram.h +++ b/include/PetriEngine/Simplification/LinearProgram.h @@ -11,6 +11,7 @@ #include #include + namespace PetriEngine { namespace Simplification { @@ -62,7 +63,10 @@ namespace PetriEngine { bool knownImpossible() const { return _result == result_t::IMPOSSIBLE; } bool knownPossible() const { return _result == result_t::POSSIBLE; } + + double upperBoundForPlace(const PQL::SimplificationContext& context, std::vector& place, uint32_t solvetime); bool isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime); + bool isBoundedImpossible(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime); void solvePotency(const PQL::SimplificationContext& context, std::vector& potencies); void make_union(const LinearProgram& other); diff --git a/include/PetriEngine/Simplification/LinearPrograms.h b/include/PetriEngine/Simplification/LinearPrograms.h index c96ce1c78..ac35290cd 100644 --- a/include/PetriEngine/Simplification/LinearPrograms.h +++ b/include/PetriEngine/Simplification/LinearPrograms.h @@ -15,6 +15,8 @@ namespace PetriEngine { result_t _result = result_t::UNKNOWN; bool has_empty = false; + virtual double upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) = 0; + virtual void boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) = 0; virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) = 0; virtual uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, @@ -25,6 +27,9 @@ namespace PetriEngine { bool empty() { return has_empty; } virtual bool satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()); + virtual bool boundedSatisfiable(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime = std::numeric_limits::max()); + virtual double upperBound(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime = std::numeric_limits::max()); + bool known_sat() { return _result == POSSIBLE; } bool known_unsat() { return _result == IMPOSSIBLE; } @@ -51,6 +56,8 @@ namespace PetriEngine { size_t _size = 0; void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + void boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) override; + double upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; @@ -80,6 +87,8 @@ namespace PetriEngine { size_t _size = 0; void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + void boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) override; + double upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; @@ -99,6 +108,8 @@ namespace PetriEngine { protected: void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + void boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) override; + double upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; @@ -113,6 +124,7 @@ namespace PetriEngine { void reset() override {} size_t size() const override { return 1; } bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) override; + bool isBoundedImpossible(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime); }; } } diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index 6090c8047..3c13aa14c 100644 --- a/src/PetriEngine/PQL/Contexts.cpp +++ b/src/PetriEngine/PQL/Contexts.cpp @@ -101,8 +101,8 @@ namespace PetriEngine { if (lp == nullptr) return lp; - const uint32_t nCol = _net->numberOfTransitions(); - const int nRow = _net->numberOfPlaces(); + const uint32_t nCol = _net->numberOfTransitions() + _net->numberOfPlaces(); + const uint32_t nRow = _net->numberOfPlaces(); std::vector indir(std::max(nCol, nRow) + 1); glp_add_cols(lp, nCol + 1); @@ -158,6 +158,123 @@ namespace PetriEngine { return nullptr; } } + + for(size_t p = 0; p < _net->numberOfPlaces(); p++){ + const int colno = 1 + p + _net->numberOfTransitions(); + glp_set_col_bnds(lp, colno, GLP_FX, (double) _marking[p], 0); + glp_set_obj_coef(lp, colno, 0); + glp_set_col_kind(lp, colno, GLP_IV); + } + /*std::vector ind(2); + std::vector col = {0, 1.0}; + + for(size_t p = 0; p < _net->numberOfPlaces(); p++){ + ind[1] = 1 + p + _net->numberOfTransitions(); + glp_set_mat_row(lp, rowno, 1, ind.data(), col.data()); + glp_set_row_bnds(lp, rowno, GLP_FX, (double) _marking[p], 0); + ++rowno; + }*/ + + return lp; + } + + glp_prob* SimplificationContext::buildBaseFromMarking(std::vector, double>>& setMarking) const + { + constexpr auto infty = std::numeric_limits::infinity(); + if (timeout()) + return nullptr; + + auto* lp = glp_create_prob(); + if (lp == nullptr) + return lp; + + const uint32_t nCol = _net->numberOfTransitions(); + const int nRow = setMarking.size(); + std::vector indir(std::max(nCol, nRow) + 1); + + glp_add_cols(lp, nCol + 1); + glp_add_rows(lp, nRow + 1); + { + std::vector col = std::vector(nRow + 1); + for (size_t t = 0; t < _net->numberOfTransitions(); ++t) { + auto pre = _net->preset(t); + auto post = _net->postset(t); + size_t l = 1; + while (pre.first != pre.second || + post.first != post.second) { + if (pre.first == pre.second || (post.first != post.second && post.first->place < pre.first->place)) { + col[l] = post.first->tokens; + indir[l] = post.first->place + 1; + ++post.first; + } + else if (post.first == post.second || (pre.first != pre.second && pre.first->place < post.first->place)) { + if (!pre.first->inhibitor) + col[l] = -(double) pre.first->tokens; + else + col[l] = 0; + indir[l] = pre.first->place + 1; + ++pre.first; + } + else { + assert(pre.first->place == post.first->place); + if (!pre.first->inhibitor) + col[l] = (double) post.first->tokens - (double) pre.first->tokens; + else + col[l] = (double) post.first->tokens; + indir[l] = pre.first->place + 1; + ++pre.first; + ++post.first; + } + ++l; + } + glp_set_mat_col(lp, t + 1, l - 1, indir.data(), col.data()); + if (timeout()) { + std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return nullptr; + } + } + } + int rowno = 1; + for (size_t p = 0; p < _net->numberOfPlaces(); p++) { + if(setMarking[p].second >= 0){ + glp_set_row_bnds(lp, rowno, GLP_LO, (0.0 - (double) setMarking[p].second), infty); + }else{ + glp_set_row_bnds(lp, rowno, GLP_FR, -infty, infty); + } + ++rowno; + if (timeout()) { + std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return nullptr; + } + } + + std::vector col = std::vector(nCol + 1); + for(size_t s = _net->numberOfPlaces(); s < setMarking.size(); s++){ + if(setMarking[s].second < 0){ + ++rowno; + continue; + } + size_t l = 1; + for (size_t t = 0; t < _net->numberOfTransitions(); ++t) { + double coef = 0; + for(auto p: setMarking[s].first){ + coef += _net->inArc(t, p); + coef -= _net->outArc(p, t); + } + + if(coef != 0){ + indir[l] = t + 1; + col[l] = coef; + l++; + } + } + glp_set_mat_row(lp, s + 1, l - 1, indir.data(), col.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, (0.0 - (double) setMarking[s].second), infty); + ++rowno; + } + return lp; } } diff --git a/src/PetriEngine/PQL/Simplifier.cpp b/src/PetriEngine/PQL/Simplifier.cpp index 218161f9d..26726f1bf 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -46,6 +46,47 @@ namespace PetriEngine { namespace PQL { } + bool Simplifier::solveFinalCond(std::vector& final_lps){ + return true; + for(int i = 0; i < final_lps.size(); i++){ + if(!final_lps[i]->satisfiable(_context)) + return false; + } + + uint32_t nPlaces = _context.net()->numberOfPlaces(); + std::vector, double>> bounds(nPlaces); + std::vector> m(final_lps.size(), std::vector(final_lps.size())); + + for(int i = 0; i < final_lps.size(); i++){ + for(int j = 0; j < final_lps.size(); j++){ + if(i == j) + continue; + for(uint32_t p = 0; p < nPlaces; p++){ + std::vector ps = {p}; + double bound_p = (double) _context.marking()[p] + final_lps[i]->upperBound(_context, ps); + std::cout << p << ": " << bound_p << "\n"; + bounds[p] = std::make_pair(std::move(ps), bound_p); + } + + if(!final_lps[j]->boundedSatisfiable(_context, bounds)){ + //std::cout << "# CANDIDATE IMPOSSIBLE\n"; + if(m[j][i]){ + std::cout << "# CANDIDATE IMPOSSIBLE\n"; + return false; + } + + m[i][j] = true; + m[j][i] = true; + } + } + } + + std::cout << "# CANDIDATE POSSIBLE\n"; + + return true; + } + + AbstractProgramCollection_ptr createGlobalUnion(AbstractProgramCollection_ptr &global_lp, std::vector &&nonglobal_lps) { //std::cout << "creating unioncollection of global and nonglobal conditions\n"; @@ -80,6 +121,7 @@ namespace PetriEngine { namespace PQL { std::vector lps; std::vector unquantified_neglpsv; std::vector global_neglpsv; + std::vector final_neglpsv; std::vector nonglobal_neglpsv; const bool same_context = qparent_neg_context == _context.negated(); @@ -116,17 +158,25 @@ namespace PetriEngine { namespace PQL { if( ( quantifiers - pre_quantifiers ) > 1){ nonglobal_neglpsv.emplace_back(r.neglps); - }else if(quantifier_found == LPQUANT::NONE){ - if(neg_is_invariant){ - global_neglpsv.emplace_back(r.neglps); - }else{ - unquantified_neglpsv.emplace_back(r.neglps); + }else { + switch(quantifier_found){ + case LPQUANT::NONE: + if(neg_is_invariant){ + global_neglpsv.emplace_back(r.neglps); + }else{ + unquantified_neglpsv.emplace_back(r.neglps); + } + break; + case LPQUANT::FINAL: + global_neglpsv.emplace_back(r.neglps); + break; + case LPQUANT::GLOBAL: + final_neglpsv.emplace_back(r.neglps); + break; + default: + nonglobal_neglpsv.emplace_back(r.neglps); } - }else if(quantifier_found == LPQUANT::FINAL){ - global_neglpsv.emplace_back(r.neglps); - }else{ - nonglobal_neglpsv.emplace_back(r.neglps); - } + } } //std::cout << "sizes or: " << lps.size() << ", " << global_neglpsv.size() << ", " << nonglobal_neglpsv.size() << "\n"; @@ -140,6 +190,12 @@ namespace PetriEngine { namespace PQL { nonglobal_neglpsv.emplace_back(uq_neglps); } + if(final_neglpsv.size() > 1){ + if(!solveFinalCond(final_neglpsv)){ + return Retval(BooleanCondition::TRUE_CONSTANT); + } + } + if(global_neglpsv.size() > 0 && nonglobal_neglpsv.size() > 0){ auto id = std::chrono::duration_cast(_context._id.time_since_epoch()).count(); std::cout << "# MERGE RULE APPLIED " << id << "\n"; @@ -180,6 +236,7 @@ namespace PetriEngine { namespace PQL { //std::cout << "simplifying and\n"; std::vector conditions; std::vector global_lpsv; + std::vector final_lpsv; std::vector unquantified_lpsv; std::vector nonglobal_lpsv; std::vector neglps; @@ -212,17 +269,25 @@ namespace PetriEngine { namespace PQL { if( ( quantifiers - pre_quantifiers ) > 1){ nonglobal_lpsv.emplace_back(r.lps); - }else if(quantifier_found == LPQUANT::NONE){ - if(is_invariant){ - global_lpsv.emplace_back(r.lps); - }else{ - unquantified_lpsv.emplace_back(r.lps); + }else { + switch(quantifier_found){ + case LPQUANT::NONE: + if(is_invariant){ + global_lpsv.emplace_back(r.lps); + }else{ + unquantified_lpsv.emplace_back(r.lps); + } + break; + case LPQUANT::GLOBAL: + global_lpsv.emplace_back(r.lps); + break; + case LPQUANT::FINAL: + final_lpsv.emplace_back(r.lps); + break; + default: + nonglobal_lpsv.emplace_back(r.lps); } - }else if (quantifier_found == LPQUANT::GLOBAL){ - global_lpsv.emplace_back(r.lps); - }else{ - nonglobal_lpsv.emplace_back(r.lps); - } + } neglps.emplace_back(r.neglps); } @@ -233,11 +298,17 @@ namespace PetriEngine { namespace PQL { return Retval(BooleanCondition::TRUE_CONSTANT); } - if(unquantified_lpsv.size() > 0){ + if(unquantified_lpsv.size() > 0){ auto uq_lps = mergeLps(std::move(unquantified_lpsv)); nonglobal_lpsv.emplace_back(uq_lps); } + if(final_lpsv.size() > 1){ + if(!solveFinalCond(final_lpsv)){ + return Retval(BooleanCondition::FALSE_CONSTANT); + } + } + if(global_lpsv.size() > 0 && nonglobal_lpsv.size() > 0){ auto id = std::chrono::duration_cast(_context._id.time_since_epoch()).count(); std::cout << "# MERGE RULE APPLIED " << id << "\n"; @@ -391,7 +462,7 @@ namespace PetriEngine { namespace PQL { } } - Member memberForPlace(size_t p, const SimplificationContext &context) { + /*Member memberForPlace(size_t p, const SimplificationContext &context) { std::vector row(context.net()->numberOfTransitions(), 0); row.shrink_to_fit(); for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) { @@ -399,6 +470,17 @@ namespace PetriEngine { namespace PQL { row[t] -= context.net()->inArc(p, t); } return Member(std::move(row), context.marking()[p]); + }*/ + + Member memberForPlace(size_t p, const SimplificationContext &context) { + std::vector row(context.net()->numberOfTransitions() + context.net()->numberOfPlaces(), 0); + row.shrink_to_fit(); + for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) { + row[t] = context.net()->outArc(t, p); + row[t] -= context.net()->inArc(p, t); + } + row[context.net()->numberOfTransitions() + p] = 1.0; + return Member(std::move(row), 0); } /********** Constraint Visitor **********/ diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 9f822df6f..054365aa4 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -128,7 +128,7 @@ namespace PetriEngine { return false; } - const uint32_t nCol = net->numberOfTransitions(); + const uint32_t nCol = net->numberOfTransitions() + net->numberOfPlaces(); const uint32_t nRow = net->numberOfPlaces() + _equations.size(); std::vector row = std::vector(nCol + 1); @@ -175,6 +175,143 @@ namespace PetriEngine { } } + // Set objective, kind and bounds + for (size_t i = 1; i <= net->numberOfTransitions(); i++) { + glp_set_obj_coef(lp, i, 1); + glp_set_col_kind(lp, i, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, i, GLP_LO, 0, infty); + } + + /*for (size_t i = 1 + net->numberOfTransitions(); i <= nCol; i++) { + glp_set_obj_coef(lp, i, 0); + glp_set_col_kind(lp, i, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, i, GLP_FR, 0, 0); + }*/ + + printConstraints(context, lp); + + // Minimize the objective + glp_set_obj_dir(lp, GLP_MIN); + auto stime = glp_time(); + glp_smcp settings; + glp_init_smcp(&settings); + auto timeout = std::min(solvetime, context.getLpTimeout()) * 1000; + settings.tm_lim = timeout; + settings.presolve = GLP_OFF; + settings.msg_lev = 0; + auto result = glp_simplex(lp, &settings); + if (result == GLP_ETMLIM) + { + _result = result_t::UKNOWN; + // std::cerr << "glpk: timeout" << std::endl; + } + else if (result == 0) + { + auto status = glp_get_status(lp); + if (status == GLP_OPT) + { + glp_iocp iset; + glp_init_iocp(&iset); + iset.msg_lev = 0; + iset.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); + iset.presolve = GLP_OFF; + auto ires = glp_intopt(lp, &iset); + if (ires == GLP_ETMLIM) + { + _result = result_t::UKNOWN; + // std::cerr << "glpk mip: timeout" << std::endl; + } + else if (ires == 0) + { + auto ist = glp_mip_status(lp); + if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { + _result = result_t::POSSIBLE; + } + else + { + _result = result_t::IMPOSSIBLE; + } + } + } + else if (status == GLP_FEAS || status == GLP_UNBND) + { + _result = result_t::POSSIBLE; + } + else + { + _result = result_t::IMPOSSIBLE; + } + } + else if (result == GLP_ENOPFS || result == GLP_ENODFS || result == GLP_ENOFEAS) + { + _result = result_t::IMPOSSIBLE; + } + glp_delete_prob(lp); + + return _result == result_t::IMPOSSIBLE; + } + + bool LinearProgram::isBoundedImpossible(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) { + bool use_ilp = true; + auto net = context.net(); + + _result = result_t::UKNOWN; + + if (_equations.size() == 0 || context.timeout()){ + return false; + } + + if (context.markingOutOfBounds()) { // the initial marking has too many tokens that exceed the int32_t limits + return false; + } + + const uint32_t nCol = net->numberOfTransitions(); + const uint32_t nRow = bounds.size() + _equations.size(); + + std::vector row = std::vector(nCol + 1); + std::vector indir(std::max(nCol, nRow) + 1); + for (size_t i = 0; i <= nCol; ++i) + indir[i] = i; + + auto lp = context.buildBaseFromMarking(bounds); + if (lp == nullptr) + return false; + + int rowno = 1 + bounds.size(); + glp_add_rows(lp, _equations.size()); + for (const auto& eq : _equations) { + auto l = eq.row->write_indir(row, indir); + assert(!(std::isinf(eq.upper) && std::isinf(eq.lower))); + glp_set_mat_row(lp, rowno, l-1, indir.data(), row.data()); + if (!std::isinf(eq.lower) && !std::isinf(eq.upper)) + { + if (eq.lower == eq.upper) + glp_set_row_bnds(lp, rowno, GLP_FX, eq.lower, eq.upper); + else + { + if (eq.lower > eq.upper) + { + _result = result_t::IMPOSSIBLE; + glp_delete_prob(lp); + return true; + } + glp_set_row_bnds(lp, rowno, GLP_DB, eq.lower, eq.upper); + } + } + else if (std::isinf(eq.lower)) + glp_set_row_bnds(lp, rowno, GLP_UP, -infty, eq.upper); + else + glp_set_row_bnds(lp, rowno, GLP_LO, eq.lower, -infty); + ++rowno; + + if (context.timeout()) + { + // std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return false; + } + } + // Set objective, kind and bounds for (size_t i = 1; i <= nCol; i++) { glp_set_obj_coef(lp, i, 1); @@ -245,6 +382,154 @@ namespace PetriEngine { return _result == result_t::IMPOSSIBLE; } + double LinearProgram::upperBoundForPlace(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) { + bool use_ilp = true; + auto net = context.net(); + + if (_equations.size() == 0 || context.timeout()){ + if(_equations.size() == 0) + std::cout << "empty bound\n"; + return -1; + } + + if (context.markingOutOfBounds()) { // the initial marking has too many tokens that exceed the int32_t limits + return -1; + } + + const uint32_t nCol = net->numberOfTransitions(); + const uint32_t nRow = net->numberOfPlaces() + _equations.size(); + + std::vector row = std::vector(nCol + 1); + std::vector indir(std::max(nCol, nRow) + 1); + for (size_t i = 0; i <= nCol; ++i) + indir[i] = i; + + auto lp = context.makeBaseLP(); + if (lp == nullptr) + return false; + + int rowno = 1 + net->numberOfPlaces(); + glp_add_rows(lp, _equations.size()); + for (const auto& eq : _equations) { + auto l = eq.row->write_indir(row, indir); + assert(!(std::isinf(eq.upper) && std::isinf(eq.lower))); + glp_set_mat_row(lp, rowno, l-1, indir.data(), row.data()); + if (!std::isinf(eq.lower) && !std::isinf(eq.upper)) + { + if (eq.lower == eq.upper) + glp_set_row_bnds(lp, rowno, GLP_FX, eq.lower, eq.upper); + else + { + if (eq.lower > eq.upper) + { + _result = result_t::IMPOSSIBLE; + glp_delete_prob(lp); + return -1; + } + glp_set_row_bnds(lp, rowno, GLP_DB, eq.lower, eq.upper); + } + } + else if (std::isinf(eq.lower)) + glp_set_row_bnds(lp, rowno, GLP_UP, -infty, eq.upper); + else + glp_set_row_bnds(lp, rowno, GLP_LO, eq.lower, -infty); + ++rowno; + + if (context.timeout()) + { + // std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return -1; + } + } + + // Set objective, kind and bounds + for (size_t i = 1; i <= nCol; i++) { + double place_delta = 0; + for(auto place : place_set){ + place_delta += (double) context.net()->outArc(i - 1, place); + place_delta -= (double) context.net()->inArc(place, i - 1); + } + + glp_set_obj_coef(lp, i, place_delta); + glp_set_col_kind(lp, i, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, i, GLP_LO, 0, infty); + } + + + printConstraints(context, lp); + + // Minimize the objective + glp_set_obj_dir(lp, GLP_MAX); + auto stime = glp_time(); + glp_smcp settings; + glp_init_smcp(&settings); + auto timeout = std::min(solvetime, context.getLpTimeout()) * 1000; + settings.tm_lim = timeout; + settings.presolve = GLP_OFF; + settings.msg_lev = 0; + auto result = glp_simplex(lp, &settings); + if (result == GLP_ETMLIM) + { + _result = result_t::UKNOWN; + // std::cerr << "glpk: timeout" << std::endl; + } + else if (result == 0) + { + auto status = glp_get_status(lp); + if (status == GLP_OPT) + { + glp_iocp iset; + glp_init_iocp(&iset); + iset.msg_lev = 0; + iset.tm_lim = std::min(std::max(timeout - (stime - glp_time()), 1), 1000); + iset.presolve = GLP_OFF; + auto ires = glp_intopt(lp, &iset); + if (ires == GLP_ETMLIM) + { + _result = result_t::UKNOWN; + // std::cerr << "glpk mip: timeout" << std::endl; + } + else if (ires == 0) + { + auto ist = glp_mip_status(lp); + if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { + _result = result_t::POSSIBLE; + } + else + { + _result = result_t::IMPOSSIBLE; + } + } + } + else if (status == GLP_FEAS || status == GLP_UNBND) + { + _result = result_t::POSSIBLE; + } + else + { + _result = result_t::IMPOSSIBLE; + } + } + else if (result == GLP_ENOPFS || result == GLP_ENODFS || result == GLP_ENOFEAS) + { + _result = result_t::IMPOSSIBLE; + } + + double rvalue; + + + if(_result == result_t::IMPOSSIBLE){ + rvalue = -2; + }else{ + rvalue = glp_get_obj_val(lp); + } + + glp_delete_prob(lp); + + return rvalue; + } + void LinearProgram::solvePotency(const PQL::SimplificationContext& context, std::vector& potencies) { bool use_ilp = false; // No need to call the ILP solver diff --git a/src/PetriEngine/Simplification/LinearPrograms.cpp b/src/PetriEngine/Simplification/LinearPrograms.cpp index 104052e71..64d0df273 100644 --- a/src/PetriEngine/Simplification/LinearPrograms.cpp +++ b/src/PetriEngine/Simplification/LinearPrograms.cpp @@ -28,6 +28,26 @@ namespace PetriEngine { return _result == POSSIBLE; } + bool AbstractProgramCollection::boundedSatisfiable(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) + { + reset(); + _result = UNKNOWN; + if (context.timeout() || has_empty || solvetime == 0){ + std::cout << "returning from timeout/empty\n"; + return true; + } + + boundedSatisfiableImpl(context, bounds, solvetime); + + bool bounded_sat = _result == POSSIBLE; + _result = UNKNOWN; + return bounded_sat; + } + + double AbstractProgramCollection::upperBound(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime){ + return upperBoundImpl(context, place_set, solvetime); + } + uint32_t AbstractProgramCollection::explorePotency(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -106,6 +126,30 @@ namespace PetriEngine { _result = IMPOSSIBLE; } + void UnionCollection::boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) + { + for (int i = lps.size() - 1; i >= 0; --i) + { + if (lps[i]->boundedSatisfiable(context, bounds, solvetime) || context.timeout()) + { + _result = POSSIBLE; + return; + } + } + if (_result != POSSIBLE) + _result = IMPOSSIBLE; + } + + double UnionCollection::upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) + { + double maxBound = -std::numeric_limits::infinity(); + for (int i = lps.size() - 1; i >= 0; --i) + { + maxBound = std::max(maxBound, lps[i]->upperBound(context, place_set, solvetime)); + } + return maxBound; + } + uint32_t UnionCollection::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -235,6 +279,54 @@ namespace PetriEngine { _result = IMPOSSIBLE; } + void MergeCollection::boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) + { + // this is where the magic needs to happen + bool hasmore = false; + do { + if (context.timeout()) + { + _result = POSSIBLE; + break; + } + + LinearProgram prog; + bool has_empty = false; + hasmore = merge(has_empty, prog); + if (has_empty) + { + _result = POSSIBLE; + return; + } + else + { + if (context.timeout() || + !prog.isBoundedImpossible(context, bounds, solvetime)) + { + _result = POSSIBLE; + break; + } + } + ++nsat; + } while (hasmore); + if (_result != POSSIBLE) + _result = IMPOSSIBLE; + } + + double MergeCollection::upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime) + { + double maxBound = -std::numeric_limits::infinity(); + bool hasmore = false; + do { + LinearProgram prog; + bool has_empty = false; + hasmore = merge(has_empty, prog); + maxBound = std::max(maxBound, prog.upperBoundForPlace(context, place_set, solvetime)); + ++nsat; + } while (hasmore); + return maxBound; + } + uint32_t MergeCollection::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -287,6 +379,10 @@ namespace PetriEngine { return false; } + double SingleProgram::upperBoundImpl(const PQL::SimplificationContext& context, std::vector& place_set, uint32_t solvetime){ + return program.upperBoundForPlace(context, place_set, solvetime); + } + void SingleProgram::satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) { // this is where the magic needs to happen @@ -300,6 +396,19 @@ namespace PetriEngine { } } + void SingleProgram::boundedSatisfiableImpl(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime) + { + // this is where the magic needs to happen + if (!program.isBoundedImpossible(context, bounds, solvetime)) + { + _result = POSSIBLE; + } + else + { + _result = IMPOSSIBLE; + } + } + uint32_t SingleProgram::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -309,5 +418,9 @@ namespace PetriEngine { program.solvePotency(context, potencies); return maxConfigurationsSolved - 1; } + + bool SingleProgram::isBoundedImpossible(const PQL::SimplificationContext& context, std::vector, double>>& bounds, uint32_t solvetime){ + return program.isBoundedImpossible(context, bounds, solvetime); + } } }