VerifyDTAPN

Merge lp:~verifydtapn-contributers/verifydtapn/DeadlockInvariantPropagation into lp:verifydtapn

  1. DeadlockInvariantPropagation
  2. Merge into trunk
Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 311
Merged at revision: 311
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/DeadlockInvariantPropagation
Merge into: lp:verifydtapn
Diff against target: 13 lines (+2/-1)
1 file modified
src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp (+2/-1)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/DeadlockInvariantPropagation
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+226022@code.launchpad.net

Description of the change

Fixed missing destination place invariant check in the deadlock-checker.

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

Tested and works.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
2--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp 2014-06-19 09:38:50 +0000
3+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp 2014-07-08 19:03:22 +0000
4@@ -293,7 +293,8 @@
5 status[id] = -1; // impossible to enable
6 else if(status[id] != -1) { // if enable able so far
7 int lb = (*arc_iter)->getInterval().getLowerBound();
8- int ub = (*arc_iter)->getInterval().getUpperBound();
9+ int destination_invariant = (*arc_iter)->getDestination().getInvariant().getBound();
10+ int ub = min((*arc_iter)->getInterval().getUpperBound(), destination_invariant);
11 // decrement if token can satisfy the bounds
12 for (TokenList::const_iterator tokenit = place_iter->tokens.begin();
13 tokenit != place_iter->tokens.end(); ++tokenit){

Subscribers

People subscribed via source and target branches