TLC model checking RealTime module: problem with variable now

[loren...@xxxxxxxxx]

Hey!

I'm just getting started with TLA+, and wanted to try and check a simple behavior: the module RealTime specified in the Specifying Systems book, in conjunction with a custom module. 

The idea was to set a time bound on the VentriculePulse action, but when I try to test it, the following error comes up:

The subscript of the next-state relation specified by the specification does not seem to contain the state variable now Successor state is not completely specified by the next-state action.

How can I link the variable now to the VentriculePulse action, being that both elements appear in different components? Or should I somehow override the VentriculePulse action inside the RealTimeHeart module to state that now must remain unchanged?

--------------------------- MODULE RealTimeHeart ---------------------------
EXTENDS Reals, Heart, RealTime

RTHeart == /\ HeartSpec  
           /\ RTnow(ventriculeChannel) 
           /\ RTBound(VentriculePulse,ventriculeChannel,MinimumPeriod, MaximumPeriod)
           /\ (now = 0)
=============================================================================

----------------------------- MODULE RealTime -------------------------------
EXTENDS Reals 
VARIABLE now

RTBound(A, v, D, E) == 
      LET TNext(t)  ==  t' = IF <<A>>_v \/ ~(ENABLED <<A>>_v)'  \* The value of t will be 0 if an A action was executed or if A is no longer enabled.
                       THEN 0 
                       ELSE t + (now'-now)

  Timer(t) == (t=0)  /\  [][TNext(t)]_<<t, v, now>>
  \* Initial state in which 't' equals 0 and every possible state is a TNext step or leaves all variables unchanged

  MaxTime(t) == [](t \leq E) 
  \* The time 't' between two consecutive A actions cannot be greater than E

  MinTime(t) == [][A => t \geq D]_v 
  \* Before two consecutives A action occur, there must have passed at least D time

  IN \EE t : Timer(t) /\ MaxTime(t) /\ MinTime(t)
-----------------------------------------------------------------------------
RTnow(v) == LET NowNext == /\ now' \in {r \in Real : r > now} 
                       /\ UNCHANGED v
                       \* A NowNext step can advance 'now' by any amount of time while leaving v unchanged
        IN  /\ now \in Real 
            /\ [][NowNext]_now
            /\ \A r \in Real : WF_now(NowNext /\ (now'>r))
=============================================================================

------------------------------- MODULE Heart -------------------------------
EXTENDS Naturals
CONSTANT PossibleStimulus, MaximumPeriod, MinimumPeriod, stimulus

VARIABLE ventriculeChannel

Ventricule == INSTANCE Channel WITH Data <- PossibleStimulus, chan <- ventriculeChannel

-----------------------------------------------------------------------

TypeInvariant == Ventricule!TypeInvariant

HeartInit ==    /\ Ventricule!Init
            /\ MaximumPeriod >= MinimumPeriod
            /\ MinimumPeriod >= 0

VentriculePulse ==  Ventricule!Send(stimulus)

HeartSpec  ==  HeartInit /\ [][VentriculePulse]_ventriculeChannel
--------------------------------------------------------------
THEOREM  HeartSpec => []TypeInvariant
==============================================================

Thanks!

Lorenzo