Add a VDM-Util function for getting current system time

[ldcouto]

Identification of the Originator

Luis Diogo Couto

Target of the request, defining the affected components of the language definition

VDM-Util library (all dialects)

Motivation for the request

A need for basic performance analysis of VDM models. Although this can be done in the command line using something like the time command, it's not very practical and does not work for the IDE version.

Description of the request

description of the modification

Add a function for getting the current time (as reported by the system) to the VDM-Unit library. Proposed signature: sysCurrentTimeMillis: () -> int

Not to go down a rabbit hole but this function is technically not referentially transparent since it depends on the system time so maybe it should be an operation instead. I think a function would be more convenient and the existence of IO functions helps justify it being a function.

benefits from the modification

The modification would allow for the use of the current system time in whatever situation a user envisions. A concrete use is simple performance analysis by seeding start and stop times across various operations calls.

possible side effects

None, to the best of my knowledge. In theory, any model with a custom VDM-Util library will not benefit from this improvement but should still function normally.

A test suite for validation of the modification in the executable models (if appropriate).

SL:

functions
test : () -> int
test () == VDMUtil`sysCurrentTimeMillis()
post RESULT >= 0

PP/RT:

class A
functions
test : () -> int
test () == VDMUtil`sysCurrentTimeMillis()
post RESULT >= 0
end A

[peterwvj]

It could be useful to have such a functionality for optimization purposes. I do not like so the idea of making it a function (exactly for the reason you are giving) but another possibility could be to make it a static operation. At least this would allow it to be accessed in a convenient way. If sysCurrentTimeMillis is intended to return the number of milliseconds since January 1 1970 then I think it is safe to make the return type nat1 :)

[nlmave]

Although I understand the "need" for this functionality, I think it is a bad idea to put it in the VDM libraries; I see no use for this other than performance monitoring of the test suite. Moreover, it will be confused with the notion of time in VDM-RT (where the simulation wall-clock is not related to real time at all). If you want to do this, I suggest to use the standard library extension mechanism (as described in CH14 of the user manual) to implement this, as part of the regression test framework. Have you considered that option, and if so, are you still convinced it makes more sense to put it in the VDMUtil libs?

[ldcouto]

Yeah, I did. We already have performance analysis for our model so I don't really need this in the library. I think it's a useful thing but I see the point about confusion with VDM-RT.

[nickbattle]

​I think Luis did consider the VDMUnit framework - he was asking me about how to write callouts to Java and explained his idea. I suggested submitting it to the LB (as we own the libraries).

I can see the point about confusing "the time" with the RT time aspects, but to me this would be a stand-alone utility function rather than something that is necessarily part of VDMUnit​. Hence the suggestion for VDMUtils.

I think it should return a nat rather than an int with postconditions. I'm staying out of the function/operation debate :-)

[tomooda]

Luis,

I think a function would be more convenient and the existence of IO functions helps justify it being a function.

Very interesting. The following fragment of state definition in VDM-SL might be useful for debugging and one reason to define it as a function rather than an operation.

state SomeState of
somevar : sometype
inv mk_SomeState(s) ==
    IO`fwriteval("SomeState.log", mk_(VDMUtil`sysCurrentTimeMillis(), s), <append>)
    and realInvariant(s)
...
end

I think IO instead of VDMUtil may be better place to define sysCurrentTimeMillis because they look to have similar applications (logging, testing and debugging) and sysCurrentTimeMillis actually involves IO with the OS.

[peterwvj]

Thinking about it I do not really think that this functionality belongs in a modelling library. I have a hard time seeing the modelling perspective. I think what we did Luis, i.e. using the Java bridge to implement this feature, is probably the most appropriate way to do it. I know it's not as convenient as having it as a library function/operation but at least chapter 15 describes (as pointed out by MV) how to contribute features that require interacting with Java.

[ldcouto]

I don't particularly disagree that the Java bridge is the way to go. But that's how the existing libraries work anyway. I think this is a matter of you guys deciding whether it's useful in general or not. If the existing libraries don't make sense for it, perhaps we could make it available in a new one?

I'm under the impression that we are moving towards using Overture for design exploration so simulation performance could become a concern. From that perspective, some support for profiling could be very helpful.

@tomooda 's example is exactly why I suggested a function. You can use them in more places than operations.

[tomooda]

I think the point is whether or not VDMUtil and IO are dedicated to modeling purpose only. I see some functions and operations, e.g. VDMUtil```get_file_pos, are not really for modeling purpose but seem like a for-convenience development utility. To me, the current library looks mixture of for modeling and for convenience.

If VDMUtil should be only for modeling purpose, I'd suggest to create a new library, e.g. DevUtil, to re-organize the existing library contents and separate modeling utilities and for-convenience dev utilities.

[peterwvj]

I do agree that systemCurrentTimeMillis() is a useful function to have, and putting convenience functionality in a "development" library could perhaps be a good way to keep a clear separation between modelling and development related functionality. Model simulation performance is a general concern so I'm not against adding new functionality that supports profiling.

[nlmave]

Dear Tomohiro,

(1) VDMUtil is a legacy library that was created to remain compatibility with VDMTools, from which it originates (2) The scope and content was never under control of the language board; it was created by CSK to support Felica where efficiency of these functions was a great concern. (3) IMHO there is a big difference between supporting simple IO functions (to access files) and math libraries with introducing a second notion of time, just for the sake of measuring the elapse time of the model execution

As I said before, any developer can create utility functions in external libraries using the standard features already available (to execute arbitrary java code in the context of the specification)

I think we need to be really conservative in extending standard library functions, to me:

• they should have a real benefit and purpose from the modelling perspective
• their behavior should not rely on the operating system onto which the Overturetool is executed (in this case: the resolution of the timer)
• their semantics should not clash with built-in language features (in this case: time in VDM++)

Regards, Marcel

On 15-4-2015 1:48, Tomohiro Oda wrote:

I think the point is whether or not VDMUtil and IO are dedicated to modeling purpose only. I see some functions and operations, e.g. |VDMUtil|`|get_file_pos|, are not really for modeling purpose but seem like a for-convenience development utility. To me, the current library looks mixture of for modeling and for convenience.

If VDMUtil should be only for modeling purpose, I'd suggest to create a new library, e.g. |DevUtil|, to re-organize the existing library contents and separate modeling utilities and for-convenience dev utilities.

— Reply to this email directly or view it on GitHub https://github.com/overturetool/language/issues/31#issuecomment-93116769.

[tomooda]

Marcel, Thank you for explaining the historical context of VDMUtil.

I think most of us agree that the proposed function is not for describing a model, but for convenience of developing a model.

Timestamping is a common habit of investigating a model execution. It's not strongly common, but I think VDMTools community also has (or had) a need for timestamps because VDMTools have the VDMUtil```current_time operation that returns the number of milliseconds since the epoch time.

With regard to the conflict with VDM-RT's time, I think millisecondsClockValue instead of systemCurrentTimeMillis may be a better name to avoid confusion.

And as I wrote before, I think we need to separate for-convenience utilities from for-modeling utilities. The current mixture of them does not justify further mixture.

To me, the point has now come down to a simple question: Do we take care of supporting a shared method to develop a model? Overture community and VDMTools community already have different ways to get a timestamp. Overture users can use the Java bridging mechanism. VDMTools users can use the current_time operation. However, I still think it's a good thing to have a common way to timestamp shared by the VDM community.

Honestly speaking, I haven't decided my call. It seems to me that pros and cons are close. If this RM accepts to rename the function to millisecondsClockValue (or any name that does not mention "time") and move it to a separate library (something like DevLib), I think cons will become small enough to afford pros.

[shinsahara]

Hi all,

I vote the "DevLib", and keep VDMUtil as old fashion.

Cheers, Shin

P.S. I found I can't vote :-)

2015/04/16 10:45、Tomohiro Oda notifications@github.com のメール：

Marcel, Thank you for explaining the historical context of VDMUtil.

I think most of us agree that the proposed function is not for describing a model, but for convenience of developing a model.

Timestamping is a common habit of investigating a model execution. It's not strongly common, but I think VDMTools community also has (or had) a need for timestamps because VDMTools have the VDMUtil`current_time operation that returns the number of milliseconds since the epoch time.

With regard to the conflict with VDM-RT's time, I think millisecondsClockValue instead of systemCurrentTimeMillis may be a better name to avoid confusion.

And as I wrote before, I think we need to separate for-convenience utilities from for-modeling utilities. The current mixture of them does not justify further mixture.

To me, the point has now come down to a simple question: Do we take care of supporting a shared method to develop a model? Overture community and VDMTools community already have different ways to get a timestamp. Overture users can use the Java bridging mechanism. VDMTools users can use the current_time operation. However, I still think it's a good thing to have a common way to timestamp shared by the VDM community.

Honestly speaking, I haven't decided my call. It seems to me that pros and cons are close. If this RM accepts to rename the function to millisecondsClockValue (or any name that does not mention "time") and move it to a separate library (something like DevLib), I think cons will become small enough to afford pros.

— Reply to this email directly or view it on GitHub https://github.com/overturetool/language/issues/31#issuecomment-93614790.

[ardbeg1958]

Hi all,

Even in a modeling activity, sometime we wish to collect date and time from the environment (please suppose we'd like to write down a mail/news server spec and want to animate the spec). In that sense, I think, it is necessary to have a time collecting feature.

The problem is, if we use the feature for another 'meta' purpose, it may interfere the modeling purpose on the way like RT time case.

The easiest work around on this might be to use existing cycles statement like:

cycles (0) IOfwriteval("SomeState.log", mk_(VDMUtilsysCurrentTimeMillis(), s), ) (assuming we have "VDMUtil`sysCurrentTimeMillis()" here).

Since we already have such an interpreter directive (cycles) in the language, isn't this a fair use of the statement?

For this reason, I basically agree to accept the original RM.

However, I still think it's a good thing to have a common way to timestamp shared by the VDM community.

I agree also this Tomo's statement. Both Overture and VDMTools can have VDMUtil`sysCurrentTimeMillis. In VDMTools, we can define sysCurrentTimeMillis as synonym of current_time.

[nlmave]

Dear Hiroshi,

Please have a look at chapter 15 of the user manual, http://raw.github.com/overturetool/documentation/master/documentation/UserGuideOvertureIDE/OvertureIDEUserGuide.pdf; accessing specific functions from the environment is possible with already available means.

Extension of a standard library is really not needed. It just creates a maintenance (and portability) problem and we open a virtual can-of-worms (there is no limit to other "useful" features that we could include as well - how about the ability to read and write XML files for example).

My position remains: we should really reject this RM!

Regards, Marcel

On 16-4-2015 6:48, SAKO Hiroshi wrote:

Hi all,

Even in a modeling activity, sometime we wish to collect date and time from the environment (please suppose we'd like to write down a mail/news server spec and want to animate the spec). In that sense, I think, it is necessary to have a time collecting feature.

The problem is, if we use the feature for another 'meta' purpose, it may interfere the modeling purpose on the way like RT time case.

The easiest work around on this might be to use existing cycles statement like:

cycles (0) IO|fwriteval("SomeState.log", mk_(VDMUtil|sysCurrentTimeMillis(), s), )

(assuming we have "VDMUtil`sysCurrentTimeMillis()" here).

For this reason, I agree to accept the original RM.

— Reply to this email directly or view it on GitHub https://github.com/overturetool/language/issues/31#issuecomment-93639885.

[kgpierce]

If performance analysis is useful in general, wouldn't it be better to have a tool feature? For example, we have the coverage feature to assess models, so why not have similar for timing.

[ardbeg1958]

Dear Marcel-san

Extension of a standard library is really not needed. It just creates a maintenance (and portability) problem and we open a virtual can-of-worms (there is no limit to other "useful" features that we could include as well - how about the ability to read and write XML files for example).

You are right.

Maybe such "useful" features must not be supported by lang. nor std. libs. They should be provided uder 3rd party libs or tool's features.

I'm going to vote to reject this RM.

[peterwvj]

Since the Language Board has unanimously decided to reject this RM I'll label the RM as so and close this issue.