#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}
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());
}
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;
}
private:
Unfolding unfolding = Unfolding();
+ // The current sequence of states that the checker has
+ // visited in order to reach the current configuration
+ std::list<std::unique_ptr<State>> state_stack;
+
/**
* @brief Explores the unfolding of the concurrent system
* represented by the ModelChecker instance "mcmodel_checker"
* @param A the set of events to "guide" UDPOR in the correct direction
* when it returns back to a node in the unfolding and must decide among
* events to select from `ex(C)`. See [1] for more details
- * @param stateSequence the sequence of states entered by the program
- * while UDPOR explored `C`. The program is in `state(C)` (using the notation of [1]),
- * which is the result of executing all actions in the stack
- *
- * TODO: We pass around the reference to the stack which is modified
- * appropriately in each recursive call. An iterative version would not
- * need to pass around the states in this manner: the `std::stack<...>`
- * could be a local variable of the function
*
* TODO: Add the optimization where we can check if e == e_prior
* to prevent repeated work when computing ex(C)
*/
- void explore(const Configuration& C, EventSet D, EventSet A, std::list<std::unique_ptr<State>>& state_stack,
- EventSet prev_exC);
+ void explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC);
/**
* @brief Identifies the next event from the unfolding of the concurrent system
* The UDPOR implementation in SimGrid ensures that the stack is updated appropriately,
* but the process must still be regenerated.
*/
- void restore_program_state_with_sequence(const std::list<std::unique_ptr<State>>& state_stack);
+ void restore_program_state_with_current_stack();
/**
* @brief Perform the functionality of the `Remove(e, C, D)` function in [1]
