Commit 318d80be authored by Jeroen Meijer's avatar Jeroen Meijer
Browse files

- change write to may-write.

- add must-write
- add copy
parent f9121a9f
......@@ -430,7 +430,8 @@ void dve_compiler::output_dependency_comment( ext_transition_t &ext_transition )
int count = count_state_variables();
char buf[BUFLEN];
append("// read : " );
line();
append("// read: " );
for(size_int_t i = 0; i < count; i++)
{
snprintf(buf, BUFLEN, "%s%d", ((i==0)?"":","), ext_transition.sv_read[i]);
......@@ -438,10 +439,18 @@ void dve_compiler::output_dependency_comment( ext_transition_t &ext_transition )
}
line();
append("// write: " );
append("// may-write: " );
for(size_int_t i = 0; i < count; i++)
{
snprintf(buf, BUFLEN, "%s%d", ((i==0)?"":","), ext_transition.sv_write[i]);
snprintf(buf, BUFLEN, "%s%d", ((i==0)?"":","), ext_transition.sv_may_write[i]);
append(buf);
}
line();
append("// must-write: " );
for(size_int_t i = 0; i < count; i++)
{
snprintf(buf, BUFLEN, "%s%d", ((i==0)?"":","), ext_transition.sv_must_write[i]);
append(buf);
}
line();
......@@ -472,15 +481,18 @@ void dve_compiler::analyse_expression( dve_expression_t & expr, ext_transition_t
mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, (*expr.left()).get_value(), dep);
} else {
// some expression, mark all & continue analysis
mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, -1, dep);
if (dep == ext_transition.sv_write && may_write_add_read) {
if (dep == ext_transition.sv_may_write || dep == ext_transition.sv_read) {
mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, -1, dep);
}
if (dep == ext_transition.sv_may_write && may_write_add_read) {
mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, -1, ext_transition.sv_read);
}
if ((*expr.left()).get_operator() == T_ASSIGNMENT) {
analyse_expression(*expr.left(), ext_transition, ext_transition.sv_write);
} else if (dep == ext_transition.sv_write) {
analyse_expression(*expr.left(), ext_transition, ext_transition.sv_may_write);
analyse_expression(*expr.left(), ext_transition, ext_transition.sv_must_write);
} else if (dep == ext_transition.sv_may_write) {
analyse_expression(*expr.left(), ext_transition, ext_transition.sv_read);
} else {
} else if (dep != ext_transition.sv_must_write) {
analyse_expression(*expr.left(), ext_transition, dep);
}
}
......@@ -493,7 +505,8 @@ void dve_compiler::analyse_expression( dve_expression_t & expr, ext_transition_t
analyse_expression( *expr.right(), ext_transition, ext_transition.sv_read );
break;
case T_ASSIGNMENT:
analyse_expression( *expr.left(), ext_transition, ext_transition.sv_write );
analyse_expression( *expr.left(), ext_transition, ext_transition.sv_may_write );
analyse_expression( *expr.left(), ext_transition, ext_transition.sv_must_write );
analyse_expression( *expr.right(), ext_transition, ext_transition.sv_read );
break;
case T_DOT:
......@@ -529,7 +542,8 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
// initialize read/write dependency vector
int count = count_state_variables();
ext_transition.sv_read.resize(count);
ext_transition.sv_write.resize(count);
ext_transition.sv_may_write.resize(count);
ext_transition.sv_must_write.resize(count);
// guard
......@@ -580,7 +594,9 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
{
// todo: test :)
analyse_expression( *(ext_transition.first->get_sync_expr_list_item(s)), ext_transition,
ext_transition.sv_write);
ext_transition.sv_may_write);
analyse_expression( *(ext_transition.first->get_sync_expr_list_item(s)), ext_transition,
ext_transition.sv_must_write);
analyse_expression( *(ext_transition.second->get_sync_expr_list_item(s)), ext_transition,
ext_transition.sv_read);
}
......@@ -590,7 +606,9 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
{
// mark entire channel
mark_dependency(ext_transition.first->get_channel_gid(),
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_write);
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_may_write);
mark_dependency(ext_transition.first->get_channel_gid(),
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_must_write);
// mark sync expressions
for(size_int_t s = 0;s < ext_transition.first->get_sync_expr_list_size();s++)
{
......@@ -604,12 +622,16 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
mark_dependency(ext_transition.first->get_channel_gid(),
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_read);
mark_dependency(ext_transition.first->get_channel_gid(),
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_write);
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_may_write);
mark_dependency(ext_transition.first->get_channel_gid(),
state_creator_t::CHANNEL_BUFFER, -1, ext_transition.sv_must_write);
// mark sync expressions
for(size_int_t s = 0;s < ext_transition.first->get_sync_expr_list_size();s++)
{
analyse_expression( *(ext_transition.first->get_sync_expr_list_item(s)), ext_transition,
ext_transition.sv_write);
ext_transition.sv_may_write);
analyse_expression( *(ext_transition.first->get_sync_expr_list_item(s)), ext_transition,
ext_transition.sv_must_write);
}
}
......@@ -618,7 +640,9 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
// mark process as read (write is probably in transition effect)
mark_dependency(ext_transition.first->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_write);
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_may_write);
mark_dependency(ext_transition.first->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_must_write);
// analyse ext_transition->first
for(size_int_t e = 0;e < ext_transition.first->get_effect_count();e++)
......@@ -630,7 +654,9 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
{
// mark process as read (write is probably in transition effect)
mark_dependency(ext_transition.second->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_write);
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_may_write);
mark_dependency(ext_transition.second->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_must_write);
// analyse ext_transition->second
for(size_int_t e = 0;e < ext_transition.second->get_effect_count();e++)
......@@ -642,7 +668,9 @@ void dve_compiler::analyse_transition_dependencies( ext_transition_t &ext_transi
{
// mark process as read/write?
mark_dependency(ext_transition.property->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_write);
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_may_write);
mark_dependency(ext_transition.property->get_process_gid(),
state_creator_t::PROCESS_STATE, -1, ext_transition.sv_must_write);
}
}
......@@ -842,9 +870,11 @@ void dve_compiler::transition_effect( ext_transition_t *et, std::string in, std:
{
if(et->synchronized)
{
for(size_int_t s = 0;s < et->first->get_sync_expr_list_size();s++)
for(size_int_t s = 0;s < et->first->get_sync_expr_list_size();s++) {
assign( cexpr( *et->first->get_sync_expr_list_item(s), out ),
cexpr( *et->second->get_sync_expr_list_item(s), in ) );
line("cpy[((int*)&"+cexpr( *et->first->get_sync_expr_list_item(s), out )+" - (int*)&"+out+")] = 0;");
}
}
else
{
......@@ -855,14 +885,17 @@ void dve_compiler::transition_effect( ext_transition_t *et, std::string in, std:
{
assign( channel_item_at( chan, channel_items( chan, in ), s, out ),
cexpr( *et->first->get_sync_expr_list_item( s ), in ) );
line("cpy[((int*)&"+channel_item_at( chan, channel_items( chan, in ), s, out )+" - (int*)&"+out+")] = 0;");
}
line( channel_items( chan, out ) + "++;" );
}
if(et->first->get_sync_mode() == SYNC_ASK_BUFFER)
{
for(size_int_t s = 0;s < et->first->get_sync_expr_list_size();s++)
for(size_int_t s = 0;s < et->first->get_sync_expr_list_size();s++) {
assign( cexpr( *et->first->get_sync_expr_list_item(s), out ),
channel_item_at( chan, "0", s, in ) );
line("cpy[((int*)&"+cexpr( *et->first->get_sync_expr_list_item(s), out )+" - (int*)&"+out+")] = 0;");
}
line( channel_items( chan, out ) + "--;" );
line( "for(size_int_t i = 1 ; i <= " + channel_items( chan, out ) + "; i++)" );
......@@ -870,7 +903,9 @@ void dve_compiler::transition_effect( ext_transition_t *et, std::string in, std:
for(size_int_t s = 0;s < et->first->get_sync_expr_list_size();s++)
{
assign( channel_item_at( chan, "i-1", s, out ), channel_item_at( chan, "i", s, in ) );
line("cpy[((int*)&"+channel_item_at( chan, "i-1", s, out )+" - (int*)&"+out+")] = 0;");
assign( channel_item_at( chan, "i", s, out ), "0" );
line("cpy[((int*)&"+channel_item_at( chan, "i", s, out )+" - (int*)&"+out+")] = 0;");
}
block_end();
}
......@@ -879,21 +914,30 @@ void dve_compiler::transition_effect( ext_transition_t *et, std::string in, std:
//first transition effect
assign( process_state( et->first->get_process_gid(), out ),
fmt( et->first->get_state2_lid() ) );
line("cpy[((int*)&"+process_state( et->first->get_process_gid(), out )+" - (int*)&"+out+")] = 0;");
for(size_int_t e = 0;e < et->first->get_effect_count();e++)
for(size_int_t e = 0;e < et->first->get_effect_count();e++) {
print_cexpr( *et->first->get_effect(e), out );
line("cpy[((int*)&"+cexpr(*et->first->get_effect(e)->left(), out)+" - (int*)&"+out+")] = 0;");
}
if(et->synchronized) //second transiton effect
{
assign( process_state( et->second->get_process_gid(), out ),
fmt( et->second->get_state2_lid() ) );
for(size_int_t e = 0;e < et->second->get_effect_count();e++)
line("cpy[((int*)&"+process_state( et->second->get_process_gid(), out )+" - (int*)&"+out+")] = 0;");
for(size_int_t e = 0;e < et->second->get_effect_count();e++) {
print_cexpr( *et->second->get_effect(e), out );
line("cpy[((int*)&"+cexpr(*et->second->get_effect(e)->left(), out)+" - (int*)&"+out+")] = 0;");
}
}
if(have_property) //change of the property process state
{
assign( process_state( et->property->get_process_gid(), out ),
fmt( et->property->get_state2_lid() ) );
line("cpy[((int*)&"+process_state( et->property->get_process_gid(), out )+" - (int*)&"+out+")] = 0;");
}
// show dependency information in the source
output_dependency_comment(*et);
......@@ -915,7 +959,7 @@ void dve_compiler::yield_state() {
if (many) {
line ("transition_info.group = " + fmt( current_label++) + ";");
}
line( "callback(arg, &transition_info, out);" );
line( "callback(arg, &transition_info, out, cpy);" );
line( "++states_emitted;" );
} else {
if ( many ) {
......@@ -1161,6 +1205,7 @@ void dve_compiler::gen_successors()
assign( process_state( (*iter_property_transitions)->get_process_gid(), out ),
fmt( (*iter_property_transitions)->get_state2_lid() ) );
line("cpy[((int*)&"+process_state( (*iter_property_transitions)->get_process_gid(), out )+" - (int*)&"+out+")] = 0;");
yield_state();
block_end();
......@@ -1233,13 +1278,16 @@ void dve_compiler::print_generator()
many = false;
current_label = 0;
line( "extern \"C\" int get_successor( void* model, int t, const state_struct_t *in, void (*callback)(void* arg, transition_info_t *transition_info, state_struct_t *out), void *arg ) " );
line( "extern \"C\" int get_successor( void* model, int t, const state_struct_t *in, void (*callback)(void* arg, transition_info_t *transition_info, state_struct_t *out, int *cpy), void *arg ) " );
block_begin();
line( "transition_info_t transition_info = { NULL, t, 0 };" );
line( "(void)model; // ignore model" );
line( "int states_emitted = 0;" );
line( "state_struct_t tmp;" );
line( "state_struct_t *out = &tmp;" );
append( "int cpy[" + fmt(count_state_variables())+ "] = { " );
for (int i = 0; i < count_state_variables(); i++) append ("1,");
line("};");
line( "goto switch_state;" );
gen_ltsmin_successors();
// switch block
......@@ -1257,7 +1305,7 @@ void dve_compiler::print_generator()
many = true;
current_label = 0;
line( "extern \"C\" int get_successors( void *model, const state_struct_t *in, void (*callback)(void *arg, transition_info_t *transition_info, state_struct_t *out), void *arg ) " );
line( "extern \"C\" int get_successors( void *model, const state_struct_t *in, void (*callback)(void *arg, transition_info_t *transition_info, state_struct_t *out, int *cpy), void *arg ) " );
block_begin();
line( "(void)model; // ignore model" );
line( "bool system_in_deadlock = true;" );
......@@ -1265,6 +1313,9 @@ void dve_compiler::print_generator()
line( "int states_emitted = 0;" );
line( "state_struct_t tmp;" );
line( "state_struct_t *out = &tmp;" );
append( "int cpy[" + fmt(count_state_variables())+ "] = { " );
for (int i = 0; i < count_state_variables(); i++) append ("1, ");
line("};");
gen_successors();
line( "return states_emitted;" );
block_end();
......@@ -1847,7 +1898,8 @@ void dve_compiler::merge_dependent_expression(std::vector<guard>& guard, int sv_
for(int i=0; i < guard.size(); i++) {
ext_transition_t et;
et.sv_read.resize(sv_count);
et.sv_write.resize(sv_count);
et.sv_may_write.resize(sv_count);
et.sv_must_write.resize(sv_count);
analyse_expression(*guard[i].expr.guard, et, et.sv_read);
guard_matrix[i] = et.sv_read;
}
......@@ -2027,7 +2079,8 @@ void dve_compiler::gen_transition_info()
// use ext_transition dummy to store read/write vector
ext_transition_t et;
et.sv_read.resize(sv_count);
et.sv_write.resize(sv_count);
et.sv_may_write.resize(sv_count);
et.sv_must_write.resize(sv_count);
analyse_expression(*guard[i].expr.guard, et, et.sv_read);
per_guard_matrix = et.sv_read;
} break;
......@@ -2150,17 +2203,17 @@ void dve_compiler::gen_transition_info()
}
}
}
transition_variable_set[i][j] = dep || current.sv_write[j];
transition_variable_set[i][j] = dep || current.sv_may_write[j];
transition_read_set[i][j] = dep;
transition_write_set[i][j] = current.sv_write[j];
transition_write_set[i][j] = current.sv_may_write[j];
}
}
// output transition vectors
snprintf(buf, BUFLEN, "int transition_dependency[][2][%d] = ", sv_count);
snprintf(buf, BUFLEN, "int transition_dependency[][3][%d] = ", sv_count);
line(buf);
block_begin();
line("// { ... read ...}, { ... write ...}");
line("// { ... read ...}, { ... may-write ...}, { ... must-write ...}");
for(size_int_t i = 0; i < transitions.size(); i++) {
ext_transition_t& current = transitions[i];
......@@ -2174,7 +2227,13 @@ void dve_compiler::gen_transition_info()
append("},{" );
for(size_int_t j = 0; j < sv_count; j++)
{
snprintf(buf, BUFLEN, "%s%d", ((j==0)?"":","), current.sv_write[j] );
snprintf(buf, BUFLEN, "%s%d", ((j==0)?"":","), current.sv_may_write[j] );
append(buf);
}
append("},{" );
for(size_int_t j = 0; j < sv_count; j++)
{
snprintf(buf, BUFLEN, "%s%d", ((j==0)?"":","), current.sv_must_write[j] );
append(buf);
}
append("}}");
......@@ -2202,8 +2261,8 @@ void dve_compiler::gen_transition_info()
block_end();
line();
// write dependencies
line( "extern \"C\" const int* get_transition_write_dependencies(int t) " );
// may_write dependencies
line( "extern \"C\" const int* get_transition_may_write_dependencies(int t) " );
block_begin();
snprintf(buf, BUFLEN, "if (t>=0 && t < %zu) return transition_dependency[t][1];", transitions.size());
line(buf);
......@@ -2212,6 +2271,23 @@ void dve_compiler::gen_transition_info()
block_end();
line();
// compatibility
line( "extern \"C\" const int* get_transition_write_dependencies(int t) " );
block_begin();
line("return get_transition_may_write_dependencies(t);");
block_end();
line();
// must_write dependencies
line( "extern \"C\" const int* get_transition_must_write_dependencies(int t) " );
block_begin();
snprintf(buf, BUFLEN, "if (t>=0 && t < %zu) return transition_dependency[t][2];", transitions.size());
line(buf);
snprintf(buf, BUFLEN, "return NULL;");
line(buf);
block_end();
line();
/////////////////////////////////////
/////////////////////////////////////
......@@ -2721,7 +2797,8 @@ dve_compiler::extract_assigns ( ext_transition_t *et,
ext_transition_t tmp;
int count = count_state_variables();
tmp.sv_read.resize(count);
tmp.sv_write.resize(count);
tmp.sv_may_write.resize(count);
tmp.sv_must_write.resize(count);
sync_mode_t sm = et->first->get_sync_mode();
if(et->synchronized)
......@@ -2815,7 +2892,8 @@ dve_compiler::get_assignment ( dve_expression_t & expr,
ext_transition_t tmp;
int count = count_state_variables();
tmp.sv_read.resize(count);
tmp.sv_write.resize(count);
tmp.sv_may_write.resize(count);
tmp.sv_must_write.resize(count);
if (expr.get_operator() == T_ASSIGNMENT) {
if ( !get_const_varname(*expr.left(), sp.variable_name) )
return false;
......
......@@ -21,7 +21,8 @@ struct ext_transition_t
dve_transition_t *second; // only when first transition is synchronized;
dve_transition_t *property; // transition of property automaton
std::vector<int> sv_read;
std::vector<int> sv_write;
std::vector<int> sv_may_write;
std::vector<int> sv_must_write;
};
typedef enum {GUARD_EXPR, GUARD_PC, GUARD_CHAN, GUARD_COMMITED_FIRST} guard_type;
......
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