DFA

API Reference

class masa.common.ltl.DFA(states: List[int], initial: int, accepting: List[int])

Bases: object

Deterministic finite automaton with propositional guards on edges.

Each edge from a parent state to a child state is labelled with a guard Formula. A transition is taken when its guard is satisfied by the current label set.

Variables:

• states – List of automaton states.

• initial – Initial automaton state.

• accepting – List of accepting (final) states.

• edges – Transition structure mapping parent -> {child: guard}.

• state – Current automaton state used by step().

Notes

The transition relation is deterministic by convention: if multiple outgoing guards from a state are simultaneously satisfied, the first one encountered in iteration order is taken. For strict determinism, ensure guards are mutually exclusive.

Creates a DFA.

Parameters:

• states – List of automaton states (typically integers).

• initial – Initial state.

• accepting – Accepting (final) states.

add_edge(parent: int, child: int, condition: Formula)

Adds a guarded transition parent -> child.

Parameters:

• parent – Source state.

• child – Destination state.

• condition – Guard formula enabling this transition when satisfied.

Notes

This overwrites any existing edge guard between the same parent/child pair.

reset() → int

Resets the DFA to the initial state.

Returns:

The reset state (i.e., initial).

has_edge(state_1: int, state_2: int) → bool

Checks whether there is an edge state_1 -> state_2.

Parameters:

• state_1 – Source state.

• state_2 – Destination state.

Returns:

True iff an explicit edge from state_1 to state_2 exists.

check(trace: Iterable[Iterable[str]]) → bool

Checks whether a trace is accepted by the DFA.

Parameters:

trace – Sequence of label sets, one per time step.

Returns:

True iff the state reached after consuming the full trace is in accepting.

transition(state: int, labels: Iterable[str]) → int

Computes the next automaton state given the current state and labels.

Parameters:

• state – Current DFA state.

• labels – Iterable of atomic proposition names holding at the current step.

Returns:

Next DFA state. If no outgoing edge guard is satisfied, returns the original state (i.e., an implicit self-loop).

step(labels: Iterable[str]) → Tuple[bool, int]

Advances the DFA by one step using the provided labels.

This updates the internal state.

Parameters:

labels – Iterable of atomic proposition names holding at the current step.

Returns:

A pair (accepting, state) where accepting indicates whether the new state is in accepting, and state is the updated automaton state.

property num_automaton_states

Returns the number of states in the automaton.

Returns:

len(self.states).

property automaton_state

Returns the number of states in the automaton.

Returns:

len(self.states).