Riverside Murder in the Alloy programming language

riverside_murder.als

// Where to download Alloy: https://alloytools.org/download.html
// Run within Alloy: java -jar org.alloytools.alloy.dist.jar

// The Riverside Diner Murder Mystery
// Recreated from Prolog to Alloy

// Define the people involved in the investigation
abstract sig Person {}

one sig Elena, David, James, Lisa, Tom extends Person {}

// Define the victim (not a suspect)
one sig Marcus extends Person {}

// Evidence predicates
pred missing_knife[p: Person] {
  p in Elena + David
}

pred matching_tires[p: Person] {
  p in James + Lisa + David
}

pred blue_uniform[p: Person] {
  p in Elena + Tom
}

// Additional facts about access and relationships
pred has_access[p: Person] {
  p in Elena + David + James + Lisa + Tom
}

// Evidence about borrowing items (new evidence that breaks the case)
pred borrowed_car[borrower: Person, owner: Person] {
  borrower = David and owner = Elena
}

pred wore_jacket[wearer: Person, owner: Person] {
  wearer = David and owner = Elena
}

pred fingerprints_on_knife[person: Person, knife_owner: Person] {
  person = David and knife_owner = Elena
}

// Derived predicates for actual evidence at scene
pred actual_driver_tires[p: Person] {
  // Either drove own car with matching tires, or borrowed car with matching tires
  (matching_tires[p] and not (some owner: Person | borrowed_car[p, owner])) or
  (some owner: Person | borrowed_car[p, owner] and matching_tires[owner])
}

pred actual_uniform[p: Person] {
  // Either wore own blue uniform, or wore someone else's blue uniform
  (blue_uniform[p] and not (some owner: Person | wore_jacket[p, owner])) or
  (some owner: Person | wore_jacket[p, owner] and blue_uniform[owner])
}

// The murder solution - original version (before new evidence)
pred original_murderer[p: Person] {
  missing_knife[p] and
  matching_tires[p] and
  blue_uniform[p]
}

// The murder solution - updated version (with new evidence)
pred murderer[p: Person] {
  (missing_knife[p] or (some owner: Person | fingerprints_on_knife[p, owner])) and
  actual_driver_tires[p] and
  actual_uniform[p]
}

// Facts to establish (mirrors the Prolog facts)
fact EvidenceFacts {
  // Original evidence
  missing_knife[Elena]
  missing_knife[David]
  
  matching_tires[James]
  matching_tires[Lisa]
  matching_tires[David]
  
  blue_uniform[Elena]
  blue_uniform[Tom]
  
  // New evidence that solves the case
  borrowed_car[David, Elena]
  wore_jacket[David, Elena]
  fingerprints_on_knife[David, Elena]
}

// Constraints
fact Constraints {
  // Everyone has access to the diner
  all p: Person - Marcus | has_access[p]
  
  // Only one murderer
  one p: Person | murderer[p]
}

// Queries (run these to solve the mystery)

// Find who had each type of evidence originally
pred knife_suspects[p: Person] { missing_knife[p] }
pred tire_suspects[p: Person] { matching_tires[p] }
pred uniform_suspects[p: Person] { blue_uniform[p] }

// Find the original solution (should be no one)
pred find_original_murderer {
  some p: Person | original_murderer[p]
}

// Find the final solution (should be David)
pred find_murderer {
  some p: Person | murderer[p]
}

// Show the evidence for each person
pred show_evidence_for[p: Person] {
  p != Marcus // Don't check the victim
}

// Commands to run the analysis
run knife_suspects for 6 Person
run tire_suspects for 6 Person  
run uniform_suspects for 6 Person
run find_original_murderer for 6 Person
run find_murderer for 6 Person
run show_evidence_for for 6 Person

// Check that David is indeed the murderer
assert DavidIsMurderer {
  murderer[David]
}
check DavidIsMurderer for 6 Person

// Check that no one else is the murderer  
assert OnlyDavidIsMurderer {
  all p: Person | murderer[p] implies p = David
}
check OnlyDavidIsMurderer for 6 Person

// Check that the original evidence alone doesn't solve the case
assert OriginalEvidenceInsufficient {
  no p: Person | original_murderer[p]
}
check OriginalEvidenceInsufficient for 6 Person

// Verify the evidence chain for David
pred david_evidence_chain {
  // David had access to Elena's knife (fingerprints)
  fingerprints_on_knife[David, Elena]
  
  // David borrowed Elena's car (which had matching tires)
  borrowed_car[David, Elena] and matching_tires[Elena]
  
  // David wore Elena's blue chef jacket
  wore_jacket[David, Elena] and blue_uniform[Elena]
  
  // Therefore David satisfies all evidence conditions
  murderer[David]
}

run david_evidence_chain for 6 Person

// Summary predicate showing the complete solution
pred complete_solution {
  // Show all the suspects for each piece of evidence
  knife_suspects[Elena] and knife_suspects[David]
  tire_suspects[James] and tire_suspects[Lisa] and tire_suspects[David]  
  uniform_suspects[Elena] and uniform_suspects[Tom]
  
  // Show that original evidence doesn't point to single person
  no p: Person | original_murderer[p]
  
  // Show the new evidence
  borrowed_car[David, Elena]
  wore_jacket[David, Elena] 
  fingerprints_on_knife[David, Elena]
  
  // Show that David is the murderer with new evidence
  murderer[David]
  
  // Show that only David is the murderer
  all p: Person | murderer[p] iff p = David
}

run complete_solution for 6 Person