alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes

Browse source 
to please sanity checks.
This commit is contained in:
Alexandre Duret-Lutz 2011-03-06 21:12:40 +01:00
parent 51e6989d91
commit 76cfd57973
3 changed files with 41 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes
to please sanity checks.
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Call divine to compile dve models. Call divine to compile dve models.

41
iface/dve2/dve2.cc
View file

@ -31,7 +31,8 @@
namespace spot namespace spot
{ {
namespace { namespace
{
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// DVE2 --ltsmin interface // DVE2 --ltsmin interface
@ -50,7 +51,7 @@ namespace spot
lt_dlhandle handle; // handle to the dynamic library lt_dlhandle handle; // handle to the dynamic library
void (*get_initial_state)(void *to); void (*get_initial_state)(void *to);
int (*have_property)(); int (*have_property)();
int (*get_successors)( void* m, int *in, TransitionCB, void *arg ); int (*get_successors)(void* m, int *in, TransitionCB, void *arg);
int (*get_state_variable_count)(); int (*get_state_variable_count)();
const char* (*get_state_variable_name)(int var); const char* (*get_state_variable_name)(int var);
@ -492,25 +493,37 @@ namespace spot
for (prop_set::const_iterator i = ps_->begin(); for (prop_set::const_iterator i = ps_->begin();
i != ps_->end(); ++i) i != ps_->end(); ++i)
{ {
int l = s->vars[(*i).var_num]; int l = s->vars[i->var_num];
int r = (*i).val; int r = i->val;
bool cond = false; bool cond = false;
switch ((*i).op) switch (i->op)
{ {
case OP_EQ: cond = (l == r); break; case OP_EQ:
case OP_NE: cond = (l != r); break; cond = (l == r);
case OP_LT: cond = (l < r); break; break;
case OP_GT: cond = (l > r); break; case OP_NE:
case OP_LE: cond = (l <= r); break; cond = (l != r);
case OP_GE: cond = (l >= r); break; break;
case OP_LT:
cond = (l < r);
break;
case OP_GT:
cond = (l > r);
break;
case OP_LE:
cond = (l <= r);
break;
case OP_GE:
cond = (l >= r);
break;
} }
if (cond) if (cond)
res &= bdd_ithvar((*i).bddvar); res &= bdd_ithvar(i->bddvar);
else else
res &= bdd_nithvar((*i).bddvar); res &= bdd_nithvar(i->bddvar);
} }
return res; return res;
} }
@ -694,7 +707,7 @@ namespace spot
d->get_state_variable_type_count = (int (*)()) d->get_state_variable_type_count = (int (*)())
lt_dlsym(h, "get_state_variable_type_count"); lt_dlsym(h, "get_state_variable_type_count");
d->get_state_variable_type_name = (const char* (*)(int)) d->get_state_variable_type_name = (const char* (*)(int))
lt_dlsym(h, "get_state_variable_type_name" ); lt_dlsym(h, "get_state_variable_type_name");
d->get_state_variable_type_value_count = (int (*)(int)) d->get_state_variable_type_value_count = (int (*)(int))
lt_dlsym(h, "get_state_variable_type_value_count"); lt_dlsym(h, "get_state_variable_type_value_count");
d->get_state_variable_type_value = (const char* (*)(int, int)) d->get_state_variable_type_value = (const char* (*)(int, int))

12
iface/dve2/dve2check.cc
View file

@ -100,9 +100,15 @@ main(int argc, char **argv)
case 'g': case 'g':
switch (opt[1]) switch (opt[1])
{ {
case 'm': output = DotModel; break; case 'm':
case 'p': output = DotProduct; break; output = DotModel;
case 'f': output = DotFormula; break; break;
case 'p':
output = DotProduct;
break;
case 'f':
output = DotFormula;
break;
default: default:
goto error; goto error;
} }