model: pull thread control logic out of take_step(), check_current...()

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index cbd1027cf3c6874227ddf3ce9631cbea69b6eb82..73272809873ca66b11de81916f75c288953e4826 100644 (file)
--- a/model.h
+++ b/model.h
@@ -6,7 +6,6 @@
 #define __MODEL_H__
 
 #include <cstddef>
-#include <ucontext.h>
 #include <inttypes.h>
 
 #include "mymemory.h"
@@ -15,6 +14,7 @@
 #include "config.h"
 #include "modeltypes.h"
 #include "stl-model.h"
+#include "context.h"
 
 /* Forward declaration */
 class Node;
@@ -171,6 +171,7 @@ private:
        bool check_action_enabled(ModelAction *curr);
 
        Thread * take_step(ModelAction *curr);
+       bool should_terminate_execution();
 
        template <typename T>
        bool check_recency(ModelAction *curr, const T *rf) const;