
:comment documentazione dell'esempio

:index int


:comment ----- TYPES DESCLARATIONS -------

:smt (define-type Customer) 
:smt (define-type Package) 
:smt (define-type Item)
:smt (define-type CreditCard)
:smt (define-type Truck)
:smt (define-type Num)
:smt (define-type String)


:comment ---------- FUNCTIONS and PREDICATES -----------



:smt (define CustName ::(-> Customer String))
:smt (define CustPhone ::(-> Customer Num))
:smt (define CustAddr ::(-> Customer String))
:smt (define CustBill ::(-> Customer String))
:smt (define CustCard ::(-> Customer CreditCard))
:smt (define PackCost ::(-> Package Num))
:smt (define ItemName ::(-> Item String))
:smt (define ItemPrice ::(-> Item Num))
:smt (define ItemP1 ::(-> Item Package))
:smt (define ItemP2 ::(-> Item Package))
:smt (define CredName ::(-> CreditCard String))
:smt (define CredAddr ::(-> CreditCard String))
:smt (define TruckName ::(-> Truck String))
:smt (define TruckP1 ::(-> Truck Package))
:smt (define TruckP2 ::(-> Truck Package))
:smt (define TruckP3 ::(-> Truck Package))

:smt (define init ::String)
:smt (define shipped ::String)
:smt (define Canceled ::String)
:smt (define paid ::String)
:smt (define unpaid ::String)
:smt (define adding_truck ::String)
:smt (define truck_ready ::String)



:db_driven 
:db_sorts Customer Package Item CreditCard Truck Num String 
:db_functions CustName CustPhone CustAddr CustBill CustCard PackCost ItemName ItemPrice   
:db_functions  ItemP1 ItemP2 CredName CredAddr TruckName TruckP1 TruckP2 TruckP3
:db_constants init shipped Canceled paid unpaid adding_truck truck_ready 
:db_relations 


:local Items Item
:local Cand Truck


:global T1_cid Customer
:global T1_name String
:global T1_phone_num Num
:global T1_addr String
:global T1_billing_addr String
:global T1_iid Item
:global T1_status String
:global T2_item_id Item
:global T3_cid Customer
:global T3_name String
:global T3_phone_num Num
:global T3_addr String
:global T3_billing_addr String
:global T3_card_id CreditCard
:global T3_status String
:global T4_iid Item
:global T4_name String
:global T4_phone_num Num
:global T4_addr String
:global T4_status String
:global T4_pid Package
:global T5_iid Item
:global T5_name String
:global T5_phone_num Num
:global T5_addr String
:global T5_status String
:global T5_pid Package
:global T5_tid Truck
:global actT2 bool
:global actT3 bool
:global actT4 bool
:global actT5 bool





:initial
:var x
:cnj (=  T1_cid  NULL_Customer) (=  T1_name NULL_String) (=  T1_phone_num  NULL_Num) (=  T1_addr   NULL_String) (=  T1_billing_addr NULL_String) (=  T1_iid NULL_Item) (= T1_status NULL_String)(= T2_item_id NULL_Item)(=  T3_cid  NULL_Customer) (=  T3_name NULL_String) (=  T3_phone_num  NULL_Num) (=  T3_addr   NULL_String) (=  T3_billing_addr NULL_String) (=  T3_card_id NULL_CreditCard) (= T3_status NULL_String)(=  T4_iid  NULL_Item) (=  T4_name NULL_String) (=  T4_phone_num  NULL_Num) (=  T4_addr NULL_String)(=  T4_status NULL_String) (= T4_pid NULL_Package)(=  T5_iid  NULL_Item) (=  T5_name NULL_String) (=  T5_phone_num  NULL_Num) (=  T5_addr NULL_String)(=  T5_status NULL_String)(= T5_pid NULL_Package)(= T5_tid NULL_Truck) (= Items[x] NULL_Item)(= Cand[x] NULL_Truck)(= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)

:u_cnj  (= T1_name NULL_String)(not (= T1_iid NULL_Item))(= T1_addr NULL_String)(not (= T2_item_id NULL_Item))

:eevar e Customer
:eevar d Package
:eevar f Item
:eevar g CreditCard
:eevar h Truck
:eevar l Num
:eevar m Num
:eevar n String
:eevar o String
:eevar p String


:comment T_1: Amazon

:comment T_1 EnterCustomerInfo:

:comment T1
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_cid NULL_Customer)(not (= n NULL_String))(not (= l NULL_Num))(not (= o NULL_String))
:numcases 1
:case 
 :val Items[j]
 :val Cand[j]

 :val T1_cid 
 :val n
 :val l
 :val o
 :val p
 :val T1_iid 
 :val T1_status 
 :val T2_item_id 
 :val T3_cid 
 :val T3_name 
 :val T3_phone_num 
 :val T3_addr 
 :val T3_billing_addr 
 :val T3_card_id 
 :val T3_status 
 :val T4_iid 
 :val T4_name 
 :val T4_phone_num 
 :val T4_addr 
 :val T4_status 
 :val T4_pid 
 :val T5_iid 
 :val T5_name 
 :val T5_phone_num 
 :val T5_addr 
 :val T5_status 
 :val T5_pid 
 :val T5_tid 
 :val actT2 
 :val actT3
 :val actT4
 :val actT5

:comment T2
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_cid NULL_Customer)(not (= n NULL_String))(not (= l NULL_Num))(not (= o NULL_String))
:numcases 1
:case 
 :val Items[j]
 :val Cand[j]

 :val T1_cid 
 :val n
 :val l
 :val o
 :val NULL_String
 :val T1_iid 
 :val T1_status 
 :val T2_item_id 
 :val T3_cid 
 :val T3_name 
 :val T3_phone_num 
 :val T3_addr 
 :val T3_billing_addr 
 :val T3_card_id 
 :val T3_status 
 :val T4_iid 
 :val T4_name 
 :val T4_phone_num 
 :val T4_addr 
 :val T4_status 
 :val T4_pid 
 :val T5_iid 
 :val T5_name 
 :val T5_phone_num 
 :val T5_addr 
 :val T5_status 
 :val T5_pid 
 :val T5_tid 
 :val actT2 
 :val actT3
 :val actT4
 :val actT5 
 


 :comment T_1 CustomerLogin:

:comment T3
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_cid NULL_Customer)(not (= e NULL_Customer))(not (= n NULL_String))
:numcases 1
:case 
 :val Items[j]
 :val Cand[j]

 :val e
 :val (CustName e)
 :val (CustPhone e)
 :val (CustAddr e)
 :val n
 :val T1_iid 
 :val T1_status 
 :val T2_item_id 
 :val T3_cid 
 :val T3_name 
 :val T3_phone_num 
 :val T3_addr 
 :val T3_billing_addr 
 :val T3_card_id 
 :val T3_status 
 :val T4_iid 
 :val T4_name 
 :val T4_phone_num 
 :val T4_addr 
 :val T4_status 
 :val T4_pid 
 :val T5_iid 
 :val T5_name 
 :val T5_phone_num 
 :val T5_addr 
 :val T5_status 
 :val T5_pid 
 :val T5_tid 
 :val actT2 
 :val actT3
 :val actT4
 :val actT5

:comment T4
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_cid NULL_Customer)(not (= e NULL_Customer))
:numcases 1
:case 
 :val Items[j]
 :val Cand[j]

 :val e
 :val (CustName e)
 :val (CustPhone e)
 :val (CustAddr e)
 :val NULL_String
 :val T1_iid 
 :val T1_status 
 :val T2_item_id 
 :val T3_cid 
 :val T3_name 
 :val T3_phone_num 
 :val T3_addr 
 :val T3_billing_addr 
 :val T3_card_id 
 :val T3_status 
 :val T4_iid 
 :val T4_name 
 :val T4_phone_num 
 :val T4_addr 
 :val T4_status 
 :val T4_pid 
 :val T5_iid 
 :val T5_name 
 :val T5_phone_num 
 :val T5_addr 
 :val T5_status 
 :val T5_pid 
 :val T5_tid 
 :val actT2 
 :val actT3
 :val actT4
 :val actT5
 
 

 
 
 :comment T_1 InitStatus
 :comment T5
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)
:numcases 1
:case 
 :val Items[j]
 :val Cand[j]

 :val T1_cid 
 :val T1_name 
 :val T1_phone_num 
 :val T1_addr 
 :val T1_billing_addr 
 :val NULL_Item
 :val init 
 :val T2_item_id 
 :val T3_cid 
 :val T3_name 
 :val T3_phone_num 
 :val T3_addr 
 :val T3_billing_addr 
 :val T3_card_id 
 :val T3_status 
 :val T4_iid 
 :val T4_name 
 :val T4_phone_num 
 :val T4_addr 
 :val T4_status 
 :val T4_pid 
 :val T5_iid 
 :val T5_name 
 :val T5_phone_num 
 :val T5_addr 
 :val T5_status 
 :val T5_pid 
 :val T5_tid 
 :val actT2 
 :val actT3
 :val actT4
 :val actT5
 
 :comment T_2: Shopping
 
 :comment T_2 opening
 
  :comment T6
 :transition
 :var j
 :guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_status init)
 :numcases 1
 :case 
  :val Items[j]
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val NULL_Item
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val true
  :val actT3
  :val actT4
  :val actT5
 
 :comment T_2 PickItem:
 
  :comment T7
 :transition
 :var j
 :guard  (= actT2 true)(= actT3 false)(= actT4 false)(= actT5 false)(= T2_item_id NULL_Item)(not (=  f NULL_Item))
 :numcases 1
 :case 
  :val Items[j]
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val f 
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val actT2
  :val actT3
  :val actT4
  :val actT5
 
 :comment T_2 AddToCart
 
  :comment T8
 :transition
 :var x
 :var j
 :guard  (= actT2 true)(= actT3 false)(= actT4 false)(= actT5 false)(not (= T2_item_id NULL_Item))(= Items[x] NULL_Item)
 :uguard (not (= Items[j] T2_item_id))
 :numcases 2
 :case (= j x)
  :val T2_item_id
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val NULL_Item
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val actT2
  :val actT3
  :val actT4
  :val actT5
:case 
  :val Items[j]
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val NULL_Item
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val actT2
  :val actT3
  :val actT4
  :val actT5

 :comment T_2 RetrieveFromCart
 
  :comment T9
 :transition
 :var x
 :var j
 :guard  (= actT2 true)(= actT3 false)(= actT4 false)(= actT5 false)(= T2_item_id NULL_Item)(not (= Items[x] NULL_Item))
 :numcases 2
 :case (= j x)
  :val NULL_Item
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val Items[x]
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val actT2
  :val actT3
  :val actT4
  :val actT5
:case 
  :val Items[j]
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T1_iid
  :val T1_status
  :val Items[x]
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val actT2
  :val actT3
  :val actT4
  :val actT5
  
  
  
  :comment T_2 closing
 
 :comment T10
 :transition
 :var j
 :guard  (= actT2 true)(= actT3 false)(= actT4 false)(= actT5 false)(not (= T2_item_id NULL_Item))
 :numcases 1
 :case 
  :val NULL_Item
  :val Cand[j]

  :val T1_cid 
  :val T1_name 
  :val T1_phone_num 
  :val T1_addr 
  :val T1_billing_addr 
  :val T2_item_id
  :val T1_status
  :val T2_item_id
  :val T3_cid 
  :val T3_name 
  :val T3_phone_num 
  :val T3_addr 
  :val T3_billing_addr 
  :val T3_card_id 
  :val T3_status 
  :val T4_iid 
  :val T4_name 
  :val T4_phone_num 
  :val T4_addr 
  :val T4_status 
  :val T4_pid 
  :val T5_iid 
  :val T5_name 
  :val T5_phone_num 
  :val T5_addr 
  :val T5_status 
  :val T5_pid 
  :val T5_tid 
  :val false
  :val actT3
  :val actT4
  :val actT5
  
   :comment T_3: Payment
 
 :comment T_3 opening
 
  :comment T11
  :transition
  :var j
  :guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_status init)(not (= T1_cid NULL_Customer))
  :numcases 1
  :case 
   :val Items[j]
   :val Cand[j]

   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val T1_billing_addr 
   :val T1_iid
   :val T1_status
   :val T2_item_id
   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val NULL_String
   :val NULL_CreditCard
   :val NULL_String
   :val T4_iid 
   :val T4_name 
   :val T4_phone_num 
   :val T4_addr 
   :val T4_status 
   :val T4_pid 
   :val T5_iid 
   :val T5_name 
   :val T5_phone_num 
   :val T5_addr 
   :val T5_status 
   :val T5_pid 
   :val T5_tid 
   :val actT2
   :val true
   :val actT4
   :val actT5
  
  :comment T12
  :transition
  :var j
  :guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_status init)(not (= T1_name NULL_String))
  :numcases 1
  :case 
   :val Items[j]
   :val Cand[j]

   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val T1_billing_addr 
   :val T1_iid
   :val T1_status
   :val T2_item_id
   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val NULL_String
   :val NULL_CreditCard
   :val NULL_String
   :val T4_iid 
   :val T4_name 
   :val T4_phone_num 
   :val T4_addr 
   :val T4_status 
   :val T4_pid 
   :val T5_iid 
   :val T5_name 
   :val T5_phone_num 
   :val T5_addr 
   :val T5_status 
   :val T5_pid 
   :val T5_tid 
   :val actT2
   :val true
   :val actT4
   :val actT5
  
  
  :comment T_3 Initialize
  
  :comment T13
  :transition
  :var j
  :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(not (= T3_status paid))(not (= T3_status shipped))(not (= T3_status Canceled))
  :numcases 1
  :case 
   :val Items[j]
   :val Cand[j]

   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val T1_billing_addr 
   :val T1_iid
   :val T1_status
   :val T2_item_id
   :val T3_cid 
   :val T3_name 
   :val T3_phone_num 
   :val T3_addr 
   :val NULL_String
   :val NULL_CreditCard
   :val unpaid
   :val T4_iid 
   :val T4_name 
   :val T4_phone_num 
   :val T4_addr 
   :val T4_status 
   :val T4_pid 
   :val T5_iid 
   :val T5_name 
   :val T5_phone_num 
   :val T5_addr 
   :val T5_status 
   :val T5_pid 
   :val T5_tid 
   :val actT2
   :val actT3
   :val actT4
   :val actT5
   
   :comment T_3 VerifyCardInfo
  
   :comment T14
   :transition
   :var j
   :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_card_id NULL_CreditCard)(= T3_status unpaid)(not (=  g NULL_CreditCard))(= (CredName  g) T3_name)(= (CredAddr  g) n)
   :numcases 1
   :case 
    :val Items[j]
    :val Cand[j]

    :val T1_cid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val T1_billing_addr 
    :val T1_iid
    :val T1_status
    :val T2_item_id
    :val T3_cid 
    :val T3_name 
    :val T3_phone_num 
    :val T3_addr 
    :val n
    :val g
    :val paid
    :val T4_iid 
    :val T4_name 
    :val T4_phone_num 
    :val T4_addr 
    :val T4_status 
    :val T4_pid 
    :val T5_iid 
    :val T5_name 
    :val T5_phone_num 
    :val T5_addr 
    :val T5_status 
    :val T5_pid 
    :val T5_tid 
    :val actT2
    :val actT3
    :val actT4
    :val actT5
	
    :comment T15
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_card_id NULL_CreditCard)(= T3_status unpaid)(= T3_cid NULL_Customer)(not (= g NULL_CreditCard))
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val n
     :val g
     :val paid
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status 
     :val T4_pid 
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	 
:comment T16
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_card_id NULL_CreditCard)(= T3_status unpaid)(= T3_cid NULL_Customer)
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val NULL_String
     :val NULL_CreditCard
     :val paid
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status 
     :val T4_pid 
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	
	 
     :comment T17
     :transition
     :var j
     :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_card_id NULL_CreditCard)(= T3_status unpaid)(not (= T3_cid NULL_Customer))(= (CustCard T3_cid) g)(not (= g NULL_CreditCard))(= (CredName g) T3_name)(= (CredAddr g) (CustBill T3_cid))
     :numcases 1
     :case 
      :val Items[j]
      :val Cand[j]

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val (CustBill T3_cid)
      :val g
      :val paid
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status 
      :val T4_pid 
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val T5_status 
      :val T5_pid 
      :val T5_tid 
      :val actT2
      :val actT3
      :val actT4
      :val actT5
   
   :comment T_3 CancelPayment
  
   :comment T18
   :transition
   :var j
   :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_status unpaid)
   :numcases 1
   :case 
    :val Items[j]
    :val Cand[j]

    :val T1_cid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val T1_billing_addr 
    :val T1_iid
    :val T1_status
    :val T2_item_id
    :val T3_cid 
    :val T3_name 
    :val T3_phone_num 
    :val T3_addr 
    :val T3_billing_addr
    :val T3_card_id
    :val Canceled
    :val T4_iid 
    :val T4_name 
    :val T4_phone_num 
    :val T4_addr 
    :val T4_status 
    :val T4_pid 
    :val T5_iid 
    :val T5_name 
    :val T5_phone_num 
    :val T5_addr 
    :val T5_status 
    :val T5_pid 
    :val T5_tid 
    :val actT2
    :val actT3
    :val actT4
    :val actT5
  
  :comment T_3 closing
 
  :comment T19
  :transition
  :var j
  :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_status shipped)
  :numcases 1
  :case 
   :val Items[j]
   :val Cand[j]

   :val T1_cid 
   :val T1_name 
   :val T1_phone_num 
   :val T1_addr 
   :val T1_billing_addr 
   :val T1_iid
   :val T3_status
   :val T2_item_id
   :val T3_cid 
   :val T3_name 
   :val T3_phone_num 
   :val T3_addr 
   :val T3_billing_addr
   :val T3_card_id
   :val T3_status
   :val T4_iid 
   :val T4_name 
   :val T4_phone_num 
   :val T4_addr 
   :val T4_status 
   :val T4_pid 
   :val T5_iid 
   :val T5_name 
   :val T5_phone_num 
   :val T5_addr 
   :val T5_status 
   :val T5_pid 
   :val T5_tid 
   :val actT2
   :val false
   :val actT4
   :val actT5
   
   :comment T20
   :transition
   :var j
   :guard  (= actT2 false)(= actT3 true)(= actT4 false)(= actT5 false)(= T3_status Canceled)
   :numcases 1
   :case 
    :val Items[j]
    :val Cand[j]

    :val T1_cid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val T1_billing_addr 
    :val T1_iid
    :val T3_status
    :val T2_item_id
    :val T3_cid 
    :val T3_name 
    :val T3_phone_num 
    :val T3_addr 
    :val T3_billing_addr
    :val T3_card_id
    :val T3_status
    :val T4_iid 
    :val T4_name 
    :val T4_phone_num 
    :val T4_addr 
    :val T4_status 
    :val T4_pid 
    :val T5_iid 
    :val T5_name 
    :val T5_phone_num 
    :val T5_addr 
    :val T5_status 
    :val T5_pid 
    :val T5_tid 
    :val actT2
    :val false
    :val actT4
    :val actT5
   
   
   :comment T_4: Packing
   
   :comment T_4 opening
 
   :comment T21
   
   :transition
   :var j
   :guard  (= actT2 false)(= actT3 false)(= actT4 false)(= actT5 false)(= T1_status paid)
   :numcases 1
   :case 
    :val Items[j]
    :val Cand[j]

    :val T1_cid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val T1_billing_addr 
    :val T1_iid
    :val T1_status
    :val T2_item_id
    :val T3_cid 
    :val T3_name 
    :val T3_phone_num 
    :val T3_addr 
    :val T3_billing_addr
    :val T3_card_id
    :val T3_status
    :val T1_iid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val NULL_String
    :val NULL_Package
    :val T5_iid 
    :val T5_name 
    :val T5_phone_num 
    :val T5_addr 
    :val T5_status 
    :val T5_pid 
    :val T5_tid 
    :val actT2
    :val actT3
    :val true
    :val actT5
	
    :comment T_4 Start:
 
    :comment T22
   
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 false)
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val NULL_Package
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	
	
    :comment T_4 Pack:
 
    :comment T23
   
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 false)(= T4_pid NULL_Package)(not (= d NULL_Package))(not (=  T4_iid NULL_Item))(= (ItemP1 T4_iid) d)
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val d
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	

 
    :comment T24
   
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 false)(= T4_pid NULL_Package)(not (= d NULL_Package))(not (=  T4_iid NULL_Item))(= (ItemP2 T4_iid) d)
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val d
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	 
	 :comment T_4 closing
	
    :comment T25
   
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 false)(= T4_status shipped)
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T4_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val T5_status 
     :val T5_pid 
     :val T5_tid 
     :val actT2
     :val actT3
     :val false
     :val actT5
	 
	 
	 :comment T_5: Shipment
	
	 :comment T_5 opening
	
    :comment T26
   
    :transition
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 false)(not (= T4_pid NULL_Package))
    :numcases 1
    :case 
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val NULL_String
     :val T4_pid 
     :val NULL_Truck
     :val actT2
     :val actT3
     :val actT4
     :val true
	 
 	 :comment T_5 NewTruck
	
     :comment T27
   
     :transition
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_tid NULL_Truck)(not (= h NULL_Truck))
     :numcases 1
     :case 
      :val Items[j]
      :val Cand[j]

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val adding_truck
      :val T5_pid 
      :val h
      :val actT2
      :val actT3
      :val actT4
      :val actT5
	  
  	 :comment T_5 AddCandidateTruck
	
      :comment T28
   
      :transition
	  :var x
      :var j
      :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (= T5_tid NULL_Truck))(not (=  T5_tid NULL_Truck))(= (TruckP1 T5_tid) T5_pid)(= Cand[x] NULL_Truck)(not (= d NULL_Package))
      :uguard (not (= Cand[j] T5_tid))
      :numcases 2
      :case (= j x)
       :val Items[j]
       :val T5_tid

       :val T1_cid 
       :val T1_name 
       :val T1_phone_num 
       :val T1_addr 
       :val T1_billing_addr 
       :val T1_iid
       :val T1_status
       :val T2_item_id
       :val T3_cid 
       :val T3_name 
       :val T3_phone_num 
       :val T3_addr 
       :val T3_billing_addr
       :val T3_card_id
       :val T3_status
       :val T4_iid 
       :val T4_name 
       :val T4_phone_num 
       :val T4_addr 
       :val T4_status
       :val T4_pid
       :val T5_iid 
       :val T5_name 
       :val T5_phone_num 
       :val T5_addr 
       :val adding_truck
       :val d
       :val NULL_Truck
       :val actT2
       :val actT3
       :val actT4
       :val actT5
	  :case
      :val Items[j]
      :val Cand[j]

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val adding_truck
      :val d
      :val NULL_Truck
      :val actT2
      :val actT3
      :val actT4
      :val actT5
	 
	    :comment T29
   
      :transition
	  :var x
      :var j
      :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (= T5_tid NULL_Truck))(not (=  T5_tid NULL_Truck))(= (TruckP1 T5_tid) T5_pid)(= Cand[x] NULL_Truck)
      :uguard (not (= Cand[j] T5_tid))
      :numcases 2
      :case (= j x)
       :val Items[j]
       :val T5_tid

       :val T1_cid 
       :val T1_name 
       :val T1_phone_num 
       :val T1_addr 
       :val T1_billing_addr 
       :val T1_iid
       :val T1_status
       :val T2_item_id
       :val T3_cid 
       :val T3_name 
       :val T3_phone_num 
       :val T3_addr 
       :val T3_billing_addr
       :val T3_card_id
       :val T3_status
       :val T4_iid 
       :val T4_name 
       :val T4_phone_num 
       :val T4_addr 
       :val T4_status
       :val T4_pid
       :val T5_iid 
       :val T5_name 
       :val T5_phone_num 
       :val T5_addr 
       :val adding_truck
       :val NULL_Package
       :val NULL_Truck
       :val actT2
       :val actT3
       :val actT4
       :val actT5
	  :case
      :val Items[j]
      :val Cand[j]

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val adding_truck
      :val NULL_Package
      :val NULL_Truck
      :val actT2
      :val actT3
      :val actT4
      :val actT5
	     
	  
     :comment T30
  
     :transition
  :var x
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (=  T5_tid NULL_Truck))(= (TruckP2 T5_tid) T5_pid)(= Cand[x] NULL_Truck)
  :uguard (not (= Cand[j] T5_tid))
     :numcases 2
     :case (= j x)
      :val Items[j]
      :val T5_tid

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val adding_truck
      :val d
      :val NULL_Truck
      :val actT2
      :val actT3
      :val actT4
      :val actT5
  :case
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val adding_truck
     :val d
     :val NULL_Truck
     :val actT2
     :val actT3
     :val actT4
     :val actT5

     :comment T31
  
     :transition
  :var x
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (=  T5_tid NULL_Truck))(= (TruckP2 T5_tid) T5_pid)(= Cand[x] NULL_Truck)
  :uguard (not (= Cand[j] T5_tid))
     :numcases 2
     :case (= j x)
      :val Items[j]
      :val T5_tid

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val adding_truck
      :val NULL_Package
      :val NULL_Truck
      :val actT2
      :val actT3
      :val actT4
      :val actT5
  :case
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val adding_truck
     :val NULL_Package
     :val NULL_Truck
     :val actT2
     :val actT3
     :val actT4
     :val actT5
	 
	
	:comment T32
       :transition
       :var x
       :var j
       :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (= T5_tid NULL_Truck))(not (= (TruckName T5_tid) NULL_String))(= (TruckP3 T5_tid) T5_pid)(= Cand[x] NULL_Truck)
    :uguard (not (= Cand[j] T5_tid))
       :numcases 2
       :case (= j x)
        :val Items[j]
        :val T5_tid

        :val T1_cid 
        :val T1_name 
        :val T1_phone_num 
        :val T1_addr 
        :val T1_billing_addr 
        :val T1_iid
        :val T1_status
        :val T2_item_id
        :val T3_cid 
        :val T3_name 
        :val T3_phone_num 
        :val T3_addr 
        :val T3_billing_addr
        :val T3_card_id
        :val T3_status
        :val T4_iid 
        :val T4_name 
        :val T4_phone_num 
        :val T4_addr 
        :val T4_status
        :val T4_pid
        :val T5_iid 
        :val T5_name 
        :val T5_phone_num 
        :val T5_addr 
        :val adding_truck
        :val d
        :val NULL_Truck
        :val actT2
        :val actT3
        :val actT4
        :val actT5
    :case
       :val Items[j]
       :val Cand[j]

       :val T1_cid 
       :val T1_name 
       :val T1_phone_num 
       :val T1_addr 
       :val T1_billing_addr 
       :val T1_iid
       :val T1_status
       :val T2_item_id
       :val T3_cid 
       :val T3_name 
       :val T3_phone_num 
       :val T3_addr 
       :val T3_billing_addr
       :val T3_card_id
       :val T3_status
       :val T4_iid 
       :val T4_name 
       :val T4_phone_num 
       :val T4_addr 
       :val T4_status
       :val T4_pid
       :val T5_iid 
       :val T5_name 
       :val T5_phone_num 
       :val T5_addr 
       :val adding_truck
       :val d
       :val NULL_Truck
       :val actT2
       :val actT3
       :val actT4
       :val actT5

	:comment T33
       :transition
       :var x
       :var j
       :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(not (= T5_tid NULL_Truck))(not (= (TruckName T5_tid) NULL_String))(= (TruckP3 T5_tid) T5_pid)(= Cand[x] NULL_Truck)
    :uguard (not (= Cand[j] T5_tid))
       :numcases 2
       :case (= j x)
        :val Items[j]
        :val T5_tid

        :val T1_cid 
        :val T1_name 
        :val T1_phone_num 
        :val T1_addr 
        :val T1_billing_addr 
        :val T1_iid
        :val T1_status
        :val T2_item_id
        :val T3_cid 
        :val T3_name 
        :val T3_phone_num 
        :val T3_addr 
        :val T3_billing_addr
        :val T3_card_id
        :val T3_status
        :val T4_iid 
        :val T4_name 
        :val T4_phone_num 
        :val T4_addr 
        :val T4_status
        :val T4_pid
        :val T5_iid 
        :val T5_name 
        :val T5_phone_num 
        :val T5_addr 
        :val adding_truck
        :val NULL_Package
        :val NULL_Truck
        :val actT2
        :val actT3
        :val actT4
        :val actT5
    :case
       :val Items[j]
       :val Cand[j]

       :val T1_cid 
       :val T1_name 
       :val T1_phone_num 
       :val T1_addr 
       :val T1_billing_addr 
       :val T1_iid
       :val T1_status
       :val T2_item_id
       :val T3_cid 
       :val T3_name 
       :val T3_phone_num 
       :val T3_addr 
       :val T3_billing_addr
       :val T3_card_id
       :val T3_status
       :val T4_iid 
       :val T4_name 
       :val T4_phone_num 
       :val T4_addr 
       :val T4_status
       :val T4_pid
       :val T5_iid 
       :val T5_name 
       :val T5_phone_num 
       :val T5_addr 
       :val adding_truck
       :val NULL_Package
       :val NULL_Truck
       :val actT2
       :val actT3
       :val actT4
       :val actT5
	   
	  
	 
:comment T_5 RetrieveTruck

:comment T34
    :transition
    :var x
    :var j
    :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_tid NULL_Truck)(not (= Cand[x] NULL_Truck))(= (TruckP1 Cand[x]) d) 
    :numcases 2
    :case (= j x)
     :val Items[j]
     :val NULL_Truck

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val truck_ready
     :val d
     :val Cand[x]
     :val actT2
     :val actT3
     :val actT4
     :val actT5
 :case
    :val Items[j]
    :val Cand[j]

    :val T1_cid 
    :val T1_name 
    :val T1_phone_num 
    :val T1_addr 
    :val T1_billing_addr 
    :val T1_iid
    :val T1_status
    :val T2_item_id
    :val T3_cid 
    :val T3_name 
    :val T3_phone_num 
    :val T3_addr 
    :val T3_billing_addr
    :val T3_card_id
    :val T3_status
    :val T4_iid 
    :val T4_name 
    :val T4_phone_num 
    :val T4_addr 
    :val T4_status
    :val T4_pid
    :val T5_iid 
    :val T5_name 
    :val T5_phone_num 
    :val T5_addr 
    :val truck_ready
    :val d
    :val Cand[x]
    :val actT2
    :val actT3
    :val actT4
    :val actT5
	
 
 :comment T35
     :transition
     :var x
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_tid NULL_Truck)(not (= Cand[x] NULL_Truck))(= (TruckP2 Cand[x]) d) 
     :numcases 2
     :case (= j x)
      :val Items[j]
      :val NULL_Truck

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val truck_ready
      :val d
      :val Cand[x]
      :val actT2
      :val actT3
      :val actT4
      :val actT5
  :case
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val truck_ready
     :val d
     :val Cand[x]
     :val actT2
     :val actT3
     :val actT4
     :val actT5
 
 
 :comment T36
     :transition
     :var x
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_tid NULL_Truck)(not (= Cand[x] NULL_Truck))(= (TruckP3 Cand[x]) d)
     :numcases 2
     :case (= j x)
      :val Items[j]
      :val NULL_Truck

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val truck_ready
      :val d
      :val Cand[x]
      :val actT2
      :val actT3
      :val actT4
      :val actT5
  :case
     :val Items[j]
     :val Cand[j]

     :val T1_cid 
     :val T1_name 
     :val T1_phone_num 
     :val T1_addr 
     :val T1_billing_addr 
     :val T1_iid
     :val T1_status
     :val T2_item_id
     :val T3_cid 
     :val T3_name 
     :val T3_phone_num 
     :val T3_addr 
     :val T3_billing_addr
     :val T3_card_id
     :val T3_status
     :val T4_iid 
     :val T4_name 
     :val T4_phone_num 
     :val T4_addr 
     :val T4_status
     :val T4_pid
     :val T5_iid 
     :val T5_name 
     :val T5_phone_num 
     :val T5_addr 
     :val truck_ready
     :val d
     :val Cand[x]
     :val actT2
     :val actT3
     :val actT4
     :val actT5
 
 
 :comment T_5 Ship:

 :comment T37
     :transition
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_status truck_ready)
     :numcases 1
     :case 
      :val Items[j]
      :val Cand[j]

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T4_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val shipped
      :val T5_pid
      :val T5_tid
      :val actT2
      :val actT3
      :val actT4
      :val actT5
 



 

  :comment T_5 closing 

 :comment T38
     :transition
     :var j
     :guard  (= actT2 false)(= actT3 false)(= actT4 true)(= actT5 true)(= T5_status shipped)
     :numcases 1
     :case 
      :val Items[j]
      :val NULL_Truck

      :val T1_cid 
      :val T1_name 
      :val T1_phone_num 
      :val T1_addr 
      :val T1_billing_addr 
      :val T1_iid
      :val T1_status
      :val T2_item_id
      :val T3_cid 
      :val T3_name 
      :val T3_phone_num 
      :val T3_addr 
      :val T3_billing_addr
      :val T3_card_id
      :val T3_status
      :val T4_iid 
      :val T4_name 
      :val T4_phone_num 
      :val T4_addr 
      :val T5_status
      :val T4_pid
      :val T5_iid 
      :val T5_name 
      :val T5_phone_num 
      :val T5_addr 
      :val T5_status
      :val T5_pid
      :val T5_tid
      :val actT2
      :val actT3
      :val actT4
      :val false
 
