Skip to main content

SpotOnDocker is a utility which exposes some of spot ( functionality as a dockerized service.

Project description


SpotOnDocker is a utility which exposes some of spot's functions as a dockerized service. The functions can be called using client API provided in C++, Python, VB.NET and C#.

Note: In v0.1.0, only Python client API is available.

Supported spot Functions:

  • mp_class: Returns class of LTL formula in Manna-Pnueli hierarchy.
  • translate: Translates LTL formula to Buchi automaton.
  • contains: Checks if the language of an LTL formula is contained within another's.
  • equiv: Checks of the language of two LTL formulas is equivalent.
  • rand_ltl: Generates a random LTL formula.
  • get_ap: Gets the atomic propositions from given LTL formula.
  • to_string_latex: LaTeX-friendly writing of LTL formula.

Installation Instructions

Server Setup

  1. Install Docker. Skip if already installed.

  2. Get the latest version of spotondocker image.

    docker pull abhibp1993/spotondocker

Python Client Setup

The following packages are required.

  • networkx
  • docker
  • thrift (Apache)
pip3 install docker networkx thrift
pip3 install spotondocker

Example (Python Client API)

It is advisable to check if spot is available on system, if not use spotondocker.

    import spot
except ImportError:
    import spotondocker.client as client
    spot = client.SpotOnDockerClient()

SpotOnDockerClient() creates a docker container and sets up the server to send requests to

Call the spot functions (only the supported ones!) as usual. For example, to get the class of formula G(a -> Fb) in Manna Pnueli hierarchy, we can call

spot.mp_class('G(a -> Fb)')

which will return a verbose like safety, guarantee, ...

In case of translation, the SpotClient.translate(..) function returns a networkx.MultiDiGraph.

nx_graph = spot.translate("(p1 W 0) | Gp2")

The returned graph has several graph properties. See spotondocker.thrift to see a list of properties associated with graph. The node and edge attributes of nx_graph contains information like id and label.

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

spotondocker-0.1.2.tar.gz (14.5 kB view hashes)

Uploaded source

Built Distribution

spotondocker-0.1.2-py3-none-any.whl (16.4 kB view hashes)

Uploaded py3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page