

:comment documentazione dell'esempio


:index int



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

:smt (define-type Case) 
:smt (define-type Claim) 
:smt (define-type Cust)
:smt (define-type Num)
:smt (define-type String)


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




:smt (define CaseCust ::(-> Case Cust))
:smt (define CaseType ::(-> Case String))
:smt (define CaseEstimate ::(-> Case Num))
:smt (define CaseDeduct ::(-> Case Num))
:smt (define CustName ::(-> Cust String))
:smt (define CustAddr ::(-> Cust String))
:smt (define CustInj ::(-> Cust String))
:smt (define ClaimAmount ::(-> Claim Num))
:smt (define ClaimState ::(-> Claim String))
:smt (define ClaimCaseId ::(-> Claim Case))



:smt (define NewCase ::String)
:smt (define CaseEnded ::String)
:smt (define ExccedDeductible ::String)
:smt (define NotExccedDeductible ::String)
:smt (define RepairPerformed ::String)
:smt (define Paid ::String)
:smt (define Approved ::String)


:db_driven 
:db_sorts Case Claim Cust Num String 
:db_functions CaseCust CaseType CaseEstimate CaseDeduct CustName 
:db_functions CustAddr CustInj ClaimAmount ClaimState ClaimCaseId 
:db_constants  NewCase CaseEnded ExccedDeductible NotExccedDeductible  RepairPerformed  Paid  Approved 
:db_relations 


:local Cases1 Case
:local Cases2 String


:global T1_case_id Case
:global T1_status String
:global T2_case_id Case
:global T2_status String
:global T2_repair_loc String
:global T3_case_id Case
:global T3_status String
:global actT2 bool
:global actT3 bool




:initial
:var x
:cnj (=  T1_case_id  NULL_Case) (=  T1_status NULL_String) (=  T2_case_id  NULL_Case) (=  T2_status  NULL_String) (=  T2_repair_loc NULL_String) (=  T3_case_id NULL_Case) (= T3_status NULL_String) (= Cases1[x] NULL_Case)(= Cases2[x] NULL_String) (=  actT2 false)(= actT3 false)

:u_cnj (= T1_status CaseEnded)(not (= T2_repair_loc NULL_String))(not (= T3_status NULL_String))

:eevar e Case
:eevar f String

:comment T_1: Main

:comment T_1 Init

:comment T1
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= T1_status NULL_String)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val e
 :val NewCase
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3 

 :comment T_1 StoreCase
 :comment T2
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_status NULL_String))(= Cases1[x] NULL_Case)(= Cases2[x] NULL_String) 
:uguard (not (= Cases1[j] T1_case_id))(not (= Cases2[j] T1_status))
:numcases 2
:case (= x j)
 :val T1_case_id
 :val T1_status

 :val e
 :val NULL_String
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3 
 
:case
 :val Cases1[j] 
 :val Cases2[j]
 
 :val e
 :val NULL_String
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3

 :comment T3
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(not (= T1_status NULL_String))(= Cases1[x] NULL_Case)(= Cases2[x] NULL_String) 
:uguard (not (= Cases1[j] T1_case_id))(not (= Cases2[j] T1_status))
:numcases 2
:case (= x j)
 :val T1_case_id
 :val T1_status

 :val NULL_Case
 :val NULL_String
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3 
 
:case
 :val Cases1[j] 
 :val Cases2[j]
 
 :val NULL_Case
 :val NULL_String
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3
 
  :comment T_1 RetrieveCase
 :comment T4
:transition
:var x
:var j
:guard  (= actT2 false)(= actT3 false)(= T1_status NULL_String) (not (= Cases1[x] NULL_Case)) (not (= Cases2[x] NULL_String))(not (= Cases2[x] CaseEnded))
:numcases 2
:case (= x j)
 :val NULL_Case
 :val NULL_String

 :val Cases1[x]
 :val Cases2[x]
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3 
 
:case
 :val Cases1[j] 
 :val Cases2[j]
 
 :val Cases1[x]
 :val Cases2[x]
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3
 
 
 
:comment T_2: NotExccedDeductible


:comment T_2 opening
:comment T5
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= T1_status NewCase)(= (CaseType T1_case_id) NotExccedDeductible)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T1_case_id
 :val NULL_String
 :val NULL_String
 :val T3_case_id 
 :val T3_status
 :val true
 :val actT3
 
 
 
:comment T_2 SuggestRepairLocations
:comment T6
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status NULL_String)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val f
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3
	
	
:comment T_2 RepairerNotify
:comment T7
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status NULL_String)(not (= T2_repair_loc NULL_String))
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val CaseEnded 
 :val T2_repair_loc
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3
 
 :comment T_2 PerformRepair
:comment T8
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status NULL_String)(not (= T2_repair_loc NULL_String))
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val CaseEnded 
 :val T2_repair_loc
 :val T3_case_id 
 :val T3_status
 :val actT2 
 :val actT3
	
:comment T_2 closing
:comment T9
:transition
:var j
:guard  (= actT2 true)(= actT3 false)(= T2_status CaseEnded)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T2_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val false
 :val actT3

 
 :comment T_3: ExccedDeductible
 
 :comment T_3 opening
:comment T10
:transition
:var j
:guard  (= actT2 false)(= actT3 false)(= T1_status NewCase)(= (CaseType T1_case_id) ExccedDeductible)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T1_case_id 
 :val NULL_String
 :val actT2
 :val true
 
:comment T_3 Unrecoverable
:comment T11
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= T3_status NULL_String)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val CaseEnded
 :val actT2
 :val actT3
 
 :comment T_3 CustomerPays
:comment T12
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= T3_status RepairPerformed)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val Paid
 :val actT2
 :val actT3
 
  :comment T_3 AdjustApproves
:comment T13
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= T3_status Paid)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val Approved
 :val actT2
 :val actT3

   :comment T_3 RepairComplete
:comment T14
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= T3_status Approved)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T1_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val CaseEnded
 :val actT2
 :val actT3
 
 :comment T_3 RepairComplete
:comment T15
:transition
:var j
:guard  (= actT2 false)(= actT3 true)(= T3_status CaseEnded)
:numcases 1
:case 
 :val Cases1[j]
 :val Cases2[j]

 :val T1_case_id
 :val T3_status
 :val T2_case_id
 :val T2_status 
 :val T2_repair_loc 
 :val T3_case_id 
 :val T3_status
 :val actT2
 :val false

 
