lbt: Do not write a trailing space.
* NEWS: Mention it. * src/ltlvisit/lbt.cc: Instead of outputting a space after each node, output one before each node but the first one.
This commit is contained in:
parent
bf3c3aecde
commit
3a5eec42de
2 changed files with 41 additions and 24 deletions
2
NEWS
2
NEWS
|
|
@ -13,6 +13,8 @@ New in spot 1.0a (not released):
|
||||||
(instead of binary operators) when placed in double quotes, but
|
(instead of binary operators) when placed in double quotes, but
|
||||||
on output they were output without quotes, making the result
|
on output they were output without quotes, making the result
|
||||||
unparsable.
|
unparsable.
|
||||||
|
- the to_lbt_string() functions would always output a trailing space.
|
||||||
|
This is not the case anymore.
|
||||||
- tgba_product::transition_annotation() would segfault when
|
- tgba_product::transition_annotation() would segfault when
|
||||||
called in a product against a Kripke structure.
|
called in a product against a Kripke structure.
|
||||||
* Minor improvements:
|
* Minor improvements:
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012 Laboratoire de Recherche et
|
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
|
||||||
// Développement de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -46,12 +46,24 @@ namespace spot
|
||||||
|
|
||||||
class lbt_visitor: public visitor
|
class lbt_visitor: public visitor
|
||||||
{
|
{
|
||||||
|
protected:
|
||||||
|
std::ostream& os_;
|
||||||
|
bool first_;
|
||||||
public:
|
public:
|
||||||
|
|
||||||
lbt_visitor(std::ostream& os)
|
lbt_visitor(std::ostream& os)
|
||||||
: os_(os)
|
: os_(os), first_(true)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void blank()
|
||||||
|
{
|
||||||
|
if (first_)
|
||||||
|
first_ = false;
|
||||||
|
else
|
||||||
|
os_ << ' ';
|
||||||
|
}
|
||||||
|
|
||||||
virtual
|
virtual
|
||||||
~lbt_visitor()
|
~lbt_visitor()
|
||||||
{
|
{
|
||||||
|
|
@ -60,23 +72,25 @@ namespace spot
|
||||||
void
|
void
|
||||||
visit(const atomic_prop* ap)
|
visit(const atomic_prop* ap)
|
||||||
{
|
{
|
||||||
|
blank();
|
||||||
std::string str = ap->name();
|
std::string str = ap->name();
|
||||||
if (!is_pnum(str.c_str()))
|
if (!is_pnum(str.c_str()))
|
||||||
os_ << '"' << str << "\" ";
|
os_ << '"' << str << '"';
|
||||||
else
|
else
|
||||||
os_ << str << ' ';
|
os_ << str;
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
visit(const constant* c)
|
visit(const constant* c)
|
||||||
{
|
{
|
||||||
|
blank();
|
||||||
switch (c->val())
|
switch (c->val())
|
||||||
{
|
{
|
||||||
case constant::False:
|
case constant::False:
|
||||||
os_ << "f ";
|
os_ << "f";
|
||||||
break;
|
break;
|
||||||
case constant::True:
|
case constant::True:
|
||||||
os_ << "t ";
|
os_ << "t";
|
||||||
break;
|
break;
|
||||||
case constant::EmptyWord:
|
case constant::EmptyWord:
|
||||||
assert(!"unsupported constant");
|
assert(!"unsupported constant");
|
||||||
|
|
@ -87,28 +101,29 @@ namespace spot
|
||||||
void
|
void
|
||||||
visit(const binop* bo)
|
visit(const binop* bo)
|
||||||
{
|
{
|
||||||
|
blank();
|
||||||
switch (bo->op())
|
switch (bo->op())
|
||||||
{
|
{
|
||||||
case binop::Xor:
|
case binop::Xor:
|
||||||
os_ << "^ ";
|
os_ << "^";
|
||||||
break;
|
break;
|
||||||
case binop::Implies:
|
case binop::Implies:
|
||||||
os_ << "i ";
|
os_ << "i";
|
||||||
break;
|
break;
|
||||||
case binop::Equiv:
|
case binop::Equiv:
|
||||||
os_ << "e ";
|
os_ << "e";
|
||||||
break;
|
break;
|
||||||
case binop::U:
|
case binop::U:
|
||||||
os_ << "U ";
|
os_ << "U";
|
||||||
break;
|
break;
|
||||||
case binop::R:
|
case binop::R:
|
||||||
os_ << "V ";
|
os_ << "V";
|
||||||
break;
|
break;
|
||||||
case binop::W:
|
case binop::W:
|
||||||
os_ << "W ";
|
os_ << "W";
|
||||||
break;
|
break;
|
||||||
case binop::M:
|
case binop::M:
|
||||||
os_ << "M ";
|
os_ << "M";
|
||||||
break;
|
break;
|
||||||
case binop::UConcat:
|
case binop::UConcat:
|
||||||
case binop::EConcat:
|
case binop::EConcat:
|
||||||
|
|
@ -129,19 +144,20 @@ namespace spot
|
||||||
void
|
void
|
||||||
visit(const unop* uo)
|
visit(const unop* uo)
|
||||||
{
|
{
|
||||||
|
blank();
|
||||||
switch (uo->op())
|
switch (uo->op())
|
||||||
{
|
{
|
||||||
case unop::Not:
|
case unop::Not:
|
||||||
os_ << "! ";
|
os_ << "!";
|
||||||
break;
|
break;
|
||||||
case unop::X:
|
case unop::X:
|
||||||
os_ << "X ";
|
os_ << "X";
|
||||||
break;
|
break;
|
||||||
case unop::F:
|
case unop::F:
|
||||||
os_ << "F ";
|
os_ << "F";
|
||||||
break;
|
break;
|
||||||
case unop::G:
|
case unop::G:
|
||||||
os_ << "G ";
|
os_ << "G";
|
||||||
break;
|
break;
|
||||||
case unop::Finish:
|
case unop::Finish:
|
||||||
case unop::Closure:
|
case unop::Closure:
|
||||||
|
|
@ -182,15 +198,14 @@ namespace spot
|
||||||
|
|
||||||
unsigned n = mo->size();
|
unsigned n = mo->size();
|
||||||
for (unsigned i = n - 1; i != 0; --i)
|
for (unsigned i = n - 1; i != 0; --i)
|
||||||
os_ << o << ' ';
|
{
|
||||||
|
blank();
|
||||||
|
os_ << o;
|
||||||
|
}
|
||||||
|
|
||||||
for (unsigned i = 0; i < n; ++i)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
{
|
|
||||||
mo->nth(i)->accept(*this);
|
mo->nth(i)->accept(*this);
|
||||||
}
|
}
|
||||||
}
|
|
||||||
protected:
|
|
||||||
std::ostream& os_;
|
|
||||||
};
|
};
|
||||||
|
|
||||||
} // anonymous
|
} // anonymous
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue