Merge lp:~verifypn-stub/verifypn/always_compile into lp:verifypn

[Peter Gjøl Jensen]

Added forced compilation via negationPush.
Without this, the dummy FireabilityConditions are not compiled into conjunctions over the places.

[lp:~verifypn-stub/verifypn/always_compile]

199. By Peter Gjøl Jensen on 2018-01-23

fixed bug in conjunction compilation

200. By Peter Gjøl Jensen on 2018-01-23

fixed conflicting flag detection

201. By Peter Gjøl Jensen on 2018-01-23

using return flags

202. By Peter Gjøl Jensen on 2018-01-23

removed debug

203. By Peter Gjøl Jensen on 2018-01-23

removed un-needed check

204. By Peter Gjøl Jensen on 2018-01-23

added error message

[Jiri Srba (srba)]

review: Approve

=== modified file 'CTL/PetriNets/OnTheFlyDG.cpp'
--- CTL/PetriNets/OnTheFlyDG.cpp	2018-01-04 10:18:59 +0000
+++ CTL/PetriNets/OnTheFlyDG.cpp	2018-01-23 19:36:42 +0000
@@ -519,9 +519,7 @@
     working_marking.setMarking(nullptr);
     query_marking.setMarking(nullptr);
     initialConfiguration();
-    negstat_t s;
-    EvaluationContext context(working_marking.marking(), net);    
-    this->query = query->pushNegation(s, context, false, false); // make sure that EG and AG is pushed
+    this->query = query;
     delete[] working_marking.marking();
     delete[] query_marking.marking();
     working_marking.setMarking(nullptr);

=== modified file 'PetriEngine/PQL/Expressions.cpp'
--- PetriEngine/PQL/Expressions.cpp	2018-01-04 10:06:58 +0000
+++ PetriEngine/PQL/Expressions.cpp	2018-01-23 19:36:42 +0000
@@ -94,7 +94,11 @@
                             if(conj->isNegated() == std::is_same<T, OrCondition>::value)
                                 _conds.insert(_conds.begin(), conj);
                             else
-                                _conds.insert(_conds.begin(), std::make_shared<CompareConjunction>(*conj, true));
+                            {
+                                auto next = std::make_shared<CompareConjunction>(std::is_same<T, OrCondition>::value);
+                                next->merge(*conj);
+                                _conds.insert(_conds.begin(), next);
+                            }
                         }
                     }
                     else

=== modified file 'PetriEngine/PQL/Expressions.h'
--- PetriEngine/PQL/Expressions.h	2017-12-13 14:19:34 +0000
+++ PetriEngine/PQL/Expressions.h	2018-01-23 19:36:42 +0000
@@ -587,9 +587,10 @@
                 }
             };
 
-            CompareConjunction() 
-            {};
+
         public:
+            CompareConjunction(bool negated = false) 
+                    : _negated(false) {};
             friend FireableCondition;
             CompareConjunction(const std::vector<cons_t>&& cons, bool negated) 
                     : _constraints(cons), _negated(negated) {};

=== modified file 'PetriEngine/Reducer.cpp'
--- PetriEngine/Reducer.cpp	2017-12-13 15:38:15 +0000
+++ PetriEngine/Reducer.cpp	2018-01-23 19:36:42 +0000
@@ -251,7 +251,7 @@
             
             // A3. We have weight of more than one on input
             // and is empty on output (should not happen).
-            if(trans.pre[0].weight != 1 || trans.post[0].weight < 1) continue;
+            if(trans.pre[0].weight != 1) continue;
                         
             // A4. Do inhibitor check, neither T, pPre or pPost can be involved with any inhibitor
             if(parent->_places[pPre].inhib|| trans.inhib) continue;

=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp	2018-01-13 20:49:50 +0000
+++ VerifyPN.cpp	2018-01-23 19:36:42 +0000
@@ -551,21 +551,24 @@
     ResultPrinter p2(&b2, &options, querynames);
 
     if(queries.size() == 0 || contextAnalysis(b2, qnet.get(), queries) != ContinueCode)  return ErrorCode;
-    
-    if (options.queryReductionTimeout > 0) {
+
+    if (options.strategy == PetriEngine::Reachability::OverApprox && options.queryReductionTimeout == 0)
+    { 
+        // Conflicting flags "-s OverApprox" and "-q 0"
+        std::cerr << "Conflicting flags '-s OverApprox' and '-q 0'" << std::endl;
+        return ErrorCode;
+    }
+
+    // simplification. We always want to do negation-push and initial marking check.
+    {
         LPCache cache;
         for(size_t i = 0; i < queries.size(); ++i)
         {
             if (queries[i]->isUpperBound()) continue;
             
-            SimplificationContext simplificationContext(qm0, qnet.get(), options.queryReductionTimeout, 
-                    options.lpsolveTimeout, &cache);
-            bool isInvariant = queries[i].get()->isInvariant();
-            
-            int preSize=queries[i]->formulaSize();
             negstat_t stats;            
             EvaluationContext context(qm0, qnet.get());
-            if(options.printstatistics)
+            if(options.printstatistics && options.queryReductionTimeout > 0)
             {
                 std::cout << "\nQuery before reduction: ";
                 queries[i]->toString(std::cout);
@@ -577,53 +580,60 @@
             
             queries[i] = Condition::initialMarkingRW([&](){ return queries[i]; }, stats,  context, false, false)
                                     ->pushNegation(stats, context, false, false);
-
-            if(options.printstatistics)
+            
+            if(options.queryReductionTimeout > 0)
             {
-                std::cout << "RWSTATS PRE:";
-                stats.print(std::cout);
-                std::cout << std::endl;
-            }
-
-            try {
-                negstat_t stats;            
-                queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(stats, context, false, false);
+                SimplificationContext simplificationContext(qm0, qnet.get(), options.queryReductionTimeout, 
+                        options.lpsolveTimeout, &cache);
+                bool isInvariant = queries[i].get()->isInvariant();
+
+                int preSize=queries[i]->formulaSize();
+
                 if(options.printstatistics)
                 {
-                    std::cout << "RWSTATS POST:";
+                    std::cout << "RWSTATS PRE:";
                     stats.print(std::cout);
                     std::cout << std::endl;
                 }
-                queries[i].get()->setInvariant(isInvariant);
-            } catch (std::bad_alloc& ba){
-                std::cerr << "Query reduction failed." << std::endl;
-                std::cerr << "Exception information: " << ba.what() << std::endl;
-                
-                delete[] qm0;
-                std::exit(3);
-            }
-
-            if(options.printstatistics)
-            {
-                std::cout << "\nQuery after reduction: ";
-                queries[i]->toString(std::cout);
-                std::cout << std::endl;
-            }
-            if(options.printstatistics){
-                int postSize=queries[i]->formulaSize();
-                double redPerc = preSize-postSize == 0 ? 0 : ((double)(preSize-postSize)/(double)preSize)*100;
-                
-                fprintf(stdout, "Query size reduced from %d to %d nodes (%.2f percent reduction).\n", preSize, postSize, redPerc);
-                if(simplificationContext.timeout()){
-                    fprintf(stdout, "Query reduction reached timeout.\n");
-                } else {
-                    fprintf(stdout, "Query reduction finished after %f seconds.\n", simplificationContext.getReductionTime());
+
+                try {
+                    negstat_t stats;            
+                    queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(stats, context, false, false);
+                    if(options.printstatistics)
+                    {
+                        std::cout << "RWSTATS POST:";
+                        stats.print(std::cout);
+                        std::cout << std::endl;
+                    }
+                    queries[i].get()->setInvariant(isInvariant);
+                } catch (std::bad_alloc& ba){
+                    std::cerr << "Query reduction failed." << std::endl;
+                    std::cerr << "Exception information: " << ba.what() << std::endl;
+
+                    delete[] qm0;
+                    std::exit(3);
+                }
+
+                if(options.printstatistics)
+                {
+                    std::cout << "\nQuery after reduction: ";
+                    queries[i]->toString(std::cout);
+                    std::cout << std::endl;
+                }
+                if(options.printstatistics){
+                    int postSize=queries[i]->formulaSize();
+                    double redPerc = preSize-postSize == 0 ? 0 : ((double)(preSize-postSize)/(double)preSize)*100;
+
+                    fprintf(stdout, "Query size reduced from %d to %d nodes (%.2f percent reduction).\n", preSize, postSize, redPerc);
+                    if(simplificationContext.timeout()){
+                        fprintf(stdout, "Query reduction reached timeout.\n");
+                    } else {
+                        fprintf(stdout, "Query reduction finished after %f seconds.\n", simplificationContext.getReductionTime());
+                    }
                 }
             }
         }
-    } else if (options.strategy == PetriEngine::Reachability::OverApprox){ // Conflicting flags "-s OverApprox" and "-q 0"
-        return 0;
-    }
+    } 
     
     qnet = nullptr;
     delete[] qm0;
@@ -737,7 +747,7 @@
         }
         
         if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
-            return 0;
+            return SuccessCode;
         }
     }
     
@@ -760,6 +770,6 @@
             options.printstatistics, 
             options.trace);
        
-    return 0;
+    return SuccessCode;
 }