diff --git a/include/PetriEngine/PQL/Contexts.h b/include/PetriEngine/PQL/Contexts.h index d7301ab28..dc28115df 100644 --- a/include/PetriEngine/PQL/Contexts.h +++ b/include/PetriEngine/PQL/Contexts.h @@ -26,6 +26,7 @@ #include "../Simplification/LPCache.h" #include "../NetStructures.h" #include "utils/structures/shared_string.h" +#include "PetriEngine/options.h" #include "utils/errors.h" @@ -36,6 +37,8 @@ #include #include +#include + namespace PetriEngine { namespace PQL { @@ -201,16 +204,22 @@ namespace PetriEngine { }; class SimplificationContext { + struct simplificationRules{ + bool G_rule = false; + bool F_rule = false; + bool X_rule = false; + }; public: SimplificationContext(const MarkVal* marking, - const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, + const PetriNet* net, int num_paths, uint32_t queryTimeout, uint32_t lpTimeout, uint32_t lpPrintLevel, Simplification::LPCache* cache, uint32_t potencyTimeout = 0) - : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), + : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout), _lpPrintLevel(lpPrintLevel), _potencyTimeout(potencyTimeout) { _negated = false; _marking = marking; _net = net; + _num_paths = num_paths; _base_lp = buildBase(); _start = std::chrono::high_resolution_clock::now(); _cache = cache; @@ -220,8 +229,26 @@ namespace PetriEngine { _markingOutOfBounds = true; } } + + _isDeadlocked = _net->deadlocked(_marking); + _id = std::chrono::system_clock::now(); + } + + SimplificationContext(const MarkVal* marking, + const PetriNet* net, int num_paths, uint32_t queryTimeout, options_t& options, + Simplification::LPCache* cache) + : SimplificationContext(marking, net, num_paths, queryTimeout, options.lpsolveTimeout, options.lpPrintLevel, cache){ + _rules = {options.useGRule, options.useFRule, options.useXRule}; + _permutationLimit = static_cast(options.permutationLimit); + } + SimplificationContext(const MarkVal* marking, + const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout, uint32_t lpPrintLevel, + Simplification::LPCache* cache, uint32_t potencyTimeout = 0) : SimplificationContext(marking, net, 1, queryTimeout, lpTimeout, lpPrintLevel, cache, potencyTimeout){}; + + std::chrono::time_point _id; + virtual ~SimplificationContext() { if(_base_lp != nullptr) glp_delete_prob(_base_lp); @@ -237,6 +264,10 @@ namespace PetriEngine { return _markingOutOfBounds; } + bool isDeadlocked() const { + return _isDeadlocked; + } + const PetriNet* net() const { return _net; } @@ -269,20 +300,52 @@ namespace PetriEngine { uint32_t getLpTimeout() const; uint32_t getPotencyTimeout() const; + uint32_t getPrintLevel() const; + + uint32_t numPaths() const{ + return _num_paths; + } + + uint32_t getNumBaseVariables() const{ + return _num_paths * (_net->numberOfPlaces() + _net->numberOfTransitions()); + } + + uint32_t getNumBaseConstraints() const{ + return _num_paths * _net->numberOfPlaces(); + } Simplification::LPCache* cache() const { return _cache; } + const simplificationRules& rules() const + { + return _rules; + } + + const uint64_t getPermutationLimit() const + { + return _permutationLimit; + } + + void addAllPathConstraint(glp_prob* lp, size_t t, size_t l, int32_t* ind, double* col) const; + void addAllPathConstraint(glp_prob* lp, size_t t, size_t l, std::vector& ind, std::vector& col) const; + glp_prob* makeBaseLP() const; + glp_prob* buildBaseFromMarking(std::vector, double>>& setMarking) const; + private: + uint32_t _num_paths = 1; + simplificationRules _rules; + uint64_t _permutationLimit = 128; bool _negated; const MarkVal* _marking; bool _markingOutOfBounds; + bool _isDeadlocked; const PetriNet* _net; - uint32_t _queryTimeout, _lpTimeout, _potencyTimeout; + 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..22e081324 100644 --- a/include/PetriEngine/PQL/Simplifier.h +++ b/include/PetriEngine/PQL/Simplifier.h @@ -39,6 +39,18 @@ namespace PetriEngine { namespace PQL { SimplificationContext& _context; Retval _return_value; + enum LPOP {NONE, GLOBAL, FINAL, NEXT, UNTIL, OTHER, NULLT}; + LPOP operator_found = LPOP::NONE; + LPOP operator_parent = LPOP::NONE; + bool op_parent_negated = false; + AbstractProgramCollection::temporalContext tcx; + int32_t operators = 0; + + bool finalLpsImpossible(std::vector& final_lps); + bool finalLpsImpossibleAll(std::vector& final_lps); + bool nextLpsImpossible(std::vector& next_lps, std::vector& final_lps, bool is_invariant, bool is_or = false); + bool isNextImpossible(AbstractProgramCollection_ptr next_lps, bool strict); + Retval simplify_or(const LogicalCondition* element); Retval simplify_and(const LogicalCondition *element); @@ -50,9 +62,14 @@ 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); + template + Retval simplify_simple_quantifier(Retval &r, bool strict); + void _accept(const NotCondition *element) override; void _accept(const AndCondition *element) override; @@ -113,6 +130,7 @@ namespace PetriEngine { namespace PQL { }; Member memberForPlace(size_t p, const SimplificationContext &context); + Member memberForPathPlace(size_t p, int trace, const SimplificationContext &context); Member constraint(const Expr *element, const SimplificationContext &context); class ConstraintVisitor : public ExpressionVisitor { @@ -123,6 +141,7 @@ namespace PetriEngine { namespace PQL { private: const SimplificationContext& _context; + int _current_path = 0; Member _return_value; void _accept(const LiteralExpr *element) override; diff --git a/include/PetriEngine/Simplification/LinearProgram.h b/include/PetriEngine/Simplification/LinearProgram.h index 310465c6d..019527ab2 100644 --- a/include/PetriEngine/Simplification/LinearProgram.h +++ b/include/PetriEngine/Simplification/LinearProgram.h @@ -11,8 +11,10 @@ #include #include + namespace PetriEngine { namespace Simplification { + using REAL = double; struct equation_t { @@ -35,6 +37,17 @@ namespace PetriEngine { enum result_t { UKNOWN, IMPOSSIBLE, POSSIBLE }; result_t _result = result_t::UKNOWN; std::vector _equations; + // does the writing + static bool _writeEquationsImpl(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, bool allocate, int32_t variable_shift = 0); + // adds rows to the lp, works from empty lp + static bool pushEquations(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations); + static bool pushEquationsShifted(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, int32_t variable_shift = 0); + // does not add rows to the lp, requires pre-allocating + static bool emplaceEquations(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations); + static bool emplaceEquationsShifted(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, int32_t variable_shift = 0); + + static result_t solve_built_lp(glp_prob* lp, const PQL::SimplificationContext& context, uint32_t solvetime , bool delete_lp = true); + result_t solve_and_set(glp_prob* lp, const PQL::SimplificationContext& context, uint32_t solvetime, bool delete_lp = true); public: void swap(LinearProgram& other) { @@ -62,11 +75,19 @@ namespace PetriEngine { bool knownImpossible() const { return _result == result_t::IMPOSSIBLE; } bool knownPossible() const { return _result == result_t::POSSIBLE; } + bool isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime); + bool isFinalImpossibleWith(const LinearProgram* withLp, bool is_next, bool is_strict, const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()) const; + bool isFinalImpossibleWithN(const std::vector& permutation, const std::vector& lps, bool is_next, bool is_strict, const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()) const; + bool isNStepsImpossible(double firelimit, bool strict, const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()); void solvePotency(const PQL::SimplificationContext& context, std::vector& potencies); + static bool solveFinalConjunctionImpossible(std::vector& lps, std::vector>& perms, std::vector& starts,const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()); + private: + static bool isFinalPermutationImpossible(glp_prob* lp, const std::vector& permutation, const std::vector& lps,const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()); + public: void make_union(const LinearProgram& other); - + std::ostream& print(std::ostream& ss, size_t indent = 0) const { for (size_t i = 0; i < indent ; ++i) ss << "\t"; diff --git a/include/PetriEngine/Simplification/LinearPrograms.h b/include/PetriEngine/Simplification/LinearPrograms.h index 0b222ebf6..029b6f910 100644 --- a/include/PetriEngine/Simplification/LinearPrograms.h +++ b/include/PetriEngine/Simplification/LinearPrograms.h @@ -8,31 +8,348 @@ namespace PetriEngine { namespace Simplification { - class AbstractProgramCollection + class AbstractProgramCollection; + + struct nextProgram { + std::shared_ptr prog; + bool hasmore; + }; + + + + + class AbstractProgramCollection + { + public: + enum operator_t {F, X, G, FREE}; + + struct temporalContext{ + operator_t _operator = operator_t::FREE; + int _next_ops = 0; + bool _is_invariant = false; + int prefix_F = 0; + int prefix_X = 0; + int prefix_G = 0; + + bool allow_basic_solve = true; + bool enable_F_rule = true; + bool enable_X_rule = true; + + temporalContext(bool is_invariant) : _is_invariant(is_invariant) {}; + temporalContext() : temporalContext(false){}; + + void update(operator_t new_operator, int leading_next_depth){ + _operator = std::min(_operator, new_operator); + _next_ops += leading_next_depth; + } + + std::tuple push_prefix(operator_t update_op, bool negated){ + auto pre_state = std::make_tuple(prefix_F, prefix_G, prefix_X); + + prefix_X += (update_op == operator_t::X); + prefix_F += ( update_op == operator_t::F && !negated ) || + ( update_op == operator_t::G && negated ); + + prefix_G += ( update_op == operator_t::F && negated ) || + ( update_op == operator_t::G && !negated ); + return pre_state; + } + + std::tuple clear_context(){ + auto pre_state = std::make_tuple(prefix_F, prefix_G, prefix_X); + + prefix_X = 0; + prefix_F = 0; + prefix_G = 0; + + return pre_state; + } + + void set_prefix(std::tuple& state){ + prefix_F = std::get<0>(state); + prefix_G = std::get<1>(state); + prefix_X = std::get<2>(state); + } + + bool has_prefix() const{ + return (prefix_F + prefix_G + prefix_X) > 0; + } + + bool skip_solve() const{ + return !allow_basic_solve; + } + }; + struct temporalProgram{ + temporalContext tcx; + LinearProgram prog; + }; + struct timepoint{ + std::vector> next; + std::vector free_lps = {}; + std::vector final_lps = {}; + std::vector next_lps = {}; + std::vector global_lps = {}; + + LinearProgram program; + bool is_compiled = false; + bool is_child = false; + + timepoint() = default; + + void print(int depth); + void print(); + + bool has_conditions() const{ + return free_lps.size() > 0 || final_lps.size() > 0 || + next_lps.size() > 0 || global_lps.size() > 0; + } + + bool is_empty() const{ + return next.size() == 0 && !has_conditions(); + } + + + std::shared_ptr clone(); + + + void make_union(LinearProgram& union_lp); + void update_next_counter(int next_ops); + bool is_impossible(std::vector& progs, std::vector>& ivals, const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime); + bool is_impossible(const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime); + }; + protected: + + struct mergeBuffer{ + temporalContext pre_ctx; + temporalContext post_ctx; + LinearProgram program; + std::shared_ptr time_path = nullptr; + mergeBuffer() = default; + mergeBuffer(temporalContext _ctx, LinearProgram _prog) : pre_ctx(_ctx), program(_prog){ + post_ctx = temporalContext(true); + }; + + + void advance_timepoint(){ + assert(time_path); + if(time_path->is_empty()){ + std::cout << "empty path\n"; + return; + } + assert(time_path->is_compiled); + time_path->is_child = true; + // create a new empty timepoint as the current timepoint, and appends the previous one + auto tp = std::make_shared(timepoint()); + + tp->next.push_back(time_path); + time_path = tp; + + } + + void compile_program(); + + void apply_operator(operator_t update_op, int next_ops); + + void merge(mergeBuffer& other); + + void print(){ + if(!time_path){ + std::cout << "LPS: [null]"; + return; + } + time_path->print(); + } + + /*std::tuple, std::vector>, std::vector> setup_solve(){ + std::vector lps; + + std::vector fixpoints; + + for(auto cur = time_path; cur != nullptr; cur = cur->next){ + if(cur->free_lps.size() > 0){ + fixpoints.push_back(lps.size()); + lps.push_back(&cur->free_lps[0].prog); + } + + for(auto& [_tcx, _prog] : cur->final_lps){ + lps.push_back(&_prog); + } + + for(auto& [_tcx, _prog] : cur->next_lps){ + lps.push_back(&_prog); + } + } + + std::vector> perms; + std::vector starts; + if(fixpoints.empty()){ + std::vector perm(lps.size()); + for(int i = 0; i < lps.size(); i++){ + perm[i] = i; + } + perms.push_back(perm); + starts.push_back(0); + } + else{ + int start = 0; + for(int fix : fixpoints){ + if(fix == start){ + start = fix + 1; + continue; + } + std::vector perm(fix - start); + for(int i = 0; i < (fix - start); i++){ + perm[i] = start + i; + } + perms.push_back(perm); + starts.push_back(start); + start = fix + 1; + } + if(start < lps.size()){ + std::vector perm(lps.size() - start); + for(int i = 0; i < (lps.size() - start); i++){ + perm[i] = start + i; + } + perms.push_back(perm); + starts.push_back(start); + } + } + + return std::make_tuple(lps, perms, starts); + }*/ + + bool lpsImpossible(const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime); + + private: + void update_next_counter(std::vector& lps, int next_ops){ + if(next_ops == 0) + return; + for(size_t i = 0; i < lps.size(); i++){ + lps[i].tcx._next_ops += next_ops; + } + } + }; + enum result_t { UNKNOWN, IMPOSSIBLE, POSSIBLE }; result_t _result = result_t::UNKNOWN; + operator_t _operator = operator_t::FREE; + int _next_ops = 0; bool has_empty = false; - virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) = 0; + virtual std::shared_ptr cloneImpl() = 0; + virtual void satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) = 0; virtual uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) = 0; + virtual nextProgram getNextProgramImpl() = 0; public: + /* it is not safe to have two iterators to the same collection, as they change the internal state */ + struct ProgramIterator{ + using interator_category = std::input_iterator_tag; + using difference_type = std::ptrdiff_t; + using value_type = LinearProgram*; + ProgramIterator() = default; + + ProgramIterator(AbstractProgramCollection* collection) + : _collection(collection) { + _collection->reset(); + _next = _collection->get_next_program(); + _next_ptr = _next.prog.get(); + } + + const value_type& operator*() const { + return _next_ptr; + } + + const LinearProgram* operator->() const { + return _next.prog.get(); + } + + ProgramIterator& operator++() { + if(!_next.hasmore){ + _collection = nullptr; + }else{ + _next = _collection->get_next_program(); + _next_ptr = _next.prog.get(); + } + return *this; + } + + ProgramIterator operator++(int) { + auto tmp = *this; + ++*this; + return tmp; + } + + friend bool operator==(const ProgramIterator& a, + const ProgramIterator& b) + { + return a._collection == b._collection; + } + + friend bool operator!=(const ProgramIterator& a, + const ProgramIterator& b) + { + return !(a == b); + } + private: + AbstractProgramCollection* _collection = nullptr; + LinearProgram* _next_ptr; + nextProgram _next; + }; + + class ProgRange { + public: + ProgRange(AbstractProgramCollection* collection) + : _collection(collection){} + + ProgramIterator begin() { + return ProgramIterator(_collection); + } + + ProgramIterator end() { + return {}; + } + + private: + AbstractProgramCollection* _collection; + }; + + ProgRange AllProgs() { + reset(); + return ProgRange(this); + } + virtual ~AbstractProgramCollection() {} bool empty() { return has_empty; } - virtual bool satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits::max()); + void update_operator(operator_t update_op){ + if(update_op != _operator || update_op == operator_t::X){ + _result = result_t::UNKNOWN; + } + //std::cout << "update_operator\n"; + //std::cout << "op: " << update_op << ", " << (update_op == operator_t::X) << "\n"; + _operator = std::min(_operator, update_op); + _next_ops += (update_op == operator_t::X); + //std::cout << "next ops: " << _next_ops << "\n"; + } + + virtual std::shared_ptr clone(); + virtual bool satisfiable(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime = std::numeric_limits::max()); + virtual nextProgram get_next_program(); bool known_sat() { return _result == POSSIBLE; } bool known_unsat() { return _result == IMPOSSIBLE; } 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 bool merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run = false) = 0; + virtual uint32_t explorePotency(const PQL::SimplificationContext& context, std::vector &potencies, @@ -48,10 +365,13 @@ namespace PetriEngine { size_t current = 0; size_t _size = 0; - void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + std::shared_ptr cloneImpl() override; + void satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; + + nextProgram getNextProgramImpl() override; public: UnionCollection(std::vector&& programs); @@ -60,7 +380,7 @@ namespace PetriEngine { void clear() override; void reset() override; size_t size() const override { return _size; } - bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) override; + bool merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run = false) override; }; class MergeCollection : public AbstractProgramCollection @@ -69,7 +389,8 @@ namespace PetriEngine { AbstractProgramCollection_ptr left = nullptr; AbstractProgramCollection_ptr right = nullptr; - LinearProgram tmp_prog; + LinearProgram tmp_prog; + mergeBuffer right_buf; bool merge_right = true; bool more_right = true; bool rempty = false; @@ -77,10 +398,16 @@ namespace PetriEngine { size_t curr = 0; size_t _size = 0; - void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + LinearProgram next_prog; + std::vector _final_programs; + + std::shared_ptr cloneImpl() override; + void satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; + + nextProgram getNextProgramImpl() override; public: MergeCollection(const AbstractProgramCollection_ptr& A, const AbstractProgramCollection_ptr& B); @@ -88,7 +415,7 @@ namespace PetriEngine { void clear() override; void reset() override; size_t size() const override { return _size - nsat; } - bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) override; + bool merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run = false) override; }; class SingleProgram : public AbstractProgramCollection { @@ -96,21 +423,30 @@ namespace PetriEngine { LinearProgram program; protected: - void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) override; + std::shared_ptr cloneImpl() override; + void satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) override; uint32_t explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) override; - + nextProgram getNextProgramImpl() override; public: SingleProgram(); + SingleProgram(LinearProgram lp); SingleProgram(LPCache* factory, const Member& lh, int64_t constant, op_t op); + virtual ~SingleProgram() {} void clear() override {} void reset() override {} size_t size() const override { return 1; } - bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) override; + bool merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run = false) override; + + LinearProgram getProgram() const{ + return program; + } + + }; } } 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/PetriEngine/Simplification/Vector.h b/include/PetriEngine/Simplification/Vector.h index a2d3cf68f..887b91f99 100644 --- a/include/PetriEngine/Simplification/Vector.h +++ b/include/PetriEngine/Simplification/Vector.h @@ -90,6 +90,21 @@ namespace PetriEngine { return l; } + size_t write_indir_shifted(std::vector& dest, std::vector& indir, int32_t shift) const + { + size_t l = 1; + for(const auto& el : _data) + { + dest[l] = el.second; + if(dest[l] != 0) + { + indir[l] = el.first + shift + 1; + ++l; + } + } + return l; + } + private: Vector(const std::vector& data) diff --git a/include/PetriEngine/options.h b/include/PetriEngine/options.h index 49f29a216..99417b4f3 100644 --- a/include/PetriEngine/options.h +++ b/include/PetriEngine/options.h @@ -62,9 +62,12 @@ 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; + int queryReductionTimeout = 30, intervalTimeout = 10, partitionTimeout = 5, lpsolveTimeout = 10, lpPrintLevel = 0, initPotencyTimeout = 10; TraceLevel trace = TraceLevel::None; bool use_query_reductions = true; + bool useGRule = true, useFRule = true, useXRule = true; + int permutationLimit = 128; + uint32_t siphontrapTimeout = 0; uint32_t siphonDepth = 0; uint32_t cores = 1; diff --git a/src/PetriEngine/PQL/Contexts.cpp b/src/PetriEngine/PQL/Contexts.cpp index f0fb0b404..2919a3890 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 @@ -87,6 +92,109 @@ namespace PetriEngine { } glp_prob* SimplificationContext::buildBase() 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 = getNumBaseVariables(); + const uint32_t nRow = getNumBaseConstraints(); + 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()); + + addAllPathConstraint(lp, t, l, indir, col); + + if (timeout()) { + std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return nullptr; + } + } + } + int rowno = 1; + std::vector ind(2); + std::vector one = {0, 1.0}; + for(size_t path = 0; path < static_cast(_num_paths); path++){ + const int variable_offset = path * ( _net->numberOfTransitions() + _net->numberOfPlaces() ); + const int constraint_offset = path * _net->numberOfPlaces(); + for (size_t p = 0; p < _net->numberOfPlaces(); p++) { + const int colno = 1 + p + _net->numberOfTransitions() + variable_offset; + ind[1] = p+1 + constraint_offset; + glp_set_mat_col(lp, colno, 1, ind.data(), one.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + ++rowno; + + 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); + + if (timeout()) { + std::cerr << "glpk: construction timeout" << std::endl; + glp_delete_prob(lp); + return nullptr; + } + } + } + + return lp; + } + + + void SimplificationContext::addAllPathConstraint(glp_prob* lp, size_t t, size_t l, int32_t* ind_data, double* col_data) const{ + std::vector indir_path(l); + for(size_t path = 0; path < static_cast(_num_paths); path++){ + const int variable_offset = path * ( _net->numberOfTransitions() + _net->numberOfPlaces() ); + for(int i = 1; i < l; i++){ + indir_path[i] = ind_data[i] + path * _net->numberOfPlaces(); + } + glp_set_mat_col(lp, t + 1 + variable_offset, l - 1, indir_path.data(), col_data); + } + } + void SimplificationContext::addAllPathConstraint(glp_prob* lp, size_t t, size_t l, std::vector& ind, std::vector& col) const{ + addAllPathConstraint(lp, t, l, ind.data(), col.data()); + } + + glp_prob* SimplificationContext::buildBaseFromMarking(std::vector, double>>& setMarking) const { constexpr auto infty = std::numeric_limits::infinity(); if (timeout()) @@ -97,7 +205,7 @@ namespace PetriEngine { return lp; const uint32_t nCol = _net->numberOfTransitions(); - const int nRow = _net->numberOfPlaces(); + const int nRow = setMarking.size(); std::vector indir(std::max(nCol, nRow) + 1); glp_add_cols(lp, nCol + 1); @@ -145,7 +253,11 @@ namespace PetriEngine { } int rowno = 1; for (size_t p = 0; p < _net->numberOfPlaces(); p++) { - glp_set_row_bnds(lp, rowno, GLP_LO, (0.0 - (double) _marking[p]), infty); + 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; @@ -153,6 +265,32 @@ namespace PetriEngine { 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 85499d9b6..c81e796d6 100644 --- a/src/PetriEngine/PQL/Simplifier.cpp +++ b/src/PetriEngine/PQL/Simplifier.cpp @@ -44,8 +44,496 @@ namespace PetriEngine { namespace PQL { return lps[0]; } - Retval Simplifier::simplify_or(const LogicalCondition *element) { + bool Simplifier::finalLpsImpossible(std::vector& final_lps){ + return finalLpsImpossibleAll(final_lps); + for(int i = 0; i < final_lps.size(); i++){ + if(!final_lps[i]->satisfiable(_context, tcx)){ + return true; + } + } + + if(final_lps.size() == 1) + return false; + + for(int i = 0; i < final_lps.size(); i++){ + for(int j = i + 1; j < final_lps.size(); j++){ + bool sat = false; + for(auto& lp_i : final_lps[i]->AllProgs()){ + for(auto& lp_j : final_lps[j]->AllProgs()){ + if(!lp_i->isFinalImpossibleWith(lp_j, false, false, _context) || + !lp_j->isFinalImpossibleWith(lp_i, false, false, _context)) + { + sat = true; + break; + } + } + if(sat) + break; + } + if(!sat) + return true; + } + } + return false; + } + + bool Simplifier::finalLpsImpossibleAll(std::vector& final_lps){ + for(int i = 0; i < final_lps.size(); i++){ + if(!final_lps[i]->satisfiable(_context, tcx)){ + return true; + } + } + + if(final_lps.size() == 1) + return false; + + std::vector iters; + + for(int i = 0; i < final_lps.size(); i++){ + iters.push_back(AbstractProgramCollection::ProgramIterator(final_lps[i].get())); + } + + auto end = AbstractProgramCollection::ProgramIterator(); + + bool done = false; + int n = final_lps.size(); + int lps_solved = 0; + while(!done){ + /* produce all permutations */ + std::vector perm(n); + for(int i = 0; i < n; i++){ + perm[i] = i; + } + + /* all current lps */ + std::vector progs; + for(int l = 0; l < n; l++){ + progs.push_back(*iters[l]); + std::cout << progs[l]->size() << "\n"; + } + bool sat = false; + do{ + if(!progs[0]->isFinalImpossibleWithN(perm, progs, false, false, _context)){ + sat = true; + break; + } + lps_solved += 1; + }while(std::next_permutation(perm.begin(), perm.end())); + + if(sat) + return false; + + int i = n - 1; + while(1){ + iters[i]++; + if(iters[i] == end){ + iters[i] = AbstractProgramCollection::ProgramIterator(final_lps[i].get()); + }else{ + break; + } + i--; + if(i < 0){ + done = true; + break; + } + } + } + + return true; + } + + + bool Simplifier::nextLpsImpossible(std::vector& next_lps, std::vector& final_lps, bool istcx, bool is_or){ + std::cout << "next lps\n"; + const bool strictNext = !_context.isDeadlocked(); + for(int i = 0; i < next_lps.size(); i++){ + if(istcx){ + bool sat = false; + for(auto& lp : next_lps[i]->AllProgs()){ + if(!lp->isNStepsImpossible(1, strictNext, _context)){ + sat = true; + break; + } + } + if(!sat){ + return true; + } + }else{ + if(!next_lps[i]->satisfiable(_context, tcx)){ + return true; + } + } + } + + if(next_lps.size() == 0 || final_lps.size() == 0 || !istcx) + return false; + + for(int j = 0; j < final_lps.size(); j++){ + // checks if lp holds in initial marking, and if it does skips it + bool init_sat = false; + for(auto& lp: final_lps[j]->AllProgs()){ + if(!lp->isNStepsImpossible(0, true, _context)){ + init_sat = true; + break; + } + } + if(init_sat) + continue; + + for(int i = 0; i < next_lps.size(); i++){ + bool sat = false; + // the lps i/j may be union/mergecollections of many programs + for(auto& lp_j : final_lps[j]->AllProgs()){ + for(auto& lp_i : next_lps[i]->AllProgs()){ + if(!lp_i->isFinalImpossibleWith(lp_j, true, strictNext, _context)){ + sat = true; + break; + } + } + if(sat) + break; + } + + if(!sat){ + return true; + } + } + } + return false; + } + + + + AbstractProgramCollection_ptr createGlobalUnion(AbstractProgramCollection_ptr &global_lp, std::vector &&nonglobal_lps) { + if(global_lp == nullptr){ + if(nonglobal_lps.size() == 0){ + return nullptr; + }else{ + 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::vector conditions; + std::vector lps; + std::vector unquantified_neglpsv, global_neglpsv, final_neglpsv, next_neglpsv, nonglobal_neglpsv; + + const bool same_context = op_parent_negated == _context.negated(); + const bool parent_final = operator_parent == LPOP::FINAL; + const bool parent_global = operator_parent == LPOP::GLOBAL; + const bool neg_istcx = (same_context && parent_final) || (!same_context && parent_global); + + const auto local_parent = operator_parent; + + auto unique_operator = LPOP::NULLT; + + for (const auto &c: element->getOperands()) { + operator_found = LPOP::NONE; + int32_t pre_operators = operators; + if(!neg_istcx) + operator_parent = LPOP::OTHER; + Visitor::visit(this, c); + operator_parent = local_parent; + + if(unique_operator == LPOP::NULLT){ + unique_operator = operator_found; + }else{ + if(operator_found != unique_operator){ + unique_operator = LPOP::OTHER; + } + } + + auto r = std::move(_return_value); + assert(r.neglps); + assert(r.lps); + + if (r.formula->isTriviallyTrue()) { + operator_found = LPOP::OTHER; + return Retval(BooleanCondition::TRUE_CONSTANT); + } else if (r.formula->isTriviallyFalse()) { + continue; + } + + conditions.push_back(r.formula); + + lps.emplace_back(r.lps); + + if( ( operators - pre_operators ) > 1){ + nonglobal_neglpsv.emplace_back(r.neglps); + }else { + switch(operator_found){ + case LPOP::NONE: + if(neg_istcx){ + global_neglpsv.emplace_back(r.neglps); + }else{ + unquantified_neglpsv.emplace_back(r.neglps); + } + break; + case LPOP::FINAL: + global_neglpsv.emplace_back(r.neglps); + break; + case LPOP::GLOBAL: + final_neglpsv.emplace_back(r.neglps); + break; + case LPOP::UNTIL: + final_neglpsv.emplace_back(r.neglps); + break; + case LPOP::NEXT: + next_neglpsv.emplace_back(r.neglps); + break; + default: + nonglobal_neglpsv.emplace_back(r.neglps); + } + } + } + + //operator_found = LPOP::OTHER; + if(unique_operator == LPOP::NULLT || unique_operator != LPOP::NONE){ + operator_found == LPOP::OTHER; + } + if (conditions.size() == 0) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } + + nonglobal_neglpsv.clear(); + if(!_context.rules().F_rule){ + final_neglpsv.clear(); + } + if(!_context.rules().G_rule){ + std::move(global_neglpsv.begin(), global_neglpsv.end(), std::back_inserter(nonglobal_neglpsv)); + global_neglpsv.clear(); + } + if(!_context.rules().X_rule){ + next_neglpsv.clear(); + } + + if(unquantified_neglpsv.size() > 0){ + auto uq_neglps = mergeLps(std::move(unquantified_neglpsv)); + nonglobal_neglpsv.emplace_back(uq_neglps); + } + + + auto global_neglp = mergeLps(std::move(global_neglpsv)); + auto neglps = createGlobalUnion(global_neglp, std::move(nonglobal_neglpsv)); + + if(neglps == nullptr){ + neglps = std::make_shared(); + } + + if(final_neglpsv.size() > 0){ + if(global_neglp){ + std::cout << "global merge\n"; + for(int i = 0; i < final_neglpsv.size(); i++){ + final_neglpsv[i] = std::make_shared(global_neglp, final_neglpsv[i]); + } + } + if(finalLpsImpossible(final_neglpsv)){ + return Retval(BooleanCondition::TRUE_CONSTANT); + } + } + + if(next_neglpsv.size() > 0){ + if(global_neglp){ + for(int i = 0; i < next_neglpsv.size(); i++){ + next_neglpsv[i] = std::make_shared(global_neglp, next_neglpsv[i]); + } + } + const bool next_istcx = neg_istcx || (operator_parent == LPOP::NONE); + if(nextLpsImpossible(next_neglpsv, final_neglpsv, next_istcx, true)){ + return Retval(BooleanCondition::TRUE_CONSTANT); + } + } + + if(lps.size() == 0){ + lps.emplace_back(std::make_shared()); + } + + try { + if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } + } + catch (std::bad_alloc &e) { + // we are out of memory, deal with it. + 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 + //std::cout << "leaving or\n"; + std::cout << "returning " << lps.size() << " + " << neglps->size() << "\n"; + return Retval( + makeOr(conditions), + std::make_shared(std::move(lps)), + std::move(neglps)); + }*/ + + + /*Retval Simplifier::simplify_and(const LogicalCondition *element) { + std::vector conditions; + std::vector global_lpsv, final_lpsv, next_lpsv, opfree_lpsv, nonglobal_lpsv; + std::vector neglps; + + const bool same_context = op_parent_negated == _context.negated(); + const bool parent_final = operator_parent == LPOP::FINAL; + const bool parent_global = operator_parent == LPOP::GLOBAL; + const bool istcx = (same_context && parent_global) || (!same_context && parent_final); + const auto local_parent = operator_parent; + + auto unique_operator = LPOP::NULLT; + for (auto &c: element->getOperands()) { + operator_found = LPOP::NONE; + int32_t pre_operators = operators; + if(!istcx) + operator_parent = LPOP::OTHER; + Visitor::visit(this, c); + operator_parent = local_parent; + + if(unique_operator == LPOP::NULLT){ + unique_operator = operator_found; + }else{ + if(operator_found != unique_operator){ + unique_operator = LPOP::OTHER; + } + } + + auto r = std::move(_return_value); + if (r.formula->isTriviallyFalse()) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } else if (r.formula->isTriviallyTrue()) { + continue; + } + + conditions.push_back(r.formula); + + std::cout << "OP: " << operator_found << "\n"; + + if( ( operators - pre_operators ) > 1){ + nonglobal_lpsv.emplace_back(r.lps); + }else { + switch(operator_found){ + case LPOP::NONE: + if(istcx){ + global_lpsv.emplace_back(r.lps); + }else{ + opfree_lpsv.emplace_back(r.lps); + } + break; + case LPOP::GLOBAL: + global_lpsv.emplace_back(r.lps); + break; + case LPOP::FINAL: + final_lpsv.emplace_back(r.lps); + break; + case LPOP::UNTIL: + final_lpsv.emplace_back(r.lps); + break; + case LPOP::NEXT: + next_lpsv.emplace_back(r.lps); + break; + default: + nonglobal_lpsv.emplace_back(r.lps); + } + } + neglps.emplace_back(r.neglps); + } + + if(unique_operator == LPOP::NULLT || unique_operator == LPOP::OTHER){ + operator_found == LPOP::OTHER; + } + + if (conditions.size() == 0) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } + nonglobal_lpsv.clear(); + if(!_context.rules().F_rule){ + final_lpsv.clear(); + } + if(!_context.rules().G_rule){ + std::move(global_lpsv.begin(), global_lpsv.end(), std::back_inserter(nonglobal_lpsv)); + global_lpsv.clear(); + } + if(!_context.rules().X_rule){ + next_lpsv.clear(); + } + + if(opfree_lpsv.size() > 0){ + auto uq_lps = mergeLps(std::move(opfree_lpsv)); + nonglobal_lpsv.emplace_back(uq_lps); + } + + auto global_lp = mergeLps(std::move(global_lpsv)); + auto lps = createGlobalUnion(global_lp, std::move(nonglobal_lpsv)); + + if(lps == nullptr){ + lps = std::make_shared(); + } + + if(final_lpsv.size() > 0){ + if(global_lp){ + std::cout << "global merge\n"; + for(int i = 0; i < final_lpsv.size(); i++){ + final_lpsv[i] = std::make_shared(global_lp, final_lpsv[i]); + } + } + if(finalLpsImpossible(final_lpsv)){ + return Retval(BooleanCondition::FALSE_CONSTANT); + } + } + + if(next_lpsv.size() > 0){ + if(global_lp){ + for(int i = 0; i < next_lpsv.size(); i++){ + next_lpsv[i] = std::make_shared(global_lp, next_lpsv[i]); + } + } + const bool next_istcx = istcx || (operator_parent == LPOP::NONE); + if(nextLpsImpossible(next_lpsv, final_lpsv, next_istcx)){ + return Retval(BooleanCondition::FALSE_CONSTANT); + } + } + + if(neglps.size() == 0){ + neglps.emplace_back(std::make_shared()); + } + + try { + if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { + return Retval(BooleanCondition::FALSE_CONSTANT); + } + } + catch (std::bad_alloc &e) { + // we are out of memory, deal with it. + 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), + std::make_shared(std::move(neglps))); + }*/ + + Retval Simplifier::simplify_or(const LogicalCondition *element) { + //std::cout << "or\n"; std::vector conditions; std::vector lps, neglpsv; for (const auto &c: element->getOperands()) { @@ -69,11 +557,14 @@ namespace PetriEngine { namespace PQL { if (conditions.size() == 0) { return Retval(BooleanCondition::FALSE_CONSTANT); } - + try { - if (!_context.timeout() && !neglps->satisfiable(_context)) { + //std::cout << "start neg or\n"; + if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { + //std::cout << "neg or is impossible\n"; return Retval(BooleanCondition::TRUE_CONSTANT); } + //std::cout << "neg or possible\n"; } catch (std::bad_alloc &e) { // we are out of memory, deal with it. @@ -83,7 +574,6 @@ 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 - return Retval( makeOr(conditions), std::make_shared(std::move(lps)), @@ -91,7 +581,7 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_and(const LogicalCondition *element) { - + //std::cout << "and\n"; std::vector conditions; std::vector lpsv; std::vector neglps; @@ -116,7 +606,7 @@ namespace PetriEngine { namespace PQL { auto lps = mergeLps(std::move(lpsv)); try { - if (!_context.timeout() && !lps->satisfiable(_context)) { + if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::FALSE_CONSTANT); } } @@ -128,7 +618,6 @@ 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 - return Retval( makeAnd(conditions), std::move(lps), @@ -138,9 +627,9 @@ namespace PetriEngine { namespace PQL { /************ Auxiliary functions for quantifier simplification ***********/ Retval Simplifier::simplify_AG(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -148,9 +637,9 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_AF(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -158,9 +647,9 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_AX(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(std::make_shared()); } else { return Retval(std::make_shared(r.formula)); @@ -168,9 +657,9 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_EG(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -178,9 +667,9 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_EF(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); @@ -188,36 +677,180 @@ namespace PetriEngine { namespace PQL { } Retval Simplifier::simplify_EX(Retval &r) { - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { return Retval(std::make_shared( std::make_shared())); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { return Retval(std::make_shared(r.formula)); } } + /*Retval Simplifier::simplify_global_quantifier(Retval &r) { + //std::cout << "triv true: " << r.formula->isTriviallyTrue() << "\n"; + //std::cout << "triv false: " << r.formula->isTriviallyFalse() << "\n"; + operator_found = LPOP::GLOBAL; + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { + return Retval(BooleanCondition::TRUE_CONSTANT); + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { + 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); - if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context)) { + operator_found = LPOP::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, tcx)) { return Retval(BooleanCondition::TRUE_CONSTANT); - } else if (r.formula->isTriviallyFalse() || !r.lps->satisfiable(_context)) { + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { return Retval(BooleanCondition::FALSE_CONSTANT); } else { - return Retval(std::make_shared(r.formula)); + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + } + } + + bool Simplifier::isNextImpossible(AbstractProgramCollection_ptr next_lps, bool strict){ + std::cout << "is next\n"; + if(strict){ + bool sat = false; + for(auto& lp: next_lps->AllProgs()){ + if(!lp->isNStepsImpossible(1, true, _context)){ + sat = true; + break; + } + } + if(!sat){ + return true; + } + }else{ + if(!next_lps->satisfiable(_context, tcx)){ + return true; + } + } + + return false; + } + + template<> + Retval Simplifier::simplify_simple_quantifier(Retval &r, bool strict){ + operator_found = LPOP::NEXT; + + bool rules_enabled = _context.rules().F_rule && _context.rules().G_rule && _context.rules().X_rule; + if(_context.rules().X_rule){ + r.lps->update_operator(AbstractProgramCollection::operator_t::X); + r.neglps->update_operator(AbstractProgramCollection::operator_t::X); + } + + if (r.formula->isTriviallyTrue() || ((!tcx.has_prefix() || !rules_enabled) && !r.neglps->satisfiable(_context, tcx))) { + //if(_context.negated()){ + // return Retval(BooleanCondition::FALSE_CONSTANT); + //}else{ + return Retval(BooleanCondition::TRUE_CONSTANT); + //} + } else if (r.formula->isTriviallyFalse() || ((!tcx.has_prefix() || !rules_enabled) && (false && !r.lps->satisfiable(_context, tcx)))) { + //if(_context.negated()){ + // return Retval(BooleanCondition::TRUE_CONSTANT); + //}else{ + return Retval(BooleanCondition::FALSE_CONSTANT); + //} + } + if(_context.rules().X_rule){ + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + }else{ + return Retval(std::make_shared(r.formula)); + } + } + + template<> + Retval Simplifier::simplify_simple_quantifier(Retval &r){ + //std::cout << "global\n"; + operator_found = LPOP::GLOBAL; + bool rules_enabled = _context.rules().F_rule && _context.rules().G_rule && _context.rules().X_rule; + if(_context.rules().F_rule && _context.rules().G_rule){ + r.lps->update_operator(AbstractProgramCollection::operator_t::G); + r.neglps->update_operator(AbstractProgramCollection::operator_t::F); + } + + if (r.formula->isTriviallyTrue() || ((!tcx.has_prefix() || !rules_enabled) && !r.neglps->satisfiable(_context, tcx))) { + //if(_context.negated()){ + // return Retval(BooleanCondition::FALSE_CONSTANT); + //}else{ + return Retval(BooleanCondition::TRUE_CONSTANT); + //} + } else if (r.formula->isTriviallyFalse() || (false && !r.lps->satisfiable(_context, tcx))) { + //if(_context.negated()){ + // return Retval(BooleanCondition::TRUE_CONSTANT); + //}else{ + return Retval(BooleanCondition::FALSE_CONSTANT); + //} + } else { + if(_context.rules().F_rule && _context.rules().G_rule){ + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + }else{ + return Retval(std::make_shared(r.formula)); + } + } + } + + template<> + Retval Simplifier::simplify_simple_quantifier(Retval &r){ + operator_found = LPOP::FINAL; + //std::cout << "final\n"; + bool rules_enabled = _context.rules().F_rule && _context.rules().G_rule && _context.rules().X_rule; + if(_context.rules().F_rule && _context.rules().G_rule){ + r.lps->update_operator(AbstractProgramCollection::operator_t::F); + r.neglps->update_operator(AbstractProgramCollection::operator_t::G); + } + + if (r.formula->isTriviallyTrue() || !r.neglps->satisfiable(_context, tcx)) { + // if(_context.negated()){ + // return Retval(BooleanCondition::FALSE_CONSTANT); + // }else{ + return Retval(BooleanCondition::TRUE_CONSTANT); + // } + } else if (r.formula->isTriviallyFalse() || ((!tcx.has_prefix() || !rules_enabled) && (false && !r.lps->satisfiable(_context, tcx)))) { + // if(_context.negated()){ + // return Retval(BooleanCondition::TRUE_CONSTANT); + //}else{ + return Retval(BooleanCondition::FALSE_CONSTANT); + //} + } else { + if(_context.rules().F_rule && _context.rules().G_rule){ + return Retval(std::make_shared(r.formula), r.lps, r.neglps); + }else{ + return Retval(std::make_shared(r.formula)); + } } } + Member memberForPathPlace(size_t p, int cur_path, const SimplificationContext &context) { + std::vector row(( context.net()->numberOfTransitions() + context.net()->numberOfPlaces() ) * context.numPaths(), 0); + row.shrink_to_fit(); + int variable_offset = cur_path * ( context.net()->numberOfTransitions() + context.net()->numberOfPlaces() ); + for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) { + row[t + variable_offset] = context.net()->outArc(t, p); + row[t + variable_offset] -= context.net()->inArc(p, t); + } + row[context.net()->numberOfTransitions() + variable_offset + p] = 1.0; + return Member(std::move(row), 0); + } + Member memberForPlace(size_t p, const SimplificationContext &context) { - std::vector row(context.net()->numberOfTransitions(), 0); + 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); } - return Member(std::move(row), context.marking()[p]); + row[context.net()->numberOfTransitions() + p] = 1.0; + return Member(std::move(row), 0); } /********** Constraint Visitor **********/ @@ -236,8 +869,8 @@ namespace PetriEngine { namespace PQL { } for (auto &i: element->places()) { - if (first) res = memberForPlace(i.first, _context); - else op(res, memberForPlace(i.first, _context)); + if (first) res = memberForPathPlace(i.first, _current_path, _context); + else op(res, memberForPathPlace(i.first, _current_path, _context)); first = false; } @@ -255,7 +888,7 @@ namespace PetriEngine { namespace PQL { } void ConstraintVisitor::_accept(const UnfoldedIdentifierExpr *element) { - _return_value = memberForPlace(element->offset(), _context); + _return_value = memberForPathPlace(element->offset(), _current_path, _context); } void ConstraintVisitor::_accept(const PlusExpr *element) { @@ -291,15 +924,19 @@ namespace PetriEngine { namespace PQL { } void ConstraintVisitor::_accept(const PathSelectExpr *element) { - if(element->offset() != 0) + if(element->offset() >= _context.numPaths()) _return_value = Member(0, false); - else + else{ + _current_path = element->offset(); Visitor::visit(*this, element->child()); + _current_path = 0; + } } /******* Simplifier accepts ********/ void Simplifier::_accept(const NotCondition *element) { + //std::cout << "negating\n"; _context.negate(); Visitor::visit(this, element->getCond()); _context.negate(); @@ -362,9 +999,9 @@ namespace PetriEngine { namespace PQL { neglps = std::make_shared(); } - if (!_context.timeout() && !lps->satisfiable(_context)) { + if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::FALSE_CONSTANT)) - } else if (!_context.timeout() && !neglps->satisfiable(_context)) { + } else if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::TRUE_CONSTANT)) } else { if (_context.negated()) { @@ -406,9 +1043,9 @@ namespace PetriEngine { namespace PQL { assert(lps); assert(neglps); - if (!_context.timeout() && !neglps->satisfiable(_context)) { + if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (!_context.timeout() && !lps->satisfiable(_context)) { + } else if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::FALSE_CONSTANT)) } else { if (_context.negated()) { @@ -449,9 +1086,9 @@ namespace PetriEngine { namespace PQL { neglps = std::make_shared(); } - if (!_context.timeout() && !lps->satisfiable(_context)) { + if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::FALSE_CONSTANT)) - } else if (!_context.timeout() && !neglps->satisfiable(_context)) { + } else if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::TRUE_CONSTANT)) } else { if (_context.negated()) { @@ -492,9 +1129,9 @@ namespace PetriEngine { namespace PQL { lps = std::make_shared(); neglps = std::make_shared(); } - if (!_context.timeout() && !lps->satisfiable(_context)) { + if (!_context.timeout() && !lps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::FALSE_CONSTANT)) - } else if (!_context.timeout() && !neglps->satisfiable(_context)) { + } else if (!_context.timeout() && !neglps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::TRUE_CONSTANT)) } else { if (_context.negated()) { @@ -516,6 +1153,13 @@ namespace PetriEngine { namespace PQL { } void Simplifier::_accept(const CompareConjunction *element) { + // this case is unclear to me in the hyperltl construction + //std::cout << "compare conjunction\n"; + assert(_context.numPaths() == 1); + if(_context.numPaths() != 1){ + std::cerr << "CompareConjunction simplification for HyperLTL is not implemented \n"; + RETURN(Retval(std::make_shared(*element, _context.negated()))) + } if (_context.timeout()) { RETURN(Retval(std::make_shared(*element, _context.negated()))) } @@ -584,7 +1228,7 @@ namespace PetriEngine { namespace PQL { } try { - if (!_context.timeout() && lps && !lps->satisfiable(_context)) { + if (!_context.timeout() && lps && !lps->satisfiable(_context, tcx)) { RETURN(Retval(BooleanCondition::getShared(neg))) } } @@ -607,7 +1251,7 @@ namespace PetriEngine { namespace PQL { if (c._upper != std::numeric_limits::max()) ++cnt; for (size_t j = 0; j < cnt; ++j) { assert(ncnt >= 0); - if (!neglps[ncnt]->satisfiable(_context)) { + if (!neglps[ncnt]->satisfiable(_context, tcx)) { if (j == 1 || c._upper == std::numeric_limits::max()) c._lower = 0; else if (j == 0) @@ -749,12 +1393,12 @@ namespace PetriEngine { namespace PQL { _context.setNegate(false); Visitor::visit(this, (*condition)[1]); Retval r2 = std::move(_return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context)) { + if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context, tcx)) { _context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context)) { + } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context, tcx)) { _context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : @@ -765,19 +1409,19 @@ namespace PetriEngine { namespace PQL { _context.setNegate(neg); if (_context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared(r2.formula))) } else { RETURN(Retval(std::make_shared( std::make_shared(r1.formula, r2.formula)))) } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { RETURN(std::move(r2)) } else { RETURN(Retval(std::make_shared(r1.formula, r2.formula))) @@ -791,12 +1435,12 @@ namespace PetriEngine { namespace PQL { _context.setNegate(false); Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(_return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context)) { + if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context, tcx)) { _context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context)) { + } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context, tcx)) { _context.setNegate(neg); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : @@ -808,19 +1452,19 @@ namespace PetriEngine { namespace PQL { _context.setNegate(neg); if (_context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared(r2.formula))) } else { RETURN(Retval(std::make_shared( std::make_shared(r1.formula, r2.formula)))) } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { RETURN(std::move(r2)) } else { RETURN(Retval(std::make_shared(r1.formula, r2.formula))) @@ -828,45 +1472,121 @@ namespace PetriEngine { namespace PQL { } } + + /* creates the LP overapproximation for the negation of phi U psi (the release), + which is G(!psi) or F(!psi and !phi) */ + AbstractProgramCollection_ptr negated_until_overapproximation(Retval& r_phi, Retval& r_psi){ + auto npsi = r_psi.neglps->clone(); + auto nphi = r_phi.neglps->clone(); + auto conj = std::make_shared(npsi, nphi); + conj->update_operator(AbstractProgramCollection::operator_t::F); + auto npsi_2 = r_psi.neglps->clone(); + npsi_2->update_operator(AbstractProgramCollection::operator_t::G); + + std::vector members; + members.push_back(conj); + members.push_back(npsi); + + return std::make_shared(std::move(members)); + } + void Simplifier::_accept(const UntilCondition *condition) { bool neg = _context.negated(); + bool rules_enabled = _context.rules().F_rule && _context.rules().G_rule && _context.rules().X_rule; _context.setNegate(false); - + operators++; + operator_parent = LPOP::OTHER; + // TODO: set allow_basic_only here and disable once othe rules are implemented + auto pre = tcx.clear_context(); + tcx.push_prefix(AbstractProgramCollection::operator_t::F, _context.negated()); + Visitor::visit(this, condition->getCond2()); Retval r2 = std::move(_return_value); - if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context)) { + if (r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(_context, tcx)) { + //std::cout << "r2 trivial true\n"; _context.setNegate(neg); + tcx.set_prefix(pre); RETURN(neg ? Retval(BooleanCondition::FALSE_CONSTANT) : Retval(BooleanCondition::TRUE_CONSTANT)) - } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context)) { + } else if (r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(_context, tcx)) { + //std::cout << "r2 trivial false\n"; _context.setNegate(neg); + tcx.set_prefix(pre); RETURN(neg ? Retval(BooleanCondition::TRUE_CONSTANT) : Retval(BooleanCondition::FALSE_CONSTANT)) } + //std::cout << "no trivial r2\n"; + operator_parent = LPOP::OTHER; Visitor::visit(this, condition->getCond1()); + Retval r1 = std::move(_return_value); _context.setNegate(neg); + tcx.set_prefix(pre); + tcx.push_prefix(AbstractProgramCollection::operator_t::F, _context.negated()); if (_context.negated()) { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { - RETURN(Retval(std::make_shared( + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { + //std::cout << "r1 trivial true neg\n"; + tcx.set_prefix(pre); + if(rules_enabled){ + r2.lps->update_operator(AbstractProgramCollection::operator_t::F); + r2.neglps->update_operator(AbstractProgramCollection::operator_t::G); + RETURN(Retval(std::make_shared( + std::make_shared(r2.formula)), r2.neglps, r2.lps)) + }else{ + RETURN(Retval(std::make_shared( std::make_shared(r2.formula)))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { - RETURN(Retval(std::make_shared(r2.formula))) + } + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { + //std::cout << "r1 trivial false neg\n"; + tcx.set_prefix(pre); + if(rules_enabled){ + RETURN(Retval(std::make_shared(r2.formula), r2.neglps, r2.lps)) + }else{ + RETURN(Retval(std::make_shared(r2.formula))) + } } else { - RETURN(Retval(std::make_shared( - std::make_shared(r1.formula, r2.formula)))) + tcx.set_prefix(pre); + if(rules_enabled){ + r2.lps->update_operator(AbstractProgramCollection::operator_t::F); + + r2.neglps = negated_until_overapproximation(r1,r2); + operator_parent = LPOP::UNTIL; + RETURN(Retval(std::make_shared( + std::make_shared(r1.formula, r2.formula)), r2.neglps, r2.lps)) + }else{ + RETURN(Retval(std::make_shared( + std::make_shared(r1.formula, r2.formula)))) + } } } else { - if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context)) { - RETURN(Retval(std::make_shared(r2.formula))) - } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context)) { + if (r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(_context, tcx)) { + //std::cout << "r1 trivial true\n"; + tcx.set_prefix(pre); + if(rules_enabled){ + r2.lps->update_operator(AbstractProgramCollection::operator_t::F); + r2.neglps->update_operator(AbstractProgramCollection::operator_t::G); + RETURN(Retval(std::make_shared(r2.formula), r2.lps, r2.neglps)) + }else{ + RETURN(Retval(std::make_shared(r2.formula))) + } + } else if (r1.formula->isTriviallyFalse() || !r1.lps->satisfiable(_context, tcx)) { + //std::cout << "r1 trivial false\n"; + tcx.set_prefix(pre); RETURN(std::move(r2)) } else { - RETURN(Retval(std::make_shared(r1.formula, r2.formula))) + tcx.set_prefix(pre); + if(rules_enabled){ + r2.lps->update_operator(AbstractProgramCollection::operator_t::F); + r2.neglps = negated_until_overapproximation(r1,r2); + operator_parent = LPOP::UNTIL; + RETURN(Retval(std::make_shared(r1.formula, r2.formula), r2.lps, r2.neglps)) + }else{ + RETURN(Retval(std::make_shared(r1.formula, r2.formula))) + } } } } @@ -895,20 +1615,61 @@ namespace PetriEngine { namespace PQL { } void Simplifier::_accept(const FCondition *condition) { + //std::cout << "accept final\n"; + operators++; + if(_context.negated()){ + operator_parent = LPOP::GLOBAL; + }else{ + operator_parent = LPOP::FINAL; + } + op_parent_negated = _context.negated(); + auto pre = tcx.push_prefix(AbstractProgramCollection::operator_t::F, _context.negated()); Visitor::visit(this, condition->getCond()); - RETURN(_context.negated() ? simplify_simple_quantifier(_return_value) - : simplify_simple_quantifier(_return_value)) + tcx.set_prefix(pre); + if(_context.negated()){ + //std::cout << "negated GCondition\n"; + auto r = simplify_simple_quantifier(_return_value); + RETURN(std::move(r)); + }else{ + //std::cout << "FCondition\n"; + RETURN(simplify_simple_quantifier(_return_value)); + } } void Simplifier::_accept(const GCondition *condition) { + operators++; + //std::cout << "accept global\n"; + if(_context.negated()){ + operator_parent = LPOP::FINAL; + }else{ + operator_parent = LPOP::GLOBAL; + } + op_parent_negated = _context.negated(); + auto pre = tcx.push_prefix(AbstractProgramCollection::operator_t::G, _context.negated()); + Visitor::visit(this, condition->getCond()); - RETURN(_context.negated() ? simplify_simple_quantifier(_return_value) - : simplify_simple_quantifier(_return_value)) + + tcx.set_prefix(pre); + 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); + RETURN(std::move(r)) + } } void Simplifier::_accept(const XCondition *condition) { + operators++; + //std::cout << "X accept\n"; + operator_parent = LPOP::NEXT; + int32_t pre_operators = operators; + auto pre = tcx.push_prefix(AbstractProgramCollection::operator_t::X, _context.negated()); Visitor::visit(this, condition->getCond()); - RETURN(simplify_simple_quantifier(_return_value)) + tcx.set_prefix(pre); + const bool is_strict_next = (operator_parent = LPOP::NONE) && (operators == pre_operators) && (!_context.isDeadlocked()); + RETURN(simplify_simple_quantifier(_return_value, is_strict_next)) } void Simplifier::_accept(const BooleanCondition *condition) { diff --git a/src/PetriEngine/Simplification/LinearProgram.cpp b/src/PetriEngine/Simplification/LinearProgram.cpp index 5733e549d..d11fb6b08 100644 --- a/src/PetriEngine/Simplification/LinearProgram.cpp +++ b/src/PetriEngine/Simplification/LinearProgram.cpp @@ -46,79 +46,157 @@ namespace PetriEngine { constexpr auto infty = std::numeric_limits::infinity(); - bool LinearProgram::isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime) { - bool use_ilp = true; - auto net = context.net(); + std::string bound_or_inf(double bound){ + std::string inf = "inf"; + std::string ninf = "ninf"; + return (std::fabs(bound) != infty)? std::to_string(bound) : ((bound > 0)? inf : ninf); + } - if (_result != result_t::UKNOWN) - { - if (_result == result_t::IMPOSSIBLE) - return _result == result_t::IMPOSSIBLE; + std::string lp_variable_name(int32_t var_idx, const PQL::SimplificationContext& context){ + //std::cout << "(v:" << var_idx << ")"; + const uint32_t paths = context.numPaths(); + const uint32_t transitions = context.net()->numberOfTransitions(); + const uint32_t places = context.net()->numberOfPlaces(); + const uint32_t variables = context.getNumBaseVariables(); + std::stringstream ss; + + const uint32_t v = var_idx % variables; + + if(paths > 1){ + uint32_t trace = v / (places + transitions); + ss << "t" << trace << "."; } - if (_equations.size() == 0 || context.timeout()){ - return false; + const uint32_t v_path = var_idx % (places + transitions); + + if(v_path < transitions){ + if(context.getPrintLevel() < 2){ + ss << "X" << (v_path); + }else{ + ss << *context.net()->transitionNames()[v_path].get(); + } + } + else{ + if(context.getPrintLevel() < 2){ + ss << "M" << (v_path - transitions); + }else{ + ss << *context.net()->placeNames()[v_path - transitions].get(); + } } - if (context.markingOutOfBounds()) { // the initial marking has too many tokens that exceed the int32_t limits - return false; + if(var_idx >= variables){ + ss << "_" << (var_idx / variables); } - const uint32_t nCol = net->numberOfTransitions(); - const uint32_t nRow = net->numberOfPlaces() + _equations.size(); + return ss.str(); + } - 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; + void printConstraints(const PQL::SimplificationContext& context, glp_prob* lp){ + + if(context.getPrintLevel() < 1) + return; - auto lp = context.makeBaseLP(); - if (lp == nullptr) - return false; + 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; - 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 true; - } - glp_set_row_bnds(lp, rowno, GLP_DB, eq.lower, eq.upper); + 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 << " + "; + const auto var_name = lp_variable_name(indices[j] - 1, context); + if(coef[j] != 1){ + std::cout << coef[j] << "*" << var_name; + }else{ + std::cout << var_name; } + first_print = false; } - 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()) + 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"; + } + + } + + bool LinearProgram::_writeEquationsImpl(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, bool allocate, int32_t variable_shift) + { + if(allocate) + glp_add_rows(lp, equations.size()); + for (const auto& eq : equations) { + auto l = eq.row->write_indir_shifted(row, indir, variable_shift); + 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 { - // std::cerr << "glpk: construction timeout" << std::endl; - glp_delete_prob(lp); - return false; + if (eq.lower > eq.upper) + { + 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; - // Set objective, kind and bounds - for (size_t i = 1; i <= nCol; 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); + if (context.timeout()) + { + return false; } + } + return false; + } + bool LinearProgram::pushEquations(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations){ + return _writeEquationsImpl(lp, context, rowno, row, indir, equations, true, 0); + } + bool LinearProgram::pushEquationsShifted(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, int32_t variable_shift){ + return _writeEquationsImpl(lp, context, rowno, row, indir, equations, true, variable_shift); + } - // Minimize the objective + bool LinearProgram::emplaceEquations(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations){ + return _writeEquationsImpl(lp, context, rowno, row, indir, equations, false, 0); + } + bool LinearProgram::emplaceEquationsShifted(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector& row, std::vector& indir, const std::vector& equations, int32_t variable_shift){ + return _writeEquationsImpl(lp, context, rowno, row, indir, equations, false, variable_shift); + } + + LinearProgram::result_t LinearProgram::solve_built_lp(glp_prob* lp, const PQL::SimplificationContext& context, uint32_t solvetime, bool delete_lp){ glp_set_obj_dir(lp, GLP_MIN); auto stime = glp_time(); glp_smcp settings; @@ -128,10 +206,12 @@ namespace PetriEngine { settings.presolve = GLP_OFF; settings.msg_lev = 0; auto result = glp_simplex(lp, &settings); + + result_t final_result = result_t::UKNOWN; + if (result == GLP_ETMLIM) { - _result = result_t::UKNOWN; - // std::cerr << "glpk: timeout" << std::endl; + final_result = result_t::UKNOWN; } else if (result == 0) { @@ -146,41 +226,724 @@ namespace PetriEngine { auto ires = glp_intopt(lp, &iset); if (ires == GLP_ETMLIM) { - _result = result_t::UKNOWN; - // std::cerr << "glpk mip: timeout" << std::endl; + final_result = result_t::UKNOWN; } else if (ires == 0) { auto ist = glp_mip_status(lp); if (ist == GLP_OPT || ist == GLP_FEAS || ist == GLP_UNBND) { - _result = result_t::POSSIBLE; + final_result = result_t::POSSIBLE; } else { - _result = result_t::IMPOSSIBLE; + final_result = result_t::IMPOSSIBLE; } } } else if (status == GLP_FEAS || status == GLP_UNBND) { - _result = result_t::POSSIBLE; + final_result = result_t::POSSIBLE; } else { - _result = result_t::IMPOSSIBLE; + final_result = result_t::IMPOSSIBLE; } } else if (result == GLP_ENOPFS || result == GLP_ENODFS || result == GLP_ENOFEAS) { - _result = result_t::IMPOSSIBLE; + final_result = result_t::IMPOSSIBLE; + } + + if(delete_lp){ + glp_delete_prob(lp); + } + + return final_result; + } + + LinearProgram::result_t LinearProgram::solve_and_set(glp_prob* lp, const PQL::SimplificationContext& context, uint32_t solvetime, bool delete_lp){ + auto res = solve_built_lp(lp, context, solvetime, delete_lp); + _result = res; + return res; + } + 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) + return _result == result_t::IMPOSSIBLE; + } + + 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 = context.getNumBaseVariables(); + const uint32_t nRow = context.getNumBaseConstraints() + _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 + context.getNumBaseConstraints(); + + if(pushEquations(lp, context, rowno, row, indir, _equations)){glp_delete_prob(lp);_result = result_t::IMPOSSIBLE;return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + + // Set objective, kind and bounds + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t i = 1; i <= net->numberOfTransitions(); i++) { + const int var = i + variable_offset; + glp_set_obj_coef(lp, var, 1); + glp_set_col_kind(lp, var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, var, GLP_LO, 0, infty); + } + } + + printConstraints(context, lp); + + return solve_and_set(lp, context, solvetime, true) == result_t::IMPOSSIBLE; + } + + bool LinearProgram::isFinalImpossibleWith(const LinearProgram* withLp, bool is_next, bool is_strict, const PQL::SimplificationContext& context, uint32_t solvetime) const{ + bool use_ilp = true; + auto net = context.net(); + + if (_equations.size() == 0 || withLp->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 = 2 * context.getNumBaseVariables(); + const uint32_t nRow = 2 * context.getNumBaseConstraints() + _equations.size() + withLp->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 + context.getNumBaseConstraints(); + if(pushEquations(lp, context, rowno, row, indir, _equations)){glp_delete_prob(lp);return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + + // Set objective, kind and bounds + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t i = 1; i <= net->numberOfTransitions(); i++) { + const int var = i + variable_offset; + glp_set_obj_coef(lp, var, 1); + glp_set_col_kind(lp, var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, var, GLP_LO, 0, infty); + } + } + + const int shift = context.getNumBaseVariables(); + glp_add_cols(lp, shift); + + // transition variable copies + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t i = 1; i <= net->numberOfTransitions(); i++) { + const int var = i + variable_offset; + glp_set_obj_coef(lp, var + shift, 1); + glp_set_col_kind(lp, var + shift, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, var + shift, GLP_LO, 0, infty); + } + } + + std::vector ind(2); + std::vector sub = {0, -1.0}; + // 'next marking' variables + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + const int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + const int constraint_offset = path * (net->numberOfPlaces()); + for(size_t p = 1; p <= net->numberOfPlaces(); p++){ + const int colno = p + net->numberOfTransitions() + variable_offset + shift; + + glp_set_obj_coef(lp, colno, 0); + glp_set_col_kind(lp, colno, use_ilp? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, colno, GLP_LO, 0, infty); + + // change the base-constraints to include variables for 'next marking' + // this adds the coefficient 1 to the p-th row, which is the base-constraint for place p + ind[1] = p + constraint_offset; + glp_set_mat_col(lp, colno, 1, ind.data(), sub.data()); + glp_set_row_bnds(lp, p + constraint_offset, GLP_FX, 0, 0); + } + } + + // copy translated version of base + glp_add_rows(lp, context.getNumBaseConstraints()); + for(size_t p = 1; p <= context.getNumBaseConstraints(); p++){ + int l = glp_get_mat_row(lp, p, indir.data(), row.data()); + for (int i = l; i >= 1; --i){ + // shift only old variables + if(indir[i] <= shift){ + indir[i] += shift; + }else{ + // from above the base contains some new variables we don't want to copy + std::swap(indir[i], indir[l]); + std::swap(row[i], row[l]); + l--; + } + } + glp_set_mat_row(lp, rowno, l, indir.data(), row.data()); + glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + rowno++; + } + // add second lp equations + if(pushEquationsShifted(lp, context, rowno, row, indir, withLp->equations(), shift)){glp_delete_prob(lp);return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + + if(is_next){ + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + glp_add_rows(lp, 1); + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for(size_t t = 1; t <= net->numberOfTransitions(); t++){ + indir[t] = t + variable_offset; + row[t] = 1.0; + } + glp_set_mat_row(lp, rowno, net->numberOfTransitions(), indir.data(), row.data()); + if(is_strict){ + glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); + }else{ + glp_set_row_bnds(lp, rowno, GLP_UP, -infty, 1.0); + } + ++rowno; + } + } + + printConstraints(context, lp); + + return solve_built_lp(lp, context, solvetime, true) == result_t::IMPOSSIBLE; + } + + bool LinearProgram::isFinalImpossibleWithN(const std::vector& permutation, const std::vector& lps, bool is_next, bool is_strict, const PQL::SimplificationContext& context, uint32_t solvetime) const{ + bool use_ilp = true; + auto net = context.net(); + + if (_equations.size() == 0 || lps.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 num_lps = lps.size() + 1; + uint32_t lp_equations = _equations.size(); + for(int i = 0; i < lps.size(); i++){ + if(lps[i]->size() == 0) + return false; + lp_equations += lps[i]->size(); + } + + const uint32_t nCol = num_lps * context.getNumBaseVariables(); + const uint32_t nRow = num_lps * context.getNumBaseConstraints() + lp_equations; + + 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; + // skip over first base + int rowno = 1 + context.getNumBaseConstraints(); + std::vector ind(2); + std::vector sub = {0, -1.0}; + + glp_add_cols(lp, context.getNumBaseVariables() * (lps.size() - 1)); + for(int perm_idx = 0; perm_idx < permutation.size(); perm_idx++){ + uint32_t lp_idx = permutation[perm_idx]; + const int variable_shift = perm_idx * context.getNumBaseVariables(); + if(perm_idx != 0){ + // copy base & add next marking variables + { + glp_add_rows(lp, context.getNumBaseConstraints()); + for(size_t p = 1; p <= context.getNumBaseConstraints(); p++){ + int l = glp_get_mat_row(lp, p, indir.data(), row.data()); + for (int i = 1; i <= l; i++){ + indir[i] += variable_shift; + } + // add variable for the next base to meet on, which last does not have + if(perm_idx != permutation.size() - 1){ + const int next_variable_shift = (perm_idx + 1) * context.getNumBaseVariables(); + const int transition_skip = (1 + (p-1) / net->numberOfPlaces()) * net->numberOfTransitions(); + const int next_var_col = p + transition_skip + next_variable_shift; + + indir[l+1] = next_var_col; + row[l+1] = -1; + l++; + } + glp_set_mat_row(lp, rowno, l, indir.data(), row.data()); + // set the next base variable equal to transitions fired in last marking + if(perm_idx != permutation.size() - 1){ + glp_set_row_bnds(lp, rowno, GLP_FX, 0, 0); + }else{ + glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + } + rowno++; + // set kind, bounds, coef of next marking variables + /*glp_set_obj_coef(lp, p + variable_shift, 0); + glp_set_col_kind(lp, p + variable_shift, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, p + variable_shift, GLP_LO, 0, infty);*/ + } + } + } + // add equations + if(pushEquationsShifted(lp, context, rowno, row, indir, lps[lp_idx]->equations(), variable_shift)){glp_delete_prob(lp);return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + + // Set objective, kind and bounds + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int path_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t t = 1; t <= net->numberOfTransitions(); t++) { + const int transition_var = t + path_offset + variable_shift; + glp_set_obj_coef(lp, transition_var, 1); + glp_set_col_kind(lp, transition_var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, transition_var, GLP_LO, 0, infty); + } + /* first base place variables already set by buildbase() */ + if(perm_idx != 0){ + for (size_t p = 1; p <= net->numberOfPlaces(); p++) { + const int place_var = p + net->numberOfTransitions() + path_offset + variable_shift; + glp_set_obj_coef(lp, place_var, 0); + glp_set_col_kind(lp, place_var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, place_var, GLP_LO, 0, infty); + } + } + } + } + + for(size_t p = 1; p <= context.getNumBaseConstraints(); p++){ + int l = glp_get_mat_row(lp, p, indir.data(), row.data()); + + // add variable for the next base to meet on, which last does not have + const int first_base_shift = context.getNumBaseVariables(); + const int transition_skip = (1 + (p-1) / net->numberOfPlaces()) * net->numberOfTransitions(); + const int first_var_col = p + transition_skip + first_base_shift; + + indir[l+1] = first_var_col; + row[l+1] = -1.0; + l++; + + glp_set_mat_row(lp, p, l, indir.data(), row.data()); + // sets the first (next) base variable equal to transitions fired in first marking + glp_set_row_bnds(lp, p, GLP_FX, 0, 0); + } + + if(is_next){ + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + glp_add_rows(lp, 1); + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for(size_t t = 1; t <= net->numberOfTransitions(); t++){ + indir[t] = t + variable_offset; + row[t] = 1.0; + } + glp_set_mat_row(lp, rowno, net->numberOfTransitions(), indir.data(), row.data()); + if(is_strict){ + glp_set_row_bnds(lp, rowno, GLP_FX, 1.0, 1.0); + }else{ + glp_set_row_bnds(lp, rowno, GLP_UP, -infty, 1.0); + } + ++rowno; + } + } + + printConstraints(context, lp); + + return solve_built_lp(lp, context, solvetime, true) == result_t::IMPOSSIBLE; + } + + // allocates all needed memory and sets variable bounds + // copies base constraints to use when cleaning the lp + std::pair, std::vector>>> prepare_lp(std::vector& lps, const PQL::SimplificationContext& context){ + bool use_ilp = true; + glp_prob* lp = context.makeBaseLP(); + std::vector, std::vector>> base; + if(!lp) + return std::make_pair(nullptr, base); + + for(int i = 1; i <= context.getNumBaseConstraints(); i++){ + std::vector indir(context.getNumBaseVariables()); + std::vector row(context.getNumBaseVariables()); + + int l = glp_get_mat_row(lp, i, indir.data(), row.data()); + + indir.resize(l+1); + indir.shrink_to_fit(); + row.resize(l+1); + row.shrink_to_fit(); + + base.emplace_back(std::make_pair(std::move(indir), std::move(row))); + } + + auto net = context.net(); + + int total_equations = 0; + for(auto& prog: lps){ + total_equations += prog->equations().size(); + } + + int total_rows = context.getNumBaseConstraints() * lps.size() + total_equations; + int total_cols = context.getNumBaseVariables() * lps.size(); + + // already contains one copy of rows/cols from makeBaseLp + glp_add_rows(lp, total_rows - context.getNumBaseConstraints()); + glp_add_cols(lp, total_cols - context.getNumBaseVariables()); + + int colno = 1; + // variables: |T| transition variables, followed by |P| place variables, repeated for each path, for each lp in lps + for(int i = 0; i < lps.size(); i++){ + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + // transition variables + for (size_t t = 1; t <= net->numberOfTransitions(); t++) { + glp_set_obj_coef(lp, colno, 1); + glp_set_col_kind(lp, colno, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, colno, GLP_LO, 0, infty); + colno++; + } + // place variables + // for the first lp, these are set by makeBaseLP() and are fixed to the initial marking + if(i > 0){ + for(size_t p = 1; p <= net->numberOfPlaces(); p++){ + glp_set_obj_coef(lp, colno, 0); + glp_set_col_kind(lp, colno, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, colno, GLP_LO, 0, infty); + colno++; + } + }else{ + colno += net->numberOfPlaces(); + } + } + } + + return std::make_pair(lp, base); + } + + void clean_lp(glp_prob* lp, std::vector, std::vector>>& base, const PQL::SimplificationContext& context){ + glp_std_basis(lp); + + // remove auxilliary variable added to every base constraint + for(int i = 1; i <= context.getNumBaseConstraints(); i++){ + auto& [indir, row] = base[i-1]; + glp_set_mat_row(lp, i, static_cast(indir.size() - 1), indir.data(), row.data()); + } + } + + bool advance_permutations(std::vector>& perms){ + for(int i = 0; i < perms.size(); i++){ + bool more = std::next_permutation(perms[i].begin(), perms[i].end()); + if(more){ + return true; + } + } + return false; + } + + void write_order(std::vector& order, std::vector>& perms, std::vector& starts){ + for(int i = 0; i < perms.size(); i++){ + for(int j = 0; j < perms[i].size(); j++){ + order[starts[i] + j] = perms[i][j]; + } + } + } + + bool permutationsOverLimit(std::vector>& perms, const PQL::SimplificationContext& context){ + uint64_t total = 1; + for(int i = 0; i < perms.size(); i++){ + if(perms[i].size() > 10){ + return true; + } + uint64_t fact = 1; + for(uint64_t j = 2; j <= perms[i].size(); j++) + fact *= j; + + total *= fact; + if(total > context.getPermutationLimit()) + return true; + } + return false; + } + + bool LinearProgram::solveFinalConjunctionImpossible(std::vector& lps, std::vector>& perms, std::vector& starts,const PQL::SimplificationContext& context, uint32_t solvetime){ + if (lps.size() == 0 || context.timeout()){ + return false; + } + + if (context.markingOutOfBounds()) { // the initial marking has too many tokens that exceed the int32_t limits + return false; + } + + for(auto prog : lps){ + if(prog->size() == 0){ + return false; + } + } + + if(permutationsOverLimit(perms, context)){ + return false; + } + + bool sat = false; + int lps_solved = 0; + + auto [lp, base] = prepare_lp(lps, context); + if(!lp) + return false; + + std::vector order; + for(int i = 0; i < lps.size();i++){ + order.push_back(i); + } + + do{ + //glp_prob* lp = context.makeBaseLP(); + std::vector ind_(glp_get_num_cols(lp)); + int l = glp_get_mat_row(lp, 1, ind_.data(), nullptr); + + write_order(order, perms, starts); + + + /*std::cout << "order : "; + for(int i = 0; i < order.size(); i++){ + std::cout << order[i] << ","; + } + std::cout << "\n";*/ + + lps_solved += 1; + if(!isFinalPermutationImpossible(lp, order, lps, context, solvetime)){ + //std::cout << "possible!\n"; + sat = true; + break; + } + + if(context.timeout()){ + sat = true; + break; + } + + l = glp_get_mat_row(lp, 1, ind_.data(), nullptr); + //std::cout << "impossible!\n"; + clean_lp(lp, base, context); + }while(advance_permutations(perms)); glp_delete_prob(lp); + //std::cout << "lps solved: " << lps_solved << "\n"; + return !sat; + } + + bool LinearProgram::isFinalPermutationImpossible(glp_prob* lp, const std::vector& permutation, const std::vector& lps,const PQL::SimplificationContext& context, uint32_t solvetime){ + bool use_ilp = true; + auto net = context.net(); + + if (context.timeout()){ + return false; + } + + int offset = 0; + + const uint32_t num_lps = lps.size() + offset; + + const uint32_t nCol = glp_get_num_cols(lp); + const uint32_t nRow = glp_get_num_rows(lp); + + 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; + + // skip over first base + int rowno = 1 + context.getNumBaseConstraints(); + /*if(freelp){ + if(emplaceEquations(lp, context, rowno, row, indir, freelp->equations())){glp_delete_prob(lp);return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int path_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t t = 1; t <= net->numberOfTransitions(); t++) { + const int transition_var = t + path_offset; + glp_set_obj_coef(lp, transition_var, 1); + glp_set_col_kind(lp, transition_var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, transition_var, GLP_LO, 0, infty); + } + } + }*/ + std::vector ind(2); + std::vector sub = {0, -1.0}; + + //glp_add_cols(lp, context.getNumBaseVariables() * (lps.size() + offset - 1)); + for(int perm_idx = 0; perm_idx < permutation.size(); perm_idx++){ + //std::cout << "perm idx " << perm_idx << "\n"; + uint32_t lp_idx = permutation[perm_idx]; + const int variable_shift = (perm_idx) * context.getNumBaseVariables(); + if(perm_idx != 0){ + // copy base and add next marking variables + { + //glp_add_rows(lp, context.getNumBaseConstraints()); + for(size_t p = 1; p <= context.getNumBaseConstraints(); p++){ + int l = glp_get_mat_row(lp, p, indir.data(), row.data()); + for (int i = 1; i <= l; i++){ + indir[i] += variable_shift; + } + // add variable for the next base to meet on, which last does not have + if(perm_idx != permutation.size() - 1){ + const int next_variable_shift = (perm_idx + 1) * context.getNumBaseVariables(); + const int transition_skip = (1 + (p-1) / net->numberOfPlaces()) * net->numberOfTransitions(); + const int next_var_col = p + transition_skip + next_variable_shift; + + indir[l+1] = next_var_col; + row[l+1] = -1; + l++; + } + glp_set_mat_row(lp, rowno, l, indir.data(), row.data()); + // set the next base variable equal to transitions fired in last marking + if(perm_idx != permutation.size() - 1){ + glp_set_row_bnds(lp, rowno, GLP_FX, 0, 0); + }else{ + glp_set_row_bnds(lp, rowno, GLP_LO, 0, infty); + } + rowno++; + } + } + } + // add equations + if(emplaceEquationsShifted(lp, context, rowno, row, indir, lps[lp_idx]->equations(), variable_shift)){return true;} + if(context.timeout()){return false;} + + // Set objective, kind and bounds + /*for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int path_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t t = 1; t <= net->numberOfTransitions(); t++) { + const int transition_var = t + path_offset + variable_shift; + glp_set_obj_coef(lp, transition_var, 1); + glp_set_col_kind(lp, transition_var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, transition_var, GLP_LO, 0, infty); + } + // first base place variables already set by buildbase() + if(perm_idx != 0 || freelp){ + for (size_t p = 1; p <= net->numberOfPlaces(); p++) { + const int place_var = p + net->numberOfTransitions() + path_offset + variable_shift; + glp_set_obj_coef(lp, place_var, 0); + glp_set_col_kind(lp, place_var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, place_var, GLP_LO, 0, infty); + } + } + }*/ + } + + for(size_t p = 1; p <= context.getNumBaseConstraints(); p++){ + int l = glp_get_mat_row(lp, p, indir.data(), row.data()); - return _result == result_t::IMPOSSIBLE; + // add variable for the next base to meet on, which last does not have + const int first_base_shift = context.getNumBaseVariables(); + const int transition_skip = (1 + (p-1) / net->numberOfPlaces()) * net->numberOfTransitions(); + const int first_var_col = p + transition_skip + first_base_shift; + + indir[l+1] = first_var_col; + row[l+1] = -1.0; + l++; + + glp_set_mat_row(lp, p, l, indir.data(), row.data()); + // sets the first (next) base variable equal to transitions fired in first marking + glp_set_row_bnds(lp, p, GLP_FX, 0, 0); + } + + printConstraints(context, lp); + + return solve_built_lp(lp, context, solvetime, false) == result_t::IMPOSSIBLE; + } + + bool LinearProgram::isNStepsImpossible(double firelimit, bool strict, const PQL::SimplificationContext& context, uint32_t solvetime){ + bool use_ilp = true; + auto net = context.net(); + + 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 = context.getNumBaseVariables(); + const uint32_t nRow = context.getNumBaseConstraints() + _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 + context.getNumBaseConstraints(); + glp_add_rows(lp, _equations.size()); + + + + if(emplaceEquations(lp, context, rowno, row, indir, _equations)){glp_delete_prob(lp);_result = result_t::IMPOSSIBLE;return true;} + if(context.timeout()){glp_delete_prob(lp);return false;} + + // Set objective, kind and bounds + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for (size_t i = 1; i <= net->numberOfTransitions(); i++) { + const int var = i + variable_offset; + glp_set_obj_coef(lp, var, 1); + glp_set_col_kind(lp, var, use_ilp ? GLP_IV : GLP_CV); + glp_set_col_bnds(lp, var, GLP_LO, 0, infty); + } + } + + for(size_t path = 0; path < static_cast(context.numPaths()); path++){ + glp_add_rows(lp, 1); + int variable_offset = path * ( net->numberOfPlaces() + net->numberOfTransitions() ); + for(size_t t = 1; t <= net->numberOfTransitions(); t++){ + indir[t] = t + variable_offset; + row[t] = 1.0; + } + glp_set_mat_row(lp, rowno, net->numberOfTransitions(), indir.data(), row.data()); + if(strict){ + glp_set_row_bnds(lp, rowno, GLP_FX, firelimit, firelimit); + }else{ + glp_set_row_bnds(lp, rowno, GLP_UP, -infty, firelimit); + } + ++rowno; + } + + printConstraints(context, lp); + + return solve_built_lp(lp, context, solvetime, true) == result_t::IMPOSSIBLE; } void LinearProgram::solvePotency(const PQL::SimplificationContext& context, std::vector& potencies) - { + { + if(context.numPaths() != 1){ + std::cerr << "Solving potency of HyperLTL LP is not implemented"; + return; + } + bool use_ilp = false; // No need to call the ILP solver auto net = context.net(); diff --git a/src/PetriEngine/Simplification/LinearPrograms.cpp b/src/PetriEngine/Simplification/LinearPrograms.cpp index c7ee2df70..4a6e22ac0 100644 --- a/src/PetriEngine/Simplification/LinearPrograms.cpp +++ b/src/PetriEngine/Simplification/LinearPrograms.cpp @@ -4,15 +4,320 @@ namespace PetriEngine { namespace Simplification { + void AbstractProgramCollection::timepoint::print(){ + print(0); + } + void AbstractProgramCollection::timepoint::print(int depth){ + std::string tabs = ""; + for(int i = 0; i < depth; i++) + tabs += "\t"; + + std::cout << tabs << "LPS: [" << free_lps.size() << "," << final_lps.size() << "," << next_lps.size() << "," << global_lps.size() << "]\n"; + for(auto& suc: next) + suc->print(depth + 1); + } + + std::shared_ptr AbstractProgramCollection::timepoint::clone(){ + auto tp = std::make_shared(timepoint()); + + std::copy(free_lps.begin(), free_lps.end(), std::back_inserter(tp->free_lps)); + std::copy(final_lps.begin(), final_lps.end(), std::back_inserter(tp->final_lps)); + std::copy(next_lps.begin(), next_lps.end(), std::back_inserter(tp->next_lps)); + std::copy(global_lps.begin(), global_lps.end(), std::back_inserter(tp->global_lps)); + + tp->is_compiled = is_compiled; + tp->is_child = is_child; + + for(auto& suc: next) + tp->next.push_back(suc->clone()); + + return tp; + } + + void AbstractProgramCollection::timepoint::make_union(LinearProgram& union_lp){ + for(auto& [tcx_lp, lp]: free_lps){ + lp.make_union(union_lp); + } + for(auto& [tcx_lp, lp]: next_lps){ + lp.make_union(union_lp); + } + for(auto& [tcx_lp, lp]: final_lps){ + lp.make_union(union_lp); + } + for(auto& [tcx_lp, lp]: global_lps){ + lp.make_union(union_lp); + } + + for(auto& suc : next){ + suc->make_union(union_lp); + } + } + + bool AbstractProgramCollection::timepoint::is_impossible(const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime){ + std::vector progs; + std::vector> ivals; + return is_impossible(progs, ivals, context, tcx, solvetime); + } + + bool AbstractProgramCollection::timepoint::is_impossible(std::vector& progs, std::vector>& ivals, const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime){ + assert(is_compiled); + //std::cout << "is_impossible " << progs.size() << "\n" ; + if(!free_lps.empty()){ + assert(free_lps.size() == 1); + bool free_impossible = free_lps[0].prog.isImpossible(context, solvetime); + if(free_impossible){ + //std::cout << "free impossible\n"; + return true; + } + + ivals.push_back(std::make_pair(progs.size(), progs.size())); + progs.push_back(&free_lps[0].prog); + } + + const int start_interval = progs.size(); + + if(tcx.enable_X_rule){ + for(auto& [lp_tcx, lp] : next_lps){ + if(!tcx.has_prefix() && !is_child){ + double lim = static_cast(lp_tcx._next_ops); + //std::cout << "lim: " << lim << "\n"; + if(lp.isNStepsImpossible(lim, (!context.isDeadlocked() && lp_tcx._next_ops == 1), context, solvetime)){ + //std::cout << "1: n step impossible\n"; + return true; + } + }else{ + if(lp.isImpossible(context, solvetime)){ + //std::cout << "basic next impossible\n"; + return true; + } + } + + progs.push_back(&lp); + } + } + + if(tcx.enable_F_rule){ + for(auto& [lp_tcx, lp] : final_lps){ + if(lp.isImpossible(context, solvetime)){ + //std::cout << "basic f impossible\n"; + return true; + } + progs.push_back(&lp); + } + + const int end_interval = progs.size(); + if(start_interval != end_interval){ + ivals.push_back(std::make_pair(start_interval, end_interval)); + } + + if(next.empty() && progs.size() > 1){ + std::vector> perms; + std::vector starts; + for(auto& [s, e] : ivals){ + if(s == e) + continue; + + starts.push_back(s); + std::vector p; + for(uint32_t i = s; i < e; i++){ + p.push_back(i); + } + perms.emplace_back(std::move(p)); + } + bool final_impossible = LinearProgram::solveFinalConjunctionImpossible(progs, perms, starts, context); + if(final_impossible){ + //std::cout << "final impossible\n"; + return true; + } + }else{ + const auto num_prog = progs.size(); + const auto num_ivals = ivals.size(); + for(auto& suc : next){ + if(suc->is_impossible(progs, ivals, context, tcx, solvetime)){ + return true; + }else{ + progs.resize(num_prog); + ivals.resize(num_ivals); + } + } + } + } + return false; + } + + void AbstractProgramCollection::mergeBuffer::compile_program(){ + //assert(!time_path->is_compiled); + time_path->is_compiled = true; + //std::cout << "CMP: [" << time_path->free_lps.size() << "," << time_path->final_lps.size() << "," << time_path->next_lps.size() << "," << time_path->global_lps.size() << "]\n"; + if(time_path->global_lps.size() == 0 && time_path->free_lps.size() < 2) + return; + LinearProgram global_program = LinearProgram(); + for(const auto& [tcx, lp] : time_path->global_lps) + global_program.make_union(lp); + + LinearProgram free_program = LinearProgram(); + for(const auto& [tcx, lp] : time_path->free_lps) + free_program.make_union(lp); + + time_path->free_lps.clear(); + time_path->free_lps.push_back({temporalContext(), free_program}); + + if(!global_program.size() == 0){ + time_path->make_union(global_program); + + time_path->global_lps.clear(); + //time_path->global_lps.push_back({temporalContext(), std::make_shared(global_program)}); + } + } + + void AbstractProgramCollection::mergeBuffer::merge(mergeBuffer& other){ + + /*time_path->print(); + other.time_path->print(); + if(!other.time_path->is_empty() && !other.time_path->has_conditions()){ + std::cout << "next only path\n"; + }*/ + //std::copy(other.time_path->next.begin(), other.time_path->next.end(), std::back_inserter(time_path->next)); + for(auto& suc : other.time_path->next){ + time_path->next.push_back(suc->clone()); + } + std::copy(other.time_path->free_lps.begin(), other.time_path->free_lps.end(), std::back_inserter(time_path->free_lps)); + std::copy(other.time_path->final_lps.begin(), other.time_path->final_lps.end(), std::back_inserter(time_path->final_lps)); + std::copy(other.time_path->global_lps.begin(), other.time_path->global_lps.end(), std::back_inserter(time_path->global_lps)); + std::copy(other.time_path->next_lps.begin(), other.time_path->next_lps.end(), std::back_inserter(time_path->next_lps)); + } + void AbstractProgramCollection::mergeBuffer::apply_operator(operator_t update_op, int next_ops){ + switch(update_op){ + case operator_t::FREE:{ + assert(next_ops == 0); + break; + } + case operator_t::G:{ + //std::cout << "next ops " << next_ops << "\n"; + //std::cout << "apply G\n"; + + auto& glps = time_path->global_lps; + auto& freelps = time_path->free_lps; + std::move(freelps.begin(), freelps.end(), std::back_inserter(glps)); + freelps.clear(); + break; + } + case operator_t::F:{ + //std::cout << "F\n"; + //print(); + compile_program(); + auto& flps = time_path->final_lps; + auto& freelps = time_path->free_lps; + auto& nextlps = time_path->next_lps; + // std::move(freelps.begin(), freelps.end(), std::back_inserter(flps)); + std::move(nextlps.begin(), nextlps.end(), std::back_inserter(flps)); + // freelps.clear(); + nextlps.clear(); + time_path->global_lps.clear(); + update_next_counter(nextlps, next_ops); + update_next_counter(flps, next_ops); + advance_timepoint(); + //std::cout << "-----\n"; + //print(); + break; + } + case operator_t::X:{ + compile_program(); + auto& xlps = time_path->next_lps; + auto& freelps = time_path->free_lps; + std::move(freelps.begin(), freelps.end(), std::back_inserter(xlps)); + freelps.clear(); + time_path->global_lps.clear(); + update_next_counter(xlps, next_ops); + update_next_counter(freelps, next_ops); + break; + } + default: + assert(false); + } + } + + bool AbstractProgramCollection::mergeBuffer::lpsImpossible(const PQL::SimplificationContext& context, temporalContext& tcx, uint32_t solvetime){ + //print(); + if(!time_path){ + return false; + } + assert(time_path); + return time_path->is_impossible(context, tcx, solvetime); + /*if(time_path->free_lps.size() != 0){ + assert(time_path->free_lps.size() == 1); + bool free_impossible = time_path->free_lps[0].prog.isImpossible(context, solvetime); + if(free_impossible){ + std::cout << "free impossible\n"; + return true; + } + } + + if(tcx.enable_F_rule){ + for(auto cur = time_path; cur != nullptr; cur = cur->next){ + for(auto& [lp_tcx, lp] : cur->final_lps){ + if(lp.isImpossible(context, solvetime)){ + //std::cout << "F impossible\n"; + return true; + } + } + } + + if(context.rules().F_rule){ + std::cout << "before Final solve\n-----\n"; + print(); + std::cout << "-----\n"; + auto [lps, perms, starts] = setup_solve(); + if(lps.size() >= 2){ + bool final_impossible = LinearProgram::solveFinalConjunctionImpossible(lps, perms, starts, context); + if(final_impossible){ + std::cout << "final impossible\n"; + return true; + } + } + } + } + + if(tcx.enable_X_rule){ + for(auto cur = time_path; cur != nullptr; cur = cur->next){ + for(auto& [lp_tcx, lp] : cur->next_lps){ + if(cur == time_path && !tcx.has_prefix()){ + double lim = static_cast(lp_tcx.prefix_X); + std::cout << "fire limit " << lim << "\n"; + if(lp.isNStepsImpossible(lim, (!context.isDeadlocked() && lp_tcx.prefix_X == 1), context, solvetime)){ + return true; + } + }else{ + if(lp.isImpossible(context, solvetime)){ + return true; + } + } + } + } + + }*/ + + return false; + } + // *********************************** // AbstractProgramCollection functions // *********************************** - bool AbstractProgramCollection::satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime) - { + AbstractProgramCollection_ptr AbstractProgramCollection::clone(){ + reset(); + return cloneImpl(); + } + + bool AbstractProgramCollection::satisfiable(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) + { reset(); - if (context.timeout() || has_empty || solvetime == 0) return true; + if (context.timeout() || has_empty || solvetime == 0 || tcx.skip_solve()){ + if(context.timeout()) + //std::cout << "returning from timeout\n"; + return true; + } if (_result != UNKNOWN) { if (_result == IMPOSSIBLE) @@ -20,11 +325,17 @@ namespace PetriEngine { return _result == POSSIBLE; } } - satisfiableImpl(context, solvetime); + //tcx.update(_operator, _next_ops); + satisfiableImpl(context, tcx, solvetime); assert(_result != UNKNOWN); return _result == POSSIBLE; } + + nextProgram AbstractProgramCollection::get_next_program(){ + return getNextProgramImpl(); + } + uint32_t AbstractProgramCollection::explorePotency(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -68,28 +379,51 @@ namespace PetriEngine { current = 0; } - bool UnionCollection::merge(bool& has_empty, LinearProgram& program, bool dry_run) + bool UnionCollection::merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run) { + //tcx.push_prefix(_operator, false); if (current >= lps.size()) { current = 0; } - if (!lps[current]->merge(has_empty, program, dry_run)) + bool has_more = lps[current]->merge(has_empty, buf, tcx, dry_run); + + if(!dry_run) + buf.apply_operator(_operator, _next_ops); + + if (!has_more) { ++current; - if (current < lps.size()) + if (current < lps.size()){ lps[current]->reset(); + } } return current < lps.size(); } - void UnionCollection::satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) + AbstractProgramCollection_ptr UnionCollection::cloneImpl(){ + std::vector members; + for(int i = 0; i < lps.size(); i++){ + members.push_back(lps[i]->clone()); + } + auto u = std::make_shared(std::move(members)); + u->_next_ops = _next_ops; + u->_operator = _operator; + return u; + } + + void UnionCollection::satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) { + //std::cout << "solve union\n"; + tcx.update(_operator, _next_ops); + //std::cout << "op" << _operator << "\n"; + //tcx.push_prefix(_operator, false); + //std::cout << "tcx:" << tcx.prefix_F << ", " << tcx.prefix_G << ", " << tcx.prefix_X << "\n"; for (int i = lps.size() - 1; i >= 0; --i) { - if (lps[i]->satisfiable(context, solvetime) || context.timeout()) + if (lps[i]->satisfiable(context, tcx, solvetime) || context.timeout()) { _result = POSSIBLE; return; @@ -99,10 +433,34 @@ namespace PetriEngine { lps.erase(lps.begin() + i); } } - if (_result != POSSIBLE) + if (_result != POSSIBLE){ + //std::cout << "union impossible\n"; _result = IMPOSSIBLE; + } } + + nextProgram UnionCollection::getNextProgramImpl(){ + if(lps.size() == 0){ + return {std::make_shared(LinearProgram()), false}; + } + assert(current < lps.size()); + AbstractProgramCollection_ptr prog = lps[current]; + // this is to handle nested unions/merges where the value of np.prog might not be a SingleProgram + nextProgram np = prog->get_next_program(); + if(!np.hasmore){ + bool hasmore = (current + 1 < lps.size()); + if(hasmore){ + current++; + }else{ + reset(); + } + return {np.prog, hasmore}; + }else{ + return np; + } + } + uint32_t UnionCollection::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -149,27 +507,42 @@ namespace PetriEngine { rempty = false; tmp_prog = LinearProgram(); + mergeBuffer right_buf = mergeBuffer(); curr = 0; + + _final_programs.clear(); + + next_prog = LinearProgram(); } - bool MergeCollection::merge(bool& has_empty, LinearProgram& program, bool dry_run) + bool MergeCollection::merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run) { - if (program.knownImpossible()) { + //std::cout << "merge conj\n"; + if (buf.program.knownImpossible()) { return false; } + //tcx.push_prefix(_operator, false); + bool lempty = false; bool more_left; + + //tcx.update(_operator, _next_ops); + while (true) { lempty = false; - LinearProgram prog = program; + //LinearProgram prog = program; if (merge_right) { assert(more_right); rempty = false; - tmp_prog = LinearProgram(); - more_right = right->merge(rempty, tmp_prog, false); + //tmp_prog = LinearProgram(); + //more_right = right->merge(rempty, tmp_prog, tcx, false); + right_buf = mergeBuffer(); + //std::cout << "empty: " <<(right_buf.time_path == nullptr) << "\n"; + more_right = right->merge(rempty, right_buf, tcx, false); + //right_buf.print(); left->reset(); merge_right = false; } @@ -177,30 +550,61 @@ namespace PetriEngine { ++curr; assert(curr <= _size); - more_left = left->merge(lempty, prog/*, dry_run || curr < nsat*/); + //more_left = left->merge(lempty, prog, tcx/*, dry_run || curr < nsat*/); + if(dry_run || curr < nsat){ + mergeBuffer dry_buf = mergeBuffer(); + more_left = left->merge(lempty, dry_buf, tcx, true); + }else{ + more_left = left->merge(lempty, buf, tcx/*, dry_run || curr < nsat*/); + //buf.print(); + } + if (!more_left) merge_right = true; 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) { program.swap(prog); - } + }*/ + //if ((!dry_run && buf.program.knownImpossible()) && (more_left || more_right)) { + // continue; + //} break; } } - if (!dry_run) - program.make_union(tmp_prog); + //if (!dry_run) + // program.make_union(tmp_prog); + + if (!dry_run){ + buf.merge(right_buf); + buf.apply_operator(_operator, _next_ops); + } + has_empty = lempty && rempty; return more_left || more_right; } - void MergeCollection::satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) + AbstractProgramCollection_ptr MergeCollection::cloneImpl(){ + auto m = std::make_shared(left->clone(), right->clone()); + m->_next_ops = _next_ops; + m->_operator = _operator; + return m; + } + + void MergeCollection::satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) { + //std::cout << "merge sat\n"; // this is where the magic needs to happen + //tcx.update(_operator, _next_ops); + //std::cout << "op" << _operator << "\n"; + //auto pre = tcx.push_prefix(_operator, false); + //auto pre_ctx = temporalContext(); + //pre_ctx.set_prefix(pre); + //std::cout << "tcx:" << tcx.prefix_F << ", " << tcx.prefix_G << ", " << tcx.prefix_X << "\n"; bool hasmore = false; do { if (context.timeout()) @@ -209,9 +613,19 @@ namespace PetriEngine { break; } - LinearProgram prog; + //LinearProgram prog; + bool has_empty = false; - hasmore = merge(has_empty, prog); + mergeBuffer buf = mergeBuffer(tcx, LinearProgram()); + + auto tmp_ctx = temporalContext(); + hasmore = merge(has_empty, buf, tmp_ctx); + + //buf.print(); + buf.apply_operator(tcx._operator, tcx._next_ops); + buf.compile_program(); + + if (has_empty) { _result = POSSIBLE; @@ -219,8 +633,10 @@ namespace PetriEngine { } else { + //std::cout << "merge before solve:\n"; + //buf.print(); if (context.timeout() || - !prog.isImpossible(context, solvetime)) + !buf.lpsImpossible(context, tcx, solvetime)) { _result = POSSIBLE; break; @@ -228,27 +644,47 @@ namespace PetriEngine { } ++nsat; } while (hasmore); + if (_result != POSSIBLE) _result = IMPOSSIBLE; } + nextProgram MergeCollection::getNextProgramImpl(){ + bool has_empty = false; + next_prog = LinearProgram(); + temporalContext tcx(false); tcx.update(_operator, _next_ops); + mergeBuffer buf = mergeBuffer(tcx, next_prog); + bool hasmore = merge(has_empty, buf, tcx); + next_prog = buf.program; + std::shared_ptr prog_ptr = std::make_shared(next_prog); + nextProgram np = {prog_ptr, hasmore}; + + if(!hasmore){ + reset(); + } + + return np; + } + uint32_t MergeCollection::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { bool hasmore = false; + temporalContext tcx(false); tcx.update(_operator, _next_ops); do { if (context.potencyTimeout() || maxConfigurationsSolved == 0) return 0; LinearProgram prog; + mergeBuffer buf = mergeBuffer(tcx, prog); bool has_empty = false; - hasmore = merge(has_empty, prog); + hasmore = merge(has_empty, buf, tcx); if (has_empty) return maxConfigurationsSolved; else { --maxConfigurationsSolved; - prog.solvePotency(context, potencies); + buf.program.solvePotency(context, potencies); } ++nsat; @@ -266,6 +702,12 @@ namespace PetriEngine { has_empty = true; } + SingleProgram::SingleProgram(LinearProgram lp) : AbstractProgramCollection() + { + program = lp; + has_empty = ( program.size() == 0 ); + } + SingleProgram::SingleProgram(LPCache* factory, const Member& lh, int64_t constant, op_t op) : AbstractProgramCollection(), program(factory->createAndCache(lh.variables()), constant, op, factory) @@ -274,20 +716,94 @@ namespace PetriEngine { assert(!has_empty); } - bool SingleProgram::merge(bool& has_empty, LinearProgram& program, bool dry_run) - { + bool SingleProgram::merge(bool& has_empty, mergeBuffer& buf, temporalContext tcx, bool dry_run) + { + + //std::cout << "\t\tmerge single\n"; if (dry_run) return false; + + /*tcx.update(_operator, _next_ops); + switch(tcx._operator){ + case operator_t::F:{ + buf.final_unmerged.push_back({tcx,&this->program}); + return false; + } + case operator_t::X:{ + buf.next_unmerged.push_back({tcx,&this->program}); + return false; + } + case operator_t::G:{ + buf.global_conditions.push_back({tcx,&this->program}); + break; + } + default: + break; + } + auto& program = buf.program; program.make_union(this->program); + */ + temporalContext lp_tcx = temporalContext(); + lp_tcx._next_ops = tcx._next_ops + _next_ops; + lp_tcx._operator = std::min(tcx._operator, _operator); + timepoint tp = timepoint(); + //auto program_ptr = std::make_shared(LinearProgram(this->program)); + switch(lp_tcx._operator){ + case operator_t::FREE:{ + tp.free_lps.push_back({lp_tcx, this->program}); + break; + } + case operator_t::G:{ + tp.global_lps.push_back({lp_tcx, this->program}); + break; + } + case operator_t::F:{ + tp.final_lps.push_back({lp_tcx, this->program}); + break; + } + case operator_t::X:{ + tp.next_lps.push_back({lp_tcx, this->program}); + break; + } + default: + assert(false); + } + buf.time_path = std::make_shared(tp); + has_empty = this->program.equations().size() == 0; assert(has_empty == this->has_empty); return false; } - void SingleProgram::satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) + AbstractProgramCollection_ptr SingleProgram::cloneImpl(){ + auto s = std::make_shared(LinearProgram(this->program)); + s->_next_ops = _next_ops; + s->_operator = _operator; + return s; + } + + void SingleProgram::satisfiableImpl(const PQL::SimplificationContext& context, temporalContext tcx, uint32_t solvetime) { + //std::cout << "sinsgle program\n"; // this is where the magic needs to happen - if (!program.isImpossible(context, solvetime)) + //tcx.update(_operator, _next_ops); + auto top = std::min(_operator, tcx._operator); + auto tnext_ops = _next_ops + tcx._next_ops; + if(context.rules().X_rule && !tcx.has_prefix() && tnext_ops >= 1 && top >= operator_t::X){ + //std::cout << "next ops " << _next_ops << "\n"; + double lim = static_cast(tnext_ops); + //std::cout << "sp fire limit " << lim << "\n"; + if (!program.isNStepsImpossible(lim, (!context.isDeadlocked() && tnext_ops == 1), context, solvetime)) + { + //std::cout << "possible x\n"; + _result = POSSIBLE; + } + else + { + //std::cout << "impossible x\n"; + _result = IMPOSSIBLE; + } + }else if (!program.isImpossible(context, solvetime)) { _result = POSSIBLE; } @@ -297,6 +813,11 @@ namespace PetriEngine { } } + nextProgram SingleProgram::getNextProgramImpl(){ + return {std::make_shared(program), false}; + } + + uint32_t SingleProgram::explorePotencyImpl(const PQL::SimplificationContext& context, std::vector &potencies, uint32_t maxConfigurationsSolved) { @@ -306,5 +827,6 @@ namespace PetriEngine { program.solvePotency(context, potencies); return maxConfigurationsSolved - 1; } + } } diff --git a/src/PetriEngine/options.cpp b/src/PetriEngine/options.cpp index f5379408d..532c590ff 100644 --- a/src/PetriEngine/options.cpp +++ b/src/PetriEngine/options.cpp @@ -110,6 +110,32 @@ 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"; + } + + optionsOut << ",LP_Rules="; + if(useFRule) + optionsOut << "F"; + if(useGRule){ + if(useFRule) optionsOut << ","; + optionsOut << "G"; + } + if(useXRule){ + if(useFRule || useGRule) optionsOut << ","; + optionsOut << "X"; + } + if(!useGRule && !useFRule && !useXRule) + optionsOut << "None"; + + if (usedctl) { if (ctlalgorithm == CTL::CZero) { @@ -185,6 +211,15 @@ 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" + " -lpr, --lp-rules Change LP simplification rules, case-insensitive, default F,G,X (all enabled)\n" + " - N disable all, incompatible with other values\n" + " - F enable F-rule\n" + " - G enable G-rule\n" + " - X enable X-rule\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" @@ -374,6 +409,53 @@ 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 LP print level argument ", std::quoted(argv[i])); + } + } else if (std::strcmp(argv[i], "-lpr") == 0 || std::strcmp(argv[i], "--lp-rules") == 0){ + if (i == argc - 1) { + throw base_error("Missing argument value after ", std::quoted(argv[i])); + } + ++i; + bool has_n = false; + useFRule = false; + useGRule = false; + useXRule = false; + for(int j = 0; j < strlen(argv[i]);j++){ + const char c = std::tolower(argv[i][j]); + switch(c){ + case ',': + break; + case 'n': + has_n = true; + break; + case 'f': + useFRule = true; + break; + case 'g': + useGRule = true; + break; + case 'x': + useXRule = true; + break; + default: + throw base_error("Argument Error: Invalid LPRule argument: unknown value '\'", argv[i][j], "\' in ", std::quoted(argv[i])); + } + } + if(has_n && (useFRule || useGRule || useXRule)){ + throw base_error("Argument Error: Invalid LPRule argument ", std::quoted(argv[i]), ", \'N\' is incompatible with other values"); + } + } else if (std::strcmp(argv[i], "-lpl") == 0 || std::strcmp(argv[i], "--lp-permutation-limit") == 0){ + if (i == argc - 1) { + throw base_error("Missing number after ", std::quoted(argv[i])); + } + if (sscanf(argv[++i], "%d", &permutationLimit) != 1 || permutationLimit < 0) { + throw base_error("Argument Error: Invalid LP permutation limit 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/VerifyPN.cpp b/src/VerifyPN.cpp index 8d9eee3f3..823390270 100644 --- a/src/VerifyPN.cpp +++ b/src/VerifyPN.cpp @@ -446,6 +446,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); @@ -579,9 +583,25 @@ void simplify_queries(const MarkVal* marking, bool wasAGCPNApprox = dynamic_cast (queries[i].get()) != nullptr; if (options.logic == TemporalLogic::LTL) { + int num_paths = 0; if (options.queryReductionTimeout == 0 || qt == 0) continue; - SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache); + + if(auto path = dynamic_cast(queries[i].get())) { + bool wasACond = path->is(); + for(;path; path = dynamic_cast(path->child().get())) + { + if(wasACond != path->is()) + { + std::stringstream ss; + queries[i]->toString(ss); + throw base_error("Missing Hyper-LTL quantifiers: ", ss.str()); + } + num_paths++; + } + } + num_paths = std::max(1, num_paths); + SimplificationContext simplificationContext(marking, net, num_paths, qt, + options, &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; @@ -612,7 +632,7 @@ void simplify_queries(const MarkVal* marking, if (options.queryReductionTimeout > 0 && qt > 0) { SimplificationContext simplificationContext(marking, net, qt, - options.lpsolveTimeout, &cache); + 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; @@ -736,7 +756,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;