Skip to content
Snippets Groups Projects
Commit 4c730505 authored by Petr Rockai's avatar Petr Rockai
Browse files

MC: Make task_queue (and hence the weaver) more flexible.

parent 7de7b7c3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
divine/mc/search.hpp
+ 24
− 26
View file @ 4c730505
......@@ -19,41 +19,40 @@
#pragma once
#include <divine/mc/weaver.hpp>
namespace divine::mc
namespace divine::mc::task
{
template< typename State, typename Label >
struct GraphTasks
struct Edge
{
struct Edge
{
State from, to;
Label label;
bool isnew;
Edge( State f, State t, Label l, bool n )
: from( f ), to( t ), label( l ), isnew( n )
{}
};
struct Expand
{
State from;
Expand( State s ) : from( s ) {}
};
State from, to;
Label label;
bool isnew;
Edge( State f, State t, Label l, bool n )
: from( f ), to( t ), label( l ), isnew( n )
{}
};
struct Start {};
using TQ_ = TaskQueue< GraphTasks< State, Label >, Start, Expand, Edge >;
template< typename State >
struct Expand
{
State from;
Expand( State s ) : from( s ) {}
};
}
namespace divine::mc
{
template< typename State, typename Label >
using GraphTQ = typename GraphTasks< State, Label >::TQ_;
using GraphTQ = task_queue< task::Start, task::Expand< State >, task::Edge< State, Label > >;
template< typename TQ >
struct Search : TQ::Skel
template< typename State, typename Label >
struct Search : GraphTQ< State, Label >::skeleton
{
using Edge = typename TQ::Tasks::Edge;
using Expand = typename TQ::Tasks::Expand;
using TQ = GraphTQ< State, Label >;
using Edge = task::Edge< State, Label >;
using Expand = task::Expand< State >;
using TQ::Skel::run;
using TQ::skeleton::run;
void run( TQ &tq, Edge e )
{
......@@ -61,5 +60,4 @@ namespace divine::mc
tq.template add< Expand >( e.to );
}
};
}
divine/mc/t-search.hpp
+ 9
− 8
View file @ 4c730505
......@@ -26,15 +26,19 @@
namespace divine::t_mc
{
enum Label { Red, Black };
using TQ = mc::GraphTQ< int, Label >;
struct Base : TQ::Skel
using TQ = mc::GraphTQ< int, Label >;
using Edge = mc::task::Edge< int, Label >;
using Expand = mc::task::Expand< int >;
struct Base : TQ::skeleton
{
brq::concurrent_hash_set< int > _states;
using TQ::Skel::run;
using TQ::skeleton::run;
void run( TQ &tq, typename TQ::Tasks::Start )
void run( TQ &tq, mc::task::Start )
{
_states.insert( 1 );
tq.add< Expand >( 1 );
......@@ -126,13 +130,10 @@ namespace divine::t_mc
struct Search
{
using Edge = TQ::Tasks::Edge;
using Expand = TQ::Tasks::Expand;
template< typename B >
auto weave( B builder )
{
return mc::Weaver< TQ >().extend( mc::Search< TQ >(), builder );
return mc::Weaver< TQ >().extend( mc::Search< int, Label >(), builder );
}
TEST( fixed )
......
divine/mc/t-weaver.hpp
+ 25
− 26
View file @ 4c730505
......@@ -22,57 +22,56 @@
namespace divine::t_mc
{
struct Tasks
struct task1
{
struct T1
{
int i;
T1( int i ) : i( i ) {}
};
int i;
task1( int i ) : i( i ) {}
};
struct T2
{
int j;
T2( int j ) : j( j ) {}
};
struct task2
{
int j;
task2( int j ) : j( j ) {}
};
using TQ = mc::TaskQueue< Tasks, Tasks::T1, Tasks::T2 >;
using tq = mc::task_queue< task1, task2 >;
struct Machine1 : TQ::Skel
struct machine1 : tq::skeleton
{
using TQ::Skel::run;
void run( TQ &tq, Tasks::T1 t )
using tq::skeleton::run;
void run( tq &q, task1 t )
{
if ( t.i < 10 )
tq.add< T2 >( t.i + 1 );
q.add< task2 >( t.i + 1 );
}
};
struct Machine2 : TQ::Skel
struct machine2 : tq::skeleton
{
using TQ::Skel::run;
void run( TQ &tq, T2 t )
using tq::skeleton::run;
void run( tq &q, task2 t )
{
tq.add< T1 >( t.j + 1 );
q.add< task1 >( t.j + 1 );
}
};
struct Counter : Tasks
struct counter
{
int t1 = 0, t2 = 0;
void run( TQ &, T1 ) { ++t1; }
void run( TQ &, T2 ) { ++t2; }
void run( tq &, task1 ) { ++t1; }
void run( tq &, task2 ) { ++t2; }
};
struct Weave
{
TEST( basic )
{
mc::Weaver< TQ, Machine1, Machine2, Counter > weaver;
weaver.add< Tasks::T1 >( 3 );
mc::Weaver< tq, machine1, machine2, counter > weaver;
weaver.add< task1 >( 3 );
weaver.run();
auto &ctr = weaver.machine< Counter >();
auto &ctr = weaver.machine< counter >();
ASSERT_EQ( ctr.t1, 5 );
ASSERT_EQ( ctr.t2, 4 );
}
......
divine/mc/weaver.hpp
+ 38
− 49
View file @ 4c730505
......@@ -19,76 +19,65 @@
#pragma once
#include <deque>
namespace divine::mc
namespace divine::mc::task
{
struct Start {};
}
template< typename... > struct MachineSkel;
template< typename TS, typename TQ, typename Task, typename... Tasks >
struct MachineSkel< TS, TQ, Task, Tasks... > : MachineSkel< TS, TQ, Tasks... >
{
using MachineSkel< TS, TQ, Tasks... >::run;
void run( TQ &, Task ) {}
};
namespace divine::mc
{
template< typename... > struct task_queue;
template< typename TS, typename TQ >
struct MachineSkel< TS, TQ > : TS
template<>
struct task_queue<>
{
void run();
void clear();
template< typename P > bool process_next( P ) { return false; }
};
template< typename TaskStruct, typename... TaskList >
struct TaskQueue
template< typename task, typename... tasks >
struct task_queue< task, tasks... > : task_queue< tasks... >
{
using TQ = TaskQueue< TaskStruct, TaskList... >;
using Tasks = TaskStruct;
template< typename TS >
struct ExtendTS : TaskStruct, TS {};
using next = task_queue< tasks... >;
using tq = task_queue< task, tasks... >;
std::deque< task > _queue;
template< typename TS, typename... Extra >
using Extend = TaskQueue< ExtendTS< TS >, Extra..., TaskList... >;
template< typename... ex >
using extend = task_queue< ex..., tasks... >;
using Queues = std::tuple< std::deque< TaskList > ... >;
Queues _queues;
template< typename Task, typename... Args >
template< typename T, typename... Args >
void add( Args... args )
{
std::get< std::deque< Task > >( _queues ).emplace_back( args... );
if constexpr ( std::is_convertible_v< T, task > )
_queue.emplace_back( args... );
else
next::template add< T >( args... );
}
template< int i = 0 >
void clear()
{
if constexpr ( i < std::tuple_size_v< Queues > )
{
std::get< i >( _queues ).clear();
return clear< i + 1 >();
}
_queue.clear();
next::clear();
}
template< int i = 0, typename P >
template< typename P >
bool process_next( P process )
{
if constexpr ( i < std::tuple_size_v< Queues > )
if ( _queue.empty() )
return next::process_next( process );
else
{
auto &q = std::get< i >( _queues );
if ( !q.empty() )
{
process( q.front() );
q.pop_front();
return true;
}
return process_next< i + 1 >( process );
process( _queue.front() );
_queue.pop_front();
return true;
}
else
return false;
}
using Skel = MachineSkel< TaskStruct, TQ, TaskList... >;
struct skeleton
{
template< typename T >
void run( tq &, const T & ) {}
};
};
template< typename TQ, typename... Machines >
......@@ -213,12 +202,12 @@ namespace divine::mc
void run() /* TODO parallel */
{
auto process = [&]( auto t ) { process_task< 0 >( t ); };
while ( _queue.template process_next< 0 >( process ) );
while ( _queue.process_next( process ) );
}
void start()
{
add< typename TQ::Tasks::Start >();
add< task::Start >();
run();
}
};
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment