-
- /* Fork an mc's slave exploration process and wait for it. */
- /* The forked process will explore a trace until:
- - a back-tracking point is found (it sets mc_expl_ctl to MC_explore)
- - there are no more states to explore (it sets mc_expl_ctl to MC_STOP)
- - a property is invalid (or dead-lock)
- */
- while(*mc_exp_ctl == MC_EXPLORE){
- if((pid = fork())){
- waitpid(pid, &status, 0);
- mmalloc_detach(raw_heap);
- raw_heap = mmalloc_attach(raw_heap_fd, (char*)(std_heap) + STD_HEAP_SIZE + getpagesize());
-
- if (WIFSIGNALED(status)) {
- INFO1("killed by signal %d\n", WTERMSIG(status));
- break;
- }else if (WIFSTOPPED(status)) {
- INFO1("stopped by signal %d\n", WSTOPSIG(status));
- break;
- }else if (WIFCONTINUED(status)) {
- INFO0("continued\n");
- break;
- }
-
- if(*mc_exp_ctl == MC_DEADLOCK){
- INFO0("**************************");
- INFO0("*** DEAD-LOCK DETECTED ***");
- INFO0("**************************");
- MC_dump_stack(mc_stack);
- MC_print_statistics(mc_stats);
- break;
- }
-
- }else{
- /* if mc_stack is empty then create first state, otherwise replay */
- if(xbt_fifo_size(mc_stack) == 0)
- MC_dpor_init();
- else
- MC_replay(mc_stack);
-
- MC_dpor();
- MC_memory_exit();
- break;
- }
- }
-
- /* If we are the mc's master process then exit */
- if(pid)
- MC_exit();
+ MC_dpor();
+ MC_exit();
+}
+
+void MC_modelcheck_with_automaton(xbt_automaton_t a){
+ MC_init_with_automaton(a);
+ MC_exit_with_automaton();
+}
+
+void MC_exit_with_automaton(void)
+{
+ MC_print_statistics_pairs(mc_stats_pair);
+ xbt_free(mc_time);
+ MC_memory_exit();