[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: loren...@xxxxxxxxx*Date*: Sun, 1 Apr 2018 20:52:57 -0700 (PDT)

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

- Prev by Date:
**Re: The level of the expression or operator substituted for 'Def' must be at most 0** - Next by Date:
**Re: The level of the expression or operator substituted for 'Def' must be at most 0** - Previous by thread:
**Re: The level of the expression or operator substituted for 'Def' must be at most 0** - Next by thread:
**Possible new language constructs for TLA+3?** - Index(es):