eas-fnf-enc.smt2

(set-logic ALL)

;(set-option :finite-model-find true)

(set-option :fmf-bound true)
(set-option :fmf-fun true)
(set-option :produce-models true)


; Declare Variable Sort
(define-sort VarId () Int)

; Declare Unary Operators.
(declare-datatype UNARY_OP ( (NOT) (Y) (G) (H) (O) ))

; Declare Binary Operators.
(declare-datatype BINARY_OP ( (AND) (OR) (IMPLIES) (S) ))

; Formula Declaration.
(declare-datatype Formula (
  (Top)
  (Bottom) 
  (P (Id VarId))
  (Op1 (op1 UNARY_OP) (f Formula))
  (Op2 (op2 BINARY_OP) (f1 Formula) (f2 Formula))
  )
)

;Trace Constructs
(define-sort Trace () Int)
(define-sort Time () Int)

(define-fun len ((tr Trace)) Int 
    (ite (= tr 1) 4 
    (ite (= tr 2) 4 
    (ite (= tr 3) 4 
    (ite (= tr 4) 1 
    (ite (= tr 5) 2 
    (ite (= tr 6) 4 
    (ite (= tr 7) 4 
    (ite (= tr 8) 4 
    (ite (= tr 9) 4 0)))))))))
)

(define-fun val ((tr Trace) (t Time) (x VarId)) Bool
    (or 
    (and (= tr 1) (= t 0) (= x 0))
    (and (= tr 1) (= t 0) (= x 1))
    (and (= tr 1) (= t 1) (= x 1))
    (and (= tr 2) (= t 0) (= x 0))
    (and (= tr 2) (= t 1) (= x 1))
    (and (= tr 2) (= t 2) (= x 1))
    (and (= tr 2) (= t 3) (= x 0))
    (and (= tr 2) (= t 3) (= x 1))
    (and (= tr 2) (= t 4) (= x 1))
    (and (= tr 3) (= t 1) (= x 0))
    (and (= tr 3) (= t 2) (= x 1))
    (and (= tr 3) (= t 4) (= x 0))
    (and (= tr 3) (= t 4) (= x 1))
    (and (= tr 4) (= t 0) (= x 0))
    (and (= tr 4) (= t 1) (= x 0))
    (and (= tr 5) (= t 0) (= x 0))
    (and (= tr 5) (= t 2) (= x 0))
    (and (= tr 6) (= t 0) (= x 0))
    (and (= tr 6) (= t 0) (= x 1))
    (and (= tr 6) (= t 2) (= x 0))
    (and (= tr 6) (= t 3) (= x 0))
    (and (= tr 6) (= t 3) (= x 1))
    (and (= tr 6) (= t 4) (= x 0))
    (and (= tr 7) (= t 0) (= x 1))
    (and (= tr 7) (= t 1) (= x 0))
    (and (= tr 7) (= t 1) (= x 1))
    (and (= tr 7) (= t 2) (= x 1))
    (and (= tr 7) (= t 3) (= x 0))
    (and (= tr 7) (= t 4) (= x 0))
    (and (= tr 8) (= t 1) (= x 0))
    (and (= tr 8) (= t 2) (= x 0))
    (and (= tr 8) (= t 2) (= x 1))
    (and (= tr 8) (= t 3) (= x 0))
    (and (= tr 8) (= t 4) (= x 0))
    (and (= tr 8) (= t 4) (= x 1))
    (and (= tr 9) (= t 0) (= x 1))
    (and (= tr 9) (= t 2) (= x 1))
    (and (= tr 9) (= t 3) (= x 0))
    (and (= tr 9) (= t 3) (= x 1))
    (and (= tr 9) (= t 4) (= x 0))
    (and (= tr 9) (= t 4) (= x 1)))
)

(define-fun-rec holds ((f Formula) (tr Trace) (t Time)) Bool
  (let ((tn (len tr))) 
    (and (<= 0 t tn)
       (match f (

         (Top true)
         
         (Bottom false)
       
         ((P i) (val tr t i))
      
         ((Op1 op g) 
           (match op (
             (NOT (not (holds g tr t))) 

             (Y (and (< 0 t) (holds g tr (- t 1))))    

             (H (and (holds g tr t) (or (= t 0) (holds f tr (- t 1)))))

             (O (or  (holds g tr t) (and (< 0 t) (holds f tr (- t 1)))))

             (G (and (holds g tr t) (or (= t tn) (holds f tr (+ t 1)))))

          )))

         ((Op2 op f1 g)     
           (match op (
             (AND (and (holds f1 tr t) (holds g tr t)))

             (OR  (or (holds f1 tr t) (holds g tr t)))
             
             (IMPLIES (or (not (holds f1 tr t)) (holds g tr t)))

             (S  (or (holds g tr t) (and (holds f1 tr t) (and (< 0 t) (holds f tr (- t 1))))))

         )))))
    )
  )
)


(declare-const phi Formula)

(define-fun-rec holds-for-all-traces ((tr Trace) (f Formula)) Bool
  (or (< tr 1)
    (and (holds (Op1 G f) tr 0)
         (holds-for-all-traces (- tr 1) f))
  )
)

(define-const pos_tr Int 3)


(assert (holds-for-all-traces pos_tr phi))

(define-fun-rec fail-for-all-traces ((tr Trace) (f Formula)) Bool
  (or (<= tr pos_tr)
    (and (not (holds (Op1 G f) tr 0))
         (fail-for-all-traces (- tr 1) f))
  )
)

(assert (fail-for-all-traces 9 phi))


(check-sat)

(get-value (phi))
;Example Formula:
;(Infix)  failure => !(Y(!(alarm) S failure))
;(Prefix) =>(failure, !(Y(S(!(alarm), failure)))