VerifyDTAPN

Merge lp:~cmoesgaard/verifydtapn/verifydtapn-workflowbound into lp:verifydtapn

  1. verifydtapn-workflowbound
  2. Merge into trunk
Proposed by Jiri Srba
Status: Merged
Merged at revision: 325
Proposed branch: lp:~cmoesgaard/verifydtapn/verifydtapn-workflowbound
Merge into: lp:verifydtapn
Diff against target: 74 lines (+17/-4)
3 files modified
src/Core/ArgsParser.cpp (+13/-1)
src/Core/ArgsParser.hpp (+1/-0)
src/Core/VerificationOptions.hpp (+3/-3)
To merge this branch: bzr merge lp:~cmoesgaard/verifydtapn/verifydtapn-workflowbound
Reviewer Review Type Date Requested Status
Peter Gjøl Jensen Approve
Jiri Srba Approve
Mathias Grund Sørensen Pending
Review via email: mp+261724@code.launchpad.net

Commit message

The bound for strong soundness checking has now type "long long".

Description of the change

The bound for strong soundness checking is now using "long long".
Needs to be used together with the updated TAPAAL GUI in this branch:
https://code.launchpad.net/~cmoesgaard/tapaal/tapaal-workflowbound

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

Tested with the UPDATE GUI and it seems the bug

https://bugs.launchpad.net/tapaal/+bug/1462468

has been fixed.

review: Approve
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/Core/ArgsParser.cpp'
2--- src/Core/ArgsParser.cpp 2014-06-16 10:49:17 +0000
3+++ src/Core/ArgsParser.cpp 2015-06-11 13:19:48 +0000
4@@ -390,6 +390,18 @@
5 return result;
6 }
7
8+unsigned long long ArgsParser::tryParseLongLong(const option& option) const {
9+ unsigned long long result = 0;
10+ try {
11+ result = boost::lexical_cast<unsigned long long>(option.second);
12+ } catch (boost::bad_lexical_cast & e) {
13+ std::cout << "Invalid value '" << option.second << "' for option '--"
14+ << option.first << "'" << std::endl;
15+ exit(1);
16+ }
17+ return result;
18+}
19+
20 std::vector<std::string> ArgsParser::parseIncPlaces(
21 const std::string& string) const {
22 std::vector<std::string> vec;
23@@ -432,7 +444,7 @@
24 tryParseInt(*map.find(WORKFLOW)));
25
26 assert(map.find(STRONG_WORKFLOW_BOUND) != map.end());
27- unsigned int workflowBound = tryParseInt(*map.find(STRONG_WORKFLOW_BOUND));
28+ unsigned long long workflowBound = tryParseLongLong(*map.find(STRONG_WORKFLOW_BOUND));
29
30
31 assert(map.find(GCD) != map.end());
32
33=== modified file 'src/Core/ArgsParser.hpp'
34--- src/Core/ArgsParser.hpp 2014-08-14 07:33:43 +0000
35+++ src/Core/ArgsParser.hpp 2015-06-11 13:19:48 +0000
36@@ -88,6 +88,7 @@
37 VerificationOptions createVerificationOptions(const option_map& map) const;
38 VerificationOptions verifyInputFiles(VerificationOptions, std::string model_file, std::string query_file) const;
39 unsigned int tryParseInt(const option& option) const;
40+ unsigned long long tryParseLongLong(const option& option) const;
41 std::vector<std::string> parseIncPlaces(const std::string& string) const;
42 void initialize();
43 void printHelp() const;
44
45=== modified file 'src/Core/VerificationOptions.hpp'
46--- src/Core/VerificationOptions.hpp 2014-06-15 19:20:11 +0000
47+++ src/Core/VerificationOptions.hpp 2015-06-11 13:19:48 +0000
48@@ -44,7 +44,7 @@
49 bool keepDeadTokens,
50 bool enableGCDLowerGuards,
51 WorkflowMode workflow,
52- int workflowBound
53+ long long workflowBound
54 ) : inputFile(""),
55 queryFile(""),
56 searchType(searchType),
57@@ -122,7 +122,7 @@
58 return workflow;
59 };
60
61- inline const int getWorkflowBound() const {
62+ inline const long long getWorkflowBound() const {
63 return workflowBound;
64 };
65
66@@ -143,7 +143,7 @@
67 bool keepDeadTokens;
68 bool enableGCDLowerGuards;
69 WorkflowMode workflow;
70- int workflowBound;
71+ long long workflowBound;
72 };
73
74 std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);

Subscribers

People subscribed via source and target branches