A forum for Spin users
You are not logged in.
Pages: 1
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
Pages: 1