tulip :: spec :: form :: GRSpec :: Class GRSpec

Class GRSpec

GR(1) specification.

The basic form is:

 (env_init & []env_safety & []<>env_prog_1 & []<>env_prog_2 & ...)
   -> (sys_init & []sys_safety & []<>sys_prog_1 & []<>sys_prog_2 & ...)

A GRSpec object contains the following attributes:

moore: select whether a strategy can see primed environment variables.
plus_one: select causal implication between assumptions and guarantees.
qinit: select quantification of initial values for variables:
- '\A \A': forall env forall sys assume env_init sys_init must be empty
- '\A \E': forall env exist sys (usually not Moore) assume env_init and require sys_init
- '\E \A': exist sys forall env assume env_init and require sys_init
- '\E \E': exist env exist sys require sys_init env_init must be empty
env_vars: alias for input_variables of LTL, concerning variables that are determined by the environment.
env_init: a list of string that specifies the assumption about the initial state of the environment.
env_safety: a list of string that specifies the assumption about the evolution of the environment state.
env_prog: a list of string that specifies the justice assumption on the environment.
sys_vars: alias for output_variables of LTL, concerning variables that are controlled by the system.
sys_init: a list of string that specifies the requirement on the initial state of the system.
sys_safety: a list of string that specifies the safety requirement.
sys_prog: a list of string that specifies the progress requirement.

An empty list for any formula (e.g., if env_init = []) is marked as "True" in the specification. This corresponds to the constant Boolean function, which usually means that subformula has no effect (is non-restrictive) on the spec.

Consult GRSpec.__init__ concerning arguments at the time of instantiation.

Instance Methods

__init__(self, env_vars=None, sys_vars=None, env_init='', sys_init='', env_safety='', sys_safety='', env_prog='', sys_prog='', moore=True, plus_one=True, qinit='\\A \\A', parser=<module 'tulip.spec.parser' from '/home/scott/scott_centre/scm...)
Instantiate a GRSpec object.

__repr__(self)
repr(x)

__str__(self)
str(x)

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

pretty(self)
Return pretty printing string.

check_syntax(self)
Raise `AssertionError` for misplaced primed variables.

copy(self)
Return a copy of `self`.

__or__(self, other)
Create union of two specifications.

to_canon(self)
Output formula in TuLiP LTL syntax.

sub_values(self, var_values)
Substitute given values for variables.

code

compile_init(self, no_str)
Compile python expression for initial conditions.

str_to_int(self)
Replace arbitrary finite vars with int vars.

ast(self, x)
Return AST corresponding to formula x.

parse(self)
Parse each clause and store it.

Inherited from LTL: check_form, check_vars

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

Static Methods

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

load(f)
Wrap loads for reading from files.

Properties
Inherited from `object`: `__class__`

Method Details

init(self, env_vars=None, sys_vars=None, env_init=`''`, sys_init=`''`, env_safety=`''`, sys_safety=`''`, env_prog=`''`, sys_prog=`''`, moore=True, plus_one=True, qinit=`'\\A \\A'`, parser=<module 'tulip.spec.parser' from '/home/scott/scott_centre/scm`...`)
(Constructor)

Instantiate a GRSpec object.

Instantiating GRSpec without arguments results in an empty formula. The default domain of a variable is "boolean".

Parameters:

env_vars (dict or iterable) - If env_vars is a dictionary, then its keys should be variable names, and values are domains of the corresponding variable. Else, if env_vars is an iterable, then assume all environment variables are boolean (or "atomic propositions"). Cf. GRSpec for details.
sys_vars (dict or iterable) - Mutatis mutandis, env_vars.
env_init, env_safety, env_prog, sys_init, sys_safety, sys_prog - A string or iterable of strings. An empty string is converted to an empty list. A string is placed in a list. iterables are converted to lists. Cf. GRSpec.
qinit - see class docstring
moore (bool)
plus_one (bool)

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.

Overrides: LTL.dumps

(inherited documentation)

loads(s)
Static Method

Create GRSpec object from TuLiP LTL file string.

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

Overrides: LTL.loads

load(f)
Static Method

Wrap loads for reading from files.

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

Parameters:

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

Overrides: LTL.load

to_canon(self)

Output formula in TuLiP LTL syntax.

The format is described in the Specifications section of the TuLiP User's Guide.

sub_values(self, var_values)

Substitute given values for variables.

Note that there are three ways to substitute values for variables:

syntactic using this function
no substitution by user code, instead flatten to python and use eval together with a dict defining the values of variables, as done in eval_init.

For converting non-integer finite types to integer types, use replace_finite_by_int.

Returns:: dict of ASTs after the substitutions, keyed by original clause (before substitution).

compile_init(self, no_str)

Compile python expression for initial conditions.

The returned bytecode can be used with eval and a dict assigning values to variables. Its value is the conjunction of env_init and sys_init.

Use the corresponding python data types for the dict values:

bool for Boolean variables
int for integers
str for arbitrary finite types

Parameters:

no_str - if True, then compile the formula where all string variables have been replaced by integers. Otherwise compile the original formula containing strings.

Returns: code

python expression compiled for eval

str_to_int(self)

Replace arbitrary finite vars with int vars.

Returns spec itself if it contains only int vars. Otherwise it returns a copy of spec with all arbitrary finite vars replaced by int-valued vars.

ast(self, x)

Return AST corresponding to formula x.

If AST for formula x has already been computed earlier, then return cached result.

parse(self)

Parse each clause and store it.

The AST resulting from each clause is stored in the dict attribute ast.

Class GRSpec

__init__(self, env_vars=None, sys_vars=None, env_init='', sys_init='', env_safety='', sys_safety='', env_prog='', sys_prog='', moore=True, plus_one=True, qinit='\\A \\A', parser=<module 'tulip.spec.parser' from '/home/scott/scott_centre/scm...) (Constructor)

__repr__(self) (Representation operator)

__str__(self) (Informal representation operator)

dumps(self, timestamp=False)

loads(s) Static Method

load(f) Static Method

to_canon(self)

sub_values(self, var_values)

compile_init(self, no_str)

str_to_int(self)

ast(self, x)

parse(self)

init(self, env_vars=None, sys_vars=None, env_init=`''`, sys_init=`''`, env_safety=`''`, sys_safety=`''`, env_prog=`''`, sys_prog=`''`, moore=True, plus_one=True, qinit=`'\\A \\A'`, parser=<module 'tulip.spec.parser' from '/home/scott/scott_centre/scm`...`)
(Constructor)

repr(self)
(Representation operator)

str(self)
(Informal representation operator)

loads(s)
Static Method

load(f)
Static Method