TLA+ asks:
What sequences of states are possible?

Alloy asks:
What structures are possible under these constraints?
Can you show me an instance?
Can you show me a counterexample?

case punya dua owner aktif
appeal dibuat untuk order yang tidak appealable
user approve case milik team sendiri padahal conflict-of-interest dilarang
task masih open setelah case closed
policy rule overlap dan menghasilkan dua outcome
evidence attached ke entity yang tidak boleh menerima evidence
assignment graph punya cycle
delegation memberi privilege lebih luas dari delegator

Apakah kombinasi entity ini mungkin?
Apakah constraint ini cukup untuk mencegah state ilegal?
Apakah ada contoh valid untuk rule ini?
Apakah assertion ini selalu benar di semua model kecil?
Apakah ada conflict antar rule?
Apakah relationship ini bisa membentuk cycle?
Apakah cardinality kita benar?

domain model
authorization model
role/permission relation
ownership and assignment
approval and delegation
policy matrix
schema cardinality
configuration consistency
state classification
constraint-heavy workflows

low-level Java performance
JVM memory model
long-running liveness
queue retry timing
throughput analysis

signatures: sets of atoms/entities
fields: relations between signatures
facts: constraints that always hold
predicates: named reusable constraints/scenarios
assertions: claims to be checked
commands: run/check with finite scope

sig User {}
sig Team {}

sig Case {
  owner: one Team,
  assignee: lone User
}

User = set of user atoms
Team = set of team atoms
Case = set of case atoms
owner: setiap Case punya tepat satu Team
assignee: setiap Case punya nol atau satu User

assert EveryOpenCaseHasOwner {
  all c: Case | c.status = Open implies one c.owner
}

check EveryOpenCaseHasOwner for 5

Counterexample kecil sering langsung menjadi fixture test.

Case
Party
Officer
Team
Assignment
Task
Evidence
Decision
Appeal

1. Open case must have exactly one owning team.
2. Open case may have one active assignee.
3. Closed case must not have open tasks.
4. Evidence must belong to exactly one case.
5. Officer cannot approve a case if they are conflicted with any party.
6. Appeal can only exist for decided case.
7. Appeal reviewer must not be the original decision maker.
8. Active assignment must belong to owning team.
9. Team hierarchy must be acyclic.
10. Delegation must not grant permission outside delegator's scope.

abstract sig CaseStatus {}
one sig Draft, Open, Decided, Closed extends CaseStatus {}

sig Team {
  parent: lone Team
}

sig Officer {
  memberOf: some Team,
  conflictedWith: set Party
}

sig Party {}

sig Case {
  status: one CaseStatus,
  owner: lone Team,
  assignee: lone Officer,
  parties: set Party,
  tasks: set Task,
  evidence: set Evidence,
  decision: lone Decision,
  appeal: lone Appeal
}

abstract sig TaskStatus {}
one sig TaskOpen, TaskDone extends TaskStatus {}

sig Task {
  taskStatus: one TaskStatus
}

sig Evidence {}

sig Decision {
  decidedBy: one Officer
}

sig Appeal {
  reviewer: one Officer
}

fact OpenCaseOwnership {
  all c: Case |
    c.status = Open implies one c.owner
}

fact NonDraftCaseHasOwner {
  all c: Case |
    c.status != Draft implies one c.owner
}

fact ClosedCaseHasNoOpenTasks {
  all c: Case |
    c.status = Closed implies no t: c.tasks | t.taskStatus = TaskOpen
}

fact EvidenceBelongsToAtMostOneCase {
  all e: Evidence |
    lone c: Case | e in c.evidence
}

fact EvidenceBelongsToExactlyOneCase {
  all e: Evidence |
    one c: Case | e in c.evidence
}

assert NoClosedCaseWithOpenTask {
  no c: Case | c.status = Closed and some t: c.tasks | t.taskStatus = TaskOpen
}

check NoClosedCaseWithOpenTask for 5

assert ClosedCaseCannotHaveAppealWithOpenTask {
  no c: Case |
    c.status = Closed and
    some c.appeal and
    some t: c.tasks | t.taskStatus = TaskOpen
}

pred DecidedCaseWithAppeal {
  some c: Case |
    c.status = Decided and
    some c.decision and
    some c.appeal
}

run DecidedCaseWithAppeal for 5

Bukan hanya “tidak ada counterexample”.
Kita juga perlu memastikan valid scenario masih mungkin.

For every important forbidden state, write check.
For every important valid state, write run.

Active assignee must be member of owning team.

fact AssigneeBelongsToOwnerTeam {
  all c: Case |
    some c.assignee implies c.owner in c.assignee.memberOf
}

fun ancestors[t: Team]: set Team {
  t.^parent
}

fun teamScope[t: Team]: set Team {
  t + t.~parent
}

fun descendants[t: Team]: set Team {
  t.^~parent
}

fun ownerScope[t: Team]: set Team {
  t + descendants[t]
}

fact AssigneeInOwnerScope {
  all c: Case |
    some c.assignee implies some (c.assignee.memberOf & ownerScope[c.owner])
}

fact TeamHierarchyAcyclic {
  no t: Team | t in t.^parent
}

Relational DB foreign key alone does not prevent hierarchy cycles.
Need recursive constraint, application check, closure table rule, trigger, or materialized path validation.

TeamA.parent = TeamB
TeamB.parent = TeamA

@Test
void teamHierarchyRejectsCycle() {
    TeamId a = teams.create("A");
    TeamId b = teams.create("B");

    teams.setParent(b, a);

    assertThatThrownBy(() -> teams.setParent(a, b))
        .isInstanceOf(HierarchyCycleException.class);
}

Officer cannot decide case if officer is conflicted with any party in that case.

fact NoConflictedDecisionMaker {
  all c: Case |
    some c.decision implies
      no (c.decision.decidedBy.conflictedWith & c.parties)
}

Appeal reviewer must not be original decision maker.
Appeal reviewer must not be conflicted with case parties.

fact AppealReviewerIndependent {
  all c: Case |
    some c.appeal implies {
      some c.decision
      c.appeal.reviewer != c.decision.decidedBy
      no (c.appeal.reviewer.conflictedWith & c.parties)
    }
}

same reviewer as decision maker
reviewer in same team
reviewer conflicted with one of multiple parties
case has no decision but appeal exists
appeal exists after closed state

Appeal can only exist for decided or closed-with-decision case.

fact AppealRequiresDecision {
  all c: Case |
    some c.appeal implies some c.decision
}

fact AppealOnlyForDecidedOrClosedCase {
  all c: Case |
    some c.appeal implies c.status in Decided + Closed
}

Closed case can have appeal, but closed case has no open tasks.
If appeal requires review task, then closed appeal may be impossible.

pred ClosedCaseWithAppeal {
  some c: Case | c.status = Closed and some c.appeal
}

run ClosedCaseWithAppeal for 5

Is this intended?
If yes, rule should say appeal cannot exist after closure.
If no, closed appeal should have no open task or closure semantics are wrong.

Officer can delegate permission to another officer.
Delegate must not gain permission outside delegator's scope.
Delegation graph must be acyclic or explicitly bounded.
Delegation expires or can be revoked.

abstract sig Permission {}
one sig ViewCase, DecideCase, ReassignCase extends Permission {}

sig Delegation {
  from: one Officer,
  to: one Officer,
  permission: some Permission,
  scope: some Team
}

fact NoSelfDelegation {
  no d: Delegation | d.from = d.to
}

fun delegatesTo: Officer -> Officer {
  Delegation.from -> Delegation.to
}

fact DelegationAcyclic {
  no o: Officer | o in o.^delegatesTo
}

fun officerBaseScope[o: Officer]: set Team {
  o.memberOf + o.memberOf.^~parent
}

fact DelegationWithinDelegatorScope {
  all d: Delegation |
    d.scope in officerBaseScope[d.from]
}

Officer in Team A delegates DecideCase on Team B.

Case priority depends on category, risk, and party type.
Exactly one policy rule should match any case.

abstract sig Risk {}
one sig Low, Medium, High extends Risk {}

abstract sig Category {}
one sig Fraud, Safety, Licensing extends Category {}

sig PolicyRule {
  risk: set Risk,
  category: set Category,
  output: one Priority
}

abstract sig Priority {}
one sig Normal, Urgent, Critical extends Priority {}

pred overlaps[r1, r2: PolicyRule] {
  r1 != r2
  some (r1.risk & r2.risk)
  some (r1.category & r2.category)
}

assert NoPolicyOverlap {
  no r1, r2: PolicyRule | overlaps[r1, r2]
}

check NoPolicyOverlap for 6

assert EveryCombinationCovered {
  all r: Risk, c: Category |
    one pr: PolicyRule | r in pr.risk and c in pr.category
}

policy configuration validation at startup
admin UI validation before activation
migration check before deployment
property-based test generating category/risk combinations

class CaseRecord {
    UUID ownerTeamId;       // nullable? unknown
    UUID assigneeUserId;    // nullable? unknown
    String status;          // invalid values possible
}

record CaseRecord(
    CaseId id,
    CaseStatus status,
    Optional<TeamId> ownerTeamId,
    Optional<OfficerId> assigneeId
) {}

status != DRAFT implies owner exists
closed implies no open tasks
assignee belongs to owner scope

domain service validation
database constraints
foreign keys
unique indexes
transactional checks
policy engine validation
property tests
startup config validation

CREATE UNIQUE INDEX ux_active_assignment_per_case
ON case_assignment(case_id)
WHERE active = true;

assert AtMostOneActiveAssignmentPerCase {
  all c: Case |
    lone a: Assignment | a.case = c and a.active = True
}

@Test
void caseCannotHaveTwoActiveAssignments() {
    CaseId caseId = fixtures.openCase();
    assignments.assign(caseId, officerA);

    assertThatThrownBy(() -> assignments.assign(caseId, officerB))
        .isInstanceOf(DuplicateActiveAssignmentException.class);
}

check NoPolicyOverlap for 5

2 teams can reveal cycle
2 officers can reveal conflict
2 policy rules can reveal overlap
3 nodes can reveal hierarchy issue

check DelegationAcyclic for 3 Officer, 3 Delegation

Risk = Low, Medium, High
AmountBand = Small, Large
AgeBand = Fresh, Stale, Expired

amount > 1000000
now - createdAt > 30 days

you have mostly relational constraints,
but need a few temporal transitions.

behavior/interleaving/fairness/retry is central.

If the hard part is “what structures are legal?” -> Alloy.
If the hard part is “what can happen over time?” -> TLA+.
If both are hard, use Alloy first for structural constraints, then TLA+ for protocol behavior.

pred ValidOpenAssignedCase {
  some c: Case |
    c.status = Open and
    one c.owner and
    one c.assignee
}

run ValidOpenAssignedCase for 5

pred ValidAppealedDecision {
  some c: Case |
    c.status = Decided and
    some c.decision and
    some c.appeal
}

run ValidAppealedDecision for 5

Never trust checks until you have run representative valid scenarios.

Case0.status = Decided
Case0.decision.decidedBy = Officer0
Case0.appeal.reviewer = Officer0

Appeal reviewer is original decision maker.

@Test
void appealReviewerCannotBeOriginalDecisionMaker() {
    OfficerId officer = fixtures.officer();
    CaseId caseId = fixtures.decidedCase(decidedBy(officer));

    assertThatThrownBy(() -> appeals.assignReviewer(caseId, officer))
        .isInstanceOf(ConflictOfInterestException.class)
        .hasMessageContaining("original decision maker");
}

@Test
void assignAppealReviewerReturnsConflictForOriginalDecisionMaker() {
    given()
        .contentType(JSON)
        .body(assignReviewerPayload(originalDecisionMakerId))
    .when()
        .post("/cases/{id}/appeal/reviewer", caseId)
    .then()
        .statusCode(409)
        .body("code", equalTo("APPEAL_REVIEWER_NOT_INDEPENDENT"));
}

-- not always expressible as simple check constraint if it crosses tables
-- enforce in domain service transaction and audit rejected attempt

appeal.reviewer_assignment_rejected.conflict.count

1. What are the core signatures?
2. What relations carry ownership, permission, or lifecycle meaning?
3. What states are forbidden?
4. What valid examples must exist?
5. What assertions were checked?
6. What counterexamples changed the design?
7. Which constraints map to DB/API/domain code/tests?

formal/
  alloy/
    case-domain/
      case-domain.als
      README.md
      counterexamples/
        duplicate-active-assignment.md
        conflicted-appeal-reviewer.md
    authorization/
      delegation.als
    policy/
      priority-policy.als

# Model Purpose

# Domain Scope

# Out of Scope

# Important Signatures

# Facts

# Assertions

# Run Scenarios

# Counterexamples Found

# Mapping to Java/DB/API Tests

Model shape:
[ ] Are signatures minimal and domain-named?
[ ] Are relations explicit instead of hidden in comments?
[ ] Are cardinalities intentional?
[ ] Are facts not overconstraining the model?

Validation:
[ ] Are valid scenarios tested with run?
[ ] Are forbidden states tested with check?
[ ] Are scopes selected intentionally?
[ ] Are integer/ordering assumptions explicit?

Domain correctness:
[ ] Ownership constraints are represented.
[ ] Terminal-state constraints are represented.
[ ] Authorization/delegation constraints are represented.
[ ] Conflict-of-interest constraints are represented.
[ ] Cross-entity invariants are represented.

Engineering mapping:
[ ] Each important fact maps to DB constraint, domain code, API contract, or config validation.
[ ] Each important counterexample maps to a Java regression test.
[ ] Each rejected business operation has a clear error contract.

Domain:
- User belongs to groups.
- Group has permissions over resources.
- Resource belongs to tenant.
- User may be delegated permission by another user.
- Delegation cannot cross tenant.
- Admin can revoke delegation.

Find:
1. A valid delegated access example.
2. A counterexample where delegation crosses tenant.
3. A counterexample where delegation cycle exists.
4. An assertion that effective permission never exceeds source permission.
5. A Java test for the smallest counterexample.

not “I wrote Alloy syntax”
but “I discovered this missing tenant boundary constraint”

ownership
assignment
authorization
delegation
approval independence
policy overlap
schema cardinality
hierarchy acyclicity
cross-entity invariants

define signatures
add minimal facts
run valid scenarios
check forbidden assertions
inspect counterexamples
map findings to Java/DB/API/tests
keep model with design docs