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

Adjust Python tests to the new simplification rules.

Browse source 
* wrap/python/tests/ltlsimple.py: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-03 12:24:02 +01:00
parent dbdd37010c
commit 916c154291
1 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2,7 +2,7 @@
# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004 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 Systemes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -75,10 +75,11 @@ c = e.require('c')
T = spot.constant.true_instance() T = spot.constant.true_instance()
F = spot.constant.false_instance() F = spot.constant.false_instance()
f1 = spot.binop.instance(spot.binop.Equiv, T, a.clone()) f1 = spot.binop.instance(spot.binop.Equiv, c.clone(), a.clone())
f2 = spot.binop.instance(spot.binop.Implies, F, b.clone()) f2 = spot.binop.instance(spot.binop.Implies, a.clone(), b.clone())
f3 = spot.binop.instance(spot.binop.Xor, F, c.clone()) f3 = spot.binop.instance(spot.binop.Xor, b.clone(), c.clone())
f4 = spot.unop.instance(spot.unop.Not, f3); del f3 f4 = spot.unop.instance(spot.unop.Not, f3); del f3
f5 = spot.binop.instance(spot.binop.Xor, F, c.clone())
assert spot.atomic_prop.instance_count() == 3 assert spot.atomic_prop.instance_count() == 3
assert spot.binop.instance_count() == 3 assert spot.binop.instance_count() == 3
@ -100,7 +101,15 @@ assert spot.multop.instance_count() == 0
f1.destroy() f1.destroy()
del f1 del f1
assert spot.atomic_prop.instance_count() == 2 assert spot.atomic_prop.instance_count() == 3
assert spot.binop.instance_count() == 2
assert spot.unop.instance_count() == 1
assert spot.multop.instance_count() == 0
f5.destroy()
del f5
assert spot.atomic_prop.instance_count() == 3
assert spot.binop.instance_count() == 2 assert spot.binop.instance_count() == 2
assert spot.unop.instance_count() == 1 assert spot.unop.instance_count() == 1
assert spot.multop.instance_count() == 0 assert spot.multop.instance_count() == 0
@ -108,7 +117,7 @@ assert spot.multop.instance_count() == 0
f4.destroy() f4.destroy()
del f4 del f4
assert spot.atomic_prop.instance_count() == 1 assert spot.atomic_prop.instance_count() == 2
assert spot.binop.instance_count() == 1 assert spot.binop.instance_count() == 1
assert spot.unop.instance_count() == 0 assert spot.unop.instance_count() == 0
assert spot.multop.instance_count() == 0 assert spot.multop.instance_count() == 0