Skip to content
GitLab
Commit 87ac63e7 authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Completed DiVinE / SPIN LTL semantics for deadlocks. 

Added LTSmin semantics under -L (io -l).
(Closes #552)
parent 35208c28
Hide whitespace changes
Inline Side-by-side
tools/compile.h
View file @ 87ac63e7
......@@ -16,6 +16,8 @@ using namespace wibble;
struct Compile {
commandline::BoolOption *o_ltsmin;
commandline::BoolOption *o_ltsmin_ltl;
commandline::BoolOption *o_textbook;
commandline::Engine *cmd_compile;
commandline::StandardParserWithMandatoryCommand &opts;
......@@ -55,8 +57,13 @@ struct Compile {
run( cmd.str() );
}
void compileDve( std::string in, bool ltsmin ) {
dve_compiler compiler(ltsmin);
void compileDve( std::string in, bool ltsmin, bool ltsmin_ltl,
bool textbook ) {
if (textbook)
die( "Textbook LTL semantics not yet implemented." );
if (ltsmin && ltsmin_ltl)
die( "Use -l OR -L." );
dve_compiler compiler(ltsmin || ltsmin_ltl, ltsmin_ltl);
compiler.read( in.c_str() );
compiler.analyse();
......@@ -82,7 +89,8 @@ struct Compile {
if ( access( input.c_str(), R_OK ) )
die( "FATAL: cannot open input file " + input + " for reading" );
if ( str::endsWith( input, ".dve" ) ) {
compileDve( input, o_ltsmin->boolValue() );
compileDve( input, o_ltsmin->boolValue(), o_ltsmin_ltl->boolValue(),
o_textbook->boolValue() );
#ifdef HAVE_MURPHI
} else if ( str::endsWith( input, ".m" ) ) {
compileMurphi( input );
......@@ -101,6 +109,12 @@ struct Compile {
o_ltsmin = cmd_compile->add< commandline::BoolOption >(
"ltsmin", 'l', "ltsmin", "",
"ltsmin interface" );
o_ltsmin_ltl = cmd_compile->add< commandline::BoolOption >(
"ltsmin", 'L', "LTSmin", "",
"ltsmin interface with LTSmin LTL semantics" );
o_textbook = cmd_compile->add< commandline::BoolOption >(
"textbook", 't', "textbook", "",
"ltsmin interface with textbook LTL semantics" );
}
......
tools/dvecompile.cpp
View file @ 87ac63e7
......@@ -137,6 +137,7 @@ std::string dve_compiler::cexpr( dve_expression_t & expr, std::string state )
void dve_compiler::gen_header()
{
line( "#include <stdlib.h>" );
line( "#include <stdio.h>" );
line( "#include <string.h>" );
line( "#include <stdint.h>" );
......@@ -1112,7 +1113,7 @@ void dve_compiler::gen_successors()
block_begin();
new_output_state();
transition_effect( &*iter_ext_transition_vector, in, out );
if (!ltsmin) line( "system_in_deadlock = false;" );
line( "system_in_deadlock = false;" );
yield_state();
block_end();
}
......@@ -1122,36 +1123,35 @@ void dve_compiler::gen_successors()
}
block_end();
if (!ltsmin)
{
new_label();
if (ltsmin_ltl) return;
if_begin( true );
if_clause( "system_in_deadlock" );
if_end(); block_begin();
new_label();
for(iter_property_transitions = property_transitions.begin();
iter_property_transitions != property_transitions.end();
iter_property_transitions++)
{
new_label();
if_begin( false );
if_begin( true );
if_clause( "system_in_deadlock" );
if_end(); block_begin();
if_clause( in_state( (*iter_property_transitions)->get_process_gid(),
(*iter_property_transitions)->get_state1_lid(), in ) );
if_cexpr_clause( (*iter_property_transitions)->get_guard(), in );
for(iter_property_transitions = property_transitions.begin();
iter_property_transitions != property_transitions.end();
iter_property_transitions++)
{
new_label();
if_begin( false );
if_end(); block_begin();
new_output_state();
if_clause( in_state( (*iter_property_transitions)->get_process_gid(),
(*iter_property_transitions)->get_state1_lid(), in ) );
if_cexpr_clause( (*iter_property_transitions)->get_guard(), in );
assign( process_state( (*iter_property_transitions)->get_process_gid(), out ),
fmt( (*iter_property_transitions)->get_state2_lid() ) );
if_end(); block_begin();
new_output_state();
yield_state();
block_end();
}
assign( process_state( (*iter_property_transitions)->get_process_gid(), out ),
fmt( (*iter_property_transitions)->get_state2_lid() ) );
yield_state();
block_end();
}
block_end();
}
void dve_compiler::gen_is_accepting()
......@@ -1233,6 +1233,7 @@ void dve_compiler::print_generator()
block_begin();
for(int i=0; i < current_label; i++)
line( "case " + fmt( i ) + ": goto l" + fmt( i ) + ";" );
line( "default: printf (\"Wrong group! Using greybox/long call + -l (DiVinE LTL semantics)? This combo is not implemented.\"); exit (-1);" );
block_end();
line("return 0;");
// end switch block
......@@ -1245,6 +1246,7 @@ void dve_compiler::print_generator()
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 ) " );
block_begin();
line( "(void)model; // ignore model" );
line( "bool system_in_deadlock = true;" );
line( "transition_info_t transition_info = { NULL, -1 };" );
line( "int states_emitted = 0;" );
line( "state_struct_t tmp;" );
......@@ -1740,6 +1742,7 @@ void dve_compiler::fill_transition_vector(std::vector<ext_transition_t>& transit
// store transition in map
ext_transition_t tmp = *iter_ext_transition_vector;
tmp.commited = 1;
tmp.buchi = 0;
transitions.push_back(tmp);
trans_count++;
}
......@@ -1768,12 +1771,29 @@ void dve_compiler::fill_transition_vector(std::vector<ext_transition_t>& transit
{
ext_transition_t tmp = *iter_ext_transition_vector;
tmp.commited = 0;
tmp.buchi = 0;
transitions.push_back(tmp);
trans_count++;
}
}
}
}
if (have_property && !ltsmin_ltl) {
for(iter_property_transitions = property_transitions.begin();
iter_property_transitions != property_transitions.end();
iter_property_transitions++)
{
ext_transition_t ext_transition;
ext_transition.synchronized = false;
ext_transition.first = *iter_property_transitions;
ext_transition.property = *iter_property_transitions;
ext_transition.buchi = 1;
analyse_transition_dependencies(ext_transition);
transitions.push_back(ext_transition);
trans_count++;
}
}
}
bool dve_compiler::split_conjunctive_expression(std::vector<guard>& guard, dve_expression_t* expr)
......@@ -1877,6 +1897,142 @@ void dve_compiler::gen_transition_info()
state_creator_t::PROCESS_STATE, -1, c_base_sv_read);
}
/////////////////////////////////
// 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()) {
// try splitting the first guard
std::vector<struct guard> gtmp;
if (split_conjunctive_expression(gtmp, current.first->get_guard())) {
// merge dependent guards again
merge_dependent_expression(gtmp, sv_count);
// add all split guards
for(int j=0; j<gtmp.size(); j++) {
g = add_guard_expr(guard, gtmp[j].expr.guard);
gs.insert(g);
}
} else {
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()) {
// try splitting the second guard
std::vector<struct guard> gtmp;
if (split_conjunctive_expression(gtmp, current.second->get_guard())) {
// merge dependent guards again
merge_dependent_expression(gtmp, sv_count);
// add all split guards
for(int j=0; j<gtmp.size(); j++) {
g = add_guard_expr(guard, gtmp[j].expr.guard);
gs.insert(g);
}
} else {
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);
}
}
}
// extract dependency matrix per guard expression
std::vector< std::vector<int> > guard_matrix;
guard_matrix.resize(guard.size());
for(int i=0; i<guard.size(); i++) {
std::vector<int> &per_guard_matrix = guard_matrix[i];
// clear per guard matrix
per_guard_matrix.resize(sv_count);
per_guard_matrix.clear();
switch(guard[i].type) {
case GUARD_PC:
mark_dependency(guard[i].pc.gid,
state_creator_t::PROCESS_STATE, -1, per_guard_matrix);
break;
case GUARD_EXPR: {
// 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);
analyse_expression(*guard[i].expr.guard, et, et.sv_read);
per_guard_matrix = et.sv_read;
} break;
case GUARD_CHAN:
mark_dependency(guard[i].chan.chan,
state_creator_t::CHANNEL_BUFFER, -1, per_guard_matrix);
break;
case GUARD_COMMITED_FIRST:
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))
mark_dependency(p, state_creator_t::PROCESS_STATE, -1, per_guard_matrix);
break;
default:
for(int j=0; j<sv_count; j++) per_guard_matrix[j]=1;
break;
}
}
// buchi transits on deadlocks, hence also depends on all other guards!
for(size_int_t i = 0; i < transitions.size(); i++) {
ext_transition_t& current = transitions[i];
set<int>& gs = guards[i];
if (current.buchi)
for(size_int_t j = 0; j < transitions.size(); j++) {
ext_transition_t& current2 = transitions[j];
set<int>& gs2 = guards[j];
if (!current2.buchi) {
gs.insert(gs2.begin(), gs2.end());
}
}
}
// output transition vectors
snprintf(buf, BUFLEN, "int transition_dependency[][2][%d] = ", sv_count);
line(buf);
......@@ -1889,8 +2045,19 @@ 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.commited?current.sv_read[j]:max(c_base_sv_read[j], current.sv_read[j])) );
append(buf);
int dep = current.commited?current.sv_read[j]:max(c_base_sv_read[j], current.sv_read[j]);
if (!dep && current.buchi) { // use guard info
set<int> &gs = guards[i];
for(set<int>::iterator ix = gs.begin(); ix != gs.end(); ix++) {
std::vector<int> &per_guard_matrix = guard_matrix[*ix];
if (per_guard_matrix[j]) {
dep = 1;
break;
}
}
}
snprintf(buf, BUFLEN, "%s%d", ((j==0)?"":","), dep);
append(buf);
}
append("},{" );
for(size_int_t j = 0; j < sv_count; j++)
......@@ -1985,88 +2152,6 @@ void dve_compiler::gen_transition_info()
line("return;");
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()) {
// try splitting the first guard
std::vector<struct guard> gtmp;
if (split_conjunctive_expression(gtmp, current.first->get_guard())) {
// merge dependent guards again
merge_dependent_expression(gtmp, sv_count);
// add all split guards
for(int j=0; j<gtmp.size(); j++) {
g = add_guard_expr(guard, gtmp[j].expr.guard);
gs.insert(g);
}
} else {
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()) {
// try splitting the second guard
std::vector<struct guard> gtmp;
if (split_conjunctive_expression(gtmp, current.second->get_guard())) {
// merge dependent guards again
merge_dependent_expression(gtmp, sv_count);
// add all split guards
for(int j=0; j<gtmp.size(); j++) {
g = add_guard_expr(guard, gtmp[j].expr.guard);
gs.insert(g);
}
} else {
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\" int get_guard(void* model, int g, state_struct_t* src) " );
......@@ -2203,44 +2288,11 @@ void dve_compiler::gen_transition_info()
// EXPORT THE GUARD MATRIX //
/////////////////////////////////
// extract dependency matrix per guard expression
std::vector<int> per_guard_matrix;
snprintf(buf, BUFLEN, "int guard[][%d] = ", sv_count);
line(buf);
block_begin();
for(int i=0; i<guard.size(); i++) {
// clear per guard matrix
per_guard_matrix.clear();
per_guard_matrix.resize(sv_count);
switch(guard[i].type) {
case GUARD_PC:
mark_dependency(guard[i].pc.gid,
state_creator_t::PROCESS_STATE, -1, per_guard_matrix);
break;
case GUARD_EXPR: {
// 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);
analyse_expression(*guard[i].expr.guard, et, et.sv_read);
per_guard_matrix = et.sv_read;
} break;
case GUARD_CHAN:
mark_dependency(guard[i].chan.chan,
state_creator_t::CHANNEL_BUFFER, -1, per_guard_matrix);
break;
case GUARD_COMMITED_FIRST:
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))
mark_dependency(p, state_creator_t::PROCESS_STATE, -1, per_guard_matrix);
break;
default:
for(int j=0; j<sv_count; j++) per_guard_matrix[j]=1;
break;
}
std::vector<int> &per_guard_matrix = guard_matrix[i];
if (i != 0) { line(","); }
append("{" );
// guard
......
tools/dvecompile.h
View file @ 87ac63e7
......@@ -16,6 +16,7 @@ struct ext_transition_t
{
int synchronized;
int commited; // used for ltsmin
int buchi; // used for ltsmin
dve_transition_t *first;
dve_transition_t *second; // only when first transition is synchronized;
dve_transition_t *property; // transition of property automaton
......@@ -55,7 +56,8 @@ struct simple_predicate
struct dve_compiler: public dve_explicit_system_t
{
bool ltsmin;
bool ltsmin; // LTSmin successor generator
bool ltsmin_ltl; // divine LTL semantics in LTsmin successor generator
bool many;
int current_label;
......@@ -94,8 +96,8 @@ struct dve_compiler: public dve_explicit_system_t
outline();
}
dve_compiler(bool ltsmin, error_vector_t & evect=gerr)
: explicit_system_t(evect), dve_explicit_system_t(evect), current_label(0), m_indent( 0 ), ltsmin(ltsmin)
dve_compiler(bool ltsmin, bool ltsmin_ltl, error_vector_t & evect=gerr)
: explicit_system_t(evect), dve_explicit_system_t(evect), current_label(0), m_indent( 0 ), ltsmin(ltsmin), ltsmin_ltl(ltsmin_ltl)
{}
virtual ~dve_compiler() {}
......
Supports Markdown
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