#include <xbt/asserts.h>
#include <xbt/log.h>
+#include <xbt/string.hpp>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
void UdporChecker::run()
{
XBT_INFO("Starting a UDPOR exploration");
-
- auto state_stack = std::list<std::unique_ptr<State>>();
+ state_stack.clear();
state_stack.push_back(get_current_state());
-
- explore(Configuration(), EventSet(), EventSet(), state_stack, EventSet());
+ explore(Configuration(), EventSet(), EventSet(), EventSet());
XBT_INFO("UDPOR exploration terminated -- model checking completed");
}
-void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A,
- std::list<std::unique_ptr<State>>& state_stack, EventSet prev_exC)
+void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC)
{
auto& stateC = *state_stack.back();
auto exC = compute_exC(C, stateC, prev_exC);
move_to_stateCe(stateC, *e);
state_stack.push_back(record_current_state());
- explore(Ce, D, std::move(A), state_stack, std::move(exC));
+ explore(Ce, D, std::move(A), std::move(exC));
// Prepare to move the application back one state.
// We need only remove the state from the stack here: if we perform
// `state(C)` all together, the RemoteApp is currently sitting
// at some *future* state with resepct to `state(C)` since the
// recursive calls have moved it there.
- restore_program_state_with_sequence(state_stack);
+ restore_program_state_with_current_stack();
// Explore(C, D + {e}, J \ C)
auto J_minus_C = J.value().get_events().subtracting(C.get_events());
- explore(C, D, std::move(J_minus_C), state_stack, std::move(prev_exC));
+ explore(C, D, std::move(J_minus_C), std::move(prev_exC));
}
// D <-- D - {e}
return exC;
}
-EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
-{
- // Here we're computing the following:
- //
- // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
- //
- // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
- EventSet incremental_exC;
-
- for (auto begin =
- maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
- begin != maximal_subsets_iterator(); ++begin) {
- const EventSet& maximal_subset = *begin;
-
- // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
- // We leave the implementation as-is to ensure that any addition would be simple
- // if it were ever added
- const bool enabled_at_config_k = false;
-
- if (enabled_at_config_k) {
- auto event = std::make_unique<UnfoldingEvent>(maximal_subset, action);
- const auto handle = unfolding.insert(std::move(event));
- incremental_exC.insert(handle);
- }
- }
- return incremental_exC;
-}
-
EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
{
EventSet enC;
state.execute_next(next_actor, get_remote_app());
}
-void UdporChecker::restore_program_state_with_sequence(const std::list<std::unique_ptr<State>>& state_stack)
+void UdporChecker::restore_program_state_with_current_stack()
{
get_remote_app().restore_initial_state();
/* Traverse the stack from the state at position start and re-execute the transitions */
for (const std::unique_ptr<State>& state : state_stack) {
- if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
+ if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
break;
state->get_transition()->replay(get_remote_app());
}
const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
- if (!enC.empty()) {
+ if (enC.empty()) {
+ throw std::invalid_argument("There are no unfolding events to select. "
+ "Are you sure that you checked that en(C) was not "
+ "empty before attempting to select an event from it?");
+ }
+
+ if (A.empty()) {
return *(enC.begin());
}
RecordTrace UdporChecker::get_record_trace()
{
RecordTrace res;
+ for (auto const& state : state_stack)
+ res.push_back(state->get_transition());
return res;
}
std::vector<std::string> UdporChecker::get_textual_trace()
{
- // TODO: Topologically sort the events of the latest configuration
- // and iterate through that topological sorting
std::vector<std::string> trace;
+ for (auto const& state : state_stack) {
+ const auto* t = state->get_transition();
+ trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
+ }
return trace;
}
