#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
-#include "src/mc/explo/udpor/CompatibilityGraph.hpp"
#include <xbt/asserts.h>
#include <xbt/log.h>
// TODO: Add verbose logging about which event is being explored
- UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"UDPOR guarantees that an event will be chosen at each point in\n"
"the search, yet no events were actually chosen\n"
//
// ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
// U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
- UnfoldingEvent* e_cur = C.get_latest_event();
- EventSet exC = prev_exC;
+ const UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
exC.remove(e_cur);
for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
// where `a` is the `action` given to us.
EventSet incremental_exC;
- // We only consider those combinations of events for which `action` is dependent with
- // the action associated with any given event ("`a` depends on all of K")
- const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](const UnfoldingEvent* e) {
- const auto e_transition = e->get_transition();
- return action.depends(e_transition);
- });
-
- // TODO: Now that the graph has been constructed, enumerate
- // all possible k-cliques of the complement of G
-
- // TODO: For each enumeration, check all possible
- // combinations of selecting a single event from
- // each set associated with the graph nodes
+ // Compute the extension set here using the algorithm Martin described...
return incremental_exC;
}
return next_state;
}
-UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
if (!enC.empty()) {
return *(enC.begin());