TLC and RealTime

[Chris Pacejo <cpa...@xxxxxxxxxxxxxxxx>]

Hi all, dumb question:  Given that TLC does not support temporal existential quantification, and that the RTBound operator is defined using a temporal existential quantifier, what is the expected way to check real-time properties with TLC?

Should I take RealTime as a template and manually incorporate its ideas into my own spec without using temporal existential quantification?  (This seems to be the approach taken by the MCRealTimeHourClock example in the distribution, but it is labeled "Random junk right now" so I don't know how much attention I should pay it.)

For context, I am specifying a simple algorithm where certain steps may take real time, and I want to ensure that the whole algorithm completes within some real time bound.