Spinroot

A forum for Spin users

You are not logged in.

#1 2015-01-22 21:29:23

Dharma
Member
Registered: 2011-09-21
Posts: 13

problem with the "verify" script?

Hi,
I'm using the latest version of modex - downloaded it two weeks ago.

When I ran verify 4_mutex.c, which is part of the modex/example, it says no error was found.

However, when I ran ./pan it does show the violation of  an assertion.

dharma@ubuntu:~/Downloads/modex/Examples$ verify 4_mutex.c

    Extract Model:
    ==============
modex 4_mutex.c
MODEX Version 2.7 - 1 January 2015
created: model and _modex_.run

    Compile and Run:
    ================
sh _modex_.run
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan: out of memory
    662568 bytes used
    4.29497e+09 bytes more needed
    1.57286e+10 bytes limit
hint: to reduce memory, recompile with
  -DBITSTATE # supertrace, approximation

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Hash-Compact 4 search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 179 byte, depth reached 0, errors: 0
        0 states, stored
        0 states, matched
        0 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000    equivalent memory usage for states (stored*(State-vector + overhead))
    0.000    actual memory usage for states (less than 1k)
4096.000    memory used for hash table (-w29)
    0.534    memory used for DFS stack (-m10000)
    0.632    total actual memory usage



pan: elapsed time 1.73e+07 seconds
pan: rate         0 states/second

No Errors Found
----

dharma@ubuntu:~/Downloads/modex/Examples$ ./pan
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: c_code line 103 precondition false: (now.cnt==1) (at depth 59)
pan: wrote model.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Hash-Compact 4 search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 260 byte, depth reached 100, errors: 1
     3643 states, stored
     2442 states, matched
     6085 transitions (= stored+matched)
     1012 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    1.001    equivalent memory usage for states (stored*(State-vector + overhead))
    0.373    actual memory usage for states (compression: 37.27%)
             state-vector as stored = 79 byte + 28 byte overhead
  128.000    memory used for hash table (-w24)
    0.534    memory used for DFS stack (-m10000)
  128.827    total actual memory usage



pan: elapsed time 0.07 seconds
pan: rate 52042.857 states/second

Offline

#2 2015-01-23 23:41:49

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: problem with the "verify" script?

It ran out of memory with the default settings that Modex/Verify uses.
Note that it tried to use -w29 -- and when you redid it manually you used -w24....

Offline

Board footer

Powered by FluxBB