Merge lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions into lp:verifypn

[Søren Moss Nielsen]

Added the requested syntax for arithmetic expressions:
 integer-sum
 integer-product
 integer-difference

[Jiri Srba (srba)]

I can see some problems when parsing the expressions.

A query in the GUI is:

EF N.P0 * N.P1 + N.P2 * N.P2 - N.P4 = 0

and your engine prints it as:

Query before reduction: AG (((P0 + P1) * ((P2 + P2) - P4)) == 0)

but the XML query output seems correct:

 <exists-path>
        <finally>
          <integer-eq>
            <integer-sum>
              <integer-product>
                <tokens-count>
                  <place>P0</place>
                </tokens-count>
                <tokens-count>
                  <place>P1</place>
                </tokens-count>
              </integer-product>
              <integer-difference>
                <integer-product>
                  <tokens-count>
                    <place>P2</place>
                  </tokens-count>
                  <tokens-count>
                    <place>P2</place>
                  </tokens-count>
                </integer-product>
                <tokens-count>
                  <place>P4</place>
                </tokens-count>
              </integer-difference>
            </integer-sum>
            <integer-constant>0</integer-constant>
          </integer-eq>
        </finally>
      </exists-path>

review: Needs Fixing

[lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions]

187. By Jiri Srba on 2017-06-19

fixed inhibitor arcs behaviour when removing preset in successor generator

188. By Lasse S. Jensen on 2017-06-22

integer-sum and integer-product are now correctly parsed in verifypn

[Lasse S. Jensen (lasjen12)]

> I can see some problems when parsing the expressions.
>
> A query in the GUI is:
>
> EF N.P0 * N.P1 + N.P2 * N.P2 - N.P4 = 0
>
> and your engine prints it as:
>
> Query before reduction: AG (((P0 + P1) * ((P2 + P2) - P4)) == 0)
>
> but the XML query output seems correct:
>
> <exists-path>
> <finally>
> <integer-eq>
> <integer-sum>
> <integer-product>
> <tokens-count>
> <place>P0</place>
> </tokens-count>
> <tokens-count>
> <place>P1</place>
> </tokens-count>
> </integer-product>
> <integer-difference>
> <integer-product>
> <tokens-count>
> <place>P2</place>
> </tokens-count>
> <tokens-count>
> <place>P2</place>
> </tokens-count>
> </integer-product>
> <tokens-count>
> <place>P4</place>
> </tokens-count>
> </integer-difference>
> </integer-sum>
> <integer-constant>0</integer-constant>
> </integer-eq>
> </finally>
> </exists-path>

The xml query is not correct. sum and product have been swapped with each other. This was an issue in the parser in verifypn.

Unmerged revisions

=== modified file 'CTL/CTLParser/CTLParser.cpp'
--- CTL/CTLParser/CTLParser.cpp	2017-03-15 20:19:30 +0000
+++ CTL/CTLParser/CTLParser.cpp	2017-06-22 19:09:16 +0000
@@ -344,28 +344,43 @@
     if (firstLetter == 'a') {
         //Construct all-paths
         query = new CTLQuery(A, getPathOperator(root), false, "");
-        assert(query->GetQuantifier() == A && "Failed setting quantifier");
+        if(query->GetQuantifier() != A){
+            std::cerr << "Error: Failed setting all operator." << std::endl;
+            exit(EXIT_FAILURE);
+        }
     }
     else if (firstLetter == 'e' ) {
         //Construct exists-path
         query = new CTLQuery(E, getPathOperator(root), false, "");
-        assert(query->GetQuantifier() == E && "Failed setting path operator");
+        if(query->GetQuantifier() != E){
+            std::cerr << "Error: Failed setting exists operator." << std::endl;
+            exit(EXIT_FAILURE);
+        }
     }
     else if (firstLetter == 'n' ) {
         //Construct negation
         query = new CTLQuery(NEG, pError, false, "");
-        assert(query->GetQuantifier() == NEG && "Failed setting negation operator");
+        if(query->GetQuantifier() != NEG){
+            std::cerr << "Error: Failed setting negation operator." << std::endl;
+            exit(EXIT_FAILURE);
+        }
     }
     else if (firstLetter == 'c' ) {
         //Construct conjunction
         query = new CTLQuery(AND, pError, false, "");
-        assert(query->GetQuantifier() == AND && "Failed setting and operator");
+        if(query->GetQuantifier() != AND){
+            std::cerr << "Error: Failed setting and operator." << std::endl;
+            exit(EXIT_FAILURE);
+        }
     }
     else if (firstLetter == 'd' ) {
         if( root_name[1] == 'i' ){
             //Construct disjunction
             query = new CTLQuery(OR, pError, false, "");
-            assert(query->GetQuantifier() == OR && "Failed setting or operator");
+            if(query->GetQuantifier() != OR){
+                std::cerr << "Error: Failed setting or operator." << std::endl;
+                exit(EXIT_FAILURE);
+            }
         }
         else if (root_name[1] == 'e'){
             //Deadlock query
@@ -403,7 +418,7 @@
             
             loperator = loperator_sym(loperator);
             
-            atom_str = first + loperator + second;
+            atom_str = first + "}" + loperator + "{" + second;
             
         }
         else {
@@ -512,9 +527,18 @@
         parameter_str = parameter_str + ")";
     }
     
-    else if(parameter->name()[0] == 'i'){
+    else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'c'){
         parameter_str = parameter_str + choppy(parameter->value()) + ")";
     }
+    else if(parameter->name()[0] == 'i' && parameter->name()[8] == 's'){
+        parameter_str = parameter_str + parsePar(parameter->first_node()) + " + " + parsePar(parameter->first_node()->next_sibling()) + ")";
+    }
+    else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'p'){
+        parameter_str = parameter_str + parsePar(parameter->first_node()) + " * " + parsePar(parameter->first_node()->next_sibling()) + ")";
+    }
+    else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'd'){
+        parameter_str = parameter_str + parsePar(parameter->first_node()) + " - " + parsePar(parameter->first_node()->next_sibling()) + ")";
+    }
     else {
         std::cerr << "Error: Failed parsing query file provided. Incorrect format around the parameter: " << parameter->name() << ". Please check spelling." << std::endl;
         exit(EXIT_FAILURE);

=== modified file 'CTL/CTLParser/CTLQuery.cpp'
--- CTL/CTLParser/CTLQuery.cpp	2017-03-12 18:46:15 +0000
+++ CTL/CTLParser/CTLQuery.cpp	2017-06-22 19:09:16 +0000
@@ -134,7 +134,7 @@
 
 std::string CTLQuery::ToString(){
     if(_hasAtom){
-        return _a;
+        return _proposition->ToString();
     }
     else if(_q == AND){
         return "(" + _firstchild->ToString() + " & " +  _secondchild->ToString() + ")";
@@ -152,13 +152,13 @@
         }
         else quanti = "E";
         if(_path == F){
-            return quanti + "F" + _firstchild->ToString();
+            return quanti + "F " + _firstchild->ToString();
         }
         else if(_path == G){
-            return quanti + "G" + _firstchild->ToString();
+            return quanti + "G " + _firstchild->ToString();
         }
         else if(_path == X){
-            return quanti + "X" + _firstchild->ToString();
+            return quanti + "X " + _firstchild->ToString();
         }
         else if(_path == U){
             return quanti + "("  + _firstchild->ToString() + ") U (" + _secondchild->ToString() + ")";

=== modified file 'CTL/CTLParser/EvaluateableProposition.cpp'
--- CTL/CTLParser/EvaluateableProposition.cpp	2017-04-11 10:21:33 +0000
+++ CTL/CTLParser/EvaluateableProposition.cpp	2017-06-22 19:09:16 +0000
@@ -37,14 +37,14 @@
         _loperator = SetLoperator(a);
         assert(_loperator != NOT_CARDINALITY);
 
-        size_t begin = a.find('(') + 1;
-        size_t end = a.find(')') - begin;
-        std::string first_parameter_str = a.substr(begin, end);
-        a = a.substr(a.find(')') + 1);
+        //size_t begin = a.find('(') + 1;
+        size_t end = a.find('}');
+        std::string first_parameter_str = a.substr(0, end);
+        a = a.substr(a.find('}') + 1);
 
-        begin = a.find('(') + 1;
-        end = a.find(')') - begin;
-        std::string second_parameter_str = a.substr(begin, end);
+        size_t begin = a.find('{') + 1;
+        //end = a.find(')') - begin;
+        std::string second_parameter_str = a.substr(begin);
         _firstParameter = CreateParameter(first_parameter_str, net->placeNames(), net->numberOfPlaces());
         _secondParameter = CreateParameter(second_parameter_str, net->placeNames(), net->numberOfPlaces());
     }
@@ -90,7 +90,8 @@
         SetFireset("all", net->transitionNames(), net->numberOfTransitions());
     }
     else{
-        assert(false && "Atomic string proposed for proposition could not be parsed");
+        std::cerr << "Error: Could not identify Evaluateable Proposition type from atom string: "<<a<<"." << std::endl;
+        exit(EXIT_FAILURE);
     }
 }
 
@@ -139,7 +140,51 @@
 }
 
 CardinalityParameter* EvaluateableProposition::CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p){
-    CardinalityParameter *param = new CardinalityParameter();   
+    CardinalityParameter *param = new CardinalityParameter();
+    while(parameter_str.substr(0,1).compare(" ")==0){
+        parameter_str = parameter_str.substr(1);
+    }
+    //std::cout<<"ParamString: "<<parameter_str<<"\n"<<std::flush;
+
+    ParameterHolder* typeHolder = new ParameterHolder();
+    if(parameter_str.substr(0,11).compare("integer-sum")==0){
+        typeHolder->type = SUM;
+        typeHolder->body = parameter_str.substr(11);
+    }
+    else if(parameter_str.substr(0,15).compare("integer-product")==0){
+        typeHolder->type = PRODUCT;
+        typeHolder->body = parameter_str.substr(15);
+    }
+    else if(parameter_str.substr(0,18).compare("integer-difference")==0){
+        typeHolder->type = DIFF;
+        typeHolder->body = parameter_str.substr(18);
+    }
+    else if(parameter_str.substr(0,16).compare("integer-constant")==0){
+        typeHolder->type = CONST;
+        typeHolder->body = parameter_str.substr(16);
+    }
+    else if(parameter_str.substr(0,12).compare("tokens-count")==0){
+        typeHolder->type = PLACE;
+        typeHolder->body = parameter_str.substr(12);
+    }
+    else{
+        std::cerr << "Error: Internal parse error - \"" << parameter_str <<"\" has unrecognized beginning." << std::endl;
+        exit(EXIT_FAILURE);
+    }
+
+    std::size_t found = typeHolder->body.find_last_of(")");
+    parameter_str = typeHolder->body.substr(1,found-1);
+
+    if(typeHolder->type != CONST && typeHolder->type != PLACE){
+        std::size_t end_of_first = GetEndingParamIndex(parameter_str) + 1;
+        param->isArithmetic = true;
+        param->arithmetictype = typeHolder->type;
+        param->arithmA = CreateParameter(parameter_str.substr(0,end_of_first), p_names, numberof_p);
+        param->arithmB = CreateParameter(parameter_str.substr(end_of_first + 2), p_names, numberof_p);
+        return param;
+    }
+
+
     char c;
     if(sscanf(parameter_str.c_str(), "%d%c", &param->value, &c) == 1) {
         //If string is identifier starting with a number, you will read two items.
@@ -178,8 +223,30 @@
     return param;
 }
 
+std::size_t EvaluateableProposition::GetEndingParamIndex(std::string param_str){
+    size_t pos = param_str.find('(');
+    size_t start_count =1;
+    size_t end_count =0;
+    std::string temp = param_str.substr(pos+1);
+    while(start_count != end_count){
+        size_t new_pos = 0;
+        if(temp.find('(') < temp.find(')')){
+            start_count++;
+            new_pos = temp.find('(') + 1;
+        }
+        else{
+            end_count++;
+            new_pos = temp.find(')') + 1;
+        }
+        pos = pos + new_pos;
+        temp = temp.substr(new_pos);
+    }
+
+    return pos;
+}
+
 LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){
-    std::string loperator_str = atom_str.substr(atom_str.find(')') + 1);
+    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;
@@ -206,22 +273,60 @@
         return fire_str + ")";
     }
     else if (_type == CARDINALITY){
-        std::string cardi_str = "(";
-        if(_firstParameter->isPlace)
-            cardi_str = cardi_str + "place(" + patch::to_string(_firstParameter->value) + ")";
-        else
-            cardi_str = cardi_str = patch::to_string(_firstParameter->value);
-        
-        cardi_str = cardi_str + " loperator ";
-        
-        if(_secondParameter->isPlace)
-            cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")";
-        else
-            cardi_str = cardi_str = patch::to_string(_secondParameter->value);
-        return cardi_str + ")";
+        return Parameter_tostring(_firstParameter) + Loperator_tostring() + Parameter_tostring(_secondParameter);
+    }
+    std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl;
+    exit(EXIT_FAILURE);
+}
+
+
+std::string EvaluateableProposition::Parameter_tostring(CardinalityParameter* param){
+    std::string cardi_str = "";
+    if(param->isPlace){
+        cardi_str = cardi_str + "place(";
+        int i = 0;
+        while(i != param->places_i.size()){
+            cardi_str = cardi_str + patch::to_string(param->places_i[i]);
+
+            if(++i < param->places_i.size()){
+                cardi_str = cardi_str + ", ";
+            }
+        }
+        cardi_str = cardi_str + ")";
+    }
+    else if(param->isArithmetic){
+        std::string arthm_ope = "";
+        if(param->arithmetictype == SUM)
+            arthm_ope = " + ";
+        else if (param->arithmetictype == PRODUCT)
+            arthm_ope = " * ";
+        else if (param->arithmetictype == DIFF)
+            arthm_ope = " - ";
+        else {
+            std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl;
+            exit(EXIT_FAILURE);
+        }
+        cardi_str = cardi_str + Parameter_tostring(param->arithmA) + arthm_ope + Parameter_tostring(param->arithmB);
     }
     else
-        std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl;
+        cardi_str = cardi_str = patch::to_string(param->value);
+    return cardi_str;
+}
+
+std::string EvaluateableProposition::Loperator_tostring(){
+    if(_loperator == LEQ)
+            return " <= ";
+    else if (_loperator == GRQ)
+        return " >= ";
+    else if (_loperator == EQ)
+        return " == ";
+    else if (_loperator == GR)
+        return " > ";
+    else if (_loperator == LE)
+        return " < ";
+    else if (_loperator == NE)
+        return " != ";
+    else std::cerr << "Error: Could not convert loperator to string" << std::endl;
     exit(EXIT_FAILURE);
 }
 

=== modified file 'CTL/CTLParser/EvaluateableProposition.h'
--- CTL/CTLParser/EvaluateableProposition.h	2017-02-08 19:14:47 +0000
+++ CTL/CTLParser/EvaluateableProposition.h	2017-06-22 19:09:16 +0000
@@ -18,12 +18,22 @@
 
 
 enum PropositionType {PropError = -1, CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2};
+enum ArithmeticType {NON = -1, SUM = 0, PRODUCT = 1, DIFF = 2, CONST = 3, PLACE = 4};
 enum LoperatorType {LopError = -1, NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4, NE = 5};
 
+struct ParameterHolder{
+    ArithmeticType type = NON;
+    std::string body = "";
+};
+
 struct CardinalityParameter{
     bool isPlace = false;
+    bool isArithmetic = false;
     int value = -1;
     std::vector<int> places_i;
+    ArithmeticType arithmetictype = NON;
+    CardinalityParameter* arithmA;
+    CardinalityParameter* arithmB;
 };
 
 class EvaluateableProposition {
@@ -39,6 +49,7 @@
 private:
     void SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t);
     CardinalityParameter* CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p);
+    std::size_t GetEndingParamIndex(std::string parameter_str);
     LoperatorType SetLoperator(std::string atom_str);
     
     PropositionType _type = PropError;
@@ -46,6 +57,8 @@
     std::vector<int> _fireset;
     CardinalityParameter* _firstParameter = nullptr;
     CardinalityParameter* _secondParameter = nullptr;
+    std::string Parameter_tostring(CardinalityParameter *param);
+    std::string Loperator_tostring();
     
 };
 

=== modified file 'CTL/PetriNets/OnTheFlyDG.cpp'
--- CTL/PetriNets/OnTheFlyDG.cpp	2017-04-11 19:03:34 +0000
+++ CTL/PetriNets/OnTheFlyDG.cpp	2017-06-22 19:09:16 +0000
@@ -395,9 +395,22 @@
         }
         return res;
     }
-    else{
-        return param->value;
+    else if(param->isArithmetic){
+        if(param->arithmetictype == NON){
+            std::cerr << "Error: Arithmetic param is not assigned a type"<< std::endl;
+            exit(EXIT_FAILURE);
+        }
+        else if(param->arithmetictype == SUM){
+            return GetParamValue(param->arithmA, marking) + GetParamValue(param->arithmB, marking);
+        }
+        else if(param->arithmetictype == PRODUCT){
+            return GetParamValue(param->arithmA, marking) * GetParamValue(param->arithmB, marking);
+        }
+        else if(param->arithmetictype == DIFF){
+            return GetParamValue(param->arithmA, marking) - GetParamValue(param->arithmB, marking);
+        }
     }
+    return param->value;
 }
 
 bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) {

=== modified file 'PetriEngine/SuccessorGenerator.cpp'
--- PetriEngine/SuccessorGenerator.cpp	2017-03-05 16:08:26 +0000
+++ PetriEngine/SuccessorGenerator.cpp	2017-06-22 19:09:16 +0000
@@ -39,7 +39,9 @@
         uint32_t finv = ptr.inputs;
         uint32_t linv = ptr.outputs;
         for (; finv < linv; ++finv) {
-            write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens;
+            if(!_net._invariants[finv].inhibitor) {
+                write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens;
+            }
         }
     }
 

=== modified file 'PetriParse/QueryXMLParser.cpp'
--- PetriParse/QueryXMLParser.cpp	2017-04-09 15:12:50 +0000
+++ PetriParse/QueryXMLParser.cpp	2017-06-22 19:09:16 +0000
@@ -386,8 +386,8 @@
             Expr_ptr child = parseIntegerExpression(it);
             if(child == NULL)  return NULL;
             expr = isMult ? 
-                (Expr_ptr)std::make_shared<PlusExpr>(expr, child) :
-                (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child);
+                (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child):
+                (Expr_ptr)std::make_shared<PlusExpr>(expr, child);
         }
         return expr;
     } else if (elementName == "integer-difference") {