Verificación y Validación de Software
Entrada 4
Entrada 4
¿Qué es un BDD y un ROBDD?
Un Diagrama de Decisión Binario (Binary Decision Diagram o BDD) es un grafo acíclico dirigido con: (a) Uno o dos nodos terminales etiquetados con 0 o 1. (b) Un conjunto de nodos variables con dos hijos. Cada nodo variable está etiquetado con un símbolo proposicional. [1]
Otro término relacionado con los diagramas de decisión son el Diagrama de Decisión Binario Reducido Ordenado (Reduced Ordered Binary Decision Diagram o ROBDD). Una ventaja de un ROBDD es que es único para una función particular y un orden de variables. Esta propiedad es útil por ejemplo en la verificación de funciones de equivalencia. [2]
Reducir un BDD a un ROBDD
Las instrucciones que se nos dieron de tarea para esta publicación, fueron las siguientes.
- Inventen una expresión Booleana (usando por mínimo 3 variables y 4 conectivos básicos).
- Construyan y dibujen su BDD.
- Reduzcan el BDD resultante a un ROBDD.
- Dibujen el ROBDD resultante.
Expresión Booleana
[(A∧D) ∧ (¬B∧¬D)] ∨ (B∨C)
Tabla de verdad
Con la tabla de verdad obtendremos los valores de salida para cada nodo al final del diagrama.
| A | B | C | D | [(A∧D) ∧ (¬B∧¬D)] ∨ (B∨C) |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 |
| 0 | 0 | 0 | 1 | 0 |
| 0 | 0 | 1 | 0 | 1 |
| 0 | 0 | 1 | 1 | 1 |
| 0 | 1 | 0 | 0 | 1 |
| 0 | 1 | 0 | 1 | 1 |
| 0 | 1 | 1 | 0 | 1 |
| 0 | 1 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 0 |
| 1 | 0 | 0 | 1 | 0 |
| 1 | 0 | 1 | 0 | 1 |
| 1 | 0 | 1 | 1 | 1 |
| 1 | 1 | 0 | 0 | 1 |
| 1 | 1 | 0 | 1 | 1 |
| 1 | 1 | 1 | 0 | 1 |
| 1 | 1 | 1 | 1 | 1 |
Para no tardar en hacer paso por paso la tabla de verdad, utilice de nuevo el programa en python para obtener la salida final de la tabla de verdad y que ya he usado en las tareas anteriores.
Dibujo del BDD
Ahora dibujamos el diagrama de decisión con las salidas obtenidas en la tabla de verdad.
La reducción la hice por pasos iniciando desde abajo del diagrama. En este caso vemos que las salidas de 0 o 1 en los nodos marcados como D, fueron simplificados dejando solo una salida por cada uno de ellos, ya que eso era posible al tener pares de ceros y unos.
Ahora subiendo al nivel de C, podemos eliminar todas los nodos en D que están repetidos, y las líneas que surgen de C dirigen solo a un nodo D, ya que tiene la misma salida.
Ahora al subir a los nodos B, podemos notar a simple vista que todo los nodos bajo ellos son iguales, por lo que podemos eliminar una rama completa y unir la línea que queda libre en el nodo A hacia el B que dejamos.
Con esto ya tenemos nuestro diagrama de decisión binario reducido y ordenado.
Dibujo del ROBDD
Nota: Las líneas punteadas en el diagrama significan que que el valor que toma el nodo del que sale es un cero, mientras que las líneas continuas son unos. Y las cajas de color naranja es la salida que arroja un cierto camino por el diagrama y que siempre termina en 0 o 1.
Recursos consultados:
[1] - Lógica y Programación - Diagramas de Decisión Binarios - PDF
[2] - Diagrama de Decisión Binario
Ramon, al inicio cuando comenzaste de abajo "D" puedes eliminar ese nodo cuando sus salidas son iguales, si su salida falsa o verdadera va a 0 o 1 se elimina. Entonces la arista bajaria directo al 0 o al 1. En tu primer imagen, el primero de la izquierda va a falso los dos, eliminarias D y bajaria directo desde C. Y asi sucesivamente. Eso afectaria a tu diagrama final, quitas el nodo D que va a 0 y baja directo de C.
ResponderEliminarPues, puede dejar un nodo D cuyo valor no importa; el valor de la variable A tampoco importa ;) Pero en sí se haría más mínimo quitando todo lo que no importa. Está bien para la tarea; 10 pts.
ResponderEliminar