Implement the RandomTransition

diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp
index bb1dada..9a479e9 100644 (file)
--- a/src/kernel/actor/SimcallObserver.cpp
+++ b/src/kernel/actor/SimcallObserver.cpp
@@ -28,6 +28,15 @@ bool RandomSimcall::depends(SimcallObserver* other)
 {
   return get_issuer() == other->get_issuer();
 }
+void RandomSimcall::serialize(Simcall& type, char* buffer)
+{
+  type = Simcall::RANDOM;
+  std::stringstream stream;
+
+  stream << min_ << ' ' << max_;
+  strcpy(buffer, stream.str().c_str());
+}
+
 bool MutexSimcall::depends(SimcallObserver* other)
 {
   if (dynamic_cast<RandomSimcall*>(other) != nullptr)

diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp
index c3ae91b..95f6e25 100644 (file)
--- a/src/kernel/actor/SimcallObserver.hpp
+++ b/src/kernel/actor/SimcallObserver.hpp
@@ -94,7 +94,7 @@ public:
     res->next_value_ = next_value_;
     return res;
   }
-  void serialize(Simcall& type, char* buffer) override { type = Simcall::RANDOM; }
+  void serialize(Simcall& type, char* buffer) override;
   int get_max_consider() const override;
   void prepare(int times_considered) override;
   std::string dot_label(int times_considered) const override;

diff --git a/src/mc/api/Transition.cpp b/src/mc/api/Transition.cpp
index 79d7d62..c964e68 100644 (file)
--- a/src/mc/api/Transition.cpp
+++ b/src/mc/api/Transition.cpp
@@ -5,7 +5,9 @@
 
 #include "src/mc/api/Transition.hpp"
 #include "xbt/asserts.h"
+#include "xbt/string.hpp"
 #include <simgrid/config.h>
+
 #if SIMGRID_HAVE_MC
 #include "src/mc/ModelChecker.hpp"
 #endif
@@ -40,6 +42,17 @@ void Transition::replay() const
   mc_model_checker->wait_for_requests();
 #endif
 }
+std::string RandomTransition::to_string(bool verbose)
+{
+  return xbt::string_printf("Random([%d;%d] ~> %d)", min_, max_, times_considered_);
+}
+
+RandomTransition::RandomTransition(aid_t issuer, int times_considered, char* buffer)
+    : Transition(issuer, times_considered)
+{
+  std::stringstream stream(buffer);
+  stream >> min_ >> max_;
+}
 
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/api/Transition.hpp b/src/mc/api/Transition.hpp
index 9955b01..416241b 100644 (file)
--- a/src/mc/api/Transition.hpp
+++ b/src/mc/api/Transition.hpp
@@ -63,6 +63,16 @@ public:
   static unsigned long get_replayed_transitions() { return replayed_transitions_; }
 };
 
+class RandomTransition : public Transition {
+  int min_;
+  int max_;
+
+public:
+  std::string to_string(bool verbose) override;
+  RandomTransition(aid_t issuer, int times_considered, char* buffer);
+  bool depends(const Transition* other) const override { return false; } // Independent with any other transition
+};
+
 } // namespace mc
 } // namespace simgrid
 

diff --git a/src/mc/api/TransitionComm.cpp b/src/mc/api/TransitionComm.cpp
index 6cc54f8..1e38480 100644 (file)
--- a/src/mc/api/TransitionComm.cpp
+++ b/src/mc/api/TransitionComm.cpp
@@ -44,6 +44,9 @@ bool CommWaitTransition::depends(const Transition* other) const
   if (aid_ == other->aid_)
     return false;
 
+  if (dynamic_cast<const RandomTransition*>(other) != nullptr)
+    return false; // Random is indep with any transition
+
   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
     return send->depends(this);
 
@@ -84,6 +87,9 @@ bool CommRecvTransition::depends(const Transition* other) const
   if (aid_ == other->aid_)
     return false;
 
+  if (dynamic_cast<const RandomTransition*>(other) != nullptr)
+    return false; // Random is indep with any transition
+
   if (const auto* other_irecv = dynamic_cast<const CommRecvTransition*>(other))
     return mbox_ == other_irecv->mbox_;
 
@@ -134,6 +140,9 @@ bool CommSendTransition::depends(const Transition* other) const
   if (aid_ == other->aid_)
     return false;
 
+  if (dynamic_cast<const RandomTransition*>(other) != nullptr)
+    return false; // Random is indep with any transition
+
   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
     return mbox_ == other_isend->mbox_;
 
@@ -175,6 +184,10 @@ Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::S
       return new CommRecvTransition(issuer, times_considered, buffer);
     case kernel::actor::SimcallObserver::Simcall::ISEND:
       return new CommSendTransition(issuer, times_considered, buffer);
+
+    case kernel::actor::SimcallObserver::Simcall::RANDOM:
+      return new RandomTransition(issuer, times_considered, buffer);
+
     case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
       return new Transition(issuer, times_considered);
     default:

diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh
index 84cba92..d67b4fc 100644 (file)
--- a/teshsuite/mc/random-bug/random-bug.tesh
+++ b/teshsuite/mc/random-bug/random-bug.tesh
@@ -7,12 +7,12 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(3)
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(4)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 3)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 4)
 > [  0.000000] (0:maestro@) Path = 1/3;1/4
 > [  0.000000] (0:maestro@) Expanded states = 27
 > [  0.000000] (0:maestro@) Visited states = 68
-> [  0.000000] (0:maestro@) Executed transitions = 46
+> [  0.000000] (0:maestro@) Executed transitions = 27
 
 ! expect return 6
 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
@@ -24,12 +24,12 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) From signal: Aborted
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(3)
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(4)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 3)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 4)
 > [  0.000000] (0:maestro@) Path = 1/3;1/4
 > [  0.000000] (0:maestro@) Expanded states = 27
 > [  0.000000] (0:maestro@) Visited states = 68
-> [  0.000000] (0:maestro@) Executed transitions = 46
+> [  0.000000] (0:maestro@) Executed transitions = 27
 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
 
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
@@ -39,7 +39,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir
 > [  0.000000] (0:maestro@) No property violation found.
 > [  0.000000] (0:maestro@) Expanded states = 43
 > [  0.000000] (0:maestro@) Visited states = 108
-> [  0.000000] (0:maestro@) Executed transitions = 72
+> [  0.000000] (0:maestro@) Executed transitions = 42
 
 ! expect return 6
 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
@@ -52,10 +52,10 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) From signal: Segmentation fault
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(3)
-> [  0.000000] (0:maestro@)   [(1)Fafard (app)] MC_RANDOM(4)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 3)
+> [  0.000000] (0:maestro@)   Random([0;5] ~> 4)
 > [  0.000000] (0:maestro@) Path = 1/3;1/4
 > [  0.000000] (0:maestro@) Expanded states = 27
 > [  0.000000] (0:maestro@) Visited states = 68
-> [  0.000000] (0:maestro@) Executed transitions = 46
+> [  0.000000] (0:maestro@) Executed transitions = 27
 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc