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

Proposed by Søren Moss Nielsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 95
Merged at revision: 95
Proposed branch: lp:~tapaal-dist-ctl/verifypn/new_deadlocksupport
Merge into: lp:~verifypn-maintainers/verifypn/trunk
Diff against target: 101 lines (+41/-5)
4 files modified
CTL/OnTheFlyDG.cpp (+13/-0)
CTLParser/CTLParser_v2.cpp (+13/-3)
CTLParser/EvaluateableProposition.cpp (+14/-1)
CTLParser/EvaluateableProposition.h (+1/-1)
To merge this branch: bzr merge lp:~tapaal-dist-ctl/verifypn/new_deadlocksupport
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+304237@code.launchpad.net

Commit message

Merged in branch verifypn/new_deadlocksupport adding deadlock support.

Description of the change

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

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== 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 @@
360 int second_param = GetParamValue(proposition->GetSecondParameter(), marking);360 int second_param = GetParamValue(proposition->GetSecondParameter(), marking);
361 return EvalCardianlity(first_param, proposition->GetLoperator(), second_param);361 return EvalCardianlity(first_param, proposition->GetLoperator(), second_param);
362 }362 }
363 else if (proposition->GetPropositionType() == DEADLOCK){
364 std::list<int> transistions = calculateFireableTransistions(marking);
365 std::list<int>::iterator it;
366 transistions.sort();
367
368 for(const auto f : proposition->GetFireset()){
369 it = std::find(transistions.begin(), transistions.end(), f);
370 if(it != transistions.end()){
371 return false;
372 }
373 }
374 return true;
375 }
363 else376 else
364 assert(false && "Incorrect query proposition type was attempted evaluated");377 assert(false && "Incorrect query proposition type was attempted evaluated");
365378
366379
=== 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 @@
337 assert(query->GetQuantifier() == AND && "Failed setting and operator");337 assert(query->GetQuantifier() == AND && "Failed setting and operator");
338 }338 }
339 else if (firstLetter == 'd' ) {339 else if (firstLetter == 'd' ) {
340 //Construct disjunction340 if( root_name[1] == 'i' ){
341 query = new CTLQuery(OR, pError, false, "");341 //Construct disjunction
342 assert(query->GetQuantifier() == OR && "Failed setting or operator");342 query = new CTLQuery(OR, pError, false, "");
343 assert(query->GetQuantifier() == OR && "Failed setting or operator");
344 }
345 else if (root_name[1] == 'e'){
346 //Deadlock query
347 std::string atom_str = root->name();
348 query = new CTLQuery(EMPTY, pError, true, atom_str);
349 query->Depth = 0;
350 return query;
351 }
352 else assert(false && "Failed parsing .xml file provided. Incorrect format.");
343 }353 }
344 else if (firstLetter == 'i' ) {354 else if (firstLetter == 'i' ) {
345 //Construct Atom355 //Construct Atom
346356
=== 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 @@
83 _secondParameter->isPlace = false;83 _secondParameter->isPlace = false;
84 _secondParameter->value = 1;84 _secondParameter->value = 1;
85 }85 }
86 else if(a.substr(0,2).compare("de") == 0){
87 _type = DEADLOCK;
88 _loperator = NOT_CARDINALITY;
89 SetFireset("all", net->transitionNames(), net->numberOfTransitions());
90 }
86 else{91 else{
87 assert(false && "Atomic string proposed for proposition could not be parsed");92 assert(false && "Atomic string proposed for proposition could not be parsed");
88 }93 }
@@ -101,12 +106,20 @@
101}106}
102107
103std::vector<int> EvaluateableProposition::GetFireset() {108std::vector<int> EvaluateableProposition::GetFireset() {
104 assert(_type == FIREABILITY && "Proposition is not a fireability proposition");109 assert((_type == FIREABILITY || _type == DEADLOCK) && "Proposition is not a fireability proposition");
105 return _fireset;110 return _fireset;
106}111}
107112
108void EvaluateableProposition::SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t){113void EvaluateableProposition::SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t){
109 std::string restof_firestring = fireset_str;114 std::string restof_firestring = fireset_str;
115
116 if(fireset_str.compare("all") == 0){
117 for(int i = 0; i < numberof_t; i++){
118 _fireset.push_back(i);
119 }
120 return;
121 }
122
110 while(restof_firestring.length() > 0){123 while(restof_firestring.length() > 0){
111 size_t position = restof_firestring.find(',');124 size_t position = restof_firestring.find(',');
112 std::string current_t = restof_firestring.substr(0, position);125 std::string current_t = restof_firestring.substr(0, position);
113126
=== 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 @@
17#include "PetriEngine/PetriNet.h"17#include "PetriEngine/PetriNet.h"
1818
1919
20enum PropositionType {CARDINALITY = 0, FIREABILITY = 1};20enum PropositionType {CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2};
21enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4};21enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4};
2222
23struct CardinalityParameter{23struct CardinalityParameter{

Subscribers

People subscribed via source and target branches