Linear Temporal Logic¶

class iglsynth.logic.ltl.LTL(formula: str, alphabet: Optional[iglsynth.logic.core.Alphabet] = None)[source]¶

Bases: iglsynth.logic.core.PL

Represents an temporal logic formula.

Parameters:	formula – (str) A formula string constructed from Atomic propositions (AP names can be alphanumeric strings that are not “true” or “false” (case insensitive) and do not contain `F, G, M, R, U, V, W, X, xor` as a sub-string. Operators: Negation (!), And(&), Or(\|), Eventually(F), Always(G), Next(X), Until(U). alphabet – (`Alphabet`) A set of atomic propositions.

alphabet¶: Returns the set of atomic propositions (as Alphabet object) over which the logic formula is defined.

evaluate(st, *args, **kwargs)[source]¶: Evaluates the LTL formula over the given state.

Warning

This function is not yet implemented.

formula¶: Returns a string representing the logic formula.

is_contained_in(other)¶

Checks whether language of “self” formula is contained within the language of given formula (other).

Parameters:	other – (`ILogic`) A logic formula.
Returns:	(bool) Whether language of “self” is contained in “other” (True) or not (False).

is_equivalent(other)¶

Checks whether given logic formula accepts the same language as the current (self) formula.

Parameters:	other – (`ILogic`) A logic formula.
Returns:	(bool) Whether self and other accept same language (True) or not (False).

Note

p.is_equivalent(q) is not the same as p == q. The first checks whether the languagesof formulas p and q are equal or not, whereas the latter (p == q) whether p and q are syntactically equivalent or not.

mp_class¶

Returns the class of LTL formula as per Manna-Pnueli hierarchy.

Returns:	(str) A character from {‘B’, ‘S’, ‘G’, ‘O’, ‘R’, ‘P’, ‘T’}.

See also

A discussion on Manna-Pnueli Hierarchy

parse(formula: str)[source]¶: Parses the given formula string to return a simplified parsed string.

simplify()¶: Returns a new logic formula with a simplified formula.

size¶: Reference: https://stackoverflow.com/questions/17920304/what-is-the-size-of-an-ltl-formula

substitute(subs_map: dict)¶

Substitutes the current AP with another AP according to given substitution map.

Parameters:	subs_map – (dict[<Logic>: <Logic>]) A substitution map.
Returns:	(AP) Substituted AP object.
Raises:	KeyError – When subs_map does not contain the AP “self”.

translate()[source]¶: Returns an :class:`Automaton <iglsynth.logic.core.Automaton> object representing an equivalent automaton for the logic formula.

tree¶: Returns the abstract syntax tree (as SyntaxTree object) of the logic formula.