Interfaces

class ggsolver.interfaces.i_spot.SpotAutomaton(formula=None, options=None)

SpotAutomaton constructs an Automaton from an LTL specification string using spot (https://spot.lrde.epita.fr/) with customizations for ggsolver.

Customizations: Since ggsolver contains several algorithms for reactive/controller synthesis, we prefer to construct deterministic automata. Given an LTL formula, SpotAutomaton automatically determines the best acceptance condition that would result in a deterministic automaton..

Programmer’s note: The graphified version of automaton does not use PL formulas as edge labels. This is intentionally done to be able to run our codes on robots that may not have logic libraries installed.

__init__(formula=None, options=None)

Given an LTL formula, SpotAutomaton determines the best options for spot.translate() function to generate a deterministic automaton in ggsolver.Automaton format.

Parameters

• formula – (str) LTL formula.

• options – (List/Tuple of str) Valid options for spot.translate() function. By default, the value is None, in which case, the options are determined automatically. See description below.

Default translation options: While constructing an automaton using spot, we use the following options: deterministic, high, complete, unambiguous, SBAcc. If selected acceptance condition is parity, then we use colored option as well.

The default options can be overriden. For quick reference, the following description is copied from spot documentation (spot.lrde.epita.fr/doxygen).

The optional arguments should be strings among the following: - at most one in ‘GeneralizedBuchi’, ‘Buchi’, or ‘Monitor’, ‘generic’, ‘parity’, ‘parity min odd’, ‘parity min even’, ‘parity max odd’, ‘parity max even’, ‘coBuchi’ (type of acceptance condition to build)

• at most one in ‘Small’, ‘Deterministic’, ‘Any’ (preferred characteristics of the produced automaton)

• at most one in ‘Low’, ‘Medium’, ‘High’ (optimization level)

• any combination of ‘Complete’, ‘Unambiguous’, ‘StateBasedAcceptance’ (or ‘SBAcc’ for short), and ‘Colored’ (only for parity acceptance)

_determine_options()

Determines the options based on where the given LTL formula lies in Manna-Pnueli hierarchy.

acc_cond()

Returns acceptance condition according to ggsolver definitions: See ACC_REACH, … variables in Automaton class. See SpotAutomaton.spot_acc_cond() for acceptance condition in spot’s nomenclature.

acc_name()

Name of acceptance condition as per spot’s nomenclature.

atoms()

Atomic propositions appearing in LTL formula.

delta(state, inp)

Transition function of automaton. For a deterministic automaton, returns a single state. Otherwise, returns a list/tuple of states.

Parameters

• state – (object) A valid state.

• inp – (list) List of atoms that are true (an element of sigma).

classmethod deserialize(obj_dict)

Constructs a graphical model from a serialized graph object. The node properties are deserialized as state properties, the edge properties are deserialized as transition properties, and the graph properties are deserialized as model properties. All the deserialized properties are represented as a function in the GraphicalModel class. See example #todo.

The format is described in GraphicalModel.serialize().

Returns

(Sub-class of GraphicalModel) An instance of the cls class. cls must be a sub-class of GraphicalModel.

final(state)

Maps every state to its acceptance set.

formula()

The LTL Formula.

init_state()

Initial state of automaton.

is_complete()

Is the automaton complete?

is_deterministic()

Is the automaton deterministic?

is_inherently_weak()

Is it the case that accepting and rejecting cycles cannot be mixed in the same SCC?

is_semi_deterministic()

Is the automaton semi-deterministic? See https://spot.lrde.epita.fr/doxygen/namespacespot.html#a56b3f00b7b93deafb097cad595998783

is_state_based_acc()

Is the acceptance condition state-based?

is_stutter_invariant()

The property recognized by the automaton is stutter-invariant (see https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf)

is_terminal()

Automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs. An automaton is weak if the transitions of an SCC all belong to the same acceptance sets.

See https://spot.lrde.epita.fr/concepts.html

is_unambiguous()

There is at most one run accepting a word (but it might be recognized several time). See https://spot.lrde.epita.fr/concepts.html.

is_weak()

Are transitions of an SCC all belong to the same acceptance sets?

num_acc_sets()

Number of acceptance sets.

serialize()

Serializes the underlying graph of the graphical model into a dictionary with the following format. The state properties are saved as node properties, transition properties are stored are edge properties and model properties are stored as graph properties in the underlying graph:

{
    "graph": {
        "nodes": <number of nodes>,
        "edges": {
            uid: {vid: key},
            ...
        }
        "node_properties": {
            "property_name": {
                "default": <value>,
                "dict": {
                    "uid": <property value>,
                    ...
                }
            },
            ...
        },
        "edge_properties": {
            "property_name": {
                "default": <value>,
                "dict": [{"edge": [uid, vid, key], "pvalue": <property value>} ...]
            },
            ...
        },
        "graph_properties": {
            "property_name": <value>,
            ...
        }
    }
}

Returns

(dict) Serialized graphical model.

sigma()

Returns the set of alphabet of automaton. It is the powerset of atoms().

spot_acc_cond()

Acceptance condition in spot’s nomenclature.

states()

States of automaton.