From c61b721a4826b3a8767a74508fcbbf0d619cf368 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Mon, 8 Jun 2020 09:19:18 +0200 Subject: [PATCH] cube: more tests * tests/core/cube.cc, tests/core/cube.test: Here. --- tests/core/cube.cc | 18 ++++++++++++++++-- tests/core/cube.test | 11 ++++++++++- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/tests/core/cube.cc b/tests/core/cube.cc index 1716039f1..fc94b1152 100644 --- a/tests/core/cube.cc +++ b/tests/core/cube.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et +// Développement de l'Epita. // // 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 << "valid : " << cs.is_valid(mc) << '\n'; std::cout << "intersect(c,c) : " << cs.intersect(mc, mc) << '\n'; + cs.display(mc); spot::cube mc1 = cs.alloc(); 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(c,c1) : " << cs.intersect(mc, mc1) << '\n'; std::cout << "intersect(c1,c) : " << cs.intersect(mc1, mc) << '\n'; + cs.display(mc1); spot::cube mc2 = cs.alloc(); cs.set_true_var(mc2, 1); @@ -163,7 +165,19 @@ int main() std::cout << "valid : " << cs.is_valid(mc2) << '\n'; std::cout << "intersect(c2,c1) : " << cs.intersect(mc1, mc2) << '\n'; std::cout << "intersect(c2,c) : " << cs.intersect(mc, mc2) << '\n'; + cs.display(mc2); + std::vector 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(mc1); cs.release(mc); diff --git a/tests/core/cube.test b/tests/core/cube.test index 414f40e49..5e38d30c3 100755 --- a/tests/core/cube.test +++ b/tests/core/cube.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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). # # This file is part of Spot, a model checking library. @@ -37,17 +37,26 @@ size : 5 cube : a&!d valid : 1 intersect(c,c) : 1 +10000000000000000000000000000000 +00010000000000000000000000000000 size : 5 cube : !a&b valid : 1 intersect(c1,c1) : 1 intersect(c,c1) : 0 intersect(c1,c) : 0 +01000000000000000000000000000000 +10000000000000000000000000000000 size : 5 cube : b&d valid : 1 intersect(c2,c1) : 1 intersect(c2,c) : 0 +01010000000000000000000000000000 +00000000000000000000000000000000 +cube : a0&!a42 +1000000000000000000000000000000000000000000000000000000000000000 +0000000000000000000000000000000000000000001000000000000000000000 bdd : T cube : 1 bdd : F