Logic Module¶

Global Variables¶

iglsynth.logic.core.TRUE = AP(name=true)¶

iglsynth.logic.core.FALSE = AP(name=false)¶

ILogic (Interface Class)¶

class iglsynth.logic.core.ILogic[source]¶

Bases: abc.ABC

ILogic is an interface class to represent logic classes in IGLSynth. All logic classes must implement the methods of this class.

Caution

DO NOT INSTANTIATE THIS CLASS!

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

formula¶: Returns a string representing the logic formula.

is_contained_in(other)[source]¶

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)[source]¶

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.

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

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

size¶: Returns the size of formula.

substitute(subs_map: dict)[source]¶: Returns a new logic formula with substituted formulas.

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.

SyntaxTree¶

class iglsynth.logic.core.SyntaxTree[source]¶

Bases: iglsynth.util.graph.Graph

Represents an Abstract Syntax Tree of a ILogic formula.

class Vertex(spot_formula)[source]¶

Bases: iglsynth.util.graph.Vertex

Represents a vertex of a SyntaxTree.

A vertex of syntax tree stores two key pieces of information.

A sub-formula string, which is represented by the sub-tree by considering the vertex as the root.
The kind (operator) represented by the vertex.

Parameters:	spot_formula – (spot.formula) The formula represented by the sub-tree with the vertex as the root.

formula¶: Returns the formula string represented by the sub-tree with vertex as root.

operator¶: Returns the operator represented by the sub-tree with vertex as root.

build_from_spot_formula(spot_formula)[source]¶

Constructs a syntax tree from a given spot formula.

Parameters:	spot_formula – (`spot.formula`)
Returns:	None

root¶: Returns the root of SyntaxTree as a SyntaxTree.Vertex.

Atomic Propositions¶

class iglsynth.logic.core.AP(formula: str, eval_func: Callable = None)[source]¶

Bases: iglsynth.logic.core.ILogic

Represents an atomic proposition.

Parameters:

formula – (str) The name of atomic proposition. Acceptable strings are alphanumeric strings that are not “true” or “false” (case insensitive) and do not contain ‘F’, ‘G’, ‘M’, ‘R’, ‘U’, ‘V’, ‘W’, ‘X’, ‘xor’.
eval_func –
(function) A function that evaluates whether the AP is true or false in a given state. The acceptable function templates are
- res <- eval_func(st)
- res <- eval_func(st, *args)
- res <- eval_func(st, *kwargs)
- res <- eval_func(st, *args, **kwargs)
where res must be a boolean.

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

evaluate(st, *args, **kwargs)[source]¶

Evaluates the AP over the given state.

Parameters:	st – (pyobject) An object representing state. It is user’s duty to ensure the implementation of given `eval_func` consumes the given state object correctly.
Returns:	(bool) If AP is evaluated to be True/False over given state.
Raises:	ValueError – When result of evaluation is not a boolean.

formula¶: Returns a string representing the logic formula.

is_contained_in(other)[source]¶

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)[source]¶

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.

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

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

size¶: Returns the size of formula.

substitute(subs_map: dict)[source]¶

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.

Alphabet¶

class iglsynth.logic.core.Alphabet(props=())[source]¶

Bases: set

add(p: iglsynth.logic.core.AP)[source]¶

Add an element to a set.

This has no effect if the element is already present.

clear()¶: Remove all elements from this set.

copy()¶: Return a shallow copy of a set.

difference()¶

Return the difference of two or more sets as a new set.

(i.e. all elements that are in this set but not the others.)

difference_update()¶: Remove all elements of another set from this set.

discard()¶

Remove an element from a set if it is a member.

If the element is not a member, do nothing.

evaluate(st, *args, **kwargs)[source]¶

Evaluates the alphabet over the given state.

Parameters:	st – (pyobject) An object representing state. It is user’s duty to ensure the implementation of given `eval_func` consumes the given state object correctly.
Returns:	(dict(key=AP, value=bool)) A mapping of atomic proposition with it’s evaluation at the given state.
Raises:	ValueError – When result of evaluation is not a boolean.

intersection()¶

Return the intersection of two sets as a new set.

(i.e. all elements that are in both sets.)

intersection_update()¶: Update a set with the intersection of itself and another.

isdisjoint()¶: Return True if two sets have a null intersection.

issubset()¶: Report whether another set contains this set.

issuperset()¶: Report whether this set contains another set.

pop()¶: Remove and return an arbitrary set element. Raises KeyError if the set is empty.

remove()¶

Remove an element from a set; it must be a member.

If the element is not a member, raise a KeyError.

symmetric_difference()¶

Return the symmetric difference of two sets as a new set.

(i.e. all elements that are in exactly one of the sets.)

symmetric_difference_update()¶: Update a set with the symmetric difference of itself and another.

union()¶

Return the union of sets as a new set.

(i.e. all elements that are in either set.)

update()¶: Update a set with the union of itself and others.

Propositional Logic Formulas¶

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

Bases: iglsynth.logic.core.AP

Represents an propositional 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(\|) 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 PL formula over the given state.

Parameters:	st – (pyobject) An object representing state. It is user’s duty to ensure the implementation of given `eval_func` consumes the given state object correctly.
Returns:	(bool) If PL formula is evaluated to be `True` or `False` over given state.
Raises:	ValueError – When result of evaluation is not a boolean.

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.

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

simplify()[source]¶: 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)[source]¶

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()¶: 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.