null value assigned to a sequence at model checker

When I run TLC, a "null" value is assigned to a sequence, even though a "seq>0" test is done. The spec and config files are attached. The output is:

TLC2 Version 2.05 of 23 July 2013

Running in Model-Checking mode.

Parsing file SimpleScheduler.tla

Parsing file /tmp/Naturals.tla

Parsing file /tmp/Sequences.tla

Semantic processing of module Naturals

Semantic processing of module Sequences

Semantic processing of module SimpleScheduler

Starting... (2015-03-27 15:21:52)

Computing initial states...

Finished computing initial states: 1 distinct state generated.

Error: Successor state is not completely specified by the next-state action.

Error: The behavior up to this point is:

State 1: <Initial predicate>

/\ running = (c1 :> NoThread @@ c2 :> NoThread)

/\ runQ = (c1 :> <<>> @@ c2 :> <<>>)

State 2: <Action line 20, col 5 to line 21, col 28 of module SimpleScheduler>

/\ running = (c1 :> NoThread @@ c2 :> NoThread)

/\ runQ = (c1 :> <<t1>> @@ c2 :> <<>>)

State 3: <Action line 24, col 4 to line 25, col 48 of module SimpleScheduler>

/\ running = (c1 :> t1 @@ c2 :> NoThread)

/\ runQ = null

11 states generated, 6 distinct states found, 4 states left on queue.

The depth of the complete state graph search is 3.

Finished. (2015-03-27 15:21:52)

My questions are: a set of sequences is not allowed in the spec? Or the sequence is not well defined or checked?

Thanks in advance

Regards

Adriano.