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

Deprecate ltl::clone(f) in favor of f->clone().

Browse source 
* src/ltlvisit/clone.hh (clone): Document and declare as deprecated.
* src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py:
Adjust clone() usage, and remove the #include "clone.hh" when
appropriate.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-08 19:41:40 +01:00
parent e44f1b8997
commit 48fb19ea44
16 changed files with 103 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

15
ChangeLog
View file

@ -1,3 +1,18 @@
2009-11-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Deprecate ltl::clone(f) in favor of f->clone().
* src/ltlvisit/clone.hh (clone): Document and declare as deprecated.
* src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py:
Adjust clone() usage, and remove the #include "clone.hh" when
appropriate.
2009-11-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make it possible to clone const formulae.

3
src/ltlast/formula_tree.cc
View file

@ -22,7 +22,6 @@
#include <cassert>
#include "formula_tree.hh"
#include "allnodes.hh"
#include "ltlvisit/clone.hh"
namespace spot
{
@ -35,7 +34,7 @@ namespace spot
{
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return n->i == True ? constant::true_instance() :
n->i == False ? constant::false_instance() : clone(v.at(n->i));
n->i == False ? constant::false_instance() : v.at(n->i)->clone();
if (node_unop* n = dynamic_cast<node_unop*>(np.get()))
return unop::instance(n->op, instanciate(n->child, v));

43
src/ltlvisit/basicreduce.cc
View file

@ -24,7 +24,6 @@
#include "ltlast/allnodes.hh"
#include <cassert>
#include "clone.hh"
#include "destroy.hh"
namespace spot
@ -95,9 +94,9 @@ namespace spot
unsigned mos = mo->size();
for (unsigned i = 0; i < mos; ++i)
if (is_GF(mo->nth(i)))
resGF->push_back(clone(mo->nth(i)));
resGF->push_back(mo->nth(i)->clone());
else
res1->push_back(clone(mo->nth(i)));
res1->push_back(mo->nth(i)->clone());
destroy(mo);
multop::vec* res3 = new multop::vec;
if (!res1->empty())
@ -330,17 +329,17 @@ namespace spot
if (uo && uo->op() == unop::X)
{
// Xa & Xb = X(a & b)
tmpX->push_back(clone(uo->child()));
tmpX->push_back(uo->child()->clone());
}
else if (is_FG(*i))
{
// FG(a) & FG(b) = FG(a & b)
unop* uo2 = dynamic_cast<unop*>(uo->child());
tmpFG->push_back(clone(uo2->child()));
tmpFG->push_back(uo2->child()->clone());
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
}
else if (bo)
@ -360,7 +359,7 @@ namespace spot
&& ftmp == bo2->second())
{
tmpUright
->push_back(clone(bo2->first()));
->push_back(bo2->first()->clone());
if (j != i)
{
destroy(*j);
@ -374,7 +373,7 @@ namespace spot
instance(multop::
And,
tmpUright),
clone(ftmp)));
ftmp->clone()));
}
else if (bo->op() == binop::R)
{
@ -391,7 +390,7 @@ namespace spot
&& ftmp == bo2->first())
{
tmpRright
->push_back(clone(bo2->second()));
->push_back(bo2->second()->clone());
if (j != i)
{
destroy(*j);
@ -401,19 +400,19 @@ namespace spot
}
tmpR
->push_back(binop::instance(binop::R,
clone(ftmp),
ftmp->clone(),
multop::
instance(multop::And,
tmpRright)));
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
destroy(*i);
}
@ -436,22 +435,22 @@ namespace spot
if (uo && uo->op() == unop::X)
{
// Xa | Xb = X(a | b)
tmpX->push_back(clone(uo->child()));
tmpX->push_back(uo->child()->clone());
}
else if (is_GF(*i))
{
// GF(a) | GF(b) = GF(a | b)
unop* uo2 = dynamic_cast<unop*>(uo->child());
tmpGF->push_back(clone(uo2->child()));
tmpGF->push_back(uo2->child()->clone());
}
else if (is_FG(*i))
{
// FG(a) | FG(b) = F(Ga | Gb)
tmpFG->push_back(clone(uo->child()));
tmpFG->push_back(uo->child()->clone());
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
}
else if (bo)
@ -471,7 +470,7 @@ namespace spot
&& ftmp == bo2->first())
{
tmpUright
->push_back(clone(bo2->second()));
->push_back(bo2->second()->clone());
if (j != i)
{
destroy(*j);
@ -480,7 +479,7 @@ namespace spot
}
}
tmpU->push_back(binop::instance(binop::U,
clone(ftmp),
ftmp->clone(),
multop::
instance(multop::Or,
tmpUright)));
@ -500,7 +499,7 @@ namespace spot
&& ftmp == bo2->second())
{
tmpRright
->push_back(clone(bo2->first()));
->push_back(bo2->first()->clone());
if (j != i)
{
destroy(*j);
@ -513,16 +512,16 @@ namespace spot
multop::
instance(multop::Or,
tmpRright),
clone(ftmp)));
ftmp->clone()));
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
}
else
{
tmpOther->push_back(clone(*i));
tmpOther->push_back((*i)->clone());
}
destroy(*i);
}

2
src/ltlvisit/clone.cc
View file

@ -87,7 +87,7 @@ namespace spot
formula*
clone_visitor::recurse(formula* f)
{
return clone(f);
return f->clone();
}
formula*

12
src/ltlvisit/clone.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -35,7 +35,7 @@ namespace spot
/// This visitor is public, because it's convenient
/// to derive from it and override part of its methods.
/// But if you just want the functionality, consider using
/// spot::ltl::clone instead.
/// spot::ltl::formula::clone instead, it is way faster.
class clone_visitor : public visitor
{
public:
@ -57,9 +57,17 @@ namespace spot
formula* result_;
};
#if __GNUC__
/// \brief Clone a formula.
/// \ingroup ltl_essential
/// \deprecated Use f->clone() instead.
formula* clone(const formula* f) __attribute__ ((deprecated));
#else
/// \brief Clone a formula.
/// \ingroup ltl_essential
/// \deprecated Use f->clone() instead.
formula* clone(const formula* f);
#endif
}
}

9
src/ltlvisit/contain.cc
View file

@ -21,7 +21,6 @@
#include "contain.hh"
#include "destroy.hh"
#include "clone.hh"
#include "tunabbrev.hh"
#include "ltlast/unop.hh"
#include "ltlast/binop.hh"
@ -88,7 +87,7 @@ namespace spot
language_containment_checker::contained(const formula* l, const formula* g)
{
record_* rl = register_formula_(l);
const formula* ng = unop::instance(unop::Not, clone(g));
const formula* ng = unop::instance(unop::Not, g->clone());
record_* rng = register_formula_(ng);
destroy(ng);
return incompatible_(rl, rng);
@ -99,9 +98,9 @@ namespace spot
language_containment_checker::neg_contained(const formula* l,
const formula* g)
{
const formula* nl = unop::instance(unop::Not, clone(l));
const formula* nl = unop::instance(unop::Not, l->clone());
record_* rnl = register_formula_(nl);
const formula* ng = unop::instance(unop::Not, clone(g));
const formula* ng = unop::instance(unop::Not, g->clone());
record_* rng = register_formula_(ng);
destroy(nl);
destroy(ng);
@ -135,7 +134,7 @@ namespace spot
const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_,
branching_postponement_,
fair_loop_approx_);
record_& r = translated_[clone(f)];
record_& r = translated_[f->clone()];
r.translation = e;
return &r;
}

9
src/ltlvisit/lunabbrev.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -20,7 +20,6 @@
// 02111-1307, USA.
#include "ltlast/allnodes.hh"
#include "ltlvisit/clone.hh"
#include "lunabbrev.hh"
#include <cassert>
@ -48,10 +47,10 @@ namespace spot
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
case binop::Xor:
result_ = multop::instance(multop::Or,
multop::instance(multop::And, clone(f1),
multop::instance(multop::And, f1->clone(),
unop::instance(unop::Not,
f2)),
multop::instance(multop::And, clone(f2),
multop::instance(multop::And, f2->clone(),
unop::instance(unop::Not,
f1)));
return;
@ -64,7 +63,7 @@ namespace spot
case binop::Equiv:
result_ = multop::instance(multop::Or,
multop::instance(multop::And,
clone(f1), clone(f2)),
f1->clone(), f2->clone()),
multop::instance(multop::And,
unop::instance(unop::Not,
f1),

2
src/ltlvisit/reduce.cc
View file

@ -314,7 +314,7 @@ namespace spot
}
else
{
prev = clone(f);
prev = f->clone();
}
f1 = unabbreviate_logic(f);
f2 = simplify_f_g(f1);

10
src/ltlvisit/syntimpl.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2005, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -404,7 +404,7 @@ namespace spot
/* F(a) = true U a */
const formula* tmp = binop::instance(binop::U,
constant::true_instance(),
clone(f1));
f1->clone());
if (special_case(tmp))
{
result_ = true;
@ -421,7 +421,7 @@ namespace spot
/* G(a) = false R a */
const formula* tmp = binop::instance(binop::R,
constant::false_instance(),
clone(f1));
f1->clone());
if (special_case(tmp))
{
result_ = true;
@ -573,8 +573,8 @@ namespace spot
bool
syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
{
formula* l = clone(f1);
formula* r = clone(f2);
formula* l = f1->clone();
formula* r = f2->clone();
if (right)
r = unop::instance(unop::Not, r);
else

9
src/tgba/bdddict.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
@ -22,7 +22,6 @@
#include <ostream>
#include <sstream>
#include <cassert>
#include <ltlvisit/clone.hh>
#include <ltlvisit/destroy.hh>
#include <ltlvisit/tostring.hh>
#include <ltlvisit/tostring.hh>
@ -59,7 +58,7 @@ namespace spot
}
else
{
f = clone(f);
f = f->clone();
num = allocate_variables(1);
var_map[f] = num;
var_formula_map[num] = f;
@ -94,7 +93,7 @@ namespace spot
}
else
{
f = ltl::clone(f);
f = f->clone();
num = allocate_variables(2);
now_map[f] = num;
now_formula_map[num] = f;
@ -120,7 +119,7 @@ namespace spot
}
else
{
f = clone(f);
f = f->clone();
num = allocate_variables(1);
acc_map[f] = num;
acc_formula_map[num] = f;

9
src/tgba/formula2bdd.cc
View file

@ -1,6 +1,6 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -24,7 +24,6 @@
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include "misc/minato.hh"
#include "ltlvisit/clone.hh"
namespace spot
{
@ -171,7 +170,7 @@ namespace spot
int var = bdd_var(b);
bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var);
assert(isi != d->var_formula_map.end());
formula* res = clone(isi->second);
formula* res = isi->second->clone();
bdd high = bdd_high(b);
if (high == bddfalse)

5
src/tgba/tgbabddconcretefactory.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -19,7 +19,6 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "ltlvisit/clone.hh"
#include "ltlvisit/destroy.hh"
#include "tgbabddconcretefactory.hh"
namespace spot
@ -79,7 +78,7 @@ namespace spot
acc_map_::iterator ai = acc_.find(a);
if (ai == acc_.end())
{
a = clone(a);
a = a->clone();
acc_[a] = b;
}
else

33
src/tgbaalgos/ltl2taa.cc
View file

@ -27,7 +27,6 @@
#include "ltlvisit/nenoform.hh"
#include "ltlvisit/destroy.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh"
#include "ltlvisit/contain.hh"
#include "ltl2taa.hh"
@ -68,7 +67,7 @@ namespace spot
const formula* f = node; // Handle negation
if (negated_)
{
f = unop::instance(unop::Not, clone(node));
f = unop::instance(unop::Not, node->clone());
to_free_.push_back(f);
}
init_ = to_string(f);
@ -76,7 +75,7 @@ namespace spot
dst.push_back(std::string("sink"));
taa::transition* t = res_->create_transition(init_, dst);
res_->add_condition(t, clone(f));
res_->add_condition(t, f->clone());
succ_state ss = { dst, f, constant::true_instance() };
succ_.push_back(ss);
}
@ -165,14 +164,14 @@ namespace spot
i1->Q.push_back(init_); // Add the initial state
i1->acc = node;
t = res_->create_transition(init_, i1->Q);
res_->add_condition(t, clone(i1->condition));
res_->add_acceptance_condition(t, clone(node));
res_->add_condition(t, i1->condition->clone());
res_->add_acceptance_condition(t, node->clone());
succ_.push_back(*i1);
}
for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
{
t = res_->create_transition(init_, i2->Q);
res_->add_condition(t, clone(i2->condition));
res_->add_condition(t, i2->condition->clone());
succ_.push_back(*i2);
}
return;
@ -185,16 +184,16 @@ namespace spot
{
std::vector<std::string> u; // Union
std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.begin()));
formula* f = clone(i1->condition); // Refined rule
formula* f = i1->condition->clone(); // Refined rule
if (!refined_ || !contained)
{
std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.begin()));
f = multop::instance(multop::And, f, clone(i2->condition));
f = multop::instance(multop::And, f, i2->condition->clone());
}
to_free_.push_back(f);
t = res_->create_transition(init_, u);
res_->add_condition(t, clone(f));
res_->add_condition(t, f->clone());
succ_state ss = { u, f, constant::true_instance() };
succ_.push_back(ss);
}
@ -205,9 +204,9 @@ namespace spot
i2->Q.push_back(init_); // Add the initial state
t = res_->create_transition(init_, i2->Q);
res_->add_condition(t, clone(i2->condition));
res_->add_condition(t, i2->condition->clone());
if (refined_ && i2->acc != constant::true_instance())
res_->add_acceptance_condition(t, clone(i2->acc));
res_->add_acceptance_condition(t, i2->acc->clone());
succ_.push_back(*i2);
}
return;
@ -262,15 +261,15 @@ namespace spot
Q.push_back(p[n].Q[m]);
Q.push_back(init_);
t = res_->create_transition(init_, Q);
res_->add_condition(t, clone(p[n].condition));
res_->add_condition(t, p[n].condition->clone());
if (p[n].acc != constant::true_instance())
res_->add_acceptance_condition(t, clone(p[n].acc));
res_->add_acceptance_condition(t, p[n].acc->clone());
succ_.push_back(p[n]);
return;
}
}
t = res_->create_transition(init_, p[n].Q);
res_->add_condition(t, clone(p[n].condition));
res_->add_condition(t, p[n].condition->clone());
succ_.push_back(p[n]);
}
return;
@ -280,7 +279,7 @@ namespace spot
for (i = vs[n].succ_.begin(); i != vs[n].succ_.end(); ++i)
{
t = res_->create_transition(init_, i->Q);
res_->add_condition(t, clone(i->condition));
res_->add_condition(t, i->condition->clone());
succ_.push_back(*i);
}
return;
@ -349,8 +348,8 @@ namespace spot
continue;
const succ_state& ss(vs[i].succ_[pos[i] - 1]);
std::copy(ss.Q.begin(), ss.Q.end(), ii(u, u.begin()));
f = multop::instance(multop::And, clone(ss.condition), f);
a = multop::instance(multop::And, clone(ss.acc), a);
f = multop::instance(multop::And, ss.condition->clone(), f);
a = multop::instance(multop::And, ss.acc->clone(), a);
}
to_free_.push_back(f);
to_free_.push_back(a);

16
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -110,7 +110,7 @@ namespace spot
}
else
{
f = clone(f);
f = f->clone();
num = dict->register_anonymous_variables(1, this);
next_map[f] = num;
next_formula_map[num] = f;
@ -139,13 +139,13 @@ namespace spot
{
vf_map::const_iterator isi = next_formula_map.find(var);
if (isi != next_formula_map.end())
return clone(isi->second);
return isi->second->clone();
isi = dict->acc_formula_map.find(var);
if (isi != dict->acc_formula_map.end())
return clone(isi->second);
return isi->second->clone();
isi = dict->var_formula_map.find(var);
if (isi != dict->var_formula_map.end())
return clone(isi->second);
return isi->second->clone();
assert(0);
// Never reached, but some GCC versions complain about
// a missing return otherwise.
@ -213,7 +213,7 @@ namespace spot
formula* ac = var_to_formula(var);
if (!a->has_acceptance_condition(ac))
a->declare_acceptance_condition(clone(ac));
a->declare_acceptance_condition(ac->clone());
a->add_acceptance_condition(t, ac);
b = high;
}
@ -604,7 +604,7 @@ namespace spot
res &= all_promises_;
}
f2b_[clone(f)] = res;
f2b_[f->clone()] = res;
// Register the reverse mapping if it is not already done.
if (b2f_.find(res) == b2f_.end())
@ -627,7 +627,7 @@ namespace spot
{
// The translated bdd maps to an already seen formula.
destroy(f);
f = clone(i->second);
f = i->second->clone();
}
else if (new_variable && lcc_)
{
@ -641,7 +641,7 @@ namespace spot
f2b_[f] = j->second;
i->second = j->first;
destroy(f);
f = clone(i->second);
f = i->second->clone();
break;
}
}

5
src/tgbatest/complementation.cc
View file

@ -12,7 +12,6 @@
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/emptiness_stats.hh"
#include "ltlvisit/destroy.hh"
#include "ltlvisit/clone.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbasafracomplement.hh"
@ -217,7 +216,7 @@ int main(int argc, char* argv[])
{
spot::ltl::formula* nf1 =
spot::ltl::unop::instance(spot::ltl::unop::Not,
spot::ltl::clone(f1));
f1->clone());
spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict);
spot::tgba_statistics a_size = spot::stats_reachable(a2);
std::cout << "Not Formula: "
@ -241,7 +240,7 @@ int main(int argc, char* argv[])
spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict);
spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not,
spot::ltl::clone(f1));
f1->clone());
spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict);
spot::tgba* nAf;

12
wrap/python/tests/ltlsimple.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
@ -23,8 +23,6 @@
import ltihooks
import spot
clone = spot.clone
e = spot.default_environment.instance()
#----------------------------------------------------------------------
@ -36,7 +34,7 @@ c2 = e.require('c')
assert c == c2
assert spot.atomic_prop.instance_count() == 3
op = spot.multop.instance(spot.multop.And, clone(a), clone(b))
op = spot.multop.instance(spot.multop.And, a.clone(), b.clone())
op2 = spot.multop.instance(spot.multop.And, op, c)
# The symbol for a subformula which hasn't been cloned is better
@ -75,9 +73,9 @@ c = e.require('c')
T = spot.constant.true_instance()
F = spot.constant.false_instance()
f1 = spot.binop.instance(spot.binop.Equiv, T, clone(a))
f2 = spot.binop.instance(spot.binop.Implies, F, clone(b))
f3 = spot.binop.instance(spot.binop.Xor, F, clone(c))
f1 = spot.binop.instance(spot.binop.Equiv, T, a.clone())
f2 = spot.binop.instance(spot.binop.Implies, F, b.clone())
f3 = spot.binop.instance(spot.binop.Xor, F, c.clone())
f4 = spot.unop.instance(spot.unop.Not, f3); del f3
assert spot.atomic_prop.instance_count() == 3