modelchecker.h File Reference

This is the API used by the user simulated program to communicate with the MC. More...

#include <stdbool.h>
#include <simgrid_config.h>
#include <xbt/base.h>

Macros
#define	MC_is_active()   0
#define	MC_visited_reduction()   0
#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_cut()   ((void)0)
#define	MC_ignore(a, b)   ((void)0)

Functions
int	MC_random (int min, int max)

Detailed Description

This is the API used by the user simulated program to communicate with the MC.

Macro Definition Documentation

MC_is_active

#define MC_is_active

(

)

0

Examples:

examples/msg/dht-chord/dht-chord.c.

MC_visited_reduction

#define MC_visited_reduction

(

)

0

Examples:

examples/msg/dht-chord/dht-chord.c.

MC_assert

#define MC_assert

(

a

)

xbt_assert(a)

MC_automaton_new_propositional_symbol

#define MC_automaton_new_propositional_symbol	(		a,
			b
	)		((void)0)

MC_automaton_new_propositional_symbol_pointer

#define MC_automaton_new_propositional_symbol_pointer	(		a,
			b
	)		((void)0)

MC_cut

#define MC_cut

(

)

((void)0)

Examples:

examples/msg/dht-chord/dht-chord.c.

MC_ignore

#define MC_ignore	(		a,
			b
	)		((void)0)

Function Documentation

MC_random()

int MC_random	(	int	min,
		int	max
	)

Examples:

examples/msg/dht-chord/dht-chord.c.