crestdsl - Welcome¶

(I know, I know, I’m really busy though…)

crestdsl is an implementation of the CREST modelling language in Python. CREST is a formalism for hybrid systems modelling. It supports hierarchical component compositiion, synchronous communication, automaton-based discrete behaviour and a formal semantics.

crestdsl is an internal domain-specific language (DSL) and shipped as Python package. This means you can run it on pretty much any operating system!

crestdsl supports various use cases that include model creation and plotting, simulation and verification (using TCTL model checking). The main focus lies on simplicity and ease of use.

Try Me! (Browser-Demo)¶

You can try crestdsl directly in your browser. Just click the badge and wait for crestdsl to be loaded into a Jupyter instance inside your browser:

Note

This live demo is made possible due to the effort of the Binder project. Thanks!

You can use this link to launch an instance with some more system modelling examples:

Quick-Install¶

To run crestdsl on your machine, use the pre-built Docker image:

docker run -p 8888:8888 crestdsl/release

For installation of crestdsl on your local machine and a description of dependencies, refer to Installation.

Publications¶

Kli19: Stefan Klikovits. A Domain-Specific Language Approach to Hybrid CPS Modelling. PhD thesis, University of Geneva, 2019.
KCB18: Stefan Klikovits, Aurélien Coet, and Didier Buchs. ML4CREST: Machine Learning for CPS Models. In 2nd International Workshop on Model-Driven Engineering for the Internet-of-Things (MDE4IoT) at MODELS‘18, volume 2245 of CEUR Workshop Proceedings, 515–520. 01 2018. URL: http://ceur-ws.org/Vol-2245/mde4iot_paper_4.pdf.
KLB17: Stefan Klikovits, Alban Linard, and Didier Buchs. CREST - A Continuous, REactive SysTems DSL. In 5th International Workshop on the Globalization of Modeling Languages (GEMOC 2017), volume 2019 of CEUR Workshop Proceedings, 286–291. 2017. URL: http://ceur-ws.org/Vol-2019/gemoc_2.pdf.
KLB18a: Stefan Klikovits, Alban Linard, and Didier Buchs. CREST - A DSL for Reactive Cyber-Physical Systems. In Ferhat Khendek and Reinhard Gotzhein, editors, 10th System Analysis and Modeling Conference (SAM 2018), volume 11150 of Lecture Notes in Computer Science, 29–45. Springer, 01 2018. doi:10.1007/978-3-030-01042-3_3.
KLB18b: Stefan Klikovits, Alban Linard, and Didier Buchs. CREST formalization. Technical Report, Software Modeling and Verification Group, University of Geneva, 2018. doi:10.5281/zenodo.1284561.

Installation¶

This page describes the several ways of using crestdsl. Additionally to the local execution here, you can try crestdsl in your browser using Jupyter and Binder, as described on the crestdsl - Welcome page.

Docker¶

crestdsl is built upon various Python packages. The probably easiest way to start using crestdsl is via Docker. The crestdsl image contains the latest release of crestdsl and all dependencies. The image is based on Jupyter’s docker stacks, so you develop right in your browser.

docker run -p 8888:8888 crestdsl/release

Remember to map the image’s port 8888 to one of your host machine’s ports (here 8888 too).

Local file storage

If you want to your persist files, you should look into mounting a volume using docker’s -v directive, like this:

docker run -p 8888:8888 -v $(pwd):/home/jovyan/my_notebooks crestdsl/release

Note

The docker image is quite large to download (~2GB). Make sure to have a good internet connection (or go grab a coffee).

Local Installation¶

pip install crestdsl

Alternatively, to install from sources, clone the repository and install locally.

git clone https://github.com/crestdsl/CREST.git
cd CREST
pip install -e .

Note

crestdsl was developed using Python 3.6. You will certainly have problems using any version of Python 2. For versions < 3.6, you might run into issues, I haven’t tested it.

Required: Patched Z3 Prover

crestdsl makes heavy use of Microsoft Research’s Z3 Solver. In order to increase usability, we added some minor improvements. The sources of this custom Z3 fork can be found at https://github.com/stklik/z3.git

To install it, you will need Python, make, and a compiler such as GCC or Clang, as explained on the official Z3 repository. If you have all these dependencies, you can run the following code to automatically install it.

bash <(curl -fsSL http://github.com/crestdsl/CREST)

Optional: Jupyter

crestdsl has been developed to work well inside Jupyter notebooks. However, by default it will not install it. To make use of this very interactive Python engine, install it verification .. code-block:: none

pip install jupyter

For other means of installation or further information, visit the Jupyter installation page directly.

Optional: Graphviz

Some crestdsl modules require additional installed resources. For example, the crestdsl.ui.dotter module allows the plotting of system models using the graphviz package. Use your system’s package manager / Homebrew to install the following package on Linux / OS X:

graphviz

libgraphviz-dev

dvipng

For Windows users: I honestly have not tried it, but please let me know if you made it work.

Modelling¶

Note

You can try the code shown on this page directly in your browser by following this link:

crestdsl is shipped as Python library. After it’s Installation you can simply import it. On this page, we will look into the creation of system models, so let’s import the model subpackage.

import crestdsl.model as crest

Defining Resources¶

CREST (crestdsl’s underlying formalism) was created for the modelling of resource-flows such as light and electricity within cyber-physical systems. In CREST and crestdsl, resources are combinations of resource names and their value domains.

Resource names are simple strings, value domains can be infinite, such as real and integer, or discrete such as ["on", "off"], as shown for the switch below. crestdsl provides several resource types such as INT, REAL, INTEGER, FLOAT, etc.

electricity = crest.Resource("Watt", crest.REAL)  # a real-valued resource
switch = crest.Resource("switch", ["on", "off"])  # a discrete resource
light = crest.Resource("Lumen", crest.INTEGER)  # a (mathematical) integer resource
counter = crest.Resource("Count", crest.INT)  # an int resource (int32)
time = crest.Resource("minutes", crest.REAL)
celsius = crest.Resource("Celsius", crest.REAL)
fahrenheit = crest.Resource("Fahrenheit", crest.REAL)

Creating System Entities¶

The resources that we defined above, are be consumed, produced and transformed in the system model’s components. These components are specified as “entities”. To create an entity, we define a Python class that inherits from crest.Entity.

Each entity coherently defines its communication interface, internal structure and behaviour.

The communication interface is made up from Input and Output ports. These two port types allow each entity to access resources and data coming from outside its scope and expose its own resources and data to the outside. Each port has to be initialised with a resource and an initial value. The difference between the two port types is that inputs can only be read from within the entity, and outputs can only be written. Thus output port values cannot influence any of the entity’s behaviour.

The entity’s hybrid behaviour is defined using two concepts. A discrete state automaton and continuous value updates. The state automaton is created by defining State objects and Transitions between them. Transitions specify one source and target state and are guarded by functions or lambda functions which access the entity’s ports to return a boolean value that signifies whether the transition is enabled or not. Every entity has to specify one current state.

Continuous behaviour is modelled using Updates. Updates relate a state, a target port and a function. When the automaton is in the respective state, the update is “continuously” executed. The “continuous” execution is only of theoretical. Practically, at runtime, crestdsl’s Simulator takes care that the function is executed whenever necessary. The update’s function specifies two parameters: self and dt. When executing, self is a reference to the entity itself and dt is the time that passed since the update was last executed. Thus, updates can be used to model continuous behaviour. (We’ll see an example later in this tutorial.)

Note

crestdsl offers the definition of transitions and updates using decorator annotations such as @transition and @update to simplify the specification.

Below, we define the LightElement entity, which models the component that is responsible for producing light from electricity. It defines one input and one output port.

Note

Entities can also contain Influences, Local ports and subentities. We will see the use of these concepts further below.

class LightElement(crest.Entity):
    """This is a definition of a new Entity type. It derives from CREST's Entity base class."""

    """we define ports - each has a resource and an initial value"""
    electricity_in = crest.Input(resource=electricity, value=0)
    light_out = crest.Output(resource=light, value=0)

    """automaton states - don't forget to specify one as the current state"""
    on = crest.State()
    off = current = crest.State()

    """transitions and guards (as lambdas)"""
    off_to_on = crest.Transition(source=off, target=on, guard=(lambda self: self.electricity_in.value >= 100))
    on_to_off = crest.Transition(source=on, target=off, guard=(lambda self: self.electricity_in.value < 100))

    """
    update functions. They are related to a state, define the port to be updated and return the port's new value
    Remember that updates need two parameters: self and dt.
    """
    @crest.update(state=on, target=light_out)
    def set_light_on(self, dt=0):
        return 800

    @crest.update(state=off, target=light_out)
    def set_light_off(self, dt=0):
        return 0

Another Entity (The HeatElement)¶

It’s time to model the heating component of our growing lamp. Its functionality is simple: if the switch_in input is on, 1% of the electricity is converted to addtional heat under the lamp. Thus, for example, by providing 100 Watt, the temperature underneath the lamp grows by 1 degree centigrade.

class HeatElement(crest.Entity):
    """ Ports """
    electricity_in = crest.Input(resource=electricity, value=0)
    switch_in = crest.Input(resource=switch, value="off")  # the heatelement has its own switch
    heat_out = crest.Output(resource=celsius, value=0)      # and produces a celsius value (i.e. the temperature increase underneath the lamp)

    """ Automaton (States) """
    state = current = crest.State() # the only state of this entity

    """Update"""
    @crest.update(state=state, target=heat_out)
    def heat_output(self, dt):
        # When the lamp is on, then we convert electricity to temperature at a rate of 100Watt = 1Celsius
        if self.switch_in.value == "on":
            return self.electricity_in.value / 100
        else:
            return 0

A Logical Entity¶

CREST does not specify a special connector type that defines what is happening for multiple incoming influence, etc. Instead standard entities are used to define add, minimum and maximum calculation which is then written to the actual target port using an influence.

We call such entities logical, since they don’t have a real-world counterpart.

# a logical entity can inherit from LogicalEntity,
# to emphasize that it does not relate to the real world
class Adder(crest.LogicalEntity):
    heat_in = crest.Input(resource=celsius, value=0)
    room_temp_in = crest.Input(resource=celsius, value=22)
    temperature_out = crest.Output(resource=celsius, value=22)

    state = current = crest.State()

    @crest.update(state=state, target=temperature_out)
    def add(self, dt):
        return self.heat_in.value + self.room_temp_in.value

Composition of a System¶

Finally, we compose the entire GrowLamp entity based on the components we defined above. In CREST any system that is composed of multiple entities has to be hierarchically structured. This means that there is one “root” entity that contains all other entities. In our case, the root entity will be defined in the GrowLamp class. All other entities (i.e. the HeatElement, LightElement and Adder) will be defined as its subentities. Subentities are connected through influences and updates between their ports.

The reason for this strictly hierarchical definition is that this way we can easily reuse the GrowLamp as a subentity in an even bigger system.

Continuous Behaviour The GrowLamp below uses Local ports to hold data. Local ports behave just as input and output ports, except that they cannot be accessed from outside the entity’s scope.

Below, we can see that the update update_time is used to continuously increase the value of the on_time local. Every time the update is executed, the port’s value is increased by the time that has passed (dt).

Influences Influences “statically link” two ports. The influence’s source port’s value is permanently written to its target port, such that any modification of the source port is also reflected in its target port. Additionally, influences can also be defined as @influence decorators for entity methods. This results that the target port’s value is a function of the source port value. In the growing lamp this functionality is used to convert the temperature unit from fahrenheit to celsius (see fahrenheit_to_celsius).

Actions CREST allows the specificaiton of one further form of behaviour: Actions. Actions are functions that are executed every time a certain transition is fired. Below, the count_switching_on action is used to increase the on_count port every time the growing lamp is turned on.

class GrowLamp(crest.Entity):

    """ - - - - - - - PORTS - - - - - - - - - - """
    electricity_in = crest.Input(resource=electricity, value=0)
    switch_in = crest.Input(resource=switch, value="off")
    heat_switch_in = crest.Input(resource=switch, value="on")
    room_temperature_in = crest.Input(resource=fahrenheit, value=71.6)

    light_out = crest.Output(resource=light, value=3.1415*1000) # note that these are bogus values for now
    temperature_out = crest.Output(resource=celsius, value=4242424242) # yes, nonsense..., they are updated when simulated

    on_time = crest.Local(resource=time, value=0)
    on_count = crest.Local(resource=counter, value=0)

    """ - - - - - - - SUBENTITIES - - - - - - - - - - """
    lightelement = LightElement()
    heatelement = HeatElement()
    adder = Adder()


    """ - - - - - - - INFLUENCES - - - - - - - - - - """
    """
    Influences specify a source port and a target port.
    They are always executed, independent of the automaton's state.
    Since they are called directly with the source-port's value, a self-parameter is not necessary.
    """
    @crest.influence(source=room_temperature_in, target=adder.room_temp_in)
    def fahrenheit_to_celsius(value):
        return (value - 32) * 5 / 9

    # we can also define updates and influences with lambda functions...
    heat_to_add = crest.Influence(source=heatelement.heat_out, target=adder.heat_in, function=(lambda val: val))

    # if the lambda function doesn't do anything (like the one above) we can omit it entirely...
    add_to_temp           = crest.Influence(source=adder.temperature_out, target=temperature_out)
    light_to_light        = crest.Influence(source=lightelement.light_out, target=light_out)
    heat_switch_influence = crest.Influence(source=heat_switch_in, target=heatelement.switch_in)


    """ - - - - - - - STATES & TRANSITIONS - - - - - - - - - - """
    on = crest.State()
    off = current = crest.State()
    error = crest.State()

    off_to_on = crest.Transition(source=off, target=on, guard=(lambda self: self.switch_in.value == "on" and self.electricity_in.value >= 100))
    on_to_off = crest.Transition(source=on, target=off, guard=(lambda self: self.switch_in.value == "off" or self.electricity_in.value < 100))

    # transition to error state if the lamp ran for more than 1000.5 time units
    @crest.transition(source=on, target=error)
    def to_error(self):
        """More complex transitions can be defined as a function. We can use variables and calculations"""
        timeout = self.on_time.value >= 1000.5
        heat_is_on = self.heatelement.switch_in.value == "on"
        return timeout and heat_is_on

    """ - - - - - - - UPDATES - - - - - - - - - - """
    # LAMP is OFF or ERROR
    @crest.update(state=[off, error], target=lightelement.electricity_in)
    def update_light_elec_off(self, dt):
        # no electricity
        return 0

    @crest.update(state=[off, error], target=heatelement.electricity_in)
    def update_heat_elec_off(self, dt):
        # no electricity
        return 0



    # LAMP is ON
    @crest.update(state=on, target=lightelement.electricity_in)
    def update_light_elec_on(self, dt):
        # the lightelement gets the first 100Watt
        return 100

    @crest.update(state=on, target=heatelement.electricity_in)
    def update_heat_elec_on(self, dt):
        # the heatelement gets the rest
        return self.electricity_in.value - 100

    @crest.update(state=on, target=on_time)
    def update_time(self, dt):
        # also update the on_time so we know whether we overheat
        return self.on_time.value + dt

    """ - - - - - - - ACTIONS - - - - - - - - - - """
    # let's add an action that counts the number of times we switch to state "on"
    @crest.action(transition=off_to_on, target=on_count)
    def count_switching_on(self):
        """
        Actions are functions that are executed when the related transition is fired.
        Note that actions do not have a dt.
        """
        return self.on_count.value + 1

Simulation¶

Simulation allows us to execute the model and see its evolution. crestdsl’s simulator is located in the simultion module. In order to use it, we have to import it.

# import the simulator
from crestdsl.simulation import Simulator

After the import, we can use a simulator by initialising it with a system model. In our case, we will explore the GrowLamp system that we defined above.

gl = GrowLamp()
sim = Simulator(gl)

Stabilisation¶

The simulator will execute the system’s transitions, updates and influences until reaching a fixpoint. This process is referred to as stabilisation. Once stable, there are no more transitions can be triggered and all updates/influences/actions have been executed. After stabilisation, all ports have their correct values, calculted from preceeding ports.

In the GrowLamp, we see that the value’s of the temperature_out and light_out ports are wrong (based on the dummy values we defined as their initial values). After triggering the stabilisation, these values have been corrected.

The simulator also has a convenience API plot() that allows the direct plotting of the entity, without having to import and call the elk library.

sim.stabilise()
sim.plot()

Stabilisaiton also has to be called after the modification of input values, such that the new values are used to update any dependent ports. Further, all transitions have to be checked on whether they are enabled and executed if they are.

Below, we show the modification of the growlamp and stabilisation. Compare the plot below to the plot above to see that the information has been updated.

# modify the growlamp instance's inputs directly, the simulator points to that object and will use it
gl.electricity_in.value = 500
gl.switch_in.value = "on"
sim.stabilise()
sim.plot()

Time advance¶

Evidently, we also want to simulate the behaviour over time. The simulator’s advance(dt) method does precisely that, by advancing dt time units.

Below we advance 500 time steps. The effect is that the global system time is now t=500 (see the growing lamp’s title bar). Additionally, the local variable on_time, which sums up the total amount of time the automaton has spent in the on state, has the value of 500 too - Just as expected!

sim.advance(500)
sim.plot()

Verification¶

Get in Touch!¶

We are very proud of crestdsl, but we’d also like to hear from you.

If you think that there is something we should improve, please leave an issue on Github.

We also appreciate any other kind of feedback. So don’t be shy, you’re warmly encouraged to leave supportive comments, constructive criticism or cheerful wishes either on Github, or contact Stefan via email (stefan.klikovits@unige.ch).

Help Wanted!¶

We’re still working on a dedicated developer/contributor tutorial.

In the meantime, if you like what you see and want to help us make crestdsl even better, don’t hesitate to get in touch. We’ll do everything we can to help you get started.

API Documentation¶

The crestdsl package is the root of the library. It wraps all other subpackages that are needed for the creation of and interaction with CREST systems. For example, the model package contains all APIs required for the creation of a crestdsl model, the simulation package provides various Simulator classes, and the ui package can be used to plot a CREST diagram of a model.

Warning

This documentation is (unfortunately) not complete yet. Please bear with me. I will gradually extend it.

crestdsl.model package¶

Domain Model

crestdsl.model.datatypes module¶

crestdsl.model.datatypes.BOOL = <Types.BOOL: <class 'bool'>>¶: Datatype for boolean values.

crestdsl.model.datatypes.FLOAT = <Types.FLOAT: <class 'float'>>¶: Datatype for floating point values (computer floats). This will be translated to the SMT solvers 32bit Float theory.

crestdsl.model.datatypes.INT = <Types.INT: <class 'int'>>¶: Datatype for int values (computer floats). This will be translated to the SMT solvers 32 bit Int theory.

crestdsl.model.datatypes.INTEGER = <Types.INTEGER: 'integer'>¶: Datatype for integer values. (Actual integers, not computer int). This will be translated to the SMT solvers Integer theory.

crestdsl.model.datatypes.REAL = <Types.REAL: 'real'>¶: Datatype for real values. (Actual real, not computer floating points). This will be translated to the SMT solvers Real theory.

crestdsl.model.datatypes.STRING = <Types.STRING: <class 'str'>>¶: Datatype for character sequences.

class crestdsl.model.datatypes.Types¶

Bases: enum.Enum

An enum holding all datatypes. Sometimes it’s better to use Types.INT to clairfy that you’re using a type. It might also resolve ambiguities

Domain Model ¶

class crestdsl.model.Resource(unit, domain)¶

A resource is a value type for CREST models. Each port is initialised with a Resource that identifies the type of values it will hold. Note, that resouce objects should be centrally defined and reused, so that ports of the same resource can reference the same resource object.

Resources are created with a unit i.e. it’s name (e.g. Watt or Lumen) and a domain. The domain is either one of the crestdsl Datatypes or a list of discrete values.

class crestdsl.model.Entity(name='', parent=None)¶

Bases: crestdsl.model.meta.CrestObject

The base class of all CREST systems and components. It is meant to be subclassed.

To create a new entity, create from this class using e.g. class MyEntity(crest.Entity). Note, that you can implement (parameterized) constructors for your entities with __init__.

Communication Interface ¶

class crestdsl.model.Input(resource=None, value=None, name=None, parent=None)¶

Bases: crestdsl.model.ports.Port

An input port of an entity. Its value can only be read from inside the entity and set only from the outside. This means you should never write an input from inside its own entity!

__init__(resource=None, value=None, name=None, parent=None)¶

Parameters

resource (Resource) – A resource that specifies the types of values the port can take.
value (object) – An initial value that matches the resource.

class crestdsl.model.Output(resource=None, value=None, name=None, parent=None)¶

Bases: crestdsl.model.ports.Port

An output port of an entity. Its value can only be set from inside the entity and read only from the outside. This means you should never read an output from inside its own entity!

__init__(resource=None, value=None, name=None, parent=None)¶

Parameters

resource (Resource) – A resource that specifies the types of values the port can take.
value (object) – An initial value that matches the resource.

class crestdsl.model.Local(resource=None, value=None, name=None, parent=None)¶

Bases: crestdsl.model.ports.Port

A local port of an entity. Its value can only be set and read from the entity itself.

__init__(resource=None, value=None, name=None, parent=None)¶

Parameters

resource (Resource) – A resource that specifies the types of values the port can take.
value (object) – An initial value that matches the resource.

Behaviour Automaton (Discrete Behaviour)¶

class crestdsl.model.State(name=None, parent=None)¶

Bases: crestdsl.model.meta.CrestObject

A state for the behaviour automaton. States don’t have much functionality, but are necessary for transtions. Don’t forget to declare one of the states as current.

__init__(name=None, parent=None)¶

class crestdsl.model.Transition(source=None, target=None, guard=None, name='', parent=None)¶

Bases: crestdsl.model.meta.CrestObject

A transition between behaviour automaton states. Note that the source and target states have to be defined for the same entity as the transition itself.

Note

Pro-tip: To avoid repetition, you can initialise it with a list of source/target states (or str-names). This will automatically create a transition from/to each. Be careful, because the transition’s name will be autoamtically numbered on inititialisation.

__init__(source=None, target=None, guard=None, name='', parent=None)¶

Parameters

source (State or str or list) – The starting state of a transition. Either a state object, or the name (str) of it.
target (State or str or list) – The target state of a transition. Either a state object, or the name (str) of it.
guard (lambda or func) – The guard function implementation. This can be either a lambda expression or the reference to a function/method. (The guard HAS to take exactly one parameter: self)

isenabled()¶: Evaluates whether the transition is currently enabled.

@crestdsl.model.transition(source='', target='')¶

A decorator for the definition of a Transition. Decorate any method to make it a guarded transition.

Don’t forget to specify the source and target states.

Parameters

source (State or str or list) – The starting state of a transition. Either a state object, or the name (str) of it.
target (State or str or list) – The target state of a transition. Either a state object, or the name (str) of it.

class crestdsl.model.Action(transition, target, function, name='', parent=None)¶

Bases: crestdsl.model.meta.CrestObject

An Action whose function is executed when a certain automaton transition is triggered.

Note

Pro-tip: To avoid repetition, you can initialise it with a list of transitions (or str-names). This will automatically create an action for each transition. Be careful, because the action’s name will be autoamtically numbered on inititialisation.

__init__(transition, target, function, name='', parent=None)¶

Parameters

source (Transition or str) – The transition at which the update should be triggered. Either a transition object, or the name (str) of it.
target (Port or str) – The target port of the action. Either a port object, or the name (str) of it.
function (lambda or func) – A conversion function that calculates the target port’s value. (The function HAS to take exactly one parameter: self)

@crestdsl.model.action(*args, **kwargs)¶

A decorator for the definition of an Action. Decorate any method to make it an action function.

Don’t forget to specify the transition and target port.

Parameters

source (Transition or str) – The transition at which the update should be triggered. Either a transition object, or the name (str) of it.
target (Port or str) – The target port of the action. Either a port object, or the name (str) of it.

Continuous Behaviour ¶

class crestdsl.model.Influence(source, target, function=None, name='', parent=None)¶

Bases: crestdsl.model.meta.CrestObject

An influence between two ports. You can specify a conversiton function that modifies the source port’s value before writing it to the target port.

__init__(source, target, function=None, name='', parent=None)¶

Parameters

source (Port or str) – The starting port of the influence. Either a port object, or the name (str) of it.
target (Port or str) – The target port of the influence. Either a port object, or the name (str) of it.
function (lambda or func) – A conversion function that calculates the target port’s value. (The function HAS to take exactly one parameter value)

@crestdsl.model.influence(source='', target='')¶

A decorator for the definition of an Influence. Decorate any method to make it an influence between two ports.

Don’t forget to specify the source and target ports.

Parameters

source (Port or str) – The starting port of the influence. Either a port object, or the name (str) of it.
target (Port or str) – The target port of the influence. Either a port object, or the name (str) of it.

class crestdsl.model.Update(state, target, function, name='', parent=None)¶

Bases: crestdsl.model.meta.CrestObject

An Update whose function is continuously executed when the automaton is in a certain state.

Note

Pro-tip: To avoid repetition, you can initialise it with a list of states (or str-names). This will automatically create an update for each state to avoid repetition. Be careful, because the update’s name will be autoamtically numbered on inititialisation.

__init__(state, target, function, name='', parent=None)¶

Parameters

source (State or str) – The state in which the update should be executed. Either a state object, or the name (str) of it.
target (Port or str) – The target port of the update. Either a port object, or the name (str) of it.
function (lambda or func) – A conversion function that calculates the target port’s value. (The function HAS to take exactly two parameters: self and dt)

@crestdsl.model.update(*args, **kwargs)¶

A decorator for the definition of an Update. Decorate any method to make it an update function.

Don’t forget to specify the state and target port.

Parameters

source (State or str) – The state in which the update should be executed. Either a state object, or the name (str) of it.
target (Port or str) – The target port of the update. Either a port object, or the name (str) of it.

Input/Output Dependencies ¶

class crestdsl.model.Dependency(source, target)¶

Bases: crestdsl.model.meta.CrestObject

A Dependency object specifies that an output depends on an input. This is necessary to resolve circular dependencies.

Don’t use this class directly. Use the @dependency class decorator instead.

__init__(source, target)¶

Parameters

source (Output or str (output portname)) – The dependency source (i.e. the output port).
target (Input or str (input portname)) – The dependency target (i.e. the input port).

@crestdsl.model.nodependencies¶

A class-decorator to declare that a class’ outputs don’t depend in its inputs.

No params!

@crestdsl.model.dependency(source, target)¶

A class-decorator to declare that a class’s output depends on an input. This is necessary to resolve circular dependencies.

Parameters

source (Output or str (output portname)) – The dependency source (i.e. the output port).
target (Input or str (input portname)) – The dependency target (i.e. the input port).

crestdsl.model.systemcheck module¶

class crestdsl.model.SystemCheck(model)¶

Bases: object

Check whether an Entity object satisfies the basic structure (CREST syntax) checks.

check_action_sanity()¶: Check that each action is properly named, has a transition and from the same entity and a target port that is in the “targets” of the entity. Also verifies the signature of the action function.

check_all(exit_on_error=False)¶

Runs a series of system checks on the model and writes eventual errors to the log.

Parameters: exit_on_error (bool) – True: checking is aborted with an exception as soon as the first error is found? False: continue until the end, even if an error is found
Returns: True if all checks passed, False otherwise.
Return type: bool
Raises: AssertionError – If exit_on_error is True and an error is discovered, the method raises an AssertionError with information about the respective problem.

check_all_objects_have_names()¶: Assert that each entity has a name defined.

check_current_states()¶: Assert that each entity has a current state that is one of the states of the entity.

check_influence_sanity()¶: Check that each influence is properly named, has a source from the “sources” of an entity and a target port that is in the “targets” of the same entity. Also verifies the signature of the influence function.

check_objects_have_parents_and_are_not_referenced_twice()¶

check that ports, states, updates, influences and transitions have a parent specificaiton each.
Test that they also are only used once (i.e. they only appear once in the list)

check_port_connections()¶: Verify that a port has maximum one influence OR one update per state writing to it. when an influence is defined, no action can write to that port.

check_transition_sanity()¶: Check that the transitions are properly named, the states are from the same entity and that the guard has the correct signature.

check_update_sanity()¶: Check that each update is properly named, has a state and from the same entity and a target port that is in the “targets” of the entity. Also verifies the signature of the update function.

test_entity_hierarchy()¶: Assert that - each entity has only appears once in the children of another entity - there is exactly one entity - the root - that has no parent

crestdsl.model.api package¶

API Functions for Entities¶

crestdsl.model.api.get_name(entity)¶

Returns the name of a given entity.

Parameters: entity (Entity) – The entity whose name should be returned.
Returns: The entity’s name or the empty string if there is no name defined (usually the root).
Return type: str

crestdsl.model.api.get_current(entity)¶

Returns the current automaton state of a given entity.

Parameters: entity (Entity) – The entity whose current state should be accessed.
Returns: The entity’s current automaton state.
Return type: State

crestdsl.model.api.get_root(entity)¶

Returns the root entity of a system.

Parameters: entity (Entity) – Any entity within the system.
Returns: The system’s root entity.
Return type: Entity

crestdsl.model.api.get_parent(entity)¶

Returns the parent of a given entity.

Parameters: entity (Entity) – The entity whose parent should be returned.
Returns: The entity’s parent entity (or None).
Return type: Entity

crestdsl.model.api.get_children(entity)¶

Returns the child entities of a given entity.

Parameters: entity (Entity) – The entity whose children should be returned.
Returns: A list of the entity’s subentities.
Return type: list of Entity

crestdsl.model.api.get_sources(entity)¶

The “sources” ports of an entity. The sources ports are all ports that can be read by updates/transitions/influences. These are an entity’s inputs, locals and all subentities’ output ports.

Parameters: entity (Entity) – The entity whose sources should be returned.
Returns: The list of ports that can be read by modifiers.
Return type: list of Port

crestdsl.model.api.get_targets(entity)¶

The “targets” ports of an entity. The targets ports are all ports that can be written by updates and influences. These are an entity’s outputs, locals and all subentities’ input ports.

Parameters: entity (Entity) – The entity whose targets should be returned.
Returns: The list of ports that can be written by modifiers.
Return type: list of Port

Convenience API for Entities Creation¶

Warning

Only use these functions once the object has been created. (You can use them for example in the constructor.)

crestdsl.model.api.add(entity, name, obj)¶

Adds the object to the entity and register it as the name. This function is similar to setattr, but does some string resolving beforehand. That means you can e.g. pass a Transition object where source/target are passed by their string identifiers.

Note

This method requires an entity to be initialised aleady. Call this method e.g. from within __init__ and be careful of what you are doing.

Warning

You cannot use this function to override objects that are already linked before. I.e. You cannot reassign a state that is used in a transition/update or a port that is already used in an influence. Be especially be careful when overriding transitions that are used in actions! We cannot currently detect these issues.

Parameters

entity (Entity) – The entity that should be extended.
name (str) – The attribute name under which you want to save the object.
obj (CrestObject) – The object that you want to set.

crestdsl.model.api.pullup(*ports, **kwargs)¶

This method takes a subentity input or output ports, creates equivalent ports in their parent’s parent entity and connects them using influences.

Use kwargs to assign a specific name.

Note

This method requires an entity to be initialised aleady. Call this method e.g. from within __init__ and be careful of what you are doing.

Parameters

ports (list of Port) – A list of subentity ports that you want to pull up.
kwargs (list of str=Port) – A list of name=Port pairs, so that name will be the pulled up port’s name in this entity.

crestdsl.model.api.relay(*port_pairs, **kwargs)¶

A convenience function to quickly create many influences in an entity.

The method takes a port pairs and connects them using influences.

Use kwargs to assign a specific name.

Note

This method requires an entity to be initialised aleady. Call this method e.g. from within __init__ and be careful of what you are doing.

Parameters

ports (list of (Port,Port)-pairs) – A list of source and target ports between which an influence should be created.
kwargs (list of str=(Port,Port)) – A list of name=Port pairs, so that string will be used as the influence’s name.

crestdsl.model.api.dependencies(*port_pairs)¶

An alternative way to define dependencies for an entity.

Note

This method requires an entity to be initialised aleady. Call this method e.g. from within __init__ and be careful of what you are doing.

Parameters: ports (list of (Output,Input)-pairs) – A list of dependency source (output) and target (input) ports between which a dependency should be declared.

crestdsl.simulation package¶

The simulation package contains everything that’s required for the simulation of crestdsl systems.

crestdsl provides in fact several simulator implementations for the exploration of model evolution. They mostly provide the same API and functionality and differ in minor details of the implementation. Below, three of them are presented. Their difference lies in the way they deal with non-determinism. CREST systems can be non-deterministic if two or more transitions are enabled from the same, currently active state. Despite the fact that non-determinism is a vital aspect of CREST to model the random execution, it is of high interest to also support its resolution and manual selection of the transition to follow, e.g. for the deliberate exploration of specific system behaviour. The dealing with such non-determinism is the discriminating difference between the individual simulators.

The three simulator implementations treat such non-determinism as follows:

1. The first implementation, the most basic CREST simulator (Simulator), randomly chooses one enabled transition when it encounters non-determinism. It thus strictly follows the basic CREST semantics. This system is useful for initial explorations in non-deterministic models (e.g. to get a feeling for possible behaviour scenarios) and for general simulation of deterministic models.

2. Secondly, the InteractiveSimulator is used when it comes to manual exploration of a non-deterministic model. Anytime a situation with multiple enabled transitions is encountered, the simulator stops and prompts the user to make a choice. Evidently, this feature is meant for the exploration of smaller models, where such situations rarely occur. For highly non-deterministic models this form of exploration can become tedious.

3. The third simulator is the PlanSimulator. It can be used for the programmatic simulation of a system trace. The simulation is launched with a list of commands that helps to orchestrate the execution. The command list contains information about advance and port setting actions. Additionally, the ports can specify which transition to take, in case non-determinism is encountered. Thus, the PlanSimulator can be even used to precisely specify a certain system evolution and chosen behaviour. This capacity is highly useful for unit testing or the analysis of specific execution schedules. The specification of large execution plans can quickly become overwhelming, especially for large systems. Usually, execution plans are therefore machine generated, e.g. in combination with a state space exploration or formal verification scenario.

Note

This text is based on a part of Stefan Klikovits’s PhD Thesis [Kli19].

class crestdsl.simulation.Simulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)¶

The vanilla crestdsl simulator. It offers APIs to stabilise a system and advance time.

Additionally, there are shortcuts to get the execution trace and to plot the system.

__init__(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)¶

Create a new simulator object. In most cases you will only need ot declare the first system parameter.

All other parameters are rarely needed.

Parameters

system (Entity) – The system/entity whose evlution should be simulated
timeunit (crestdsl.model.REAL or crestdsl.model.INT) – Set this to decide whether the next transition time should be precise or round up to the next integer.
plotter (crestdsl.ui.elk or crestdsl.ui.dotter) – Modify the library that this simulator uses for drawing CREST diagrams.
default_to_integer_real (bool) – Should the SMT solver use INTEGER and REAL theories when encountering int/float datatypes (unless otherwise specified)?
record_traces (bool) – You can deactivate the recording of trace data. (Slightly more performance/memory friendly, although usually you wouldn’t notice.)
own_context (bool) – DON’T USE THIS! It’s a preliminary switch that should enable parallel execution at some point in the future.
max_step_size (numeric value) – This will only ever advance in steps of a certain maximum size. You can use it to increase the amount of trace data. Can also be useful for non-linear systems. (Although they aren’t really supported by crestdsl anyway)

system¶: A handle to the system that is being simulated. You can use it to e.g. modify input values

stabilise()¶: Stabilise the system. This includes propagation of all port values through influences and updates, then triggering any enabled transitions, then doing propagation again, and transitions, and … until a fixpoint is reached.

Warning

This can result in an infinite loop if your system has a cycle of enabled transitions.

stabilize()¶: For all the Americans out there. Does the same thing as stabilise().

advance(time_to_advance, consider_behaviour_changes=True)¶

Advance a certain amount of time in your system.

Parameters

time_to_advance (numeric) – The time advance that should be simulated
consider_behaviour_changes (bool) – You usually won’t have to modify this (so don’t!) Allows you to deactivate searching for if/else condition changes. It will be removed soon anyway!

advance_to_behaviour_change(consider_behaviour_changes=True)¶

Calculates when the next discrete change in behaviour will happen and advance as many time units. Note, this also does the according stabilisation, so you cannot stop “before” the behaviour change.

Parameters: consider_behaviour_changes (bool) – You usually won’t have to modify this (so don’t!) Allows you to deactivate searching for if/else condition changes. It will be removed soon anyway!

next_behaviour_change_time(excludes=None)¶

Calculates when the next discrete change in behaviour will happen.

Parameters: excludes (list of objects) – If you don’t care about behaviour changes in certain objects, use excludes to ignore them. Don’t use it unless you know what you’re doing!
Returns: Returns a tuple of (numeric, object) that states when the next behaviour change will happen (in time units), and in which object it will happen (i.e. a transition, update or influence)
Return type: tuple

trace¶: A handle to the TraceStore object that holds the ports values and states.

global_time¶: Return the global time value (i.e. the sum of all time advances)

plot(entity=None, **kwargs)¶

Create a drawing of the system. Uses the default plotter defined in the Config unless you specified a different library when you initialised.

Parameters

entity (Entity) – If you wish to plot something else than the simulator’s system. (Why would you, though?!)
kwargs (dict) – Anything defined as keyword argument will be passed on to the plotting library. This way you can parameterise things.

class crestdsl.simulation.InteractiveSimulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)¶

Bases: crestdsl.simulation.simulator.Simulator

This is a simulator will stop every time two transitions are enabled in the same entity at the same time and prompt the user for what to do.

Next to choosing a transition,uUsers can perform various actions (e.g. inspect variables, plot the system or stop the simulation.

class crestdsl.simulation.PlanSimulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)¶

Bases: crestdsl.simulation.simulator.Simulator

The PlanSimulator offers the same interface as the usual Simulator. However, it additionally allows the triggering of an execution_plan in the run_plan() method.

run_plan(execution_plan)¶

Executes a plan. The execution plan is a heterogeneous list of the following items:

numeric values: (specify time advances)

pairs of (numeric, {entity: transition}-dict): advance a certain time and choose transition, everytime non-determinism is encountered in entity

{port: value} dicts (for setting of input ports)

{entity: transitions} dicts (for resolving conflicts)

The list items will be iteratively consumed. If errors are observed they raise ValueError exceptions.

If there is non-determinism, but no dict specifies how to resolve it, then we fall back to randomness.

Here’s a documented example of a plan: [

# advance 10 time units: 10,

# set values: {entity.port : 33, entity.port2: -200}, # advance 20 time units and choose these transitions everytime there is a conflict in this period (20, {entity: entity.transition1, entity.subentity: entity.subentity.transition2} ),

# advance 33 time units. # When you hit a conflict, check if the first element is an entity-state dict # if the entity is a key in the first element, then pop it and # use it to reolve the conflict (otherwise choose randomly) # then continue until anothoer conflict or end of advance 33, {entity: entity.transitionA}, {entity: entity.transitionB}, {entity: entity.transitionA},

# if you have two entities and you don’t know which one will be conflicting first # (because they’ll have conflicts at the same time) # you can put them both in a dict and duplicate the dict. # the first one will pop the first dict, the second one the second dict:

444, {entity.subentity1: entity.subentity2.transA, entity.subentity2: entity.subentity2.transB}, {entity.subentity1: entity.subentity2.transA, entity.subentity2: entity.subentity2.transB},

]

Parameters: execution_plan (list) – The list of instructions that should be executed.
Raises: ValueError – In case there is something wrongly specified (e.g. take a transition that is not enabled, or so)

crestdsl.ui package¶

crestdsl.ui.plot(object, name='', **kwargs)¶

Submodules¶

crestdsl.ui.dotter module¶

crestdsl.ui.dotter.gen_Action(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Entity(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Influence(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Input(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Local(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_MetaEntity(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Output(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_State(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Transition(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.gen_Update(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.dotter.generate(object, name, parent=None, **kwargs)¶

crestdsl.ui.dotter.get_color(seed=None)¶

crestdsl.ui.dotter.plot(object_to_dot, name='', **kwargs)¶

List of plotter options:: updates = True update_labels = False transitions = True transition_labels = False influence_labels = False interface_only = False no_behaviour = False show_update_ports = False color_updates : False

crestdsl.ui.draw_statespace module¶

crestdsl.ui.draw_statespace.draw_plot(statespace)¶

crestdsl.ui.draw_statespace.draw_plotly(statespace, text_func=None, highlight=None, debug=False)¶

crestdsl.ui.draw_statespace.plot_layout(statespace)¶

crestdsl.ui.draw_statespace.plotly_data(statespace, text_func=None, highlight=None, debug=False)¶

crestdsl.ui.elk module¶

crestdsl.ui.elk.gen_Action(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_Entity(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_Influence(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_MetaEntity(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_Port(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_State(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_Transition(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.gen_Update(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.generate(object, name, parent)¶

crestdsl.ui.elk.generate_midpoint(obj, name='', parent=None, **kwargs)¶

crestdsl.ui.elk.generate_root(object_to_plot, name)¶: wraps the generated graph in a root entity

crestdsl.ui.elk.logger = <Logger crestdsl.ui.elk (WARNING)>¶: Produces JSON that can be interpreted by the Eclipse Layout Kernel (ELK). I tried to use OpenKieler’s elkjs.

crestdsl.ui.elk.plot(object_to_plot, name='', **kwargs)¶

crestdsl.ui.elk.show_json(object_to_plot, name='', **kwargs)¶

Verifiable Properties (Checks)¶

crestdsl.verification.check(arg)¶

Use this function to create a Check object. Checks are the basic form of verifiable properties. There are two types of checks, state checks and port checks. State checks assert that an entity is in a given state, port checks compare the value of a port to a constant or another port.

Use check(entity) == entity.stateA to create a state check, for instance.

Port checks are created using check(entity.port) <= 33 or `check(entity.port) != another.port

You can also combine these atomic checks to larger ones. The operators are: - conjunction (and): & - disjunction (or): | - negation (not): -

Parameters: arg (Entity or Port) – If you pass an entity, a StateCheck will be returned. If you pass in a Port, the function will create a PortCheck.
Returns: depending on what you put in, you will receive either a StateCheck or a PortCheck
Return type: StateCheck or PortCheck

Examples

>>> state_chk = check(entity) == entity.my_state
>>> port_chk = check(entity.port) == 33
>>> and_chk = state_chk & port_chk
>>> or_chk = state_chk | port_chk
>>> not_chk = -state_chk

Convenience API ¶

crestdsl.verification.after(time)¶

Initialises a Verifier that will test if formula is valid after a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. after(30) states that the formula has to hold after 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.before(time)¶

Initialises a Verifier that will test if formula is valid before a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. before(30) states that the formula has to hold in the initial 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.is_possible(check)¶

Test if it is possible to reach a system configuration described by check.

The TCTL formula will be EF(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.always(check)¶

Test if every reachable a system configuration satisfies the check.

The TCTL formula will be AG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.always_possible(check, within=None)¶

Test if it is always possible to reach a system configuration described by check.

Parameters

check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
within (numeric) – If specified, tests if the state can always be reached within a certain maximum time span. For example “Can we always raise the temperature within 30 minutes”.

Returns

The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.

Return type

Verifier

crestdsl.verification.never(check)¶

Test if a system configuration that adheres to``check`` can never be reached.

The TCTL formula will be AG(Not(check))

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.forever(check)¶

Test if there is one path where every state satisfies check.

The TCTL formula will be EG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

class crestdsl.verification.Verifier(system=None)¶

This class hosts the functionality for the verification API.

Notes

You shouldn’t create a Verifier object directly. Use the convenience API methods instead (e.g. ispossible() or always()).

after(time)¶

after(time)

Initialises a Verifier that will test if formula is valid after a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. after(30) states that the formula has to hold after 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

always(check)¶

always(check)

Test if every reachable a system configuration satisfies the check.

The TCTL formula will be AG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

always_possible(check, within=None)¶

always_possible(check, within=None)

Test if it is always possible to reach a system configuration described by check.

Parameters

check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
within (numeric) – If specified, tests if the state can always be reached within a certain maximum time span. For example “Can we always raise the temperature within 30 minutes”.

Returns

The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.

Return type

Verifier

before(time)¶

before(time)

Initialises a Verifier that will test if formula is valid before a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. before(30) states that the formula has to hold in the initial 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

check(draw_result=False)¶

Triggers the verification. This includes the compiling the tctl formula, explorating the statespace and then checking the formula on the statespace.

Parameters: draw_result (bool) – The verifier can draw the statespace and highlight the nodes that satisfy the formula. This is VERY slow though. So don’t run it if the statespace is bigger than a few dozen nodes.
Returns: The result of the model checking. I.e. if the formula holds on the root state of the state space.
Return type: bool

forever(check)¶

forever(check)

Test if there is one path where every state satisfies check.

The TCTL formula will be EG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

property formula¶: The current formula (as TCTL object).

is_possible(check)¶

is_possible(check)

Test if it is possible to reach a system configuration described by check.

The TCTL formula will be EF(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

never(check)¶

never(check)

Test if a system configuration that adheres to``check`` can never be reached.

The TCTL formula will be AG(Not(check))

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

Expert Model Checking API ¶

class crestdsl.verification.StateSpace(system=None, *args, **kwargs)¶

Creates a graph of initial node + stabilised nodes. Graph elements are SystemState objects.

This class is based on networkx.DiGraph. See networkx documentation for more info.

calculate_successors_for_node(ssnode)¶: CAREFUL!! this is the one where we only do one at a time! BUT: it’s faster than executing the parallel one on one thread

explore(iterations_left=1, iteration_counter=1, parallel=False)¶

Asserts that the graph is expanded so all paths have a minimum length i.e. the length to the leaves is at least a amount

Parameters

iterations_left (int) – How many iterations of exploration should be done (or None for “inifitely many”)
iteration_counter (int) – Don’t specify it. It’s for logging purposes only.
parallel (bool) – Unstable. Don’t use it!

explore_until_time(time)¶

Asserts that the graph is expanded so all paths have a minimum length i.e. the length to the leaves is at least a amount

Parameters: time (numeric) – The minimum length of all paths between root and the nodes

class crestdsl.verification.ModelChecker(statespace=None)¶

Create a ModelChecker that can explore a StateSpace. Use check() to trigger the exploration.

__init__(statespace=None)¶

Parameters: statespace (StateSpace) – The statespace (timed Kripke structure) that will be explored.

check(formula, systemstate=None)¶

Trigger the model checking implementation.

Parameters

formula (TCTLFormula) – A tctl formula object that specifies the property that should be checked.
systemstate (SystemState) – In case you want to execute the formula on a different state than the statespace’s root.

Returns

The result of the model checking. I.e. if the formula is satisfied.

Return type

bool

TCTL API ¶

class crestdsl.verification.tctl.Interval(start=0, end=inf, start_op=<built-in function ge>, end_op=<built-in function lt>)¶

Define an interval for the timed versions of the TCTL operators.

Use comparison operators (<, >, <=, >=, ==) to specify the bounds of the interval. Note, that you can only apply one operator at a time. (Use parenthesis!)

Examples

>>> intvl = Interval()  # [0, ∞)
>>> intvl2 = Interval() > 33  # (33, ∞)
>>> intvl3 = Interval() <= 42  # [0, 42]
>>> invtl4 = Interval() == 100  # [100, 100]
>>> invtl5 = (Interval() > 12) < 48  # (12, 48)

ends_before(value)¶

Test if the interval ends before a certain time.

Parameters: value (numeric) – The value you want to test.

ininterval(value)¶

Test if a value is inside the interval.

Parameters: value (numeric) – The value you want to test.

is_after(value)¶

Test if the interval starts after a certain time.

Parameters: value (numeric) – The value you want to test.

is_before(value)¶

Test if the interval ends before a certain time.

Parameters: value (numeric) – The value you want to test.

starts_after(value)¶

Test if the interval starts after a certain time.

Parameters: value (numeric) – The value you want to test.

starts_at(value)¶

Test if the interval starts at a certain time.

Parameters: value (numeric) – The value you want to test.

starts_at_or_after(value)¶

Test if the interval starts at or after a certain time.

Parameters: value (numeric) – The value you want to test.

class crestdsl.verification.tctl.TCTLFormula(formula)¶: The base class of all TCTL formulas. Don’t use it!

class crestdsl.verification.tctl.Not(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.And(phi, psi)¶

__init__(phi, psi)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)

class crestdsl.verification.tctl.Or(phi, psi)¶

__init__(phi, psi)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)

class crestdsl.verification.tctl.Implies(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.Equality(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.EU(phi, psi, interval=None)¶

__init__(phi, psi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.EF(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.EG(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AU(phi, psi, interval=None)¶

__init__(phi, psi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AF(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AG(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

crestdsl.config module¶

crestdsl.config.config = <crestdsl.config.ConfigObject object>¶: A global singleton object that holds various settings, e.g. for global choice of the default plotting library or the rounding precision of the output values. Import it with from crestdsl.config import config to access the properties.

See also

crestdsl.config.ConfigObject

class crestdsl.config.ConfigObject¶

An object that holds various configuration settings that are used throughout crestdsl.

approx = 100¶: precision for when we have to round z3’s fractions to actual numbers

consider_behaviour_changes = True¶: This should be True if you’re using conditinoal statements in your updates/influences/guards, etc.

property default_plotter¶

The default plotting library used.

What is the default plotting output library. Currently the choice is between elk and graphviz dot

epsilon = 1e-10¶: When converting from infinitesimal values to actual float numbers, what value should epsilon take? (Should be very small)

property interactive¶: This value tells us if we’re running in Jupyter or not.

plotformat = 'png'¶: When we’re in commandline and plotting graphviz to a file, we’ll use this format. Possible output values are listed here: https://www.graphviz.org/doc/info/output.html.

record_traces = True¶: Should the simulator record traces by default? (needs a small amount of more performance & memory)

remove_epsilon_transition_after = 5¶: If we detect the same transition doing lots of epsilon steps, we block it after this many detections.

property set_default_plotter¶

The default plotting library used.

What is the default plotting output library. Currently the choice is between elk and graphviz dot

ui_display_round = 4¶: When showing numbers in plots, to what precision should they be rounded?

use_integer_and_real = True¶: Should we replace Python’s int and float with Z3’s Integer and Real for simulation?