- init();
- yyparse();
- automaton = get_automaton();
- xbt_new_propositional_symbol(automaton,"pready", &predPready);
- xbt_new_propositional_symbol(automaton,"cready", &predCready);
- xbt_new_propositional_symbol(automaton,"consume", &predConsume);
- xbt_new_propositional_symbol(automaton,"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);