(define-theory procedures (Planning))
(in-theory 'procedures)


(DEFINE-RELATION FOLLOWING-PHASE-OF (?A ?B) :IFF-DEF
 (AND (EXISTS (?C) (AND (TEMPORAL-PART-OF ?A ?C) (TEMPORAL-PART ?C ?B)))
      (TEMPORALIZED-ENTITY ?A)
      (TEMPORALIZED-ENTITY ?B)
      (FOLLOWS ?A ?B)
      (*PHASE ?A)
      (*PHASE ?B))
 :CONSTRAINTS (AND (*PHASE ?A) (*PHASE ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE FOLLOWING-PHASE-OF *PHASE)
      (DOMAIN FOLLOWING-PHASE-OF *PHASE)))
(DEFINE-RELATION PRECEDING-PHASE-OF (?A ?B) :IFF-DEF
 (AND (EXISTS ?U
       (AND (EXISTS (?D ?E ?F ?G)
             (AND (BEGINPOINT ?B ?G)
                  (DURATION-VALUE ?G ?F)
                  (ENDPOINT ?A ?E)
                  (TIME-VALUE ?E ?D)
                  (< ?D ?F)))
            (EXISTS (?H) (AND (THE-TIME-UNIT ?A ?H) (IDENTITY ?H ?U)))
            (EXISTS (?I) (AND (THE-TIME-UNIT ?B ?I) (IDENTITY ?I ?U)))))
      (EXISTS (?C) (AND (TEMPORAL-PART-OF ?A ?C) (TEMPORAL-PART ?C ?B)))
      (TEMPORALIZED-ENTITY ?A)
      (TEMPORALIZED-ENTITY ?B)
      (PRECEDES ?A ?B)
      (*PHASE ?A)
      (*PHASE ?B))
 :CONSTRAINTS (AND (*PHASE ?A) (*PHASE ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE PRECEDING-PHASE-OF *PHASE)
      (DOMAIN PRECEDING-PHASE-OF *PHASE)))
(DEFINE-RELATION PROCEDURAL-PROPERTY (?A ?B) :DEF
 (AND (TYPICALITY-PROPERTY ?A ?B) (PROCEDURE ?A)))
(DEFINE-RELATION _ABANDONED (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_ACTIVATED ?A ?B)")
            (HOLDS-AT ?K "(_ABANDONED ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _ABORTED-PROCEDURE (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_ACTIVATED ?A ?B ?C)")
            (HOLDS-AT ?K "(_ABORTED-PROCEDURE ?A ?B ?D)")))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _ACTIVATED (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_READY ?A ?B)")
            (HOLDS-AT ?K "(_ACTIVATED ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)
      (PROCEDURE ?A)
      (BOOLEAN ?B))
 :CONSTRAINTS (AND (PROCEDURE ?A) (BOOLEAN ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE _ACTIVATED BOOLEAN)
      (DOMAIN _ACTIVATED PROCEDURE)))
(DEFINE-RELATION _COMPLETED (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_ACTIVATED ?A ?B)")
            (HOLDS-AT ?K "(_COMPLETED ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _REACTIVATED (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_SUSPENDED ?A ?B)")
            (HOLDS-AT ?K "(_REACTIVATED ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)
      (PROCEDURE ?A)
      (BOOLEAN ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE _REACTIVATED BOOLEAN)
      (DOMAIN _REACTIVATED PROCEDURE)))
(DEFINE-RELATION _READY (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_RESERVED ?A ?B)")
            (HOLDS-AT ?K "(_READY ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _RECORDED (?A ?B) :DEF
 (AND (OR (_COMPLETED ?A ?B) (_ABANDONED ?A ?B) (_ABORTED-PROCEDURE ?A ?B))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _RESERVED (?A ?B) :DEF (PROCEDURAL-PROPERTY ?A ?B))
(DEFINE-RELATION _SUSPENDED (?A ?B) :DEF
 (AND (EXISTS (?Z ?K)
       (AND (INTERVAL ?Z)
            (INTERVAL ?K)
            (PROCEDURE ?A)
            (BOOLEAN ?B)
            (MEETS ?Z ?K)
            (HOLDS-AT ?Z "(_ACTIVATED ?A ?B)")
            (HOLDS-AT ?K "(_SUSPENDED ?A ?B)")))
      (PROCEDURAL-PROPERTY ?A ?B)))
(DEFINE-CLASS *EVENT (?SELF)
 "The class of phases, during which some changes
happen."
 :DEF
 (AND (EXISTS (?Y ?Z)
       (AND (SITUATION ?Y)
            (SITUATION ?Z)
            (CONTEXT-OF ?Y ?SELF)
            (EXISTS (?B) (AND (BEGINPOINT ?SELF ?B) (CO-OCCUR ?Y ?B)))
            (CONTEXT-OF ?Z ?SELF)
            (EXISTS (?C) (AND (ENDPOINT ?SELF ?C) (CO-OCCUR ?Z ?C)))
            (DIFFERENT ?Y ?Z)))
      (*PHASE ?SELF)
      (EXISTS (?A) (AND (TEMPORAL-PART-OF ?SELF ?A) (PROCESS ?A)))))
(DEFINE-CLASS *PHASE (?SELF)
 "The (reified) class of processes which are part of 
another process."
 :IFF-DEF
 (AND (PROCESS ?SELF)
      (EXISTS (?A) (AND (TEMPORAL-PART-OF ?SELF ?A) (PROCESS ?A))))
 :AXIOM-DEF (THE-ARCHETYPE *PHASE REIFIED-PROPERTY))
(DEFINE-CLASS *STATE (?SELF)
 "The class of phases, during which no changes
happen."
 :DEF
 (AND (EXISTS (?Y ?Z)
       (AND (SITUATION ?Y)
            (SITUATION ?Z)
            (CONTEXT-OF ?Y ?SELF)
            (EXISTS (?A) (AND (BEGINPOINT ?SELF ?A) (CO-OCCUR ?Y ?A)))
            (CONTEXT-OF ?Z ?SELF)
            (EXISTS (?B) (AND (ENDPOINT ?SELF ?B) (CO-OCCUR ?Z ?B)))
            (EQUAL-BUT-TIME ?Y ?Z)))
      (*PHASE ?SELF))
 :AXIOM-DEF (THE-ARCHETYPE *STATE REIFIED-PROPERTY))
(DEFINE-CLASS ACT-STAGE (?SELF)
 "An act stage is an act that constitutes a phase
of a procedure."
 :DEF
 (AND (STAGE ?SELF)
      (EXISTS (?A) (AND (TEMPORAL-PART-OF ?SELF ?A) (PROCEDURE ?A))))
 :CONSTRAINTS
 (EXISTS (?B)
         (AND (METHOD ?SELF ?B) (OR (SEQUENTIAL-PLAN ?B) (CYCLICAL-PLAN ?B))))
 :AXIOM-DEF (THE-ARCHETYPE ACT-STAGE REIFIED-PROPERTY))
(DEFINE-CLASS CASE-STAGE (?SELF)
:DEF
 (AND (PLANNING-STAGE ?SELF)
      (EXISTS (?A)
              (AND (MEETS ?SELF ?A)
                   (AND (STAGE ?A)
                        (FORALL (?B)
                         (=> (DEPENDENTLY-CO-EXIST ?A ?B)
                          (INCOHERENT ?B)))))))
 :CONSTRAINTS (EXISTS (?C) (AND (METHOD ?SELF ?C) (CASE-PLAN ?C))))
(DEFINE-CLASS CONCURRENT-STAGE (?SELF)
:DEF
 (AND (PLANNING-STAGE ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF MEETS 2))
 :CONSTRAINTS (EXISTS (?A) (AND (METHOD ?SELF ?A) (CONCURRENT-PLAN ?A))))
(DEFINE-CLASS INFORMATION-GATHERING (?SELF)
:DEF (PROCEDURE ?SELF))
(DEFINE-CLASS INFORMATION-STAGE (?SELF)
 "An information stage is an act -performed to gather 
information- that constitutes a phase of a procedure."
 :DEF
 (AND (ACT-STAGE ?SELF)
      (EXISTS (?A)
              (AND (CONVENTIONAL-GOAL ?SELF ?A) (INFORMATION-GATHERING ?A))))
 :AXIOM-DEF (THE-ARCHETYPE INFORMATION-STAGE REIFIED-PROPERTY))
(DEFINE-CLASS PARTLY-CONCURRENT-STAGE (?SELF)
:DEF
 (AND (PLANNING-STAGE ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF MEETS 3)
      (EXISTS (?A)
              (AND (MEETS ?SELF ?A)
                   (AND (STAGE ?A)
                        (FORALL (?B)
                         (=> (DEPENDENTLY-CO-EXIST ?A ?B)
                          (INCOHERENT ?B)))))))
 :CONSTRAINTS (EXISTS (?C) (AND (METHOD ?SELF ?C) (PARTLY-CONCURRENT-PLAN ?C))))
(DEFINE-CLASS PLANNING-STAGE (?SELF)
 "A stage performed to accomplish a branching
or a synchronization contained in a plan that constitutes the method of the procedure 
at hand."
 :DEF
 (AND (STAGE ?SELF)
      (EXISTS (?A) (AND (TEMPORAL-PART-OF ?SELF ?A) (PROCEDURE ?A))))
 :CONSTRAINTS
 (EXISTS (?B)
         (AND (METHOD ?SELF ?B) (OR (BRANCHING-PLAN ?B) (SYNCHRO-PLAN ?B))))
 :AXIOM-DEF (THE-ARCHETYPE PLANNING-STAGE REIFIED-PROPERTY))
(DEFINE-CLASS STAGE (?SELF)
 "A stage is a distinct phase of a procedure." :DEF
 (AND (ACTIVITY ?SELF)
      (EXISTS (?A) (AND (TEMPORAL-PART-OF ?SELF ?A) (PROCEDURE ?A))))
 :AXIOM-DEF (THE-ARCHETYPE STAGE REIFIED-PROPERTY))