Test LP generalization

include/PetriEngine/AbstractPetriNetBuilder.h

@@ -105,6 +105,11 @@ namespace PetriEngine {
             throw base_error("Product colors are not supported in standard P/T nets");
         }
 
+        virtual void addTokens(std::string&& place, Colored::Multiset&& tokens)
+        {
+            throw base_error("Parsing marking is not supported");
+        }
+
         virtual void enableColors() {
             _isColored = true;
         }

include/PetriEngine/Colored/ColoredPetriNetBuilder.h

@@ -152,6 +152,13 @@ namespace PetriEngine {
             return _string_set;
         }
 
+        // Since ColoredPetriNetBuilder takes ownership of any colors given to it, we need to be able to tell it to
+        // forget about those colors and "leak" the memory
+        void leak_colors()
+        {
+            _ownsColors = false;
+        }
+
     private:
         shared_name_index_map _placenames;
         shared_name_index_map _transitionnames;
@@ -164,6 +171,7 @@ namespace PetriEngine {
         Colored::ColorTypeMap _colors;
         PetriNetBuilder _ptBuilder;
         shared_string_set& _string_set;
+        bool _ownsColors = true;
 
         void addArc(const std::string& place,
                 const std::string& transition,

include/PetriEngine/Colored/PnmlWriter.h

@@ -11,10 +11,23 @@
 namespace PetriEngine::Colored {
     class PnmlWriter {
     public:
-        PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0) {}
+        PnmlWriter(PetriEngine::ColoredPetriNetBuilder &b, std::ostream &out) : _builder(b), _out(out), _tabsCount(0)
+        {
+            for (auto &namedSort: _builder._colors)
+            {
+                std::vector<const ColorType *> types;
+                ColorType *colortype = const_cast<ColorType *>(namedSort.second);
+                colortype->getColortypes(types);
+                if (is_number(types[0]->operator[](size_t{0}).getColorName())) {
+                    _namedSortTypes.emplace(colortype->getName(), "finite range");
+                } else {
+                    _namedSortTypes.emplace(colortype->getName(), "cyclic enumeration");
+                }
+            }
+        }
 
         void toColPNML();
-
+        void writeInitialTokens(const std::string& placeId);
     private:
         PetriEngine::ColoredPetriNetBuilder &_builder;
         std::ostream &_out;
@@ -77,6 +90,8 @@ namespace PetriEngine::Colored {
 
         void handlehlinitialMarking(Multiset marking);
 
+        void handleTokenExpression(const Multiset& tokens);
+
         void handleType(const Place &place);
 
         void add_arcs_from_transition(Transition &transition);

include/PetriEngine/ExplicitColored/ColoredResultPrinter.h

@@ -2,6 +2,7 @@
 #define COLORED_RESULT_PRINTER_H
 
 #include "AtomicTypes.h"
+#include "ExplicitColoredPetriNetBuilder.h"
 #include "PetriEngine/ExplicitColored/Algorithms/SearchStatistics.h"
 #include "PetriEngine/Reachability/ReachabilityResult.h"
 
@@ -28,12 +29,22 @@ namespace PetriEngine::ExplicitColored {
         bool isInitial;
     };
 
+    struct ExplicitColoredTraceContext
+    {
+        ExplicitColoredTraceContext(std::vector<TraceStep> traceSteps, ExplicitColoredPetriNetBuilder cpnBuilder)
+            : traceSteps(std::move(traceSteps)), cpnBuilder(std::move(cpnBuilder)) {}
+        ExplicitColoredTraceContext(ExplicitColoredTraceContext&&) = default;
+        ExplicitColoredTraceContext& operator=(ExplicitColoredTraceContext&&) = default;
+        std::vector<TraceStep> traceSteps;
+        ExplicitColoredPetriNetBuilder cpnBuilder;
+    };
+
     class IColoredResultPrinter {
     public:
         virtual void printResult(
             const SearchStatistics& searchStatistics,
             Reachability::AbstractHandler::Result result,
-            const std::vector<TraceStep>* trace
+            const ExplicitColoredTraceContext* trace
         ) const = 0;
         virtual void printNonExplicitResult(
             std::vector<std::string> techniques,
@@ -58,7 +69,7 @@ namespace PetriEngine::ExplicitColored {
         void printResult(
             const SearchStatistics& searchStatistics,
             Reachability::AbstractHandler::Result result,
-            const std::vector<TraceStep>* trace
+            const ExplicitColoredTraceContext* trace
         ) const override;
 
         void printNonExplicitResult(
@@ -67,7 +78,8 @@ namespace PetriEngine::ExplicitColored {
         ) const override;
     private:
         void _printCommon(Reachability::AbstractHandler::Result result, const std::vector<std::string>& extraTechniques) const;
-        void _printTrace(const std::vector<TraceStep>& trace) const;
+        void _printTrace(const ExplicitColoredTraceContext& trace) const;
+        void _printMarkings(const ExplicitColoredPetriNetBuilder& explicitCpnBuilder, const TraceStep& traceStep) const;
         uint32_t _queryOffset;
         std::ostream& _stream;
         std::string _queryName;

include/PetriEngine/ExplicitColored/ExplicitColoredInteractiveMode.h

@@ -12,17 +12,17 @@ namespace PetriEngine::ExplicitColored {
     public:
         static int run(const std::string& model_path);
     private:
-        ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, const ExplicitColoredPetriNetBuilder& builder);
+        ExplicitColoredInteractiveMode(const ColoredSuccessorGenerator& successorGenerator, const ColoredPetriNet& cpn, ExplicitColoredPetriNetBuilder& builder);
         int _run_internal();
         static std::string _readUntilDoubleNewline(std::istream& in);
-        std::optional<ColoredPetriNetMarking> _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut) const;
+        std::optional<ColoredPetriNetMarking> _parseMarking(const rapidxml::xml_document<>& markingXml, std::ostream& errorOut);
         std::optional<std::pair<Transition_t, Binding>> _parseTransition(const rapidxml::xml_document<>& transitionXml, std::ostream& errorOut) const;
         void _printCurrentMarking(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const;
         void _printValidBindings(std::ostream& out, const ColoredPetriNetMarking& currentMarking) const;
         std::optional<Color_t> _findColorIndex(const Colored::ColorType* colorType, const char* colorName) const;
         const ColoredSuccessorGenerator& _successorGenerator;
         const ColoredPetriNet& _cpn;
-        const ExplicitColoredPetriNetBuilder& _builder;
+        ExplicitColoredPetriNetBuilder& _builder;
     };
 }
 #endif //COLOREDINTERACTIVEMODE_H

include/PetriEngine/ExplicitColored/ExplicitColoredModelChecker.h

@@ -7,6 +7,7 @@
 #include "Visitors/ConditionCopyVisitor.h"
 
 #include "ColoredResultPrinter.h"
+#include "ExplicitColoredPetriNetBuilder.h"
 #include "Algorithms/ExplicitWorklist.h"
 
 namespace PetriEngine::ExplicitColored {
@@ -34,7 +35,7 @@ namespace PetriEngine::ExplicitColored {
             options_t& options
         ) const;
 
-        std::pair<Result, std::optional<std::vector<TraceStep>>> explicitColorCheck(
+        std::pair<Result, std::optional<ExplicitColoredTraceContext>> explicitColorCheck(
             const std::string& pnmlModel,
             const PQL::Condition_ptr& query,
             options_t& options,

include/PetriEngine/ExplicitColored/ExplicitColoredPetriNetBuilder.h

@@ -1,5 +1,7 @@
 #ifndef EXPLICIT_COLORED_PETRI_NET_BUILDER_H
 #define EXPLICIT_COLORED_PETRI_NET_BUILDER_H
+#include <rapidxml.hpp>
+
 #include "PetriEngine/AbstractPetriNetBuilder.h"
 #include "ColoredPetriNet.h"
 
@@ -27,6 +29,7 @@ namespace PetriEngine::ExplicitColored {
         void addColorType(const std::string& id, const Colored::ColorType* type) override;
         void addVariable(const Colored::Variable* variable) override;
         void addToColorType(Colored::ProductType* colorType, const Colored::ColorType* newConstituent) override;
+        void addTokens(std::string&& place, Colored::Multiset&& tokens) override;
         void sort() override;
 
         const std::unordered_map<std::string, uint32_t>& getPlaceIndices() const;
@@ -45,6 +48,8 @@ namespace PetriEngine::ExplicitColored {
 
         ColoredPetriNetBuilderStatus build();
         ColoredPetriNet takeNet();
+
+        ColoredPetriNetMarking parseMarking(const rapidxml::xml_document<>& markingXml);
     private:
         std::unordered_map<Place_t, const Colored::ColorType*> _underlyingColorType;
         std::unordered_map<std::string, Place_t> _placeIndices;
@@ -66,6 +71,8 @@ namespace PetriEngine::ExplicitColored {
         std::unordered_map<Transition_t, std::string> _transitionToId;
         std::unordered_map<Variable_t, std::string> _variableToId;
 
+        bool _parsingStandAloneMarking = false;
+        ColoredPetriNetMarking _standAloneMarking;
         void _createArcsAndTransitions();
         ColoredPetriNetBuilderStatus _calculateTransitionVariables();
         void _calculatePrePlaceConstraints();

include/PetriEngine/PQL/Contexts.h

@@ -36,6 +36,8 @@
 #include <chrono>
 #include <glpk.h>
 
+#include <chrono>
+
 namespace PetriEngine {
 
     namespace PQL {
@@ -179,13 +181,15 @@ namespace PetriEngine {
         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;
+                std::cout << "paths: " << _num_paths << "\n";
                 _base_lp = buildBase();
                 _start = std::chrono::high_resolution_clock::now();
                 _cache = cache;
@@ -195,8 +199,17 @@ namespace PetriEngine {
                         _markingOutOfBounds = true;
                     }
                 }
+
+                _isDeadlocked = _net->deadlocked(_marking);
+                _id = std::chrono::system_clock::now();
             }
 
+            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<std::chrono::system_clock> _id;
+
             virtual ~SimplificationContext() {
                 if(_base_lp != nullptr)
                     glp_delete_prob(_base_lp);
@@ -212,6 +225,10 @@ namespace PetriEngine {
                 return _markingOutOfBounds;
             }
 
+            bool isDeadlocked() const {
+                return _isDeadlocked;
+            }
+
             const PetriNet* net() const {
                 return _net;
             }
@@ -244,20 +261,40 @@ namespace PetriEngine {
 
             uint32_t getLpTimeout() const;
             uint32_t getPotencyTimeout() const;
+            uint32_t getPrintLevel() const;
+
+            int 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;
             }
 
+            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<int32_t>& ind, std::vector<double>& col) const;
+
             glp_prob* makeBaseLP() const;
 
+            glp_prob* buildBaseFromMarking(std::vector<std::pair<std::vector<uint32_t>, double>>& setMarking) const;
+
         private:
+            int _num_paths = 1;
             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;

include/PetriEngine/PQL/Simplifier.h

@@ -39,6 +39,18 @@ namespace PetriEngine { namespace PQL {
         SimplificationContext& _context;
         Retval _return_value;
 
+        enum LPQUANT {NONE, GLOBAL, FINAL, NEXT, UNTIL, OTHER, NULLT};
+        LPQUANT quantifier_found = LPQUANT::NONE;
+        LPQUANT quantifier_parent = LPQUANT::NONE;
+        bool qparent_neg_context = false;
+        int32_t quantifiers = 0;
+
+        bool solveFinalCond(std::vector<AbstractProgramCollection_ptr>& final_lps);
+
+        bool finalLpsImpossible(std::vector<AbstractProgramCollection_ptr>& final_lps);
+        bool nextLpsImpossible(std::vector<AbstractProgramCollection_ptr>& next_lps, std::vector<AbstractProgramCollection_ptr>& 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 <typename Quantifier>
         Retval simplify_simple_quantifier(Retval &r);
 
+        template <typename Quantifier>
+        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 memberForTracePlace(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;

include/PetriEngine/Simplification/LinearProgram.h

@@ -11,8 +11,10 @@
 #include <memory>
 #include <glpk.h>
 
+
 namespace PetriEngine {
     namespace Simplification {
+        using REAL = double;
 
         struct equation_t
         {
@@ -35,6 +37,11 @@ namespace PetriEngine {
             enum result_t { UKNOWN, IMPOSSIBLE, POSSIBLE };
             result_t _result = result_t::UKNOWN;
             std::vector<equation_t> _equations;
+
+            bool addEquations(glp_prob* lp, const PQL::SimplificationContext& context, int& rowno, std::vector<REAL>& row, std::vector<int32_t>& indir, std::vector<equation_t>& equations);
+
+            bool solve_built_lp(glp_prob* lp, const PQL::SimplificationContext& context, uint32_t solvetime, bool set_result, bool delete_lp = true);
+
         public:
             void swap(LinearProgram& other)
             {
@@ -62,7 +69,13 @@ namespace PetriEngine {
             bool knownImpossible() const { return _result == result_t::IMPOSSIBLE; }
             bool knownPossible() const { return _result == result_t::POSSIBLE; }
 
+
+
+            double upperBoundForPlace(const PQL::SimplificationContext& context, std::vector<uint32_t>& place, uint32_t solvetime);
             bool isImpossible(const PQL::SimplificationContext& context, uint32_t solvetime);
+            bool isFinalImpossibleWith(LinearProgram& withLp, bool is_next, bool is_strict, const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits<uint32_t>::max());
+            bool isNStepsImpossible(double firelimit, bool strict, const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits<uint32_t>::max());
+            bool isBoundedImpossible(const PQL::SimplificationContext& context, std::vector<std::pair<std::vector<uint32_t>, double>>& bounds, uint32_t solvetime);
             void solvePotency(const PQL::SimplificationContext& context, std::vector<uint32_t>& potencies);
 
             void make_union(const LinearProgram& other);