UPPAAL translations fail generating trace

[Jiri Srba]

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).

[Jiri Srba (srba)]

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?

[Mathias Grund Sørensen (mathias.grund)]

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.