Lines Matching defs:initial
148 ;; record of states, initial-states, transition and label-fn.
150 (defmacro initial-states (m) `(<- ,m :initial-states))
156 ;; A periodic path is a record of initial-state, (finite) prefix, and (finite)
159 ;; NOTE TO MYSELF: The initial state might not be required. It is difficult to
161 ;; Professor Emerson talk about Kripke Structures with initial states and
162 ;; Kripke Structures without initial states (and so in Dr. Clarke's Book). I
163 ;; follow the "with initial states" in that jargon, though I do believe that we
164 ;; can modify the theorems for Kripke Structures "without initial states". The
166 ;; initial states" should not bother us at this time.
168 (defmacro initial-state (p) `(<- ,p :initial-state))
177 (defun initial-statep (p m)
178 (memberp p (initial-states m)))
183 (in-theory (disable next-statep initial-statep label-of))