Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' into MC_LTL
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 5 Dec 2011 10:16:17 +0000 (11:16 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 5 Dec 2011 10:16:17 +0000 (11:16 +0100)
1  2 
src/include/mc/mc.h
src/mc/private.h

diff --combined src/include/mc/mc.h
@@@ -1,5 -1,3 +1,3 @@@
- /*    $Id: simix.h 5497 2008-05-26 12:19:15Z cristianrosa $    */
  /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
     All rights reserved.                                          */
  
@@@ -16,7 -14,6 +14,7 @@@
  #include "mc/datatypes.h"
  #include "simix/datatypes.h"
  #include "gras_config.h" /* Definition of HAVE_MC */
 +#include "xbt/automaton.h"
  
  #ifdef HAVE_MC
  extern int _surf_do_model_check;
  SG_BEGIN_DECL()
  
  /********************************* Global *************************************/
 -XBT_PUBLIC(void) MC_init(void);
 +XBT_PUBLIC(void) MC_init_safety_stateless(void);
 +XBT_PUBLIC(void) MC_init_safety_stateful(void);
 +XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a);
 +XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a, char *prgm);
  XBT_PUBLIC(void) MC_exit(void);
 +XBT_PUBLIC(void) MC_exit_liveness(void);
  XBT_PUBLIC(void) MC_assert(int);
 +XBT_PUBLIC(void) MC_assert_stateful(int);
 +XBT_PUBLIC(void) MC_assert_pair_stateful(int);
 +XBT_PUBLIC(void) MC_assert_pair_stateless(int);
  XBT_PUBLIC(void) MC_modelcheck(void);
 +XBT_PUBLIC(void) MC_modelcheck_stateful(void);
 +XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a);
 +XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm);
  XBT_PUBLIC(int) MC_random(int, int);
  XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
  XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
diff --combined src/mc/private.h
@@@ -1,5 -1,3 +1,3 @@@
- /*    $Id: private.h 5497 2008-05-26 12:19:15Z cristianrosa $  */
  /* Copyright (c) 2007 Arnaud Legrand, Bruno Donnassolo.
     All rights reserved.                                          */
  
  #include "xbt/function_types.h"
  #include "xbt/mmalloc.h"
  #include "../simix/private.h"
 +#include "xbt/automaton.h"
 +#include "xbt/hash.h"
  
  /****************************** Snapshots ***********************************/
  
  typedef struct s_mc_mem_region{
 +  int type;
    void *start_addr;
    void *data;
    size_t size;
@@@ -35,11 -30,7 +33,11 @@@ typedef struct s_mc_snapshot
    mc_mem_region_t *regions;
  } s_mc_snapshot_t, *mc_snapshot_t;
  
 +extern char *prog_name;
 +
  void MC_take_snapshot(mc_snapshot_t);
 +void MC_take_snapshot_liveness(mc_snapshot_t s);
 +void MC_take_snapshot_to_restore_liveness(mc_snapshot_t s);
  void MC_restore_snapshot(mc_snapshot_t);
  void MC_free_snapshot(mc_snapshot_t);
  
@@@ -48,19 -39,14 +46,19 @@@ extern double *mc_time
  
  /* Bound of the MC depth-first search algorithm */
  #define MAX_DEPTH 1000
 +#define MAX_DEPTH_LIVENESS 50
  
  int MC_deadlock_check(void);
  void MC_replay(xbt_fifo_t stack);
 +void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
  void MC_wait_for_requests(void);
  void MC_get_enabled_processes();
  void MC_show_deadlock(smx_req_t req);
 -void MC_show_stack(xbt_fifo_t stack);
 -void MC_dump_stack(xbt_fifo_t stack);
 +void MC_show_deadlock_stateful(smx_req_t req);
 +void MC_show_stack_safety_stateless(xbt_fifo_t stack);
 +void MC_dump_stack_safety_stateless(xbt_fifo_t stack);
 +void MC_show_stack_safety_stateful(xbt_fifo_t stack);
 +void MC_dump_stack_safety_stateful(xbt_fifo_t stack);
  
  /********************************* Requests ***********************************/
  int MC_request_depend(smx_req_t req1, smx_req_t req2);
@@@ -72,6 -58,10 +70,6 @@@ int MC_request_is_enabled(smx_req_t req
  int MC_request_is_enabled_by_idx(smx_req_t req, unsigned int idx);
  int MC_process_is_enabled(smx_process_t process);
  
 -/********************************** DPOR **************************************/
 -void MC_dpor_init(void);
 -void MC_dpor(void);
 -void MC_dpor_exit(void);
  
  /******************************** States **************************************/
  /* Possible exploration status of a process in a state */
@@@ -99,7 -89,7 +97,7 @@@ typedef struct mc_state 
                                         multi-request like waitany ) */
  } s_mc_state_t, *mc_state_t;
  
 -extern xbt_fifo_t mc_stack;
 +extern xbt_fifo_t mc_stack_safety_stateless;
  
  mc_state_t MC_state_new(void);
  void MC_state_delete(mc_state_t state);
@@@ -119,18 -109,9 +117,18 @@@ typedef struct mc_stats 
    unsigned long executed_transitions;
  } s_mc_stats_t, *mc_stats_t;
  
 +typedef struct mc_stats_pair {
 +  //unsigned long pair_size;
 +  unsigned long visited_pairs;
 +  unsigned long expanded_pairs;
 +  unsigned long executed_transitions;
 +} s_mc_stats_pair_t, *mc_stats_pair_t;
 +
  extern mc_stats_t mc_stats;
 +extern mc_stats_pair_t mc_stats_pair;
  
  void MC_print_statistics(mc_stats_t);
 +void MC_print_statistics_pairs(mc_stats_pair_t);
  
  /********************************** MEMORY ******************************/
  /* The possible memory modes for the modelchecker are standard and raw. */
@@@ -186,98 -167,4 +184,98 @@@ typedef struct s_memory_map 
  memory_map_t get_memory_map(void);
  
  
 +/********************************** DPOR for safety (stateless) **************************************/
 +void MC_dpor_init(void);
 +void MC_dpor(void);
 +void MC_dpor_exit(void);
 +
 +/***** DPOR for safety (stateful) **** */
 +
 +typedef struct s_mc_state_with_snapshot{
 +  mc_snapshot_t system_state;
 +  mc_state_t graph_state;
 +}s_mc_state_ws_t, *mc_state_ws_t;
 +
 +extern xbt_fifo_t mc_stack_safety_stateful;
 +
 +void MC_init_stateful(void);
 +void MC_modelcheck_stateful(void);
 +mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
 +void MC_dpor_stateful_init(void);
 +void MC_dpor_stateful(void);
 +void MC_exit_stateful(void);
 +
 +
 +/********************************** Double-DFS for liveness property**************************************/
 +
 +typedef struct s_mc_pair{
 +  mc_snapshot_t system_state;
 +  mc_state_t graph_state;
 +  xbt_state_t automaton_state;
 +}s_mc_pair_t, *mc_pair_t;
 +
 +typedef struct s_mc_pair_reached{
 +  xbt_state_t automaton_state;
 +  xbt_dynar_t prop_ato;
 +  mc_snapshot_t system_state;
 +}s_mc_pair_reached_t, *mc_pair_reached_t;
 +
 +typedef struct s_mc_pair_visited{
 +  xbt_state_t automaton_state;
 +  xbt_dynar_t prop_ato;
 +  mc_snapshot_t system_state;
 +  int search_cycle;
 +}s_mc_pair_visited_t, *mc_pair_visited_t;
 +
 +typedef struct s_mc_pair_visited_hash{
 +  xbt_state_t automaton_state;
 +  xbt_dynar_t prop_ato;
 +  xbt_dict_t hash_regions;
 +  int search_cycle;
 +}s_mc_pair_visited_hash_t, *mc_pair_visited_hash_t;
 +
 +int MC_automaton_evaluate_label(xbt_exp_label_t l);
 +mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
 +
 +int reached(xbt_state_t st);
 +void set_pair_reached(xbt_state_t st);
 +int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
 +void MC_show_stack_liveness_stateful(xbt_fifo_t stack);
 +void MC_dump_stack_liveness_stateful(xbt_fifo_t stack);
 +void MC_pair_delete(mc_pair_t pair);
 +void MC_exit_liveness(void);
 +mc_state_t MC_state_pair_new(void);
 +int visited(xbt_state_t st, int search_cycle);
 +void set_pair_visited(xbt_state_t st, int search_cycle);
 +int visited_hash(xbt_state_t st, int search_cycle);
 +void set_pair_visited_hash(xbt_state_t st, int search_cycle);
 +
 +/* **** Double-DFS stateful without visited state **** */
 +
 +extern xbt_fifo_t mc_stack_liveness_stateful;
 +
 +void MC_ddfs_stateful_init(xbt_automaton_t a);
 +void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore);
 +
 +/* **** Double-DFS stateless **** */
 +
 +typedef struct s_mc_pair_stateless{
 +  mc_state_t graph_state;
 +  xbt_state_t automaton_state;
 +  int requests;
 +}s_mc_pair_stateless_t, *mc_pair_stateless_t;
 +
 +extern xbt_fifo_t mc_stack_liveness_stateless;
 +extern mc_snapshot_t initial_snapshot_liveness;
 +extern xbt_automaton_t automaton;
 +
 +mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);
 +void MC_ddfs_stateless_init();
 +void MC_ddfs_stateless(int search_cycle);
 +void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
 +void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
 +void MC_pair_stateless_delete(mc_pair_stateless_t pair);
 +
 +
 +
  #endif