model-checker: new examples for liveness model checking

model-checker : add or remove debug information

model-checker : change variable successors (local->global) in dfs algorithm

model-checker : memory leaks fixed in dfs algorithm for liveness properties

model-checker : function mmalloc_compare_mdesc fixed (blocks unchecked)

model-checker : function to compare values of propositional symbols fixed

model-checker : remove unused variables

model-checker : function to compare propositional symbol values

model-checker : change printf for size_t variables

model-checker : test data in libsimgrid memory region between each state

model-checker : new functions to compare mmalloc in std_heap

model-checker : add type in s_mc_mem_region (0=std_heap, 1=libsimgrid)

model-checker : add files for examples

model-checker : nettoyage du code

model-checker : new comparison for reached pairs (automaton state + values of propositional symbols + snapshot of system state)

model-checker : new comparison of pair reached (automaton state + values of propositional symbols)

model-checker : delete visited in struct xbt_state_t (unused)

model-checker : delete struct reached_pair_stateless unused

model-checker : delete num in struct mc_pair_t

model-checker : empty pair for stateless ddfs fixed

model-checker : ddfs stateless and stateful fixed

model-checker : update ddfs stateful model checking for liveness properties, bug with stateless mode

model-checker : new structure reached_pair_stateless for acceptance cyle detection

model-checker : stateless model checking for liveness properties

model-checker : separate informations for safety stateful/stateless and liveness stateful/stateless

model-checker : new example bugged1 for stateful dpor

model-checker : one more condition before interleaving process in state

model-checker : add condition of invisibility to reduce transitions

model-checker : new structure mc_pair_prop_t and backup of the values of atomic propositions for each state

model-checker : DPOR (independant transitions) algorithm for liveness properties

model-checker : separate dfs and dpor algorithms with restore snapshot/replay or visited states

model-checker : example changed

model-checker : 128bits->160bits for hash of visited pair

model-checker : restore interleaved process when restore snapshot

model-checker : dfs with good restore snapshot

model-checker : correction of dfs algorithm for liveness properties

model-checker : test dpor without replay from initial state but with
restore snapshot -> ok for safety properties, need more specifications
for liveness

model-checker : rename file mc_dfs -> mc_liveness

MC LTL : last version dfs algorithm before reduction

MC LTL : add statistics

model checker : dfs algorithm corrected

model-check : show stack when property not valid

model-check : dump stack for acceptance cycle

model-check : show stack for acceptance cycle

model check : acceptance cycle detection with automaton (depth first search without dpor)

détection de cycle d'acceptation ok mais boucle infinie en cas d'absence de cycle

correction compile warnings

start new example with parsing lex/yacc of automaton in promela

include new files struct automaton for cmake

new dfs algorithm with automaton of LTL formula

new struct automaton

You can now specify if you want sleep to see memory usage.

Optimize bprintf during cluster loop.

Add optimization flag with gcc46.

use more consistently the resource create of models, killing some useless/borken forwarder methods

save some useless strdups

reduce the amount of damn paranoid checks in simdag. Valgrind is here to report the errors, nowadays

Fix memoryleak.

Need to set state_file and availability file into the loop.

There is no contexts in SimDag

Rewrite perl script for optorsim

Update include tag.

Move arguments outside of the loop of hosts.

Remove unused and old function.

Remove supernovae mode for SimGrid v3.7

Test the help command.

Update tag include

Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid

setup a mallocator for the simdag tasks. The gain is quite disapointing, but not null

memory cleanups

s/GRAS_STUB_GENERATOR/SIMGRID_LUA/ to actually match file name.

Guard against multiple inclusion.

Fix race condition with gras-mmrpc test.

Register messages before opening the sockets, to avoid to receive
unknown messages.

Figlet for 3.7 was incomplete.

Also do some whitespace cleanup (and save up to 247 bytes!).

tesh: add tests with empty output.

tesh: do not fail on empty output, when sorting is enabled.

Merge stuff again. Damn, I should pull before changing stuff

merge branches

use a user level mallocator on the task content

enlarge my cluster once again

Performance boost by using a swag internally in SD_simulate

Use the partial invalidation optimization by default for the network too

This memory leak fix did not work with complex simulations.

SIMIX_CANCELED is a more adapted state in SIMIX_comm_cancel()

restore some stuff that got killed from the gitignore during some sort of cleanup

enlarge my cluster

first prealpha not working prototype (please public keep away) version of what could be a GOAL loader using simdag

typo--

Add example to kill a process.

Timings have changed: comms cannot continue when a process is dead

Now that processes are terminated cleanly, this recv can fail

In case of failures, a process may become runnable without time step

Since commit e5922b4 (clean unfinished comms when terminating a process),
the test msg-actions was failing on a deadlock instead of waking up
the last process (who can terminate normally after a failed recv).

Improve debug messages

Revalidate Chord tesh output (the end of the simulation is clean now)

Make cancelling a non-running task a no-op

Fix remaining memory leaks in MSG

Simix: clean unfinished comms when terminating a process

Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot//simgrid/simgrid

Fighting more memory leaks in Chord

[trace] fix tesh'es to follow recent changes in the paje header