Wrong error trace and "cannot generate trace" problem

I think the wrong trace generated when last=0 is a problem in UPPAAL. UPPAAL returns the same trace to trace for all translations. As far as i can tell TAPAAL parses and interprets the UPPAAL trace correctly.

Here is the UPPAAL trace returned for Optimized Standard Reduction (note that there is no delay between firing T0 and T1 even though there should be a small delay). I've added some comments to the trace to make it easier to see where the problem is:

/////////////////////// Initialize /////////////////////////////////////////
State:
( Control._a48 Lock.P_lock Token(1)._BOTTOM_ Token(2)._BOTTOM_ Token(3)._BOTTOM_ Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=0 Token(2).x=0 Token(3).x=0 Token(4).x=0 Token(5).x=0 lock=0

Transitions:
  Control._a48->Control._a49 { 1, c0!, 1 }
  Token(1)._BOTTOM_->Token(1).P0 { 1, c0?, 1 }

State:
( Control._a49 Lock.P_lock Token(1).P0 Token(2)._BOTTOM_ Token(3)._BOTTOM_ Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=0 Token(2).x=0 Token(3).x=0 Token(4).x=0 Token(5).x=0 lock=0

Transitions:
  Control._a49->Control.finish { 1, c1!, 1 }
  Token(2)._BOTTOM_->Token(2).P7 { 1, c1?, 1 }

State:
( Control.finish Lock.P_lock Token(1).P0 Token(2).P7 Token(3)._BOTTOM_ Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=0 Token(2).x=0 Token(3).x=0 Token(4).x=0 Token(5).x=0 lock=0

/////////////////////// Delay 3.5 /////////////////////////////////////////
Delay: 3.5

State:
( Control.finish Lock.P_lock Token(1).P0 Token(2).P7 Token(3)._BOTTOM_ Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=3.5 Token(1).x=3.5 Token(2).x=3.5 Token(3).x=3.5 Token(4).x=3.5 Token(5).x=3.5 lock=0

/////////////////////// Fire T0 /////////////////////////////////////////
Transitions:
  Lock.P_lock.P_T0_1_in { 1, T0_1_in!, x := 0 }
  Token(3)._BOTTOM_->Token(3).P_hp_T0_1 { 1, T0_1_in?, x := 0 }ck->L

State:
( Control.finish Lock.P_T0_1_in Token(1).P0 Token(2).P7 Token(3).P_hp_T0_1 Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=3.5 Token(2).x=3.5 Token(3).x=0 Token(4).x=3.5 Token(5).x=3.5 lock=0

Transitions:
  Lock.P_T0_1_in->Lock.P_T0_2_in { 1, T0_2_in!, x := 0 }
  Token(1).P0->Token(1).P_hp_T0_2 { x >= 3 && x < 4, T0_2_in?, 1 }

State:
( Control.finish Lock.P_T0_2_in Token(1).P_hp_T0_2 Token(2).P7 Token(3).P_hp_T0_1 Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=3.5 Token(2).x=3.5 Token(3).x=0 Token(4).x=3.5 Token(5).x=3.5 lock=0

Transitions:
  Lock.P_T0_2_in->Lock.P_T0_2_out { 1, T0_3!, x := 0 }
  Token(2).P7->Token(2).P6 { x > 3 && x <= 4, T0_3?, 1 }

State:
( Control.finish Lock.P_T0_2_out Token(1).P_hp_T0_2 Token(2).P6 Token(3).P_hp_T0_1 Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=3.5 Token(2).x=3.5 Token(3).x=0 Token(4).x=3.5 Token(5).x=3.5 lock=0

Transitions:
  Lock.P_T0_2_out->Lock.P_T0_1_out { 1, T0_2_out!, x := 0 }
  Token(1).P_hp_T0_2->Token(1).P1 { 1, T0_2_out?, 1 }

State:
( Control.finish Lock.P_T0_1_out Token(1).P1 Token(2).P6 Token(3).P_hp_T0_1 Token(4)._BOTTOM_ Token(5)._BOTTOM_ )
Lock.x=0 Token(1).x=3.5 Token(2).x=3.5 Token(3).x=0 Token(4).x=3.5 Token(5).x=3.5 lock=0

Transitions:
  Lock.P_T0_1_out->Lock.P_lock { 1, T0_1_out!, x := 0 }
  Token(3).P_hp_...

This problem seems to be fixed now. At least I cannot reproduce it on my Mac anymore. Please, verify and close this bug if true.

My observations:

Problem 1: This seems to be related to UPPAAL. Running verification using verifytapn, generates a correct, executable trace. Lasse described where the problem lies in the trace UPPAAL returns..

Problem 2: is not reproducable.

Problem 2. is not a problem any more. Just verified it and it has correct behaviour.

This is UPPAAL related problem, we will have to wait for a new development release of UPPAAL engine.

In the new development version of verifyta the generated trace can be executed. So this bug is closed.