# Re: TLC simulation error with liveness properties

Hi,

I've hit what seems to be the exact same problem on a different Spec.

I modified your preempt example to try and pinpoint the issue:

----- MODULE simulate_bug -----
EXTENDS Naturals, TLC

CONSTANTS
CPUS

(* --algorithm test {
variables
var = [v \in TASKS |-> 0];
define {
Worked == <>(\A t \in TASKS : var[t] = 1)
}

{
init:	var[self] := 0;
none:	skip;
work:	var[self] := 1;
}

} *)
=====
SPECIFICATION Spec

CONSTANTS CPUS = {cpu0}

PROPERTIES Worked

\$> java tlc2.TLC -simulate simulate_bug.tla
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply EXCEPT construct to the string "none".

It seems the error only arises when all of the following conditions are met:
* The liveness property involves <>. I don't hit the bug if e.g. Worked == [](\A t \in TASKS : var[t] < 2)
* Each ProcSet element is a tuple

The Spec I'm working on (with which I hit the problem) meets those conditions.

As a sidenote, the error message is always of the shape 'Attempted to apply EXCEPT construct to the string "<label>"' where <label> is the SECOND label in the process for some reason.