XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
"Logging specific to algorithms for liveness properties verification");
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);
}
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);
}
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);
}
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);
}
int res = MC_automaton_evaluate_label(
l->u.exp_not, atomic_propositions_values);
return (!res);
}
int res = MC_automaton_evaluate_label(
l->u.exp_not, atomic_propositions_values);
return (!res);
}
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t p = nullptr;
xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t p = nullptr;
xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = res.first; i != res.second; ++i) {
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
for (auto i = res.first; i != res.second; ++i) {
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
MC_state_interleave_process(initial_pair->graph_state.get(), &p.copy);
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
MC_state_interleave_process(initial_pair->graph_state.get(), &p.copy);
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
/* If new acceptance pair, return new pair */
if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
this->showAcceptanceCycle(current_pair->depth);
/* If new acceptance pair, return new pair */
if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
this->showAcceptanceCycle(current_pair->depth);
&& (visited_num = this->insertVisitedPair(
reached_pair, current_pair)) != -1) {
&& (visited_num = this->insertVisitedPair(
reached_pair, current_pair)) != -1) {
/* Get values of atomic propositions (variables used in the property formula) */
std::vector<int> prop_values = this->getPropositionValues();
/* Get values of atomic propositions (variables used in the property formula) */
std::vector<int> prop_values = this->getPropositionValues();
/* FIXME : get search_cycle value for each acceptant state */
if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
/* FIXME : get search_cycle value for each acceptant state */
if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
/* Create the initial state */
simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
/* Create the initial state */
simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());