Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase
See merge request simgrid/simgrid!139
include docs/source/Start_your_own_project.rst
include docs/source/The_XBT_toolbox.rst
include docs/source/Tutorial_Algorithms.rst
+include docs/source/Tutorial_DAG.rst
include docs/source/Tutorial_MPI_Applications.rst
include docs/source/Tutorial_Model-checking.rst
include docs/source/XML_reference.rst
include docs/source/img/zoom_comm.svg
include docs/source/index.rst
include docs/source/intl.rst
+include docs/source/tuto_dag/dag_lab1.cpp
+include docs/source/tuto_dag/dag_lab2-1.cpp
+include docs/source/tuto_dag/dag_lab2-2.cpp
+include docs/source/tuto_dag/dag_lab2-3.cpp
+include docs/source/tuto_dag/img/dag.svg
+include docs/source/tuto_dag/img/dag1.svg
+include docs/source/tuto_dag/img/dag2.svg
+include docs/source/tuto_dag/simple_dax.xml
+include docs/source/tuto_dag/simple_dot.dot
+include docs/source/tuto_dag/simple_json.json
+include docs/source/tuto_dag/small_platform.xml
include docs/source/tuto_disk/CMakeLists.txt
include docs/source/tuto_disk/Dockerfile
include docs/source/tuto_disk/analysis.irst
include src/kernel/xml/simgrid_dtd.c
include src/kernel/xml/simgrid_dtd.h
include src/mc/AddressSpace.hpp
-include src/mc/ModelChecker.cpp
-include src/mc/ModelChecker.hpp
include src/mc/VisitedState.cpp
include src/mc/VisitedState.hpp
include src/mc/api/ActorState.hpp
include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
+include src/mc/api/guide/BasicGuide.hpp
+include src/mc/api/guide/GuidedState.hpp
include src/mc/compare.cpp
include src/mc/datatypes.h
include src/mc/explo/CommunicationDeterminismChecker.cpp
include src/mc/explo/UdporChecker.cpp
include src/mc/explo/UdporChecker.hpp
include src/mc/explo/simgrid_mc.cpp
+ include src/mc/explo/udpor/Comb.hpp
include src/mc/explo/udpor/Configuration.cpp
include src/mc/explo/udpor/Configuration.hpp
include src/mc/explo/udpor/Configuration_test.cpp
include tools/cmake/Modules/FindNS3.cmake
include tools/cmake/Modules/FindPAPI.cmake
include tools/cmake/Modules/FindValgrind.cmake
+include tools/cmake/Modules/nlohmann_jsonConfig.cmake
include tools/cmake/Modules/pybind11Config.cmake
include tools/cmake/Option.cmake
include tools/cmake/Tests.cmake
#include "src/mc/explo/UdporChecker.hpp"
#include "src/mc/api/State.hpp"
+ #include "src/mc/explo/udpor/Comb.hpp"
+ #include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+
#include <xbt/asserts.h>
#include <xbt/log.h>
namespace simgrid::mc::udpor {
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
{
// Initialize the map
}
// are no enabled transitions that can be executed from the
// state reached by `C` (denoted `state(C)`), i.e. by some
// execution of the transitions in C obeying the causality
- // relation. Here, then, we would be in a deadlock.
+ // relation. Here, then, we may be in a deadlock (the other
+ // possibility is that we've finished running everything, and
+ // we wouldn't be in deadlock then)
if (enC.empty()) {
get_remote_app().check_deadlock();
}
"the search, yet no events were actually chosen\n"
"*********************************\n\n");
- // Move the application into stateCe and actually make note of that state
+ // Move the application into stateCe and make note of that state
move_to_stateCe(*stateC, *e);
auto stateCe = record_current_state();
// D <-- D + {e}
D.insert(e);
- // TODO: Determine a value of K to use or don't use it at all
constexpr unsigned K = 10;
- if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
- J.subtract(C.get_events());
+ if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
restore_program_state_to(*stateC);
// Explore(C, D + {e}, J \ C)
- explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
+ auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+ explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
}
// D <-- D - {e}
begin != maximal_subsets_iterator(); ++begin) {
const EventSet& maximal_subset = *begin;
- // TODO: Determine if `a` is enabled here
+ // 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) {
}
}
}
-
return incremental_exC;
}
"one transition of the state of an visited event is enabled, yet no\n"
"state was actually enabled. Please report this as a bug.\n"
"*********************************\n\n");
- state.execute_next(next_actor);
+ state.execute_next(next_actor, get_remote_app());
}
void UdporChecker::restore_program_state_to(const State& stateC)
{
- // TODO: Perform state regeneration in the same manner as is done
- // in the DFSChecker.cpp
+ get_remote_app().restore_initial_state();
+ // TODO: We need to have the stack of past states available at this
+ // point. Since the method is recursive, we'll need to keep track of
+ // this as we progress
}
std::unique_ptr<State> UdporChecker::record_current_state()
auto next_state = this->get_current_state();
// In UDPOR, we care about all enabled transitions in a given state
- next_state->mark_all_enabled_todo();
+ next_state->consider_all();
return next_state;
}
return nullptr;
}
- EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
- {
- // TODO: Compute k-partial alternatives using [2]
- return EventSet();
- }
-
void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
{
- // TODO: Perform clean up here
+ const EventSet C_union_D = C.get_events().make_union(D);
+ const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
+ const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
+
+ // Move {e} \ Q_CDU from U to G
+ if (Q_CDU.contains(e)) {
+ this->unfolding.remove(e);
+ }
+
+ // foreach ê in #ⁱ_U(e)
+ for (const auto* e_hat : es_immediate_conflicts) {
+ // Move [ê] \ Q_CDU from U to G
+ const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
+ this->unfolding.remove(to_remove);
+ }
}
RecordTrace UdporChecker::get_record_trace()
src/mc/explo/LivenessChecker.hpp
src/mc/explo/UdporChecker.cpp
src/mc/explo/UdporChecker.hpp
-
+
+ src/mc/explo/udpor/Comb.hpp
src/mc/explo/udpor/Configuration.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/EventSet.cpp
src/mc/transition/TransitionSynchro.cpp
src/mc/transition/TransitionSynchro.hpp
- src/mc/AddressSpace.hpp
- src/mc/ModelChecker.cpp
- src/mc/ModelChecker.hpp
- src/mc/VisitedState.cpp
- src/mc/VisitedState.hpp
+ src/mc/api/guide/BasicGuide.hpp
+ src/mc/api/guide/GuidedState.hpp
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
+
+ src/mc/AddressSpace.hpp
+ src/mc/VisitedState.cpp
+ src/mc/VisitedState.hpp
src/mc/compare.cpp
src/mc/mc_exit.hpp
src/mc/mc_forward.hpp
docs/source/tuto_s4u/master-workers-lab3.cpp
docs/source/tuto_s4u/master-workers-lab4.cpp
+ docs/source/Tutorial_DAG.rst
+ docs/source/tuto_dag/dag_lab1.cpp
+ docs/source/tuto_dag/dag_lab2-1.cpp
+ docs/source/tuto_dag/dag_lab2-2.cpp
+ docs/source/tuto_dag/dag_lab2-3.cpp
+ docs/source/tuto_dag/img/dag1.svg
+ docs/source/tuto_dag/img/dag2.svg
+ docs/source/tuto_dag/img/dag.svg
+ docs/source/tuto_dag/simple_dax.xml
+ docs/source/tuto_dag/simple_dot.dot
+ docs/source/tuto_dag/simple_json.json
+ docs/source/tuto_dag/small_platform.xml
+
docs/source/Tutorial_MPI_Applications.rst
docs/source/tuto_smpi/3hosts.png
docs/source/tuto_smpi/3hosts.xml
tools/cmake/Modules/FindNS3.cmake
tools/cmake/Modules/FindPAPI.cmake
tools/cmake/Modules/FindValgrind.cmake
+ tools/cmake/Modules/nlohmann_jsonConfig.cmake
tools/cmake/Modules/pybind11Config.cmake
tools/cmake/Option.cmake
tools/cmake/Tests.cmake
