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

formula: rename the constants for consistency

Browse source 
False/True are problematic in Python, and I don't like that the
enum is op::False but the constructor formula::ff().  So let's
just use ff and tt everywhere, and also eword instead of EmptyWord.

* src/ltlast/formula.hh (False, True, EmptyWord, AP, is_false, is_true):
Rename to...
(ff, tt, eword, ap, is_ff, is_tt): ... these.
* iface/ltsmin/ltsmin.cc, src/ltlast/formula.cc,
src/ltlvisit/apcollect.cc, src/ltlvisit/dot.cc, src/ltlvisit/mark.cc,
src/ltlvisit/mutation.cc, src/ltlvisit/print.cc,
src/ltlvisit/relabel.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc, src/ltlvisit/unabbrev.cc,
src/twa/acc.cc, src/twa/acc.hh, src/twa/formula2bdd.cc,
src/twaalgos/gtec/gtec.cc, src/twaalgos/hoa.cc, src/twaalgos/ltl2taa.cc,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/neverclaim.cc,
src/twaalgos/product.cc, src/twaalgos/remfin.cc, src/twaalgos/safety.cc,
src/tests/parseerr.test, src/tests/utf8.test, wrap/python/spot.py:
Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-09-27 22:47:17 +02:00
parent fad05632a2
commit 8b4ec5ded0
27 changed files with 211 additions and 211 deletions
Download patch file Download diff file Expand all files Collapse all files

4
iface/ltsmin/ltsmin.cc
View file

@ -647,12 +647,12 @@ namespace spot
// appropriately. ALIVE_PROP is the bdd that should be ANDed
// to all transitions leaving a live state, while DEAD_PROP should
// be ANDed to all transitions leaving a dead state.
if (dead.is_false())
if (dead.is_ff())
{
alive_prop = bddtrue;
dead_prop = bddfalse;
}
else if (dead.is_true())
else if (dead.is_tt())
{
alive_prop = bddtrue;
dead_prop = bddtrue;

106
src/ltlast/formula.cc
View file

@ -138,7 +138,7 @@ namespace spot
void
fnode::destroy_aux() const
{
if (SPOT_UNLIKELY(is(op::AP)))
if (SPOT_UNLIKELY(is(op::ap)))
{
auto i = m.ap2name.find(id());
auto n = m.name2ap.erase(i->second);
@ -165,10 +165,10 @@ namespace spot
case op::x: \
return #x; \
break
C(False);
C(True);
C(EmptyWord);
C(AP);
C(ff);
C(tt);
C(eword);
C(ap);
C(Not);
C(X);
C(F);
@ -618,7 +618,7 @@ namespace spot
// - 0[*min..max] = 0 if min > 0
// - b[:*0..max] = 1
// - b[:*min..max] = 0 if min > 0
if (child->is_false()
if (child->is_ff()
|| (o == op::FStar && child->is_boolean()))
{
if (min == 0)
@ -709,7 +709,7 @@ namespace spot
// F(0) = G(0) = 0
// F(1) = G(1) = 1
if (f->is_false() || f->is_true())
if (f->is_ff() || f->is_tt())
return f;
assert(!f->is_eword());
@ -719,10 +719,10 @@ namespace spot
case op::Not:
{
// !1 = 0
if (f->is_true())
if (f->is_tt())
return ff();
// !0 = 1
if (f->is_false())
if (f->is_ff())
return tt();
// ![*0] = 1[+]
if (f->is_eword())
@ -754,7 +754,7 @@ namespace spot
}
case op::X:
// X(1) = 1, X(0) = 0
if (f->is_true() || f->is_false())
if (f->is_tt() || f->is_ff())
return f;
assert(!f->is_eword());
break;
@ -771,10 +771,10 @@ namespace spot
case op::NegClosure:
case op::NegClosureMarked:
// {1} = 0
if (f->is_true())
if (f->is_tt())
return ff();
// {0} = 1, {[*0]} = 1
if (f->is_false() || f->is_eword())
if (f->is_ff() || f->is_eword())
return tt();
// {b} = !b
if (f->is_boolean())
@ -806,9 +806,9 @@ namespace spot
}
// - (1 ^ Exp) = !Exp
// - (0 ^ Exp) = Exp
if (first->is_true())
if (first->is_tt())
return unop(op::Not, second);
if (first->is_false())
if (first->is_ff())
return second;
if (first == second)
{
@ -830,9 +830,9 @@ namespace spot
// - (0 <=> Exp) = !Exp
// - (1 <=> Exp) = Exp
// - (Exp <=> Exp) = 1
if (first->is_false())
if (first->is_ff())
return unop(op::Not, second);
if (first->is_true())
if (first->is_tt())
return second;
if (first == second)
{
@ -850,19 +850,19 @@ namespace spot
// - (Exp => 1) = 1
// - (Exp => 0) = !Exp
// - (Exp => Exp) = 1
if (first->is_true())
if (first->is_tt())
return second;
if (first->is_false())
if (first->is_ff())
{
second->destroy();
return tt();
}
if (second->is_true())
if (second->is_tt())
{
first->destroy();
return second;
}
if (second->is_false())
if (second->is_ff())
return unop(op::Not, first);
if (first == second)
{
@ -876,9 +876,9 @@ namespace spot
// - (Exp U 0) = 0
// - (0 U Exp) = Exp
// - (Exp U Exp) = Exp
if (second->is_true()
|| second->is_false()
|| first->is_false()
if (second->is_tt()
|| second->is_ff()
|| first->is_ff()
|| first == second)
{
first->destroy();
@ -890,14 +890,14 @@ namespace spot
// - (0 W Exp) = Exp
// - (1 W Exp) = 1
// - (Exp W Exp) = Exp
if (second->is_true()
|| first->is_false()
if (second->is_tt()
|| first->is_ff()
|| first == second)
{
first->destroy();
return second;
}
if (first->is_true())
if (first->is_tt())
{
second->destroy();
return first;
@ -908,9 +908,9 @@ namespace spot
// - (Exp R 0) = 0
// - (1 R Exp) = Exp
// - (Exp R Exp) = Exp
if (second->is_true()
|| second->is_false()
|| first->is_true()
if (second->is_tt()
|| second->is_ff()
|| first->is_tt()
|| first == second)
{
first->destroy();
@ -922,14 +922,14 @@ namespace spot
// - (1 M Exp) = Exp
// - (0 M Exp) = 0
// - (Exp M Exp) = Exp
if (second->is_false()
|| first->is_true()
if (second->is_ff()
|| first->is_tt()
|| first == second)
{
first->destroy();
return second;
}
if (first->is_false())
if (first->is_ff())
{
second->destroy();
return first;
@ -942,15 +942,15 @@ namespace spot
// - [*0] <>-> Exp = 0
// - Exp <>-> 0 = 0
// - boolExp <>-> Exp = boolExp & Exp
if (first->is_true())
if (first->is_tt())
return second;
if (first->is_false()
if (first->is_ff()
|| first->is_eword())
{
second->destroy();
return ff();
}
if (second->is_false())
if (second->is_ff())
{
first->destroy();
return second;
@ -964,15 +964,15 @@ namespace spot
// - [*0] []-> Exp = 1
// - Exp []-> 1 = 1
// - boolExp []-> Exp = !boolExp | Exp
if (first->is_true())
if (first->is_tt())
return second;
if (first->is_false()
if (first->is_ff()
|| first->is_eword())
{
second->destroy();
return tt();
}
if (second->is_true())
if (second->is_tt())
{
first->destroy();
return second;
@ -1000,13 +1000,13 @@ namespace spot
m.ap2name.emplace(next_id_, name);
// next_id_ is incremented by setup_props(), called by the
// constructor of fnode
return ires.first->second = new fnode(op::AP, {});
return ires.first->second = new fnode(op::ap, {});
}
const std::string&
fnode::ap_name() const
{
if (op_ != op::AP)
if (op_ != op::ap)
throw std::runtime_error("ap_name() called on non-AP formula");
auto i = m.ap2name.find(id());
assert(i != m.ap2name.end());
@ -1014,9 +1014,9 @@ namespace spot
}
size_t fnode::next_id_ = 0U;
const fnode* fnode::ff_ = new fnode(op::False, {});
const fnode* fnode::tt_ = new fnode(op::True, {});
const fnode* fnode::ew_ = new fnode(op::EmptyWord, {});
const fnode* fnode::ff_ = new fnode(op::ff, {});
const fnode* fnode::tt_ = new fnode(op::tt, {});
const fnode* fnode::ew_ = new fnode(op::eword, {});
const fnode* fnode::one_star_ = nullptr; // Only built when necessary.
void fnode::setup_props(op o)
@ -1032,8 +1032,8 @@ namespace spot
switch (op_)
{
case op::False:
case op::True:
case op::ff:
case op::tt:
is_.boolean = true;
is_.sugar_free_boolean = true;
is_.in_nenoform = true;
@ -1055,7 +1055,7 @@ namespace spot
is_.lbt_atomic_props = true;
is_.spin_atomic_props = true;
break;
case op::EmptyWord:
case op::eword:
is_.boolean = false;
is_.sugar_free_boolean = false;
is_.in_nenoform = true;
@ -1077,7 +1077,7 @@ namespace spot
is_.lbt_atomic_props = true;
is_.spin_atomic_props = true;
break;
case op::AP:
case op::ap:
is_.boolean = true;
is_.sugar_free_boolean = true;
is_.in_nenoform = true;
@ -1119,7 +1119,7 @@ namespace spot
is_.not_marked = true;
is_.eventual = children[0]->is_universal();
is_.universal = children[0]->is_eventual();
is_.in_nenoform = (children[0]->is(op::AP));
is_.in_nenoform = (children[0]->is(op::ap));
is_.sere_formula = is_.boolean;
is_.syntactic_safety = children[0]->is_syntactic_guarantee();
@ -1336,7 +1336,7 @@ namespace spot
is_.not_marked = true;
// f U g is universal if g is eventual, or if f == 1.
is_.eventual = children[1]->is_eventual();
is_.eventual |= children[0]->is_true();
is_.eventual |= children[0]->is_tt();
is_.boolean = false;
is_.sere_formula = false;
is_.finite = false;
@ -1357,7 +1357,7 @@ namespace spot
props = children[0]->props & children[1]->props;
is_.not_marked = true;
// f W g is universal if f and g are, or if g == 0.
is_.universal |= children[1]->is_false();
is_.universal |= children[1]->is_ff();
is_.boolean = false;
is_.sere_formula = false;
is_.finite = false;
@ -1380,7 +1380,7 @@ namespace spot
is_.not_marked = true;
// g R f is universal if f is universal, or if g == 0.
is_.universal = children[1]->is_universal();
is_.universal |= children[0]->is_false();
is_.universal |= children[0]->is_ff();
is_.boolean = false;
is_.sere_formula = false;
is_.finite = false;
@ -1402,7 +1402,7 @@ namespace spot
props = children[0]->props & children[1]->props;
is_.not_marked = true;
// g M f is eventual if both g and f are eventual, or if f == 1.
is_.eventual |= children[1]->is_true();
is_.eventual |= children[1]->is_tt();
is_.boolean = false;
is_.sere_formula = false;
is_.finite = false;
@ -1585,7 +1585,7 @@ namespace spot
if (m != unbounded())
os << +m;
}
if (op_ == op::AP)
if (op_ == op::ap)
os << " \"" << ap_name() << '"';
if (auto s = size())
{

40
src/ltlast/formula.hh
View file

@ -41,10 +41,10 @@ namespace spot
{
enum class op: uint8_t
{
False,
True,
EmptyWord,
AP,
ff,
tt,
eword,
ap,
// unary operators
Not,
X,
@ -210,9 +210,9 @@ namespace spot
return ff_;
}
bool is_false() const
bool is_ff() const
{
return op_ == op::False;
return op_ == op::ff;
}
static const fnode* tt()
@ -220,9 +220,9 @@ namespace spot
return tt_;
}
bool is_true() const
bool is_tt() const
{
return op_ == op::True;
return op_ == op::tt;
}
static const fnode* eword()
@ -232,12 +232,12 @@ namespace spot
bool is_eword() const
{
return op_ == op::EmptyWord;
return op_ == op::eword;
}
bool is_constant() const
{
return op_ == op::False || op_ == op::True || op_ == op::EmptyWord;
return op_ == op::ff || op_ == op::tt || op_ == op::eword;
}
bool is_Kleene_star() const
@ -579,7 +579,7 @@ namespace spot
{
if (f->is(op::Not))
f = f->nth(0);
if (f->is(op::AP))
if (f->is(op::ap))
return f;
return nullptr;
};
@ -1088,9 +1088,9 @@ namespace spot
return formula(fnode::ff());
}
bool is_false() const
bool is_ff() const
{
return ptr_->is_false();
return ptr_->is_ff();
}
static formula tt()
@ -1098,9 +1098,9 @@ namespace spot
return formula(fnode::tt());
}
bool is_true() const
bool is_tt() const
{
return ptr_->is_true();
return ptr_->is_tt();
}
static formula eword()
@ -1130,7 +1130,7 @@ namespace spot
bool is_literal()
{
return (is(op::AP) ||
return (is(op::ap) ||
// If f is in nenoform, Not can only occur in front of
// an atomic proposition. So this way we do not have
// to check the type of the child.
@ -1194,10 +1194,10 @@ namespace spot
{
switch (op o = kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
return *this;
case op::Not:
case op::X:

2
src/ltlvisit/apcollect.cc
View file

@ -47,7 +47,7 @@ namespace spot
s = new atomic_prop_set;
f.traverse([&](const formula& f)
{
if (f.is(op::AP))
if (f.is(op::ap))
s->insert(f);
return false;
});

12
src/ltlvisit/dot.cc
View file

@ -60,9 +60,9 @@ namespace spot
return src;
op o = f.kind();
std::string str = (o == op::AP) ? f.ap_name() : f.kindstr();
std::string str = (o == op::ap) ? f.ap_name() : f.kindstr();
if (o == op::AP || f.is_constant())
if (o == op::ap || f.is_constant())
*sinks_ << " " << src << " [label=\""
<< str << "\", shape=box];\n";
else
@ -71,10 +71,10 @@ namespace spot
int childnum = 0;
switch (o)
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::Not:
case op::X:
case op::F:

16
src/ltlvisit/mark.cc
View file

@ -37,10 +37,10 @@ namespace spot
ltl::formula res;
switch (f.kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::Not:
case op::X:
case op::F:
@ -103,10 +103,10 @@ namespace spot
ltl::formula res;
switch (f.kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::Not:
case op::X:
case op::F:

8
src/ltlvisit/mutation.cc
View file

@ -67,11 +67,11 @@ namespace spot
switch (f.kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::ff:
case op::tt:
case op::eword:
return f;
case op::AP:
case op::ap:
if (opts_ & Mut_Ap2Const)
{
if (mutation_counter_-- == 0)

24
src/ltlvisit/print.cc
View file

@ -423,16 +423,16 @@ namespace spot
op o = f.kind();
switch (o)
{
case op::False:
case op::ff:
emit(KFalse);
break;
case op::True:
case op::tt:
emit(KTrue);
break;
case op::EmptyWord:
case op::eword:
emit(KEmptyWord);
break;
case op::AP:
case op::ap:
{
const std::string& str = f.ap_name();
if (!is_bare_word(str.c_str()))
@ -483,7 +483,7 @@ namespace spot
case op::Not:
{
formula c = f[0];
if (c.is(op::AP))
if (c.is(op::ap))
{
// If we negate a single letter in UTF-8, use a
// combining overline.
@ -585,7 +585,7 @@ namespace spot
formula right = f[1];
unsigned last = left.size() - 1;
bool onelast = false;
if (left.is(op::Concat) && left[last].is_true())
if (left.is(op::Concat) && left[last].is_tt())
{
visit(left.all_but(last));
onelast = true;
@ -609,7 +609,7 @@ namespace spot
}
else if (o == op::EConcat)
{
if (f[1].is(op::True))
if (f[1].is_tt())
{
os_ << '!';
// No recursion on right.
@ -743,7 +743,7 @@ namespace spot
unsigned default_max = formula::unbounded();
// Abbreviate "1[*]" as "[*]".
if (!c.is(op::True) || o != op::Star)
if (!c.is_tt() || o != op::Star)
{
if (o == op::Star)
{
@ -1042,13 +1042,13 @@ namespace spot
op o = f.kind();
switch (o)
{
case op::False:
case op::ff:
os_ << 'f';
break;
case op::True:
case op::tt:
os_ << 't';
break;
case op::AP:
case op::ap:
{
const std::string& str = f.ap_name();
if (!is_pnum(str.c_str()))
@ -1100,7 +1100,7 @@ namespace spot
os_ << "& ";
first_ = true;
break;
case op::EmptyWord:
case op::eword:
case op::Closure:
case op::NegClosure:
case op::NegClosureMarked:

4
src/ltlvisit/relabel.cc
View file

@ -121,7 +121,7 @@ namespace spot
formula
visit(formula f)
{
if (f.is(op::AP))
if (f.is(op::ap))
return rename(f);
else
return f.map([this](formula f)
@ -420,7 +420,7 @@ namespace spot
formula
visit(formula f)
{
if (f.is(op::AP) || (c.find(f) != c.end()))
if (f.is(op::ap) || (c.find(f) != c.end()))
return rename(f);
unsigned sz = f.size();

8
src/ltlvisit/simpfg.cc
View file

@ -29,16 +29,16 @@ namespace spot
formula simplify_f_g(formula p)
{
// 1 U p = Fp
if (p.is(op::U) && p[0].is_true())
if (p.is(op::U) && p[0].is_tt())
return formula::F(p[1]);
// 0 R p = Gp
if (p.is(op::R) && p[0].is_false())
if (p.is(op::R) && p[0].is_ff())
return formula::G(p[1]);
// p W 0 = Gp
if (p.is(op::W) && p[1].is_false())
if (p.is(op::W) && p[1].is_ff())
return formula::G(p[0]);
// p M 1 = Fp
if (p.is(op::M) && p[1].is_true())
if (p.is(op::M) && p[1].is_tt())
return formula::F(p[0]);
return p.map(simplify_f_g);
}

34
src/ltlvisit/simplify.cc
View file

@ -100,13 +100,13 @@ namespace spot
switch (f.kind())
{
case op::True:
case op::tt:
result = bddtrue;
break;
case op::False:
case op::ff:
result = bddfalse;
break;
case op::AP:
case op::ap:
result = bdd_ithvar(dict->register_proposition(f, this));
break;
case op::Not:
@ -385,15 +385,15 @@ namespace spot
switch (op o = f.kind())
{
case op::False:
case op::True:
case op::ff:
case op::tt:
// Negation of constants is taken care of in the
// constructor of unop::Not, so these cases should be
// caught by nenoform_recursively().
assert(!negated);
result = f;
break;
case op::AP:
case op::ap:
result = negated ? formula::Not(f) : f;
break;
case op::X:
@ -526,7 +526,7 @@ namespace spot
rec(f1, false), rec(f2, negated));
break;
}
case op::EmptyWord:
case op::eword:
case op::Not:
SPOT_UNREACHABLE();
}
@ -849,10 +849,10 @@ namespace spot
switch (op o = f.kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::Not:
case op::FStar:
return f;
@ -1772,16 +1772,16 @@ namespace spot
trace << "bo: trying basic reductions" << std::endl;
// Rewrite U,R,W,M as F or G when possible.
// true U b == F(b)
if (bo.is(op::U) && a.is(op::True))
if (bo.is(op::U) && a.is_tt())
return recurse(formula::F(b));
// false R b == G(b)
if (bo.is(op::R) && a.is(op::False))
if (bo.is(op::R) && a.is_ff())
return recurse(formula::G(b));
// a W false == G(a)
if (bo.is(op::W) && b.is(op::False))
if (bo.is(op::W) && b.is_ff())
return recurse(formula::G(a));
// a M true == F(a)
if (bo.is(op::M) && b.is(op::True))
if (bo.is(op::M) && b.is_tt())
return recurse(formula::F(a));
if (bo.is(op::W, op::M) || bo.is(op::U, op::R))
@ -3292,9 +3292,9 @@ namespace spot
if (f == g)
return true;
if (g.is(op::True) || f.is(op::False))
if (g.is_tt() || f.is_ff())
return true;
if (g.is(op::False) || f.is(op::True))
if (g.is_ff() || f.is_tt())
return false;
// Often we compare a literal (an atomic_prop or its negation)

8
src/ltlvisit/snf.cc
View file

@ -51,7 +51,7 @@ namespace spot
formula out;
switch (f.kind())
{
case op::EmptyWord:
case op::eword:
out = formula::ff();
break;
case op::Star:
@ -95,9 +95,9 @@ namespace spot
out = formula::OrRat(v);
break;
}
case op::False:
case op::True:
case op::AP:
case op::ff:
case op::tt:
case op::ap:
case op::Not:
case op::X:
case op::F:

8
src/ltlvisit/unabbrev.cc
View file

@ -92,10 +92,10 @@ namespace spot
switch (out.kind())
{
case op::False:
case op::True:
case op::EmptyWord:
case op::AP:
case op::ff:
case op::tt:
case op::eword:
case op::ap:
case op::Not:
case op::X:
case op::Closure:

4
src/tests/parseerr.test
View file

@ -96,7 +96,7 @@ a & (, a & 0
EOF
run 0 ../equals -E recover.txt
check 'a - b' 'AP(@3 #0 "a")' '>>> a - b
check 'a - b' 'ap(@3 #0 "a")' '>>> a - b
^
syntax error, unexpected $undefined
@ -105,7 +105,7 @@ syntax error, unexpected $undefined
ignoring trailing garbage
'
check '{a[*9999999999]}' 'Closure(@5 #0 [Star(@4 #0 0.. [AP(@3 #0 "a")])])' \
check '{a[*9999999999]}' 'Closure(@5 #0 [Star(@4 #0 0.. [ap(@3 #0 "a")])])' \
'>>> {a[*9999999999]}
^^^^^^^^^^
value too large ignored

4
src/tests/utf8.test
View file

@ -26,12 +26,12 @@ set -e
# ----
run 0 ../ltl2text '□◯a' >out
echo 'G(@5 #0 [X(@4 #0 [AP(@3 #0 "a")])])' > exp
echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "a")])])' > exp
cmp out exp
# ----
run 0 ../ltl2text '□◯"αβγ"' >out
echo 'G(@5 #0 [X(@4 #0 [AP(@3 #0 "αβγ")])])' > exp
echo 'G(@5 #0 [X(@4 #0 [ap(@3 #0 "αβγ")])])' > exp
cmp out exp

20
src/twa/acc.cc
View file

@ -411,9 +411,9 @@ namespace spot
int acc_cond::is_rabin() const
{
if (code_.is_false())
if (code_.is_ff())
return num_ == 0 ? 0 : -1;
if ((num_ & 1) || code_.is_true())
if ((num_ & 1) || code_.is_tt())
return -1;
if (is_rs(code_, acc_op::Or, acc_op::And, all_sets()))
@ -424,9 +424,9 @@ namespace spot
int acc_cond::is_streett() const
{
if (code_.is_true())
if (code_.is_tt())
return num_ == 0 ? 0 : -1;
if ((num_ & 1) || code_.is_false())
if ((num_ & 1) || code_.is_ff())
return -1;
if (is_rs(code_, acc_op::And, acc_op::Or, all_sets()))
@ -444,7 +444,7 @@ namespace spot
pairs.resize(num_);
return true;
}
if (code_.is_true()
if (code_.is_tt()
|| code_.back().op != acc_op::Or)
return false;
@ -670,7 +670,7 @@ namespace spot
if (sets == 0)
{
max = true;
odd = is_true();
odd = is_tt();
return true;
}
acc_cond::mark_t u_inf;
@ -1107,7 +1107,7 @@ namespace spot
acc_cond::acc_code acc_cond::acc_code::complement() const
{
if (is_true())
if (is_tt())
return acc_cond::acc_code::f();
return complement_rec(&back());
}
@ -1169,7 +1169,7 @@ namespace spot
acc_cond::acc_code
acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const
{
if (is_true() || is_false())
if (is_tt() || is_ff())
return *this;
return strip_rec(&back(), rem, missing);
}
@ -1177,7 +1177,7 @@ namespace spot
acc_cond::mark_t
acc_cond::acc_code::used_sets() const
{
if (is_true() || is_false())
if (is_tt() || is_ff())
return 0U;
acc_cond::mark_t used_in_cond = 0U;
auto pos = &back();
@ -1205,7 +1205,7 @@ namespace spot
std::pair<acc_cond::mark_t, acc_cond::mark_t>
acc_cond::acc_code::used_inf_fin_sets() const
{
if (is_true() || is_false())
if (is_tt() || is_ff())
return {0U, 0U};
acc_cond::mark_t used_fin = 0U;

24
src/twa/acc.hh
View file

@ -395,14 +395,14 @@ namespace spot
return !(*this == other);
}
bool is_true() const
bool is_tt() const
{
unsigned s = size();
return s == 0
|| ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
}
bool is_false() const
bool is_ff() const
{
unsigned s = size();
return s > 1
@ -561,12 +561,12 @@ namespace spot
void append_and(acc_code&& r)
{
if (is_true() || r.is_false())
if (is_tt() || r.is_ff())
{
*this = std::move(r);
return;
}
if (is_false() || r.is_true())
if (is_ff() || r.is_tt())
return;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
@ -652,12 +652,12 @@ namespace spot
void append_and(const acc_code& r)
{
if (is_true() || r.is_false())
if (is_tt() || r.is_ff())
{
*this = r;
return;
}
if (is_false() || r.is_true())
if (is_ff() || r.is_tt())
return;
unsigned s = size() - 1;
unsigned rs = r.size() - 1;
@ -742,9 +742,9 @@ namespace spot
void append_or(acc_code&& r)
{
if (is_true() || r.is_false())
if (is_tt() || r.is_ff())
return;
if (is_false() || r.is_true())
if (is_ff() || r.is_tt())
{
*this = std::move(r);
return;
@ -894,14 +894,14 @@ namespace spot
return uses_fin_acceptance_;
}
bool is_true() const
bool is_tt() const
{
return code_.is_true();
return code_.is_tt();
}
bool is_false() const
bool is_ff() const
{
return code_.is_false();
return code_.is_ff();
}
bool is_buchi() const

8
src/twa/formula2bdd.cc
View file

@ -72,11 +72,11 @@ namespace spot
};
switch (f.kind())
{
case op::False:
case op::ff:
return bddfalse;
case op::True:
case op::tt:
return bddtrue;
case op::EmptyWord:
case op::eword:
case op::Star:
case op::FStar:
case op::F:
@ -98,7 +98,7 @@ namespace spot
case op::OrRat:
case op::AndRat:
SPOT_UNIMPLEMENTED();
case op::AP:
case op::ap:
return bdd_ithvar(d->register_proposition(f, owner));
case op::Not:
return bdd_not(recurse(f[0]));

4
src/twaalgos/gtec/gtec.cc
View file

@ -133,7 +133,7 @@ namespace spot
{
{
auto acc = ecs_->aut->acc();
if (acc.get_acceptance().is_false())
if (acc.get_acceptance().is_ff())
return nullptr;
if (acc.uses_fin_acceptance())
throw std::runtime_error
@ -395,7 +395,7 @@ namespace spot
{
{
auto acc = ecs_->aut->acc();
if (acc.get_acceptance().is_false())
if (acc.get_acceptance().is_ff())
return nullptr;
if (acc.uses_fin_acceptance())
throw std::runtime_error

4
src/twaalgos/hoa.cc
View file

@ -299,7 +299,7 @@ namespace spot
acc_cond::acc_code acc_c = aut->acc().get_acceptance();
if (aut->acc().is_generalized_buchi())
{
if (aut->acc().is_true())
if (aut->acc().is_tt())
os << "acc-name: all";
else if (aut->acc().is_buchi())
os << "acc-name: Buchi";
@ -309,7 +309,7 @@ namespace spot
}
else if (aut->acc().is_generalized_co_buchi())
{
if (aut->acc().is_false())
if (aut->acc().is_ff())
os << "acc-name: none";
else if (aut->acc().is_co_buchi())
os << "acc-name: co-Buchi";

8
src/twaalgos/ltl2taa.cc
View file

@ -60,9 +60,9 @@ namespace spot
init_ = f;
switch (f.kind())
{
case op::False:
case op::ff:
return;
case op::True:
case op::tt:
{
std::vector<formula> empty;
res_->create_transition(init_, empty);
@ -70,9 +70,9 @@ namespace spot
succ_.push_back(ss);
return;
}
case op::EmptyWord:
case op::eword:
SPOT_UNIMPLEMENTED();
case op::AP:
case op::ap:
{
if (negated_)
f = formula::Not(f);

60
src/twaalgos/ltl2tgba_fm.cc
View file

@ -81,7 +81,7 @@ namespace spot
else if (sub.is(op::W))
{
// f W 0 = Gf
if (sub[1].is_false())
if (sub[1].is_ff())
implied_subformulae(sub[0], rec, true);
}
else
@ -90,7 +90,7 @@ namespace spot
// in 'f R g' and 'f M g' always evaluate 'g'.
formula b = sub;
sub = b[1];
if (b[0].is_false())
if (b[0].is_ff())
{
assert(b.is(op::R)); // because 0 M g = 0
// 0 R f = Gf
@ -539,7 +539,7 @@ namespace spot
bdd now_to_concat()
{
if (to_concat_ && !to_concat_.is(op::EmptyWord))
if (to_concat_ && !to_concat_.is(op::eword))
return recurse(to_concat_);
return bddfalse;
}
@ -557,14 +557,14 @@ namespace spot
bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest.is(op::EmptyWord))
if (dest.is(op::eword))
{
out |= label & next_to_concat();
}
else
{
formula dest2 = formula::Concat({dest, to_concat_});
if (!dest2.is(op::False))
if (!dest2.is_ff())
out |=
label & bdd_ithvar(dict_.register_next_variable(dest2));
}
@ -576,13 +576,13 @@ namespace spot
{
switch (op o = f.kind())
{
case op::False:
case op::ff:
return bddfalse;
case op::True:
case op::tt:
return next_to_concat();
case op::EmptyWord:
case op::eword:
return now_to_concat();
case op::AP:
case op::ap:
return (bdd_ithvar(dict_.register_proposition(f))
& next_to_concat());
case op::F:
@ -661,7 +661,7 @@ namespace spot
bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest.is(op::EmptyWord))
if (dest.is(op::eword))
{
res |= label &
bdd_ithvar(dict_.register_next_variable(f));
@ -669,7 +669,7 @@ namespace spot
else
{
formula dest2 = formula::Concat({dest, f});
if (!dest2.is(op::False))
if (!dest2.is_ff())
res |= label & bdd_ithvar
(dict_.register_next_variable(dest2));
}
@ -711,10 +711,10 @@ namespace spot
// If the destination is not 0 or [*0], it means it
// can have successors. Fusion the tail.
if (!dest.is(op::False, op::EmptyWord))
if (!dest.is(op::ff, op::eword))
{
formula dest2 = formula::Fusion({dest, f});
if (!dest2.is(op::False))
if (!dest2.is_ff())
res |= label &
bdd_ithvar(dict_.register_next_variable(dest2));
}
@ -858,12 +858,12 @@ namespace spot
// If the destination is not 0 or [*0], it means it
// can have successors. Fusion the tail and append
// anything to concatenate.
if (!dest.is(op::False, op::EmptyWord))
if (!dest.is(op::ff, op::eword))
{
formula dest2 = formula::Fusion({dest, tail});
if (to_concat_)
dest2 = formula::Concat({dest2, to_concat_});
if (!dest2.is(op::False))
if (!dest2.is_ff())
res |= label
& bdd_ithvar(dict_.register_next_variable(dest2));
}
@ -1117,13 +1117,13 @@ namespace spot
{
switch (op o = node.kind())
{
case op::False:
case op::ff:
return bddfalse;
case op::True:
case op::tt:
return bddtrue;
case op::EmptyWord:
case op::eword:
SPOT_UNIMPLEMENTED();
case op::AP:
case op::ap:
return bdd_ithvar(dict_.register_proposition(node));
case op::F:
{
@ -1248,7 +1248,7 @@ namespace spot
else
{
formula dest2 = formula::unop(o, dest);
if (dest2.is_false())
if (dest2.is_ff())
continue;
res |=
label & bdd_ithvar(dict_.register_next_variable(dest2));
@ -1290,7 +1290,7 @@ namespace spot
if (!dest.accepts_eword())
{
formula dest2 = formula::unop(o, dest);
if (dest2.is_false())
if (dest2.is_ff())
continue;
res |= label
& bdd_ithvar(dict_.register_next_variable(dest2));
@ -1333,7 +1333,7 @@ namespace spot
// r(f1 W f2) = r(f2) + r(f1) if recurring
//
// also f1 W 0 = G(f1), so we can enable recurring on f1
bdd f1 = recurse(node[0], node[1].is_false());
bdd f1 = recurse(node[0], node[1].is_ff());
bdd f2 = recurse(node[1]);
if (!recurring_)
f1 &= bdd_ithvar(dict_.register_next_variable(node));
@ -1346,7 +1346,7 @@ namespace spot
// r(f2) is in factor, so we can propagate the recurring_ flag.
// if f1=false, we can also turn it on (0 R f = Gf).
bdd res = recurse(node[1],
recurring_ || node[0].is_false());
recurring_ || node[0].is_ff());
// r(f1 R f2) = r(f2)(r(f1) + X(f1 R f2)) if not recurring
// r(f1 R f2) = r(f2) if recurring
if (recurring_ && !dict_.unambiguous)
@ -1419,7 +1419,7 @@ namespace spot
formula dest2 = formula::binop(o, dest, node[1]);
bool unamb = dict_.unambiguous;
if (!dest2.is(op::False))
if (!dest2.is_ff())
{
// If the rhs is Boolean, the
// unambiguous code will produce a more
@ -1456,14 +1456,14 @@ namespace spot
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest.is(op::EmptyWord))
if (dest.is(op::eword))
{
res |= label & f2;
}
else
{
formula dest2 = formula::binop(o, dest, node[1]);
if (!dest2.is(op::False))
if (!dest2.is_ff())
res |= label &
bdd_ithvar(dict_.register_next_variable(dest2));
if (dest.accepts_eword())
@ -2080,7 +2080,7 @@ namespace spot
{
dest = simplifier->simplify(dest);
// Ignore the arc if the destination reduces to false.
if (dest.is_false())
if (dest.is_ff())
continue;
}
@ -2131,11 +2131,11 @@ namespace spot
// f ----> 1
//
// because there is no point in looping on f if we can go to 1.
if (dests.front().dest.is_true())
if (dests.front().dest.is_tt())
{
dest_map::iterator i = dests.begin();
bdd c = bddfalse;
while (i != dests.end() && i->dest.is_true())
while (i != dests.end() && i->dest.is_tt())
c |= i++->cond;
for (; i != dests.end(); ++i)
i->cond -= c;
@ -2158,7 +2158,7 @@ namespace spot
// When translating LTL for an event-based logic
// with unobservable events, the 1 state should
// accept all events, even unobservable events.
if (unobs && t.dest.is_true() && now.is_true())
if (unobs && t.dest.is_tt() && now.is_tt())
t.cond = all_events;
// Will this be a new state?

2
src/twaalgos/neverclaim.cc
View file

@ -205,7 +205,7 @@ namespace spot
print_never_claim(std::ostream& os, const const_twa_ptr& g,
const char* options)
{
if (!(g->acc().is_buchi() || g->acc().is_true()))
if (!(g->acc().is_buchi() || g->acc().is_tt()))
throw std::runtime_error
("Never claim output only supports Büchi acceptance");
never_claim_output d(os, options);

2
src/twaalgos/product.cc
View file

@ -81,7 +81,7 @@ namespace spot
};
res->set_init_state(new_state(left_state, right_state));
if (right_acc.is_false())
if (right_acc.is_ff())
// Do not bother doing any work if the resulting acceptance is
// false.
return res;

4
src/twaalgos/remfin.cc
View file

@ -311,7 +311,7 @@ namespace spot
auto code = aut->get_acceptance();
if (code.is_true())
if (code.is_tt())
return nullptr;
acc_cond::mark_t inf_pairs = 0U;
@ -586,7 +586,7 @@ namespace spot
auto c = acc.inf(m);
for (unsigned i = 0; i < sz; ++i)
{
if (!code[i].is_true())
if (!code[i].is_tt())
continue;
add[i] = m;
code[i].append_and(c);

2
src/twaalgos/safety.cc
View file

@ -65,7 +65,7 @@ namespace spot
bool is_safety_mwdba(const const_twa_graph_ptr& aut)
{
if (!(aut->acc().is_buchi() || aut->acc().is_true()))
if (!(aut->acc().is_buchi() || aut->acc().is_tt()))
throw std::runtime_error
("is_safety_mwdba() should be called on a Buchi automaton");

2
wrap/python/spot.py
View file

@ -124,7 +124,7 @@ def _formula_traverse(self, func):
def _formula_map(self, func):
k = self.kind()
if k in (FalseVal, TrueVal, EmptyWord, AP):
if k in (ff, tt, eword, ap):
return self;
if k in (Not, X, F, G, Closure, NegClosure, NegClosureMarked):
return formula.unop(k, func(self[0]))