From 66839b1a2920ef6f219e248beb5660ca24ef9491 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 23 Feb 2023 11:53:07 +0100 Subject: [PATCH] bdd_to_formula: add CNF variant * spot/twa/formula2bdd.hh, spot/twa/formula2bdd.cc (bdd_to_cnf_formula): New function. * python/spot/__init__.py: Add a default dictionary for convenience. * tests/python/bdditer.py: Add test cases. * NEWS: Mention it. --- NEWS | 3 ++ python/spot/__init__.py | 8 ++++-- spot/twa/formula2bdd.cc | 32 +++++++++++++++++---- spot/twa/formula2bdd.hh | 23 +++++++++++----- tests/python/bdditer.py | 61 +++++++++++++++++++++++++++++++++++++++-- 5 files changed, 111 insertions(+), 16 deletions(-) diff --git a/NEWS b/NEWS index 3cfa6edc2..86fd461e1 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.11.4.dev (not yet released) supports only one): it now reuse the edges leaving initial states without incoming transitions. + - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula() + that converts a BDD into a CNF instead of a DNF. + Python: - spot.acd() no longer depends on jQuery for interactivity. diff --git a/python/spot/__init__.py b/python/spot/__init__.py index ef4cd772e..02bdcb1f6 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1,6 +1,6 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2014-2022 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2014-2023 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -1347,6 +1347,10 @@ def bdd_to_formula(b, dic=_bdd_dict): from spot.impl import bdd_to_formula as bf return bf(b, dic) +def bdd_to_cnf_formula(b, dic=_bdd_dict): + from spot.impl import bdd_to_cnf_formula as bf + return bf(b, dic) + def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index 7596c0759..15434395f 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2019, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -30,11 +30,14 @@ namespace spot namespace { // Convert a BDD which is known to be a conjonction into a formula. + // If dual is true, dualize the result, i.e., negate literals, and + // exchange ∧ and ∨. + template static formula conj_to_formula(bdd b, const bdd_dict_ptr d) { if (b == bddfalse) - return formula::ff(); + return dual ? formula::tt() : formula::ff(); std::vector v; while (b != bddtrue) { @@ -49,11 +52,14 @@ namespace spot bdd high = bdd_high(b); if (high == bddfalse) { - res = formula::Not(res); + if (!dual) + res = formula::Not(res); b = bdd_low(b); } else { + if (dual) + res = formula::Not(res); // If bdd_low is not false, then b was not a conjunction. assert(bdd_low(b) == bddfalse); b = high; @@ -61,7 +67,7 @@ namespace spot assert(b != bddfalse); v.emplace_back(res); } - return formula::And(v); + return dual ? formula::Or(v) : formula::And(v); } } // anonymous @@ -143,7 +149,23 @@ namespace spot minato_isop isop(f); bdd cube; while ((cube = isop.next()) != bddfalse) - v.emplace_back(conj_to_formula(cube, d)); + v.emplace_back(conj_to_formula(cube, d)); return formula::Or(std::move(v)); } + + formula + bdd_to_cnf_formula(bdd f, const bdd_dict_ptr d) + { + if (f == bddtrue) + return formula::tt(); + + std::vector v; + + minato_isop isop(!f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v.emplace_back(conj_to_formula(cube, d)); + return formula::And(std::move(v)); + } + } diff --git a/spot/twa/formula2bdd.hh b/spot/twa/formula2bdd.hh index 4d5c81a60..a84d27996 100644 --- a/spot/twa/formula2bdd.hh +++ b/spot/twa/formula2bdd.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -52,12 +52,21 @@ namespace spot /// \brief Convert a BDD into a formula. /// - /// Format the BDD as an irredundant sum of product (see the - /// minato_isop class for details) and map the BDD variables back - /// into their atomic propositions. This works only for Boolean - /// formulas, and all the BDD variables used in \a f should have - /// been registered in \a d. Although the result has type - /// formula, it obviously does not use any temporal operator. + /// Format the BDD as a Boolean spot::formula object. This works only + /// for Boolean formulas, and all the BDD variables used in \a f + /// should have been registered in \a d. Although the result has + /// type formula, it obviously does not use any temporal operator. + /// + /// The bdd_to_formula() version produces an irredundant sum of + /// product (see the minato_isop class for details) and map the BDD + /// variables back into their atomic propositions. + /// + /// The bdd_to_cnf_formula() version produces an irredundant product of + /// sum, using the dual construction. + /// @{ SPOT_API formula bdd_to_formula(bdd f, const bdd_dict_ptr d); + SPOT_API + formula bdd_to_cnf_formula(bdd f, const bdd_dict_ptr d); + /// @} } diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py index 95cc441b3..4a2afeea1 100644 --- a/tests/python/bdditer.py +++ b/tests/python/bdditer.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2017, 2018, 2021, 2022, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -27,6 +27,19 @@ import sys from unittest import TestCase tc = TestCase() +# CPython use reference counting, so that automata are destructed +# when we expect them to be. However other implementations like +# PyPy may call destructors latter, causing different output. +from platform import python_implementation +if python_implementation() == 'CPython': + def gcollect(): + pass +else: + import gc + def gcollect(): + gc.collect() + + run = spot.translate('a & !b').accepting_run() b = run.prefix[0].label c = buddy.bdd_satone(b) @@ -43,12 +56,15 @@ while c != buddy.bddtrue: c = h tc.assertEqual(res, [0, -1]) +del res res2 = [] for i in run.aut.ap(): res2.append((str(i), run.aut.register_ap(i))) tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]") - +del res2 +del c +gcollect() f = spot.bdd_to_formula(b) tc.assertTrue(f._is(spot.op_And)) @@ -56,9 +72,50 @@ tc.assertTrue(f[0]._is(spot.op_ap)) tc.assertTrue(f[1]._is(spot.op_Not)) tc.assertTrue(f[1][0]._is(spot.op_ap)) tc.assertEqual(str(f), 'a & !b') +del f +gcollect() try: f = spot.bdd_to_formula(b, spot.make_bdd_dict()) sys.exit(2) except RuntimeError as e: tc.assertIn("not in the dictionary", str(e)) + +f = spot.bdd_to_cnf_formula(b) +tc.assertEqual(str(f), 'a & !b') + +del run +del f + +gcollect() + +f = spot.bdd_to_cnf_formula(buddy.bddtrue) +tc.assertEqual(str(f), '1') +del f +gcollect() + +f = spot.bdd_to_cnf_formula(buddy.bddfalse) +tc.assertEqual(str(f), '0') +del f +gcollect() + +aut = spot.translate('(a & b) <-> c') +# With pypy, running GC here will destroy the translator object used +# by translate(). That object has temporary automata that reference +# the BDDs variables and those affect the order in which the +# bdd_to_formula() result is object is presented. The different order +# is not wrong, but it makes it diffuclt to write tests. +gcollect() + +for e in aut.out(aut.get_init_state_number()): + b = e.cond + break + +f1 = spot.bdd_to_formula(b) +tc.assertEqual(str(f1), '(!a & !c) | (a & b & c) | (!b & !c)') +f2 = spot.bdd_to_cnf_formula(b) +tc.assertEqual(str(f2), '(a | !c) & (!a | !b | c) & (b | !c)') + +b1 = spot.formula_to_bdd(f1, spot._bdd_dict, aut) +b2 = spot.formula_to_bdd(f2, spot._bdd_dict, aut) +tc.assertEqual(b1, b2)