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

Proposed by Søren Moss Nielsen on 2016-09-06
Status: Merged
Approved by: Jiri Srba on 2016-09-08
Approved revision: 98
Merged at revision: 97
Proposed branch: lp:~tapaal-dist-ctl/verifypn/logicaloperator_change
Merge into: lp:~verifypn-maintainers/verifypn/trunk
Diff against target: 61 lines (+11/-3)
4 files modified
CTL/OnTheFlyDG.cpp (+3/-0)
CTLParser/CTLParser_v2.cpp (+5/-2)
CTLParser/EvaluateableProposition.cpp (+2/-0)
CTLParser/EvaluateableProposition.h (+1/-1)
To merge this branch: bzr merge lp:~tapaal-dist-ctl/verifypn/logicaloperator_change
Reviewer Review Type Date Requested Status
Jiri Srba 2016-09-06 Approve on 2016-09-08
Review via email: mp+304999@code.launchpad.net

Description of the change

Tested the queries
        <property>
  <id>DifferentTests</id>
  <description>TAPAAL generated query</description>
  <formula>
   <exists-path>
    <next>
     <integer-ne>
      <integer-constant>1</integer-constant>
      <integer-constant>2</integer-constant>
     </integer-ne>
    </next>
   </exists-path>
  </formula>
 </property>
and
        <property>
  <id>DifferentTests</id>
  <description>TAPAAL generated query</description>
  <formula>
   <exists-path>
    <next>
     <integer-ne>
      <integer-constant>2</integer-constant>
      <integer-constant>2</integer-constant>
     </integer-ne>
    </next>
   </exists-path>
  </formula>
 </property>

It works.

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-29 09:38:49 +0000
3+++ CTL/OnTheFlyDG.cpp 2016-09-06 12:48:46 +0000
4@@ -410,6 +410,9 @@
5 else if (lop == GRQ){
6 return a >= b;
7 }
8+ else if (lop == NE){
9+ return a != b;
10+ }
11 assert(false && "Unsupported LOperator attemped evaluated");
12 }
13
14
15=== modified file 'CTLParser/CTLParser_v2.cpp'
16--- CTLParser/CTLParser_v2.cpp 2016-08-30 08:24:00 +0000
17+++ CTLParser/CTLParser_v2.cpp 2016-09-06 12:48:46 +0000
18@@ -486,12 +486,15 @@
19 else if(loperator.compare("integer-eq")== 0){
20 return " eq ";
21 }
22- else if(loperator.compare("integer-gr")== 0){
23+ else if(loperator.compare("integer-gt")== 0){
24 return " gr ";
25 }
26- else if(loperator.compare("integer-ls")== 0){
27+ else if(loperator.compare("integer-lt")== 0){
28 return " ls ";
29 }
30+ else if(loperator.compare("integer-ne")== 0){
31+ return " ne ";
32+ }
33 else assert(true && "Could not parse unsupported logical operator");
34 return "";
35 }
36
37=== modified file 'CTLParser/EvaluateableProposition.cpp'
38--- CTLParser/EvaluateableProposition.cpp 2016-08-29 09:38:49 +0000
39+++ CTLParser/EvaluateableProposition.cpp 2016-09-06 12:48:46 +0000
40@@ -186,6 +186,8 @@
41 return GR;
42 else if (loperator_str.compare(" ls ")== 0)
43 return LE;
44+ else if (loperator_str.compare(" ne ")== 0)
45+ return NE;
46 else assert(false && "Could not parse the given logical operator");
47 }
48
49
50=== modified file 'CTLParser/EvaluateableProposition.h'
51--- CTLParser/EvaluateableProposition.h 2016-08-29 09:38:49 +0000
52+++ CTLParser/EvaluateableProposition.h 2016-09-06 12:48:46 +0000
53@@ -18,7 +18,7 @@
54
55
56 enum PropositionType {CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2};
57-enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4};
58+enum LoperatorType {NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4, NE = 5};
59
60 struct CardinalityParameter{
61 bool isPlace;

Subscribers

People subscribed via source and target branches