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

[Søren Moss Nielsen]

Merged in branch verifypn/new_deadlocksupport adding deadlock support.

The code for supporting deadlock queries, has been re-added in this new branch.

[Jiri Srba (srba)]

review: Approve

=== modified file 'CTL/OnTheFlyDG.cpp'
--- CTL/OnTheFlyDG.cpp	2016-08-04 10:59:43 +0000
+++ CTL/OnTheFlyDG.cpp	2016-08-29 09:42:25 +0000
@@ -360,6 +360,19 @@
         int second_param = GetParamValue(proposition->GetSecondParameter(), marking);
         return EvalCardianlity(first_param, proposition->GetLoperator(), second_param);
     }
+    else if (proposition->GetPropositionType() == DEADLOCK){
+        std::list<int> transistions = calculateFireableTransistions(marking);
+        std::list<int>::iterator it;
+        transistions.sort();
+
+        for(const auto f : proposition->GetFireset()){
+            it = std::find(transistions.begin(), transistions.end(), f);
+            if(it != transistions.end()){
+                return false;
+            }
+        }
+        return true;
+    }
     else
         assert(false && "Incorrect query proposition type was attempted evaluated");
 

=== modified file 'CTLParser/CTLParser_v2.cpp'
--- CTLParser/CTLParser_v2.cpp	2016-08-07 12:46:34 +0000
+++ CTLParser/CTLParser_v2.cpp	2016-08-29 09:42:25 +0000
@@ -337,9 +337,19 @@
         assert(query->GetQuantifier() == AND && "Failed setting and operator");
     }
     else if (firstLetter == 'd' ) {
-        //Construct disjunction
-        query = new CTLQuery(OR, pError, false, "");
-        assert(query->GetQuantifier() == OR && "Failed setting or operator");
+        if( root_name[1] == 'i' ){
+            //Construct disjunction
+            query = new CTLQuery(OR, pError, false, "");
+            assert(query->GetQuantifier() == OR && "Failed setting or operator");
+        }
+        else if (root_name[1] == 'e'){
+            //Deadlock query
+            std::string atom_str = root->name();
+            query = new CTLQuery(EMPTY, pError, true, atom_str);
+            query->Depth = 0;
+            return query;
+        }
+        else assert(false && "Failed parsing .xml file provided. Incorrect format.");
     }
     else if (firstLetter == 'i' ) {
         //Construct Atom

=== modified file 'CTLParser/EvaluateableProposition.cpp'
--- CTLParser/EvaluateableProposition.cpp	2016-08-04 10:59:43 +0000
+++ CTLParser/EvaluateableProposition.cpp	2016-08-29 09:42:25 +0000
@@ -83,6 +83,11 @@
         _secondParameter->isPlace = false;
         _secondParameter->value = 1;
     }
+    else if(a.substr(0,2).compare("de") == 0){
+        _type = DEADLOCK;
+        _loperator = NOT_CARDINALITY;
+        SetFireset("all", net->transitionNames(), net->numberOfTransitions());
+    }
     else{
         assert(false && "Atomic string proposed for proposition could not be parsed");
     }
@@ -101,12 +106,20 @@
 }
 
 std::vector<int> EvaluateableProposition::GetFireset() {
-    assert(_type == FIREABILITY && "Proposition is not a fireability proposition");
+    assert((_type == FIREABILITY || _type == DEADLOCK) && "Proposition is not a fireability proposition");
     return _fireset;
 }
 
 void EvaluateableProposition::SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t){
     std::string restof_firestring = fireset_str;
+    
+    if(fireset_str.compare("all") == 0){
+        for(int i = 0; i < numberof_t; i++){
+            _fireset.push_back(i);
+        }
+        return;
+    }
+    
     while(restof_firestring.length() > 0){
         size_t position = restof_firestring.find(',');
         std::string current_t = restof_firestring.substr(0, position);

=== modified file 'CTLParser/EvaluateableProposition.h'
--- CTLParser/EvaluateableProposition.h	2016-05-16 12:24:30 +0000
+++ CTLParser/EvaluateableProposition.h	2016-08-29 09:42:25 +0000
@@ -17,7 +17,7 @@
 #include "PetriEngine/PetriNet.h"
 
 
-enum PropositionType {CARDINALITY = 0, FIREABILITY = 1};
+enum PropositionType {CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2};
 enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4};
 
 struct CardinalityParameter{