

:comment documentazione dell'esempio


:index int



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

:smt (define-type CompInId) 
:smt (define-type JobCatId) 
:smt (define-type EmpId)
:smt (define-type UserId)
:smt (define-type Num)
:smt (define-type String)


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




:smt (define what ::(-> CompInId JobCatId))
:smt (define who ::(-> CompInId EmpId))
:smt (define jobCatDescr ::(-> JobCatId String))
:smt (define empName ::(-> EmpId String))
:smt (define userName ::(-> UserId String))


:smt (define Published ::String)
:smt (define Open ::String)
:smt (define Success ::String)
:smt (define Received ::String)
:smt (define Registered ::String)
:smt (define Notified ::String)
:smt (define Winner ::String)
:smt (define Loser ::String)
:smt (define Ninety ::Num)
:smt (define Zero ::Num)



:db_driven 
:db_sorts CompInId JobCatId EmpId UserId Num String 
:db_functions what who jobCatDescr empName userName  
:db_constants  Published Open Success Received 
:db_constants Registered Notified Winner Loser Ninety Zero
:db_relations 


:local JobOffers1 JobCatId
:local JobOffers2 String
:local JobOffers3 String
:local JobOffers4 String
:local Application1 UserId
:local Application2 JobCatId
:local Application3 EmpId
:local Application4 int
:local Application5 String



:global T1_uid UserId
:global T1_eid EmpId
:global T1_jid JobCatId
:global T1_jtype String
:global T1_timeout Num
:global T1_score int
:global T1_pos_status String
:global T1_date String
:global T2_uid UserId
:global T2_eid EmpId
:global T2_jid JobCatId
:global T2_jtype String
:global T2_app_status String
:global T3_uid UserId
:global T3_eid EmpId
:global T3_jid JobCatId
:global T3_score int
:global T3_withdraw_status String
:global actT2 bool
:global actT3 bool
:global Init bool
:global SelectedJob bool
:global SelectedApplication bool




:initial
:var x
:cnj (=  T1_uid  NULL_UserId) (=  T1_eid NULL_EmpId) (=  T1_jid  NULL_JobCatId) (=  T1_jtype  NULL_String) (=  T1_timeout NULL_Num) (=  T1_score -1) (= T1_pos_status NULL_String) (= T1_date NULL_String)(= T2_uid NULL_UserId)(= T2_eid NULL_EmpId)(= T2_jid NULL_JobCatId)(= T2_jtype NULL_String)(= T2_app_status NULL_String)(= T3_uid NULL_UserId)(= T3_eid NULL_EmpId)(= T3_jid NULL_JobCatId) (= T3_withdraw_status NULL_String)(= SelectedJob false)(= SelectedApplication false)(=  actT2 false)(= actT3 false)(= Init true)(= JobOffers1[x] NULL_JobCatId)(= JobOffers2[x] NULL_String)(= JobOffers3[x] NULL_String)(= JobOffers4[x] NULL_String)(= Application1[x] NULL_UserId)(= Application2[x] NULL_JobCatId)(= Application3[x] NULL_EmpId)(= Application4[x] -1)(= Application5[x] NULL_String)

:u_cnj (= T1_pos_status Notified)(not (= Application1[z1] NULL_UserId))(not (= Winner Application5[z1]))(not (= Loser Application5[z1]))

:eevar d JobCatId
:eevar e CompInId
:eevar f UserId
:eevar g EmpId
:eevar h int
:eevar l String
:eevar m String
:eevar n String
:eevar o String


:comment T_1: HiringProcess


:comment T_1 Init timeout
:comment T1
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= Init true)(= SelectedJob false)(= SelectedApplication false)(not (= f NULL_UserId))
:numcases 1
:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val f 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val Ninety
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3
:val false 
:val SelectedJob
:val SelectedApplication


:comment T_1 CreateJob

:comment T2
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= n NULL_String))(not (= d NULL_JobCatId)) (= (jobCatDescr d) m)(not (= T1_pos_status Open))(not (= T1_timeout Zero))
:numcases 1
:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]


:val T1_uid 
:val T1_eid 
:val d
:val m 
:val T1_timeout 
:val T1_score 
:val Open 
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status 
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication


:comment T_1 PositionJobOpening
:comment T3
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T1_jid NULL_JobCatId))(not (= T1_jtype NULL_String))(not (= T1_date NULL_String))(= T1_pos_status Open)(= JobOffers1[x] NULL_JobCatId)(= JobOffers2[x] NULL_String)(= JobOffers3[x] NULL_String)(= JobOffers4[x] NULL_String)(not (= T1_timeout Zero))
:uguard (not (= JobOffers1[j] T1_jid))(not (= JobOffers2[j] T1_date))(not (= JobOffers3[j] T1_jtype))(not (= JobOffers4[x] T1_pos_status))
:numcases 2
:case (= x j)
 :val T1_jid 
 :val T1_date
 :val T1_jtype 
 :val T1_pos_status
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]

:val f
:val g
:val d
:val m
:val T1_timeout 
:val T1_score 
:val Published 
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status 
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:case 
  :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]

:val f
:val g
:val d
:val m
:val T1_timeout 
:val T1_score 
:val Published 
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init 
:val SelectedJob
:val SelectedApplication

:comment T_1 Waiting
:comment T4
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T1_pos_status Open))(not (= T1_timeout Zero))
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val Zero
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication



:comment T_1 JobOfferSelect
:comment T5
:transition
:var j
:var x
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(= T1_pos_status Published)(not (= d NULL_JobCatId))(= JobOffers1[x] d)(= JobOffers2[x] n)(= JobOffers3[x] (jobCatDescr d))(= JobOffers4[x] Open)(not (= T1_timeout Zero))
:numcases 2
:case (= x j)
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]


:val NULL_UserId
:val NULL_EmpId
:val d
:val (jobCatDescr d) 
:val T1_timeout
:val -1
:val Published
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val true
:val SelectedApplication

:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]


:val NULL_UserId
:val NULL_EmpId
:val d
:val (jobCatDescr d) 
:val T1_timeout
:val -1
:val Published
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val true
:val SelectedApplication


:comment T_1 AssessApplication
:comment T6
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T1_pos_status Open))(not (= Application1[x] NULL_UserId))(= Application4[x] -1)(>= h 0)(<= h 100)(not (= T1_timeout Zero))
:numcases 2
:case (= x j)
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j] 
 :val JobOffers4[j] 
 :val Application1[x]
 :val Application2[x]
 :val Application3[x]
 :val h
 :val Application5[j]


:val T1_uid 
:val T1_eid
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j]
 :val Application2[j]
 :val Application3[j]
 :val Application4[j]
 :val Application5[j]


:val T1_uid 
:val T1_eid
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:comment T_1 DetermineWinner1
:comment T7
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T1_pos_status Open))(not (= T1_pos_status Notified)) (= T1_timeout Zero)
:numcases 2
:case (> Application4[j] 80)
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Winner


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val Notified
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Loser 


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val Notified
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication



:comment T_1 SelectedApplication
:comment T8
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T1_pos_status Open))(not (= Application1[x] NULL_UserId))(not (= Application3[x] NULL_EmpId))(not (= Application2[x] NULL_JobCatId))
:numcases 2
:case (= x j)
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]  


:val Application1[x]  
:val Application3[x] 
:val Application2[x] 
:val m
:val T1_timeout
:val Application4[x] 
:val Published
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid 
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val true

:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val Application1[x]  
:val Application3[x] 
:val Application2[x] 
:val m
:val T1_timeout
:val Application4[x] 
:val Published
:val n
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid 
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val true

:comment T_2 Application


:comment T_2 Opening 
:comment T9
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= SelectedJob true) (= SelectedApplication false)(= T1_pos_status Published)(not (= T1_jid NULL_JobCatId))(not (= T1_jtype NULL_String))
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]

:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype
:val T1_timeout
:val T1_score 
:val T1_pos_status
:val T1_date
:val NULL_UserId 
:val NULL_EmpId
:val T1_jid
:val T1_jtype 
:val NULL_String  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val true
:val actT3 
:val Init
:val false
:val SelectedApplication


:comment T_2 ReceiveApplication
:comment T10
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(not (= T2_jid NULL_JobCatId))(not (= T2_jtype NULL_String))(= T2_app_status NULL_String)(not (= e NULL_CompInId))(= (who e) g)(= (what e) T2_jid)(not (= f NULL_UserId))
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val f 
:val g
:val T2_jid
:val T2_jtype 
:val Received  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:comment T_2 RegisterApplication
:comment T11
:transition
:var x
:var j
:guard  (= actT2 true)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(= T2_app_status Received)(= Application1[x] NULL_UserId)(= Application2[x] NULL_JobCatId)(= Application3[x] NULL_EmpId)(= Application4[x] -1) (not (= T2_jid NULL_JobCatId))(not (= T2_uid NULL_UserId))(not (= T2_eid NULL_EmpId))
:uguard (not (= Application1[j] T2_uid))(not (= Application2[j] T2_jid))(not (= Application3[j] T2_eid))
:numcases 2
:case (= x j)
 :val JobOffers1[j] 
 :val JobOffers2[j]
 :val JobOffers3[j] 
 :val JobOffers4[j] 
 :val T2_uid
 :val T2_jid
 :val T2_eid
 :val -1 
 :val NULL_String


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val Registered  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication
:case 
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]

:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val Registered  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication


:comment T_2 Closing
:comment T12
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication false)(= T2_app_status Registered)
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val Registered  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status 
:val false
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication



:comment T_3: Withdraw

:comment T_3 Opening
:comment T13
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= Init false)(= SelectedJob false)(= SelectedApplication true)(not (= T1_jid NULL_JobCatId))(not (= T1_uid NULL_UserId))(not (= T1_eid NULL_EmpId))
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T1_uid 
:val T1_eid
:val T1_jid
:val T1_score 
:val NULL_String
:val actT2 
:val true
:val Init
:val SelectedJob
:val false

:comment T_3 WithdrawDone

:comment T14
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 true)(= Init false)(= SelectedJob false)(= SelectedApplication false)(= Application1[x] T3_uid)(= Application2[x] T3_jid )(= Application3[x] T3_eid)(= Application4[x] T3_score)(= T3_withdraw_status NULL_String)
:numcases 2
:case (= j x)
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val NULL_UserId 
 :val NULL_JobCatId
 :val NULL_EmpId 
 :val -1
 :val NULL_String

:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val Success
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j]
  
:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val Success
:val actT2 
:val actT3 
:val Init
:val SelectedJob
:val SelectedApplication

:comment T_3 Closing
:comment T15
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= Init false)(= SelectedJob false)(= SelectedApplication false)(= T3_withdraw_status Success)
:numcases 1
:case
 :val JobOffers1[j] 
 :val JobOffers2[j] 
 :val JobOffers3[j]
 :val JobOffers4[j]
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 


:val T1_uid 
:val T1_eid 
:val T1_jid
:val T1_jtype 
:val T1_timeout
:val T1_score 
:val T1_pos_status 
:val T1_date 
:val T2_uid 
:val T2_eid 
:val T2_jid
:val T2_jtype 
:val T2_app_status  
:val T3_uid 
:val T3_eid
:val T3_jid
:val T3_score 
:val T3_withdraw_status
:val actT2 
:val false 
:val Init
:val SelectedJob
:val SelectedApplication
