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,9 +181,9 @@ namespace PetriEngine {
         public:
 
             SimplificationContext(const MarkVal* marking,
-                    const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
+                    const PetriNet* net, 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;
@@ -195,8 +197,12 @@ namespace PetriEngine {
                         _markingOutOfBounds = true;
                     }
                 }
+
+                _id = std::chrono::system_clock::now();
             }
 
+            std::chrono::time_point<std::chrono::system_clock> _id;
+
             virtual ~SimplificationContext() {
                 if(_base_lp != nullptr)
                     glp_delete_prob(_base_lp);
@@ -244,6 +250,7 @@ namespace PetriEngine {
 
             uint32_t getLpTimeout() const;
             uint32_t getPotencyTimeout() const;
+            uint32_t getPrintLevel() const;
 
             Simplification::LPCache* cache() const
             {
@@ -257,7 +264,7 @@ namespace PetriEngine {
             const MarkVal* _marking;
             bool _markingOutOfBounds;
             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,13 @@ namespace PetriEngine { namespace PQL {
         SimplificationContext& _context;
         Retval _return_value;
 
+        enum LPQUANT {NONE, GLOBAL, FINAL, OTHER, UNTIL};
+        LPQUANT quantifier_found = LPQUANT::NONE;
+        LPQUANT quantifier_parent = LPQUANT::NONE;
+        bool qparent_neg_context = false;
+        int32_t quantifiers = 0;
+
+
         Retval simplify_or(const LogicalCondition* element);
         Retval simplify_and(const LogicalCondition *element);
 
@@ -50,6 +57,8 @@ namespace PetriEngine { namespace PQL {
         Retval simplify_EF(Retval &r);
         Retval simplify_EX(Retval &r);
 
+        Retval simplify_global_quantifier(Retval &r);
+
         template <typename Quantifier>
         Retval simplify_simple_quantifier(Retval &r);
 

include/PetriEngine/Simplification/LinearPrograms.h

@@ -31,9 +31,11 @@ namespace PetriEngine {
 
                 virtual void clear() = 0;
                 virtual void reset() = 0;
+                //virtual AbstractProgramCollection clone() = 0;
                 virtual size_t size() const = 0;
                 virtual bool merge(bool& has_empty, LinearProgram& program, bool dry_run = false) = 0;
 
+
                 virtual uint32_t explorePotency(const PQL::SimplificationContext& context,
                                                 std::vector<uint32_t> &potencies,
                                                 uint32_t maxConfigurationsSolved = std::numeric_limits<uint32_t>::max());

include/PetriEngine/Simplification/Member.h

@@ -4,6 +4,7 @@
 #include <functional>
 #include <cassert>
 #include <cstring>
+#include <cstdint>
 //#include "../PQL/PQL.h"
 
 namespace PetriEngine {

include/PetriEngine/options.h

@@ -62,7 +62,7 @@ struct options_t {
     StatisticsLevel printstatistics = StatisticsLevel::Full;
     std::set<size_t> 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;
     uint32_t siphontrapTimeout = 0;

include/PetriParse/PNMLParser.h

@@ -79,6 +79,10 @@ class PNMLParser {
         return queries;
     }
 
+    void parseMarking(
+        const rapidxml::xml_document<>& doc,
+        PetriEngine::AbstractPetriNetBuilder* builder,
+        ColorTypeMap* colorTypes);
 private:
     void parseElement(rapidxml::xml_node<>* element);
     void parsePlace(rapidxml::xml_node<>* element);

include/utils/structures/shared_string.h

@@ -14,6 +14,7 @@
 #include <string>
 #include <memory>
 #include <algorithm>
+#include <cstdint>
 
 typedef const std::string const_string;
 typedef std::shared_ptr<const_string> shared_const_string;

src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp

@@ -35,9 +35,12 @@ namespace PetriEngine {
 
     ColoredPetriNetBuilder::~ColoredPetriNetBuilder() {
         // cleaning up colors
-        for(auto& e : _colors)
-            if(e.second != Colored::ColorType::dotInstance())
-                delete e.second;
+        if (_ownsColors)
+        {
+            for(auto& e : _colors)
+                if(e.second != Colored::ColorType::dotInstance())
+                    delete e.second;
+        }
         for(auto& v : _variables)
             delete v;
         _colors.clear();