G1 Clause Meanings

• The first part guarantees that at each time i, MX is in at least one state.

• The second part (with the paired barred variables) guarantees that MX is not in more than one state at time i.

• The time i runs from 0 through p(n)

Previous slide

Next slide

Back to first slide

View graphic version