int r=0;
int cs=0;
-int predR(){
- return r;
-}
-
-int predCS(){
- return cs;
-}
-
#ifdef GARBAGE_STACK
/** Do not use a clean stack */
static void garbage_stack(void) {
char **options = &argv[1];
MSG_config("model-check/property","promela_bugged1_liveness");
- MC_automaton_new_propositional_symbol("r", &predR);
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MC_automaton_new_propositional_symbol_pointer("r", &r);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
const char* platform_file = options[0];
const char* application_file = options[1];
int cs = 0;
-int predCS(){
- return cs;
-}
-
-
int coordinator(int argc, char **argv);
int client(int argc, char **argv);
MSG_init(&argc, argv);
MSG_config("model-check/property","promela_bugged2_liveness");
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
MSG_create_environment("../msg_platform.xml");
MSG_function_register("coordinator", coordinator);
int r, cs;
-static int predR(){
- return r;
-}
-
-static int predCS(){
- return cs;
-}
-
-
int main(int argc, char **argv){
int err, size, rank;
exit(1);
}
- MC_automaton_new_propositional_symbol("r", &predR);
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MC_automaton_new_propositional_symbol_pointer("r", &r);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
MC_ignore(&(status.count), sizeof(status.count));
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void));
+XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_pointer(const char *id, int* value);
XBT_PUBLIC(void *) MC_snapshot(void);
XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
XBT_PUBLIC(void) MC_cut(void);
#define MC_assert(a) xbt_assert(a)
#define MC_automaton_new_propositional_symbol(a, b) ((void)0)
+#define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
#define MC_snapshot() ((void*)0)
#define MC_compare_snapshots(a, b) 0
#define MC_cut() ((void)0)
XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, int(*fct)(void));
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value);
+
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
+ xbt_automaton_t a, const char* id,
+ int(*callback)(void*), void* data, void (*free_function)(void*));
+
XBT_PUBLIC(int) xbt_automaton_propositional_symbol_evaluate(xbt_automaton_propositional_symbol_t symbol);
char* xbt_automaton_propositional_symbol_get_name(xbt_automaton_propositional_symbol_t symbol);
mmalloc_set_current_heap(heap);
}
+void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value)
+{
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
+ mmalloc_set_current_heap(heap);
+}
+
void MC_dump_stacks(FILE* file)
{
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
return prop_symb;
}
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_pointer(xbt_automaton_t a, const char* id, int* value)
+{
+ xbt_automaton_propositional_symbol_t prop_symb = NULL;
+ prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
+ prop_symb->pred = strdup(id);
+ prop_symb->function = NULL;
+ prop_symb->data = value;
+ prop_symb->free_function = NULL;
+ xbt_dynar_push(a->propositional_symbols, &prop_symb);
+ return prop_symb;
+}
+
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new_callback(
+ xbt_automaton_t a, const char* id,
+ int(*callback)(void*), void* data, void (*free_function)(void*))
+{
+ xbt_automaton_propositional_symbol_t prop_symb = NULL;
+ prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);
+ prop_symb->pred = strdup(id);
+ prop_symb->function = callback;
+ prop_symb->data = data;
+ prop_symb->free_function = free_function;
+ xbt_dynar_push(a->propositional_symbols, &prop_symb);
+ return prop_symb;
+}
+
int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){
/* single id for each state, id and type sufficient for comparison*/