

:comment documentation

:index int




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


:smt (define PatName ::(-> int int ))
:smt (define PatAddr ::(-> int int))
:smt (define DocName ::(-> int int))
:smt (define DocS1 ::(-> int int))
:smt (define DocS2 ::(-> int int))
:smt (define DocS3 ::(-> int int))
:smt (define SympName ::(-> int int))
:smt (define MedG1 ::(-> int int))
:smt (define MedG2 ::(-> int int))
:smt (define MedG3 ::(-> int int))
:smt (define MedB1 ::(-> int int))
:smt (define MedB2 ::(-> int int))
:smt (define MedB3 ::(-> int int))


:smt (define No ::int)
:smt (define Paid ::int)
:smt (define Init ::int)
:smt (define Yes ::int)
:smt (define WritingPrescription ::int)
:smt (define empty ::int)
:smt (define nonempty ::int)
:smt (define TakingMedicine ::int)
:smt (define Zero ::int)
:smt (define One ::int)

:db_driven 
 
:db_functions PatName PatAddr DocName DocS1 DocS2 DocS3 
:db_functions SympName MedG1 MedG2 MedG3 MedB1 MedB2 MedB3
:db_constants No Paid Init Yes WritingPrescription empty nonempty TakingMedicine Zero One
:db_relations

:local Request int
:local AvailableDoctor int
:local Symptons1 int
:local Symptons2 int
:local Symptons3 int
:local Prescription int

:global T1_pid int
:global T1_did int
:global T1_status int 
:global T2_pid int
:global T2_did int
:global T2_s1 int
:global T2_s2 int
:global T2_s3 int
:global T2_status int
:global T3_s1 int
:global T3_s2 int
:global T3_s3 int
:global T3_mid int
:global T3_status int
:global T3_med_status int
:global T3_has_good int
:global T3_has_bad int
:global actT2 bool
:global actT3 bool



:smt (define (Guardia1 T2did::int s1::int s2::int s3::int T2status::int A::int B::int)::bool(or(and (not (= s1 NULL))(=> (or (= (DocS1 T2did) s1)(= (DocS1 T2did) s2)(= (DocS1 T2did) s3)(= (DocS2 T2did) s1)(= (DocS2 T2did) s2)(= (DocS2 T2did) s3)(= (DocS3 T2did) s1)(= (DocS3 T2did) s2)(= (DocS3 T2did) s3)) (= T2status A)))(= T2status B)))

:smt (define (Guardia2 T3mid::int s1::int s2::int s3::int T3has::int A::int B::int )::bool(or(and (not (= s1 NULL))(=> (or (= (MedG1 T3mid) s1)(= (MedG1 T3mid) s2)(= (MedG1 T3mid) s3)(= (MedG2 T3mid) s1)(= (MedG2 T3mid) s2)(= (MedG2 T3mid) s3)(= (MedG3 T3mid) s1)(= (MedG3 T3mid) s2)(= (MedG3 T3mid) s3)) (= T3has A)))(= T3has B)))

:smt (define (Guardia3 T3mid::int s1::int s2::int s3::int T3has::int A::int B::int)::bool(or(and (not (= s1 NULL))(=> (or (= (MedB1 T3mid) s1)(= (MedB1 T3mid) s2)(= (MedB1 T3mid) s3)(= (MedB2 T3mid) s1)(= (MedB2 T3mid) s2)(= (MedB2 T3mid) s3)(= (MedB3 T3mid) s1)(= (MedB3 T3mid) s2)(= (MedB3 T3mid) s3)) (= T3has A)))(= T3has B)))

:initial
:var x
:cnj (=  T1_pid  NULL) (=  T1_did NULL) (=  T1_status  NULL) (=  T2_pid  NULL) (=  T2_did NULL) (=  T2_s1 NULL) (= T2_s2 NULL)(=  T2_s3 NULL) (= T2_status NULL)(= T3_s1 NULL)(= T3_s2 NULL)(= T3_s3 NULL)(= T3_mid NULL)(= T3_med_status NULL)(= T3_status NULL)(= T3_has_good NULL)(= T3_has_bad NULL)(= Request[x] NULL)(= AvailableDoctor[x] NULL)(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)(= Prescription[x] NULL)(= actT2 false)(= actT3 false)

:u_cnj  (not (= T1_pid NULL))(not (= T2_pid NULL))

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


:comment T_1: MakeAppointment

:comment T_1 EnterPatientInfo

:comment T1
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(not (= e NULL))
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val e 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

:comment T_1 AddRequest

:comment T2
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_pid NULL))(= Request[x] NULL)(not (= d NULL))(not (= f NULL))
:uguard (not (= Request[j] T1_pid))
:numcases 2
:case (= j x)
 :val T1_pid
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val d
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val d
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
:comment T3
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_pid NULL))(= Request[x] NULL)
:uguard (not (= Request[j] T1_pid))
:numcases 2
:case (= j x)
 :val T1_pid
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

 
 :comment T_1 RetrieveRequest
 
 :comment T4
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= Request[x] NULL))(not (= d NULL))(not (= f NULL))
:numcases 2
:case (= j x)
 :val NULL
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val Request[x]
 :val d
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val Request[x]
 :val d
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
 :comment T5
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= Request[x] NULL))
:numcases 2
:case (= j x)
 :val NULL
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val Request[x]
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val Request[x]
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
 :comment T_1 EnterDoctorInfo
 :comment T6
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(not (= d NULL))
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val d
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
  :comment T_1 AddDoctor
 :comment T7
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_did NULL))(= AvailableDoctor[x] NULL)(not (= e NULL))(not (= f NULL))
:uguard (not (= AvailableDoctor[j] T1_did))
:numcases 2
:case (= j x)
 :val Request[j]
 :val T1_did
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val e
 :val NULL
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val e
 :val NULL
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

 
 
 :comment T8
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_did NULL))(= AvailableDoctor[x] NULL)
:uguard (not (= AvailableDoctor[j] T1_did))
:numcases 2
:case (= j x)
 :val Request[j]
 :val T1_did
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val NULL
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
   :comment T_1 RetrieveDoctor
 :comment T9
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= AvailableDoctor[x] NULL))(not (= e NULL))(not (= f NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val NULL
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val e
 :val AvailableDoctor[x]
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val e
 :val AvailableDoctor[x]
 :val f
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

 :comment T10
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= AvailableDoctor[x] NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val NULL
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val AvailableDoctor[x]
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val NULL
 :val AvailableDoctor[x]
 :val NULL
 :val T2_pid 
 :val T2_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
 
 :comment T_2: SeeDoctor
 
 :comment T_2 opening
 :comment T11
 :transition
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_pid NULL))(not (= T1_did NULL))
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val NULL
 :val NULL
 :val NULL
 :val NULL
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val true 
 :val actT3
 
 
 :comment T_2 AddSympton
 :comment T12
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s1 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val m
 :val n
 :val o
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val m
 :val n
 :val o
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

 :comment T13
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s1 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
  
 :comment T14
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s2 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))(not (= m NULL))(not (= n NULL))(not (= o NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val m
 :val n
 :val o 
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val m 
 :val n
 :val o
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
:comment T15
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s2 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
  :comment T16
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s3 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val m
 :val n
 :val o
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val m
 :val n
 :val o
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
:comment T17
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(not (= T2_s3 NULL))(= Symptons1[x] NULL)(= Symptons2[x] NULL)(= Symptons3[x] NULL)
:uguard (not (= Symptons1[x] T2_s1))(not (= Symptons2[x] T2_s2))(not (= Symptons3[x] T2_s3))(not (= m NULL))(not (= n NULL))(not (= o NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val T2_s1
 :val T2_s2
 :val T2_s3
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val NULL
 :val NULL
 :val NULL
 :val Init
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
 :comment T_2 CheckSympton
   :comment T18
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status Init)(not (= Symptons1[x] NULL))(not (= Symptons2[x] NULL))(not (= Symptons3[x] NULL)) (Guardia1 T2_did T2_s1 T2_s2 T2_s3 T2_status Yes No)(not (= f NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val NULL
 :val NULL
 :val NULL
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val Symptons1[x]
 :val Symptons2[x]
 :val Symptons3[x]
 :val f
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val Symptons1[x] 
 :val Symptons2[x]
 :val Symptons3[x]
 :val f
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

   :comment T19
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status Init)(not (= Symptons1[x] NULL))(not (= Symptons2[x] NULL))(not (= Symptons3[x] NULL)) (Guardia1 T2_did T2_s1 T2_s2 T2_s3 T2_status Yes No)
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val NULL
 :val NULL
 :val NULL
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T2_pid 
 :val T2_did 
 :val Symptons1[x]
 :val Symptons2[x]
 :val Symptons3[x]
 :val NULL
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid 
 :val T1_did 
 :val T1_status 
 :val T2_pid 
 :val T2_did
 :val Symptons1[x] 
 :val Symptons2[x]
 :val Symptons3[x]
 :val NULL
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3
 
  :comment T_2 closing
 :comment T20
 :transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status No)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val NULL
 :val NULL
 :val NULL
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val false 
 :val actT3
 
 :comment T21
 :transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status Paid)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val NULL
 :val NULL
 :val NULL
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val T3_status 
 :val T3_med_status 
 :val T3_has_good 
 :val T3_has_bad 
 :val false 
 :val actT3
 
 :comment T_3: TakeMedicine
 
 :comment T_3 opening
  :comment T22
 :transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status Yes)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val NULL
 :val NULL
 :val NULL
 :val NULL 
 :val NULL
 :val actT2 
 :val true
 
 
  :comment T_3 StartPrescription
  :comment T23
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val WritingPrescription 
 :val empty
 :val T3_has_good 
 :val T3_has_bad 
 :val actT2 
 :val actT3

  :comment T_3 AddMedicine
  :comment T24
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 true)(not (= T3_mid NULL))(not (= g NULL))(= Prescription[x] NULL)
:uguard (not (= Prescription[j] T3_mid))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val T3_mid

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val g
 :val WritingPrescription
 :val nonempty
 :val f
 :val h
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val g
 :val WritingPrescription
 :val nonempty
 :val f
 :val h
 :val actT2 
 :val actT3

  :comment T25
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 true)(not (= T3_mid NULL))(not (= g NULL))(= Prescription[x] NULL)
:uguard (not (= Prescription[j] T3_mid))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val T3_mid

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val g
 :val WritingPrescription
 :val nonempty
 :val NULL
 :val NULL
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val g
 :val WritingPrescription
 :val nonempty
 :val NULL
 :val NULL
 :val actT2 
 :val actT3

  :comment T_3 FinishPrescription
  :comment T26
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status WritingPrescription)(= T3_med_status nonempty)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid 
 :val TakingMedicine 
 :val T3_med_status
 :val Zero
 :val Zero
 :val actT2 
 :val actT3
 
  :comment T_3 Checkout
  :comment T27
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(not (= Prescription[x] NULL))(not (= f NULL))(not (= h NULL))(not (= l NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val NULL

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val Prescription[x]
 :val TakingMedicine
 :val f
 :val h
 :val l
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val Prescription[x]
 :val TakingMedicine
 :val f
 :val h
 :val l
 :val actT2 
 :val actT3

  :comment T28
 :transition
 :var x
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(not (= Prescription[x] NULL))
:numcases 2
:case (= j x)
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val NULL

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val Prescription[x]
 :val TakingMedicine
 :val NULL
 :val NULL
 :val NULL
 :val actT2 
 :val actT3
:case
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val Prescription[x]
 :val TakingMedicine
 :val NULL
 :val NULL
 :val NULL
 :val actT2 
 :val actT3
 
  :comment T_3 UpdateCheckoutStatus1
  :comment T29
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(= T3_has_good Zero)(Guardia2 T3_mid T3_s1 T3_s2 T3_s3 f One Zero)(not (= f NULL))
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val T3_status
 :val T3_med_status 
 :val f
 :val T3_has_bad
 :val actT2 
 :val actT3

 :comment T30
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(= T3_has_good Zero)(Guardia2 T3_mid T3_s1 T3_s2 T3_s3 f One Zero)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val T3_status
 :val T3_med_status 
 :val NULL
 :val T3_has_bad
 :val actT2 
 :val actT3
 
  :comment T_3 UpdateCheckoutStatus2
  :comment T31
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(= T3_has_bad Zero)(Guardia3 T3_mid T3_s1 T3_s2 T3_s3 f One Zero)(not (= f NULL))
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val T3_status
 :val T3_med_status 
 :val T3_has_good
 :val f
 :val actT2 
 :val actT3

  :comment T32
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(= T3_has_bad Zero)(Guardia3 T3_mid T3_s1 T3_s2 T3_s3 f One Zero)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val T3_status
 :val T3_med_status 
 :val T3_has_good
 :val NULL
 :val actT2 
 :val actT3
 
 
   :comment T_3 UpdateCheckoutStatus3
  :comment T33
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status TakingMedicine)(= T3_has_bad Zero)(= T3_has_good One)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T2_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val Paid
 :val T3_med_status 
 :val T3_has_good
 :val T3_has_bad
 :val actT2 
 :val actT3
 
 
    :comment T_3 closing
  :comment T34
 :transition
:var j
:guard  (= actT2 true)(= actT3 true)(= T3_status Paid)
:numcases 1
:case 
 :val Request[j]
 :val AvailableDoctor[j]
 :val Symptons1[j]
 :val Symptons2[j]
 :val Symptons3[j]
 :val Prescription[j]

 :val T1_pid
 :val T1_did
 :val T1_status
 :val T1_pid 
 :val T1_did 
 :val T2_s1 
 :val T2_s2 
 :val T2_s3 
 :val T3_status 
 :val T3_s1 
 :val T3_s2 
 :val T3_s3 
 :val T3_mid
 :val T3_status
 :val T3_med_status 
 :val T3_has_good
 :val T3_has_bad
 :val actT2 
 :val false
 
