1 /* simgrid/modelchecker.h - Formal Verification made possible in SimGrid */
3 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
5 /* This program is free software; you can redistribute it and/or modify it
6 * under the terms of the license (GNU LGPL) which comes with this package. */
8 #ifndef SIMGRID_MODELCHECKER_H
9 #define SIMGRID_MODELCHECKER_H
11 #include <stddef.h> /* size_t */
16 /** Explore every branches where that function returns a value between min and max (inclusive) */
17 XBT_PUBLIC int MC_random(int min, int max);
19 /** Assertion for the model-checker: Defines a safety property to verify */
20 XBT_PUBLIC void MC_assert(int);
22 /** Check whether the model-checker is currently active, ie if this process was started with simgrid-mc.
23 * It is off in simulation or when replaying MC traces (see MC_record_replay_is_active()) */
24 XBT_PUBLIC int MC_is_active();
28 #endif /* SIMGRID_MODELCHECKER_H */