Re: TLC simulation error with liveness properties

[valentin....@xxxxxxx]

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
	TASK_NAME,
	CPUS

TASKS == {TASK_NAME} \X CPUS

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

fair process (task \in TASKS)
{
init:	var[self] := 0;
none:	skip;
work:	var[self] := 1;
}

} *)
=====
SPECIFICATION Spec

CONSTANTS CPUS = {cpu0}
	  TASK_NAME = task0

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.