Merge lp:~tapaal-dist-ctl/verifypn/verifypn-conf-opti into lp:~verifypn-maintainers/verifypn/trunk

[Søren Moss Nielsen]

===============================================================
:::::::::::::::: Configuration optimization :::::::::::::::::::
===============================================================
Setup:
   - TIMEOUT: 60sec
   - ModelDB size: 78
   - Total possible answers: 1248

Base:
   //The current trunk as of commit 79
   ANSWERS: 927

New version
   ANSWERS: 935

[Jiri Srba (srba)]

review: Approve

=== modified file 'CTL/DependencyGraph.h'
--- CTL/DependencyGraph.h	2016-03-31 11:56:31 +0000
+++ CTL/DependencyGraph.h	2016-04-13 16:24:44 +0000
@@ -31,7 +31,7 @@
     void initialize(CTLTree &t_query);
 
 protected:
-    CTLTree *_query;
+    CTLTree *_query = nullptr;
     PetriEngine::PetriNet *_petriNet;
     PetriEngine::MarkVal *_initialMarking;
     PNMLParser::InhibitorArcList _inhibitorArcs;

=== modified file 'CTL/OnTheFlyDG.cpp'
--- CTL/OnTheFlyDG.cpp	2016-04-12 12:11:40 +0000
+++ CTL/OnTheFlyDG.cpp	2016-04-13 16:24:44 +0000
@@ -5,7 +5,10 @@
 namespace ctl{
 
 OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, PetriEngine::MarkVal *t_initial, PNMLParser::InhibitorArcList inhibitorArcs):
-    DependencyGraph(t_net, t_initial, inhibitorArcs){_compressoption = false;}
+    DependencyGraph(t_net, t_initial, inhibitorArcs)
+{
+    _compressoption = false;
+}
 
 
 bool OnTheFlyDG::fastEval(CTLTree &query, Marking &marking) {
@@ -303,8 +306,9 @@
 
 Configuration &OnTheFlyDG::initialConfiguration()
 {
-    Marking *initial = new Marking(_initialMarking, _nplaces);
-    return *createConfiguration(*initial, *_query);
+    Markings.insert(&initial_marking);
+    Configuration* initial = createConfiguration(initial_marking, *_query);
+    return *initial;
 }
 
 bool OnTheFlyDG::evaluateQuery(CTLTree &query, Marking &marking){
@@ -437,10 +441,28 @@
 
 void OnTheFlyDG::clear(bool t_clear_all)
 {
-    for(auto c : Configurations){
-        delete c;
+//    int i = 0;
+//    int max_i = Markings.size();
+    for(Marking *m : Markings){
+//        printf("Cleaning up marking %d of %d: ", ++i, max_i);
+//        m->print();
+//        printf("\n");
+
+//        if(m == &initial_marking)
+//            printf("Successor count: %d\n",(int) m->successors.size());
+        for(Configuration *c : m->successors){
+//            c->configPrinter();
+            delete c;
+        }
+
+        m->successors.resize(0);
     }
-    Configurations.clear();
+//    printf("Done Cleaning Configurations\n");
+
+//    for(Configuration *c : Configurations){
+//        delete c;
+//    }
+//    Configurations.clear();
 
     if(t_clear_all){
         for(auto m : Markings){
@@ -452,6 +474,11 @@
 
 Configuration *OnTheFlyDG::createConfiguration(Marking &t_marking, CTLTree &t_query)
 {
+    for(Configuration* c : t_marking.successors){
+        if(c->query == &t_query)
+            return c;
+    }
+
     Configuration* newConfig = new Configuration();
     newConfig->marking = &t_marking;
     newConfig->query = &t_query;
@@ -460,13 +487,17 @@
     if(t_query.quantifier == NEG){
         newConfig->IsNegated = true;
     }
-    auto pair = Configurations.insert(newConfig);
-
-    if(!pair.second) {
-        delete newConfig;
-    }
-
-    return *(pair.first);
+
+    t_marking.successors.push_back(newConfig);
+    return newConfig;
+
+    //auto pair = Configurations.insert(newConfig);
+
+//    if(!pair.second) {
+//        delete newConfig;
+//    }
+
+//    return *(pair.first);
 }
 
 

=== modified file 'CTL/OnTheFlyDG.h'
--- CTL/OnTheFlyDG.h	2016-04-12 08:29:03 +0000
+++ CTL/OnTheFlyDG.h	2016-04-13 16:24:44 +0000
@@ -22,18 +22,18 @@
     std::list<Edge *> successors(Configuration &v);
     Configuration &initialConfiguration();
     void clear(bool t_clear_all);
-    int configuration_count() { return Configurations.size();}
+    int configuration_count() { return 0;/*Configurations.size();*/}
     int marking_count() { return Markings.size(); }
 
-
+    Marking initial_marking = Marking(_initialMarking, _nplaces);
     boost::unordered_set< Marking*,
                         boost::hash<Marking*>,
                         Marking::Marking_Equal_To> Markings;
 
-    boost::unordered_set< Configuration*,
-                        boost::hash<Configuration*>,
-                        Configuration::Configuration_Equal_To> Configurations;
-    bool isCompressing() {return _compressoption;};
+//    boost::unordered_set< Configuration*,
+//                        boost::hash<Configuration*>,
+//                        Configuration::Configuration_Equal_To> Configurations;
+    bool isCompressing() {return _compressoption;}
                         
 protected:
     bool evaluateQuery(CTLTree &query, Marking &marking);

=== modified file 'CTL/marking.h'
--- CTL/marking.h	2016-04-07 13:20:00 +0000
+++ CTL/marking.h	2016-04-13 16:24:44 +0000
@@ -15,8 +15,11 @@
 //inline functions to make the class
 //act/look/feel like an array.
 
+class Configuration;
+
 class Marking
 {
+    typedef std::vector<Configuration*> succ_container_type;
     public:
     // Equality checker for containers
     // with pointers to markings
@@ -28,7 +31,7 @@
 
     Marking(){}
     Marking(PetriEngine::MarkVal* t_marking, size_t t_length)
-        : m_marking(t_marking), m_length(t_length){}
+        : m_marking(t_marking), m_length(t_length){ }
 
     virtual ~Marking(){ free(m_marking); }
 
@@ -43,6 +46,7 @@
     inline PetriEngine::MarkVal* Value() const {return m_marking;}
     void print() const;
     inline size_t Length() const {return m_length;}
+    succ_container_type successors;
 private:
     PetriEngine::MarkVal* m_marking;
     size_t m_length;