:comment Running example BPM 19

:comment This  specification formalizes the example of a job hiring process in a company presented in BPM19.
:comment Property to be checked:  we exit the loop after a qualified candidate has been found, and the case variable ''time_passed'' says that OneMonth is passed. Remember that EvaluateCV and AssignWinner tasks are executed instantaneously.
:comment The tool returns SAFE!

:index int



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

:smt (define-type JobCatId) 
:smt (define-type UserId)
:smt (define-type StringName)
:smt (define-type NumAge)
:smt (define-type BOOLE)
:smt (define-type String)
:smt (define-type StringDate)
:smt (define-type StringControl)



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



:smt (define userName ::(-> UserId StringName))
:smt (define userAge ::(-> UserId NumAge))



:smt (define Eligible ::String)
:smt (define NotEligible ::String)
:smt (define OneMonth ::StringDate)
:smt (define OneMonthPlusOneWeek ::StringDate)
:smt (define LessThanOneMonth ::StringDate)
:smt (define Qualified ::String)
:smt (define Idle ::StringControl)
:smt (define Enabled ::StringControl)
:smt (define Completed ::StringControl)
:smt (define Error ::StringControl)
:smt (define Waiting :: StringControl)
:smt (define TRUE ::BOOLE)
:smt (define FALSE ::BOOLE)



:db_driven 
:db_sorts JobCatId UserId  StringName NumAge String StringDate StringControl BOOLE
:db_functions userName  userAge
:db_constants  Eligible NotEligible OneMonth Qualified OneMonthPlusOneWeek LessThanOneMonth
:db_constants Idle Enabled Completed Error Waiting TRUE FALSE
:db_relations 


:local Application1 UserId
:local Application2 JobCatId
:local Application3 StringName
:local Application4 NumAge
:local Application5 int
:local Application6 String


:global case_jid JobCatId
:global case_uid UserId
:global case_nameuid StringName
:global case_ageuid NumAge
:global case_result String
:global case_winner UserId
:global case_time_passed StringDate
:global case_qualif BOOLE
:global lcycleBProc StringControl
:global lcycleBStart StringControl
:global lcycleBseq StringControl
:global lcycleBForExc StringControl
:global lcycleBseq1 StringControl
:global lcycleBloop StringControl
:global lcycleBseq2 StringControl
:global lcycleBAppRec StringControl
:global lcycleBEvCV StringControl
:global lcycleBEvApp StringControl
:global lcycleBAssWin StringControl
:global lcycleBDecElig StringControl
:global lcycleBSelWin StringControl
:global lcycleBMakeOf StringControl
:global lcycleBSubProc StringControl


:initial
:var x
:cnj (=  case_jid  NULL_JobCatId) (=  case_uid NULL_UserId) (= case_nameuid NULL_StringName) (=  case_ageuid  NULL_NumAge) (=  case_result NULL_String) (=  case_winner NULL_UserId) (= case_time_passed NULL_StringDate) (= case_qualif FALSE)(= lcycleBProc Enabled)(= lcycleBStart Idle)(= lcycleBseq Idle)(= lcycleBForExc Idle)(=  lcycleBseq1  Idle)(= lcycleBloop Idle)(=  lcycleBseq2  Idle)(= lcycleBAppRec Idle)(= lcycleBEvCV Idle)(= lcycleBEvApp Idle)(= lcycleBAssWin Idle)(= lcycleBDecElig Idle)(= lcycleBSelWin Idle)(= lcycleBMakeOf Idle)(= lcycleBSubProc Idle)(= Application1[x] NULL_UserId)(= Application2[x] NULL_JobCatId)(= Application3[x] NULL_StringName)(= Application4[x] NULL_NumAge)(= Application5[x] 0)(= Application6[x] NULL_String)

:u_cnj (= case_qualif TRUE)(= case_time_passed OneMonth)

:eevar d JobCatId
:eevar e UserId
:eevar g StringName
:eevar h NumAge
:eevar l int
:eevar m String
:eevar n StringDate
:eevar o StringControl
:eevar p BOOLE


:comment T1: Process Block 1

:transition
:var j
:guard  (= lcycleBProc Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val Waiting 
 :val Enabled
 :val lcycleBseq 
 :val lcycleBForExc 
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf 
 :val lcycleBSubProc

:comment T2: Process Block 2

:transition
:var j
:guard  (= lcycleBStart Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val Idle
 :val Enabled 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc 

:comment T3: Process Block 3

:transition
:var j
:guard  (= lcycleBseq Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val Completed 
 :val lcycleBStart
 :val Idle 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc 

:comment T4: Sequence flow 1

:transition
:var j
:guard  (= lcycleBseq Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val Waiting
 :val Enabled 
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc 

:comment T5: Sequence flow 2

:transition
:var j
:guard  (= lcycleBForExc Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val Idle 
 :val lcycleBseq1
 :val lcycleBloop
 :val lcycleBseq2 
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val Enabled
 :val lcycleBSubProc

:comment T6: Sequence flow 3

:transition
:var j
:guard  (= lcycleBMakeOf Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val Completed
 :val lcycleBForExc 
 :val lcycleBseq1
 :val lcycleBloop
 :val lcycleBseq2 
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val Idle
 :val lcycleBSubProc

:comment T7: Forward Exc 1

:transition
:var j
:guard  (= lcycleBForExc Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val Waiting
 :val lcycleBseq1 
 :val lcycleBloop
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Enabled

:comment T8: Forward Exc 2

:transition
:var j
:guard  (= lcycleBSubProc Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val lcycleBloop
 :val lcycleBseq2 
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val Enabled 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Idle


:comment T9:Subproc 1

:transition
:var j
:guard  (= lcycleBSubProc Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val Enabled
 :val lcycleBseq2 
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Waiting

:comment T10:Subproc 2

:transition
:var j
:guard  (= lcycleBloop Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val Idle
 :val lcycleBseq2 
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Completed

:comment T11: Forward Exc 3

:transition
:var j
:guard  (= lcycleBAssWin Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val Completed 
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val Idle 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T12: Forward Exc 4

:transition
:var j
:guard  (= lcycleBAppRec Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner 
 :val OneMonth 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1 
 :val Idle 
 :val Idle
 :val Idle 
 :val Idle 
 :val Idle 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Error

:comment T13: Forward Exc 5

:transition
:var j
:guard  (= lcycleBSubProc Error)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc 
 :val Enabled
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val Idle

:comment T14: Forward Exc 6

:transition
:var j
:guard  (= lcycleBseq1 Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val Completed 
 :val Idle
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T15: Loop 1

:transition
:var j
:guard  (= lcycleBloop Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val Waiting 
 :val Enabled
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T16: Loop 2

:transition
:var j
:guard  (= lcycleBseq2 Completed)(= case_qualif TRUE)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc 
 :val lcycleBseq1
 :val Completed 
 :val Idle
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T17: Loop 3

:transition
:var j
:guard  (= lcycleBseq2 Completed)(= case_qualif FALSE)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val Idle
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val Enabled 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T18: Loop 4

:transition
:var j
:guard  (= lcycleBEvApp Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc 
 :val lcycleBseq1
 :val lcycleBloop 
 :val Enabled
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val Idle 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T19: Sequence flow1 1

:transition
:var j
:guard  (= lcycleBseq1 Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc 
 :val Waiting
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val Enabled 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T20: Sequence flow1 2

:transition
:var j
:guard  (= lcycleBDecElig Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val Idle 
 :val Enabled
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T21: Sequence flow1 3

:transition
:var j
:guard  (= lcycleBSelWin Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc 
 :val Completed
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val Idle
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T22: Sequence flow2   1

:transition
:var j
:guard  (= lcycleBseq2 Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val Waiting
 :val Enabled 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T23: Sequence flow2   2

:transition
:var j
:guard  (= lcycleBAppRec Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val Idle 
 :val Enabled 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T24: Sequence flow2   3

:transition
:var j
:guard  (= lcycleBEvCV Completed)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val Completed
 :val lcycleBAppRec 
 :val Idle
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T25: Start

:transition
:var j
:guard  (= lcycleBStart Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val d 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val Completed
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T26: ApplicationReceived   

:transition
:var j
:guard  (= lcycleBAppRec Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val e 
 :val g 
 :val h
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val Completed 
 :val lcycleBEvCV 
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T27: Evaluate CV 1

:transition
:var j
:guard  (= lcycleBEvCV Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val TRUE
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val Completed
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:comment T28: Evaluate CV 2

:transition
:var j
:guard  (= lcycleBEvCV Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val FALSE
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val Completed
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc


:comment T29: Evaluate Application 

:transition
:var x
:var j
:guard  (= lcycleBEvApp Enabled)(= Application1[x] NULL_UserId)(= Application2[x] NULL_JobCatId)(= Application3[x] NULL_StringName)(= Application4[x] NULL_NumAge)(= Application5[x] 0)(= Application6[x] NULL_String)(> l 0)(< l 101)
:numcases 2
:case (= j x)
 :val case_uid 
 :val case_jid
 :val case_nameuid 
 :val case_ageuid 
 :val l 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val Completed 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val Completed 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc


:comment T30: Decide Eligible

:transition
:var j
:guard  (= lcycleBDecElig Enabled)
:numcases 2
:case (> Application5[j] 80)
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Eligible

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val Completed 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc

:case
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val NotEligible

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val Completed 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc


:comment T31: Select Winner 

:transition
:var x
:var j
:guard  (= lcycleBSelWin Enabled)(= Application6[x] Eligible)
:numcases 2
:case (= j x)
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val Application2[x]
 :val Application1[x] 
 :val Application3[x] 
 :val Application4[x]
 :val Application6[x] 
 :val Application1[x]
 :val OneMonthPlusOneWeek 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val Completed
 :val lcycleBMakeOf
 :val lcycleBSubProc

:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val Application2[x]
 :val Application1[x] 
 :val Application3[x] 
 :val Application4[x]
 :val Application6[x] 
 :val Application1[x]
 :val OneMonthPlusOneWeek 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val lcycleBAssWin 
 :val lcycleBDecElig 
 :val Completed
 :val lcycleBMakeOf
 :val lcycleBSubProc



:comment T32:  Assign Winner 

:transition
:var j
:guard  (= lcycleBAssWin Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val Qualified 
 :val case_uid
 :val LessThanOneMonth
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val Completed 
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val lcycleBMakeOf
 :val lcycleBSubProc



:comment T33:  MakeOffer 

:transition
:var j
:guard  (= lcycleBMakeOf Enabled)
:numcases 1
:case 
 :val Application1[j] 
 :val Application2[j]
 :val Application3[j] 
 :val Application4[j] 
 :val Application5[j] 
 :val Application6[j]

 :val case_jid 
 :val case_uid 
 :val case_nameuid 
 :val case_ageuid
 :val case_result 
 :val case_winner
 :val case_time_passed 
 :val case_qualif
 :val lcycleBProc 
 :val lcycleBStart
 :val lcycleBseq 
 :val lcycleBForExc
 :val lcycleBseq1
 :val lcycleBloop 
 :val lcycleBseq2
 :val lcycleBAppRec 
 :val lcycleBEvCV
 :val lcycleBEvApp 
 :val lcycleBAssWin
 :val lcycleBDecElig 
 :val lcycleBSelWin
 :val Completed
 :val lcycleBSubProc


