Nonactive components can impose invariant restrictios in simulator
Bug #1003486 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Released
|
High
|
Jakob Taankvist | ||
Bug Description
Open the attached net. Verify the query. Once you get to simulator, the delay button says "cannot delay due to invariant
in the second net" but the second net is deactivated. Apparently the deactivated nets are not reflected in the simulator.
Related branches
lp:~tapaal-contributor/tapaal/deactivateInvariants
- Kenneth Yrke Jørgensen: Approve
- Jiri Srba: Approve
-
Diff: 136 lines (+43/-29)3 files modifiedsrc/dk/aau/cs/model/tapn/NetworkMarking.java (+32/-19)
src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java (+10/-0)
src/dk/aau/cs/verification/TAPNComposer.java (+1/-10)
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
| Changed in tapaal: | |
| status: | New → Fix Committed |
| Changed in tapaal: | |
| status: | Fix Committed → Fix Released |
To post a comment you must log in.
