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

[Søren Moss Nielsen]

Minor bug fix in main

===============================================================
::::::::::::::::::::Added BFS Strategy ::::::::::::::::::::::::
===============================================================
Setup:
   - TIMEOUT: 60sec
   - ModelDB size: 78
   - Total possible answers: 1248

Base(DFS):
   //The current trunk as of commit 65
   ANSWERS: 747

BFS
   ANSWERS: 606
   More specific statistics are communicated via E-mail
   (All answers are consistent

[Jiri Srba (srba)]

review: Approve

=== added file 'CTL/SearchStrategies/BreadthFirstSearch.cpp'
--- CTL/SearchStrategies/BreadthFirstSearch.cpp	1970-01-01 00:00:00 +0000
+++ CTL/SearchStrategies/BreadthFirstSearch.cpp	2016-04-10 10:18:24 +0000
@@ -0,0 +1,44 @@
+#include "BreadthFirstSearch.h"
+
+ctl::BreadthFirstSearch::BreadthFirstSearch()
+{
+
+}
+
+void ctl::BreadthFirstSearch::push(ctl::Edge *e)
+{
+    W.push_back(e);
+}
+
+void ctl::BreadthFirstSearch::push_dependency(ctl::Edge *e)
+{
+    W.push_back(e);
+}
+
+ctl::Edge *ctl::BreadthFirstSearch::pop()
+{
+    Edge *e = W.front();
+    W.pop_front();
+    return e;
+}
+
+bool ctl::BreadthFirstSearch::remove(ctl::Edge *e)
+{
+    iterator current = W.begin();
+    iterator end = W.end();
+
+    while(current != end){
+        if((*current) == e){
+            W.erase(current);
+            return true;
+        }
+    }
+
+    return false;
+}
+
+size_t ctl::BreadthFirstSearch::size() {return W.size();}
+
+bool ctl::BreadthFirstSearch::empty() {return W.empty();}
+
+void ctl::BreadthFirstSearch::clear(){ W.clear();}

=== added file 'CTL/SearchStrategies/BreadthFirstSearch.h'
--- CTL/SearchStrategies/BreadthFirstSearch.h	1970-01-01 00:00:00 +0000
+++ CTL/SearchStrategies/BreadthFirstSearch.h	2016-04-10 10:18:24 +0000
@@ -0,0 +1,28 @@
+#ifndef BREADTHFIRSTSEARCH_H
+#define BREADTHFIRSTSEARCH_H
+
+#include <deque>
+#include "AbstractSearchStrategy.h"
+
+namespace ctl{
+
+class BreadthFirstSearch : public ctl::AbstractSearchStrategy
+{
+public:
+    BreadthFirstSearch();
+
+    // AbstractSearchStrategy interface
+    void push(Edge *e);
+    void push_dependency(Edge *e);
+    Edge *pop();
+    bool remove(Edge *e);
+    size_t size();
+    bool empty();
+    void clear();
+
+private:
+    std::deque<Edge*> W; //Waiting list
+    typedef std::deque<Edge*>::iterator iterator;
+};
+}
+#endif // BREADTHFIRSTSEARCH_H

=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp	2016-04-06 12:58:00 +0000
+++ VerifyPN.cpp	2016-04-10 10:18:24 +0000
@@ -64,6 +64,7 @@
 
 #include "CTL/SearchStrategies/AbstractSearchStrategy.h"
 #include "CTL/SearchStrategies/DepthFirstSearch.h"
+#include "CTL/SearchStrategies/BreadthFirstSearch.h"
 
 using namespace std;
 using namespace PetriEngine;
@@ -170,6 +171,9 @@
     if(t_strategy == DFS){
         strategy = new ctl::DepthFirstSearch();
     }
+    else if (t_strategy == BFS){
+        strategy = new ctl::BreadthFirstSearch();
+    }
     else{
         fprintf(stderr, "Error: unsupported ctl search strategy");
         exit(EXIT_FAILURE);
@@ -420,9 +424,9 @@
 		// the default search strategy for CTL logic is DFS
 		searchstrategy = DFS;
 	}
-        if (isCTLlogic && searchstrategy != DFS) {
-		// for CTL logic only DFS strategy is supported		
-                fprintf(stderr, "Only DFS search strategy may be used with CTL logic.\n\n");
+        if (isCTLlogic && (searchstrategy != DFS && searchstrategy != BFS)) {
+		// for CTL logic only DFS and BFS strategy is supported		
+                fprintf(stderr, "Only DFS and BFS search strategy may be used with CTL logic.\n\n");
                 return ErrorCode;
 	}