如何查找 NuSMV 模型使用的内存和运行时答案

【问题标题】：How to find memory and runtime used by a NuSMV model如何查找 NuSMV 模型使用的内存和运行时
【发布时间】：2018-11-30 22:08:54
【问题描述】：

给定一个 NuSMV 模型，如何找到它的运行时以及它消耗了多少内存？

因此可以在系统提示符下使用此命令找到运行时：/usr/bin/time -f "time %es" NuSMV filename.smv

上面给出了挂钟时间。有没有更好的方法从 NuSMV 本身获取运行时统计信息？

另外如何找出程序在处理文件期间使用了多少 RAM 内存？

【问题讨论】：

标签： performance time nusmv

【解决方案1】：

一种可能是使用usage 命令，该命令显示当前使用的RAM 数量，以及用户和系统工具自启动以来使用的时间（因此，应在您要分析的每个操作之前和之后调用usage）。

执行示例：

NuSMV > usage
Runtime Statistics
------------------
Machine name: *****
User time    0.005 seconds
System time  0.005 seconds

Average resident text size       =     0K
Average resident data+stack size =     0K
Maximum resident size            =  6932K

Virtual text size                =  8139K
Virtual data size                = 34089K
    data size initialized        =  3424K
    data size uninitialized      =   178K
    data size sbrk               = 30487K
Virtual memory limit             = -2147483648K (-2147483648K)

Major page faults = 0
Minor page faults = 2607
Swaps = 0
Input blocks = 0
Output blocks = 0
Context switch (voluntary) = 9
Context switch (involuntary) = 0

NuSMV > reset; read_model -i nusmvLab.2018.06.07.smv ; go ; check_property ; usage
-- specification (L6 != pc U cc = len) IN mm is true
-- specification  F (min = 2 & max = 9) IN mm is true
-- specification  G !((((max > arr[0] & max > arr[1]) & max > arr[2]) & max > arr[3]) & max > arr[4]) IN mm is true
-- invariant max >= min IN mm is true

Runtime Statistics
------------------
Machine name: *****
User time   47.214 seconds
System time  0.284 seconds

Average resident text size       =     0K
Average resident data+stack size =     0K
Maximum resident size            = 270714K

Virtual text size                =  8139K
Virtual data size                = 435321K
    data size initialized        =  3424K
    data size uninitialized      =   178K
    data size sbrk               = 431719K
Virtual memory limit             = -2147483648K (-2147483648K)

Major page faults = 1
Minor page faults = 189666
Swaps = 0
Input blocks = 48
Output blocks = 0
Context switch (voluntary) = 12
Context switch (involuntary) = 145

【讨论】：

所以只是在上面确认一下，用户时间是47.214秒还是47.214-0.005秒？而使用的内存是435321K还是435321+8139K？
@user_1_1_1 自工具启动以来，时间以绝对值形式给出，因此应计算运行某些命令之前/之后的增量时间。我认为应该跟踪的内存数字是 Memory resident size，因为另一个是 Virtual 内存数字，这些可能超过程序实际使用的内存。你可能想用谷歌仔细检查我的断言。