gym_tl_tools.automaton

Functions

`add_or_parentheses`(condition)
`replace_atomic_pred_ids_to_names`(condition, ...)

Classes

`Automaton`(tl_spec, atomic_predicates, parser)
`AutomatonStateCounter`(*, state, ind)
`Edge`(raw_state, atomic_pred_names)	Represents an edge in a finite state automaton from a LTL formula.
`Predicate`(*, name, formula)	Represents a predicate in a TL formula.
`RobNextStatePair`(*, robustness, next_state)	Represents a pair of robustness value and transition.
`RobustnessCounter`(*, robustness, ind)
`Transition`(*, condition, next_state[, ...])	Represents a transition in a finite state automaton from a LTL formula.

class gym_tl_tools.automaton.Automaton(tl_spec: str, atomic_predicates: list[~gym_tl_tools.automaton.Predicate], parser: ~gym_tl_tools.parser.Parser = <gym_tl_tools.parser.Parser object>)[source]

Bases: object

property is_goaled: bool: Check if the current state of the automaton is a goal state. :returns: True if the current state is a goal state, False otherwise. :rtype: bool

property is_terminated: bool: Check if the automaton is in a terminal state (goal or trap). :returns: True if the automaton is in a terminal state, False otherwise. :rtype: bool

property is_trapped: bool: Check if the current state of the automaton is a trap state. :returns: True if the current state is a trap state, False otherwise. :rtype: bool

reset(seed: int | None = None) → None[source]: Reset the automaton to its initial state.

step(var_value_dict: dict[str, float], terminal_state_reward: float = 5, state_trans_reward_scale: float = 100, dense_reward: bool = False, dense_reward_scale: float = 0.01) → tuple[float, int][source]

Step the automaton to the next state based on the current predicate values. This function updates the current state of the automaton based on the values of variables defining atomic predicates provided in var_value_dict.

Parameters:

var_value_dict (dict[str, float]) – A dictionary mapping the variable names used in the atomic predicate definitions to their current values. e.g. {“d_robot_goal”: 3.0, “d_robot_obstacle”: 1.0, “d_robot_goal”: 0.5}.
terminal_state_reward (float = 5)

Returns:

reward (float) – The reward for the current step.
new_state (int) – The new automaton state.

tl_reward(ap_rob_dict: dict[str, float], curr_aut_state: int, terminal_state_reward: float = 5, state_trans_reward_scale: float = 100, dense_reward: bool = False, dense_reward_scale: float = 0.01) → tuple[float, int][source]

Calculate the reward of the step from a given automaton.

Parameters:

ap_rob_dict (dict[str, float]) – A dictionary mapping the names of atomic predicates to their robustness values.
curr_aut_state (int) – The current state of the automaton.
dense_reward (bool) – If True, the reward is calculated based on the maximum robustness of non-trap transitions.
terminal_state_reward (float) – The reward given when the automaton reaches a terminal state.

Returns:

reward (float) – The reward of the step based on the MDP and automaton states.
next_aut_state (int) – The resultant automaton state after the step.

transition_robustness(transitions: list[Transition], ap_rob_dict: dict[str, float]) → tuple[list[RobNextStatePair], list[RobNextStatePair], list[RobNextStatePair], list[RobNextStatePair], list[RobNextStatePair]][source]

Calculate the robustness of transitions in the automaton. This function computes the robustness values for each transition based on the conditions of the transitions and the robustness values of the atomic predicates.

Parameters:

transitions (list[Transition]) – A list of transitions in the automaton.
ap_rob_dict (dict[str, float]) – A dictionary mapping the names of atomic predicates to their robustness values.

Returns:

pos_trap_rob_trans_pairs (list[RobNextStatePair]) – A list of pairs of positive robustness values and transitions that lead to trap states.
pos_non_trap_rob_trans_pairs (list[RobNextStatePair]) – A list of pairs of positive robustness values and transitions that do not lead to trap states.
zero_trap_rob_trans_pairs (list[RobNextStatePair]) – A list of pairs of zero robustness values and transitions that lead to trap states.
zero_non_trap_rob_trans_pairs (list[RobNextStatePair]) – A list of pairs of zero robustness values and transitions that do not lead to trap states.

class gym_tl_tools.automaton.AutomatonStateCounter(*, state: int, ind: int)[source]

Bases: BaseModel

ind: int

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

state: int

class gym_tl_tools.automaton.Edge(raw_state: str, atomic_pred_names: list[str])[source]

Bases: object

Represents an edge in a finite state automaton from a LTL formula. .. attribute:: state

The automaton state.

type:

int

transitions

The transitions from this state to other states.

Type:: list[Transition]

is_inf_zero_acc

Indicates if the edge has an Inf(0) acceptance condition.

Type:: bool

is_terminal_state

Indicates if the edge is a terminal state (i.e., no further transitions are possible).

Type:: bool

is_trap_state

Indicates if the edge is a trap state (i.e., all transitions lead to trap states).

Type:: bool

class gym_tl_tools.automaton.Predicate(*, name: str, formula: str)[source]

Bases: BaseModel

Represents a predicate in a TL formula.

name

The name of the atomic predicate. e.g. “psi_goal_robot”.

Type:: str

formula

The formula of the atomic predicate, which can be a Boolean expression. e.g. “d_robot_goal < 5”.

Type:: str

formula: str

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

name: str

class gym_tl_tools.automaton.RobNextStatePair(*, robustness: float, next_state: int)[source]

Bases: BaseModel

Represents a pair of robustness value and transition.

robustness

The robustness value of the transition.

Type:: float

next_state

The next state of the automaton after the transition.

Type:: int

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

next_state: int

robustness: float

class gym_tl_tools.automaton.RobustnessCounter(*, robustness: float, ind: int)[source]

Bases: BaseModel

ind: int

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

robustness: float

class gym_tl_tools.automaton.Transition(*, condition: str, next_state: int, is_trapped_next: bool = False)[source]

Bases: BaseModel

Represents a transition in a finite state automaton from a LTL formula.

next_state

The next automaton state after the transition.

Type:: int

condition

The condition that triggers the transition represented as a Boolean expression. e.g. “psi_1 & psi_2” or “psi_1 | !psi_2”.

Type:: str

is_trapped_next

Indicates if the next state is a trap state (i.e., no further transitions are possible). Defaults to False.

Type:: bool

condition: str

is_trapped_next: bool

model_config: ClassVar[ConfigDict] = {}: Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

next_state: int

gym_tl_tools.automaton.add_or_parentheses(condition: str) → str[source]

gym_tl_tools.automaton.replace_atomic_pred_ids_to_names(condition: str, atom_prop_names: list[str])[source]