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

[Søren Moss Nielsen]

add all binary comparison operators for the CTL query predicates

All operators should be supported now.
== : <integer-eq>
>= : <integer-ge>
<= : <integer-le>
<= : <integer-le>
 < : <integer-ls>
 > : <integer-gr>

[Jiri Srba (srba)]

Looks fine, there is one warning:

CTLParser/CTLParser_v2.cpp:485:1: warning: control may reach end of non-void
      function [-Wreturn-type]
}

I will merge it anyway now, but please fix the warning is a new branch.

review: Approve

=== modified file 'CTL/OnTheFlyDG.cpp'
--- CTL/OnTheFlyDG.cpp	2016-05-16 12:24:30 +0000
+++ CTL/OnTheFlyDG.cpp	2016-08-04 11:04:35 +0000
@@ -367,10 +367,13 @@
 
 int OnTheFlyDG::GetParamValue(CardinalityParameter *param, Marking& marking) {
     if(param->isPlace){
+        bool foundplace = false;
         int res = 0;
         for(int place : param->places_i){
             res = res + marking.Value()[place];
+            foundplace = true;
         }
+        assert(foundplace && "Place parameter does not contain places. Please provide valid place names in the query.");
         return res;
     }
     else{
@@ -379,16 +382,21 @@
 }
 
 bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) {
-    if(lop == EQ)
+    if(lop == EQ){
         return a == b;
-    else if (lop == LE)
+    }
+    else if (lop == LE){
         return a < b;
-    else if (lop == LEQ)
+    }
+    else if (lop == LEQ){
         return a <= b;
-    else if (lop == GR)
+    }
+    else if (lop == GR){
         return a > b;
-    else if (lop == GRQ)
+    }
+    else if (lop == GRQ){
         return a >= b;
+    }
     assert(false && "Unsupported LOperator attemped evaluated");
 }
 

=== modified file 'CTLParser/CTLParser_v2.cpp'
--- CTLParser/CTLParser_v2.cpp	2016-05-16 12:24:30 +0000
+++ CTLParser/CTLParser_v2.cpp	2016-08-04 11:04:35 +0000
@@ -374,13 +374,13 @@
         return query;
     }
     else if (firstLetter == 't' ){
-        std::string atom_str = "integer-constant(0) le integer-constant(0)";
+        std::string atom_str = "true";
         query = new CTLQuery(EMPTY, pError, true, atom_str);
         query->Depth = 0;
         return query;
     }
     else if (firstLetter == 'f' ){
-        std::string atom_str = "integer-constant(2) le integer-constant(0)";
+        std::string atom_str = "false";
         query = new CTLQuery(EMPTY, pError, true, atom_str);
         query->Depth = 0;
         return query;
@@ -466,16 +466,22 @@
 }
 
 std::string CTLParser_v2::loperator_sym(std::string loperator){
-    if(loperator.compare("integer-le") == 0){
+    if(loperator.compare("integer-le")== 0){
         return " le ";
     }
-    else if(loperator.compare("integer-ge")){
+    else if(loperator.compare("integer-ge")== 0){
         return " ge ";
     }
-    else if(loperator.compare("integer-eq")){
+    else if(loperator.compare("integer-eq")== 0){
         return " eq ";
     }
-    else return " " + loperator + " ";
+    else if(loperator.compare("integer-gr")== 0){
+        return " gr ";
+    }
+    else if(loperator.compare("integer-ls")== 0){
+        return " ls ";
+    }
+    else assert(true && "Could not parse unsupported logical operator");
 }
 
 CTLQuery * CTLParser_v2::CopyQuery(CTLQuery *source){

=== modified file 'CTLParser/EvaluateableProposition.cpp'
--- CTLParser/EvaluateableProposition.cpp	2016-05-16 12:24:30 +0000
+++ CTLParser/EvaluateableProposition.cpp	2016-08-04 11:04:35 +0000
@@ -30,6 +30,7 @@
 }
 
 EvaluateableProposition::EvaluateableProposition(std::string a, PetriEngine::PetriNet *net) {
+    std::cout<<a<<std::endl;
     if(a.substr(0,2).compare("in") == 0 || a.substr(0,2).compare("to") == 0){
         _type = CARDINALITY;
         _loperator = SetLoperator(a);
@@ -57,10 +58,30 @@
         SetFireset(fireset_str, net->transitionNames(), net->numberOfTransitions());
     }
     else if(a.substr(0,2).compare("tr") == 0){
-        
+        _type = CARDINALITY;
+        _loperator = EQ;
+        
+        _firstParameter = new CardinalityParameter();
+        _secondParameter = new CardinalityParameter();
+        
+        _firstParameter->isPlace = false;
+        _firstParameter->value = 0;
+        
+        _secondParameter->isPlace = false;
+        _secondParameter->value = 0;
     }
     else if(a.substr(0,2).compare("fa") == 0){
-        
+        _type = CARDINALITY;
+        _loperator = EQ;
+        
+        _firstParameter = new CardinalityParameter();
+        _secondParameter = new CardinalityParameter();
+        
+        _firstParameter->isPlace = false;
+        _firstParameter->value = 0;
+        
+        _secondParameter->isPlace = false;
+        _secondParameter->value = 1;
     }
     else{
         assert(false && "Atomic string proposed for proposition could not be parsed");
@@ -140,14 +161,18 @@
 }
 
 LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){
-    std::string loperator_str = atom_str.substr(atom_str.find(')'));
-    loperator_str = loperator_str.substr(0, loperator_str.find('('));
-    if(loperator_str.compare(" le "))
+    std::string loperator_str = atom_str.substr(atom_str.find(')') + 1);
+    loperator_str = loperator_str.substr(0, 4);
+    if(loperator_str.compare(" le ")== 0)
             return LEQ;
-    else if (loperator_str.compare(" ge "))
+    else if (loperator_str.compare(" ge ")== 0)
         return GRQ;
-    else if (loperator_str.compare(" eq "))
+    else if (loperator_str.compare(" eq ")== 0)
         return EQ;
+    else if (loperator_str.compare(" gr ")== 0)
+        return GR;
+    else if (loperator_str.compare(" ls ")== 0)
+        return LE;
     else assert(false && "Could not parse the given logical operator");
 }
 
@@ -166,7 +191,7 @@
         else
             cardi_str = cardi_str = patch::to_string(_firstParameter->value);
         
-        cardi_str = cardi_str + " le ";
+        cardi_str = cardi_str + " loperator ";
         
         if(_secondParameter->isPlace)
             cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")";