From 533cb83ec1eb9354865b040f2e63cb0b05f9cfdd Mon Sep 17 00:00:00 2001 From: "bruno.gonzalez" Date: Mon, 22 Sep 2025 18:47:00 +0200 Subject: [PATCH 1/6] 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 2/6] 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 3/6] 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 4/6] 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 5/6] 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 6/6] 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;