// Find a satisfying assignment.
// Where is S1 and S2?
// Task 3 : 



// Formula 1 (Task 1) : expressed in the homework language.
// positive connections
connects(R1, R2) ^ connects(R2, R3) ^ connects(R3, R4) ^ connects(R4, R1) ^

// Formula 2 (Task 1) : expressed in the homework language.
// negative connections
~connects(R1, R3) ^ ~connects(R1, R4) ^ 
~connects(R2, R4) ^ ~connects(R2, R1) ^
~connects(R3, R1) ^ ~connects(R3, R2) ^
~connects(R4, R2) ^ ~connects(R4, R3) ^
~(all r connects(r,r)) ^


// Formula 3 (Task 1) : expressed in the homework language.
// A situation is safe iff no 2 trains occupy the same rail.
(all s safe(s) <-> (all r all t1 all t2	(on(t1,r,s) ^ on(t2,r,s) -> Equals(t1,t2))  )   )	 ^


// Formula 4 (Task 1) : expressed in the homework language.
(safe(S1)) ^


// Formula 5 (Task 1) : expressed in the homework language.
// Dynamics.
// Only move to connected rails.
(all t all r2 (on(t,r2,S2) ->	exists r1 (on(t,r1,S1) ^ connects(r1,r2) ^ legal(t,r1,r2)))) ^    

// Formula 6 (Task 1) : Definition of legal.
// A move is legal means that it is OK for t1 to move from r1 to r2.
// A move is legal if there is no train on r2 in situation S1.
(all t1 all r1 all r2	(legal(t1,r1,r2) <-> ( ~(exists t2 (on(t2,r2,S1)))))) ^

// Axiom 1 (Task 2) :  Every train is always on some rail.
(all t all s exists r on(t,r,s))  ^

// Axiom 2 (Task 2) :  No train is on two rails at the same time.
all t all s all r1 (on(t,r1,s) -> (all r2 (on(t,r2,s) -> Equals(r1,r2)))  )^

// Assertion 1 (Task 4) : There is a possible train wreck.
//~safe(S2)

zend