Marion Guthmuller [Tue, 15 Nov 2011 15:51:03 +0000 (16:51 +0100)]
model-checker : detection of acceptance cycle when the first acceptance pair reached
Marion Guthmuller [Mon, 14 Nov 2011 16:15:47 +0000 (17:15 +0100)]
model-checker : add region (data of program) in snapshot
Marion Guthmuller [Mon, 14 Nov 2011 16:14:30 +0000 (17:14 +0100)]
model-checker : add name of program in arguments of function MSG_main_liveness_stateless, MC_modelcheck_liveness_stateless, MC_init_liveness_stateless, MC_ddfs_stateless_init and MC_ddfs_stateless
Marion Guthmuller [Thu, 10 Nov 2011 10:12:52 +0000 (11:12 +0100)]
model-checker : MC_replay_liveness function extended to replay all pairs in stack or just a part
Marion Guthmuller [Wed, 9 Nov 2011 10:59:32 +0000 (11:59 +0100)]
model-checker : example for detection of acceptance cycle with liveness properties fixed
Marion Guthmuller [Wed, 9 Nov 2011 10:57:22 +0000 (11:57 +0100)]
model-checker : new version of stateless double dfs algorithm for liveness properties
Marion Guthmuller [Wed, 9 Nov 2011 10:56:39 +0000 (11:56 +0100)]
model-checker : add number of requests executed for each pair in s_mc_pair_stateless structure
Marion Guthmuller [Wed, 9 Nov 2011 10:54:54 +0000 (11:54 +0100)]
model-checker : pair without request executed not replay in MC_replay_liveness function
Marion Guthmuller [Mon, 7 Nov 2011 14:47:04 +0000 (15:47 +0100)]
model-checker : add new MAX_DEPTH_LIVENESS with verification liveness properties
Marion Guthmuller [Fri, 4 Nov 2011 15:13:42 +0000 (16:13 +0100)]
model-checker : last version (incorrect) of double dfs algorithm for liveness properties before major rewrite to correct an error in the behavior of MC (possible evolution in Büchi automaton untreated)
Marion Guthmuller [Thu, 3 Nov 2011 13:39:53 +0000 (14:39 +0100)]
model-checker : more condition (state with processes interleaved > 0) for detection of acceptance cycle
Marion Guthmuller [Thu, 3 Nov 2011 13:37:08 +0000 (14:37 +0100)]
model-checker: new examples for liveness model checking
Marion Guthmuller [Wed, 2 Nov 2011 13:37:57 +0000 (14:37 +0100)]
model-checker : add or remove debug information
Marion Guthmuller [Wed, 2 Nov 2011 13:35:31 +0000 (14:35 +0100)]
model-checker : change variable successors (local->global) in dfs algorithm
Marion Guthmuller [Wed, 2 Nov 2011 13:19:08 +0000 (14:19 +0100)]
model-checker : memory leaks fixed in dfs algorithm for liveness properties
Marion Guthmuller [Fri, 28 Oct 2011 14:14:22 +0000 (16:14 +0200)]
model-checker : function mmalloc_compare_mdesc fixed (blocks unchecked)
Marion Guthmuller [Tue, 25 Oct 2011 14:44:25 +0000 (16:44 +0200)]
model-checker : function to compare values of propositional symbols fixed
Marion Guthmuller [Tue, 25 Oct 2011 12:36:24 +0000 (14:36 +0200)]
model-checker : remove unused variables
Marion Guthmuller [Tue, 25 Oct 2011 11:21:28 +0000 (13:21 +0200)]
model-checker : function to compare propositional symbol values
Marion Guthmuller [Tue, 25 Oct 2011 08:47:11 +0000 (10:47 +0200)]
model-checker : change printf for size_t variables
Marion Guthmuller [Fri, 21 Oct 2011 12:27:46 +0000 (14:27 +0200)]
model-checker : test data in libsimgrid memory region between each state
Marion Guthmuller [Wed, 12 Oct 2011 15:06:29 +0000 (17:06 +0200)]
model-checker : new functions to compare mmalloc in std_heap
Marion Guthmuller [Tue, 4 Oct 2011 07:52:30 +0000 (09:52 +0200)]
model-checker : add type in s_mc_mem_region (0=std_heap, 1=libsimgrid)
Marion Guthmuller [Thu, 22 Sep 2011 16:12:01 +0000 (18:12 +0200)]
model-checker : add files for examples
Marion Guthmuller [Thu, 22 Sep 2011 16:05:17 +0000 (18:05 +0200)]
model-checker : nettoyage du code
Marion Guthmuller [Wed, 21 Sep 2011 14:59:05 +0000 (16:59 +0200)]
model-checker : new comparison for reached pairs (automaton state + values of propositional symbols + snapshot of system state)
Marion Guthmuller [Thu, 15 Sep 2011 15:40:24 +0000 (17:40 +0200)]
model-checker : new comparison of pair reached (automaton state + values of propositional symbols)
Marion Guthmuller [Tue, 13 Sep 2011 15:56:54 +0000 (17:56 +0200)]
model-checker : delete visited in struct xbt_state_t (unused)
Marion Guthmuller [Mon, 12 Sep 2011 13:24:43 +0000 (15:24 +0200)]
model-checker : delete struct reached_pair_stateless unused
Marion Guthmuller [Mon, 12 Sep 2011 12:58:30 +0000 (14:58 +0200)]
model-checker : delete num in struct mc_pair_t
Marion Guthmuller [Fri, 9 Sep 2011 15:52:13 +0000 (17:52 +0200)]
model-checker : empty pair for stateless ddfs fixed
Marion Guthmuller [Tue, 23 Aug 2011 16:46:29 +0000 (18:46 +0200)]
model-checker : ddfs stateless and stateful fixed
Marion Guthmuller [Mon, 22 Aug 2011 09:27:09 +0000 (11:27 +0200)]
model-checker : update ddfs stateful model checking for liveness properties, bug with stateless mode
Marion Guthmuller [Sun, 21 Aug 2011 11:02:18 +0000 (13:02 +0200)]
model-checker : new structure reached_pair_stateless for acceptance cyle detection
Marion Guthmuller [Sun, 21 Aug 2011 09:37:04 +0000 (11:37 +0200)]
model-checker : stateless model checking for liveness properties
Marion Guthmuller [Sat, 20 Aug 2011 15:24:24 +0000 (17:24 +0200)]
model-checker : separate informations for safety stateful/stateless and liveness stateful/stateless
Marion Guthmuller [Tue, 16 Aug 2011 14:01:23 +0000 (16:01 +0200)]
model-checker : new example bugged1 for stateful dpor
Marion Guthmuller [Wed, 20 Jul 2011 12:57:24 +0000 (14:57 +0200)]
model-checker : one more condition before interleaving process in state
Marion Guthmuller [Tue, 19 Jul 2011 16:10:51 +0000 (18:10 +0200)]
model-checker : add condition of invisibility to reduce transitions
Marion Guthmuller [Tue, 5 Jul 2011 10:20:04 +0000 (12:20 +0200)]
model-checker : new structure mc_pair_prop_t and backup of the values of atomic propositions for each state
Marion Guthmuller [Tue, 5 Jul 2011 09:16:08 +0000 (11:16 +0200)]
model-checker : DPOR (independant transitions) algorithm for liveness properties
Marion Guthmuller [Fri, 1 Jul 2011 15:02:03 +0000 (17:02 +0200)]
model-checker : separate dfs and dpor algorithms with restore snapshot/replay or visited states
Marion Guthmuller [Fri, 24 Jun 2011 15:20:26 +0000 (17:20 +0200)]
model-checker : example changed
Marion Guthmuller [Fri, 24 Jun 2011 13:44:19 +0000 (15:44 +0200)]
model-checker : 128bits->160bits for hash of visited pair
Marion Guthmuller [Fri, 24 Jun 2011 12:30:42 +0000 (14:30 +0200)]
model-checker : restore interleaved process when restore snapshot
Marion Guthmuller [Fri, 24 Jun 2011 12:24:47 +0000 (14:24 +0200)]
model-checker : dfs with good restore snapshot
Marion Guthmuller [Fri, 24 Jun 2011 09:51:08 +0000 (11:51 +0200)]
model-checker : correction of dfs algorithm for liveness properties
Marion Guthmuller [Mon, 20 Jun 2011 14:00:37 +0000 (16:00 +0200)]
model-checker : test dpor without replay from initial state but with
restore snapshot -> ok for safety properties, need more specifications
for liveness
Marion Guthmuller [Fri, 17 Jun 2011 07:13:40 +0000 (09:13 +0200)]
model-checker : rename file mc_dfs -> mc_liveness
Marion Guthmuller [Fri, 20 May 2011 16:14:01 +0000 (18:14 +0200)]
MC LTL : last version dfs algorithm before reduction
Marion Guthmuller [Fri, 20 May 2011 08:41:01 +0000 (10:41 +0200)]
MC LTL : add statistics
Marion Guthmuller [Thu, 19 May 2011 15:41:45 +0000 (17:41 +0200)]
model checker : dfs algorithm corrected
Marion Guthmuller [Wed, 4 May 2011 14:26:47 +0000 (16:26 +0200)]
model-check : show stack when property not valid
Marion Guthmuller [Wed, 4 May 2011 14:18:02 +0000 (16:18 +0200)]
model-check : dump stack for acceptance cycle
Marion Guthmuller [Wed, 4 May 2011 14:07:05 +0000 (16:07 +0200)]
model-check : show stack for acceptance cycle
Marion Guthmuller [Wed, 4 May 2011 11:45:41 +0000 (13:45 +0200)]
model check : acceptance cycle detection with automaton (depth first search without dpor)
Marion Guthmuller [Fri, 29 Apr 2011 08:31:48 +0000 (10:31 +0200)]
détection de cycle d'acceptation ok mais boucle infinie en cas d'absence de cycle
Marion Guthmuller [Thu, 21 Apr 2011 09:32:22 +0000 (11:32 +0200)]
correction compile warnings
Marion Guthmuller [Thu, 21 Apr 2011 08:44:17 +0000 (10:44 +0200)]
start new example with parsing lex/yacc of automaton in promela
Marion Guthmuller [Thu, 21 Apr 2011 08:35:11 +0000 (10:35 +0200)]
include new files struct automaton for cmake
Marion Guthmuller [Thu, 21 Apr 2011 08:25:50 +0000 (10:25 +0200)]
new dfs algorithm with automaton of LTL formula
Marion Guthmuller [Thu, 21 Apr 2011 08:10:51 +0000 (10:10 +0200)]
new struct automaton
Navarrop [Fri, 21 Oct 2011 11:07:27 +0000 (13:07 +0200)]
You can now specify if you want sleep to see memory usage.
Navarrop [Fri, 21 Oct 2011 10:32:56 +0000 (12:32 +0200)]
Optimize bprintf during cluster loop.
Navarrop [Fri, 21 Oct 2011 10:32:35 +0000 (12:32 +0200)]
Add optimization flag with gcc46.
Martin Quinson [Thu, 20 Oct 2011 14:17:35 +0000 (16:17 +0200)]
use more consistently the resource create of models, killing some useless/borken forwarder methods
Martin Quinson [Thu, 20 Oct 2011 14:15:56 +0000 (16:15 +0200)]
save some useless strdups
Martin Quinson [Thu, 20 Oct 2011 13:20:32 +0000 (15:20 +0200)]
reduce the amount of damn paranoid checks in simdag. Valgrind is here to report the errors, nowadays
Navarrop [Thu, 20 Oct 2011 12:42:56 +0000 (14:42 +0200)]
Fix memoryleak.
Navarrop [Thu, 20 Oct 2011 12:42:33 +0000 (14:42 +0200)]
Need to set state_file and availability file into the loop.
Christophe Thiéry [Thu, 20 Oct 2011 12:02:25 +0000 (14:02 +0200)]
There is no contexts in SimDag
Navarrop [Thu, 20 Oct 2011 11:22:19 +0000 (13:22 +0200)]
Rewrite perl script for optorsim
Navarrop [Thu, 20 Oct 2011 11:21:56 +0000 (13:21 +0200)]
Update include tag.
Navarrop [Thu, 20 Oct 2011 11:21:18 +0000 (13:21 +0200)]
Move arguments outside of the loop of hosts.
Navarrop [Thu, 20 Oct 2011 09:14:17 +0000 (11:14 +0200)]
Remove unused and old function.
Navarrop [Thu, 20 Oct 2011 09:11:25 +0000 (11:11 +0200)]
Remove supernovae mode for SimGrid v3.7
Navarrop [Thu, 20 Oct 2011 09:10:23 +0000 (11:10 +0200)]
Test the help command.
Navarrop [Mon, 17 Oct 2011 15:35:37 +0000 (17:35 +0200)]
Update tag include
Martin Quinson [Thu, 20 Oct 2011 11:26:50 +0000 (13:26 +0200)]
Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
Martin Quinson [Thu, 20 Oct 2011 11:26:28 +0000 (13:26 +0200)]
setup a mallocator for the simdag tasks. The gain is quite disapointing, but not null
Martin Quinson [Thu, 20 Oct 2011 11:24:15 +0000 (13:24 +0200)]
memory cleanups
Arnaud Giersch [Tue, 18 Oct 2011 07:41:02 +0000 (09:41 +0200)]
s/GRAS_STUB_GENERATOR/SIMGRID_LUA/ to actually match file name.
Arnaud Giersch [Tue, 18 Oct 2011 07:40:24 +0000 (09:40 +0200)]
Guard against multiple inclusion.
Arnaud Giersch [Fri, 14 Oct 2011 11:38:25 +0000 (13:38 +0200)]
Fix race condition with gras-mmrpc test.
Register messages before opening the sockets, to avoid to receive
unknown messages.
Arnaud Giersch [Tue, 11 Oct 2011 11:17:40 +0000 (13:17 +0200)]
Figlet for 3.7 was incomplete.
Also do some whitespace cleanup (and save up to 247 bytes!).
Arnaud Giersch [Thu, 20 Oct 2011 09:21:18 +0000 (11:21 +0200)]
tesh: add tests with empty output.
Arnaud Giersch [Thu, 20 Oct 2011 09:20:58 +0000 (11:20 +0200)]
tesh: do not fail on empty output, when sorting is enabled.
Martin Quinson [Thu, 20 Oct 2011 08:27:04 +0000 (10:27 +0200)]
Merge stuff again. Damn, I should pull before changing stuff
Martin Quinson [Thu, 20 Oct 2011 08:25:30 +0000 (10:25 +0200)]
merge branches
Martin Quinson [Thu, 20 Oct 2011 08:19:18 +0000 (10:19 +0200)]
use a user level mallocator on the task content
Martin Quinson [Thu, 20 Oct 2011 08:17:59 +0000 (10:17 +0200)]
enlarge my cluster once again
Martin Quinson [Thu, 20 Oct 2011 08:11:44 +0000 (10:11 +0200)]
Performance boost by using a swag internally in SD_simulate
Martin Quinson [Thu, 20 Oct 2011 07:47:59 +0000 (09:47 +0200)]
Use the partial invalidation optimization by default for the network too
Christophe Thiéry [Thu, 20 Oct 2011 06:39:27 +0000 (08:39 +0200)]
This memory leak fix did not work with complex simulations.
Christophe Thiéry [Thu, 20 Oct 2011 06:39:03 +0000 (08:39 +0200)]
SIMIX_CANCELED is a more adapted state in SIMIX_comm_cancel()
Martin Quinson [Wed, 19 Oct 2011 19:48:16 +0000 (21:48 +0200)]
restore some stuff that got killed from the gitignore during some sort of cleanup
Martin Quinson [Wed, 19 Oct 2011 19:47:44 +0000 (21:47 +0200)]
enlarge my cluster
Martin Quinson [Wed, 19 Oct 2011 19:47:23 +0000 (21:47 +0200)]
first prealpha not working prototype (please public keep away) version of what could be a GOAL loader using simdag
Martin Quinson [Wed, 19 Oct 2011 19:43:59 +0000 (21:43 +0200)]
typo--
Navarrop [Mon, 17 Oct 2011 13:59:15 +0000 (15:59 +0200)]
Add example to kill a process.