bool handle_events();
void wait_client(simgrid::mc::Process& process);
void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value);
+ void wait_for_requests()
+ {
+ mc_model_checker->wait_client(mc_model_checker->process());
+ }
private:
void setup_ignore();
bool handle_message(char* buffer, ssize_t size);
void MC_wait_for_requests(void)
{
-#ifdef HAVE_MC
- if (mc_mode == MC_MODE_SERVER) {
- mc_model_checker->wait_client(mc_model_checker->process());
- return;
- }
-#endif
+ assert(mc_mode != MC_MODE_SERVER);
smx_process_t process;
smx_simcall_t req;
XBT_DEBUG("********* Start communication determinism verification *********");
/* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Get an enabled process and insert it in the interleave set of the initial state */
MC_EACH_SIMIX_PROCESS(process,
MC_handle_comm_pattern(call, req, value, NULL, 0);
/* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Create the new expanded state */
next_state = MC_state_new();
{
XBT_INFO("Check communication determinism");
mc_reduce_kind = e_mc_reduce_none;
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
if (mc_mode == MC_MODE_CLIENT) {
// This will move somehwere else:
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, NULL, 1);
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
count++;
}
}
MC_simcall_handle(req, value);
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
}
/* Update statistics */
mc_pair_t initial_pair = NULL;
smx_process_t process;
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
if(_sg_mc_visited > 0)
MC_simcall_handle(req, value);
/* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
current_pair->requests--;
current_pair->exploration_started = 1;
mc_reduce_kind = e_mc_reduce_none;
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the liveness algorithm");
_sg_mc_liveness = 1;
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Get an enabled process and insert it in the interleave set of the initial state */
smx_process_t process;
/* Answer the request */
MC_simcall_handle(req, value);
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Create the new expanded state */
next_state = MC_state_new();
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the safety algorithm");