} else {
if(strcmp(req, "2") == 0){
XBT_INFO("CS idle. Grant immediatly");
+ MC_compare();
answer = MSG_task_create("grant", 0, 1000, NULL);
MSG_task_send(answer, req);
CS_used = 1;
/********************************* Snapshot comparison test *************************************/
void MC_test_snapshot_comparison(void);
+void MC_compare(void);
+
SG_END_DECL()
#endif /* _MC_MC_H */
mc_stats_pair_t mc_stats_pair = NULL;
xbt_fifo_t mc_stack_liveness = NULL;
mc_snapshot_t initial_snapshot_liveness = NULL;
+int compare;
xbt_automaton_t _mc_property_automaton = NULL;
}
+void MC_compare(void){
+ compare = 1;
+}
+
void MC_modelcheck(void)
{
mc_time = xbt_new0(double, simix_process_maxpid);
+ compare = 0;
+
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- if(xbt_dynar_is_empty(reached_pairs)){
+ if(xbt_dynar_is_empty(reached_pairs) || !compare){
return 0;
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
+
+ compare = 0;
return 0;
extern mc_snapshot_t initial_snapshot_liveness;
extern xbt_automaton_t _mc_property_automaton;
+extern int compare;
typedef struct s_mc_pair{
mc_snapshot_t system_state;