Lab test for EECS 4315

Question

Introduce a class, named ExistsNext, that represents the CTL operator ∃ ◯. Its API can be found here. Do not make any changes to the classes provided here. The API and the jar file containing these classes are provided here and here. The snippet 
Formula formula = new ExistsNext(new AtomicProposition("a"));
System.out.println(formula);
produces the output 
EX a

Note that the transitions and the labelling are implemented differently in the TransitionSystem class than in Lab 7 and 8. You are encouraged to study this class and the implementation of the sat methods in the classes in the logic package before attempting the sat method of the ExistsNext class.

Marks

The total of 16 marks is distributed as follows:
fields1 marks
constructor1 marks
equals method1 marks
hashCode method1 mark
toString method1 mark
sat method8 marks
general3 marks

Solution

A solution can be found here.

Tests

Some tests can be found here.