remove files unneeded for lttv

[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
deleted file mode 100644 (file)
index 0c4a8c7..0000000
--- a/verif/nico-md-merge/commit_sum.log
+++ /dev/null
@@ -1,65 +0,0 @@
-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'