Lab test for EECS 4315
Question
Introduce a class, named ExistsEventually, 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 ExistsEventually(new AtomicProposition("a"));
System.out.println(formula);
produces the output
EF a
Marks
The total of 16 marks is distributed as follows:
| fields | 1 marks |
| constructor | 1 marks |
| equals method | 1 marks |
| hashCode method | 1 mark |
| toString method | 1 mark |
| sat method | 8 marks |
| general | 3 marks |
Solution
A solution can be found here.
Tests
Some tests can be found here.