From cb707b8701ee4fd96572edd26a456649cf82565c Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Tue, 30 Jul 2019 14:00:23 +0000
Subject: [PATCH] MC: Extract the task queue type from the final machine stack.
---
divine/mc/machine.hpp | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/divine/mc/machine.hpp b/divine/mc/machine.hpp
index ca14ecb94..9ceb142a4 100644
--- a/divine/mc/machine.hpp
+++ b/divine/mc/machine.hpp
@@ -491,9 +491,19 @@ namespace divine::mc
struct TMachine : machine::tree< smt::NoSolver > {};
struct GMachine : machine::graph< smt::NoSolver > {};
+ template< typename M >
+ struct TQ : M::tq {};
+
+ template< typename M >
+ struct MW
+ {
+ struct TQ : M::tq {};
+ struct W : Weaver< TQ > {};
+ };
+
template< typename M >
auto weave( M &machine )
{
- return mc::Weaver< typename M::tq >().extend_ref( machine );
+ return typename MW< M >::W().extend_ref( machine );
}
}
--
GitLab