Use Linear Programming to initialize potencies

Scripts/MCC24/competition-scripts/tapaal.sh

@@ -87,9 +87,9 @@ STRATEGIES_RAND[1]="-s RDFS --seed-offset 1337 -q 0 -l 0 -d 0"
 STRATEGIES_RAND[2]="-s RPFS --seed-offset 2018 -q 0 -l 0 -d $SHORTRED"
 STRATEGIES_RAND[3]="-tar -s RDFS --seed-offset 9220 -q 0 -l 0 -d $SHORTRED"
 
-STRATEGIES_RW_RAND[0]="-s RandomWalk --seed-offset 0 -q 0 -l 0 -d 0"
+STRATEGIES_RW_RAND[0]="-s RandomWalk --seed-offset 0 -q 0 -l 0 -d 0 --init-potency-timeout 0"
 STRATEGIES_RW_RAND[1]="-s RandomWalk --seed-offset 1337 -q 0 -l 0 -d 5"
-STRATEGIES_RW_RAND[2]="-s RandomWalk --seed-offset 2018 -q 5 -l 2 -d 5"
+STRATEGIES_RW_RAND[2]="-s RandomWalk --seed-offset 2018 -q 5 -l 2 -d 5 --init-potency-timeout 0"
 STRATEGIES_RW_RAND[3]="-s RandomWalk --seed-offset 9220 -q 5 -l 3 -d 10"
 
 run_multi=false;
@@ -259,7 +259,7 @@ function verifyparallel {
     echo "---------------------------------------------------"
     echo "            Step 1: Parallel processing            "
     echo "---------------------------------------------------"
-    echo "Doing parallel verification of individual queries (on ${#QUERIES[@]} remaining queries)"
+    echo "Doing parallel verification of individual queries ($NUMBER in total)"
     echo "Each query is verified by ${#STRATEGIES_PAR[@]} parallel strategies for $TIMEOUT_PAR seconds"
 
     i=0

include/PetriEngine/PQL/Contexts.h

@@ -180,8 +180,9 @@ namespace PetriEngine {
 
             SimplificationContext(const MarkVal* marking,
                     const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
-                    Simplification::LPCache* cache)
-                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
+                    Simplification::LPCache* cache, uint32_t potencyTimeout = 0)
+                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout),
+                    _potencyTimeout(potencyTimeout) {
                 _negated = false;
                 _marking = marking;
                 _net = net;
@@ -225,27 +226,32 @@ namespace PetriEngine {
                 return (diff.count() >= _queryTimeout);
             }
 
+            bool potencyTimeout() const {
+                auto end = std::chrono::high_resolution_clock::now();
+                auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _start);
+                return (diff.count() >= _potencyTimeout);
+            }
+
             uint32_t getLpTimeout() const;
+            uint32_t getPotencyTimeout() const;
 
             Simplification::LPCache* cache() const
             {
                 return _cache;
             }
 
-
             glp_prob* makeBaseLP() const;
 
         private:
             bool _negated;
             const MarkVal* _marking;
             const PetriNet* _net;
-            uint32_t _queryTimeout, _lpTimeout;
+            uint32_t _queryTimeout, _lpTimeout, _potencyTimeout;
+            mutable glp_prob* _base_lp = nullptr;
             std::chrono::high_resolution_clock::time_point _start;
             Simplification::LPCache* _cache;
-            mutable glp_prob* _base_lp = nullptr;
 
             glp_prob* buildBase() const;
-
         };
 
     } // PQL

include/PetriEngine/PQL/PotencyVisitor.h

@@ -0,0 +1,119 @@
+/* Copyright (C) 2023  Malo Dautry
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_POTENCYVISITOR_H
+#define VERIFYPN_POTENCYVISITOR_H
+
+#include "Visitor.h"
+#include "PetriEngine/PQL/Simplifier.h"
+
+namespace PetriEngine { namespace PQL {
+
+    /**
+     * Copmutes the initial potencies of a query.
+     * It computes the lps equations along the AST, and solve the different
+     * systems of equations.
+     * The result is aggregated in the potencies.
+    */
+    void initPotencyVisit(std::shared_ptr<Condition> element, SimplificationContext& context,
+                          std::vector<uint32_t> &potencies,
+                          uint32_t maxConfigurationsSolved = std::numeric_limits<uint32_t>::max());
+
+    /**
+     * Visitor made to compute the initial potencies of a query.
+     * It computes the lps equations along the AST, and merge them into one object.
+     * The result is stored in the _return_value.lps attribute.
+     * It's up to the caller to solve the equations and aggregate the solutions.
+    */
+    class PotencyVisitor : public Visitor {
+
+    public:
+        explicit PotencyVisitor(SimplificationContext& context) :
+                _context(context) {}
+
+        RetvalPot get_return_value() { return std::move(_return_value); }
+
+    protected:
+        SimplificationContext& _context;
+        RetvalPot _return_value;
+
+        RetvalPot simplify_or(const LogicalCondition* element);
+        RetvalPot simplify_and(const LogicalCondition *element);
+
+        RetvalPot simplify_AG(RetvalPot &r);
+        RetvalPot simplify_AF(RetvalPot &r);
+        RetvalPot simplify_AX(RetvalPot &r);
+
+        RetvalPot simplify_EG(RetvalPot &r);
+        RetvalPot simplify_EF(RetvalPot &r);
+        RetvalPot simplify_EX(RetvalPot &r);
+
+        template <typename Quantifier>
+        RetvalPot simplify_simple_quantifier(RetvalPot &r);
+
+        void _accept(const NotCondition *element) override;
+
+        void _accept(const AndCondition *element) override;
+
+        void _accept(const OrCondition *element) override;
+
+        void _accept(const LessThanCondition *element) override;
+
+        void _accept(const LessThanOrEqualCondition *element) override;
+
+        void _accept(const EqualCondition *element) override;
+
+        void _accept(const NotEqualCondition *element) override;
+
+        void _accept(const DeadlockCondition *element) override;
+
+        void _accept(const CompareConjunction *element) override;
+
+        void _accept(const UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(const ControlCondition *condition) override;
+
+        void _accept(const EFCondition *condition) override;
+
+        void _accept(const EGCondition *condition) override;
+
+        void _accept(const AGCondition *condition) override;
+
+        void _accept(const AFCondition *condition) override;
+
+        void _accept(const EXCondition *condition) override;
+
+        void _accept(const AXCondition *condition) override;
+
+        void _accept(const EUCondition *condition) override;
+
+        void _accept(const AUCondition *condition) override;
+
+        void _accept(const GCondition *condition) override;
+
+        void _accept(const FCondition *condition) override;
+
+        void _accept(const XCondition *condition) override;
+
+        void _accept(const UntilCondition *condition) override;
+
+        void _accept(const BooleanCondition *element) override;
+
+        void _accept(const PathSelectCondition *element) override;
+    };
+
+} }
+#endif // VERIFYPN_POTENCYVISITOR_H

include/PetriEngine/PQL/Simplifier.h

@@ -25,6 +25,7 @@
 namespace PetriEngine { namespace PQL {
 
     Retval simplify(std::shared_ptr<Condition> element, SimplificationContext& context);
+    AbstractProgramCollection_ptr mergeLps(std::vector<AbstractProgramCollection_ptr> &&lps);
 
     class Simplifier : public Visitor {
 
@@ -111,6 +112,7 @@ namespace PetriEngine { namespace PQL {
         void _accept(const PathSelectCondition *element) override;
     };
 
+    Member memberForPlace(size_t p, const SimplificationContext &context);
     Member constraint(const Expr *element, const SimplificationContext &context);
 
     class ConstraintVisitor : public ExpressionVisitor {

include/PetriEngine/Reachability/ReachabilitySearch.h

@@ -64,7 +64,8 @@ namespace PetriEngine {
                     bool keep_trace,
                     size_t seed,
                     int64_t depthRandomWalk = 50000,
-                    const int64_t incRandomWalk = 5000);
+                    const int64_t incRandomWalk = 5000,
+                    const std::vector<MarkVal>& initPotencies = std::vector<MarkVal>());
             size_t maxTokens() const;
         private:
             struct searchstate_t {
@@ -83,15 +84,17 @@ namespace PetriEngine {
                 StatisticsLevel,
                 size_t seed,
                 int64_t depthRandomWalk,
-                const int64_t incRandomWalk);
+                const int64_t incRandomWalk,
+                const std::vector<MarkVal>& initPotencies);
 
             template<typename Q, typename W = Structures::StateSet, typename G>
             bool tryReach(
                 std::vector<std::shared_ptr<PQL::Condition > >& queries,
                 std::vector<ResultPrinter::Result>& results,
                 bool usequeries,
                 StatisticsLevel statisticsLevel,
-                size_t seed);
+                size_t seed,
+                const std::vector<MarkVal>& initPotencies);
 
             void printStats(searchstate_t& s, Structures::StateSetInterface*, StatisticsLevel);
 
@@ -127,7 +130,8 @@ namespace PetriEngine {
         template<typename Q, typename W, typename G>
         bool ReachabilitySearch::tryReach(std::vector<std::shared_ptr<PQL::Condition> >& queries,
                                         std::vector<ResultPrinter::Result>& results, bool usequeries,
-                                        StatisticsLevel statisticsLevel, size_t seed)
+                                        StatisticsLevel statisticsLevel, size_t seed,
+                                        const std::vector<MarkVal>& initPotencies)
         {
 
             // set up state
@@ -145,8 +149,14 @@ namespace PetriEngine {
             state.setMarking(_net.makeInitialMarking());
             working.setMarking(_net.makeInitialMarking());
 
-            W states(_net, _kbound);    // stateset
-            Q queue(seed);           // working queue
+            W states(_net, _kbound); // stateset
+
+            Q queue(seed); // Working queue
+            if constexpr (std::is_base_of_v<Structures::PotencyQueue, Q>) {
+                if (!initPotencies.empty())
+                    queue = Q(initPotencies, seed);
+            }
+
             G generator = _makeSucGen<G>(_net, queries); // successor generator
             auto r = states.add(state);
             // this can fail due to reductions; we push tokens around and violate K
@@ -221,7 +231,8 @@ namespace PetriEngine {
         bool ReachabilitySearch::tryReachRandomWalk(std::vector<std::shared_ptr<PQL::Condition> >& queries,
                                                     std::vector<ResultPrinter::Result>& results, bool usequeries,
                                                     StatisticsLevel statisticsLevel, size_t seed,
-                                                    int64_t depthRandomWalk, const int64_t incRandomWalk)
+                                                    int64_t depthRandomWalk, const int64_t incRandomWalk,
+                                                    const std::vector<MarkVal>& initPotencies)
         {
             // Set up state
             searchstate_t ss;
@@ -239,8 +250,8 @@ namespace PetriEngine {
             candidate.setMarking(_net.makeInitialMarking());
             currentStepState.setMarking(_net.makeInitialMarking());
 
-            Structures::RandomWalkStateSet states(_net, _kbound, query, seed); // State set
-            G generator = _makeSucGen<G>(_net, queries);                       // Successor generator
+            Structures::RandomWalkStateSet states(_net, _kbound, query, initPotencies, seed); // State set
+            G generator = _makeSucGen<G>(_net, queries); // Successor generator
 
             // Check initial marking
             if(ss.usequeries)

include/PetriEngine/Simplification/LinearProgram.h

@@ -10,10 +10,10 @@
 #include <unordered_set>
 #include <memory>
 #include <glpk.h>
-    
+
 namespace PetriEngine {
     namespace Simplification {
-        
+
         struct equation_t
         {
             double upper = std::numeric_limits<double>::infinity();
@@ -29,7 +29,7 @@ namespace PetriEngine {
                 return row < other.row;
             }
         };
-        
+
         class LinearProgram {
         private:
             enum result_t { UKNOWN, IMPOSSIBLE, POSSIBLE };
@@ -41,54 +41,51 @@ namespace PetriEngine {
                 std::swap(_result, other._result);
                 std::swap(_equations, other._equations);
             }
+
+            LinearProgram() {}
             virtual ~LinearProgram();
-            LinearProgram()
-            {
-            };
-
+
             LinearProgram(const LinearProgram& other)
-            : _result(other._result), _equations(other._equations)
-            {
-
-            }
-
+            : _result(other._result), _equations(other._equations) {}
+
             LinearProgram(Vector* vec, int constant, op_t op, LPCache* factory);
             size_t size() const
             {
                 return _equations.size();
             }
-            
+
             const std::vector<equation_t>& equations() const
             {
                 return _equations;
             }
-                       
+
             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);
+            void solvePotency(const PQL::SimplificationContext& context, std::vector<uint32_t>& potencies);
 
             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";
+                for (size_t i = 0; i < indent ; ++i) ss << "\t";
                 ss << "### LP\n";
-                
-                for(const equation_t& eq : _equations)
+
+                for (const equation_t& eq : _equations)
                 {
-                    for(size_t i = 0; i < indent ; ++i) ss << "\t";
+                    for (size_t i = 0; i < indent ; ++i) ss << "\t";
                     eq.row->print(ss);
                     ss << " IN [" << eq.lower << ", " << eq.upper << "]\n";
                 }
-                
-                for(size_t i = 0; i < indent ; ++i) ss << "\t";                
+
+                for (size_t i = 0; i < indent ; ++i) ss << "\t";
                 ss << "### LP DONE";
                 return ss;
             }
             static std::vector<std::pair<double,bool>> bounds(const PQL::SimplificationContext& context, uint32_t solvetime, const std::vector<uint32_t>& places);
         };
-    }   
+    }
 }
 
 #endif /* LINEARPROGRAM_H */
-