{
}
+// virtual
RecordTrace Checker::getRecordTrace()
{
return {};
}
+// virtual
+std::vector<std::string> Checker::getTextualTrace()
+{
+ return {};
+}
+
}
}
* Could this be handled in the Session/ModelChecker instead?
*/
virtual RecordTrace getRecordTrace();
+ virtual std::vector<std::string> getTextualTrace();
protected:
Session& getSession() { return *session_; }
return std::move(res);
}
+// TODO, deduplicate with SafetyChecker
+std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
+{
+ std::vector<std::string> res;
+ for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ item; item = xbt_fifo_get_prev_item(item)) {
+ mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+ int value;
+ smx_simcall_t req = MC_state_get_executed_request(state, &value);
+ if (req) {
+ char* req_str = simgrid::mc::request_to_string(
+ req, value, simgrid::mc::RequestType::executed);
+ res.push_back(req_str);
+ xbt_free(req_str);
+ }
+ }
+ return std::move(res);
+}
+
void CommunicationDeterminismChecker::prepare()
{
mc_state_t initial_state = nullptr;
~CommunicationDeterminismChecker();
int run() override;
RecordTrace getRecordTrace() override;
+ std::vector<std::string> getTextualTrace() override;
private:
void prepare();
int main();
MC_state_delete(this->graph_state, 1);
}
-void LivenessChecker::showStack(xbt_fifo_t stack)
-{
- int value;
- simgrid::mc::Pair* pair;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(pair->graph_state, &value);
- if (req && req->call != SIMCALL_NONE) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void LivenessChecker::dumpStack(xbt_fifo_t stack)
-{
- simgrid::mc::Pair* pair;
- while ((pair = (simgrid::mc::Pair*) xbt_fifo_pop(stack)) != nullptr)
- delete pair;
-}
-
simgrid::xbt::unique_ptr<s_xbt_dynar_t> LivenessChecker::getPropositionValues()
{
unsigned int cursor = 0;
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
simgrid::mc::dumpRecordPath();
- this->showStack(mc_stack);
- this->dumpStack(mc_stack);
+ for (auto& s : this->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
XBT_INFO("Counter-example depth : %zd", depth);
}
+std::vector<std::string> LivenessChecker::getTextualTrace() // override
+{
+ std::vector<std::string> trace;
+ for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ item; item = xbt_fifo_get_prev_item(item)) {
+ simgrid::mc::Pair* pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+ int value;
+ smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value);
+ if (req && req->call != SIMCALL_NONE) {
+ char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
+ trace.push_back(std::string(req_str));
+ xbt_free(req_str);
+ }
+ }
+ return std::move(trace);
+}
+
int LivenessChecker::main(void)
{
simgrid::mc::Pair* current_pair = nullptr;
~LivenessChecker();
int run() override;
RecordTrace getRecordTrace() override;
+ std::vector<std::string> getTextualTrace() override;
private:
int main();
void prepare();
int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);
- void dumpStack(xbt_fifo_t stack);
- void showStack(xbt_fifo_t stack);
simgrid::xbt::unique_ptr<s_xbt_dynar_t> getPropositionValues();
simgrid::mc::VisitedPair* insertAcceptancePair(simgrid::mc::Pair* pair);
int insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
XBT_INFO("******************************************");
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
return std::move(res);
}
+std::vector<std::string> SafetyChecker::getTextualTrace() // override
+{
+ std::vector<std::string> trace;
+ for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ item; item = xbt_fifo_get_prev_item(item)) {
+ mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+ int value;
+ smx_simcall_t req = MC_state_get_executed_request(state, &value);
+ if (req) {
+ char* req_str = simgrid::mc::request_to_string(
+ req, value, simgrid::mc::RequestType::executed);
+ trace.push_back(req_str);
+ xbt_free(req_str);
+ }
+ }
+ return std::move(trace);
+}
+
int SafetyChecker::run()
{
this->init();
~SafetyChecker();
int run() override;
RecordTrace getRecordTrace() override;
+ std::vector<std::string> getTextualTrace() override;
private:
// Temp
void init();
XBT_DEBUG("**** End Replay ****");
}
-/**
- * \brief Dumps the contents of a model-checker's stack and shows the actual
- * execution trace
- * \param stack The stack to dump
- */
-void MC_dump_stack_safety(xbt_fifo_t stack)
-{
- MC_show_stack_safety(stack);
-
- mc_state_t state;
-
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != nullptr)
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
-}
-
-
-void MC_show_stack_safety(xbt_fifo_t stack)
-{
- int value;
- mc_state_t state;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t)xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(state, &value);
- if (req) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
void MC_show_deadlock(void)
{
XBT_INFO("**************************");
XBT_INFO("*** DEAD-LOCK DETECTED ***");
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
simgrid::mc::dumpRecordPath();
- MC_dump_stack_safety(mc_stack);
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
XBT_INFO("No core dump was generated by the system.");
XBT_INFO("Counter-example execution trace:");
simgrid::mc::dumpRecordPath();
- MC_dump_stack_safety(mc_stack);
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
MC_print_statistics(mc_stats);
}
XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
XBT_PRIVATE void MC_show_deadlock(void);
-XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
-XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
/** Stack (of `mc_state_t`) representing the current position of the
* the MC in the exploration graph