
:index int

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

:smt (define-type Customer) 
:smt (define-type Item) 
:smt (define-type String)
:smt (define-type Num)

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



:smt (define CustName ::(-> Customer String))
:smt (define ItemName ::(-> Item String))
:smt (define ItemPrice ::(-> Item Num))


:smt (define QuoteCreated ::String)
:smt (define New ::String)
:smt (define AdjustmentsRequired ::String)
:smt (define Modified ::String)
:smt (define QuoteApproved ::String)
:smt (define Approved ::String)
:smt (define Refusal ::String)
:smt (define Refused ::String)
:smt (define Notified ::String)
:smt (define ProceedAdjust ::String)
:smt (define Proceedd ::String)
:smt (define NotProceed ::String)
:smt (define QuoteCanceled ::String)



:db_driven 
:db_sorts Customer Item String Num
:db_functions CustName ItemName ItemPrice  
:db_constants  QuoteCreated New AdjustmentsRequired Modified QuoteApproved Approved
:db_constants Refusal Refused Notified ProceedAdjust Proceedd NotProceed QuoteCanceled 
:db_relations 

:local CandQuote1 Customer
:local CandQuote2 Item
:local CandQuote3 Num
:local CandQuote4 String
:local Notification1 Customer
:local Notification2 Item
:local Notification3 Num
:local Notification4 String
:local Notification5 String

:global T1_status String
:global T1_cid Customer
:global T1_iid Item
:global T1_unit Num
:global T1_quote_states String
:global T2_status String
:global T2_quote_states String
:global T2_cid Customer
:global T2_iid Item
:global T2_unit Num
:global T2_days_passed int
:global actT2 bool
:global flag int



:initial
:var x
:cnj (=  T1_status  NULL_String) (=  T1_cid  NULL_Customer) (=  T1_iid  NULL_Item) (=  T1_unit  NULL_Num) (=  T1_quote_states NULL_String) (=  T2_status NULL_String) (= T2_quote_states NULL_String) (= T2_cid NULL_Customer) (= T2_iid NULL_Item) (= T2_unit NULL_Num) (= T2_days_passed 0) (= CandQuote1[x] NULL_Customer) (= CandQuote2[x] NULL_Item)(= CandQuote3[x] NULL_Num) (= CandQuote4[x] NULL_String)(= Notification1[x] NULL_Customer) (= Notification2[x] NULL_Item)(= Notification3[x] NULL_Num)(= Notification4[x] NULL_String)(= Notification5[x] NULL_String)(= actT2 false)(= flag 0)


:u_cnj (= T1_cid NULL_Customer)(= T1_status Notified)(not (= T1_iid NULL_Item))

:eevar e Customer
:eevar d Item
:eevar f Num
:eevar g String
:eevar m String
:eevar n String
:eevar o int




:comment T_1: OrderMgmt

:comment T_1 CreateQuotation

:comment T1
:transition
:var j
:guard  (= actT2 false)(= flag 0)(= T1_cid NULL_Customer)(not (= e NULL_Customer))(not (= d NULL_Item)) (not (= f NULL_Num))
:numcases 1
:case 
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val QuoteCreated 
 :val e
 :val d
 :val f
 :val New
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
 
 :comment T_1 InsertCandidateQuote
 
 :comment T2
:transition
:var x
:var j
:guard  (= actT2 false)(= flag 0)(not (= T1_cid NULL_Customer))(not (= d NULL_Item)) (not (= f NULL_Num))(= CandQuote1[x] NULL_Customer)(= CandQuote2[x] NULL_Item)(= CandQuote3[x] NULL_Num)(= CandQuote4[x] NULL_String)
:uguard (not (= CandQuote1[j] T1_cid))(not (= CandQuote2[j] T1_iid))(not (= CandQuote3[j] T1_unit))(not (= CandQuote4[j] T1_quote_states))
:numcases 2
:case (= x j)
 :val T1_cid 
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val QuoteCreated 
 :val NULL_Customer
 :val d
 :val f
 :val New
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val QuoteCreated 
 :val NULL_Customer
 :val d
 :val f
 :val New
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 

 :comment T3
:transition
:var x
:var j
:guard  (= actT2 false)(= flag 0)(not (= T1_cid NULL_Customer))(= CandQuote1[x] NULL_Customer)(= CandQuote2[x] NULL_Item)(= CandQuote3[x] NULL_Num)(= CandQuote4[x] NULL_String)
:uguard (not (= CandQuote1[j] T1_cid))(not (= CandQuote2[j] T1_iid))(not (= CandQuote3[j] T1_unit))(not (= CandQuote4[j] T1_quote_states))
:numcases 2
:case (= x j)
 :val T1_cid 
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val QuoteCreated 
 :val NULL_Customer
 :val NULL_Item
 :val NULL_Num
 :val New
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val QuoteCreated 
 :val NULL_Customer
 :val NULL_Item
 :val NULL_Num
 :val New
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
 
 :comment T_1 ModifyQuote
 
 :comment T4
 :transition
 :var x
 :var j
 :guard  (= actT2 false)(= flag 0)(= T1_cid NULL_Customer)(= T1_status AdjustmentsRequired)(not (= CandQuote1[x] NULL_Customer)) (not (= CandQuote2[x] NULL_Item))(not (= CandQuote3[x] NULL_Num))(not (= CandQuote4[x] NULL_String))(= CandQuote4[x] New)
 :numcases 2
 :case (= j x)
  :val NULL_Customer
  :val NULL_Item 
  :val NULL_Num
  :val NULL_String
  :val Notification1[j] 
  :val Notification2[j] 
  :val Notification3[j] 
  :val Notification4[j] 
  :val Notification5[j] 

  :val m 
  :val CandQuote1[x] 
  :val CandQuote2[x]
  :val CandQuote3[x]
  :val CandQuote4[x]
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
 :case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

  :val m
  :val CandQuote1[x] 
  :val CandQuote2[x]
  :val CandQuote3[x]
  :val CandQuote4[x]
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
  
 :comment T5
 :transition
 :var x
 :var j
 :guard  (= actT2 false)(= flag 0)(= T1_cid NULL_Customer)(= T1_status AdjustmentsRequired)(not (= CandQuote1[x] NULL_Customer)) (not (= CandQuote2[x] NULL_Item))(not (= CandQuote3[x] NULL_Num))(not (= CandQuote4[x] NULL_String))(= CandQuote4[x] New)
 :numcases 2
 :case (= j x)
  :val NULL_Customer
  :val NULL_Item 
  :val NULL_Num
  :val NULL_String
  :val Notification1[j] 
  :val Notification2[j] 
  :val Notification3[j] 
  :val Notification4[j] 
  :val Notification5[j] 

  :val NULL_String
  :val CandQuote1[x] 
  :val CandQuote2[x]
  :val CandQuote3[x]
  :val CandQuote4[x]
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
 :case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

  :val NULL_String
  :val CandQuote1[x] 
  :val CandQuote2[x]
  :val CandQuote3[x]
  :val CandQuote4[x]
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
  
 :comment T_1 ModifyQuote2
 
 :comment T6
 :transition
:var x
:var j
:guard  (= actT2 false)(= flag 0)(not (= T1_cid NULL_Customer))(= T1_status AdjustmentsRequired)(not (= d NULL_Item))(not (= f NULL_Num))(= CandQuote1[x] NULL_Customer)(= CandQuote2[x] NULL_Item)(= CandQuote3[x] NULL_Num)(= CandQuote4[x] NULL_String)
:uguard (not (= CandQuote1[j] T1_cid))(not (= CandQuote2[j] T1_iid))(not (= CandQuote3[j] T1_unit))(not (= CandQuote4[j] T1_quote_states))
:numcases 2
:case (= j x)
 :val T1_cid 
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j]

 :val m
 :val e
 :val d
 :val f
 :val Modified
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val m
 :val e
 :val d
 :val f
 :val Modified
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 

 :comment T7
 :transition
:var x
:var j
:guard  (= actT2 false)(= flag 0)(not (= T1_cid NULL_Customer))(= T1_status AdjustmentsRequired)(not (= d NULL_Item))(not (= f NULL_Num))(= CandQuote1[x] NULL_Customer)(= CandQuote2[x] NULL_Item)(= CandQuote3[x] NULL_Num)(= CandQuote4[x] NULL_String)
:uguard (not (= CandQuote1[j] T1_cid))(not (= CandQuote2[j] T1_iid))(not (= CandQuote3[j] T1_unit))(not (= CandQuote4[j] T1_quote_states))
:numcases 2
:case (= j x)
 :val T1_cid 
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j]

 :val NULL_String
 :val e
 :val d
 :val f
 :val Modified
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag 
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val NULL_String
 :val e
 :val d
 :val f
 :val Modified
 :val T2_status
 :val T2_quote_states 
 :val T2_cid 
 :val T2_iid 
 :val T2_unit
 :val T2_days_passed 
 :val actT2
 :val flag
 
 :comment T_1 ApproveQuotation
 
 :comment T8
 :transition
 :var j
 :guard  (= actT2 false)(= flag 0)(= T1_status QuoteCreated)
 :numcases 1
 :case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

  :val QuoteApproved
  :val T1_cid
  :val T1_iid
  :val T1_unit
  :val Approved
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
 
  :comment T9
 :transition
 :var j
 :guard  (= actT2 false)(= flag 0)(= T1_status QuoteCreated)
 :numcases 1
 :case 
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

  :val AdjustmentsRequired
  :val T1_cid
  :val T1_iid
  :val T1_unit
  :val New
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
  
    :comment T10
 :transition
 :var j
 :guard  (= actT2 false)(= flag 0)(= T1_status QuoteCreated)
 :numcases 1
 :case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j]  

  :val Refusal
  :val T1_cid
  :val T1_iid
  :val T1_unit
  :val Refused
  :val T2_status
  :val T2_quote_states 
  :val T2_cid 
  :val T2_iid 
  :val T2_unit
  :val T2_days_passed 
  :val actT2
  :val flag 
 
 
   
 	:comment  T_2: QuoteMgmt
	
	:comment T_2 opening
	
   :comment T11
   :transition
   :var j
   :guard  (= actT2 false)(= flag 0)(= T1_status QuoteApproved)
   :numcases 1
   :case 
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j]  

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val NULL_String
    :val T1_quote_states 
    :val T1_cid 
    :val T1_iid 
    :val T1_unit
    :val 0 
    :val true
    :val flag 
	
	:comment T_2 SendToCustomer
	
   :comment T12
   :transition
   :var j
   :guard  (= actT2 true)(= flag 0)(= T2_status NULL_String)(>= o 0)
   :numcases 1
   :case
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j] 

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val ProceedAdjust
    :val T2_quote_states 
    :val T2_cid 
    :val T2_iid 
    :val T2_unit
    :val o
    :val actT2
    :val flag 

	
	
	:comment T13
   :transition
   :var j
   :guard  (= actT2 true)(= flag 0)(= T2_status NULL_String)(>= o 0)
   :numcases 1
   :case 
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j] 

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val Proceedd
    :val T2_quote_states 
    :val T2_cid 
    :val T2_iid 
    :val T2_unit
    :val o
    :val actT2
    :val flag 
   
	
	
	:comment T14
   :transition
   :var j
   :guard  (= actT2 true)(= flag 0)(= T2_status NULL_String)(>= o 0)
   :numcases 1
   :case 
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j] 

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val NotProceed
    :val T2_quote_states 
    :val T2_cid 
    :val T2_iid 
    :val T2_unit
    :val o
    :val actT2
    :val flag 
 
	:comment T_2 CancelQuote
	
		:comment T15
   :transition
   :var j
   :guard  (= actT2 true)(= flag 0)(= T2_status NotProceed)
   :numcases 1
   :case 
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j] 

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val QuoteCanceled
    :val T2_quote_states 
    :val T2_cid 
    :val T2_iid 
    :val T2_unit
    :val T2_days_passed
    :val actT2
    :val flag 
	
		:comment T16
   :transition
   :var j
   :guard  (= actT2 true)(= flag 0)(>= T2_days_passed 5)
   :numcases 1
   :case 
    :val CandQuote1[j] 
    :val CandQuote2[j]
    :val CandQuote3[j] 
    :val CandQuote4[j] 
    :val Notification1[j] 
    :val Notification2[j] 
    :val Notification3[j] 
    :val Notification4[j] 
    :val Notification5[j] 

    :val T1_status
    :val T1_cid
    :val T1_iid
    :val T1_unit
    :val T1_quote_states
    :val QuoteCanceled
    :val T2_quote_states 
    :val T2_cid 
    :val T2_iid 
    :val T2_unit
    :val T2_days_passed
    :val actT2
    :val flag 
	
	:comment T_2 NotifyCustomer
 
 :comment T17
 :transition
:var x
:var j
:guard  (= actT2 true)(= flag 0)(= T2_status Proceedd)(= Notification1[x] NULL_Customer)(= Notification2[x] NULL_Item)(= Notification3[x] NULL_Num)(= Notification4[x] NULL_String)(= Notification5[x] NULL_String)
:uguard (not (= Notification1[j] T2_cid))(not (= Notification2[j] T2_iid))(not (= Notification3[j] T2_unit))(not (= Notification4[j] T2_quote_states))(not (= Notification5[j] T2_status))
:numcases 2
:case (= j x)
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val T2_cid
 :val T2_iid 
 :val T2_unit
 :val T2_quote_states
 :val T2_status


 :val T1_status
 :val T1_cid
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notified
 :val m
 :val T2_cid
 :val T2_iid
 :val T2_unit
 :val T2_days_passed
 :val actT2
 :val 1 
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 


  :val T1_status
  :val T1_cid
  :val T1_iid
  :val T1_unit
  :val T1_quote_states
  :val Notified
  :val m
  :val T2_cid
  :val T2_iid
  :val T2_unit
  :val T2_days_passed
  :val actT2
  :val 1 
 
  :comment T18
 :transition
:var x
:var j
:guard  (= actT2 true)(= flag 0)(= T2_status QuoteCanceled)(= Notification1[x] NULL_Customer)(= Notification2[x] NULL_Item)(= Notification3[x] NULL_Num)(= Notification4[x] NULL_String)(= Notification5[x] NULL_String)
:uguard (not (= Notification1[j] T2_cid))(not (= Notification2[j] T2_iid))(not (= Notification3[j] T2_unit))(not (= Notification4[j] T2_quote_states))(not (= Notification5[j] T2_status))
:numcases 2
:case (= j x)
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val T2_cid
 :val T2_iid 
 :val T2_unit
 :val T2_quote_states
 :val T2_status


 :val T1_status
 :val T1_cid
 :val T1_iid
 :val T1_unit
 :val T1_quote_states
 :val Notified
 :val m 
 :val T2_cid
 :val T2_iid
 :val T2_unit
 :val T2_days_passed
 :val actT2
 :val 1
:case
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 


  :val T1_status
  :val T1_cid
  :val T1_iid
  :val T1_unit
  :val T1_quote_states
  :val Notified
  :val m
  :val T2_cid
  :val T2_iid
  :val T2_unit
  :val T2_days_passed
  :val actT2
  :val 1 

 :comment T19
 :transition
:var j
:guard  (= actT2 true)(= flag 1)
:numcases 1
:case 
 :val CandQuote1[j] 
 :val CandQuote2[j]
 :val CandQuote3[j] 
 :val CandQuote4[j] 
 :val Notification1[j] 
 :val Notification2[j] 
 :val Notification3[j] 
 :val Notification4[j] 
 :val Notification5[j] 

 :val T1_status 
 :val T1_cid 
 :val T1_iid 
 :val T1_unit 
 :val T1_quote_states 
 :val T2_status 
 :val T2_quote_states
 :val T2_cid 
 :val T2_iid
 :val T2_unit 
 :val o
 :val actT2 
 :val 0
 

      :comment  T_2 closing
	
      :comment T20
      :transition
      :var j
      :guard  (= actT2 true) (= flag 0)(= T2_status Notified) 
      :numcases 1
      :case 
       :val CandQuote1[j] 
       :val CandQuote2[j]
       :val CandQuote3[j] 
       :val CandQuote4[j]
       :val NULL_Customer
       :val NULL_Item 
       :val NULL_Num
       :val NULL_String
       :val NULL_String

       :val T2_status
       :val T1_cid
       :val T1_iid
       :val T1_unit
       :val T1_quote_states
       :val T2_status
       :val T2_quote_states 
       :val T2_cid 
       :val T2_iid 
       :val T2_unit
       :val T2_days_passed
       :val false
       :val flag 
	   
	   
	         :comment T21
      :transition
      :var j
      :guard  (= actT2 true)(= flag 0) (= T2_status ProceedAdjust) 
      :numcases 1
      :case 
       :val CandQuote1[j] 
       :val CandQuote2[j]
       :val CandQuote3[j] 
       :val CandQuote4[j]
       :val NULL_Customer
       :val NULL_Item 
       :val NULL_Num
       :val NULL_String
       :val NULL_String

       :val T2_status
       :val T1_cid
       :val T1_iid
       :val T1_unit
       :val T1_quote_states
       :val T2_status
       :val T2_quote_states 
       :val T2_cid 
       :val T2_iid 
       :val T2_unit
       :val T2_days_passed
       :val false
       :val flag 

