Skip to content

GitLab

Commit b2b7d671 authored by Elwin Pater's avatar Elwin Pater Committed by Michael Weber
Browse files

Export guards 

    * Split guard on localstate, condition and channel
    * Works for committed transitions
parent 516abcc2
Hide whitespace changes
Inline Side-by-side
tools/dvecompile.cpp
View file @ b2b7d671
......@@ -962,16 +962,6 @@ void dve_compiler::gen_ltsmin_successors()
// only generate if not synchonized or synchonized with a committed transition
new_label();
// committed state
if_begin( true );
for(size_int_t p = 0; p < get_process_count(); p++)
for(size_int_t c = 0; c < dynamic_cast<dve_process_t*>(get_process(p))->get_state_count(); c++)
if(dynamic_cast<dve_process_t*>(get_process(p))->get_commited(c))
if_clause( in_state( p, c, in ) );
if_end(); // otherwise this condition is disjoint with the new condition
transition_guard( &*iter_ext_transition_vector, in );
block_begin();
new_output_state();
......@@ -1651,6 +1641,75 @@ void dve_compiler::gen_state_info()
}
bool dve_compiler::eq_expr(dve_expression_t* e1, dve_expression_t* e2) {
bool result = false;
const char* s1 = strdup(cexpr(*e1, "(..)").c_str());
const char* s2 = strdup(cexpr(*e2, "(..)").c_str());
result = strcmp(s1, s2)==0;
free((void*)s1);
free((void*)s2);
return result;
}
int dve_compiler::add_guard_pc(std::vector<guard> &guard, divine::size_int_t gid, divine::size_int_t lid) {
// look for program counter guard
for(int i=0; i < guard.size(); i++) {
if (guard[i].type == GUARD_PC) {
if (guard[i].pc.gid == gid && guard[i].pc.lid == lid) {
return i;
}
}
}
// not found, add this one as new
struct guard g;
g.type = GUARD_PC;
g.pc.gid = gid;
g.pc.lid = lid;
guard.push_back(g);
return guard.size() - 1;
}
int dve_compiler::add_guard_expr(std::vector<guard> &guard, dve_expression_t* expr) {
// look for expression guard
for(int i=0; i < guard.size(); i++) {
if (guard[i].type == GUARD_EXPR) {
if (eq_expr(expr, guard[i].expr.guard)) {
return i;
}
}
}
// not found, add this one as new
struct guard g;
g.type = GUARD_EXPR;
g.expr.guard = expr;
guard.push_back(g);
return guard.size() - 1;
}
int dve_compiler::add_guard_chan(std::vector<guard> &guard, divine::size_int_t chan, divine::sync_mode_t sync_mode) {
// look for expression guard
for(int i=0; i < guard.size(); i++) {
if (guard[i].type == GUARD_CHAN) {
if (guard[i].chan.chan == chan && guard[i].chan.sync_mode == sync_mode) {
return i;
}
}
}
// not found, add this one as new
struct guard g;
g.type = GUARD_CHAN;
g.chan.chan = chan;
g.chan.sync_mode = sync_mode;
guard.push_back(g);
return guard.size() - 1;
}
void dve_compiler::fill_transition_vector(std::vector<ext_transition_t>& transitions)
{
// true if committed states are found
......@@ -1719,6 +1778,7 @@ void dve_compiler::fill_transition_vector(std::vector<ext_transition_t>& transit
void dve_compiler::gen_transition_info()
{
int sv_count = count_state_variables();
bool has_commited = false;
char buf[1024];
// initialize read/write dependency vector
......@@ -1729,9 +1789,11 @@ void dve_compiler::gen_transition_info()
// mark commited processes as read
for(size_int_t i = 0; i < get_process_count(); i++)
for(size_int_t j = 0; j < dynamic_cast<dve_process_t*>(get_process(i))->get_state_count(); j++)
if(dynamic_cast<dve_process_t*>(get_process(i))->get_commited(j))
if(dynamic_cast<dve_process_t*>(get_process(i))->get_commited(j)) {
has_commited = true;
mark_dependency(dynamic_cast<dve_process_t*>(get_process(i))->get_gid(),
state_creator_t::PROCESS_STATE, -1, c_base_sv_read);
}
// output transition vectors
sprintf(buf, "int transition_dependency[][2][%d] = ", sv_count);
......@@ -1745,7 +1807,7 @@ void dve_compiler::gen_transition_info()
append("{{" );
for(size_int_t j = 0; j < sv_count; j++)
{
sprintf(buf, "%s%d", ((j==0)?"":","), max(c_base_sv_read[j], current.sv_read[j]) );
sprintf(buf, "%s%d", ((j==0)?"":","), (current.commited?current.sv_read[j]:max(c_base_sv_read[j], current.sv_read[j])) );
append(buf);
}
append("},{" );
......@@ -1814,7 +1876,152 @@ void dve_compiler::gen_transition_info()
block_end();
line();
/////////////////////////////////
// SPLIT THE GUARD EXPRESSIONS //
/////////////////////////////////
// transition -> set of guards
std::map<int, std::set<int> > guards;
// set of guards
std::vector<guard> guard;
// reserve two guards for committed/not committed
if (has_commited) {
struct guard g;
g.type = GUARD_COMMITED_FIRST;
guard.push_back(g);
}
for(size_int_t i = 0; i < transitions.size(); i++) {
ext_transition_t& current = transitions[i];
// reference to the set of guards for transition i
set<int>& gs = guards[i];
int g;
// push the local state as guard
g = add_guard_pc(guard, current.first->get_process_gid(), current.first->get_state1_lid());
gs.insert(g);
// push first guard as a whole
if (current.first->get_guard()) {
g = add_guard_expr(guard, current.first->get_guard());
gs.insert(g);
}
// check synchronized
if ( current.synchronized ) {
g = add_guard_pc(guard, current.second->get_process_gid(), current.second->get_state1_lid());
gs.insert(g);
if (current.second->get_guard()) {
g = add_guard_expr(guard, current.second->get_guard());
gs.insert(g);
}
} else {
// synchronized on channel?
int chan = current.first->get_channel_gid();
if (current.first->get_sync_mode() == SYNC_EXCLAIM_BUFFER ||
current.first->get_sync_mode() == SYNC_ASK_BUFFER) {
g = add_guard_chan(guard, chan, current.first->get_sync_mode());
gs.insert(g);
}
}
// committed?
if (has_commited) {
if (!current.commited) {
gs.insert(0);
}
}
}
// export the guard value for this state
line ("extern \"C\" const bool get_guard(int g, state_struct_t* src) " );
block_begin();
line("switch(g)");
block_begin();
for(int i=0; i<guard.size(); i++) {
switch(guard[i].type) {
case GUARD_PC:
sprintf(buf, "case %d: return (%s);", i, in_state(guard[i].pc.gid, guard[i].pc.lid, "(*src)").c_str());
line(buf);
break;
case GUARD_EXPR:
sprintf(buf, "case %d: return (%s);", i, cexpr(*guard[i].expr.guard,"(*src)").c_str());
line(buf);
break;
case GUARD_CHAN:
sprintf(buf, "case %d: return (%s);", i, relate( channel_items(guard[i].chan.chan, "(*src)"), "!=",
(guard[i].chan.sync_mode == SYNC_EXCLAIM_BUFFER? fmt( channel_capacity( guard[i].chan.chan ) ) : "0" ) ).c_str());
line(buf);
break;
case GUARD_COMMITED_FIRST:
sprintf(buf, "case %d:", i);
line(buf);
// committed state
block_begin();
if_begin( true );
for(size_int_t p = 0; p < get_process_count(); p++)
for(size_int_t c = 0; c < dynamic_cast<dve_process_t*>(get_process(p))->get_state_count(); c++)
if(dynamic_cast<dve_process_t*>(get_process(p))->get_commited(c))
if_clause( in_state( p, c, "(*src)" ) );
if_end();
line(" return 0;"); // bail out early
line("return 1;");
block_end();
break;
}
}
block_end();
sprintf(buf, "return false;");
line(buf);
block_end();
line();
// export the number of guards
line ("extern \"C\" const int get_guards_count() " );
block_begin();
sprintf(buf, "return %zu;", guard.size());
line(buf);
block_end();
line();
sprintf(buf, "int* guards_per_transition[%zu] = ", transitions.size() );
line(buf);
block_begin();
for(int i=0; i < transitions.size(); i++) {
set<int>& gs = guards[i];
sprintf(buf, "((int[]){");
append(buf);
sprintf(buf, "%zu", gs.size());
append(buf);
for(set<int>::iterator ix = gs.begin(); ix != gs.end(); ix++) {
sprintf(buf, ", %d", *ix);
append(buf);
}
line("}),");
}
block_end();
line(";");
line();
// export the guards per transition group
line ("extern \"C\" const int* get_guards(int t) " );
block_begin();
sprintf(buf, "if (t>=0 && t < %zu) return guards_per_transition[t];", transitions.size());
line(buf);
line("return NULL;");
block_end();
line();
line ("extern \"C\" const int** get_all_guards() " );
block_begin();
line("return (const int**)&guards_per_transition;");
block_end();
line();
}
......
tools/dvecompile.h
View file @ b2b7d671
......@@ -23,6 +23,28 @@ struct ext_transition_t
std::vector<int> sv_write;
};
typedef enum {GUARD_EXPR, GUARD_PC, GUARD_CHAN, GUARD_COMMITED_FIRST} guard_type;
struct guard
{
guard_type type;
union
{
struct {
dve_expression_t * guard;
} expr; // expression
struct {
divine::size_int_t gid;
divine::size_int_t lid;
} pc; // programm counter
struct {
divine::size_int_t chan;
divine::sync_mode_t sync_mode;
} chan;
};
};
struct dve_compiler: public dve_explicit_system_t
{
bool ltsmin;
......@@ -192,6 +214,10 @@ struct dve_compiler: public dve_explicit_system_t
void gen_state_struct();
void gen_initial_state();
void gen_state_info();
bool eq_expr(dve_expression_t*, dve_expression_t*);
int add_guard_expr(std::vector<guard> &guard, dve_expression_t* expr);
int add_guard_pc (std::vector<guard> &guard, divine::size_int_t gid, divine::size_int_t lid);
int add_guard_chan(std::vector<guard> &guard, divine::size_int_t chan, divine::sync_mode_t sync_mode);
void fill_transition_vector(std::vector<ext_transition_t>&);
void gen_transition_info();
......
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