Commit aa0423df authored by Michael Weber's avatar Michael Weber

Merge remote branch 'laarman/next'

* laarman/next:
  timer fix: exclude hash table allocation time
  compiler fix: parenthesis around program counter guards
parents ff31c5f7 3bc7a42b
......@@ -105,6 +105,8 @@ struct Algorithm
}
}
//void init();
Algorithm( Config *c = 0, int slack = 0 )
: m_config( c ), m_slack( slack ), m_table( 0 )
{
......
......@@ -313,6 +313,15 @@ struct Map : Algorithm, DomainWorker< Map< G, _Statistics > >
ce._traceCycle( *this, hasher, table() );
}
void _init() {
m_initialTable = &shared.initialTable;
table();
}
void init() {
domain().parallel().run( shared, &This::_init );
}
Result run()
{
shared.iteration = 1;
......
......@@ -182,6 +182,15 @@ struct Metrics : Algorithm, DomainWorker< Metrics< G, Statistics > >
}
}
void _init() {
m_initialTable = &shared.initialTable;
table();
}
void init() {
domain().parallel().run( shared, &This::_init );
}
Result run() {
progress() << " exploring... \t\t\t " << std::flush;
domain().parallel().run( shared, &This::_visit );
......
......@@ -26,6 +26,8 @@ struct NestedDFS : Algorithm
std::deque< Node > ce_lasso;
std::deque< Node > toexpand;
void init() {}
algorithm::Statistics< G > stats;
struct Extension {
......
......@@ -509,6 +509,15 @@ struct Owcty : Algorithm, DomainWorker< Owcty< G, Statistics > >
shared.stats.updateResult( result() );
shared.stats = algorithm::Statistics< G >();
}
void _init() {
m_initialTable = &shared.initialTable;
table();
}
void init() {
domain().parallel().run( shared, &This::_init );
}
Result run()
{
......
......@@ -178,6 +178,15 @@ struct Reachability : Algorithm, DomainWorker< Reachability< G, Statistics > >
}
}
void _init() {
m_initialTable = &shared.initialTable;
table();
}
void init() {
domain().parallel().run( shared, &This::_init );
}
Result run() {
progress() << " searching... \t" << std::flush;
......
......@@ -136,6 +136,15 @@ struct Simple : Algorithm, DomainWorker< Simple< G > >
}
}
void _init() {
m_initialTable = &shared.initialTable;
table();
}
void init() {
domain().parallel().run( shared, &This::_init );
}
Result run() {
progress() << " exploring... \t\t\t\t" << std::flush;
domain().parallel().run( shared, &This::_visit );
......
......@@ -97,6 +97,17 @@ struct Report
}
#endif
void reset() {
#ifdef POSIX
gettimeofday(&tv, NULL);
#endif
#ifdef _WIN32
hProcess = GetCurrentProcess();
GetLocalTime(&stStart);
#endif
}
void signal( int s )
{
m_finished = false;
......
......@@ -93,9 +93,9 @@ struct Main {
return;
}
Result res;
Report rep( config );
report = &rep;
Result res;
#ifdef PERFORMANCE
if ( statistics )
......@@ -444,6 +444,8 @@ struct Main {
Result run() {
try {
Algorithm alg( &config );
alg.init();
report->reset();
setupParallel< Stats >( Preferred(), report, alg );
return alg.run();
} catch (std::exception &e) {
......
......@@ -94,10 +94,9 @@ void dve_compiler::write_C(dve_expression_t & expr, std::ostream & ostr, std::st
break;
case T_DOT:
ostr<<state_name<<".";
ostr<<parent_table->get_process(parent_table->get_state(expr.get_ident_gid())->
get_process_gid())->get_name(); ostr<<".state"<<(ltsmin?".var":"")<<" == ";
ostr<<parent_table->get_state(expr.get_ident_gid())->get_lid();
ostr << in_state(
parent_table->get_state(expr.get_ident_gid())->get_process_gid(),
parent_table->get_state(expr.get_ident_gid())->get_lid(), state_name );
break;
case T_IMPLY:
......
......@@ -175,7 +175,7 @@ struct dve_compiler: public dve_explicit_system_t
void block_end() { deindent(); line( "}" ); }
std::string in_state( int process, int state, std::string from_state ) {
return process_state( process, from_state ) + " == " + wibble::str::fmt( state );
return "(" + process_state( process, from_state ) + " == " + wibble::str::fmt( state ) + ")";
}
void setOutput( std::ostream &o ) {
......
Markdown is supported
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