TSys class

Deterministic Transition System¶

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.

The example shows an example of defining a deterministic transition system.

Car Parking Transition System¶

Consider a car parking with $n$ slots where cars can enter or exit. There are two properties of interest, namely whether the parking lot is empty or full.

The CarParking class demonstrates how a parameterized transition system can be defined.

In [36]:

# This code block is necessary only when using `ggsolver:v0.1` docker image.
import sys
sys.path.append('/home/ggsolver/')

from examples.jupyter_patch import *

In [37]:

import logging
logger = logging.getLogger()
logger.setLevel(logging.ERROR)

A deterministic transition system is defined as follows:

• First we define a class that inherits from ggsolver.models.TSys class. We will call it CarParking.
• Define its __init__ method to define instance variables that store input parameters. In our case, the only input parameter is the number of slots in parking lot: num_slots.
• Implement the component functions states, actions, delta, atoms, label that define the transition system.

Note: If `__init__` method is defined for your derived class, then a call to `super(DerivedTSys, self).__init__()` must be made.

In [38]:

from ggsolver.models import TSys

class CarParking(TSys):
    def __init__(self, num_slots):
        super(CarParking, self).__init__()
        self.num_slots = num_slots

    def states(self):
        """
        To determine whether parking is full or empty, we can maintain a count of the number of cars
        in the parking lot. Hence, the states can be represented by integers from 0 to num_slots.
        """
        return list(range(self.num_slots + 1))

    def actions(self):
        """
        There are two actions: enter and exit, that represent a car has entered or exited.
        """
        return ["enter", "exit"]

    def delta(self, state, act):
        """
        The transition function should determine the next state, i.e. how many cars will be there in the parking lot, based on how many cars are currently in the parking lot and the action: whether a car is entering or exiting.
        """
        if state == 0 and act == "exit":
            return 0
        elif state == self.num_slots and act == "enter":
            return self.num_slots
        elif act == "enter":
            return state + 1
        else:   # if act == "exit":
            return state - 1

    def atoms(self):
        """
        We care about two properties: whether the parking lot is "empty" or it is "full".
        Hence, we will define two atomic propositions.
        """
        return ["empty", "full"]

    def label(self, state):
        """
        The parking lot is empty if count is 0, and it is full when count is equal to num_slots.
        """
        if state == 0:
            return ["empty"]
        elif state == self.num_slots:
            return ["full"]
        else:
            return []

Note that our class definition closely follows the mathematical definition of a transition system. This provides an easy interface to implement various real-life or research paper based transition sysetsm models directly.

Moreover, the ability to define parameters such as num_slots allows us to define a family of parameterized transition systems. This is particularly useful when running batch simulations.

However, the above style of defining transition system is inefficient. Especially, when running planning algorithms on large transition system, a large number of calls are made to states and delta function. Since there is non-trivial computation occurring in these functions, it slows the algorithms.

In such cases, it is efficient to use discrete graph representation of the transition system. We provide an easy interface to construct and visualize the equivalent graph representation of the defined transition system. This involves three steps:

• Instantiate your derived transition system class.
• Graphify the instance.
• Save to PNG the graph to a PNG for visualization.

Note: Graphs with more than 500 nodes cannot be saved to PNG. At present the best way to visualize such graphs is to serialize them and manually check them.

We demonstrate these steps next.

Instantiate CarParking¶

This is same as instantiating any class in Python.

In [39]:

tsys = CarParking(num_slots=5)

In case the initial state of the transition system is known, it can be set by calling initialize function as shown below. In our case, assume that parking lot starts empty.

The initial state of the transition system can be checked using init_state property.

In [40]:

tsys.initialize(0)
print("init_state:", tsys.init_state())

init_state: 0

Graphify¶

The graphify function returns a ggsolver.graph.Graph object that represents a multi-digraph. See Graph Class API and Graph Class Example for more information about Graph class.

Note: If any changes are made to the transition system after a call to graphify, the changes will not reflect in the graph. The graphify must be called again.

In [41]:

graph = tsys.graphify()

 [SUCCESS] <Graph with |V|=6, |E|=12> generated. 

Visualize using to_png function¶

A graph with less than 500 nodes can be visualized using to_png function. The to_png function requires one positional argument:

• fpath: Path to where the generated PNG should be stored.

In [42]:

# Define path where to save the generated PNG.
fpath = "out/car_parking_nolabels.png"

# Generate a PNG
graph.to_png(fpath)

# Show PNG in Jupyter Notebook
html = img2html(fpath)
IPython.display.HTML(html)

Out[42]:

As you may notice, the generated PNG has the structure as expected. However, it would be nice to be visualize what atomic propositions hold in which state and which edges correspond to which actions.

For this purpose, we pass two optional arguments to to_png function.

In [43]:

# Define path where to save the generated PNG.
fpath = "out/car_parking_labeled.png"

# Generate a PNG
graph.to_png(fpath, nlabel=["state", "label"], elabel=["input"])

# Show PNG in Jupyter Notebook
html = img2html(fpath)
IPython.display.HTML(html)

Out[43]:

Serialization¶

The graph of a transition system can be serialized into a dictionary. This allows us to save it or share it easily over a communication channel.

See Graph.Serialize() API Documentation to understand the components of generated dictionary.

In [44]:

graph.serialize()

Out[44]:

{'graph': {'nodes': 6,
  'edges': {0: {1: 1, 0: 1},
   1: {2: 1, 0: 1},
   2: {3: 1, 1: 1},
   3: {4: 1, 2: 1},
   4: {5: 1, 3: 1},
   5: {5: 1, 4: 1}},
  'node_properties': {'state': {'default': None,
    'dict': {0: 0, 1: 1, 2: 2, 3: 3, 4: 4, 5: 5}},
   'label': {'default': None,
    'dict': {0: ['empty'], 1: [], 2: [], 3: [], 4: [], 5: ['full']}}},
  'edge_properties': {'prob': {'default': None, 'dict': []},
   'input': {'default': None,
    'dict': [{'edge': (0, 1, 0), 'pvalue': 'enter'},
     {'edge': (0, 0, 0), 'pvalue': 'exit'},
     {'edge': (1, 2, 0), 'pvalue': 'enter'},
     {'edge': (1, 0, 0), 'pvalue': 'exit'},
     {'edge': (2, 3, 0), 'pvalue': 'enter'},
     {'edge': (2, 1, 0), 'pvalue': 'exit'},
     {'edge': (3, 4, 0), 'pvalue': 'enter'},
     {'edge': (3, 2, 0), 'pvalue': 'exit'},
     {'edge': (4, 5, 0), 'pvalue': 'enter'},
     {'edge': (4, 3, 0), 'pvalue': 'exit'},
     {'edge': (5, 5, 0), 'pvalue': 'enter'},
     {'edge': (5, 4, 0), 'pvalue': 'exit'}]}},
  'graph_properties': {'inp_domain': ['enter', 'exit'],
   'is_probabilistic': False,
   'actions': ['enter', 'exit'],
   'is_deterministic': True,
   'init_state': 0,
   'atoms': ['empty', 'full']}}}