Module 7 — Compute the reachable states of a design · Binary Decision Diagrams with CUDD

formal.org
Binary Decision Diagrams with CUDD

Module 7 — Compute the reachable states of a designState encoding, transition relations, images as relational products, frontiers and fixpoints, the order of current and next states, and counterexamples to invariants.Katas in this module (4)

Kata 7.1 — Make a counter reach exactly 5 states

Kata 7.2 — Open the lock

Kata 7.3 — Name what a preimage step quantifies

Kata 7.4 — Reach every state in two steps

Part of Binary Decision Diagrams with CUDD on formal.org.