- xbt_automaton_t a = MC_create_automaton("promela2_bugged2_liveness");
- xbt_new_propositional_symbol(a,"pready", &predPready);
- xbt_new_propositional_symbol(a,"cready", &predCready);
- xbt_new_propositional_symbol(a,"consume", &predConsume);
- xbt_new_propositional_symbol(a,"produce", &predProduce);
+ MSG_init(&argc, argv);
+
+ MSG_config("model-check/property","promela2_bugged2_liveness");
+ MC_automaton_new_propositional_symbol("pready", &predPready);
+ MC_automaton_new_propositional_symbol("cready", &predCready);
+ MC_automaton_new_propositional_symbol("consume", &predConsume);
+ MC_automaton_new_propositional_symbol("produce", &predProduce);