Как найти память и время выполнения, используемые моделью NuSMV - PullRequest
Новая
       29

Как найти память и время выполнения, используемые моделью NuSMV

0 голосов
/ 01 декабря 2018

Учитывая модель NuSMV, как найти время выполнения и сколько памяти она потребляет?

Таким образом, время выполнения можно найти с помощью этой команды в системном приглашении: / usr / bin / time -f "time%es "NuSMV filename.smv

Выше приведено время настенных часов.Есть ли лучший способ получить статистику времени выполнения из самого NuSMV?

Кроме того, как узнать, сколько ОЗУ программа использовала при обработке файла?

1 Ответ

0 голосов
/ 05 декабря 2018

Одной из возможностей является использование команды usage, которая отображает как объем RAM , используемый в данный момент, так и User и System * 1007.* время, используемое инструментом с момента его запуска (таким образом, 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
...