tests/inputs/summary.lisp

145 (defmacro initial-states (m) `(<- ,m :initial-states))
154 (defun initial-statep (p m)
155   (memberp p (initial-states m)))
270        (subset (initial-states m) (states m))
283        (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
284        (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)))
293        (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
294        (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)
333   (and (only-evaluations-p (initial-states C) (variables C))
334        (strict-evaluation-list-p (variables C) (initial-states C))
427         (initial-states (initial-states C)))
429            (label-fn (create-label-fn (set-union initial-states states) vars ()))
430            (transition (create-next-states (set-union initial-states states)
431                                            (set-union initial-states states)
433       (>_ :states (set-union initial-states states)
434           :initial-states initial-states
502        :initial-states (corresponding-states (initial-states C) variables)
544 ;; spots.  For example, we have to say that for each initial state in
545 ;; m there is an initial state in n, that is bisim-equiv.  Instead of
548 (defun c-bisimilar-initial-state-witness-m->n (s m n vars)
550   (evaluation-eq-member s (initial-states n) vars))
552 (defun c-bisimilar-initial-state-witness-n->m (m s n vars)
554   (evaluation-eq-member s (initial-states m) vars))
568                 (memberp s (initial-states m)))
569            (memberp (c-bisimilar-initial-state-witness-m->n s m n vars)
570                     (initial-states n))))
574                 (memberp s (initial-states n)))
575            (memberp (c-bisimilar-initial-state-witness-n->m m s n vars)
576                     (initial-states m))))
578 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
580                  (memberp s (initial-states m)))
582                            (c-bisimilar-initial-state-witness-m->n s m n vars)
585 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
587                  (memberp s (initial-states n)))
588             (circuit-bisim (c-bisimilar-initial-state-witness-n->m m s n vars)