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

Proposed by Søren Moss Nielsen on 2016-08-04
Status: Merged
Approved by: Jiri Srba on 2016-08-07
Approved revision: 95
Merged at revision: 93
Proposed branch: lp:~tapaal-dist-ctl/verifypn/true_false_and_equal_support
Merge into: lp:~verifypn-maintainers/verifypn/trunk
Diff against target: 169 lines (+58/-19)
3 files modified
CTL/OnTheFlyDG.cpp (+13/-5)
CTLParser/CTLParser_v2.cpp (+12/-6)
CTLParser/EvaluateableProposition.cpp (+33/-8)
To merge this branch: bzr merge lp:~tapaal-dist-ctl/verifypn/true_false_and_equal_support
Reviewer Review Type Date Requested Status
Jiri Srba 2016-08-04 Approve on 2016-08-07
Review via email: mp+302011@code.launchpad.net

Commit message

add all binary comparison operators for the CTL query predicates

Description of the change

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

To post a comment you must log in.
Jiri Srba (srba) wrote :

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

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-05-16 12:24:30 +0000
3+++ CTL/OnTheFlyDG.cpp 2016-08-04 11:04:35 +0000
4@@ -367,10 +367,13 @@
5
6 int OnTheFlyDG::GetParamValue(CardinalityParameter *param, Marking& marking) {
7 if(param->isPlace){
8+ bool foundplace = false;
9 int res = 0;
10 for(int place : param->places_i){
11 res = res + marking.Value()[place];
12+ foundplace = true;
13 }
14+ assert(foundplace && "Place parameter does not contain places. Please provide valid place names in the query.");
15 return res;
16 }
17 else{
18@@ -379,16 +382,21 @@
19 }
20
21 bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) {
22- if(lop == EQ)
23+ if(lop == EQ){
24 return a == b;
25- else if (lop == LE)
26+ }
27+ else if (lop == LE){
28 return a < b;
29- else if (lop == LEQ)
30+ }
31+ else if (lop == LEQ){
32 return a <= b;
33- else if (lop == GR)
34+ }
35+ else if (lop == GR){
36 return a > b;
37- else if (lop == GRQ)
38+ }
39+ else if (lop == GRQ){
40 return a >= b;
41+ }
42 assert(false && "Unsupported LOperator attemped evaluated");
43 }
44
45
46=== modified file 'CTLParser/CTLParser_v2.cpp'
47--- CTLParser/CTLParser_v2.cpp 2016-05-16 12:24:30 +0000
48+++ CTLParser/CTLParser_v2.cpp 2016-08-04 11:04:35 +0000
49@@ -374,13 +374,13 @@
50 return query;
51 }
52 else if (firstLetter == 't' ){
53- std::string atom_str = "integer-constant(0) le integer-constant(0)";
54+ std::string atom_str = "true";
55 query = new CTLQuery(EMPTY, pError, true, atom_str);
56 query->Depth = 0;
57 return query;
58 }
59 else if (firstLetter == 'f' ){
60- std::string atom_str = "integer-constant(2) le integer-constant(0)";
61+ std::string atom_str = "false";
62 query = new CTLQuery(EMPTY, pError, true, atom_str);
63 query->Depth = 0;
64 return query;
65@@ -466,16 +466,22 @@
66 }
67
68 std::string CTLParser_v2::loperator_sym(std::string loperator){
69- if(loperator.compare("integer-le") == 0){
70+ if(loperator.compare("integer-le")== 0){
71 return " le ";
72 }
73- else if(loperator.compare("integer-ge")){
74+ else if(loperator.compare("integer-ge")== 0){
75 return " ge ";
76 }
77- else if(loperator.compare("integer-eq")){
78+ else if(loperator.compare("integer-eq")== 0){
79 return " eq ";
80 }
81- else return " " + loperator + " ";
82+ else if(loperator.compare("integer-gr")== 0){
83+ return " gr ";
84+ }
85+ else if(loperator.compare("integer-ls")== 0){
86+ return " ls ";
87+ }
88+ else assert(true && "Could not parse unsupported logical operator");
89 }
90
91 CTLQuery * CTLParser_v2::CopyQuery(CTLQuery *source){
92
93=== modified file 'CTLParser/EvaluateableProposition.cpp'
94--- CTLParser/EvaluateableProposition.cpp 2016-05-16 12:24:30 +0000
95+++ CTLParser/EvaluateableProposition.cpp 2016-08-04 11:04:35 +0000
96@@ -30,6 +30,7 @@
97 }
98
99 EvaluateableProposition::EvaluateableProposition(std::string a, PetriEngine::PetriNet *net) {
100+ std::cout<<a<<std::endl;
101 if(a.substr(0,2).compare("in") == 0 || a.substr(0,2).compare("to") == 0){
102 _type = CARDINALITY;
103 _loperator = SetLoperator(a);
104@@ -57,10 +58,30 @@
105 SetFireset(fireset_str, net->transitionNames(), net->numberOfTransitions());
106 }
107 else if(a.substr(0,2).compare("tr") == 0){
108-
109+ _type = CARDINALITY;
110+ _loperator = EQ;
111+
112+ _firstParameter = new CardinalityParameter();
113+ _secondParameter = new CardinalityParameter();
114+
115+ _firstParameter->isPlace = false;
116+ _firstParameter->value = 0;
117+
118+ _secondParameter->isPlace = false;
119+ _secondParameter->value = 0;
120 }
121 else if(a.substr(0,2).compare("fa") == 0){
122-
123+ _type = CARDINALITY;
124+ _loperator = EQ;
125+
126+ _firstParameter = new CardinalityParameter();
127+ _secondParameter = new CardinalityParameter();
128+
129+ _firstParameter->isPlace = false;
130+ _firstParameter->value = 0;
131+
132+ _secondParameter->isPlace = false;
133+ _secondParameter->value = 1;
134 }
135 else{
136 assert(false && "Atomic string proposed for proposition could not be parsed");
137@@ -140,14 +161,18 @@
138 }
139
140 LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){
141- std::string loperator_str = atom_str.substr(atom_str.find(')'));
142- loperator_str = loperator_str.substr(0, loperator_str.find('('));
143- if(loperator_str.compare(" le "))
144+ std::string loperator_str = atom_str.substr(atom_str.find(')') + 1);
145+ loperator_str = loperator_str.substr(0, 4);
146+ if(loperator_str.compare(" le ")== 0)
147 return LEQ;
148- else if (loperator_str.compare(" ge "))
149+ else if (loperator_str.compare(" ge ")== 0)
150 return GRQ;
151- else if (loperator_str.compare(" eq "))
152+ else if (loperator_str.compare(" eq ")== 0)
153 return EQ;
154+ else if (loperator_str.compare(" gr ")== 0)
155+ return GR;
156+ else if (loperator_str.compare(" ls ")== 0)
157+ return LE;
158 else assert(false && "Could not parse the given logical operator");
159 }
160
161@@ -166,7 +191,7 @@
162 else
163 cardi_str = cardi_str = patch::to_string(_firstParameter->value);
164
165- cardi_str = cardi_str + " le ";
166+ cardi_str = cardi_str + " loperator ";
167
168 if(_secondParameter->isPlace)
169 cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")";

Subscribers

People subscribed via source and target branches