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

cube: more tests

Browse source 
* tests/core/cube.cc, tests/core/cube.test: Here.
This commit is contained in:
Etienne Renault 2020-06-08 09:19:18 +02:00
parent 6243803018
commit c61b721a48
2 changed files with 26 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

18
tests/core/cube.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement // Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et
// de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -144,6 +144,7 @@ int main()
std::cout << "cube : " << cs.dump(mc, aps) << '\n'; std::cout << "cube : " << cs.dump(mc, aps) << '\n';
std::cout << "valid : " << cs.is_valid(mc) << '\n'; std::cout << "valid : " << cs.is_valid(mc) << '\n';
std::cout << "intersect(c,c) : " << cs.intersect(mc, mc) << '\n'; std::cout << "intersect(c,c) : " << cs.intersect(mc, mc) << '\n';
cs.display(mc);
spot::cube mc1 = cs.alloc(); spot::cube mc1 = cs.alloc();
cs.set_false_var(mc1, 0); cs.set_false_var(mc1, 0);
@ -154,6 +155,7 @@ int main()
std::cout << "intersect(c1,c1) : " << cs.intersect(mc1, mc1) << '\n'; std::cout << "intersect(c1,c1) : " << cs.intersect(mc1, mc1) << '\n';
std::cout << "intersect(c,c1) : " << cs.intersect(mc, mc1) << '\n'; std::cout << "intersect(c,c1) : " << cs.intersect(mc, mc1) << '\n';
std::cout << "intersect(c1,c) : " << cs.intersect(mc1, mc) << '\n'; std::cout << "intersect(c1,c) : " << cs.intersect(mc1, mc) << '\n';
cs.display(mc1);
spot::cube mc2 = cs.alloc(); spot::cube mc2 = cs.alloc();
cs.set_true_var(mc2, 1); cs.set_true_var(mc2, 1);
@ -163,7 +165,19 @@ int main()
std::cout << "valid : " << cs.is_valid(mc2) << '\n'; std::cout << "valid : " << cs.is_valid(mc2) << '\n';
std::cout << "intersect(c2,c1) : " << cs.intersect(mc1, mc2) << '\n'; std::cout << "intersect(c2,c1) : " << cs.intersect(mc1, mc2) << '\n';
std::cout << "intersect(c2,c) : " << cs.intersect(mc, mc2) << '\n'; std::cout << "intersect(c2,c) : " << cs.intersect(mc, mc2) << '\n';
cs.display(mc2);
std::vector<std::string> apsx;
for (unsigned i = 0; i < 44; ++i)
apsx.push_back("a" + std::to_string(i));
spot::cubeset csx(apsx.size());
spot::cube mcx = csx.alloc();
csx.set_true_var(mcx, 0);
csx.set_false_var(mcx, 42);
std::cout << "cube : " << csx.dump(mcx, apsx) << '\n';
csx.display(mcx);
cs.release(mcx);
cs.release(mc2); cs.release(mc2);
cs.release(mc1); cs.release(mc1);
cs.release(mc); cs.release(mc);

11
tests/core/cube.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de # Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -37,17 +37,26 @@ size : 5
cube : a&!d cube : a&!d
valid : 1 valid : 1
intersect(c,c) : 1 intersect(c,c) : 1
10000000000000000000000000000000
00010000000000000000000000000000
size : 5 size : 5
cube : !a&b cube : !a&b
valid : 1 valid : 1
intersect(c1,c1) : 1 intersect(c1,c1) : 1
intersect(c,c1) : 0 intersect(c,c1) : 0
intersect(c1,c) : 0 intersect(c1,c) : 0
01000000000000000000000000000000
10000000000000000000000000000000
size : 5 size : 5
cube : b&d cube : b&d
valid : 1 valid : 1
intersect(c2,c1) : 1 intersect(c2,c1) : 1
intersect(c2,c) : 0 intersect(c2,c) : 0
01010000000000000000000000000000
00000000000000000000000000000000
cube : a0&!a42
1000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000001000000000000000000000
bdd : T bdd : T
cube : 1 cube : 1
bdd : F bdd : F