UPPAAL translations fail generating trace

Bug #1219511 reported by Jiri Srba
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
New
Low
Unassigned

Bug Description

Open the attached net and verify. The initial fragment of the trace is ok but it is incomplete. In the middle we get:

Exception in thread "AWT-EventQueue-0" dk.aau.cs.util.RequireException: Tokens do not enable transition
 at dk.aau.cs.util.Require.that(Require.java:6)
 at dk.aau.cs.model.tapn.LocalTimedMarking.fireTransition(LocalTimedMarking.java:147)
 at dk.aau.cs.model.tapn.NetworkMarking.fireTransition(NetworkMarking.java:204)
 at dk.aau.cs.model.tapn.simulation.TAPNNetworkTimedTransitionStep.performStepFrom(TAPNNetworkTimedTransitionStep.java:21)
 at pipe.gui.Animator.setTimedTrace(Animator.java:127)
 at pipe.gui.Animator.SetTrace(Animator.java:89)
...

Is this a TAPAAL issue or the UPPAAL engine issue (problem is both with broadcast and broadcast degree 2; TAPAAL engine
gives good answer).

Revision history for this message
Jiri Srba (srba) wrote :
Revision history for this message
Jiri Srba (srba) wrote :

The last state before the exception is:

State:
( Control.P_lock Token0.P3 Token1.P3 Token2.P3 Token3.P0 Token4._BOTTOMIN_ Token5._BOTTOMIN_ Token6._BOTTOMIN_ )
Token0.x=4.46875 Token1.x=3.21875 Token2.x=1.96875 Token3.x=0.71875 Token4.x=4.46875 Token5.x=4.46875 Token6.x=4.46875 count0=0 count1=0 count2=0 Max=7 Active=4 lock=0 CapacityOutTokens=1 CapacityInTokens=2

and now comes the transition:

Transitions:
 Token4._BOTTOMIN_->Token4.P4 { (CapacityOutTokens == 1 || CapacityInTokens == 0) && lock == 0 && Active + 1 <= Max, T0!, x := 0, CapacityOutTokens := CapacityOutTokens - 1, Active := Active + 1 }
 Token3.P0->Token3.P1 { x > 1, T0?, 1 }

where Token3 should have age x>1, but it is only Token3.x=0.71875 in the state and hence the transition cannot fire.

This could be possibly a UPPAAL bug during trace generation?

Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

I have also tried now and I agree that this look like a UPPAAL trace bug. I tested this on various versions, including latest dev build for 64-bit mac.

Jiri Srba (srba)
Changed in tapaal:
importance: High → Low
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Bug attachments

Remote bug watches

Bug watches keep track of this bug in other bug trackers.