;; These functions are used in the compositional model-checking work to prove
;; compositional reductions. These are only for reference purposes and might
;; sometimes be simplified, but the essence of each function is in here.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++ Properties of ltl syntax ++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++


;; So an LTL formula is either (i) a constant 'True or 'False, (ii) a variable
;; which is a quote or a symbol other than the LTL operator symbol, or of the
;; form (P + Q), (P & Q), (P U Q), (P W Q), (~ P), (F P), (G P), (X P), where P
;; and Q are LTL formulas.


(defun ltl-formulap (f)
  (cond ((atom f) (or (ltl-constantp f)
                      (ltl-variablep f)))
        ((equal (len f) 3)
         (and (memberp (second f) '(+ & U W))
              (ltl-formulap (first f))
              (ltl-formulap (third f))))
        ((equal (len f) 2)
         (and (memberp (first f) '(~ X F G))
              (ltl-formulap (second f))))
        (t nil)))

;; A formula is called resctricted with respect to a collection vars of
;; variables if it mentions no variable other than those in vars. Here is the
;; recursive definition.

(defun restricted-formulap (f v-list)
  (cond ((atom f) (or (ltl-constantp f) 
                      (and (ltl-variablep f)
                           (memberp f v-list))))
        ((equal (len f) 3) (and (memberp (second f) '(& + U W))
                                (restricted-formulap (first f) v-list)
                                (restricted-formulap (third f) v-list)))
        ((equal (len f) 2) (and (memberp (first f) '(~ X F G))
                                (restricted-formulap (second f) v-list)))
        (t nil)))))

;; Now we show the obvious thing that a restricted formula is also an ltl
;; formula.

(defthm restricted-formula-is-an-ltl-formula
  (implies (restricted-formulap f v-list)
           (ltl-formulap f))
  :rule-classes :forward-chaining)

;; Given an LTL formula, can we create a v-list such that the LTL-formula is a
;; restricted formula over the variables in v-list? The function
;; create-restricted-var-set attempts that.

(defun create-restricted-var-set (f)
  (cond ((atom f) (if (ltl-constantp f) nil (list f)))
        ((equal (len f) 3) (set-union (create-restricted-var-set (first f))
                                      (create-restricted-var-set (third f))))
        ((equal (len f) 2) (create-restricted-var-set (second f)))
        (t nil)))  

;; And show that we have been successful

(defthm ltl-formula-is-a-restricted-formula
  (implies (ltl-formulap f)
           (restricted-formulap f (create-restricted-var-set f)))
  :rule-classes :forward-chaining)

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++ The LTL semantics function ++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

(mutual-recursion

(defun ltl-periodic-path-semantics (f init prefix cycle label)
  (cond ((atom f)
         (if (ltl-constantp f) 
             (equal f 'true)
           (memberp f (<- label init))))
        ((equal (len f) 3)
         (case (second f)
           (& (and (ltl-periodic-path-semantics (first f) init prefix cycle
                                                label)
                   (ltl-periodic-path-semantics (third f) init prefix cycle
                                                label)))
           (+ (or (ltl-periodic-path-semantics (first f) init prefix cycle
                                               label)
                  (ltl-periodic-path-semantics (third f) init prefix cycle
                                               label)))
           (U (let* ((found-and-index
                      (find-state-satisfying-formula 
                       (third f) init prefix cycle label
                       (+ 1 (len prefix) (len cycle))))
                     (found (first found-and-index))
                     (index (second found-and-index))) 
                (if (not found) 
                    nil
                  (ltl-periodic-path-semantics* (first f) init prefix
                                                cycle label index))))
           (W (let* ((found-and-index
                      (find-state-satisfying-formula 
                       (third f) init prefix cycle label
                       (+ 1 (len prefix) (len cycle))))
                     (found (first found-and-index))
                     (index (second found-and-index)))
                (if (not found) 
                    (ltl-periodic-path-semantics* (first f) init prefix
                                                  cycle label
                                                  (+ 1 (len prefix) (len cycle)))
                  (ltl-periodic-path-semantics* (first f) init prefix
                                                cycle label index))))
           (t nil)))
        ((equal (len f) 2)
         (case (first f)               
           (~ (not (ltl-periodic-path-semantics (second f) init prefix cycle
                                                label)))
           (G  (ltl-periodic-path-semantics* (second f) init prefix
                                             cycle label
                                             (+ 1 (len prefix) (len cycle))))
           (F (let* ((found-and-index
                      (find-state-satisfying-formula 
                       (second f) init prefix cycle label
                       (+ 1 (len prefix) (len cycle))))
                     (found (first found-and-index)))
                (if found t nil)))
           (X (ltl-periodic-path-semantics (second f) (first prefix)
                                           (if (endp (rest prefix)) 
                                               cycle 
                                             (rest prefix))
                                           cycle
                                           label))
           (t nil)))
        (t nil)))

(defun ltl-periodic-path-semantics* (f init prefix cycle label dist)
  (if (zp dist) t
    (and (ltl-periodic-path-semantics f init prefix cycle label)
         (ltl-periodic-path-semantics* f (first prefix)
                                       (if (endp (rest prefix))
                                           cycle
                                         (rest prefix))
                                       cycle label (1- dist)))))

(defun find-state-satisfying-formula (f init prefix cycle label dist)
  (cond ((zp dist) (list nil 0))
        ((ltl-periodic-path-semantics f init prefix cycle label)
         (list t 0))
        (t (let* ((found-and-index
                      (find-state-satisfying-formula 
                        f (first prefix)
                        (if (endp (rest prefix)) cycle (rest prefix))
                        cycle label (1- dist)))
                  (found (first found-and-index))
                  (ndx (second found-and-index)))
             (list found (1+ ndx))))))

)

(defun ltl-ppath-semantics (f ppath m)
  (ltl-periodic-path-semantics f (initial-state ppath) 
                               (prefix ppath) (cycle ppath)
                               (label-fn m)))

(defun-sk ltl-semantics (f m)
  (forall ppath
          (implies (compatible-ppath-p ppath m)
                   (ltl-ppath-semantics f ppath m))))

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++ Bisimilarity Arguments +++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

(encapsulate
 (((bisimilar * * * * *) => *)
  ((bisimilar-transition-witness-m->n * * * * * *) => *)
  ((bisimilar-initial-state-witness-m->n * * * *) => *)
  ((bisimilar-transition-witness-n->m * * * * * *) => *)
  ((bisimilar-initial-state-witness-n->m * * * *) => *)
  ((bisimilar-equiv * * *) => *))

 (local
  (defun bisimilar (p m q n vars)
    (declare (ignore vars))
    (and (equal p q)
         (equal m n)))
  )

 (local
  (defun bisimilar-transition-witness-m->n (p r m q n vars)
    (declare (ignore p m q n vars))
    r)
  )

 (local
  (defun bisimilar-initial-state-witness-m->n (s m n vars)
    (declare (ignore m n vars))
    s)
  )


 (local
  (defun bisimilar-transition-witness-n->m (p m q r n vars)
    (declare (ignore p m q n vars))
    r)
  )

 (local
  (defun bisimilar-initial-state-witness-n->m (m s n vars)
    (declare (ignore m n vars))
    s)
  )

 (local
  (defun bisimilar-equiv (m n vars)
    (declare (ignore vars))
    (equal m n))
  )


 ;; If two Kripke Structures m and n are equivalent with respect to a bisimilar
 ;; relation B, then for every initial-state of m there is a initial-state of n
 ;; that is bisimilar.

 (defthm bisimilar-equiv-implies-init->init-m->n
   (implies (and (bisimilar-equiv m n vars)
                 (memberp s (initial-states m)))
            (memberp (bisimilar-initial-state-witness-m->n s m n vars)
                     (initial-states n))))
 
 (defthm bisimilar-equiv-implies-bisimilar-initial-states-m->n
   (implies (and (bisimilar-equiv m n vars)
                 (memberp s (initial-states m)))
            (bisimilar s m 
                       (bisimilar-initial-state-witness-m->n s m n vars) 
                       n vars)))
 
 ;; And the same result holds for n to m
 
 (defthm bisimilar-equiv-implies-init->init-n->m
   (implies (and (bisimilar-equiv m n vars)
                 (memberp s (initial-states n)))
            (memberp (bisimilar-initial-state-witness-n->m m s n vars)
                     (initial-states m))))
 
 (defthm bisimilar-equiv-implies-bisimilar-initial-states-n->m
   (implies (and (bisimilar-equiv m n vars)
                 (memberp s (initial-states n)))
            (bisimilar (bisimilar-initial-state-witness-n->m m s n vars) 
                       m s n vars)))
 
 ;; Bisimilar states have the same label with respect to vars. I just use
 ;; set-equality because they might not have "equal" labels. BTW, I might not
 ;; need the modelp hypothesis here. But I plug it in, just so that I can keep
 ;; the (functional instance of) bisimilarity relation as simple as possible.
 
 (defthm bisimilar-states-have-labels-equal
   (implies (and (bisimilar p m q n vars)
                 (modelp m)
                 (modelp n))
            (set-equal (set-intersect (label-of p m) vars)
                       (set-intersect (label-of q n) vars))))
            
 
 
 ;; Of course bisimilarity witness is a member of states of the corresponding model.
 
 (defthm bisimilar-witness-member-of-states-m->n
   (implies (and (bisimilar p m q n vars)
                 (next-statep p r m)
                 (memberp r (states m)))
            (memberp (bisimilar-transition-witness-m->n p r m q n vars) 
                     (states n))))

 ;; Again this part may not be required. 

 (defthm bisimilar-witness-member-of-states-n->m
   (implies (and (bisimilar p m q n vars)
                 (next-statep q r n)
                 (memberp r (states n)))
            (memberp  (bisimilar-transition-witness-n->m p m q r n vars)
                      (states m))))

 ;; And if two states are bisimilar, then for every next state of one, there is
 ;; a next state of another which is bisimilar.

 (defthm bisimilar-witness-matches-transition-m->n
   (implies (and (bisimilar p m q n vars)
                 (next-statep p r m))
            (next-statep q (bisimilar-transition-witness-m->n p r m q n vars)
                         n)))

 (defthm bisimilar-witness-produces-bisimilar-states-m->n
   (implies (and (bisimilar p m q n vars)
                 (next-statep p r m))
            (bisimilar r m
                       (bisimilar-transition-witness-m->n p r m q n vars) 
                       n vars)))

 ;; Again this part may not be required. 

 (defthm bisimilar-witness-matches-transition-n->m
   (implies (and (bisimilar p m q n vars)
                  (next-statep q r n))
            (next-statep p (bisimilar-transition-witness-n->m p m q r n vars)
                         m)))



 (defthm bisimilar-witness-produces-bisimilar-states-n->m
   (implies (and (bisimilar p m q n vars)
                 (next-statep q r n))
            (bisimilar (bisimilar-transition-witness-n->m p m q r n vars) 
                       m r n vars)))

)

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++ Proofs on bisimilary ++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

;; The following function determines a weird path in n, when given a cycle in
;; m. The weird path is a finite path compatible with n, and can be thought of
;; as the append of the prefix and cycle.

(defun find-matching-prefix-and-cycle-for-cycle-m->n (cycle m seen q states n vars path)
  (declare (xargs :measure (nfix (- (1+ (len states)) (len seen)))))
  ;; for termination using Pigeon-hole arguments
  (if (< (len states) (len seen)) (mv seen q path) 
    (let* ((path-produced (find-matching-path-for-path-m->n 
                           cycle m q n vars))
           (node-witness (bisimilar-transition-witness-m->n
                          (last-val cycle) (first cycle) m 
                          (last-val path-produced) n vars)))
      (if (memberp node-witness seen)
          (mv (snoc seen node-witness) node-witness (append path path-produced))
        (find-matching-prefix-and-cycle-for-cycle-m->n cycle m (snoc seen node-witness) 
                                                       node-witness states n
                                                       vars (append path
                                                                    path-produced))))))

;; And we pick up the prefix from the weird path

(defun find-matching-prefix-for-cycle-m->n (cycle m q n vars)
  (mv-let (seen witness path)
          (find-matching-prefix-and-cycle-for-cycle-m->n 
           cycle m (list q) q (states n) n vars nil)
          (find-prefix cycle (del-last seen) witness path)))

; and also the cycle.

(defun find-matching-cycle-for-cycle-m->n (cycle m q n vars)
  (mv-let (seen witness path)
          (find-matching-prefix-and-cycle-for-cycle-m->n
           cycle m (list q) q (states n) n vars nil)
          (find-cycle cycle (del-last seen) witness path)))

(defun find-matching-periodic-path-m->n (ppath m n vars)
  (let* ((init-p (initial-state ppath))
         (prefix-p (prefix ppath))
         (first-p (first prefix-p)) 
         (cycle-p (cycle ppath))
         (init-q (bisimilar-initial-state-witness-m->n init-p m n vars))
         (first-q (bisimilar-transition-witness-m->n init-p first-p m init-q n
                                                     vars))
         (match-path (find-matching-path-for-path-m->n prefix-p m first-q n
                                                       vars))
         (last-p (last-val prefix-p))
         (last-q (last-val match-path))
         (first-cp (first cycle-p))
         (first-cq (bisimilar-transition-witness-m->n last-p first-cp m last-q
                                                      n vars))
         (match-prefix (find-matching-prefix-for-cycle-m->n
                        cycle-p m first-cq n vars))
         (match-cycle (find-matching-cycle-for-cycle-m->n
                       cycle-p m first-cq n vars)))
    (>_ :initial-state init-q
        :prefix (append match-path match-prefix)
        :cycle match-cycle)))