TLC simulation error with liveness properties

Hi,

I'm working on a model that tries to simulate thread priorities (spec below) and while the TLC model checking works fine, the -simulate run fails with an weird error: 'Attempted to apply EXCEPT construct to the string "prio_en"' (it looks to me like a TLC bug but I may be tripping over some unsupported feature). It always fails after the maximum simulation depth. Removing the liveness properties from .cfg works fine. Note that full checking always succeeds.

Thanks,

Catalin

------------------------------ MODULE preempt ---------------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS PROCS, PRIORITY_LEVELS

Threads == PROCS \X (1..PRIORITY_LEVELS)

(* --algorithm preempt {
variables
	current_prio = [t \in PROCS |-> 1];
	worked	= [p \in Threads |-> FALSE];

define {
	ProcId(self)	== self[1]
	Priority(self)	== self[2]

	Enabled(self)	== Priority(self) >= current_prio[ProcId(self)]

	TypeInv		== /\ current_prio \in [PROCS -> 1..PRIORITY_LEVELS]
			   /\ worked \in [Threads -> BOOLEAN]

	Worked		== <>(\A t \in Threads : worked[t])
}

macro prio_enter(prio) {
	prio := current_prio[ProcId(self)];		\* save current priority
	current_prio[ProcId(self)] := Priority(self);	\* set the thread's priority
}

macro prio_exit(prio) {
	current_prio[ProcId(self)] := prio;		\* restore priority
}

fair+ process (t \in Threads)
	variable priority;
{
start:
	while (TRUE) {
prio_en:	await Enabled(self);
		prio_enter(priority);
work:		await Enabled(self);
		worked[self] := TRUE;
prio_ex:	await Enabled(self);
		prio_exit(priority);
	}
}
} *)
==============================================================================

SPECIFICATION Spec
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.

CONSTANTS PROCS = {p1, p2}
	  PRIORITY_LEVELS = 2

INVARIANTS TypeInv

PROPERTIES Worked