
:index int

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




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

:smt (define Sname::(-> int int))
:smt (define G1::(-> int int))
:smt (define G2::(-> int int))
:smt (define G3::(-> int int))
:smt (define p1::(-> int int))
:smt (define p2::(-> int int))
:smt (define p3::(-> int int))
:smt (define Gname::(-> int int))
:smt (define Cname::(-> int int))
:smt (define Crecord::(-> int int))

:smt (define No ::int)
:smt (define Yes ::int)
:smt (define AnalyzeRequest ::int)
:smt (define SelectingSupplier ::int)
:smt (define SupplierSelected ::int)
:smt (define ResultSent ::int)
:smt (define Acquired ::int)
:smt (define Good ::int)
:smt (define NoticeSent::int)


:db_driven 
:db_functions Sname G1 G2 G3 p1 p2 p3 Gname Cname Crecord  
:db_constants  No Yes AnalyzeRequest SelectingSupplier SupplierSelected
:db_constants ResultSent Acquired Good NoticeSent
:db_relations 


:local Cand int
:local Log1 int
:local Log2 int
:local Log3 int
:local Log4 int
:local Log5 int

:global T1_Cid int
:global T1_g1 int
:global T1_g2 int
:global T1_g3 int
:global T1_Sid int
:global T1_status int
:global T1_HasSupp int
:global T1_SuppResp int
:global T2_g1 int
:global T2_g2 int
:global T2_g3 int
:global T2_Sid int
:global T2_status int
:global flagReReq int
:global flagSendNo int
:global flagChooseSup int
:global actT2 bool






:smt (define (Guardia p::bool T2g1::int T2g2::int T2g3::int T2Sid::int )::bool (and  (=> (not (= T2g1 NULL)) (or (and p (= (G1 T2Sid) T2g1)) (and p (= (G2 T2Sid) T2g1)) (and p (= (G3 T2Sid) T2g1)))) (=> (not (= T2g2 NULL)) (or (and p (= (G1 T2Sid) T2g2)) (and p (= (G2 T2Sid) T2g2)) (and p (= (G3 T2Sid) T2g2)))) (=> (not (= T2g3 NULL)) (or (and p (= (G1 T2Sid) T2g3)) (and p (= (G2 T2Sid) T2g3)) (and p (= (G3 T2Sid) T2g3)))) ))



:initial
:var x
:cnj (=  T1_Cid  NULL) (=  T1_g1  NULL) (=  T1_g2  NULL) (=  T1_g3  NULL) (=  T1_Sid  NULL) (=  T1_status  NULL) (= T1_HasSupp NULL) (= T1_SuppResp NULL) (= T2_g1 NULL) (= T2_g2 NULL) (= T2_g3 NULL) (= T2_status NULL) (= T2_Sid NULL) (= Cand[x] NULL) (= Log1[x] NULL)(= Log2[x] NULL)(= Log3[x] NULL)(= Log4[x] NULL)(= Log5[x] NULL) (= flagReReq 0) (= flagSendNo 0) (= flagChooseSup 0) (= actT2 false)

:u_cnj (= T1_SuppResp Yes) (= T1_Cid NULL) (not (= T1_status NoticeSent))(not (= T1_status Acquired))

:eevar e 
:eevar d 
:eevar f 
:eevar g 
:eevar h 
:eevar l 
:eevar m 
:eevar n 
:eevar o 


:comment part1
:comment T1
:transition
:var j
:guard  (= flagReReq 0) (= flagSendNo 0) (= flagChooseSup 0)(= actT2 false) (not (= e NULL))
:numcases 1
:case  
 :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 
 :val e
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val NULL
 :val AnalyzeRequest
 :val NULL
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 1
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
 
:comment T2
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= d NULL))
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 
 :val T1_Cid[j]
 :val d
 :val f
 :val g
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
 :comment T3
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= d NULL))
:numcases 1
:case 
  :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val d
 :val NULL
 :val NULL
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 


:comment T4
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= f NULL))
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val d
 :val f
 :val g
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
 :comment T5
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= f NULL))
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val NULL
 :val f
 :val NULL
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
:comment T6
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= g NULL))
:numcases 1
:case 
:val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val d
 :val f
 :val g
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
:comment T7
:transition
:var j
:guard  (= flagReReq 1)(= flagSendNo 0) (= flagChooseSup 0) (not (= g NULL))
:numcases 1
:case 
:val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val NULL
 :val NULL
 :val g
 :val T1_Sid[j] 
 :val T1_status[j]
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val 0
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 


 
 

 :comment T_1 AnalyzeAcquisitionRequest 

:comment T8
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0)(= actT2 false) (=  T1_status AnalyzeRequest)  (not (= T1_Cid NULL))  (= (Crecord T1_Cid) Good) 
:numcases 1
:case 
:val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val SelectingSupplier
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
 

 
:comment T_1 SendNoSuppliersNotice 


:comment T9
:transition
:var x
:var j
:guard  (= flagChooseSup 0) (= flagSendNo 0) (= flagReReq 0) (= actT2 false) (=  T1_status SupplierSelected) (= T1_Sid NULL) (= NULL Log1[x]) 
:uguard (not (= Log1[j] T1_Cid))
:numcases 2
:case (= x j)
:val Cand[j]
 :val T1_Cid
 :val T1_g1[j]
 :val T1_g2[j]
 :val T1_g3[j]
 :val T1_HasSupp[j]
 
 :val e
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
:case 
:val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val e
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
:comment T10 // con e=NULL
:transition
:var x
:var j
:guard  (= flagChooseSup 0) (= flagSendNo 0) (= flagReReq 0) (= actT2 false) (=  T1_status SupplierSelected) (= T1_Sid NULL) (= NULL Log1[x]) 
:uguard (not (= Log1[j] T1_Cid))
:numcases 2
:case (= x j)
:val Cand[j]
 :val T1_Cid 
 :val T1_g1
 :val T1_g2
 :val T1_g3
 :val T1_HasSupp

 :val NULL
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
:case 
 :val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 
 :val NULL
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
  




 :comment part 2
 
:comment T11
 :transition
:var x
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0) (= actT2 false) (= T1_SuppResp No) (= NULL Log1[x])  
:numcases 2
:uguard (not (= Log1[j] T1_Cid))
:case (= x j)
:val Cand[j]
 :val T1_Cid 
 :val T1_g1
 :val T1_g2
 :val T1_g3
 :val T1_HasSupp

 :val e
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
:case 
:val Cand[j]
 :val Log1[j] 
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 

 :val e
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
 
 :comment part 2
 
:comment T12 // con e=NULL
 :transition
:var x
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0) (= actT2 false) (= T1_SuppResp No) (= NULL Log1[x])  
:numcases 2
:uguard (not (= Log1[j] T1_Cid))
:case (= x j)
 :val Cand[j]
 :val T1_Cid 
 :val T1_g1
 :val T1_g2
 :val T1_g3
 :val T1_HasSupp

 :val NULL
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val NULL
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 1
 :val flagChooseSup
 :val actT2
 
 :comment part3: 
:comment T13
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 1)(= flagReReq 0) 
:numcases 1
:case
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val d
 :val f 
 :val g
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 2
 :val flagChooseSup
 :val actT2

:comment T14
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 1)(= flagReReq 0) 
:numcases 1
:case
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val NULL
 :val NULL
 :val NULL
 :val T1_Sid[j] 
 :val NoticeSent
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j]
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 2
 :val flagChooseSup
 :val actT2
 

 
:comment part6:
:comment T15
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 2)(= flagReReq 0)  
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val h
 :val T1_status
 :val n
 :val o
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 0
 :val flagChooseSup
 :val actT2


:comment T16
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 2)(= flagReReq 0)  
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val h
 :val T1_status
 :val NULL
 :val NULL
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 0
 :val flagChooseSup
 :val actT2
 
:comment T17
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 2)(= flagReReq 0)  
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val NULL
 :val T1_status
 :val NULL
 :val NULL
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val 0
 :val flagChooseSup
 :val actT2
 



:comment T_1 SubmitResultToSupplier

:comment T18
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0)(= actT2 false)(=  T1_status SupplierSelected) (not (= T1_Sid NULL)) 
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val ResultSent
 :val T1_HasSupp[j] 
 :val Yes
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
:comment T19
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0)(= actT2 false)(=  T1_status SupplierSelected) (not (= T1_Sid NULL)) 
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val ResultSent
 :val T1_HasSupp[j] 
 :val No
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 



:comment T_1 AcquireDeliverGood 

:comment T20
:transition
:var j
:guard  (= flagChooseSup 0)(= flagSendNo 0)(= flagReReq 0)(= actT2 false)(=  T1_SuppResp Yes) 
:numcases 1
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val Acquired 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 


:comment T_2 opening 

:comment T21
:transition
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0)(= actT2 false)(= T1_status SelectingSupplier) 
:numcases 1
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val NULL
 :val NULL
 :val flagReReq 
 :val flagSendNo
 :val flagChooseSup
 :val true
 

:comment T_2 AddSupplier 


:comment T22
:transition
:var x
:var j
:guard (= flagReReq 0) (= flagSendNo 0) (= flagChooseSup 0) (= actT2 true)   (= Cand[x] NULL) (not (= h NULL))    
:uguard (not (= Cand[j] T2_Sid))
:numcases 2
:case 
:val T2_Sid
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]

 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val h
 :val T2_status[j]
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]

 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val h
 :val T2_status[j]
 :val flagReReq 
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 

:comment T_2 ChooseSupplier 
 

:comment T23
:transition
:var x
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0) (= actT2 true) (not (= Cand[x] NULL))
:numcases 2
:case (= x j)
:val NULL
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]

 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val Cand[x]
 :val m
 :val flagReReq 
 :val flagSendNo
 :val 1
 :val actT2
 
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val Cand[x]
 :val m
 :val flagReReq
 :val flagSendNo
 :val 1
 :val actT2

:comment T24
:transition
:var x
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0) (= actT2 true) (not (= Cand[x] NULL))
:numcases 2
:case (= x j)
:val NULL
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val Cand[x]
 :val NULL
 :val flagReReq 
 :val flagSendNo
 :val 1
 :val actT2
 
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val Cand[x]
 :val NULL
 :val flagReReq
 :val flagSendNo
 :val 1
 :val actT2
 
 
:comment T25
:transition
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 1) (= actT2 true)(not  (= T2_Sid NULL)) (Guardia true T2_g1 T2_g2 T2_g3 T2_Sid)
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid[j]
 :val T2_status[j]
 :val flagReReq 
 :val flagSendNo
 :val 0
 :val actT2
 

:comment T_2 ChooseOptimalSupplier 

:comment T26
:transition
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0) (= actT2 true)(= T2_status NULL)(not (= T2_Sid NULL)) 
:numcases 1
:case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid
 :val SupplierSelected
 :val flagReReq 
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 
 


:comment T_2 ChooseNoSupplier 

:comment T27
:transition
:var j
:guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0) (= actT2 true)(= T2_status NULL)(= T2_Sid NULL) 
:numcases 1
:case 
 :val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j] 
 :val T1_Cid[j]
 :val T1_g1[j] 
 :val T1_g2[j] 
 :val T1_g3[j] 
 :val T1_Sid[j] 
 :val T1_status[j] 
 :val T1_HasSupp[j] 
 :val T1_SuppResp[j] 
 :val T2_g1[j] 
 :val T2_g2[j] 
 :val T2_g3[j] 
 :val T2_Sid
 :val SupplierSelected
 :val flagReReq
 :val flagSendNo
 :val flagChooseSup
 :val actT2
 

 
 :comment T_2 closing 

 :comment T28
 :transition
 :var j
 :guard (= flagReReq 0)(= flagSendNo 0)(= flagChooseSup 0)(= actT2 true) (= T2_status SupplierSelected) 
 :numcases 1
 :case 
:val Cand[j]
 :val Log1[j]
 :val Log2[j]
 :val Log3[j]
 :val Log4[j]
 :val Log5[j]

  :val T1_Cid[j]
  :val T1_g1[j] 
  :val T1_g2[j] 
  :val T1_g3[j] 
  :val T2_Sid[j] 
  :val T2_status[j] 
  :val T1_HasSupp[j] 
  :val T1_SuppResp[j] 
  :val T2_g1[j] 
  :val T2_g2[j] 
  :val T2_g3[j] 
  :val T2_Sid[j]
  :val T2_status[j]
  :val flagReReq 
  :val flagSendNo
  :val flagChooseSup
  :val false
  
