// Change to layout 2
// Task 8 : 


// I ran Layout 2 with the assertion that there could be a wreck (~safe(S2)).
// It prove that therewould be no wrecks.

// In Task 6, T1 started at R1, T2 started at R3.  They both went to R2 (a  wreck).
// In order to prevent the, we need to check all incoming rails, to each possible destination of each train.

//Layout 1
connects(R1, R2) ^ connects(R2, R3) ^ connects(R3, R4) ^ connects(R4, R1) ^
(all r connects(r,r)) ^
~connects(R1, R3) ^ ~connects(R1, R4) ^ 
~connects(R2, R4) ^ ~connects(R2, R1) ^
~connects(R3, R1) ^ ~connects(R3, R2) ^
~connects(R4, R2) ^ ~connects(R4, R3) ^

// 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)))))) ^


// In Task 6, T1 started at R1, T2 started at R3.  They both went to R2 (a  wreck).
// In order to prevent the, we need to check all incoming rails, to each possible destination of each train.

// A move is legal if 
// there is no train on r2 in situation S1, other than itself.

//(	all t1 all r1 all r2 legal(t1,r1,r2) <-> (~(exists t2 ( on(t2,r2,S1) ^ ~Equals(t1,t2) ) ) ) )^


/////////////////////////////////////////////////////////////////////////////////////////////
// Task 7 : new difinition of legal which outlaws the bad behaviour demonstrated in Task 6.
// The bad behaviour in task 6 was that the trains collided.  
// This happened because the legal rule allowed two trains to move to the same rail,
// since the topology allowed it and we only checked that the rail was empty or this trian was not on it.
/////////////////////////////////////////////////////////////////////////////////////////////
// A move is legal if 
// for a given rail (r2) 
// // redundant because this is a connecting rail also  // there is no train that rail (r2) other than myself and
// there are no train on any of the connecting rails that is not me (t1).
// Note that this rail also connects to this rail, so we do not need a separate pieces saying it 
// is legal to stay put.
/////////////////////////////////////////////////////////////////////////////////////////////
// Previous definition of legal:
//(all t1 all r1 all r2 legal(t1,r1,r2) <-> (~(exists t2 ( on(t2,r2,S1) ^ ~Equals(t1,t2) ) ) ) )^
/////////////////////////////////////////////////////////////////////////////////////////////

/////////////////////////////////////////////////////////////////////////////////////////////
/////////////////////////////////////////////////////////////////////////////////////////////
// New definition of legal:
/////////////////////////////////////////////////////////////////////////////////////////////
// A move is legal iff there are no trains on any of the rails that connect to the destination rails that are not me.
(all t1	all r1 all r2(legal(t1,r1,r2)<->(all r3 connects(r3,r2)->(  ~(exists t2 (on(t2,r3,S1)^~Equals(t1,t2)))  ))))^

//other equivalent version (both work fine and generate the same results)
//equivalent to the above - show the proof in the write-up 
//(all t1	all r1 all r2(legal(t1,r1,r2)<->(all r3 all t2 (connects(r3,r2) ^ on(t2,r3,S1)) -> Equals(t1,t2))))^
/////////////////////////////////////////////////////////////////////


// 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)))  )^

//////////////////////////////////////////////////////////////////////////////////
// Task 8-9: Constrain S1 to be deadlocked.
//////////////////////////////////////////////////////////////////////////////////
// A situation is deadlocked if 
//		for each train, 
//			if that train is on rail 1, then there exists a train on one of the connecting rails that is not itself.
// This shows that a train CAN move.  However, it may not choose to move even if it can move.
//////////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////
// for every train and every considered destination : there is a train on one of the rails that connect to the considered destination that is not me.
//(all s (deadlocked(s)<->(all t1 all r1 all r2 (on(t1,r1,s)^connects(r1,r2)^(~Equals(r1,r2))-> (exists r3 (connects(r3,r2)->(  (exists t2 (on(t2,r3,S1)^~Equals(t1,t2)))  )))))))^

//(	all t1 all r1 all r2 (
//		on(t1,r1,S1)^connects(r1,r2)^(~Equals(r1,r2)-> (
//		exists r3 (connects(r3,r2)->(  (exists t2 (on(t2,r3,S1)^~Equals(t1,t2)))  )))))
//		)
//
//)^


//////////////////////////////////////////////////////////////////////////////////
//deadlock (S1) assertion
(
	// for each
	all t1 all r1 (  
		//if there is a train on r1 at s1 that connects to a different rail, 
		on(t1,r1,S1) ->	(
			all r2 ( 
				(connects(r1,r2)^~Equals(r1,r2)) -> (
					exists t2 exists r3 (
						 (connects(r3,r2)^on(t2,r3,S1)^~Equals(t1,t2))	
					)
				)	
			)
		)	
	)
)^
//////////////////////////////////////////////////////////////////////////////////

//deadlock(S1)^
///////////////////////////////////////////////////////////////////////////////////////////////////////

// Assertion 1 (Task 5 no wrecks) : There is a possible train wreck.
//~safe(S2)^

zend