TLC model checking RealTime module: problem with variable now

72 views
Skip to first unread message

loren...@gmail.com

unread,
Apr 2, 2018, 12:59:07 AM4/2/18
to tlaplus
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
Reply all
Reply to author
Forward
0 new messages