// Change to layout 2
// Task 10 : 


// 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 2:
  connects(R1, R1)  ^   connects(R1, R2)  ^ (~connects(R1, R3)) ^   connects(R1, R4) ^ 
  connects(R2, R1)  ^   connects(R2, R2)  ^ (~connects(R2, R3)) ^ (~connects(R2, R4)) ^ 
(~connects(R3, R1)) ^   connects(R3, R2)  ^   connects(R3, R3)  ^   connects(R3, R4) ^ 
(~connects(R4, R1)) ^ (~connects(R4, R2)) ^   connects(R4, R3)  ^   connects(R4, R4) ^ 


// 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)
																					  )
																		 )  
												)
											 ) v (
												// all t3 ~on(t3,r2,S1) ^	alldeadlocked(S1) ^ iamit(t1)
												all t3 ((~on(t3,r2,S1)) ^ alldeadlocked(S1) ^ iamit(t1,S1) )
											 )
										  )										 
					 )
)^


(all t1 all t2 ( (iamit(t1,S1)^~iamit(t2,S1)) v (iamit(t2,S1)^~iamit(t1,S1)) v Equals(t1,t2)  ))^

// enforce movement
(all t1 all r1 ( 
			iamit(t1,S1) -> (
				on(t1,r1,S1) -> ~on(t1,r1,S2)
			)
		)
)^


(all t1  ( 
			iamit(t1,S1) -> (
				~iamit(t1,S2)
			)
		)
)^

// extra credit axiom
(all t1  all s1 all s2 ( exists r1   
			(
				on(t1,r1,s1) ^ ~on(t1,r1,s2)
			)
		)
)^

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


//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 r2 PossibleMoves(T1,R2,r2,S1) <->  on(T1,R2,S1) 

	//->(  connects(R1,r2)^~Equals(R1,r2)

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

	//	)

	//)


//)^


//////////////////////////////////////////////////////////////////////////////////



// Another valid definition of deadlock
//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 ( 
//				legal(t1,r1,r2)->Equals(r1,r2)
//			)
//		)
//	) 
//)^

//////////////////////////////////////////////////////////////////////////////////
//deadlock (S1) assertion
(
	// for each
	all t1 all r1 deadlocked(t1,r1,S1) <-> (  
		//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))	
					)
				)	
			)
		)	
	)
)^


//////////////////////////////////////////////////////////////////////////////////
(all t1 all r1 deadlocked(t1,r1,S1))^


(
	alldeadlocked(S1) <-> (
							all t1 all r1 deadlocked(t1,r1,S1)
							)
)^

//////////////////////////////////////////////////////////////////////////////////


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

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

zend