Данный солвер преобразует формулу логики линейного времени в автомат Бюхи. Решение выдается в требуемом для курса формате.

Поддерживаемые операторы приведены в таблице ниже в порядке возрастания приоритета.

Тип	Классическая логика					Операторы логики линейного времени
Оператор	Импликация	Исключающее ИЛИ	Дизъюнкция	Конъюнкция	Отрицание	Next	Future		Globally		Until	Weak until	Release
Запись	->	+	|	&	!	X	F	<>	G	[]	U	W	R

В качестве имени переменной можно использовать любую комбинацию латинских букв и цифр, за исключением букв, обозначающих операторы LTL.

Можно использовать любые скобки в выражении - фигурные, квадратные и круглые. Выражения в скобках вычисляются с наивысшим приоритетом.

Пример формулы: G{q -> (!p & X(!q U p))} или [][q -> [!p & X[!q U p]]].

Формат решения можно настроить с помощью переключателей под полем ввода выражения: Компактный вид таблицы - компактизирует запись множеств истинности; Инвертировать порядок перебора - порядок перебора истинности для атомов будет инвертирован.