Measuring memory usage

(6 posts) (4 voices)
  • Started 1 year ago by Saleem
  • Latest reply from Hilleman
  • 2 Members Subscribed To Topic

  1. Saleem
    Member

    How can we check memory used after verifying the specification/model/query? In verification results, I can just check. 1) Execution time 2) Diameter 3) States found and so on...but I can not check how much memory is used. Can any one help me in finding answer to this question.

    Posted 1 year ago #

  2. Daniel Ricketts
    Moderator

    Saleem,

    I'm not sure if I understand your question. Do you want to see how much memory is being used while the model checker is being run or after it is run? During the run, the memory being used can be checked as for any other process being run on your computer. We may able to display this value while the model checker is running. If you mean the amount of memory used after the model checker is finished, then I don't understand your question. Sorry, but could please clarify? Thanks.

    Dan

    Posted 1 year ago #

  3. Saleem
    Member

    Daniel Thanks for you reply. I do not know if it is possible using TLC or not. But I want to know how much memory was used after the model checker has run. In other model checkers like Uppaal we can check how much memory was used after a query has processed. In TLC 1) Execution time 2) Diameter 3) and States found are quite explicit from the results obtained but not the memory usage. Is it possible in TLC?

    Saleem

    Posted 1 year ago #

  4. Daniel Ricketts
    Moderator

    Saleem,

    Thanks for your TLC question. So you would like to see the peak memory usage that occurred during the run of TLC, as the utility memtime does for Uppaal. Am I understanding this correctly? Currently, this would only be possible using an external application, not directly through TLC. However, we may be able to add peak memory usage information as a TLC feature in the future. How would you use the memory information if it were available? I'd like to hear about your specific use case.

    Dan

    Posted 1 year ago #

  5. Leslie Lamport
    Key Master

    I'm not sure if the request makes sense, since TLC can use as much memory it is given. (See the "Maximum JVM heap size in MB" option in the "How to Run" section of the Model Overview page in the Toolbox.) I don't know how that memory is allocated to the different model checking tasks, but I could find out. However, Saleem apparently wants memory-usage information for comparing TLC with other model checkers. His request therefore has lower priority than the many pending tasks that will improve TLC or make it easier to use. Unless other people indicate that they want such a feature, it will not be implemented.

    Leslie

    Posted 1 year ago #

  6. Hilleman
    Member

    I want to know how much memory was used after the model checker has run. In other model checkers like Uppaal we can check how much memory was used after a query has processed. ipad2 Chargers iPad 2 Pouch Case ipad 2 Soft case

    Posted 8 months ago #

RSS feed for this topic

Reply

You must log in to post.