loren...@gmail.com
unread,Apr 2, 2018, 12:59:07 AM4/2/18Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Sign in to report message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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