From 76cfd5797323a8d70d6f9b3004de7f6c8ebc54e3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 6 Mar 2011 21:12:40 +0100 Subject: [PATCH] * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes to please sanity checks. --- ChangeLog | 5 +++++ iface/dve2/dve2.cc | 41 +++++++++++++++++++++++++++-------------- iface/dve2/dve2check.cc | 12 +++++++++--- 3 files changed, 41 insertions(+), 17 deletions(-) diff --git a/ChangeLog b/ChangeLog index 563819c0a..ba4532115 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2011-03-06 Alexandre Duret-Lutz + + * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes + to please sanity checks. + 2011-03-06 Alexandre Duret-Lutz Call divine to compile dve models. diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 55b9ab9ab..96e1d024b 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -31,7 +31,8 @@ namespace spot { - namespace { + namespace + { //////////////////////////////////////////////////////////////////////// // DVE2 --ltsmin interface @@ -50,7 +51,7 @@ namespace spot lt_dlhandle handle; // handle to the dynamic library void (*get_initial_state)(void *to); 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)(); const char* (*get_state_variable_name)(int var); @@ -492,25 +493,37 @@ namespace spot for (prop_set::const_iterator i = ps_->begin(); i != ps_->end(); ++i) { - int l = s->vars[(*i).var_num]; - int r = (*i).val; + int l = s->vars[i->var_num]; + int r = i->val; bool cond = false; - switch ((*i).op) + switch (i->op) { - case OP_EQ: cond = (l == r); break; - case OP_NE: cond = (l != r); 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; + case OP_EQ: + cond = (l == r); + break; + case OP_NE: + cond = (l != r); + 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) - res &= bdd_ithvar((*i).bddvar); + res &= bdd_ithvar(i->bddvar); else - res &= bdd_nithvar((*i).bddvar); + res &= bdd_nithvar(i->bddvar); } return res; } @@ -694,7 +707,7 @@ namespace spot d->get_state_variable_type_count = (int (*)()) lt_dlsym(h, "get_state_variable_type_count"); 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)) lt_dlsym(h, "get_state_variable_type_value_count"); d->get_state_variable_type_value = (const char* (*)(int, int)) diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index 2985aae6f..37cbd0f63 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -100,9 +100,15 @@ main(int argc, char **argv) case 'g': switch (opt[1]) { - case 'm': output = DotModel; break; - case 'p': output = DotProduct; break; - case 'f': output = DotFormula; break; + case 'm': + output = DotModel; + break; + case 'p': + output = DotProduct; + break; + case 'f': + output = DotFormula; + break; default: goto error; }