Merge lp:~verifypn-stub/verifypn/ctl-structural into lp:verifypn

[Peter Gjøl Jensen]

Adds structural reductions to the CTL verification -- only enabled if the formulas are next-free.
Also adds partial order reduction to EF leafs in CTL verification, although only yielding a minor speedup.

Consistent on 2017 models.
Improvements;

CTLCardinality:
r180: 3916
r187: 3922
r188: 3999
trunk: 4154
this: 4201

CTLFireability:
r180: 3111
r187: 3171
r188: 3248
trunk: 3575
this: 3655

[Jiri Srba (srba)]

The switch that disables partial order reduction should be active also
for CTL verification for EF and AG leafs.

review: Needs Fixing

[lp:~verifypn-stub/verifypn/ctl-structural]

224. By Peter Gjøl Jensen on 2018-01-04

propagating switch for po-reduction to ctl-engine

[Jiri Srba (srba)]

Please, fix the warning:

CTL/PetriNets/OnTheFlyDG.cpp:24:9: warning: field '_redgen' will be initialized after field
      '_partial_order' [-Wreorder]
        _redgen(*t_net), _partial_order(partial_order) {
        ^

review: Needs Fixing

[lp:~verifypn-stub/verifypn/ctl-structural]

225. By Peter Gjøl Jensen on 2018-01-04

fixed reorder warning

[Jiri Srba (srba)]

review: Approve

=== modified file 'CTL/CTLEngine.cpp'
--- CTL/CTLEngine.cpp	2017-12-04 13:45:29 +0000
+++ CTL/CTLEngine.cpp	2018-01-04 10:26:07 +0000
@@ -66,7 +66,6 @@
         cout << "	Processed Edges   : " << result.processedEdges << endl;
         cout << "	Processed N. Edges: " << result.processedNegationEdges << endl;
         cout << "	Explored Configs  : " << result.exploredConfigurations << endl;
-        if(!only_stats) result.query->toString(cout);
         std::cout << endl;
     }
 }
@@ -77,6 +76,7 @@
                     bool gamemode,
                     bool printstatistics,
                     bool mccoutput,
+                    bool partial_order,
                     const std::vector<std::string>& querynames,
                     const std::vector<std::shared_ptr<Condition>>& queries,
                     const std::vector<size_t>& querynumbers
@@ -90,7 +90,7 @@
 
     for(auto qnum : querynumbers){
         CTLResult result(queries[qnum]);
-        PetriNets::OnTheFlyDG graph(net); 
+        PetriNets::OnTheFlyDG graph(net, partial_order); 
         graph.setQuery(result.query);
         std::shared_ptr<Algorithm::FixedPointAlgorithm> alg = nullptr;
         bool solved = false;
 
=== modified file 'CTL/CTLEngine.h'
--- CTL/CTLEngine.h	2017-11-26 13:43:04 +0000
+++ CTL/CTLEngine.h	2018-01-04 10:26:07 +0000
@@ -16,6 +16,7 @@
                     bool gamemode,
                     bool printstatistics,
                     bool mccoutput,
+                    bool partial_order,
                     const std::vector<std::string>& querynames,
                     const std::vector<std::shared_ptr<PetriEngine::PQL::Condition>>& reducedQueries,
                     const std::vector<size_t>& ids);
 
=== modified file 'CTL/PetriNets/OnTheFlyDG.cpp'
--- CTL/PetriNets/OnTheFlyDG.cpp	2017-11-29 21:20:21 +0000
+++ CTL/PetriNets/OnTheFlyDG.cpp	2018-01-04 10:26:07 +0000
@@ -18,9 +18,10 @@
 
 namespace PetriNets {
 
-OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net) : encoder(t_net->numberOfPlaces(), 0), 
+OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encoder(t_net->numberOfPlaces(), 0), 
         edge_alloc(new linked_bucket_t<DependencyGraph::Edge,1024*10>(1)), 
-        conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)) {
+        conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)),
+        _redgen(*t_net), _partial_order(partial_order) {
     net = t_net;
     n_places = t_net->numberOfPlaces();
     n_transitions = t_net->numberOfTransitions();
@@ -37,7 +38,6 @@
     {
         ((PetriConfig*)&(*conf_alloc)[i])->~PetriConfig();
     }
-    std::cout << "NEDGES " << edge_alloc->size() << std::endl;
     delete conf_alloc;
     delete edge_alloc;
 }
@@ -176,7 +176,7 @@
                 if (valid || left != NULL) {
                     //if left side is guaranteed to be not satisfied, skip successor generation
                     Edge* leftEdge = NULL;
-                    nextStates (query_marking,
+                    nextStates (query_marking, cond,
                                 [&](){ leftEdge = newEdge(*v, std::numeric_limits<uint32_t>::max());},
                                 [&](Marking& mark){
                                     auto res = fastEval(cond, &mark);
@@ -227,7 +227,7 @@
                     subquery->addTarget(c);
                 }
                 Edge* e1 = NULL;
-                nextStates(query_marking,
+                nextStates(query_marking, cond,
                         [&](){e1 = newEdge(*v, std::numeric_limits<uint32_t>::max());},
                         [&](Marking& mark)
                         {
@@ -264,7 +264,7 @@
                 auto cond = static_cast<AXCondition*>(v->query);
                 Edge* e = newEdge(*v, std::numeric_limits<uint32_t>::max());
                 Condition::Result allValid = Condition::RTRUE;
-                nextStates(query_marking, 
+                nextStates(query_marking, cond,
                         [](){}, 
                         [&](Marking& mark){
                             auto res = fastEval((*cond)[0], &mark);
@@ -326,7 +326,7 @@
 
                 Configuration *left = NULL;
                 bool valid = false;
-                nextStates(query_marking, 
+                nextStates(query_marking, cond,
                     [&](){
                         auto r0 = fastEval((*cond)[0], &query_marking);
                         if (r0 == Condition::RUNKNOWN) {
@@ -389,7 +389,7 @@
                     subquery->addTarget(c);
                 }
 
-                nextStates(query_marking,
+                nextStates(query_marking, cond,
                             [](){},
                             [&](Marking& mark){
                                 auto res = fastEval(cond, &mark);
@@ -424,7 +424,7 @@
             else if(v->query->getPath() == X){
                 auto cond = static_cast<EXCondition*>(v->query);
                 auto query = (*cond)[0];
-                nextStates(query_marking, 
+                nextStates(query_marking, cond,
                         [](){}, 
                         [&](Marking& marking) {
                             auto res = fastEval(query, &marking);
@@ -478,25 +478,24 @@
     return initial_config;
 }
 
-void OnTheFlyDG::nextStates(Marking& t_marking, 
+
+void OnTheFlyDG::nextStates(Marking& t_marking, Condition* ptr,
     std::function<void ()> pre, 
     std::function<bool (Marking&)> foreach, 
     std::function<void ()> post)
 {
-
     bool first = true;
-    PetriEngine::SuccessorGenerator PNGen(*net);
-    PNGen.prepare(&query_marking);
     memcpy(working_marking.marking(), query_marking.marking(), n_places*sizeof(PetriEngine::MarkVal));    
-
-    
-    while(PNGen.next(working_marking)){
-        if(first) pre();
-        first = false;
-        if(!foreach(working_marking))
-        {
-            break;
-        }
+    auto qf = static_cast<QuantifierCondition*>(ptr);
+    if(!_partial_order || ptr->getQuantifier() != E || ptr->getPath() != F || (*qf)[0]->isTemporal())
+    {
+        PetriEngine::SuccessorGenerator PNGen(*net);
+        dowork<PetriEngine::SuccessorGenerator>(PNGen, first, pre, foreach);
+    }
+    else
+    {
+        _redgen.setQuery(ptr);
+        dowork<PetriEngine::ReducingSuccessorGenerator>(_redgen, first, pre, foreach);
     }
 
     if(!first) post();
 
=== modified file 'CTL/PetriNets/OnTheFlyDG.h'
--- CTL/PetriNets/OnTheFlyDG.h	2017-11-26 22:46:37 +0000
+++ CTL/PetriNets/OnTheFlyDG.h	2018-01-04 10:26:07 +0000
@@ -12,6 +12,7 @@
 #include "PetriEngine/Structures/ptrie_map.h"
 #include "PetriEngine/Structures/AlignedEncoder.h"
 #include "PetriEngine/Structures/linked_bucket.h"
+#include "PetriEngine/ReducingSuccessorGenerator.h"
 
 namespace PetriNets {
 class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
@@ -20,7 +21,7 @@
     using Condition = PetriEngine::PQL::Condition;
     using Condition_ptr = PetriEngine::PQL::Condition_ptr;
     using Marking = PetriEngine::Structures::State;
-    OnTheFlyDG(PetriEngine::PetriNet *t_net);
+    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
 
     virtual ~OnTheFlyDG();
 
@@ -57,7 +58,6 @@
     uint32_t n_places = 0;
     size_t _markingCount = 0;
     size_t _configurationCount = 0;
-
     //used after query is set
     Condition_ptr query = nullptr;
 
@@ -66,10 +66,27 @@
     {
         return fastEval(query.get(), unfolded);
     }
-    void nextStates(Marking& t_marking, 
+    void nextStates(Marking& t_marking, Condition*,
     std::function<void ()> pre, 
     std::function<bool (Marking&)> foreach, 
     std::function<void ()> post);
+    template<typename T>
+    void dowork(T& gen, bool& first, 
+    std::function<void ()>& pre, 
+    std::function<bool (Marking&)>& foreach)
+    {
+        gen.prepare(&query_marking);
+
+        while(gen.next(working_marking)){
+            if(first) pre();
+            first = false;
+            if(!foreach(working_marking))
+            {
+                gen.reset();
+                break;
+            }
+        }
+    }
     PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
     PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
     {
@@ -86,7 +103,12 @@
 
     // Problem  with linked bucket and complex constructor
     linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
-        
+    
+    PetriEngine::ReducingSuccessorGenerator _redgen;
+    bool _partial_order = false;
+
 };
+
+
 }
 #endif // ONTHEFLYDG_H
 
=== modified file 'PetriEngine/PQL/Expressions.cpp'
--- PetriEngine/PQL/Expressions.cpp	2017-12-14 08:59:40 +0000
+++ PetriEngine/PQL/Expressions.cpp	2018-01-04 10:26:07 +0000
@@ -2997,11 +2997,13 @@
         }
         
         void SimpleQuantifierCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
-            // Not implemented
+            _cond->findInteresting(generator, negated);
         }
         
         void UntilCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
-            // Not implemented
+            _cond1->findInteresting(generator, negated);
+            _cond1->findInteresting(generator, !negated);
+            _cond2->findInteresting(generator, negated);
         }
         
         void AndCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
 
=== modified file 'PetriEngine/PQL/Expressions.h'
--- PetriEngine/PQL/Expressions.h	2017-12-13 14:17:08 +0000
+++ PetriEngine/PQL/Expressions.h	2018-01-04 10:26:07 +0000
@@ -254,6 +254,7 @@
             bool isUpperBound() override;
             void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
             virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
+            virtual bool containsNext() const override { return _cond->containsNext(); }
         private:
             virtual std::string op() const = 0;
             
@@ -272,7 +273,7 @@
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override;
-            
+            bool containsNext() const override { return true; }            
         private:
             std::string op() const override;
         };
@@ -324,6 +325,7 @@
             Quantifier getQuantifier() const override { return Quantifier::A; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override;
+            bool containsNext() const override { return true; }
         private:
             std::string op() const override;
         };
@@ -385,7 +387,7 @@
             { if(i == 0) return _cond1; return _cond2;}
             Path getPath() const override             
             { return Path::U; }
-
+            bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
         private:
             virtual std::string op() const = 0; 
             
@@ -463,6 +465,9 @@
             { return _compiled->getQueryType(); }
             int formulaSize() const override
             { return _compiled->formulaSize(); }
+            bool containsNext() const override
+            { return false; }
+
         private:
             std::string _name;
             Condition_ptr _compiled;
@@ -503,6 +508,8 @@
             auto end() const { return _conds.end(); }
             bool empty() const { return _conds.size() == 0; }
             bool singular() const { return _conds.size() == 1; }
+            bool containsNext() const override 
+            { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
         protected:
             LogicalCondition() {};
             Retval simplifyOr(SimplificationContext& context) const;
@@ -632,6 +639,8 @@
                                     (_constraints[0]._lower == 0 || 
                                      _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
             };
+            bool containsNext() const override { return false;}
+
         private:
             std::vector<cons_t> _constraints;
             bool _negated = false;
@@ -665,6 +674,7 @@
                 if(id == 0) return _expr1;
                 else return _expr2;
             }
+            bool containsNext() const override { return false; }
         protected:
             uint32_t _distance(DistanceContext& c, 
                     std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
@@ -825,6 +835,7 @@
             CTLType getQueryType() const override { return CTLType::LOPERATOR; }
             const Condition_ptr& operator[](size_t i) const { return _cond; };
             virtual bool isTemporal() const override { return _temporal;}
+            bool containsNext() const override { return _cond->containsNext(); }
 
         private:
             Condition_ptr _cond;
@@ -864,6 +875,7 @@
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override { return Path::pError; }
             CTLType getQueryType() const override { return CTLType::EVAL; }
+            bool containsNext() const override { return false; }
         private:
             const bool _value;
         };
@@ -894,6 +906,7 @@
             Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
             Path getPath() const override { return Path::pError; }
             CTLType getQueryType() const override { return CTLType::EVAL; }
+            bool containsNext() const override { return false; }
         };
 
     }
 
=== modified file 'PetriEngine/PQL/PQL.h'
--- PetriEngine/PQL/PQL.h	2017-12-11 08:24:36 +0000
+++ PetriEngine/PQL/PQL.h	2018-01-04 10:26:07 +0000
@@ -289,7 +289,7 @@
             virtual Path getPath() const = 0;
             static std::shared_ptr<Condition> 
             initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated);
-            
+            virtual bool containsNext() const = 0;            
         protected:
             //Value for checking if condition is trivially true or false.
             //0 is undecided (default), 1 is true, 2 is false.
 
=== modified file 'PetriEngine/PetriNetBuilder.cpp'
--- PetriEngine/PetriNetBuilder.cpp	2017-12-08 12:21:38 +0000
+++ PetriEngine/PetriNetBuilder.cpp	2018-01-04 10:26:07 +0000
@@ -395,7 +395,8 @@
         QueryPlaceAnalysisContext placecontext(getPlaceNames(), getTransitionNames(), net);
         for(uint32_t i = 0; i < queries.size(); ++i)
         {
-            if(results[i] == Reachability::ResultPrinter::Unknown)
+            if(results[i] == Reachability::ResultPrinter::Unknown ||
+               results[i] == Reachability::ResultPrinter::CTL )
             {
                 queries[i]->analyze(placecontext);        
             }
 
=== modified file 'PetriEngine/PetriNetBuilder.h'
--- PetriEngine/PetriNetBuilder.h	2017-12-08 13:28:43 +0000
+++ PetriEngine/PetriNetBuilder.h	2018-01-04 10:26:07 +0000
@@ -112,6 +112,10 @@
             return reducer.RuleE();
         }
         
+        size_t RuleF() const {
+            return reducer.RuleF();
+        }
+        
         Reducer* getReducer() { return &reducer; }
         
         std::vector<std::pair<std::string, uint32_t>> orphanPlaces() const {
 
=== modified file 'PetriEngine/Reducer.cpp'
--- PetriEngine/Reducer.cpp	2017-12-08 13:34:25 +0000
+++ PetriEngine/Reducer.cpp	2018-01-04 10:26:07 +0000
@@ -10,11 +10,12 @@
 #include "PetriNetBuilder.h"
 #include <PetriParse/PNMLParser.h>
 #include <queue>
+#include <set>
 
 namespace PetriEngine {
 
     Reducer::Reducer(PetriNetBuilder* p) 
-    : _removedTransitions(0), _removedPlaces(0), _ruleA(0), _ruleB(0), _ruleC(0), _ruleD(0), _ruleE(0), parent(p) {
+    : _removedTransitions(0), _removedPlaces(0), _ruleA(0), _ruleB(0), _ruleC(0), _ruleD(0), _ruleE(0), _ruleF(0), parent(p) {
     }
 
     Reducer::~Reducer() {
@@ -180,12 +181,14 @@
             assert(!t.skip || (t.pre.size() == 0 && t.post.size() == 0));
             for(Arc& a : t.pre)
             {
+                assert(a.weight > 0);
                 Place& p = parent->_places[a.place];
                 assert(!p.skip);
                 assert(std::find(p.consumers.begin(), p.consumers.end(), i) != p.consumers.end());
             }
             for(Arc& a : t.post)
             {
+                assert(a.weight > 0);
                 Place& p = parent->_places[a.place];
                 assert(!p.skip);
                 assert(std::find(p.producers.begin(), p.producers.end(), i) != p.producers.end());
@@ -239,14 +242,10 @@
 
             // A2. we have more/less than one arc in pre or post
             // checked first to avoid out-of-bounds when looking up indexes.
-            if(trans.pre.size() != 1 || trans.post.size() != 1) continue;
+            if(trans.pre.size() != 1) continue;
 
             uint32_t pPre = trans.pre[0].place;
-            uint32_t pPost = trans.post[0].place;
-            
-            // A1. continue if source and destination are the same
-            if (pPre == pPost) continue;
-            
+                        
             // A2. Check that pPre goes only to t
             if(parent->_places[pPre].consumers.size() != 1) continue;
             
@@ -255,10 +254,21 @@
             if(trans.pre[0].weight != 1 || trans.post[0].weight < 1) continue;
                         
             // A4. Do inhibitor check, neither T, pPre or pPost can be involved with any inhibitor
-            if(parent->_places[pPre].inhib || parent->_places[pPost].inhib || trans.inhib) continue;
-
+            if(parent->_places[pPre].inhib|| trans.inhib) continue;
+            
             // A5. dont mess with query!
-            if(placeInQuery[pPre] > 0 || placeInQuery[pPost]) continue;
+            if(placeInQuery[pPre] > 0) continue;
+            // check A1, A4 and A5 for post
+            bool ok = true;
+            for(auto& pPost : trans.post)
+            {
+                if(parent->_places[pPost.place].inhib || pPre == pPost.place || placeInQuery[pPost.place] > 0)
+                {
+                    ok = false;
+                    break;
+                }
+            }
+            if(!ok) continue;
             
             continueReductions = true;
             _ruleA++;
@@ -280,40 +290,45 @@
                 }                
             }
             
-            size_t weight = trans.post[0].weight;
-            
-            // UA2. move the token for the initial marking, makes things simpler.
-            parent->initialMarking[pPost] += (parent->initialMarking[pPre] * weight);
+            for(auto& pPost : trans.post)
+            {
+                // UA2. move the token for the initial marking, makes things simpler.
+                parent->initialMarking[pPost.place] += (parent->initialMarking[pPre] * pPost.weight);
+            }
             parent->initialMarking[pPre] = 0;
 
             // Remove transition t and the place that has no tokens in m0
             // UA1. remove transition
+            auto toMove = trans.post;
             skipTransition(t);
-            assert(pPost != pPre);
 
             // UA2. update arcs
             for(auto& _t : parent->_places[pPre].producers)
             {
-                assert(pPre != pPost);
                 assert(_t != t);
                 // move output-arcs to post.
-                Transition& trans = getTransition(_t);
-                auto source = getOutArc(trans, pPre);
-                assert(source != trans.pre.end());
-                auto dest = getOutArc(trans, pPost);
-                if(dest == trans.post.end())
-                {
-                    source->place = pPost;
-                    source->weight *= weight;
-                    parent->_places[pPost].producers.push_back(_t);
-
-                    std::sort(trans.post.begin(), trans.post.end());
-                    std::sort(  parent->_places[pPost].producers.begin(), 
-                                parent->_places[pPost].producers.end());
-                }
-                else
-                {
-                    dest->weight += (source->weight * weight);
+                Transition& src = getTransition(_t);
+                auto source = *getOutArc(src, pPre);
+                for(auto& pPost : toMove)
+                {
+                    Arc a;
+                    a.place = pPost.place;
+                    a.weight = source.weight * pPost.weight;
+                    assert(a.weight > 0);
+                    a.inhib = false;
+                    auto dest = std::lower_bound(src.post.begin(), src.post.end(), a);
+                    if(dest == src.post.end() || dest->place != pPost.place)
+                    {
+                        dest = src.post.insert(dest, a);
+                        auto& prod = parent->_places[pPost.place].producers;
+                        auto lb = std::lower_bound(prod.begin(), prod.end(), _t);
+                        prod.insert(lb, _t);
+                    }
+                    else
+                    {
+                        dest->weight += (source.weight * pPost.weight);
+                    }
+                    assert(dest->weight > 0);
                 }
             }                
             // UA1. remove place
@@ -714,7 +729,8 @@
             if(placeInQuery[p] > 0) continue;
             if(place.producers.size() > place.consumers.size()) continue;
             
-            bool ok = true;
+            std::set<uint32_t> notenabled;
+            bool ok = true;            
             for(uint cons : place.consumers)
             {
                 Transition& t = getTransition(cons);
@@ -723,12 +739,21 @@
                     ok = false;
                     break;
                 }               
+                else
+                {
+                    notenabled.insert(cons);
+                }
             }
             
             if(!ok) continue;
-            
+
             for(uint prod : place.producers)
             {
+                if(notenabled.count(prod) == 0)
+                {
+                    ok = false;
+                    break;
+                }
                 // check that producing arcs originate from transition also 
                 // consuming. If so, we know it will never fire.
                 Transition& t = getTransition(prod);
@@ -741,24 +766,63 @@
             }
             
             if(!ok) continue;
+
+            _ruleE++;
+            continueReductions = true;
             
             parent->initialMarking[p] = 0;
             
-            auto torem = place.consumers;
-            for(uint cons : torem)
-            {
+            bool skipplace = notenabled.size() == place.consumers.size();
+            for(uint cons : notenabled)
                 skipTransition(cons);
+
+            if(skipplace)
+                skipPlace(p);
+            
+        }
+        assert(consistent());
+        return continueReductions;
+    }
+   
+    bool Reducer::ReducebyRuleF(uint32_t* placeInQuery) {
+        bool continueReductions = false;
+        const size_t numberofplaces = parent->numberOfPlaces();
+        for(uint32_t p = 0; p < numberofplaces; ++p)
+        {
+            if(hasTimedout()) return false;
+            Place& place = parent->_places[p];
+            if(place.skip) continue;
+            if(place.inhib) continue;
+            if(placeInQuery[p] > 0) continue;
+            if(place.consumers.size() > 0) continue;
+            
+            ++_ruleF;
+            continueReductions = true;
+            skipPlace(p);
+            std::vector<uint32_t> torem;
+            for(auto& t : place.producers)
+            {
+                auto& trans = parent->_transitions[t];
+                if(trans.post.size() != 0)
+                    continue;
+                bool ok = true;
+                for(auto& a : trans.pre)
+                {
+                    if(placeInQuery[a.place] > 0)
+                    {
+                        ok = false;
+                    }
+                }
+                if(ok) torem.push_back(t);
             }
-
-            skipPlace(p);
-            _ruleE++;
-            continueReductions = true;
+            
+            for(auto t : torem)
+                skipTransition(t);
+            assert(consistent());
         }
-        assert(consistent());
         return continueReductions;
     }
 
-
     void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout) {
         this->_timeout = timeout;
         _timer = std::chrono::high_resolution_clock::now();
@@ -773,11 +837,12 @@
                     changed |= ReducebyRuleA(context.getQueryPlaceCount());
                     changed |= ReducebyRuleB(context.getQueryPlaceCount());
                     changed |= ReducebyRuleE(context.getQueryPlaceCount());
+                    changed |= ReducebyRuleF(context.getQueryPlaceCount());
                 } while(changed && !hasTimedout());
                 // RuleC and RuleD are expensive, so wait with those till nothing else changes
                 changed |= ReducebyRuleD(context.getQueryPlaceCount());
                 changed |= ReducebyRuleC(context.getQueryPlaceCount());
-            } while(changed);
+            } while(!hasTimedout() && changed);
 
         } else if (enablereduction == 2) { // for k-boundedness checking only rules A and D are applicable
             while ( (
 
=== modified file 'PetriEngine/Reducer.h'
--- PetriEngine/Reducer.h	2017-12-13 14:17:08 +0000
+++ PetriEngine/Reducer.h	2018-01-04 10:26:07 +0000
@@ -114,7 +114,11 @@
         size_t RuleE() const {
             return _ruleE;
         }
-        
+
+        size_t RuleF() const {
+            return _ruleF;
+        }
+
         void postFire(std::ostream&, const std::string& transition);
         void extraConsume(std::ostream&, const std::string& transition);
         void initFire(std::ostream&);
@@ -122,7 +126,7 @@
     private:
         size_t _removedTransitions;
         size_t _removedPlaces;
-        size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE;
+        size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE, _ruleF;
         PetriNetBuilder* parent;
         bool reconstructTrace = false;
         std::chrono::high_resolution_clock::time_point _timer;
@@ -134,6 +138,7 @@
         bool ReducebyRuleC(uint32_t* placeInQuery);
         bool ReducebyRuleD(uint32_t* placeInQuery);
         bool ReducebyRuleE(uint32_t* placeInQuery);
+        bool ReducebyRuleF(uint32_t* placeInQuery);
         
         std::string getTransitionName(uint32_t transition);
         std::string getPlaceName(uint32_t place);
 
=== modified file 'PetriEngine/ReducingSuccessorGenerator.cpp'
--- PetriEngine/ReducingSuccessorGenerator.cpp	2017-12-05 15:13:40 +0000
+++ PetriEngine/ReducingSuccessorGenerator.cpp	2018-01-04 10:26:07 +0000
@@ -18,7 +18,9 @@
     }
 
     ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : ReducingSuccessorGenerator(net) {
-        _queries = queries;
+        _queries.reserve(queries.size());
+        for(auto& q : queries)
+            _queries.push_back(q.get());
     }
 
     ReducingSuccessorGenerator::~ReducingSuccessorGenerator() {
@@ -182,6 +184,12 @@
     void ReducingSuccessorGenerator::prepare(const Structures::State* state) {
         _parent = state;
         constructEnabled();
+        if(_ordering.size() == 0) return;
+        if(_ordering.size() == 1)
+        {
+            _stubborn[_ordering.front()] = true;
+            return;
+        }
         for (auto &q : _queries) {
             q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
             q->findInteresting(*this, false);
 
=== modified file 'PetriEngine/ReducingSuccessorGenerator.h'
--- PetriEngine/ReducingSuccessorGenerator.h	2017-05-10 11:10:00 +0000
+++ PetriEngine/ReducingSuccessorGenerator.h	2018-01-04 10:26:07 +0000
@@ -29,6 +29,9 @@
     {
        return _current;
     }
+    void setQuery(PQL::Condition* ptr) { _queries.clear(); _queries = {ptr};}
+    void reset();
+
 private:
     bool *_enabled, *_stubborn;
     std::unique_ptr<place_t[]> _places;
@@ -39,8 +42,7 @@
     bool _netContainsInhibitorArcs;
     std::vector<std::vector<uint32_t>> _inhibpost;
     
-    std::vector<std::shared_ptr<PQL::Condition> > _queries;
-    void reset();
+    std::vector<PQL::Condition* > _queries;
     void constructEnabled();
     void constructPrePost();
     void constructDependency();
 
=== modified file 'PetriEngine/Structures/light_deque.h'
--- PetriEngine/Structures/light_deque.h	2017-03-05 16:08:26 +0000
+++ PetriEngine/Structures/light_deque.h	2018-01-04 10:26:07 +0000
@@ -48,6 +48,11 @@
             return _front == _back;
         }
         
+        size_t size()
+        {
+            return _back - _front;
+        }
+        
         T front()
         {
             return _data.get()[_front];
 
=== modified file 'PetriEngine/SuccessorGenerator.h'
--- PetriEngine/SuccessorGenerator.h	2017-12-05 02:09:55 +0000
+++ PetriEngine/SuccessorGenerator.h	2018-01-04 10:26:07 +0000
@@ -35,6 +35,8 @@
         return _parent->marking();
     }
 
+    void reset();
+    
 protected:
     /**
      * Checks if the conditions are met for fireing t, if write != NULL,
@@ -63,7 +65,6 @@
     const Structures::State* _parent;
     uint32_t _suc_pcounter;
     uint32_t _suc_tcounter;
-    void reset();
 
     friend class ReducingSuccessorGenerator;
 };
 
=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp	2017-12-12 10:13:45 +0000
+++ VerifyPN.cpp	2018-01-04 10:26:07 +0000
@@ -478,7 +478,8 @@
                         << "Applications of rule B: " << builder.RuleB() << std::endl
                         << "Applications of rule C: " << builder.RuleC() << std::endl
                         << "Applications of rule D: " << builder.RuleD() << std::endl
-                        << "Applications of rule E: " << builder.RuleE() << std::endl;
+                        << "Applications of rule E: " << builder.RuleE() << std::endl
+                        << "Applications of rule F: " << builder.RuleF() << std::endl;
         }
     }
 }
@@ -656,7 +657,26 @@
 
         if(alldone) return SuccessCode;
     }
-
+    
+    //--------------------- Apply Net Reduction ---------------//
+        
+    if ( (options.enablereduction == 1 || options.enablereduction == 2) 
+         && std::all_of(queries.begin(), queries.end(), [](auto& a){ return !a->containsNext(); })) {
+        // Compute how many times each place appears in the query
+        builder.startTimer();
+        builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout);
+        printer.setReducer(builder.getReducer());        
+    }
+    
+    printStats(builder, options);
+    
+    auto net = std::unique_ptr<PetriNet>(builder.makePetriNet());
+    
+    for(auto& q : queries)
+    {
+        q->indexPlaces(builder.getPlaceNames());
+    }
+    
     //----------------------- Verify CTL queries -----------------------//
     std::vector<size_t> ctl_ids;
     for(size_t i = 0; i < queries.size(); ++i)
@@ -670,24 +690,25 @@
     if (ctl_ids.size() > 0) {
         options.isctl=true;
         PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
-        std::unique_ptr<PetriNet> ctlnet(builder.makePetriNet());
+
         // Assign indexes
-        if(queries.size() == 0 || contextAnalysis(builder, ctlnet.get(), queries) != ContinueCode)  return ErrorCode;
+        if(queries.size() == 0 || contextAnalysis(builder, net.get(), queries) != ContinueCode)  return ErrorCode;
         if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::DFS;
         if(options.strategy != PetriEngine::Reachability::DFS){
             fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");
             options.strategy = PetriEngine::Reachability::DFS;
         }
-        v = CTLMain(ctlnet.get(),
+        v = CTLMain(net.get(),
             options.ctlalgorithm,
             options.strategy,
             options.gamemode,
             options.printstatistics,
             true,
+            options.stubbornreduction,
             querynames,
             queries,
             ctl_ids);
-                
+
         if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
             return v;
         }
@@ -695,24 +716,6 @@
         options.strategy=reachabilityStrategy;
     }
     options.isctl=false;
-    //--------------------- Apply Net Reduction ---------------//
-        
-    if (options.enablereduction == 1 || options.enablereduction == 2) {
-        // Compute how many times each place appears in the query
-        builder.startTimer();
-        std::unique_ptr<PetriNet> net(builder.makePetriNet(false));
-        builder.reduce(queries, results, options.enablereduction, options.trace, net.get(), options.reductionTimeout);
-        printer.setReducer(builder.getReducer());        
-    }
-    
-    printStats(builder, options);
-    
-    std::unique_ptr<PetriNet> net(builder.makePetriNet());
-    
-    for(auto& q : queries)
-    {
-        q->indexPlaces(builder.getPlaceNames());
-    }
     
     //----------------------- Siphon Trap ------------------------//