// Modify the definition of legal to include allowing the train to stay on the rail it's 
// currently on.  You may also need to modify the connects relation.  It this domain still safe?  
// Demonstrate using the java code.

// Task 5 : 

// There are many possible safe configurations.
// Mine chose a situation where the trains were on rails 1 and 4.  Then, neither moved.

// I modified the connects relation to allow all trains to be connected to themselves.
// First I removed the negation of this relation ( (all r ~connects(r,r)) )from Formula 2.
// Then I added this relation ( (all r connects(r,r)) )to Formula 1.

// 


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

// Formula 2 (Task 1) : expressed in the homework language.
~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)))))) ^


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


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