-
-static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
- xbt_dynar_t atomic_propositions_values)
-{
-
- switch (l->type) {
- case 0:{
- int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
- int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
- return (left_res || right_res);
- }
- case 1:{
- int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
- int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
- return (left_res && right_res);
- }
- case 2:{
- int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
- return (!res);
- }
- case 3:{
- unsigned int cursor = 0;
- xbt_automaton_propositional_symbol_t p = nullptr;
- xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
- if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
- return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
- }
- return -1;
- }
- case 4:
- return 2;
- default:
- return -1;
- }
-}
-
-static void MC_pre_modelcheck_liveness(void)