tulip :: spec :: form :: LTL :: Class LTL

Class LTL

LTL formula (specification)

Minimal class that describes an LTL formula in the canonical TuLiP syntax. It contains three attributes:

formula: a str of the formula. Syntax is only enforced if the user requests it, e.g., using the check_form method.
input_variables: a dict of variables (names given as strings) and their domains; each key is a variable name and its value (in the dictionary) is its domain. See notes below. Semantically, these variables are considered to be inputs (i.e., uncontrolled, externally determined).
output_variables: similar to input_variables, but considered to be outputs, i.e., controlled, the strategy for setting of which we seek in formal synthesis.

N.B., domains are specified in multiple datatypes. The type is indicated below in parenthesis. Recognized domains, along with examples, are:

boolean (str); this domain is specified by "boolean";
finite_set (set); e.g., {1,3,5};
range (tuple of length 2); e.g., (0,15).

As with the formula attribute, type-checking is only performed if requested by the user. E.g., any iterable can act as a finite_set. However, a range domain must be a tuple of length 2; otherwise it is ambiguous with finite_set.

Instance Methods

__init__(self, formula=None, input_variables=None, output_variables=None)
Instantiate an LTL object.

__repr__(self)
repr(x)

__str__(self)
str(x)

dumps(self, timestamp=False)
Dump TuLiP LTL file string.

check_vars(self)
Raise Exception if variabe definitions are invalid.

check_form(self, check_undeclared_identifiers=False)
Verify formula syntax and type-check variable domains.

Inherited from object: __delattr__, __format__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __setattr__, __sizeof__, __subclasshook__

Static Methods

loads(s)
Create LTL object from TuLiP LTL file string.

load(f)
Wrap loads for reading from files.

Properties
Inherited from `object`: `__class__`

Method Details

init(self, formula=None, input_variables=None, output_variables=None)
(Constructor)

Instantiate an LTL object.

Any non-None arguments are saved to the corresponding attribute by reference.

Overrides: object.__init__

repr(self)
(Representation operator)

repr(x)

Overrides: object.__repr__: (inherited documentation)

str(self)
(Informal representation operator)

str(x)

Overrides: object.__str__: (inherited documentation)

dumps(self, timestamp=False)

Dump TuLiP LTL file string.

Parameters:

timestamp - If True, then add comment to file with current time in UTC.

check_vars(self)

Raise Exception if variabe definitions are invalid.

Checks:

env and sys have common vars
some var is also a possible value of some var (including itself) (of arbitrary finite data type)

check_form(self, check_undeclared_identifiers=False)

Verify formula syntax and type-check variable domains.

Return True iff OK.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

load(f)
Static Method

Wrap loads for reading from files.

Parameters:

f - file or str. In the latter case, attempt to open a file named "f" read-only.

Class LTL

__init__(self, formula=None, input_variables=None, output_variables=None) (Constructor)

__repr__(self) (Representation operator)

__str__(self) (Informal representation operator)