temporal_logic

all_globally_exists_finally_one_of_sub_spaces(primes: dict, sub_spaces: List[dict]) str

Constructs a CTL formula that queries whether there it is alsways possible to reach one of the given subspaces.

Note

This query is equivalent to asking whether every attractor is inside one of the subspaces.

Note

Typically this query is used to decide whether a known set of attractors A1, A2, … An is complete, i.e., whether there are any more attractors. To find out pick arbitrary representative states x1, x2, … xn for each attractor and call the function AGEF_oneof_subspaces with the argument Subspaces = [x1, x2, …, xn].

arguments:
  • subspaces: a list of subspace

returns:
  • formula: the CTL formula

example:

>>> subspaces = [{"v1":0,"v2":0},{"v2":1}]
>>> all_globally_exists_finally_one_of_sub_spaces(subspaces)
"AG(EF(!v1&!v2 | v2))"
exists_finally_nested_reachability(primes: dict, subspaces: List[Union[dict, str]]) str

Constructs a CTL formula that queries whether there is a path that visits the given subspaces in the order given.

arguments:
  • subspaces: a list of subspaces

returns:
  • ctl_formula: the CTL formula

example:

>>> subspaces = ["1--", "-01"]
>>> exists_finally_nested_reachability(subspaces)
"EF(v1&EF(!v2&v3))"
exists_finally_one_of_subspaces(primes: dict, subspaces: List[Union[dict, str]]) str

Constructs a CTL formula that queries whether there is a path that leads to one of the Subspaces.

arguments:
  • subspaces: a list of subspaces

returns:
  • formula: the CTL formula

example:

>>> subspaces = [{"v1":0,"v2":0}, "1-1--"]
>>> exists_finally_one_of_subspaces(primes, subspaces)
"EF(!v1&!v2 | v1&v3)"
exists_finally_unsteady_components(names: List[str]) str

Constructs a CTL formula that queries whether for every variables v specified in names there is a path to a state x in which v is unsteady.

Note

Typically this query is used to find out if the variables given in names are oscillating in a given attractor.

arguments:
  • names: a list of names of variables

returns:
  • ctl_formula: the CTL formula

example:

>>> names = ["v1","v2"]
>>> exists_finally_unsteady_components(names)
"EF(v1_steady!=0) & EF(v2_steady!=0))"
subspace2proposition(primes: dict, subspace: Union[dict, str]) str

Constructs a CTL formula that is true in a state x if and only if x belongs to the given Subspace.

Note

Typically this query is used to define INIT constraints from a given subspace.

arguments:
  • subspace: a subspace in string or dictionary representation

returns:
  • proposition: the proposition

example:

>>> subspace = {"v1":0,"v2":1}
>>> init = f"INIT {subspace2proposition(subspace)}"
>>> init
"INIT v1&!v2"