Configuration C;
EventSet prev_exC;
- const auto initial_state = get_current_state();
+ auto initial_state = get_current_state();
const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
const auto root_event = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
explore(std::move(C), std::move(A), std::move(D), {EventSet()}, root_event.get(), std::move(prev_exC));
+
+ XBT_INFO("UDPOR exploration terminated -- model checking completed");
}
void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
StateHandle UdporChecker::record_newly_visited_state()
{
- const auto next_state = this->get_current_state();
+ auto next_state = this->get_current_state();
const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
// In UDPOR, we care about all enabled transitions in a given state
UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
- // TODO: Actually select an event here
+ if (!enC.empty()) {
+ return *(enC.begin());
+ }
+
+ for (const auto& event : A) {
+ if (enC.contains(event)) {
+ return event;
+ }
+ }
return nullptr;
}
{
this->events_.insert(e);
- // Re-compute the maxmimal events
+ // TODO: Re-compute the maxmimal events
}
UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& causes,
// TODO: Implement this
}
-StateManager::Handle StateManager::record_state(const std::unique_ptr<State>&& state)
+StateManager::Handle StateManager::record_state(std::unique_ptr<State> state)
{
- // // TODO: Throw an error perhaps if the state is nullptr?
+ if (state.get() == nullptr) {
+ throw std::invalid_argument("Expected a newly-allocated State but got NULL instead");
+ }
- // // std::map<int, std::unique_ptr<int>> a;
- // // auto test = std::make_unique<int>(10);
- // // std::move(state);
- // // // const auto&& ab = std::move(test);
- // // a.insert({1, test});
+ const auto integer_handle = this->current_handle_;
+ this->state_map_.insert({integer_handle, std::move(state)});
- // const auto&& state2 = std::move(state);
-
- // const auto integer_handle = this->current_handle_;
- // this->state_map_.insert(std::make_pair(std::move(integer_handle), state2));
-
- // // Increment the current handle
- // // TODO: Check for state handle overflow!
- // this->current_handle_++;
- return 0;
+ // TODO: Check for state handle overflow!
+ this->current_handle_++;
+ return integer_handle;
}
std::optional<std::reference_wrapper<State>> StateManager::get_state(StateManager::Handle handle)
{
- // TODO: Return the actual state based on the handle provided
- return std::nullopt;
+ auto state = this->state_map_.find(handle);
+ if (state == this->state_map_.end()) {
+ return std::nullopt;
+ }
+ auto& state_ref = *state->second.get();
+ return std::optional<std::reference_wrapper<State>>{state_ref};
}
} // namespace simgrid::mc::udpor
EventSet& operator=(const EventSet&) = default;
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
- // EventSet(const Configuration&);
- // EventSet(Configuration&&);
+
+ inline auto begin() const { return this->events_.begin(); }
+ inline auto end() const { return this->events_.end(); }
void remove(UnfoldingEvent* e);
void subtract(const EventSet& other);
using Handle = StateHandle;
Handle current_handle_ = 0ul;
- std::map<Handle, std::unique_ptr<State>> state_map_;
+ std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
public:
- Handle record_state(const std::unique_ptr<State>&&);
+ Handle record_state(std::unique_ptr<State>);
std::optional<std::reference_wrapper<State>> get_state(Handle);
};