#include <xbt/sysdep.h>
#include "src/mc/mc_request.h"
-#include "src/mc/mc_liveness.h"
+#include "src/mc/LivenessChecker.hpp"
#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_smx.h"
namespace simgrid {
namespace mc {
+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 xbt_dynar_t visited_pairs;
Pair::Pair() : num(++mc_stats->expanded_pairs),
MC_state_delete(this->graph_state, 1);
}
-static void show_stack_liveness(xbt_fifo_t stack)
+void LivenessChecker::showStack(xbt_fifo_t stack)
{
int value;
simgrid::mc::Pair* pair;
}
}
-static void dump_stack_liveness(xbt_fifo_t stack)
+void LivenessChecker::dumpStack(xbt_fifo_t stack)
{
simgrid::mc::Pair* pair;
while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
delete pair;
}
-static simgrid::xbt::unique_ptr<s_xbt_dynar_t> get_atomic_propositions_values()
+simgrid::xbt::unique_ptr<s_xbt_dynar_t> LivenessChecker::getPropositionValues()
{
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t ps = nullptr;
return std::move(values);
}
-static int snapshot_compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
+int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
{
simgrid::mc::Snapshot* s1 = state1->graph_state->system_state;
simgrid::mc::Snapshot* s2 = state2->graph_state->system_state;
int num1 = state1->num;
int num2 = state2->num;
- return snapshot_compare(num1, s1, num2, s2);
+ return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
}
-static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair)
+simgrid::mc::VisitedPair* LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
{
auto acceptance_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(::acceptance_pairs);
auto new_pair =
if (xbt_automaton_propositional_symbols_compare_value(
pair_test->atomic_propositions.get(),
new_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_pair.get()) == 0) {
+ if (this->compare(pair_test, new_pair.get()) == 0) {
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
xbt_fifo_shift(mc_stack);
if (dot_output != nullptr)
return new_raw_pair;
}
-static void remove_acceptance_pair(int pair_num)
+void LivenessChecker::removeAcceptancePair(int pair_num)
{
unsigned int cursor = 0;
simgrid::mc::VisitedPair* pair_test = nullptr;
}
}
-
-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)
+void LivenessChecker::prepare(void)
{
simgrid::mc::Pair* initial_pair = nullptr;
mc_model_checker->wait_for_requests();
unsigned int cursor = 0;
xbt_automaton_state_t automaton_state;
-
+
xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) {
if (automaton_state->type == -1) { /* Initial automaton state */
initial_pair = new Pair();
initial_pair->automaton_state = automaton_state;
initial_pair->graph_state = MC_state_new();
- initial_pair->atomic_propositions = get_atomic_propositions_values();
+ initial_pair->atomic_propositions = this->getPropositionValues();
initial_pair->depth = 1;
/* Get enabled processes and insert them in the interleave set of the graph_state */
}
}
-static void MC_replay_liveness(xbt_fifo_t stack)
+
+void LivenessChecker::replay(xbt_fifo_t stack)
{
xbt_fifo_item_t item;
simgrid::mc::Pair* pair = nullptr;
/**
* \brief Checks whether a given pair has already been visited by the algorithm.
*/
-static
-int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
{
if (_sg_mc_visited == 0)
return -1;
if (xbt_automaton_propositional_symbols_compare_value(
pair_test->atomic_propositions.get(),
new_visited_pair->atomic_propositions.get()) == 0) {
- if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+ if (this->compare(pair_test, new_visited_pair) == 0) {
if (pair_test->other_num == -1)
new_visited_pair->other_num = pair_test->num;
else
return -1;
}
-static int MC_modelcheck_liveness_main(void)
+LivenessChecker::LivenessChecker(Session& session) : Checker(session)
+{
+}
+
+LivenessChecker::~LivenessChecker()
+{
+}
+
+void LivenessChecker::showAcceptanceCycle(std::size_t depth)
+{
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("| ACCEPTANCE CYCLE |");
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("Counter-example that violates formula :");
+ MC_record_dump_path(mc_stack);
+ this->showStack(mc_stack);
+ this->dumpStack(mc_stack);
+ MC_print_statistics(mc_stats);
+ XBT_INFO("Counter-example depth : %zd", depth);
+}
+
+int LivenessChecker::main(void)
{
simgrid::mc::Pair* current_pair = nullptr;
int value, res, visited_num = -1;
simgrid::mc::Pair* next_pair = nullptr;
simgrid::xbt::unique_ptr<s_xbt_dynar_t> prop_values;
simgrid::mc::VisitedPair* reached_pair = nullptr;
-
+
while(xbt_fifo_size(mc_stack) > 0){
/* Get current pair */
if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) {
/* If new acceptance pair, return new pair */
- if ((reached_pair = is_reached_acceptance_pair(current_pair)) == nullptr) {
- int counter_example_depth = current_pair->depth;
- XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
- XBT_INFO("| ACCEPTANCE CYCLE |");
- XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
- XBT_INFO("Counter-example that violates formula :");
- MC_record_dump_path(mc_stack);
- simgrid::mc::show_stack_liveness(mc_stack);
- simgrid::mc::dump_stack_liveness(mc_stack);
- MC_print_statistics(mc_stats);
- XBT_INFO("Counter-example depth : %d", counter_example_depth);
+ if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
+ this->showAcceptanceCycle(current_pair->depth);
return SIMGRID_MC_EXIT_LIVENESS;
}
}
/* Pair already visited ? stop the exploration on the current path */
if ((current_pair->exploration_started == 0)
- && (visited_num = simgrid::mc::is_visited_pair(
+ && (visited_num = this->insertVisitedPair(
reached_pair, current_pair)) != -1) {
if (dot_output != nullptr){
XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
current_pair->requests = 0;
goto backtracking;
-
+
}else{
req = MC_state_get_request(current_pair->graph_state, &value);
/* Answer the request */
simgrid::mc::handle_simcall(req, value);
-
+
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();
current_pair->requests--;
current_pair->exploration_started = 1;
- /* Get values of atomic propositions (variables used in the property formula) */
- prop_values = get_atomic_propositions_values();
+ /* Get values of atomic propositions (variables used in the property formula) */
+ prop_values = this->getPropositionValues();
/* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
next_pair = new Pair();
next_pair->graph_state = MC_state_new();
next_pair->automaton_state = transition_succ->dst;
- next_pair->atomic_propositions = get_atomic_propositions_values();
+ next_pair->atomic_propositions = this->getPropositionValues();
next_pair->depth = current_pair->depth + 1;
/* Get enabled processes and insert them in the interleave set of the next graph_state */
for (auto& p : mc_model_checker->process().simix_processes())
}
} /* End of visited_pair test */
-
+
} else {
backtracking:
if(visited_num == -1)
XBT_DEBUG("No more request to execute. Looking for backtracking point.");
-
+
prop_values.reset();
-
+
/* 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 ((current_pair = (simgrid::mc::Pair*) xbt_fifo_shift(mc_stack)) != nullptr) {
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
xbt_fifo_unshift(mc_stack, current_pair);
- MC_replay_liveness(mc_stack);
+ this->replay(mc_stack);
XBT_DEBUG("Backtracking done");
break;
}else{
/* Delete pair */
XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
- if (current_pair->automaton_state->type == 1)
- remove_acceptance_pair(current_pair->num);
+ if (current_pair->automaton_state->type == 1)
+ this->removeAcceptancePair(current_pair->num);
delete current_pair;
}
}
} /* End of if (current_pair->requests > 0) else ... */
-
+
} /* End of while(xbt_fifo_size(mc_stack) > 0) */
XBT_INFO("No property violation found.");
return SIMGRID_MC_EXIT_SUCCESS;
}
-int modelcheck_liveness(void)
+int LivenessChecker::run()
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
/* Create the initial state */
initial_global_state = xbt_new0(s_mc_global_t, 1);
- MC_pre_modelcheck_liveness();
- int res = MC_modelcheck_liveness_main();
-
- return res;
+ this->prepare();
+ return this->main();
}
}
