/* 

  Muddle Management problem in Picat.

  From 
  http://logic4fun.rsise.anu.edu.au/demo/example1.html
  """
  Philosophical Railway
  It happened, in the days when trains used to call at the tiny village of 
  Much Tittering in the Woods, that the 1215 once pulled up there and stood 
  for the best part of an hour. Nobody now remembers why. At any rate, the 
  driver, the porter, the signalman, the stationmaster and the guard spent the 
  time in such merry conversation as is customary among employees of railway 
  companies. Their names, in alphabetical order, were 
    James, Kant, Locke, Mill and Nietzsche. 
  For reasons lost in the mists of railway history, they agreed to make two 
  statements each, one true and the other false. They said:

  MILL:         Nietzsche is the stationmaster.
                James is either the guard or the porter.
  LOCKE:        Neither Kant nor Nietzsche is the signalman.
                Mill is not the stationmaster.
  KANT:         Mill's second statement was false.
                Locke's first statement was true.
  NIETZSCHE:    Either James is the porter or I am.
                Neither Locke nor Mill is the guard.
  JAMES:        I am not the signalman.
                Nietzsche's second statement was false.
  
  What was the driver's name? 
  """

  Encoding in Finder:
  http://logic4fun.rsise.anu.edu.au/demo/encoding1.html

  Solution:
  http://logic4fun.rsise.anu.edu.au/cgi/wwfinder/puzzledemo1
  """
  Model 1
  
  philosopher | James     Kant      Locke     Mill      Nietzsche
  ------------+--------------------------------------------------
          job | guard     porter    signalman s'master  driver
  """

  This model:

  [Nietzsche = driver]
  [James = guard]
  [Kant = porter]
  [Locke = signalman]
  [Mill = stationmaster]
  driver = Nietzsche


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.


main => go.

go ?=>
  N = 5,

  Occupation = [Driver, Guard, Porter, Signalman, Stationmaster],
  Occupation = 1..Occupation.len,
  OccupationS = ["driver", "guard", "porter", "signalman", "stationmaster"],

  % decision variables
  Philosophers = [James, Kant, Locke, Mill, Nietzsche],
  Philosophers :: 1..N,
  PhilosophersS = ["James", "Kant", "Locke", "Mill", "Nietzsche"],

  all_different(Philosophers),

  % MILL:         Nietzsche is the stationmaster.
  %               James is either the guard or the porter.
  (Nietzsche #= Stationmaster)
     +
  (James #= Guard #\/ James #= Porter)
    #= 1,

  
  % LOCKE:        Neither Kant nor Nietzsche is the signalman.
  %               Mill is not the stationmaster.
  (Kant #!= Signalman #/\ Nietzsche #!= Signalman)
    +
  (Mill #!= Stationmaster)
    #= 1,
     
  % KANT:         Mill's second statement was false.
  %               Locke's first statement was true.
  #~(James #= Guard #\/ James #= Porter) % Mill's second 
    +
  (Kant #!= Signalman #/\ Nietzsche #!= Signalman) % Locke's first)
    #= 1,
 
  
  % NIETZSCHE:    Either James is the porter or I am.
  %               Neither Locke nor Mill is the guard.
  (James #= Porter #\/ Nietzsche #= Porter)
     +
   (Locke #!= Guard #/\ Mill #!= Guard)
     #= 1,

  % JAMES:        I am not the signalman.
  %               Nietzsche's second statement was false.
  (James #!= Signalman)
     +
  (#~(Locke #!= Guard #/\ Mill #!= Guard))       % Nietzsche's second
     #= 1,

  solve(Philosophers),

  println(Philosophers),
  foreach(I in 1..N)
    nth(P,Philosophers,I),
    println([PhilosophersS[P]=OccupationS[I]])
  end,
  nth(DriverP,Philosophers,Driver),
  println(driver=PhilosophersS[DriverP]),
  fail,
  
  nl.

go => true.