Merge lp:~verifypn-cpn/verifypn/rulef-tracefix into lp:verifypn

[Peter Gjøl Jensen]

Fixed the attached bug.

Disabeling rule H if a trace is requested.
Adding missing "extraconsume" on transition when ruleF is applied.

[Jiri Srba (srba)]

If rule H is disabled because trace is selected, we should at least print this information
to stdout.

review: Needs Fixing

[lp:~verifypn-cpn/verifypn/rulef-tracefix]

217. By Peter Gjøl Jensen on 2019-03-28

added warning of disabled rule

218. By Peter Gjøl Jensen on 2019-03-28

switched to cout to avoid confusing the GUI

[Jiri Srba (srba)]

review: Approve

=== modified file 'PetriEngine/Reducer.cpp'
--- PetriEngine/Reducer.cpp	2018-05-17 18:59:24 +0000
+++ PetriEngine/Reducer.cpp	2019-03-28 13:54:47 +0000
@@ -972,6 +972,15 @@
             
             if((numberofplaces - _removedPlaces) > 1)
             {
+                if(reconstructTrace)
+                {
+                    for(auto t : place.consumers)
+                    {
+                        std::string tname = getTransitionName(t);
+                        const ArcIter arc = getInArc(p, getTransition(t));
+                        _extraconsume[tname].emplace_back(getPlaceName(p), arc->weight);
+                    }
+                }
                 skipPlace(p);
                 continueReductions = true;
             }
@@ -1066,6 +1075,8 @@
     
     bool Reducer::ReducebyRuleH(uint32_t* placeInQuery)
     {
+        if(reconstructTrace) 
+            return false; // we don't know where in the loop the tokens are needed
         bool continueReductions = false;
         for(uint32_t t1 = 0; t1 < parent->numberOfTransitions(); ++t1)
         {
@@ -1164,6 +1175,8 @@
         _timer = std::chrono::high_resolution_clock::now();
         assert(consistent());
         this->reconstructTrace = reconstructTrace;
+        if(reconstructTrace && enablereduction >= 1 && enablereduction <= 2)
+            std::cout << "Rule H disabled when a trace is requested." << std::endl;
         if (enablereduction == 1) { // in the aggressive reduction all four rules are used as long as they remove something
             bool changed = false;
             do