; trap(x) holds iff Q_x is a trap
(define-fun trap ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)) Bool
  ; Code here for "Q_x is a trap"
)

; mintrap(x) holds iff Q_x is a minimal trap
(define-fun mintrap ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)) Bool
  (and
    ; Code here for "Q_x is a trap"
    ; Code here for "Q_x is non empty"
    (forall ((y1 Bool) (y2 Bool) (y3 Bool) (y4 Bool))         ; Every strict subset of Q_x is not a trap
      (=>
        (and
          ; Code here for "Q_y is non empty"
          ; Code here for "Q_y subset of Q_y"
          ; Code here for "Q_y != Q_x"
        )
        ; Code here for "Q(y) is not a trap"
      )
    )
  )
)

; constraints(x, M) holds iff "Q_x marks M_0" implies "Q_x marks M"
(define-fun constraints ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool)
                         (m1 Int) (m2 Int) (m3 Int) (m4 Int)) Bool
  (=>
    ; Code here for "Q_x is marked in M_0, i.e. contains place p1 or p4"
    ; Code here for "Some place of Q_x is marked in M"
  )
)

; mreach(m) holds iff there is a solution of the marking equation
; from (2, 0, 0, 1) thats leads to m
(define-fun mreach ((m1 Int) (m2 Int) (m3 Int) (m4 Int)) Bool
  (exists ((t1 Int) (t2 Int) (t3 Int) (t4 Int) (t5 Int))
    (and
      (>= t1 0)
      (>= t2 0)
      (>= t3 0)
      (>= t4 0)
      (>= t5 0)
      ; Code here for the marking equation
    )
  )
)

; There exists a solution to the marking equation
(declare-const m1 Int)
(declare-const m2 Int)
(declare-const m3 Int)
(declare-const m4 Int)

(assert (>= m1 0))
(assert (= m2 2))
(assert (>= m3 1))
(assert (>= m4 0))
(assert (mreach m1 m2 m3 m4))


; The reachable marking satisfies minimal trap constraints
;; (In general, non minimal trap constraints may be necessary
;;  to disprove reachability, but here it's not the case.
;;  You may simply replace "mintrap" by "trap" below.)
(assert
  (forall ((x1 Bool) (x2 Bool) (x3 Bool) (x4 Bool))
    (=>
      (mintrap x1 x2 x3 x4)
      (constraints x1 x2 x3 x4 m1 m2 m3 m4)      
    )
  )
)

(check-sat)