Merge lp:~peter-gjoel/verifydtapn/ABPTraceFix into lp:verifydtapn

Proposed by Peter Gjøl Jensen
Status: Merged
Merged at revision: 332
Proposed branch: lp:~peter-gjoel/verifydtapn/ABPTraceFix
Merge into: lp:verifydtapn
Diff against target: 19 lines (+4/-3)
1 file modified
src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp (+4/-3)
To merge this branch: bzr merge lp:~peter-gjoel/verifydtapn/ABPTraceFix
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+268300@code.launchpad.net

Commit message

Fixed an issue for time-dart trace generation (replacing goto * for an infinite delay with "delay forever".

Description of the change

Fixes minor issue in trace-generation for time-darts.

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

Manually tested on some examples and it seems to work fine. Can I merge it to trunk?

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

> Manually tested on some examples and it seems to work fine. Can I merge it to
> trunk?

Yes please.

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp'
2--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2014-08-08 07:57:49 +0000
3+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp 2015-08-18 08:12:13 +0000
4@@ -217,11 +217,12 @@
5 }
6
7 last = mc;
8- mc->cut(placeStats);
9+
10 if(l == NULL) { // set specific last marking to last marking in delay if deadlock
11- l = mc;
12+ l = new NonStrictMarkingBase(*mc);
13 }
14-
15+ mc->cut(placeStats);
16+
17 traceStack.push(mc); // add delay marking to the trace
18 mc->setParent(NULL); // set parrent
19 diff--;

Subscribers

People subscribed via source and target branches

to all changes: