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

Simplify ![*0] as [+].

Browse source 
* src/ltlast/unop.cc: Simplify ![*0] as 1[+].
* src/ltlast/unop.hh: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2010-10-14 18:38:28 +02:00
parent 437128b55b
commit d7781bc4d6
2 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ltlast/unop.cc
View file

@ -145,6 +145,11 @@ namespace spot
// !0 = 1 // !0 = 1
if (child == constant::false_instance()) if (child == constant::false_instance())
return constant::true_instance(); return constant::true_instance();
// ![*0] = 1[+]
if (child == constant::empty_word_instance())
return bunop::instance(bunop::Star,
constant::true_instance(), 1);
unop* u = dynamic_cast<unop*>(child); unop* u = dynamic_cast<unop*>(child);
if (u) if (u)
{ {
@ -155,6 +160,7 @@ namespace spot
u->destroy(); u->destroy();
return c; return c;
} }
// !Closure(Exp) = NegClosure(Exp)
if (u->op() == Closure) if (u->op() == Closure)
{ {
formula* c = unop::instance(NegClosure, formula* c = unop::instance(NegClosure,
@ -162,6 +168,7 @@ namespace spot
u->destroy(); u->destroy();
return c; return c;
} }
// !NegClosure(Exp) = Closure(Exp)
if (u->op() == NegClosure) if (u->op() == NegClosure)
{ {
formula* c = unop::instance(Closure, formula* c = unop::instance(Closure,

7
src/ltlast/unop.hh
View file

@ -29,6 +29,7 @@
#include <map> #include <map>
#include <iosfwd> #include <iosfwd>
#include "refformula.hh" #include "refformula.hh"
#include "bunop.hh"
namespace spot namespace spot
{ {
@ -65,6 +66,7 @@ namespace spot
/// - G([*0]) = 1 /// - G([*0]) = 1
/// - !1 = 0 /// - !1 = 0
/// - !0 = 1 /// - !0 = 1
/// - ![*0] = 1[+] (read below)
/// - !!Exp = Exp /// - !!Exp = Exp
/// - !Closure(Exp) = NegClosure(Exp) /// - !Closure(Exp) = NegClosure(Exp)
/// - !NegClosure(Exp) = Closure(Exp) /// - !NegClosure(Exp) = Closure(Exp)
@ -78,6 +80,11 @@ namespace spot
/// This rewriting implies that it is not possible to build an /// This rewriting implies that it is not possible to build an
/// LTL formula object that is SYNTACTICALLY equal to one of /// LTL formula object that is SYNTACTICALLY equal to one of
/// these left expressions. /// these left expressions.
///
/// Note that the "![*0]" form cannot be read using the PSL
/// grammar. Spot cannot read it either. However some
/// BDD-based algorithm may need to negate any constant, so we
/// handle this one as well.
static formula* instance(type op, formula* child); static formula* instance(type op, formula* child);
virtual void accept(visitor& v); virtual void accept(visitor& v);