Models
Automaton
- class ggsolver.models.Automaton(**kwargs)[source]
Represents an Automaton.
\[\mathcal{A} = (Q, \Sigma := 2^{AP}, \delta, q_0, F)\]In the Automaton class, each component is represented as a function.
The set of states \(Q\) is represented by Automaton.states function,
The set of atomic propositions \(AP\) is represented by Automaton.atoms function,
The set of symbols \(\Sigma\) is represented by Automaton.sigma function,
The transition function \(\delta\) is represented by Automaton.delta function,
The initial state \(q_0\) is represented by Automaton.init_state function.
An automaton may have one of the following acceptance conditions:
(
Automaton.ACC_REACH
, 0)(
Automaton.ACC_SAFETY
, 0)(
Automaton.ACC_BUCHI
, 0)(
Automaton.ACC_PARITY
, 0)(
Automaton.ACC_PREF_LAST
, None)(
Automaton.ACC_ACC_PREF_MP
, None)
- ACC_BUCHI = 'Buchi'
- ACC_COBUCHI = 'co-Buchi'
- ACC_PARITY = 'Parity Min Even'
- ACC_PREF_LAST = 'Preference Last'
- ACC_PREF_MP = 'Preference MostPreferred'
- ACC_REACH = 'Reach'
- ACC_SAFETY = 'Safety'
- ACC_TYPES = ['undefined', 'Reach', 'Safety', 'Buchi', 'co-Buchi', 'Parity Min Even', 'Preference Last', 'Preference MostPreferred']
Acceptance conditions supported by Automaton.
- __init__(**kwargs)[source]
Supported keyword arguments:
- 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.
acc_cond – (tuple) A tuple of automaton acceptance type and an acceptance set. For example, DFA has an acceptance condition of (Automaton.ACC_REACH, 0).
is_deterministic – (bool) Whether the Automaton is deterministic.
- acc_cond()[source]
Acceptance condition of the automaton.
- Returns
(2-tuple) A value of type (acc_type, acc_set) where acc_type is from
Automaton.ACC_TYPES
and acc_set is either an integer or a list of integer.
- acc_type()[source]
Acceptance type of the automaton.
- Returns
A value from
Automaton.ACC_TYPES
.
- atoms()[source]
Returns a list/tuple of atomic propositions.
- Returns
(list of str) A list of atomic proposition.
- 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)[source]
Returns the acceptance set associated with the given state.
- Parameters
state – (an element of self.states()) A valid state.
- Returns
(int) Acceptance set associated with the given state.
- from_automaton(aut: Automaton)[source]
Constructs a DFA from another Automaton instance. The input automaton’s acceptance condition must match that of a DFA.
- graphify(pointed=False)
Constructs the underlying graph of the graphical model.
- Parameters
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_pointed()
Constructs the underlying graph of the graphical model. The constructed graph contains only the states that are reachable from the initial state.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_unpointed()
Constructs the underlying graph of the graphical model. The constructed graph contains all possible states in the model.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- init_state()
Returns the initial state of the graphical model.
- initialize(state)
Sets the initial state of the graphical model.
Note
The function does NOT check if the given state is valid.
- is_complete()[source]
Is the automaton complete? That is, is transition function well-defined at every state for any input symbol?
- is_deterministic()
Returns True if the graphical model is deterministic. Else, returns False.
- is_nondeterministic()
Returns True if the graphical model is non-deterministic. Else, returns False.
- is_probabilistic()
Returns True if the graphical model is probabilistic. Else, returns False.
- classmethod load(fpath, protocol='json')
Loads the graphical model from file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- save(fpath, pointed=False, overwrite=False, protocol='json')
Saves the graphical model to file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- 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.
- states()
Defines the states component of the graphical model.
- Returns
(list/tuple of JSONifiable object). List or tuple of states.
TSys
- class ggsolver.models.TSys(is_deterministic=True, is_probabilistic=False, **kwargs)[source]
Represents a transition system [Principles of Model Checking, Def. 2.1].
\[TSys = (S, A, T, AP, L)\]In the TSys class, each component is represented as a function.
The set of states \(S\) is represented by TSys.states function,
The set of actions \(A\) is represented by TSys.actions function,
The transition function \(T\) is represented by TSys.delta function,
The set of atomic propositions is represented by TSys.atoms function,
The labeling function \(L\) is represented by TSys.label function.
All of the above functions are marked abstract. The recommended way to use TSys class is by subclassing it and implementing its component functions.
A transition system can be either deterministic or non-deterministic or probabilistic. To define a deterministic transition system, provide a keyword argument is_deterministic=True to the constructor. To define a nondeterministic transition system, provide a keyword argument is_deterministic=False to the constructor. To define a probabilistic transition system, provide a keyword arguments is_deterministic=False, is_probabilistic=True to the constructor.
The design of TSys class closely follows its mathematical definition. Hence, the signatures of delta function for deterministic, nondeterministic, probabilistic transition systems are different.
deterministic: delta(state, act) -> single state
non-deterministic: delta(state, act) -> a list of states
probabilistic: delta(state, act) -> a distribution over states
An important feature of TSys class is the graphify() function. It constructs a Graph object that is equivalent to the transition system. The nodes of the Graph represent the states of TSys, the edges of the Graph are defined by the set of actions and the delta function. The atomic propositions, labeling function are stored as node, edge and graph properties. By default, every Graph returned a TSys.graphify() function have the following (node/edge/graph) properties:
state: (node property) A Map from every node to the state of transition system it represents.
actions: (graph property) List of valid actions.
input: (edge property) A map from every edge (uid, vid, key) to its associated action label.
prob: (edge property) The probability associated with the edge (uid, vid, key).
atoms: (graph property) List of valid atomic propositions.
label: (node property) A map every node to the list of atomic propositions true in the state represented by that node.
init_state: (graph property) Initial state of transition system.
is_deterministic: (graph property) Is the transition system deterministic?
is_probabilistic: (graph property) Is the transition system probabilistic?
Note: Some features of probabilistic transition system are not tested. If you are trying to implement a probabilistic transition system, reach out to Abhishek Kulkarni (a.kulkarni2@ufl.edu).
Next, we demonstrate how to use TSys class to define a deterministic, non-deterministic and probabilistic transition system.
- __init__(is_deterministic=True, is_probabilistic=False, **kwargs)[source]
Constructs a transition system.
- Parameters
is_deterministic – (bool). If True then the transition system is deterministic. Otherwise, it is either non-deterministic or probabilistic.
is_probabilistic – (bool). If is_deterministic is False, then if is_probabilistic is True then the transition system is probabilistic. Otherwise, it is non-deterministic.
input_domain – (optional, function). A member function of TSys class that defines the inputs to the transition system. [Default: TSys.actions]
input_name – (optional, str). The name of input property during graphify().
init_state – (optional, JSON-serializable object). The initial state of the transition system.
- actions()[source]
Defines the actions component of the transition system.
- Returns
(list/tuple of str). List or tuple of action labels.
- atoms()[source]
Defines the atomic propositions component of the transition system.
- Returns
(list/tuple of str). List or tuple of atomic proposition labels.
- delta(state, act)[source]
Defines the transition function of the transition system.
- Parameters
state – (object) A valid state.
act – (str) An action.
- Returns
(object/list(object)/util.Distribution object). Depending on the type of transition system, the return type is different. - Deterministic: returns a single state. - Non-deterministic: returns a list/tuple of states. - Probabilistic: returns a distribution over all state.
- 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.
- graphify(pointed=False)
Constructs the underlying graph of the graphical model.
- Parameters
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_pointed()
Constructs the underlying graph of the graphical model. The constructed graph contains only the states that are reachable from the initial state.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_unpointed()
Constructs the underlying graph of the graphical model. The constructed graph contains all possible states in the model.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- init_state()
Returns the initial state of the graphical model.
- initialize(state)
Sets the initial state of the graphical model.
Note
The function does NOT check if the given state is valid.
- is_deterministic()
Returns True if the graphical model is deterministic. Else, returns False.
- is_nondeterministic()
Returns True if the graphical model is non-deterministic. Else, returns False.
- is_probabilistic()
Returns True if the graphical model is probabilistic. Else, returns False.
- label(state)[source]
Defines the labeling function of the transition system.
- Parameters
state – (object) A valid state.
- Returns
(list/tuple of str). A list/tuple of atomic propositions that are true in the given state.
- classmethod load(fpath, protocol='json')
Loads the graphical model from file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- save(fpath, pointed=False, overwrite=False, protocol='json')
Saves the graphical model to file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- 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.
- states()
Defines the states component of the graphical model.
- Returns
(list/tuple of JSONifiable object). List or tuple of states.
Game
- class ggsolver.models.Game(is_turn_based=True, is_deterministic=True, is_probabilistic=False, **kwargs)[source]
Represents a game transition system, hereafter referred simply as a game. A Game can represent two mathematical structures commonly used in literature, namely
\[G = (S, A, T, AP, L, formula)\]\[G = (S, A, T, F, WinCond)\]In the Game class, each component is represented as a function. By defining the relevant functions, a Game class may represent either of the two mathematical structures.
The set of states \(S\) is represented by Game.states function,
The set of actions \(A\) is represented by Game.actions function,
The transition function \(T\) is represented by Game.delta function,
The set of atomic propositions \(AP\) is represented by Game.atoms function,
The labeling function \(L\) is represented by Game.label function.
When the winning condition is represented by a logic formula \(formula\), we define Game.formula function.
When the winning condition is represented by a final states \(F\), we define Game.final function. In this case, we must also specify the acceptance condition.
The winning condition \(WinCond\) is represented by Game.win_cond function.
All of the above functions are marked abstract. The recommended way to use Game class is by subclassing it and implementing the relevant component functions.
Categorization of a Game: A game is categorized by three types:
A game can be either deterministic or non-deterministic or probabilistic. To define a deterministic transition system, provide a keyword argument is_deterministic=True to the constructor. To define a nondeterministic transition system, provide a keyword argument is_deterministic=False to the constructor. To define a probabilistic transition system, provide a keyword arguments is_deterministic=False, is_probabilistic=True to the constructor.
The design of Game class closely follows its mathematical definition. Hence, the signatures of delta function for deterministic, nondeterministic, probabilistic games are different.
deterministic: delta(state, act) -> single state
non-deterministic: delta(state, act) -> a list of states
probabilistic: delta(state, act) -> a distribution over states
A game can be turn-based or concurrent. To define a concurrent game, provide a keyword argument is_turn_based=False. The game is turn_based by default.
A game can be a 1/1.5/2/2.5-player game. A one-player game models a deterministic motion planning-type problem in a static environment. A 1.5-player game is an MDP. A two-player game models a deterministic interaction between two strategic players. And, a 2.5-player game models a stochastic interaction between two strategic players.
If a game is one or two player, then the
Game.delta()
is deterministic. If a game is 1.5 or 2.5 player, then theGame.delta()
is either non-deterministic (when transition probabilities are unknown), and probabilistic (when transition probabilities are known).
Every state in a turn-based game is controlled by a player. To define which player controls which state, define a game component
Game.turn()
which takes in a state and returns a value between 0 and 3 to indicate which player controls the state.An important feature of Game class is the graphify() function. It constructs a Graph object that is equivalent to the game. The nodes of the Graph represent the states of Game, the edges of the Graph are defined by the set of actions and the delta function. The atomic propositions, labeling function are stored as node, edge and graph properties. By default, every Graph returned a Game.graphify() function have the following (node/edge/graph) properties:
state: (node property) A Map from every node to the state of transition system it represents.
actions: (graph property) List of valid actions.
input: (edge property) A map from every edge (uid, vid, key) to its associated action label.
prob: (edge property) The probability associated with the edge (uid, vid, key).
atoms: (graph property) List of valid atomic propositions.
label: (node property) A map every node to the list of atomic propositions true in the state represented by that node.
init_state: (graph property) Initial state of transition system.
is_deterministic: (graph property) Is the transition system deterministic?
is_probabilistic: (graph property) Is the transition system probabilistic?
is_turn_based: (graph property) Is the transition system turn-based?
final: (node property) Returns an integer denoting the acceptance set the state belongs to.
win_cond: (graph property) The winning condition of the game.
formula: (graph property) A logic formula representing the winning condition of the game.
turn: (node property) A map from every node to an integer (0/1/2) that denotes which player controls the node.
p1_acts: (graph property) A subset of actions accessible to P1.
p2_acts: (graph property) A subset of actions accessible to P2.
Note: Some features of probabilistic transition system are not tested. If you are trying to implement a probabilistic transition system, reach out to Abhishek Kulkarni (a.kulkarni2@ufl.edu).
- __init__(is_turn_based=True, is_deterministic=True, is_probabilistic=False, **kwargs)[source]
Constructs a transition system.
- Parameters
is_deterministic – (bool). If True then the transition system is deterministic. Otherwise, it is either non-deterministic or probabilistic.
is_probabilistic – (bool). If is_deterministic is False, then if is_probabilistic is True then the transition system is probabilistic. Otherwise, it is non-deterministic.
input_domain – (optional, function). A member function of TSys class that defines the inputs to the transition system. [Default: TSys.actions]
input_name – (optional, str). The name of input property during graphify().
init_state – (optional, JSON-serializable object). The initial state of the transition system.
- actions()
Defines the actions component of the transition system.
- Returns
(list/tuple of str). List or tuple of action labels.
- atoms()
Defines the atomic propositions component of the transition system.
- Returns
(list/tuple of str). List or tuple of atomic proposition labels.
- delta(state, act)
Defines the transition function of the transition system.
- Parameters
state – (object) A valid state.
act – (str) An action.
- Returns
(object/list(object)/util.Distribution object). Depending on the type of transition system, the return type is different. - Deterministic: returns a single state. - Non-deterministic: returns a list/tuple of states. - Probabilistic: returns a distribution over all state.
- 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)[source]
Defines whether the given state is a final state. The structure of final state is based on the winning condition [See Automata, Logics and Infinite Games (Ch. 2)].
- Parameters
state – (object) A valid state.
- Returns
(int or a list of ints). The integer denotes the acceptance set the state belongs to.
- graphify(pointed=False)
Constructs the underlying graph of the graphical model.
- Parameters
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_pointed()
Constructs the underlying graph of the graphical model. The constructed graph contains only the states that are reachable from the initial state.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- graphify_unpointed()
Constructs the underlying graph of the graphical model. The constructed graph contains all possible states in the model.
- Returns
(
ggsolver.graph.Graph
object) An equivalent graph representation of the graphical model.
- init_state()
Returns the initial state of the graphical model.
- initialize(state)
Sets the initial state of the graphical model.
Note
The function does NOT check if the given state is valid.
- is_deterministic()
Returns True if the graphical model is deterministic. Else, returns False.
- is_nondeterministic()
Returns True if the graphical model is non-deterministic. Else, returns False.
- is_probabilistic()
Returns True if the graphical model is probabilistic. Else, returns False.
- label(state)
Defines the labeling function of the transition system.
- Parameters
state – (object) A valid state.
- Returns
(list/tuple of str). A list/tuple of atomic propositions that are true in the given state.
- classmethod load(fpath, protocol='json')
Loads the graphical model from file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- save(fpath, pointed=False, overwrite=False, protocol='json')
Saves the graphical model to file.
- Parameters
fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the
TSys.graphify_pointed()
is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise,TSys.graphify_unpointed()
is called, which constructs the complete transition system.overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.
Note
Pickle protocol is not tested.
- 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.
- states()
Defines the states component of the graphical model.
- Returns
(list/tuple of JSONifiable object). List or tuple of states.
- turn(state)[source]
Defines the player who controls the given state.
- Parameters
state – (object) A valid state.
- Returns
(int). In turn-based game, turn can be 1 for player 1 or 2 for player 2. In concurrent games, the turn must be 0.
Note
For concurrent games, the turn function can be left unimplemented.