# TLC model checking RealTime module: problem with variable now

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