LTL formula → Büchi automaton

Applied Logic. The final assignment - Question 3.

Notice: All calculation will be done on your computer.

Enter your LTL formula here:

You can use the following syntax:

The constant true and false.
A word in lowercase alphabets for a proposition.
NOT, ~ for the NOT operator
AND, /\ for the AND operator
OR, \/ for the OR operator
-> for the IMPLIES operator
X, F, G, U, R for corresponding operators.