;;; -*- Mode:Common-Lisp; Package:DME-user; Base:10 -*-
;
;
; by Marcos Vescovi
; Design Verification Procedure
;
;

(in-package :dme-user)
(in-implementation #+clos-frames :Clos-And-Epikit #-clos-frames :epikit)
(in-theory *background-theory*)


(define-function DEVICE-FUNCTION (?name) :-> ?device-function)

(define-function CPD (?name) :-> ?cpd)

(define-function CPD-node (?name) :-> ?cpd-node)

(define-function CPD-arc (?name) :-> ?cpd-arc)

;;; Commented out by JPR.  Superseded by the above ^^^^^

;;=============================================================================
;;
;; Classes Definition
;;
;;=============================================================================

;;-----------------------------------------------------------------------------
;;
;; Define Device-Function =    Context : Device
;;                                       Set.of.Objects
;;                                       Conditions
;;
;;                                     +
;;
;;                             Formula on CPDs 
;;
;;-----------------------------------------------------------------------------
  
;(define-class DEVICE-FUNCTION (?function)
;  :Axiom-Def (dme-kernel-class DEVICE-FUNCTION)  
;  :def (and (has-one ?function device)
;	    (has-one ?function set.of.objects)
;	    (has-one ?function conditions)
;	    (has-one ?function formula.on.cpds)))

;;-----------------------------------------------------------------------------

;(define-function DEVICE (?function) :-> ?device
;     :def (and (device-function ?function)
;               (equal (type-of ?device) 'cons)))

;;
;; Example of (get-function-value ?function 'device) :
;;
;;          (REFRIGERATOR ?ref)
;;
;;

;;-----------------------------------------------------------------------------


;(define-function SET.OF.OBJECTS (?function) :-> ?set.of.objects
;     :def (and (device-function ?function)
;               (equal (type-of ?set.of.objects) 'cons)))

;;
;; Example of (get-function-value ?function 'set.of.objects) :
;;
;;          ((ROOM ?room)(FURNACE ?furn))
;;
;;

;;-----------------------------------------------------------------------------

;(define-function CONDITIONS (?function) :-> ?conditions
;     :def (and (device-function ?function)
;               (equal (type-of ?conditions) 'cons)))

;;
;; Example of (get-function-value ?function 'conditions) :
;;
;;        ((= (switch-of ?ref) on) (connected-to ?ref ?room))
;;
;;

;;-----------------------------------------------------------------------------

;(define-function FORMULA.ON.CPDS (?function) :-> ?form.cpds
;     :def (and (device-function ?function)
;               (or (equal (type-of ?form.cpds) 'cons)
;                   (cpd ?form.cpds))))

;;
;; Example of (get-function-value ?function 'formula.on.cpds) :
;;
;;        (or (some-time CPD1) (every-time (and CPD2 CPD3)))
;;
;;  equivalent to :  (or CPD1 (every-time (and CPD2 CPD3)))
;;
;;


;;-----------------------------------------------------------------------------
;;
;; Define CPD - Causal Process Description
;;
;;-----------------------------------------------------------------------------
  
;(define-class CPD (?cpd)
;  :Axiom-Def (dme-kernel-class CPD)  
;  :def (and (has-one ?cpd set.of.nodes)
;	    (has-one ?cpd set.of.arcs)
;	    (has-one ?cpd initial.arcs)
;	    (has-one ?cpd min.number.states) ))

;;-----------------------------------------------------------------------------
    
;(define-function SET.OF.NODES (?cpd) :-> ?set.of.nodes
;     :def (and (cpd ?cpd) 
;               (or (equal (type-of ?set.of.nodes) 'cons)
;                   (node ?set.of.nodes))))

;;-----------------------------------------------------------------------------
 
;(define-function SET.OF.ARCS (?cpd) :-> ?set.of.arcs
;     :def (and (cpd ?cpd) 
;               (or (equal (type-of ?set.of.arcs) 'cons)
;                   (null ?set.of.arcs))))

;;-----------------------------------------------------------------------------

;(define-function INITIAL.ARCS (?cpd) :-> ?initial.arcs
;     :def (and (cpd ?cpd) 
;               (or (equal (type-of ?initial.arcs) 'cons)
;                   (null ?initial.arcs))))

;;-----------------------------------------------------------------------------

;(define-function MIN.NUMBER.STATES (?cpd) :-> ?mns
;     :def (and (cpd ?cpd) 
;               (numberp ?mns)))

;;-----------------------------------------------------------------------------
;;
;; Define Nodes of a CPD
;;
;;-----------------------------------------------------------------------------

;(define-class NODE (?node)
;  :Axiom-Def (dme-kernel-class NODE)    
;  :def (and (has-one ?node logical.formula)
;	    (has-one ?node pointed.by)
;	    (has-one ?node can.be.inst.to)
;	    (has-one ?node sent.from.input)
;	    (has-one ?node transformed.formula)
;	    (has-one ?node graphical-representation)))

;;-----------------------------------------------------------------------------

;(define-function LOGICAL.FORMULA (?node) :-> ?log.for
;     :def (and (node ?node) 
;               (or (equal (type-of ?log.for) 'cons)
;                   (statement ?log.for))))
;;
;; Example of (get-function-value ?node 'logical.formula) :
;;
;;        (or Statement22 (and Statement43 Statement67))
;;
;;

;;-----------------------------------------------------------------------------

;(define-function POINTED.BY (?node) :-> ?pointed.by
;     :def (and (node ?node) (equal (type-of ?pointed.by) 'cons)))

;;
;; Function POINTED.BY ===> Data Structure for the
;; Design Verification Procedure
;;

;;-----------------------------------------------------------------------------

;(define-function CAN.BE.INST.TO (?node) :-> ?can.be
;     :def (and (node ?node) (equal (type-of ?can.be) 'cons)))

;;
;; Function CAN.BE.INST.TO ===> Data Structure for the 
;; Design Verification Procedure
;;

;;-----------------------------------------------------------------------------

;(define-function SENT.FROM.INPUT (?node) :-> ?s.f.i
;     :def (and (node ?node) (equal (type-of ?s.f.i) 'cons)))

;;
;; Function SENT.FROM.INPUT ===> Data Structure for the
;; Design Verification Procedure
;;

;;-----------------------------------------------------------------------------

;(define-function TRANSFORMED.FORMULA (?node) :-> ?tf
;     :def (and (node ?node) (equal (type-of ?tf) 'cons)))

;;
;; Function TRANSFORMED.FORMULA ===> Data Structure for the
;; Design Verification Procedure
;;


;;-----------------------------------------------------------------------------
;;
;; Define Statements of a Node
;;
;;-----------------------------------------------------------------------------

;(define-class STATEMENT (?statement)
;  :Axiom-Def (dme-kernel-class STATEMENT)      
;  :def (and (has-one ?statement set.of.vars)
;	    (has-one ?statement arit.formula) ))

;;-----------------------------------------------------------------------------

;(define-function SET.OF.VARS (?statement) :-> ?set.of.vars
;     :def (and (statement ?statement) (equal (type-of ?set.of.vars) 'cons)))

;;-----------------------------------------------------------------------------

;(define-function ARIT.FORMULA (?statement) :-> ?arit.form
;     :def (and (statement ?statement) (equal (type-of ?arit.form) 'cons)))

;;
;; Examples of (get-function-value ?statement 'arit.formula) :
;;
;;             (> (temp-of ?ref)
;;                (+ (pressure ?ref) (* (temp-of ?room)(temp-of ?cond))))
;;
;;             (connected-to ?ref ?room)
;;

;;-----------------------------------------------------------------------------
;;
;; Define Arcs of a CPD
;;
;;-----------------------------------------------------------------------------

;(define-class ARC (?arc)
;  :Axiom-Def (dme-kernel-class ARC)        
;  :def (and (has-one ?arc link.nodes)
;	    (has-one ?arc type)
;	    (has-one ?arc temporal)
;	    (has-one ?arc created)
;	    (has-one ?arc set.of.fragments)
;	    (has-one ?arc transformed.formula)
;	    (has-one ?arc graphical.articulation.points)))

;(define-function graphical.articulation.points (?arc) :-> ?graph.art.pts
;  :def (and (arc ?arc) (equal (type-of ?graph.art.pts) 'cons))
;  :axiom-def (dme-kernel-class graphical.articulation.points))



;;-----------------------------------------------------------------------------

;(define-function LINK.NODES (?arc) :-> ?ln
;     :def (and (arc ?arc)(equal (type-of ?ln) 'cons)))

;;
;;
;; Example of (get-function-value ?arc 'link.nodes) : (node1 node2)
;;
;;

;;-----------------------------------------------------------------------------

;(define-function TYPE (?arc) :-> ?type
;     :def (and (arc ?arc)
;               (or (equal ?type 'causal)
;                   (equal ?type 'temporal)
;                   (null ?type))))                 ;;?type = causal by default

;;-----------------------------------------------------------------------------

;(define-function TEMPORAL (?arc) :-> ?temporal
;     :def (and (arc ?arc)
;               (or (null ?temporal)             
;                   (equal ?temporal 'same-time)
;                   (equal ?temporal 'before) 
;                   (equal ?temporal 'not-after))))
;                   ;;?temporal = not-after by default
                                                                    
;;---------------------------------------------------------------------------- 
;(define-function CREATED (?arc) :-> ?created
;     :def (and (arc ?arc)(equal (type-of ?created) 'cons)))

;;
;; Example of (get-function-value ?arc 'created) :
;;
;;           (and (by-constraint-of ?ref)
;;                (or (by-activation-of Model-Fragment)
;;                    (with-participation-of ?Wall)))
;;

;;-----------------------------------------------------------------------------

;(define-function SET.OF.FRAGMENTS (?arc) :-> ?s.of.fr
;		   :def (and (arc ?arc)(equal (type-of ?s.of.fr) 'cons))) 


;;-----------------------------------------------------------------------------
;;
;; Define Variables - Behavior
;;
;;-----------------------------------------------------------------------------
  
;(define-class VARIABLE (?var)
;  :Axiom-Def (dme-kernel-class VARIABLE)          
;  :def (has-one ?var values))

;(define-function VALUES (?var) :-> ?values
;     :def (and (VARIABLE ?var)(equal (type-of ?values) 'cons)))


;;;; Don't delete this form-feed char.
;
;;;; 
;;;; Enable GNU Emacs version numbers.  Don't mess with these
;;;; lines, or we'll find you and we'll kill you...
;;;; 
;;;; Local Variables:
;;;; mode: lisp
;;;; version-control: t  
;;;; End: