-#include "automaton.h"
+#include "xbt/automaton.h"
xbt_automaton_t xbt_automaton_new_automaton(){
xbt_automaton_t automaton = NULL;
xbt_dynar_push(a->propositional_symbols, &prop_symb);
return prop_symb;
}
+
+int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
+
+ /* single id for each state, id and type sufficient for comparison*/
+
+ if(strcmp(s1->id, s2->id))
+ return 1;
+
+ if(s1->type != s2->type)
+ return 1;
+
+ return 0;
+
+}
+
+int automaton_transition_compare(const void *t1, const void *t2){
+
+ if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
+ return 1;
+
+ if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
+ return 1;
+
+ if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
+ return 1;
+
+ return 0;
+
+}
+
+int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
+
+ if(l1->type != l2->type)
+ return 1;
+
+ switch(l1->type){
+
+ case 0 : // OR
+ case 1 : // AND
+ if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
+ return 1;
+ else
+ return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
+ break;
+
+ case 2 : // NOT
+ return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
+ break;
+
+ case 3 : // predicat
+ return (strcmp(l1->u.predicat, l2->u.predicat));
+ break;
+
+ case 4 : // 1
+ return 0;
+ break;
+
+ default :
+ return -1;
+ break;
+
+ }
+
+}
+
+
+int propositional_symbols_compare_value(const void *s1, const void *s2){
+
+ return (!((int)s1 == (int)s2));
+
+}
typedef struct xbt_exp_label* xbt_exp_label_t;
+
typedef struct xbt_transition {
xbt_state_t src;
xbt_state_t dst;
xbt_exp_label_t label;
} s_xbt_transition;
-
typedef struct xbt_transition* xbt_transition_t;
+
typedef struct xbt_propositional_symbol{
char* pred;
void* function;
XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
+XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
+
+XBT_PUBLIC(int) propositional_symbols_compare_value(const void *s1, const void *s2);
+
+XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
+
+XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
+
+
SG_END_DECL()
#endif
-#include "automatonparse_promela.h"
+#include "xbt/automatonparse_promela.h"
char* state_id_src;
char* id_state = strdup(id);
char* first_part = strtok(id,"_");
- int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final, 2=état initial/final
+ int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final
if(strcmp(first_part,"accept")==0){
- char* second_part = strtok(NULL,"_");
- if(strcmp(second_part,"init")==0){
- type = 2;
- }else{
- type = 1;
- }
-
+ type = 1;
}else{
char* second_part = strtok(NULL,"_");
if(strcmp(second_part,"init")==0){
state = xbt_automaton_new_state(automaton, type, id_state);
}
- if(type==-1 || type==2)
+ if(type==-1)
automaton->current_state = state;
if(src)
return automaton;
}
-void display_automaton(){
- xbt_automaton_display(automaton);
-}
XBT_PUBLIC(xbt_exp_label_t) new_label(int type, ...);
XBT_PUBLIC(xbt_automaton_t) get_automaton(void);
-
+
XBT_PUBLIC(void) display_automaton(void);
SG_END_DECL()
#include <stdlib.h>
#include <string.h>
-#include "xbt/dynar.h"
-#include "xbt/sysdep.h"
-#include "xbt/graph.h"
+#include <xbt/dynar.h>
+#include <xbt/sysdep.h>
+#include <xbt/graph.h>
SG_BEGIN_DECL()
int type; /* -1 = init, 0 = inter, 1 = final */
xbt_dynar_t in;
xbt_dynar_t out;
- int visited;
} s_xbt_state;
typedef struct xbt_state* xbt_state_t;
typedef struct xbt_exp_label* xbt_exp_label_t;
+
typedef struct xbt_transition {
xbt_state_t src;
xbt_state_t dst;
xbt_exp_label_t label;
} s_xbt_transition;
-
typedef struct xbt_transition* xbt_transition_t;
+
typedef struct xbt_propositional_symbol{
char* pred;
void* function;
XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
+XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
+
+XBT_PUBLIC(int) propositional_symbols_compare_value(const void *s1, const void *s2);
+
+XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
+
+XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
+
+
SG_END_DECL()
#endif
}
+int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
+
+ if(s1->num_reg != s2->num_reg)
+ return 1;
+
+ int i;
+ for(i=0 ; i< s1->num_reg ; i++){
+
+ if(s1->regions[i]->size != s2->regions[i]->size)
+ return 1;
+
+ if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
+ return 1;
+
+ if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0)
+ return 1;
+
+ }
+
+ return 0;
+
+}
+
int reached(xbt_automaton_t a){
if(xbt_dynar_is_empty(reached_pairs)){
pair = xbt_new0(s_mc_pair_reached_t, 1);
pair->automaton_state = a->current_state;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(pair->system_state);
/* Get values of propositional symbols */
unsigned int cursor = 0;
cursor = 0;
mc_pair_reached_t pair_test;
- //int size = xbt_dynar_length(pair->prop_ato);
- //int i, d1, d2;
xbt_dynar_foreach(reached_pairs, cursor, pair_test){
- /*if(memcmp(pair_test->automaton_state, pair->automaton_state, sizeof(xbt_state_t)) == 0){
- for(i=0; i< size; i++){
- d1 = xbt_dynar_get_as(pair->prop_ato, i, int);
- d2 = xbt_dynar_get_as(pair_test->prop_ato, i, int);
- if(d1 == d2){
+ if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
+ //XBT_DEBUG("Same automaton state");
+ if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
+ //XBT_DEBUG("Same values of propositional symbols");
+ if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
+ //XBT_DEBUG("Same system state");
MC_UNSET_RAW_MEM;
return 1;
}
}
- }*/
-
- if(memcmp(pair_test, pair, sizeof(mc_pair_reached_t)) == 0){
- MC_UNSET_RAW_MEM;
- return 1;
}
}
pair = xbt_new0(s_mc_pair_reached_t, 1);
pair->automaton_state = a->current_state;
pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(pair->system_state);
/* Get values of propositional symbols */
unsigned int cursor = 0;
MC_UNSET_RAW_MEM;
-
-
+
cursor= 0;
xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
MC_UNSET_RAW_MEM;
}
- cursor = 0;
-
-
+ cursor = 0;
xbt_dynar_foreach(successors, cursor, pair_succ){
#include "private.h"
#include <stdlib.h>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
+ "Logging specific to algorithms for memory_map");
+
memory_map_t get_memory_map(void)
{
FILE *fp; /* File pointer to process's proc maps file */
xbt_assert(fp,
"Cannot open /proc/self/maps to investigate the memory map of the process. Please report this bug.");
+ //XBT_DEBUG("/proc/self/maps");
+
ret = xbt_new0(s_memory_map_t, 1);
/* Read one line at the time, parse it and add it to the memory map to be returned */
while ((read = getline(&line, &n, fp)) != -1) {
+ //XBT_DEBUG("%s", line);
+
/* Wipeout the new line character */
line[read - 1] = '\0';
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;
extern xbt_fifo_t mc_stack_liveness_stateful;
int reached(xbt_automaton_t a);
int set_pair_reached(xbt_automaton_t a);
+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);
#include "xbt/automaton.h"
-#include "xbt/dynar.h"
xbt_automaton_t xbt_automaton_new_automaton(){
xbt_automaton_t automaton = NULL;
xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
xbt_state_t state = NULL;
state = xbt_new0(struct xbt_state, 1);
- state->visited = 0;
state->type = type;
state->id = strdup(id);
state->in = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
xbt_dynar_push(a->propositional_symbols, &prop_symb);
return prop_symb;
}
+
+int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
+
+ /* single id for each state, id and type sufficient for comparison*/
+
+ if(strcmp(s1->id, s2->id))
+ return 1;
+
+ if(s1->type != s2->type)
+ return 1;
+
+ return 0;
+
+}
+
+int automaton_transition_compare(const void *t1, const void *t2){
+
+ if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
+ return 1;
+
+ if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
+ return 1;
+
+ if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
+ return 1;
+
+ return 0;
+
+}
+
+int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
+
+ if(l1->type != l2->type)
+ return 1;
+
+ switch(l1->type){
+
+ case 0 : // OR
+ case 1 : // AND
+ if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
+ return 1;
+ else
+ return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
+ break;
+
+ case 2 : // NOT
+ return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
+ break;
+
+ case 3 : // predicat
+ return (strcmp(l1->u.predicat, l2->u.predicat));
+ break;
+
+ case 4 : // 1
+ return 0;
+ break;
+
+ default :
+ return -1;
+ break;
+
+ }
+
+}
+
+
+int propositional_symbols_compare_value(const void *s1, const void *s2){
+
+ return (!((int)s1 == (int)s2));
+
+}
