#include "../simix/smx_private.h"
#include "xbt/fifo.h"
#include "mc_private.h"
-#include "xbt/automaton/automaton_create.h"
+#include "xbt/automaton.h"
XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
+/* Configuration support */
+e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
+
+void _mc_cfg_cb_reduce(const char *name, int pos) {
+ char *val= xbt_cfg_get_string(_surf_cfg_set, name);
+ if (!strcasecmp(val,"none")) {
+ mc_reduce_kind = e_mc_reduce_none;
+ } else if (!strcasecmp(val,"dpor")) {
+ mc_reduce_kind = e_mc_reduce_dpor;
+ } else {
+ xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
+ }
+ xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+void _mc_cfg_cb_checkpoint(const char *name, int pos) {
+ _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
+ xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+void _mc_cfg_cb_property(const char *name, int pos) {
+ _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
+ xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+}
+
+
/* MC global data structures */
mc_state_t mc_current_state = NULL;
xbt_fifo_t mc_stack_liveness = NULL;
mc_snapshot_t initial_snapshot_liveness = NULL;
-xbt_automaton_t automaton;
+xbt_automaton_t _mc_property_automaton = NULL;
-static void MC_init_liveness(xbt_automaton_t a);
static void MC_assert_pair(int prop);
+void MC_do_the_modelcheck_for_real() {
+ if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
+ if (mc_reduce_kind==e_mc_reduce_unset)
+ mc_reduce_kind=e_mc_reduce_dpor;
+
+ XBT_INFO("Check a safety property");
+ MC_modelcheck();
+
+ } else {
+
+ if (mc_reduce_kind==e_mc_reduce_unset)
+ mc_reduce_kind=e_mc_reduce_none;
+
+ XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
+ MC_automaton_load(_surf_mc_property_file);
+ MC_modelcheck_liveness();
+ }
+}
/**
* \brief Initialize the model-checker data structures
}
-static void MC_init_liveness(xbt_automaton_t a){
+void MC_modelcheck(void)
+{
+ MC_init_safety();
+ MC_dpor();
+ MC_exit();
+}
+void MC_modelcheck_liveness(){
+ /* init stuff */
XBT_DEBUG("Start init mc");
mc_time = xbt_new0(double, simix_process_maxpid);
MC_UNSET_RAW_MEM;
- automaton = a;
MC_ddfs_init();
-
-}
-
-
-void MC_modelcheck(void)
-{
- MC_init_safety();
- MC_dpor();
- MC_exit();
-}
-
-
-
-void MC_modelcheck_liveness(xbt_automaton_t a){
- MC_init_liveness(a);
- MC_exit_liveness();
-}
-
-void MC_exit_liveness(void)
-{
+ /* We're done */
MC_print_statistics_pairs(mc_stats_pair);
//xbt_free(mc_time);
//MC_memory_exit();
MC_show_stack_safety(stack);
- if(!_surf_do_mc_checkpoint){
+ if(!_surf_mc_checkpoint){
mc_state_t state;
}
-xbt_automaton_t MC_create_automaton(const char *file){
+void MC_automaton_load(const char *file){
+ MC_SET_RAW_MEM;
+
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_automaton_load(_mc_property_automaton,file);
+
+ MC_UNSET_RAW_MEM;
+}
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
MC_SET_RAW_MEM;
- xbt_automaton_t a = xbt_create_automaton(file);
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+ xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
MC_UNSET_RAW_MEM;
- return a;
}