@startuml
skinparam classAttributeIconSize 0
skinparam noteBackgroundColor #FFF9C4

class BankAccount {
  - accountNumber: String
  - balance: Real
  - isOverdraftEnabled: Boolean
  + withdraw(amount: Real)
  + deposit(amount: Real)
}

note right of BankAccount
  **क्लास अनिवार्यताएँ:**
  context BankAccount
  
  -- बैलेंस कभी भी ऋणात्मक नहीं हो सकता जब तक कि ओवरड्राफ्ट सक्षम न हो
  inv balanceRule: 
    self.balance >= 0 या self.isOverdraftEnabled
  
  -- ओवरड्राफ्ट सीमा 500 से अधिक नहीं हो सकती
  inv overdraftLimit: 
    self.isOverdraftEnabled implies self.balance >= -500
end note
@enduml

@startuml
skinparam classAttributeIconSize 0
skinparam noteBackgroundColor #E8F5E9

class ShoppingCart {
  - items: Bag<Product>
  - totalAmount: Real
  + checkout(): Receipt
  + getTotal(): Real
}

note right of ShoppingCart
  **ऑपरेशन कॉन्ट्रैक्ट्स:**
  
  -- प्री-शर्त: कार्ट खाली नहीं होना चाहिए
  context ShoppingCart::checkout(): Receipt
  pre: self.items->notEmpty()
  
  -- पोस्ट-शर्त: कार्ट खाली कर दिया गया, रसीद उत्पन्न की गई
  post: self.items->isEmpty() and result <> null
  
  -- बॉडी: क्वेरी ऑपरेशन परिभाषा
  context ShoppingCart::getTotal(): Real
  body: self.items->collect(price)->sum()
end note
@enduml

@startuml
skinparam classAttributeIconSize 0
skinparam noteBackgroundColor #E3F2FD

class Employee {
  - firstName: String
  - birthDate: Date
  - {derived} age: Integer
  - {initial} isActive: Boolean = true
}

note right of Employee
  **व्युत्पन्न और प्रारंभिक मान:**
  
  -- उ возраст की गणना स्वचालित रूप से करें
  context Employee::age: Integer
  derive: self.birthDate.yearsSinceToday()
  
  -- निर्माण के समय प्रारंभिक अवस्था
  context Employee::isActive: Boolean
  init: true
end note
@enduml

@startuml
skinparam stateBackgroundColor #F3E5F5

[*] --> Created
Created --> PendingApproval : submit()

state PendingApproval {
}

PendingApproval --> Approved : [total < 10000]
PendingApproval --> Rejected : [total >= 10000]

Approved --> Shipped : ship()
Shipped --> [*]

note right of PendingApproval
  **राज्य अविनाशीता:**
  context Order
  inv: self.status = 'Pending' implies 
       self.submittedBy->notEmpty()
end note

note right of Approved
  **approve() की पश्च-शर्त:**
  context Order::approve()
  post: self.status = 'Approved' and 
        self.approvedDate <> null
end note
@enduml

@startuml
skinparam classAttributeIconSize 0
skinparam noteBackgroundColor #FFFDE7
skinparam noteBorderColor #FBC02D

class Employee {
  - SSN: String
  - firstName: String
  - birthDate: Date
  - hireDate: Date
  - salary: Float
  + age(): Integer
}

class Department {
  - number: Integer
  - name: String
  - locations: Set<String>
  - {derived} nbrEmployees: Integer
}

class Project {
  - number: Integer
  - name: String
  - location: String
}

Employee "0..*" -- "1" Department : worksFor > department
Employee "0..*" -- "0..*" Project : worksOn > project
Employee "1" -- "0..1" Department : manages > managedDept
Department "1" -- "0..*" Project : controls > projects
Employee "1" -- "0..*" Employee : supervisor > subordinates

note right of Employee
  **जटिल अविनाशीता और नेविगेशन:**
  context Employee
  
  -- 1. मूल गुण नियम
  inv ageCheck: self.age() >= 18
  
  -- 2. संबंधों का नेविगेशन (बहुलता)
  inv maxProjects: self.worksOn->size() <= 4
  
  -- 3. इटरेटर्स का उपयोग (forAll)
  -- प्रबंधक को अधीनस्थों से पहले नियुक्त किया जाना चाहिए
  inv hireOrder: self.subordinates->forAll(
    sub | sub.hireDate > self.hireDate
  )
  
  -- 4. क्रॉस-संबंध नियम
  -- कर्मचारी केवल उन प्रोजेक्ट्स पर काम कर सकता है जिन पर उनके विभाग का नियंत्रण हो
  inv projectControl: 
    self.worksFor.controls->includesAll(self.worksOn)
    
  -- 5. अद्वितीय पहचानकर्ता (की)
  inv uniqueSSN: Employee.allInstances()->forAll(e1, e2 | 
    e1 <> e2 implies e1.SSN <> e2.SSN
  )
end note

note bottom of Department
  **व्युत्पन्न गुण:**
  context Department::nbrEmployees: Integer
  derive: self.worksFor->size()
end note

note right of Project
  **प्रोजेक्ट अविनाशीता:**
  context Project
  
  -- प्रोजेक्ट स्थान विभाग के स्थानों में से एक होना चाहिए
  inv validLocation: 
    self.controls.locations->includes(self.location)
end note

@enduml

@startuml
skinparam classAttributeIconSize 0

class Employee {
  - worksOn: Set<Project>
}

note right of Employee
  **जटिल तर्क के लिए 'let' का उपयोग:**
  context Employee
  
  -- कुल घंटे की गणना करें और सीमाओं की जांच करें
  inv workingHours: 
    let totalHours: Integer = 
      self.worksOn->collect(hours)->sum() 
    in totalHours >= 30 और totalHours <= 50
end note
@enduml

@startuml
skinparam classAttributeIconSize 0

class Company {
  - employees: Set<Employee>
  + hireEmployee(p: Employee)
}

note right of Company
  **पोस्ट-शर्तों में @pre का उपयोग:**
  context Company::hireEmployee(p: Employee)
  
  -- नए कर्मचारी सेट पुराने सेट + नए व्यक्ति है
  post: self.employees = self.employees@pre->including(p)
end note
@enduml