SMT and Transition Systems

Time to use Z3 again: let's try to assert our transition relation so that we can use Z3 to answer questions about the system. To do this, we need to write our transition relation in SMT-LIB 2.

There's two new aspects of SMT-LIB 2 that will make things easier for us. First, SMT-LIB identifiers can be quoted which means they can have form |...| where ... is a sequence of pretty much any character but |. This is convenient as it allows us to write, for example, identifiers such as |s'.is_counting|. This will make things more readable, hopefully.

Second, SMT-LIB 2 allows us to define functions using the define-fun command. Its shape is

(define-fun <ident> ( <args> ) <type>
	<expression>
)

where <args> is zero or more arguments (<ident> <type>). For example:

(define-fun add_1 ( (n Int) ) Int
	(+ n 1)
)
(define-fun is_even ( (n Int) ) Bool
	(= (mod n 2) 0)
)

(declare-const n Int)
(assert
	(is_even (add_1 n))
)

; Is there an `n` such that `n + 1` is even? (yes)
(check-sat)
(get-model)

Running Z3, we obtain

> z3 test.smt2
sat
(
  (define-fun n () Int
    (- 1))
)

So, let's define a function for our transition relation. The definition is a bit daunting because, again, SMT-LIB 2 is really designed to be parsed by solvers. Human readability is not the main concern, but relatively small examples are quite readable if indented properly.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

Full code in the Version 1 section below.

Now, if we want to use this transition relation function, we need to give ourselves actual state variables to apply it to. Let's switch notation to prepare for the more complex manipulations we will soon investigate. Let's distinguish state variables using indices: instead of referring to s and s' to distinguish between previous and next state, let's just say we have a state of index 0 and another one of index 1. So, instead of writing s.cnt and s'.cnt we can just write cnt_0 and cnt_1 respectively.

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

We can now assert our transition relation over these two states, i.e. force state 1 to be a successor of state 0.

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

Nice 😸. Let's see if we can force state 0 and the inputs of state 1 to have Z3 produce a new state that's a successor of state 0. For instance,

• state 0: cnt is strictly greater than 7 and is_counting is false;
• state 1: start_stop is pressed and reset is not.

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    start_stop_1
    (not reset_1)
))

(check-sat)
(get-model)

The check-sat command asks Z3 whether there exists a valuation of all state variables verifying all our constraints. Said constraints include that state 1 must be a legal successor of state 0.

Full code in the Version 1 section below.

> z3 test.smt2
sat
(
  (define-fun cnt_0 () Int
    8)
  (define-fun reset_1 () Bool
    false)
  (define-fun start_stop_1 () Bool
    true)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun cnt_1 () Int
    9)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

It works. In this model (yours might differ), Z3 decided to have cnt_0 be 8 which, given all the constraints, means that cnt_1 is 9. This is because is_counting_1 is true, which is a consequence of the last assertion we wrote (is_counting_0 is false and start_stop_1 is true).

Maybe we can ask for something more interesting, i.e. maybe we can actually prove something. Let's modify our last assertion: we keep the constraints over state 0 and replace state 1's by cnt_1 must be 0.

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
))

(check-sat)
(get-model)

Note that this assertion replaces the one above where we constrained state 1's inputs.

The question we are asking Z3 is now "say cnt > 7 and we're not counting; is it possible then to have cnt = 0 in one transition?".

Full code in the Version 2 section below.

sat
(
  (define-fun start_stop_1 () Bool
    true)
  (define-fun reset_1 () Bool
    true)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun cnt_0 () Int
    8)
  (define-fun cnt_1 () Int
    0)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Z3 answers "yes" (sat), and shows us that by pressing reset in state 1, then we have cnt = 0. That's fair, but what if we don't allow reset to be pressed in state 1?

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
    (not reset_1)
))

(check-sat)

Readers comfortable with our toy stopwatch system know this should not be possible. If reset is not pressed, cnt can only increase or stay the same depending on whether the system is counting.

Humans (us) "knowing" this is not possible is not very valuable, as humans are notoriously great at being wrong. Let's just ask Z3 to prove (or disprove) what we know.

Full code in the Version 1 section below.

> z3 test.smt2
unsat

So, Z3's answer is that "there exists no valuation of the state variables verifying these constraints". That is, given the constraints on state 0, it is not possible to reach a state where cnt = 0 and reset is not pressed in one transition.

We can see this result as a consequence of a more abstract property of the system. That is, there are only three possible cnt values in the successor of any given state. Given cnt_0, cnt_1 can only be 0, cnt_0, or cnt_0 + 1.

Exercise: have Z3 prove this property by rewriting the last assertion of Version 3. Check out Version 4 for the solution. Hint below.

Full Code For All Examples

Version 1

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    start_stop_1
    (not reset_1)
))

(check-sat)
(get-model)

> z3 test.smt2
sat
(
  (define-fun cnt_0 () Int
    8)
  (define-fun reset_1 () Bool
    false)
  (define-fun start_stop_1 () Bool
    true)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun cnt_1 () Int
    9)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Version 2

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
))

(check-sat)
(get-model)

> z3 test.smt2
sat
(
  (define-fun start_stop_1 () Bool
    true)
  (define-fun reset_1 () Bool
    true)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun cnt_0 () Int
    8)
  (define-fun cnt_1 () Int
    0)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Version 3

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
    (not reset_1)
))

(check-sat)

> z3 test.smt2
unsat

Version 4

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert
    ; negate what we want to prove
    (not
        ; three possible values for `cnt_1` (not necessarily different)
        (or
            (= cnt_1 0)
            (= cnt_1 cnt_0)
            (= cnt_1 (+ cnt_0 1))
        )
    )
)

(check-sat)

> z3 test.smt2
unsat