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

Post rebase fixups.

Browse source 
* src/ltltest/randltl.cc: Document the -wf option.  Declare formula*
as const.  Simplify GF_n().
* src/tgbatest/ltl2tgba.cc: Suppress unused variable.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-26 12:26:20 +02:00
parent 84b1d24e8f
commit dcc809ff4a
2 changed files with 16 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/ltltest/randltl.cc
View file

@ -71,6 +71,7 @@ syntax(char* prog)
<< " -u generate unique formulae" << " -u generate unique formulae"
<< std::endl << std::endl
<< " -s N seed for the random number generator" << std::endl << " -s N seed for the random number generator" << std::endl
<< " -wf append weak fairness conditions to all formulae\n"
<< std::endl << std::endl
<< "Where:" << std::endl << "Where:" << std::endl
<< " F are floating values" << std::endl << " F are floating values" << std::endl
@ -97,26 +98,21 @@ to_int(const char* s)
// GF(p_1) & GF(p_2) & ... & GF(p_n) // GF(p_1) & GF(p_2) & ... & GF(p_n)
formula* GF_n(spot::ltl::atomic_prop_set* ap) const formula* GF_n(spot::ltl::atomic_prop_set* ap)
{ {
const formula* result = 0;
formula* result = 0;
multop::type op = multop::And;
spot::ltl::atomic_prop_set::const_iterator i = ap->begin(); spot::ltl::atomic_prop_set::const_iterator i = ap->begin();
while (i != ap->end()) while (i != ap->end())
{ {
std::ostringstream p; std::ostringstream p;
p << (*i)->name(); p << (*i)->name();
++i; ++i;
formula* f = unop::instance(unop::G, const formula* f =
unop::instance(unop::F, unop::instance(unop::G,
env.require(p.str()))); unop::instance(unop::F,
env.require(p.str())));
if (result) if (result)
result = multop::instance(op, f, result); result = multop::instance(multop::And, f, result);
else else
result = f; result = f;
} }
@ -140,7 +136,7 @@ main(int argc, char** argv)
bool opt_u = false; bool opt_u = false;
spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true); spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true);
spot::ltl::ltl_simplifier simp(simpopt); spot::ltl::ltl_simplifier simp(simpopt);
bool opt_wFair = false; bool opt_wfair = false;
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
@ -224,7 +220,7 @@ main(int argc, char** argv)
} }
else if (!strcmp(argv[argn], "-wf")) else if (!strcmp(argv[argn], "-wf"))
{ {
opt_wFair = true; opt_wfair = true;
} }
else else
{ {
@ -383,9 +379,10 @@ main(int argc, char** argv)
} }
} }
if (opt_wFair) if (opt_wfair)
{ {
spot::ltl::formula* g = GF_n(atomic_prop_collect(f, 0)); const spot::ltl::formula* g =
GF_n(atomic_prop_collect(f, 0));
f = spot::ltl::unop::instance(unop::Not, f = spot::ltl::unop::instance(unop::Not,
spot::ltl::binop::instance(binop::Implies, g, f)); spot::ltl::binop::instance(binop::Implies, g, f));
} }

2
src/tgbatest/ltl2tgba.cc
View file

@ -1154,8 +1154,6 @@ main(int argc, char** argv)
degeneralized = 0; degeneralized = 0;
if (degeneralize_opt != DegenSBA) if (degeneralize_opt != DegenSBA)
to_free = 0; to_free = 0;
aut_red = 0;
output = -1; output = -1;
} }
if (tgta_opt) if (tgta_opt)