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

Proposed by Søren Moss Nielsen on 2016-08-29
Status: Merged
Approved by: Jiri Srba on 2016-08-29
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 2016-08-29 Approve on 2016-08-29
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.
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'CTL/OnTheFlyDG.cpp'
2--- CTL/OnTheFlyDG.cpp 2016-08-04 10:59:43 +0000
3+++ CTL/OnTheFlyDG.cpp 2016-08-29 09:42:25 +0000
4@@ -360,6 +360,19 @@
5 int second_param = GetParamValue(proposition->GetSecondParameter(), marking);
6 return EvalCardianlity(first_param, proposition->GetLoperator(), second_param);
7 }
8+ else if (proposition->GetPropositionType() == DEADLOCK){
9+ std::list<int> transistions = calculateFireableTransistions(marking);
10+ std::list<int>::iterator it;
11+ transistions.sort();
12+
13+ for(const auto f : proposition->GetFireset()){
14+ it = std::find(transistions.begin(), transistions.end(), f);
15+ if(it != transistions.end()){
16+ return false;
17+ }
18+ }
19+ return true;
20+ }
21 else
22 assert(false && "Incorrect query proposition type was attempted evaluated");
23
24
25=== modified file 'CTLParser/CTLParser_v2.cpp'
26--- CTLParser/CTLParser_v2.cpp 2016-08-07 12:46:34 +0000
27+++ CTLParser/CTLParser_v2.cpp 2016-08-29 09:42:25 +0000
28@@ -337,9 +337,19 @@
29 assert(query->GetQuantifier() == AND && "Failed setting and operator");
30 }
31 else if (firstLetter == 'd' ) {
32- //Construct disjunction
33- query = new CTLQuery(OR, pError, false, "");
34- assert(query->GetQuantifier() == OR && "Failed setting or operator");
35+ if( root_name[1] == 'i' ){
36+ //Construct disjunction
37+ query = new CTLQuery(OR, pError, false, "");
38+ assert(query->GetQuantifier() == OR && "Failed setting or operator");
39+ }
40+ else if (root_name[1] == 'e'){
41+ //Deadlock query
42+ std::string atom_str = root->name();
43+ query = new CTLQuery(EMPTY, pError, true, atom_str);
44+ query->Depth = 0;
45+ return query;
46+ }
47+ else assert(false && "Failed parsing .xml file provided. Incorrect format.");
48 }
49 else if (firstLetter == 'i' ) {
50 //Construct Atom
51
52=== modified file 'CTLParser/EvaluateableProposition.cpp'
53--- CTLParser/EvaluateableProposition.cpp 2016-08-04 10:59:43 +0000
54+++ CTLParser/EvaluateableProposition.cpp 2016-08-29 09:42:25 +0000
55@@ -83,6 +83,11 @@
56 _secondParameter->isPlace = false;
57 _secondParameter->value = 1;
58 }
59+ else if(a.substr(0,2).compare("de") == 0){
60+ _type = DEADLOCK;
61+ _loperator = NOT_CARDINALITY;
62+ SetFireset("all", net->transitionNames(), net->numberOfTransitions());
63+ }
64 else{
65 assert(false && "Atomic string proposed for proposition could not be parsed");
66 }
67@@ -101,12 +106,20 @@
68 }
69
70 std::vector<int> EvaluateableProposition::GetFireset() {
71- assert(_type == FIREABILITY && "Proposition is not a fireability proposition");
72+ assert((_type == FIREABILITY || _type == DEADLOCK) && "Proposition is not a fireability proposition");
73 return _fireset;
74 }
75
76 void EvaluateableProposition::SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t){
77 std::string restof_firestring = fireset_str;
78+
79+ if(fireset_str.compare("all") == 0){
80+ for(int i = 0; i < numberof_t; i++){
81+ _fireset.push_back(i);
82+ }
83+ return;
84+ }
85+
86 while(restof_firestring.length() > 0){
87 size_t position = restof_firestring.find(',');
88 std::string current_t = restof_firestring.substr(0, position);
89
90=== modified file 'CTLParser/EvaluateableProposition.h'
91--- CTLParser/EvaluateableProposition.h 2016-05-16 12:24:30 +0000
92+++ CTLParser/EvaluateableProposition.h 2016-08-29 09:42:25 +0000
93@@ -17,7 +17,7 @@
94 #include "PetriEngine/PetriNet.h"
95
96
97-enum PropositionType {CARDINALITY = 0, FIREABILITY = 1};
98+enum PropositionType {CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2};
99 enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4};
100
101 struct CardinalityParameter{

Subscribers

People subscribed via source and target branches