Skip to content

DFA

API Reference

masa.common.ltl.DFA 

DFA(states: List[int], initial: int, accepting: List[int])

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.

Attributes:

Name Type Description
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:

Name Type Description Default
states List[int]

List of automaton states (typically integers).

 required
initial int

Initial state.

 required
accepting List[int]

Accepting (final) states.

 required
Source code in masa/common/ltl.py 
243
244
245
246
247
248
249
250
251
252
253
254
255
def __init__(self, states: List[int], initial: int, accepting: List[int]):
    """Creates a DFA.

    Args:
      states: List of automaton states (typically integers).
      initial: Initial state.
      accepting: Accepting (final) states.
    """
    self.states = states
    self.initial = initial
    self.accepting = accepting
    self.edges = {s: {} for s in self.states}
    self.state = self.initial

states instance-attribute 

states = states

initial instance-attribute 

initial = initial

accepting instance-attribute 

accepting = accepting

edges instance-attribute 

edges = {s: {} for s in self.states}

state instance-attribute 

state = self.initial

num_automaton_states property 

num_automaton_states

Returns the number of states in the automaton.

Returns:

Type Description

len(self.states).

automaton_state property 

automaton_state

Returns the number of states in the automaton.

Returns:

Type Description

len(self.states).

add_edge 

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

Adds a guarded transition parent -> child.

Parameters:

Name Type Description Default
parent int

Source state.

 required
child int

Destination state.

 required
condition Formula

Guard formula enabling this transition when satisfied.

 required
Notes

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

Source code in masa/common/ltl.py 
257
258
259
260
261
262
263
264
265
266
267
268
269
def add_edge(self, parent: int, child: int, condition: Formula):
    """Adds a guarded transition ``parent -> child``.

    Args:
      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.
    """
    self.edges[parent][child] = condition

reset 

reset() -> int

Resets the DFA to the initial state.

Returns:

Type Description
int

The reset state (i.e., initial).
Source code in masa/common/ltl.py 
271
272
273
274
275
276
277
278
def reset(self) -> int:
    """Resets the DFA to the initial state.

    Returns:
      The reset state (i.e., :attr:`initial`).
    """
    self.state = self.initial
    return self.state

has_edge 

has_edge(state_1: int, state_2: int) -> bool

Checks whether there is an edge state_1 -> state_2.

Parameters:

Name Type Description Default
state_1 int

Source state.

 required
state_2 int

Destination state.

 required

Returns:

Type Description
bool

True iff an explicit edge from state_1 to state_2 exists.
Source code in masa/common/ltl.py 
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
def has_edge(self, state_1: int, state_2: int) -> bool:
    """Checks whether there is an edge ``state_1 -> state_2``.

    Args:
      state_1: Source state.
      state_2: Destination state.

    Returns:
      ``True`` iff an explicit edge from ``state_1`` to ``state_2`` exists.
    """
    try:
        _ = self.edges[state_1][state_2]
        return True
    except KeyError:
        return False

check 

check(trace: Iterable[Iterable[str]]) -> bool

Checks whether a trace is accepted by the DFA.

Parameters:

Name Type Description Default
trace Iterable[Iterable[str]]

Sequence of label sets, one per time step.

 required

Returns:

Type Description
bool

True iff the state reached after consuming the full trace is in
bool

accepting.
Source code in masa/common/ltl.py 
296
297
298
299
300
301
302
303
304
305
306
307
308
309
def check(self, trace: Iterable[Iterable[str]]) -> bool:
    """Checks whether a trace is accepted by the DFA.

    Args:
      trace: Sequence of label sets, one per time step.

    Returns:
      ``True`` iff the state reached after consuming the full trace is in
      :attr:`accepting`.
    """
    state = self.initial
    for labels in trace:
        state = self.transition(state, labels)
    return state in self.accepting

transition 

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

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

Parameters:

Name Type Description Default
state int

Current DFA state.

 required
labels Iterable[str]

Iterable of atomic proposition names holding at the current step.

 required

Returns:

Type Description
int

Next DFA state. If no outgoing edge guard is satisfied, returns the
int

original state (i.e., an implicit self-loop).
Source code in masa/common/ltl.py 
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
def transition(self, state: int, labels: Iterable[str]) -> int:
    """Computes the next automaton state given the current state and labels.

    Args:
      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).
    """
    for next_state in self.edges[state].keys():
        if self.edges[state][next_state].sat(labels):
            return next_state
    return state

step 

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

Advances the DFA by one step using the provided labels.

This updates the internal state.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names holding at the current step.

 required

Returns:

Type Description
bool

A pair (accepting, state) where accepting indicates whether
int

the new state is in accepting, and state is the updated
Tuple[bool, int]

automaton state.
Source code in masa/common/ltl.py 
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
def step(self, labels: Iterable[str]) -> Tuple[bool, int]:
    """Advances the DFA by one step using the provided labels.

    This updates the internal :attr:`state`.

    Args:
      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 :attr:`accepting`, and ``state`` is the updated
      automaton state.
    """
    next_state = self.transition(self.state, labels)
    self.state = next_state
    return self.state in self.accepting, self.state