Automata

Note

All the following automata inherit from ggsolver.models.Automaton. Refer to the class documentation for a description of inherited functions.

DFA: Deterministic Finite Automaton

class ggsolver.automata.DFA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Represents a Deterministic Finite-state Automaton.

  • Acceptance Type: Automaton.ACC_REACH

  • Acceptance condition: (Reach, 0)

    • Accepts: Finite words.

    • Interpretation: \(\mathsf{Last}(\rho) \in F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

  • Number of Acceptance Sets: 1

  • final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Constructs a DFA.

Parameters
  • states – (Iterable) An iterable over states in the automaton.

  • atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

  • trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

  • init_state – (object) The initial state, a member of states iterable.

  • final – (Iterable[states]) The set of final states, a subset of states iterable.

Monitor: Deterministic Safety Automaton

class ggsolver.automata.Monitor(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Represents a Safety automaton.

  • Acceptance Type: Automaton.ACC_SAFETY

  • Acceptance condition: (Safety, 0)

    • Accepts: Infinite words.

    • Interpretation: \(\mathsf{Occ}(\rho) \subseteq F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

  • Number of Acceptance Sets: 1

  • final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Constructs a Monitor.

Parameters
  • states – (Iterable) An iterable over states in the automaton.

  • atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

  • trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

  • init_state – (object) The initial state, a member of states iterable.

  • final – (Iterable[states]) The set of final states, a subset of states iterable.

DBA: Deterministic Buchi Automaton

class ggsolver.automata.DBA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Represents a Deterministic Buchi automaton.

  • Acceptance Type: Automaton.ACC_BUCHI

  • Acceptance condition: (Buchi, 0)

    • Accepts: Infinite words.

    • Interpretation: \(\mathsf{Inf}(\rho) \cap F \neq \emptyset\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

  • Number of Acceptance Sets: 1

  • final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Constructs a DBA.

Parameters
  • states – (Iterable) An iterable over states in the automaton.

  • atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

  • trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

  • init_state – (object) The initial state, a member of states iterable.

  • final – (Iterable[states]) The set of final states, a subset of states iterable.

DCBA: Deterministic co-Buchi Automaton

class ggsolver.automata.DCBA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Represents a Deterministic co-Buchi automaton.

  • Acceptance Type: Automaton.ACC_COBUCHI

  • Acceptance condition: (co-Buchi, 0)

    • Accepts: Infinite words.

    • Interpretation: \(\mathsf{Inf}(\rho) \subseteq F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

  • Number of Acceptance Sets: 1

  • final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Constructs a DCBA.

Parameters
  • states – (Iterable) An iterable over states in the automaton.

  • atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

  • trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

  • init_state – (object) The initial state, a member of states iterable.

  • final – (Iterable[states]) The set of final states, a subset of states iterable.

DPA: Deterministic Parity Automaton

class ggsolver.automata.DPA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Represents a Deterministic Buchi automaton.

  • Acceptance Type: Automaton.ACC_PARITY

  • Acceptance condition: (Parity Min Even , 0)

    • Accepts: Infinite words.

    • Interpretation: \(\min_{q \in \mathsf{Inf}(\rho)} \chi(q)\) is even, where \(\chi: Q \rightarrow \mathbb{N}\) is a coloring function that associates every state in DPA with a color (an integer).

  • Number of Acceptance Sets: k, where k is a positive integer.

  • final(state) a value between 0 and k-1 to indicate that the color of a state.

Note

The DPA definition is not stable. DO NOT USE IT!

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)[source]

Constructs a DPA.

Parameters
  • states – (Iterable) An iterable over states in the automaton.

  • atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

  • trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

  • init_state – (object) The initial state, a member of states iterable.

  • final – (dict[state: int]) A state to color mapping.