VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
{
simgrid::mc::Process* process = &(mc_model_checker->process());
VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
{
simgrid::mc::Process* process = &(mc_model_checker->process());
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
if (pair->search_cycle == 1)
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
if (pair->search_cycle == 1)
new_pair->atomic_propositions.get()) == 0) {
if (this->compare(pair_test.get(), new_pair.get()) == 0) {
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
new_pair->atomic_propositions.get()) == 0) {
if (this->compare(pair_test.get(), new_pair.get()) == 0) {
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
return nullptr;
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
return nullptr;
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
initial_pair->search_cycle = 0;
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
initial_pair->search_cycle = 0;
simgrid::mc::restore_snapshot(initial_global_state->snapshot);
/* Traverse the stack from the initial state and re-execute the transitions */
simgrid::mc::restore_snapshot(initial_global_state->snapshot);
/* Traverse the stack from the initial state and re-execute the transitions */
pair->num, pair->automaton_state, pair->atomic_propositions.get(),
pair->graph_state);
pair->num, pair->automaton_state, pair->atomic_propositions.get(),
pair->graph_state);
visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
std::vector<std::string> LivenessChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
std::vector<std::string> LivenessChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
simgrid::xbt::unique_ptr<s_xbt_dynar_t> prop_values;
std::shared_ptr<VisitedPair> reached_pair = nullptr;
simgrid::xbt::unique_ptr<s_xbt_dynar_t> prop_values;
std::shared_ptr<VisitedPair> reached_pair = nullptr;
/* Update current state in buchi automaton */
simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
/* Update current state in buchi automaton */
simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
/* Traverse the stack backwards until a pair with a non empty interleave
set is found, deleting all the pairs that have it empty in the way. */
/* Traverse the stack backwards until a pair with a non empty interleave
set is found, deleting all the pairs that have it empty in the way. */
- while (!liveness_stack.empty()) {
- current_pair = liveness_stack.back();
- liveness_stack.pop_back();
+ while (!livenessStack_.empty()) {
+ current_pair = livenessStack_.back();
+ livenessStack_.pop_back();
if (current_pair->requests > 0) {
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
if (current_pair->requests > 0) {
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
/* 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());