domain.pddl

 
;; This domain encodes the domain of a concurrent 
;; systems, especially communication protocols 
;; (c) Stefan Edelkamp, 2004 
 
(define (domain protocol)
 
(:requirements  :equality 
 ;; equality needed for blocked transition in case of a mismatch 
 
 :typing) 
(:types process proctype state queue transition 
        number message
 ;; tags for size and messages 
 
        queuetype queue-state
        - object
)
(:predicates 
   (is-a-queue ?q - queue ?pt - queuetype) 
   ;; true if type of communication channel matches queuetype 
 
   (is-a-process ?q - process ?pt - proctype) 
   ;; true if process class matches process type 
 
   (at-process ?p - process ?s - state) 
   ;; true for current local state 
 
   (trans ?pt - proctype ?t - transition ?s1 ?s2 - state) 
   ;; local state transition 
 
   ;; false for all outgoing transition at a given local state 
 
   (writes ?p - process ?q - queue ?t - transition) 
   ;; true if transition writes data in channel 
 
   (reads ?p - process ?q - queue ?t - transition) 
   ;; true if transition reads data in channel 
 
   (enabled ?p - process ?t - transition) 
   ;; true if process can perform state transition 
 
   (pending ?p - process) 
   ;; true if process is waiting for instructions 
 
   (activate ?p - process ?t - transition) 
   ;; if process is waiting for instructions 
 
   (queue-next ?qt - queuetype ?qs1 ?qs2 - queue-state) 
   ;; true for two neighboring cells in a queue 
 
   (queue-head ?q - queue ?qs - queue-state) 
   ;; true if head is at given queue position 
 
   (queue-tail ?q - queue ?qs - queue-state) 
   ;; true if tail is at given queue position 
 
   (advance-tail ?q - queue) 
   ;; true queue tail has yet to advance one cell 
 
   (advance-head ?q - queue) 
   ;; true queue head has yet to advance one cell 
 
   (settled ?q - queue) 
   ;; true if queue has completed restructuring 
 
   (blocked ?p - process) 
   ;; true if no local state transition is applicable 
 
   (blocked-trans ?p - process ?t - transition) 
   ;; true if process is blocked 
 
   (queue-msg ?q - queue ?p - queue-state ?m - message) 
   ;; true if queue cell is labelled with given message 
 
   (queue-head-msg ?q - queue ?m - message) 
   ;; true if queue at head cell is labelled with given message 
 
   (queue-tail-msg ?q - queue ?m - message) 
   ;; true if queue at tail cell is labelled with given message 
 
   (trans-msg ?t - transition ?m - message) 
   ;; true if message written or read by the transition 
 
   (inc ?n1 ?n2 - number) 
   ;; links successive integers 
 
   (dec ?n1 ?n2 - number) 
   ;; links successive integers 
 
   (queue-size ?q - queue ?n1 - number) 
   ;; current elements in communication channel 
 
   (queue-max ?qt - queuetype ?n1 - number) 
   ;; maximum elements in communication channel 
 
   (is-zero ?n1 - number) 
   ;; true if number is equal to zero 
 
   (is-not-zero ?n1 - number) 
   ;; true if number is not equal to zero 
 
   (is-max ?qt - queuetype ?n1 - number) 
   ;; true if number is equal to maximum queue size 
 
   (is-not-max ?qt - queuetype ?n1 - number) 
   ;; true if number is not equal to maximum queue size 
 
) 
 
 
 
   ;; transition that reads data from channel 
 
(:action queue-read  
   :parameters (?p - process 
                ?t - transition 
                ?q - queue  
                ?m - message  
   ) 
   :precondition 
      (and  
        ;; matching transition activated 
 
        (activate ?p ?t) 
        (settled ?q)  
        (reads ?p ?q ?t) 
        ;; if messages match 
 
        (queue-head-msg ?q ?m) 
        (trans-msg ?t ?m) 
      ) 
    :effect  
      (and  
         (not (activate ?p ?t))   
 
        ;; set flag for queue update  
 
	(advance-head ?q) 
	(not (settled ?q)) 
        ;; set flag for state transition  
 
	(enabled ?p ?t) 
      ) 
) 
 
 
;; determines if no local state transition can fire 
 
(:derived (blocked ?p - process) 
   (and 
     (exists (?s - state) 
      (exists (?pt - proctype) 
        (and 
        ;; select local state 
 
        (at-process ?p ?s) 
        (is-a-process ?p ?pt) 
         ;; select active transition  
 
        (forall (?t - transition) 
          (or (forall (?s2 - state) 
                  (not (trans ?pt ?t ?s ?s2)))
             (blocked-trans ?p ?t)))

        )))) 
) 
 
;; determines if a state transition cannot read, queue empty 
 
(:derived (blocked-trans ?p - process ?t - transition) 
   (and 
     (exists (?q - queue) 
      (exists (?m - message) 
       (exists (?n - number) 
	(and (activate ?p ?t) 
	  (reads ?p ?q ?t) 
	  (settled ?q) 
        (trans-msg ?t ?m) 
        (queue-size ?q ?n) 
        (is-zero ?n) 
	  ))) 
	 )) 
   ) 
 
;; determines if a state transition cannot write, queue full 
 
(:derived (blocked-trans ?p - process ?t - transition) 
   (and 
     (exists (?q - queue) 
      (exists (?qt - queuetype) 
       (exists (?m - message) 
        (exists (?n - number) 
	 (and 
	  (activate ?p ?t) 
	  (writes ?p ?q ?t) 
	  (settled ?q) 
	  (trans-msg ?t ?m) 
	  (is-a-queue ?q ?qt) 
        (queue-size ?q ?n) 
        (is-max ?qt ?n) 
          )))) 
          )) 
   ) 
 
;; determines if a state transition cannot read, wrong message 
 
(:derived (blocked-trans ?p - process ?t - transition) 
     (and 
        (exists (?q - queue) 
        (exists (?m - message) 
        (exists (?n - message) 
          (and (activate ?p ?t) 
               (reads ?p ?q ?t) 
               (settled ?q) 
               (trans-msg ?t ?m) 
               (queue-head-msg ?q ?n) 
               (not (= ?m ?n)) 
           )))           )))
 
;; state transition that writes message in communication channel 
 
(:action queue-write 
   :parameters (?p - process  
                ?t - transition 
                ?q - queue 
	          ?m - message 
   ) 
   :precondition  
      (and  
        (activate ?p ?t) 
        (settled ?q) 
        (writes ?p ?q ?t) 
        (trans-msg ?t ?m) 
      ) 
   :effect 
      (and  
         (not (activate ?p ?t))  

	  (enabled ?p ?t) 
	  (not (settled ?q)) 
 
	  (advance-tail ?q) 
        (queue-tail-msg ?q ?m) 
      ) 
) 
 
 
;; update communication channel due to read operation 
 
(:action advance-queue-head  
   :parameters (?q - queue ?qt - queuetype  
	          ?qs1 ?qs2 - queue-state 
	          ?m - message ?n1 ?n2 - number 
) 
   :precondition 
     (and  
	(queue-next ?qt ?qs1 ?qs2) 
	(is-a-queue ?q ?qt) 
	(queue-head ?q ?qs1) 
	(advance-head ?q) 
        (queue-msg ?q ?qs2 ?m) 
      (queue-size ?q ?n1) 
       (dec ?n1 ?n2) 
      ) 
   :effect 
     (and 	 
        (settled ?q) 
        (queue-head ?q ?qs2) 
        (not (advance-head ?q)) 
        (not (queue-head ?q ?qs1)) 
        (queue-head-msg ?q ?m) 
         (not (queue-size ?q ?n1)) 
         (queue-size ?q ?n2) 
      )       
) 
 
;; update communication channel due to write operation, empty queue 
 
(:action advance-empty-queue-tail    
   :parameters (?q - queue ?qt - queuetype  
	        ?qs1 ?qs2 - queue-state 
	        ?m ?m1 - message ?n1 ?n2 - number 
) 
   :precondition 
     (and  
	(queue-next ?qt ?qs1 ?qs2) 
	(is-a-queue ?q ?qt) 
	(queue-tail ?q ?qs1) 
	(advance-tail ?q)
      (queue-tail-msg ?q ?m) 
      (queue-head-msg ?q ?m1)  
      (queue-size ?q ?n1) 
      (inc ?n1 ?n2) 
      (is-zero ?n1) 
     ) 
   :effect 
     (and 	 
	(settled ?q) 
	(not (advance-tail ?q)) 
      (queue-tail ?q ?qs2) 
      (not (queue-tail ?q ?qs1)) 
      (queue-msg ?q ?qs2 ?m) 
      (queue-head-msg ?q ?m) 
      (not (queue-head-msg ?q ?m1)) 
      (queue-size ?q ?n2) 
      (not (queue-size ?q ?n1)) 
     )       
) 
 
;; update communication channel due to write operation 
 
(:action advance-non-empty-queue-tail    
   :parameters ( 
        ?q - queue ?qt - queuetype 
	  ?qs1 ?qs2 - queue-state 
        ?m - message 
        ?n1 ?n2 - number  
) 
   :precondition 
     (and  
	 (queue-next ?qt ?qs1 ?qs2) 
	 (is-a-queue ?q ?qt) 
	 (queue-tail ?q ?qs1) 
	 (advance-tail ?q) 
       (queue-tail-msg ?q ?m) 
       (queue-size ?q ?n1) 
       (inc ?n1 ?n2) 
       (is-not-zero ?n1) 
     ) 
   :effect 
     (and 	 
	  (settled ?q) 
	  (not (advance-tail ?q)) 
        (queue-tail ?q ?qs2) 
        (not (queue-tail ?q ?qs1)) 
        (queue-msg ?q ?qs2 ?m) 
        (not (queue-size ?q ?n1)) 
        (queue-size ?q ?n2) 
     )       
) 
 
;; execute local state transition 
 
(:action perform-trans 
   :parameters (?p - process 
	 	  ?pt - proctype 
                ?t - transition ?s1 ?s2 - state 
   ) 
   :precondition  
      (and  
	(forall (?q - queue) (settled ?q)) 
        (trans ?pt ?t ?s1 ?s2)  
        (enabled ?p ?t)  
        (at-process ?p ?s1)  
      ) 
   :effect  
      (and  
        (at-process ?p ?s2) 
        (not (at-process ?p ?s1))  
        (not (enabled ?p ?t)) 
	(pending ?p) 
      ) 
) 
 
;; activate local state transition 
 
 
(:action activate-trans 
   :parameters (?p - process 
                ?pt - proctype 
                ?t - transition ?s1 ?s2 - state 
   ) 
   :precondition  
      (and  
	(forall (?q - queue) (settled ?q)) 
        (trans ?pt ?t ?s1 ?s2)  
        (is-a-process ?p ?pt) 
        (at-process ?p ?s1) 
        (pending ?p)  
      ) 
   :effect  
      (and  
        (activate ?p ?t) 
        (not (pending ?p)) 
      ) 
) 

)