Lines Matching defs:create
339 ;; Now let us try to create a Kripke Structure from the circuit. We need to
353 ;; Now we create all the states of the model.
355 (defun create-all-evaluations (vars states)
357 (let ((rec-states (create-all-evaluations (cdr vars) states)))
361 ;; Now let us create the label function.
370 (defun create-label-fn (states vars label)
372 (create-label-fn (rest states) vars
410 (defun create-next-states-of-p (p states vars equations)
413 (cons (first states) (create-next-states-of-p
415 (create-next-states-of-p p (rest states) vars equations))))
417 (defun create-next-states (states states-prime vars equations)
420 (create-next-states (rest states) states-prime vars equations)
422 (create-next-states-of-p (first states) states-prime vars equations))))
424 (defun create-kripke (C)
428 (let* ((states (create-all-evaluations vars (list ())))
429 (label-fn (create-label-fn (set-union initial-states states) vars ()))
430 (transition (create-next-states (set-union initial-states states)
522 (c-bisim-equiv (create-kripke C)
523 (create-kripke (cone-of-influence-reduction C vars))
530 (defthm create-kripke-produces-circuit-model
532 (circuit-modelp (create-kripke C))))
546 ;; quantifying, we create such a state (for m to n) and (n to m).