move everything out of trunk

[lttv.git] / verif / nico-md-merge / commit_sum.log

diff --git a/verif/nico-md-merge/commit_sum.log b/verif/nico-md-merge/commit_sum.log
new file mode 100644 (file)
index 0000000..0c4a8c7
--- /dev/null
+++ b/verif/nico-md-merge/commit_sum.log
@@ -0,0 +1,65 @@
+make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge'
+rm -f pan* trail.out
+cat defines > pan.ltl
+spin -f "!(`cat commit_sum.ltl | grep -v ^//`)" >> pan.ltl
+spin -a -X -N pan.ltl model.spin
+Exit-Status 0
+gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR  pan.c
+./pan -v -X -m100000 -w21  -a -c1
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 302)
+
+(Spin Version 5.1.6 -- 9 May 2008)
+       + Partial Order Reduction
+
+Full statespace search for:
+       never claim             +
+       assertion violations    + (if within scope of claim)
+       acceptance   cycles     + (fairness disabled)
+       invalid end states      - (disabled by never claim)
+
+State-vector 92 byte, depth reached 178, errors: 0
+   117886 states, stored
+   210653 states, matched
+   328539 transitions (= stored+matched)
+   440774 atomic steps
+hash conflicts:      3201 (resolved)
+
+Stats on memory usage (in Megabytes):
+   12.142      equivalent memory usage for states (stored*(State-vector + overhead))
+    8.971      actual memory usage for states (compression: 73.88%)
+               state-vector as stored = 64 byte + 16 byte overhead
+    8.000      memory used for hash table (-w21)
+    3.052      memory used for DFS stack (-m100000)
+   19.939      total actual memory usage
+
+unreached in proctype switcher
+       line 81, "pan.___", state 8, "(1)"
+       line 87, "pan.___", state 15, "write_off = new_off"
+       line 84, "pan.___", state 18, "((prev_off!=write_off))"
+       line 84, "pan.___", state 18, "else"
+       line 97, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
+       line 103, "pan.___", state 25, "(1)"
+       line 98, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
+       line 98, "pan.___", state 26, "else"
+       line 91, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)"
+       (7 of 31 states)
+unreached in proctype tracer
+       line 177, "pan.___", state 48, "events_lost = (events_lost+1)"
+       (1 of 51 states)
+unreached in proctype reader
+       (0 of 29 states)
+unreached in proctype cleaner
+       (0 of 9 states)
+unreached in proctype :init:
+       line 284, "pan.___", state 35, "(run switcher())"
+       (1 of 43 states)
+unreached in proctype :never:
+       line 307, "pan.___", state 8, "-end-"
+       (1 of 8 states)
+
+pan: elapsed time 0.91 seconds
+pan: rate 129545.05 states/second
+pan: avg transition delay 2.7698e-06 usec
+make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge'