1 /* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "src/mc/explo/UdporChecker.hpp"
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification ");
11 namespace simgrid::mc::udpor {
13 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
15 /* Create initial data structures, if any ...*/
16 XBT_INFO("Starting a UDPOR exploration");
18 // TODO: Initialize state structures for the search
21 void UdporChecker::run()
23 // NOTE: `A`, `D`, and `C` are derived from the
24 // original UDPOR paper [1], while
25 // `prev_exC` arises from the incremental computation
26 // of ex(C) from the former paper described in [3]
32 * Maintains the mapping between handles referenced by events in
33 * the current state of the unfolding
35 StateManager state_manager_;
37 const auto initial_state = std::make_unique<State>(get_remote_app());
38 const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
39 const auto root_event = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
40 explore(std::move(C), {EventSet()}, std::move(D), std::move(A), root_event.get(), std::move(prev_exC));
43 void UdporChecker::explore(Configuration C, std::list<EventSet> max_evt_history, EventSet D, EventSet A,
44 UnfoldingEvent* cur_evt, EventSet prev_exC)
46 // Perform the incremental computation of exC
47 auto [exC, enC] = this->extend(C, max_evt_history, *cur_evt, prev_exC);
49 // If enC is a subset of D, intuitively
50 // there aren't any enabled transitions
51 // which are "worth" exploring since their
52 // exploration would lead to a so-called
53 // "sleep-set blocked" trace.
54 if (enC.is_subset_of(D)) {
57 if (C.events_.size() > 0) {
59 // g_var::nb_traces++;
61 // TODO: Log here correctly
62 // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
67 // When `en(C)` is empty, intuitively this means that there
68 // are no enabled transitions that can be executed from the
69 // state reached by `C` (denoted `state(C)`) (i.e. by some
70 // execution of the transitions in C obeying the causality
71 // relation). Hence, it is at this point we should check for a deadlock
73 get_remote_app().check_deadlock();
79 UnfoldingEvent* e = this->select_next_unfolding_event(A, enC);
81 XBT_ERROR("\n\n****** CRITICAL ERROR ****** \n"
82 "UDPOR guarantees that an event will be chosen here, yet no events were actually chosen...\n"
83 "******************");
87 // TODO: Add verbose logging about which event is being explored
89 // TODO: Execute the transition associated with the event
90 // and map the new state
92 // const auto cur_state_id = cur_evt->get_state_id();
93 // auto curEv_StateId = currentEvt->get_state_id();
94 // auto nextState_id = App::app_side_->execute_transition(curEv_StateId, e->get_transition_tag());
95 // e->set_state_id(nextState_id);
97 // Configuration is the same + event e
100 C1.events_.insert(e);
101 C1.updateMaxEvent(e);
103 max_evt_history.push_back(C1.maxEvent);
105 // A <-- A \ {e}, ex(C) <-- ex(C) \ {e}
109 // Explore(C + {e}, D, A \ {e})
110 this->explore(C1, max_evt_history, D, A, e, exC);
115 // TODO: Determine a value of K to use or don't use it at all
116 constexpr unsigned K = 10;
117 auto J = this->compute_partial_alternative(D, C, K);
119 J.subtract(C.events_);
120 max_evt_history.pop_back();
121 explore(C, max_evt_history, D, J, cur_evt, prev_exC);
126 this->clean_up_explore(e, C, D);
129 std::tuple<EventSet, EventSet> UdporChecker::extend(const Configuration& C, const std::list<EventSet>& max_evt_history,
130 const UnfoldingEvent& cur_event, const EventSet& prev_exC) const
132 // exC.remove(cur_event);
134 // TODO: Compute extend() as it exists in tiny_simgrid
137 return std::tuple<EventSet, EventSet>();
140 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
142 // TODO: Actually select an event here
146 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const EventSet& C, const unsigned k) const
148 // TODO: Compute k-partial alternatives using [2]
152 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const EventSet& C, const EventSet& D)
154 // TODO: Perform clean up here
157 RecordTrace UdporChecker::get_record_trace()
163 std::vector<std::string> UdporChecker::get_textual_trace()
165 std::vector<std::string> trace;
169 } // namespace simgrid::mc::udpor
171 namespace simgrid::mc {
173 Exploration* create_udpor_checker(const std::vector<char*>& args)
175 return new simgrid::mc::udpor::UdporChecker(args);
178 } // namespace simgrid::mc