;;(C) Copyright IBM Corp. 1992
;; This file is included in the IBM Research Report RT0084,
;; "Task-Specific Language Constructs for Describing Constrints in
;;  Job Assignment Probelms" by T.Hama, M.Hori, and Y.Nakamura.
;;

(in-package "ONTOLINGUA-USER")

(define-theory JOB-ASSIGNMENT-TASK (jat-generic)
    "This theory defines a task ontology for the job assignment task.
The job assignment task, which is a class of sheduling problems, is a
problem of assigning all given jobs to the available resources within
the time range, while satisfying various constraints.
This theory is based on Ontolingua V 3.0")

(in-theory 'JOB-ASSIGNMENT-TASK)

;;
;; Generic classes for assignemnt task
;;
(define-class ASSIGNMENT-OBJECT (?object)
    "ASSIGNMENT-OBJECT denotes an object appearing generally in
assignment problems."
    :def (individual ?object)
    :axiom-def (subclass-partition
		ASSIGNMENT-OBJECT
		(setof source target))
)

(define-class SOURCE (?source)
    "SOURCE denotes an object to be assigned to an object of TARGET."
    :def (assignment-object ?source)
)

(define-class TARGET (?target)
    "TARGET denotes an object to which an object of SOURCE is to be
assigned."
    :def (assignment-object ?target)
)

(define-function ASSIGNMENT (?source) :-> ?target
    "ASSIGNMENT denotes a mapping from SOURCE to TARGET."
    :def (and (source ?source)
	      (target ?target))
)


;;
;; Definitons related to JOB
;;

(define-class JOB (?job)
    "JOB is an abstract class that denotes an object to be assigned to
     a resource, or a collection of such objects."
    :def (source ?job)
)

(define-class TEMPORALLY-FIXED-JOB-CLASS (?class)
    "TEMPORALLY-FIXED-JOB-CLASS denotes a job whose assignment to a
time range is predefined."
    :iff-def (and (class ?class)
		  (subclass-of ?class job)
		  (slot-cardinality ?class assigned-time-range 1))
)

(define-class FIXED-LENGTH-JOB-CLASS (?class)
    "FIXED-LENGTH-JOB-CLASS  denotes a job whoes length is independent
of a resource and fixed."
    :iff-def (and (class ?class)
		  (subclass-of ?class job)
		  (slot-cardinality ?class fixed-length-job.length 1))
)

(define-class UNIT-LENGTH-JOB-CLASS (?class)
    "UNIT-LENGTH-JOB denotes a job whose length is the same."
    :iff-def (and (fixed-length-job-class ?class)
		  (= (value-cardinality ?class JOB-UNIT-LENGTH) 1)
		  (forall ?i (=> (instance-of ?i ?class)
				 (= (fixed-length-job.length ?i)
				    (job-unit-length ?class)))))
)

(define-function JOB-UNIT-LENGTH (?job-class) :-> ?length
    "Each job class of unit-length-job-class has its own length."
    :def (and (unit-length-job-class ?job-class)
	      (duration ?length))
)
		 
(define-function JOB.LENGTH (?job ?res) :-> ?length
    "JOB.LENGTH returns a duration of the job."
    :def (and (job ?job)
	      (resource ?res)
	      (duration ?length))
)    

(define-function FIXED-LENGTH-JOB.LENGTH (?job) :-> ?length
    "FIXED-LENGTH-JOB.LENGTH returns a duration of the job. The length
does not depend on resources."
    :def (and (job ?job)
	      (duration ?length))
)    

(define-function JOB.TIME-RANGE (?job) :-> ?time-range
    "JOB-TIME-RAGNE returns a time range where a job is permitted to
     be assigned"
    :def (and (job ?job)
	      (time-range ?time-range))
)

;;
;; Definitions related to RESOURCE
;;

(define-class RESOURCE (?resource)
    "RESOURCE is an abstract class that denotes an object to which a
     job is assigned, or a collection of such objects."
    :def (target ?resource)
)

;;
;; Definition for TIME-RANGE 

(define-class JAT-TIME-RANGE (?time-range)
    "JAT-TIME-RANGE denotes a time range which is referred to in the
job assignment task."
    :def (and (time-range ?time-range)
	      (target ?time-range))
)

(define-class DISCRETE-TIME-RANGE-CLASS (?class)
    "DISCRETE-TIME-RANGE-CLASS denotes a time range whose start time
and end time are measured by a time-range-unit."
    :iff-def (and (class ?class)
		  (= (value-cardinality ?class TIME-RANGE-UNIT) 1)
		  (forall ?i (=> (instance-of ?i ?class)
				 (and (measured-by
				       (time-range.start-time ?i)
				       (time-range-unit ?class))
				      (measured-by
				       (time-range.end-time ?i)
				       (time-range-unit ?class))))))
)

(define-function TIME-RANGE-UNIT (?tr-class) :-> ?unit
    "A time-range class of discrete-time-range-class has its own
minimun unit of duration."
    :def (and (discrete-time-range-class ?tr-class)
	      (duration ?unit))
)

(define-relation MEASURED-BY (?tp ?unit)
    "A time point ?tp can be measured by a unit of duration ?unit."
    :def (and (time-point ?tp)
	      (duration ?unit))
)
 
(define-class UNIT-TIME-RANGE-CLASS (?class)
    "UNIT-TIME-RANGE-CLASS deontes a time ragne whose duration is a
unit length."
    :iff-def (and (discrete-time-range-class ?class)
		  (forall ?i (=> (instance-of ?i ?class)
				 (= (time-range.duration ?i)
				    (time-range-unit ?class)))))
)


;;
;; Definition for ASSIGNMENT
;;

(define-function ASSIGNED-RESOURCE (?job) :-> ?res
    "ASSIGNED-RESOURCE returns a resouce to which a job is assinged."
    :def (and (job ?job)
	      (resource ?res))
    :axiom-def (subrelation-of assigned-resource assignment)
)

(define-function ASSIGNED-TIME-RANGE (?job) :-> ?time-range
    "ASSIGNED-TIME_RANGE returns a time range to which a job is assigned."
    :def (and (job ?job)
	      (jat-time-range ?time-range))
    :axiom-def (subrelation-of assigned-time-range assignment)
)