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

* src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-01-23 13:01:43 +00:00
parent 4b4b640ec4
commit e73ce85cfc
2 changed files with 11 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2004-01-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments.
2004-01-13 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-01-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* configure.ac, NEWS: Bump version to 0.0o. * configure.ac, NEWS: Bump version to 0.0o.

11
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -40,8 +40,8 @@ namespace spot
namespace namespace
{ {
// Helper dictionary. We represent formula using a BDD to simplify // Helper dictionary. We represent formulae using BDDs to
// them, and them translate the BDD back into formulae. // simplify them, and then translate BDDs back into formulae.
// //
// The name of the variables are inspired from Couvreur's FM paper. // The name of the variables are inspired from Couvreur's FM paper.
// "a" variables are promises (written "a" in the paper) // "a" variables are promises (written "a" in the paper)
@ -323,7 +323,7 @@ namespace spot
{ {
const formula* child = node->child(); const formula* child = node->child();
int x = dict_.register_next_variable(node); int x = dict_.register_next_variable(node);
// GFy is pretty frequent and easy to optimize, to we // GFy is pretty frequent and easy to optimize, so we
// want to detect it. // want to detect it.
const unop* Fy = dynamic_cast<const unop*>(child); const unop* Fy = dynamic_cast<const unop*>(child);
if (Fy && Fy->op() == unop::F) if (Fy && Fy->op() == unop::F)
@ -344,11 +344,13 @@ namespace spot
} }
case unop::Not: case unop::Not:
{ {
// r(!y) = !r(y)
res_ = bdd_not(recurse(node->child())); res_ = bdd_not(recurse(node->child()));
return; return;
} }
case unop::X: case unop::X:
{ {
// r(Xy) = Next[y]
int x = dict_.register_next_variable(node->child()); int x = dict_.register_next_variable(node->child());
res_ = bdd_ithvar(x); res_ = bdd_ithvar(x);
return; return;
@ -366,6 +368,7 @@ namespace spot
switch (node->op()) switch (node->op())
{ {
// r(f1 logical-op f2) = r(f1) logical-op r(f2)
case binop::Xor: case binop::Xor:
res_ = bdd_apply(f1, f2, bddop_xor); res_ = bdd_apply(f1, f2, bddop_xor);
return; return;